Udowodnienie jeśli wtedy jeszcze w Coq

Question

Jestem nowy na Coq i próbuję coś udowodnić dość podstawowe

Lemma eq_if_eq: forall A1 A2 (jeśli beq_nat A1 A2 następnie a2 innego a1) = a1 .

Natknąłem się na rozwiązanie przedstawione poniżej, ale myślę, że musi być lepszy sposób. Idealnie, chciałbym, aby czysto przypadek na beq_nat a1 a2 podczas umieszczania wartości sprawy na liście hipotezy. Czy istnieje taktyka t taka, że ​​użycie t (beq_nat a1 a2) daje dwie pod-kolumny, jedną gdzie beq_nat a1 a2 = true i drugą, gdzie beq_nat a1 a2 = false? Oczywiście, induction jest bardzo blisko, ale traci swoją historię.

Oto dowód Walczyłem przez:

Proof. 
Hint Resolve beq_nat_refl. 
Hint Resolve beq_nat_eq. 
Hint Resolve beq_nat_true. 
Hint Resolve beq_nat_false. 
intros. 
compare (beq_nat a1 a2) true. 
intros. assert (a1 = a2). auto. 
replace (beq_nat a1 a2) with true. auto. 
intros. assert (a1 <> a2). apply beq_nat_false. 
apply not_true_is_false. auto. 
assert (beq_nat a1 a2 = false). apply not_true_is_false. auto. 
replace (beq_nat a1 a2) with false. auto. 
Qed. 

Answer 1

Okazuje się, że taktyka remember była wszystkim, czego potrzebowałem. Coś podobnego do linii remember (beq_nat a1 a2) as e; induction e; etc.

Answer 2

Generalnie do tego rodzaju rzeczy, używam wariant destruct eqn. Wyglądałoby to tak:

destruct (beq_nat a1 a2) as []_eqn. (* Coq <= 8.3 *) 

destruct (beq_nat a1 a2) as []eqn:? (* Coq >= 8.4 *) 

Dodaje równość jako hipotezę. W wariancie 8.4 można zastąpić znak zapytania nazwą, aby nadać jej hipotezę.

Answer 3

Taktyka, która spełnia to, o co prosisz, to case_eq. Poniższy skrypt potwierdza lemat w 8.4pl3:

intros. 
case_eq (beq_nat a1 a2). 
intuition. 
apply beq_nat_true_iff in H. 
intuition. 
intuition.