coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Difference between dot and semicolon in a proof
- Date: Tue, 19 Jul 2016 10:50:42 +1000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f49.google.com
- Ironport-phdr: 9a23:WBqFshwpmw/tpJHXCy+O+j09IxM/srCxBDY+r6Qd0ekfIJqq85mqBkHD//Il1AaPBtSDra8cwLaO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwud7yzR9aZ05z//tvx0qWbWx9Piju5bOE6BzSNhiKViPMrh5B/IL060BrDrygAUe1XwWR1OQDbxE6ktY/jtKJkpi9Xorcq89NKeaT8ZaUxC7JCXxo8NGVg4dDouALDBReO+XIGUy1ClwdLDhPF8BDlV43w9Cr7t/Z48CafNMzyC7szXGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==
Now it makes sense why the proof was not working with replacing semicolon by dot. Thank you Jonathan and Benjamin.
-Mukesh TiwariOn Mon, Jul 18, 2016 at 5:45 PM, Benjamin Werner <benjamin.werner AT inria.fr> wrote:
There is a difference between dot and semicolon when the application of a tactic produces more than one subgoal.Then, the tactic(s) appearing after the semicolon is applied to all the subgoals. When the tacticis after a dot, it is only applied to the first goal.You can make your proof a « oneliner » (ie. get rid of all dots) by using semicolon and thebracket notation:tac; [tac1 | tacB | tacC]applies tac, and then tacA to the first produced subgoal (produced by tac), tacB to the second, etcBenjaminLe 18 juil. 2016 à 03:45, mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> a écrit :If I replace all the semicolons by dots then It is not provable by following the same tactics.Hi Everyone,Pardon me if this is stupid question, but I am trying to understand the difference between dot (.) and semicolon (;) in Coq. My understanding is that we can interchange the dot and semicolon in Coq file. If you add dot after each tactic then you see the intermediate steps/calculation after applying the tactic to goal, and if you don't want to see the intermediate steps then use semicolon to combine multiple tactics.
Currently I am trying to go though the coq-graph [1] code.
Lemma Union_dec :
forall (e1 e2 : U_set) (x : U),
{e1 x} + {~ e1 x} -> {e2 x} + {~ e2 x} -> Union e1 e2 x -> {e1 x} + {e2 x}.
Proof.
intros; case H.
left; trivial.
intros; case H0; intros.
right; trivial.
absurd (Union e1 e2 x). apply Not_union; trivial.
trivial.
Qed.
Lemma Union_dec :
forall (e1 e2 : U_set) (x : U),
{e1 x} + {~ e1 x} -> {e2 x} + {~ e2 x} -> Union e1 e2 x -> {e1 x} + {e2 x}.
Proof.
intros. case H.
left. trivial.
intros. case H0. intros.
right. trivial.
absurd (Union e1 e2 x). apply Not_union. trivial.
trivial.and goal is
U : Set
e1, e2 : U_set
x : U
H : {e1 x} + {~ e1 x}
H0 : {e2 x} + {~ e2 x}
H1 : Union e1 e2 x
n : ~ e1 x
============================
~ e2 x
subgoal 2 (ID 51) is:
Union e1 e2 x
Regards,
Mukesh Tiwari
[1] https://github.com/coq-contribs/graph-basics/blob/master/Sets.v
- [Coq-Club] Difference between dot and semicolon in a proof, mukesh tiwari, 07/18/2016
- Re: [Coq-Club] Difference between dot and semicolon in a proof, Jonathan Leivent, 07/18/2016
- Re: [Coq-Club] Difference between dot and semicolon in a proof, Benjamin Werner, 07/18/2016
- Re: [Coq-Club] Difference between dot and semicolon in a proof, mukesh tiwari, 07/19/2016
Archive powered by MHonArc 2.6.18.