Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Difference between dot and semicolon in a proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Difference between dot and semicolon in a proof


Chronological Thread 
  • From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Difference between dot and semicolon in a proof
  • Date: Mon, 18 Jul 2016 11:45:30 +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-f44.google.com
  • Ironport-phdr: 9a23:R0RaZxWU5DOam6PzJMqaK2yoEhXV8LGtZVwlr6E/grcLSJyIuqrYZheOt8tkgFKBZ4jH8fUM07OQ6PG4HzBQqsrR+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0p82YP1UArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBK79ZuEzSaFSJDUgKWE8osPx5jfZSg7a42YfX34W2gZJHAHf7VmuW4ryvzD6quti0TObe8z3TKwxcTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

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.

If I replace all the semicolons by dots then It is not provable by following the same tactics.

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



Archive powered by MHonArc 2.6.18.

Top of Page