Come convinco coq che (A/\ B)/\ C == A/\ B/\ C?

Question

Nella mia prova mi imbatto in problemi in cui c'è un nelle mie ipotesi, e ho bisogno di dimostrare (A /\ B) /\ C. Questi sono logicamente esattamente gli stessi, ma coq non li risolverà con assumption..

Ho risolto questi problemi applicando un assioma, ma esiste un modo più elegante (e corretto) per gestirli?

Answer 1

Quindi il modo in cui sono andato a questo proposito è da definire il mio lemma,

Lemma conj_assoc : forall A B C, A /\ (B /\ C) <-> (A /\ B) /\ C. 

Questo è uno implica l'altro.

intros. split. dividerà questo in due obiettivi.

1. A /\ (B /\ C) -> (A /\ B) /\ C
2. (A /\ B) /\ C -> A /\ (B /\ C)

Proving ognuna di queste è circa la stessa. Per (1),

• intro Habc. per ottenere il presupposto dalla dimensione della mano sinistra.
• destruct Habc as [Ha Hbc]. destruct Hbc as [Hb Hc]. per ottenere le ipotesi individuali.
• auto per utilizzare queste ipotesi.

Lascio a voi di lavorare fuori (2) ma è molto simile.

Poi Qed.

Answer 2

Come un suggerimento generale, se avete qualcosa come questo che si sospetta essere ovvio, controllare la libreria standard. Ecco come: Locate "/\". produce una risposta che risolve il Notation per noi,

Notation   Scope  
"A /\ B" := and A B : type_scope 
         (default interpretation) 

Ora possiamo emettere il comando, SearchAbout and. per vedere ciò che è di portata, e scoprire che and_assoc testimoni l'implicazione che ti interessa, infatti. , puoi prendere spunto dallo dall'intuizione: la tattica intuition può sfruttare questa implicazione da sola.

Lemma conj_example : forall A B C D, 
    (A /\ B) /\ C -> (A /\ (B /\ C) -> D) -> D. 
Proof. intuition. Qed. 

Answer 3

Se si dispone di A /\ B /\ C come un presupposto, e il vostro obiettivo è (A /\ B) /\ C, è possibile utilizzare la tattica tauto. Questa tattica risolve tutte le tautologie nel calcolo proposizionale. C'è anche una tattica firstorder che può risolvere alcune formule con quantificatori.

Se si dispone di A /\ B /\ C e si desidera passare (A /\ B) /\ C come argomento per un lemma, sarà necessario lavorare un po 'di più.Un metodo è quello di impostare (A /\ B) /\ C come un obiettivo intermedio e dimostrarlo:

assert ((A /\ B) /\ C). tauto. 

Se A, B e C sono grandi espressioni, è possibile utilizzare una tattica composto da abbinare sopra l'ipotesi H : A /\ B /\ C e applicare la tattica tauto ad esso . Questo è un approccio ambiguo, eccessivo in questo caso, ma utile in situazioni più complesse in cui si desidera automatizzare una dimostrazione con molti casi simili.

match type of H with ?x /\ ?y /\ ?z => 
    assert (x /\ (y /\ z)); [tauto | clear H] 
end. 

C'è un modo più semplice, ovvero applicare un lemma noto che esegue la trasformazione.

apply and_assoc in H. 

È possibile trovare il lemma sfogliando la documentazione della libreria. Puoi anche cercarlo. Questo non è il lemma più facile da cercare perché è un'equivalenza e gli strumenti di ricerca sono orientati verso implicazioni e uguaglianze. È possibile utilizzare SearchPattern (_ /\ _ /\ _). per cercare i lemmi del modulo forall x1 … xn, ?A /\ ?B /\ ?C (dove ?A, ?B e ?C può essere una qualsiasi espressione). È possibile utilizzare SearchRewrite (_ /\ _ /\ _) per cercare i lemmi del modulo forall x1 … xn, (?A /\ ?B /\ ?C) = ?D. Sfortunatamente, questo non trova quello che cerchiamo, che è un lemma del modulo forall x1 … xn, (?A /\ ?B /\ ?C) <-> ?D. Che cosa funziona è

Coq < SearchPattern (_ <-> (_ /\ _ /\ _)) 
and_assoc: forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C