Coqチラシの裏

Coqチラシの裏

CoqCheatSheetを補完するとも思えない。

前提が

H : A /\ B refine (and_ind _ H). , refine (match H with conj H0 H1 => _ end).
H : A \/ B refine (or_ind _ _ H). , refine (match H with or_introl H0 => _ | or_intror H0 => _ end).
H : ~P refine (H _).
H : forall x:A, ... refine (H _).
H : exists x:P, ... refine (ex_ind _ H). , refine (match H with ex_intro x H0 => _ end).
H : C x y .. = C a b ..
H : C x y .. = D a b ..
H : x = y
H : False refine (False_ind _ H). , exact (match H with end).

ゴールが

A -> B refine (fun H => _).
A /\ B refine (conj _ _).
A \/ B refine (or_introl B _). , refine (or_intror A _).
~P refine (fun H => _).
forall x:A, ... refine (fun x => _).
exists x:P, ... (証拠 t : P に対して) refine (ex_intro (fun x => P x) t _).
x = x exact (eq_refl x). , exact (refl_equal x).
True exact I.