Proving se poi il resto in Coq

Question

Sono nuovo a Coq e sto cercando di dimostrare qualcosa piuttosto semplice

Lemma eq_if_eq: forall A1 A2, (se beq_nat a1 a2 a1 poi a2 altro) = A1 .

Ho faticato con una soluzione pubblicata di seguito, ma penso che ci sia un modo migliore. Idealmente, mi piacerebbe scrivere in modo pulito su beq_nat a1 a2 mentre inserisco i valori del caso nella lista delle ipotesi. C'è una tattica t tale che usando t (beq_nat a1 a2) produce due sottocasi, una dove beq_nat a1 a2 = true e un'altra dove beq_nat a1 a2 = false? Ovviamente, induction è molto vicino ma perde la sua storia.

Ecco la prova ho faticato attraverso:

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

Si scopre che la semplice tattica remember era tutto ciò di cui avevo bisogno. Qualcosa sulla falsariga di remember (beq_nat a1 a2) as e; induction e; etc.

Answer 2

Generalmente per questo genere di cose, io uso il eqn variante di distruzione. Sarebbe come questo:

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

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

Aggiungerà l'uguaglianza come un'ipotesi. Nella variante 8.4, è possibile sostituire il punto interrogativo con un nome da dare all'ipotesi.

Answer 3

La tattica che fa quello che stai chiedendo è case_eq. Il seguente script dimostra il lemma in 8.4pl3:

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