The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> I had a quick look into the git history of Coq. It was first committed
> quite a while ago, in December 1997, just after the redesign of Coq's
> kernel by Jean-Christophe Filliâtre. [1] However, I think it's likely
> that `ex2` is even much older, predating the old SVN repo.
>
> [1]: Commit 2b62054dcccae08fdb5b61145e4b84d746e6faf1 (imported from SVN)

Indeed, ex2 can be traced back at least to Coq version 4.5 in 1988!
The date 1997 is however a typo, it should be read as 1999.

The redesign by Jean-Christophe Filliâtre started in a new fresh cvs
repository, hence the discontinuity of history. Curious people will
find in the main Coq archive an history of Coq versions and successive
version control systems used [2]. "Gallino-archeologists" may be also
interested in the history chapter of the reference manual [3], and
specifically in Huet's early-history section [4]!

[2] https://github.com/coq/coq/blob/v8.11/dev/doc/archive/versions-history.tex
[3] https://coq.inria.fr/refman/history.html
[4] https://coq.inria.fr/refman/history.html#version-1

> > > I wondered for some time for what reason there is `ex2` in Coq's stdlib.
> >
> > I guess the main difference is that is saves a "destruct" whenever
> > eliminating an exisist2-hypothesis and a "split" whenever proving one.
> 
> This looks like a valid point for `ex2`! Indeed, I sometimes find those
> long 'destruct chains' a bit annoying, e.g:
>
> 
>   pose proof my_lemma _ H as (x&L1&L2&L3).
> 
> 
> (Of course, I know that you can write an ltac that does this destructing
> for you, and I sometimes use this kind of ltac.)
> 
>
> Having n-ary conjunctions is also a nice alternative.

I'm not sure we have indeed to look for deep reasons about ex2. I was
personally not born at the time of version 4.5 but I suspect it was
just convenient to formulate some statements using ex2 (see attached
file for a 4.5 example).

Since it does not scale, my own view is that there is no reason to
specifically keep ex2, except for compatibility. However, we cannot
neglect the practical impact of using ex-of-and vs ex2, as Christian
and you emphasized, with different associated technical answers.

More generally, it has escaped to noone that the question of how to
exactly represent tuples is a difficult question! Mathematically
speaking, there is no difference between (A/\B)/\C, A/\(B/\C) or a
ternary A/\B/\C. Why would we have to care so much about the exact
parenthesizing when starting to formalizing? Why couldn't proof
assistants reason more semantically? Maybe one (longer term) answer
(among others) would be to natively support associative operators in
the core of the logic?

Best,

Hugo


(****************************************************************************)
(*                                                                          *)
(*                          Constructions in Caml                           *)
(*                                                                          *)
(*                             Lemme de Newman                              *)
(*                                                                          *)
(*             CAML V2.5    Constructions V4.5     Vernacular V1.2          *)
(****************************************************************************)
(* Charger Base, puis Relations *)

(* On definit  la confluence, la confluence locale, et la           *)
(* noetherianite de R. Pour cela on dit que deux points sont        *)
(* coherents s'ils se reduisent sur un meme point.                  *)

Definition coherent [x:A][y:A]<A>Ex2((Rstar x),(Rstar y)).
  
Theorem coherent_intro  (x:A)(y:A)(z:A)
                        (Rstar x z)->(Rstar y z)->(coherent x y)
Proof   [x:A][y:A][z:A][h1:(Rstar x z)][h2:(Rstar y z)]
                [C:Prop][h:(w:A)(Rstar x w)->(Rstar y w)->C](h z h1 h2).  
  
(* Un cas particulierement simple de coherence : *)

Lemma Rstar_coherent
        (x:A)(y:A)(Rstar x y)->(coherent x y)
Proof   [x:A][y:A][h:(Rstar x y)](coherent_intro x y y h (Rstar_re y)).  
  
(* Etre coherent est une propriete symetrique *)

Lemma coherent_sym
                (x:A)(y:A)(coherent x y)->(coherent y x)
Proof   [x:A][y:A][h:(coherent x y)]
                (h (coherent y x) 
                   ([w:A][h1:(Rstar x w)][h2:(Rstar y w)]
                         (coherent_intro y x w h2 h1))).  
  
Definition confluent    
        [x:A](y:A)(z:A)(Rstar x y)->(Rstar x z)->(coherent y z).  
  
Definition local_confluent
        [x:A](y:A)(z:A)(R x y)->(R x z)->(coherent y z).  
  
Definition noetherien
        (x:A)(P:A->Prop)((y:A)((z:A)(R y z)->(P z))->(P y))->(P x).  
  
(* Les hypotheses generales du theoreme *)

Hypothesis Hyp1:noetherien.  
  Hypothesis Hyp2:(x:A)(local_confluent x).  
  
(* L'hypothese d'induction *)

Variable        x:A.  
  Hypothesis    hyp_ind:(u:A)(R x u)->(confluent u).  
  
(* Preuve de la confluence en x *)

Variables       y,z:A.  
  Hypothesis    h1:(Rstar x y).  
  Hypothesis    h2:(Rstar x z).  
  
(* cas particulier x->u et u->*y *)

Variable        u:A.  
  Hypothesis    t1:(R x u).  
  Hypothesis    t2:(Rstar u y).  
  
(* Le cas du diagramme : on a aussi x->v et v->*z *)

Variable        v:A.  
  Hypothesis    u1:(R x v).  
  Hypothesis    u2:(Rstar v z).  
  
Theorem diagramme       (coherent y z)
Proof (Hyp2 x u v t1 u1         
        (coherent y z)                  (* confluence locale de x pour u,v *)
                                        (* fournit w, u->*w et v->*w *)
        ([w:A][s1:(Rstar u w)][s2:(Rstar v w)]
  (hyp_ind u t1 y w t2 s1               (* la confluence en u => 
coherent(y,w)*)
        (coherent y z)                  (* qui fournit a, y->*a et z->*a*)
        
        ([a:A][v1:(Rstar y a)][v2:(Rstar w a)]
  (hyp_ind v u1 a z                     (* la confluence en v => 
coherent(a,z)*)
        (Rstar_trans v w a s2 v2) u2    (* qui fournit b, a->*b et z->*b*)
        (coherent y z)

        ([b:A][w1:(Rstar a b)][w2:(Rstar z b)]
  (coherent_intro y z b (Rstar_trans y a b v1 w1) w2))))))).  
  
Discharge v.  
  
Theorem casRxy  (coherent y z)
Proof (Rstar_Rind x z h2 
                ([v:A][w:A](coherent y w))
                (coherent_sym x y (Rstar_coherent x y h1))      (* cas x=z *)
                diagramme).                                     (* cas 
x->v->*z*)
Discharge u.     

Theorem Ind_proof (coherent y z)
Proof (Rstar_Rind x y h1 ([u:A][v:A](coherent v z))
                (Rstar_coherent x z h2)                         (* cas x=y*)
                casRxy).                                        (* cas 
x->u->*z*)

Discharge x.                    

Theorem NewmanProof (x:A)(confluent x)
Proof [x:A](Hyp1 x confluent Ind_proof).  

(* Timing: 4.18s sur SUN 3-60 apres Base et Relations *)