Mise en forme des theories

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 301 insertions, 292 deletions

diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
index 9c53a28be..d97943280 100644
--- a/theories/Relations/Newman.v
+++ b/theories/Relations/Newman.v
@@ -23,24 +23,23 @@ Let Rstar_Rstar' := Rstar_Rstar' A R.
 Definition coherence (x y:A) := ex2 (Rstar x) (Rstar y).
 
 Theorem coherence_intro :
- forall x y z:A, Rstar x z -> Rstar y z -> coherence x y.
-Proof
-  fun (x y z:A) (h1:Rstar x z) (h2:Rstar y z) =>
-    ex_intro2 (Rstar x) (Rstar y) z h1 h2.
+  forall x y z:A, Rstar x z -> Rstar y z -> coherence x y.
+Proof fun (x y z:A) (h1:Rstar x z) (h2:Rstar y z) =>
+  ex_intro2 (Rstar x) (Rstar y) z h1 h2.
   
 (** A very simple case of coherence : *)
 
 Lemma Rstar_coherence : forall x y:A, Rstar x y -> coherence x y.
- Proof
-   fun (x y:A) (h:Rstar x y) => coherence_intro x y y h (Rstar_reflexive y).  
+Proof
+  fun (x y:A) (h:Rstar x y) => coherence_intro x y y h (Rstar_reflexive y).  
   
 (** coherence is symmetric *)
 Lemma coherence_sym : forall x y:A, coherence x y -> coherence y x.
- Proof
-   fun (x y:A) (h:coherence x y) =>
-     ex2_ind
-       (fun (w:A) (h1:Rstar x w) (h2:Rstar y w) =>
-          coherence_intro y x w h2 h1) h.
+Proof
+  fun (x y:A) (h:coherence x y) =>
+    ex2_ind
+      (fun (w:A) (h1:Rstar x w) (h2:Rstar y w) =>
+        coherence_intro y x w h2 h1) h.
 
 Definition confluence (x:A) :=
   forall y z:A, Rstar x y -> Rstar x z -> coherence y z.  
@@ -54,68 +53,67 @@ Definition noetherian :=
   
 Section Newman_section.
 
-(** The general hypotheses of the theorem *)
+  (** The general hypotheses of the theorem *)
 
-Hypothesis Hyp1 : noetherian.
-Hypothesis Hyp2 : forall x:A, local_confluence x.  
+  Hypothesis Hyp1 : noetherian.
+  Hypothesis Hyp2 : forall x:A, local_confluence x.  
   
-(** The induction hypothesis *)
+  (** The induction hypothesis *)
 
-Section Induct.
-  Variable x : A.
-  Hypothesis hyp_ind : forall u:A, R x u -> confluence u.  
+  Section Induct.
+    Variable x : A.
+    Hypothesis hyp_ind : forall u:A, R x u -> confluence u.  
   
-(** Confluence in [x] *)
+    (** Confluence in [x] *)
 
-  Variables y z : A.  
-  Hypothesis h1 : Rstar x y.  
-  Hypothesis h2 : Rstar x z.  
+    Variables y z : A.  
+    Hypothesis h1 : Rstar x y.  
+    Hypothesis h2 : Rstar x z.  
   
-(** particular case [x->u] and [u->*y]   *)
-Section Newman_.
-  Variable u : A.  
-  Hypothesis t1 : R x u.  
-  Hypothesis t2 : Rstar u y.  
+    (** particular case [x->u] and [u->*y]   *)
+    Section Newman_.
+      Variable u : A.  
+      Hypothesis t1 : R x u.  
+      Hypothesis t2 : Rstar u y.  
+      
+      (** In the usual diagram, we assume also [x->v] and [v->*z] *)
+      
+      Theorem Diagram : forall (v:A) (u1:R x v) (u2:Rstar v z), coherence y z.
+      Proof
+       (* We draw the diagram ! *)
+      fun (v:A) (u1:R x v) (u2:Rstar v z) =>
+	ex2_ind
+	 (* local confluence in x for u,v *)
+	 (* gives w, u->*w and v->*w *)
+	(fun (w:A) (s1:Rstar u w) (s2:Rstar v w) =>
+          ex2_ind
+              (* confluence in u => coherence(y,w) *)
+              (* gives a, y->*a and z->*a *)
+          (fun (a:A) (v1:Rstar y a) (v2:Rstar w a) =>
+            ex2_ind
+              (* confluence in v => coherence(a,z) *)
+              (* gives b, a->*b and z->*b *)
+            (fun (b:A) (w1:Rstar a b) (w2:Rstar z b) =>
+              coherence_intro y z b (Rstar_transitive y a b v1 w1) w2)
+            (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2))
+          (hyp_ind u t1 y w t2 s1)) (Hyp2 x u v t1 u1).
   
-(** In the usual diagram, we assume also [x->v] and [v->*z] *)
-
-Theorem Diagram : forall (v:A) (u1:R x v) (u2:Rstar v z), coherence y z.
-
-Proof
-   (* We draw the diagram ! *)
-  fun (v:A) (u1:R x v) (u2:Rstar v z) =>
-    ex2_ind
-       (* local confluence in x for u,v *)
-       (* gives w, u->*w and v->*w *)
-      (fun (w:A) (s1:Rstar u w) (s2:Rstar v w) =>
-         ex2_ind
-            (* confluence in u => coherence(y,w) *)
-            (* gives a, y->*a and z->*a *)
-           (fun (a:A) (v1:Rstar y a) (v2:Rstar w a) =>
-              ex2_ind
-                 (* confluence in v => coherence(a,z) *)
-                 (* gives b, a->*b and z->*b *)
-                (fun (b:A) (w1:Rstar a b) (w2:Rstar z b) =>
-                   coherence_intro y z b (Rstar_transitive y a b v1 w1) w2)
-                (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2))
-           (hyp_ind u t1 y w t2 s1)) (Hyp2 x u v t1 u1).
-  
-Theorem caseRxy : coherence y z.
-Proof
-  Rstar_Rstar' x z h2 (fun v w:A => coherence y w)
-    (coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*)
-    Diagram.                                     (*i case x->v->*z i*)
-End Newman_.
-
-Theorem Ind_proof : coherence y z.
-Proof
-  Rstar_Rstar' x y h1 (fun u v:A => coherence v z)
-    (Rstar_coherence x z h2) (*i case x=y i*)
-    caseRxy.                                   (*i case x->u->*z i*)
-End Induct.
-
-Theorem Newman : forall x:A, confluence x.
-Proof fun x:A => Hyp1 x confluence Ind_proof.  
+      Theorem caseRxy : coherence y z.
+      Proof
+        Rstar_Rstar' x z h2 (fun v w:A => coherence y w)
+	(coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*)
+	Diagram.                                     (*i case x->v->*z i*)
+    End Newman_.
+
+    Theorem Ind_proof : coherence y z.
+    Proof
+      Rstar_Rstar' x y h1 (fun u v:A => coherence v z)
+      (Rstar_coherence x z h2) (*i case x=y i*)
+      caseRxy.                                   (*i case x->u->*z i*)
+  End Induct.
+
+  Theorem Newman : forall x:A, confluence x.
+  Proof fun x:A => Hyp1 x confluence Ind_proof.  
 
 End Newman_section.
 
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 317a5ed07..3cae9d571 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -22,75 +22,77 @@ Section Properties.
   Variable R : relation A.
 
   Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y.
-
-Section Clos_Refl_Trans.
-
-  Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R).
-apply Build_preorder.
-exact (rt_refl A R).
-
-exact (rt_trans A R).
-Qed.
-
-
-
-Lemma clos_rt_idempotent :
- incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R).
-red in |- *.
-induction 1; auto with sets.
-intros.
-apply rt_trans with y; auto with sets.
-Qed.
-
-  Lemma clos_refl_trans_ind_left :
-   forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
-     P M ->
-     (forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) ->
-     forall a:A, clos_refl_trans A R M a -> P a.
-intros.
-generalize H H0.
-clear H H0.
-elim H1; intros; auto with sets.
-apply H2 with x; auto with sets.
-
-apply H3.
-apply H0; auto with sets.
-
-intros.
-apply H5 with P0; auto with sets.
-apply rt_trans with y; auto with sets.
-Qed.
-
-
-End Clos_Refl_Trans.
-
-
-Section Clos_Refl_Sym_Trans.
-
-  Lemma clos_rt_clos_rst :
-   inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R).
-red in |- *.
-induction 1; auto with sets.
-apply rst_trans with y; auto with sets.
-Qed.
-
-  Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R).
-apply Build_equivalence.
-exact (rst_refl A R).
-
-exact (rst_trans A R).
-
-exact (rst_sym A R).
-Qed.
-
-  Lemma clos_rst_idempotent :
-   incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
-     (clos_refl_sym_trans A R).
-red in |- *.
-induction 1; auto with sets.
-apply rst_trans with y; auto with sets.
-Qed.
-
-End Clos_Refl_Sym_Trans.
+  
+  Section Clos_Refl_Trans.
+
+    Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R).
+    Proof.
+      apply Build_preorder.
+      exact (rt_refl A R).
+      
+      exact (rt_trans A R).
+    Qed.
+
+    Lemma clos_rt_idempotent :
+      incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R).
+    Proof.
+      red in |- *.
+      induction 1; auto with sets.
+      intros.
+      apply rt_trans with y; auto with sets.
+    Qed.
+
+    Lemma clos_refl_trans_ind_left :
+      forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
+	P M ->
+	(forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) ->
+	forall a:A, clos_refl_trans A R M a -> P a.
+    Proof.
+      intros.
+      generalize H H0.
+      clear H H0.
+      elim H1; intros; auto with sets.
+      apply H2 with x; auto with sets.
+      
+      apply H3.
+      apply H0; auto with sets.
+
+      intros.
+      apply H5 with P0; auto with sets.
+      apply rt_trans with y; auto with sets.
+    Qed.
+
+
+  End Clos_Refl_Trans.
+
+
+  Section Clos_Refl_Sym_Trans.
+
+    Lemma clos_rt_clos_rst :
+      inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R).
+    Proof.
+      red in |- *.
+      induction 1; auto with sets.
+      apply rst_trans with y; auto with sets.
+    Qed.
+
+    Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R).
+    Proof.
+      apply Build_equivalence.
+      exact (rst_refl A R).
+      exact (rst_trans A R).
+      exact (rst_sym A R).
+    Qed.
+
+    Lemma clos_rst_idempotent :
+      incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
+      (clos_refl_sym_trans A R).
+    Proof.
+      red in |- *.
+      induction 1; auto with sets.
+      apply rst_trans with y; auto with sets.
+    Qed.
+  
+  End Clos_Refl_Sym_Trans.
 
 End Properties.
\ No newline at end of file
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index e0f13b46e..977135fab 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -10,63 +10,62 @@
 
 Section Relation_Definition.
 
-   Variable A : Type.
-   
-   Definition relation := A -> A -> Prop.
+  Variable A : Type.
+  
+  Definition relation := A -> A -> Prop.
 
-   Variable R : relation.
+  Variable R : relation.
    
 
-Section General_Properties_of_Relations.
-
-  Definition reflexive : Prop := forall x:A, R x x.
-  Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.
-  Definition symmetric : Prop := forall x y:A, R x y -> R y x.
-  Definition antisymmetric : Prop := forall x y:A, R x y -> R y x -> x = y.
-
-  (* for compatibility with Equivalence in  ../PROGRAMS/ALG/  *)
-  Definition equiv := reflexive /\ transitive /\ symmetric.
-
-End General_Properties_of_Relations.
-
+  Section General_Properties_of_Relations.
+    
+    Definition reflexive : Prop := forall x:A, R x x.
+    Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.
+    Definition symmetric : Prop := forall x y:A, R x y -> R y x.
+    Definition antisymmetric : Prop := forall x y:A, R x y -> R y x -> x = y.
 
+    (* for compatibility with Equivalence in  ../PROGRAMS/ALG/  *)
+    Definition equiv := reflexive /\ transitive /\ symmetric.
 
-Section Sets_of_Relations.
+  End General_Properties_of_Relations.
 
-   Record preorder : Prop := 
-     {preord_refl : reflexive; preord_trans : transitive}.
 
-   Record order : Prop := 
-     {ord_refl : reflexive;
-      ord_trans : transitive;
-      ord_antisym : antisymmetric}.
 
-   Record equivalence : Prop := 
-     {equiv_refl : reflexive;
-      equiv_trans : transitive;
-      equiv_sym : symmetric}.
-   
-   Record PER : Prop :=  {per_sym : symmetric; per_trans : transitive}.
-
-End Sets_of_Relations.
+  Section Sets_of_Relations.
+    
+    Record preorder : Prop := 
+      { preord_refl : reflexive; preord_trans : transitive}.
+    
+    Record order : Prop := 
+      { ord_refl : reflexive;
+	ord_trans : transitive;
+	ord_antisym : antisymmetric}.
+    
+    Record equivalence : Prop := 
+      { equiv_refl : reflexive;
+	equiv_trans : transitive;
+	equiv_sym : symmetric}.
+    
+    Record PER : Prop :=  {per_sym : symmetric; per_trans : transitive}.
 
+  End Sets_of_Relations.
 
 
-Section Relations_of_Relations.
+  Section Relations_of_Relations.
+    
+    Definition inclusion (R1 R2:relation) : Prop :=
+      forall x y:A, R1 x y -> R2 x y.
+    
+    Definition same_relation (R1 R2:relation) : Prop :=
+      inclusion R1 R2 /\ inclusion R2 R1.
+    
+    Definition commut (R1 R2:relation) : Prop :=
+      forall x y:A,
+	R1 y x -> forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & R1 z y'.
 
-  Definition inclusion (R1 R2:relation) : Prop :=
-    forall x y:A, R1 x y -> R2 x y.
+  End Relations_of_Relations.
 
-  Definition same_relation (R1 R2:relation) : Prop :=
-    inclusion R1 R2 /\ inclusion R2 R1.
-   
-  Definition commut (R1 R2:relation) : Prop :=
-    forall x y:A,
-      R1 y x -> forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & R1 z y'.
 
-End Relations_of_Relations.
-
-   
 End Relation_Definition.
 
 Hint Unfold reflexive transitive antisymmetric symmetric: sets v62.
@@ -75,4 +74,4 @@ Hint Resolve Build_preorder Build_order Build_equivalence Build_PER
   preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl
   equiv_trans equiv_sym per_sym per_trans: sets v62.
 
-Hint Unfold inclusion same_relation commut: sets v62.
\ No newline at end of file
+Hint Unfold inclusion same_relation commut: sets v62.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index b538620d1..e4918d40e 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -24,7 +24,7 @@ Require Import List.
 Section Transitive_Closure.
   Variable A : Type.
   Variable R : relation A.
-
+  
   Inductive clos_trans (x: A) : A -> Prop :=
     | t_step : forall y:A, R x y -> clos_trans x y
     | t_trans :
@@ -48,16 +48,16 @@ End Reflexive_Transitive_Closure.
 Section Reflexive_Symetric_Transitive_Closure.
   Variable A : Type.
   Variable R : relation A.
-
+  
   Inductive clos_refl_sym_trans : relation A :=
     | rst_step : forall x y:A, R x y -> clos_refl_sym_trans x y
     | rst_refl : forall x:A, clos_refl_sym_trans x x
     | rst_sym :
-        forall x y:A, clos_refl_sym_trans x y -> clos_refl_sym_trans y x
+      forall x y:A, clos_refl_sym_trans x y -> clos_refl_sym_trans y x
     | rst_trans :
-        forall x y z:A,
-          clos_refl_sym_trans x y ->
-          clos_refl_sym_trans y z -> clos_refl_sym_trans x z.
+      forall x y z:A,
+        clos_refl_sym_trans x y ->
+        clos_refl_sym_trans y z -> clos_refl_sym_trans x z.
 End Reflexive_Symetric_Transitive_Closure.
 
 
@@ -92,18 +92,18 @@ End Disjoint_Union.
 
 
 Section Lexicographic_Product.
-(* Lexicographic order on dependent pairs *)
+  (* Lexicographic order on dependent pairs *)
 
-Variable A : Set.
-Variable B : A -> Set.
-Variable leA : A -> A -> Prop.
-Variable leB : forall x:A, B x -> B x -> Prop.
+  Variable A : Set.
+  Variable B : A -> Set.
+  Variable leA : A -> A -> Prop.
+  Variable leB : forall x:A, B x -> B x -> Prop.
 
-Inductive lexprod : sigS B -> sigS B -> Prop :=
-  | left_lex :
+  Inductive lexprod : sigS B -> sigS B -> Prop :=
+    | left_lex :
       forall (x x':A) (y:B x) (y':B x'),
         leA x x' -> lexprod (existS B x y) (existS B x' y')
-  | right_lex :
+    | right_lex :
       forall (x:A) (y y':B x),
         leB x y y' -> lexprod (existS B x y) (existS B x y').
 End Lexicographic_Product.
@@ -117,9 +117,9 @@ Section Symmetric_Product.
 
   Inductive symprod : A * B -> A * B -> Prop :=
     | left_sym :
-        forall x x':A, leA x x' -> forall y:B, symprod (x, y) (x', y)
+      forall x x':A, leA x x' -> forall y:B, symprod (x, y) (x', y)
     | right_sym :
-        forall y y':B, leB y y' -> forall x:A, symprod (x, y) (x, y').
+      forall y y':B, leB y y' -> forall x:A, symprod (x, y) (x, y').
 
 End Symmetric_Product.
 
@@ -131,34 +131,34 @@ Section Swap.
   Inductive swapprod : A * A -> A * A -> Prop :=
     | sp_noswap : forall x x':A * A, symprod A A R R x x' -> swapprod x x'
     | sp_swap :
-        forall (x y:A) (p:A * A),
-          symprod A A R R (x, y) p -> swapprod (y, x) p.
+      forall (x y:A) (p:A * A),
+        symprod A A R R (x, y) p -> swapprod (y, x) p.
 End Swap.
 
 
 Section Lexicographic_Exponentiation.
-
-Variable A : Set.
-Variable leA : A -> A -> Prop.
-Let Nil := nil (A:=A).
-Let List := list A.
-
-Inductive Ltl : List -> List -> Prop :=
-  | Lt_nil : forall (a:A) (x:List), Ltl Nil (a :: x)
-  | Lt_hd : forall a b:A, leA a b -> forall x y:list A, Ltl (a :: x) (b :: y)
-  | Lt_tl : forall (a:A) (x y:List), Ltl x y -> Ltl (a :: x) (a :: y).
-
-
-Inductive Desc : List -> Prop :=
-  | d_nil : Desc Nil
-  | d_one : forall x:A, Desc (x :: Nil)
-  | d_conc :
+  
+  Variable A : Set.
+  Variable leA : A -> A -> Prop.
+  Let Nil := nil (A:=A).
+  Let List := list A.
+  
+  Inductive Ltl : List -> List -> Prop :=
+    | Lt_nil : forall (a:A) (x:List), Ltl Nil (a :: x)
+    | Lt_hd : forall a b:A, leA a b -> forall x y:list A, Ltl (a :: x) (b :: y)
+    | Lt_tl : forall (a:A) (x y:List), Ltl x y -> Ltl (a :: x) (a :: y).
+
+
+  Inductive Desc : List -> Prop :=
+    | d_nil : Desc Nil
+    | d_one : forall x:A, Desc (x :: Nil)
+    | d_conc :
       forall (x y:A) (l:List),
         leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
 
-Definition Pow : Set := sig Desc.
-
-Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b).
+  Definition Pow : Set := sig Desc.
+  
+  Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b).
 
 End Lexicographic_Exponentiation.
 
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 6578f6c85..938d514df 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -13,16 +13,19 @@ Require Export Relation_Operators.
 Require Export Operators_Properties.
 
 Lemma inverse_image_of_equivalence :
- forall (A B:Set) (f:A -> B) (r:relation B),
-   equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
-intros; split; elim H; red in |- *; auto.
-intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
+  forall (A B:Set) (f:A -> B) (r:relation B),
+    equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
+Proof.
+  intros; split; elim H; red in |- *; auto.
+  intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
 Lemma inverse_image_of_eq :
- forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
-split; red in |- *;
- [  (* reflexivity *) reflexivity
- |  (* transitivity *) intros; transitivity (f y); assumption
- |  (* symmetry *) intros; symmetry  in |- *; assumption ].
-Qed.
\ No newline at end of file
+  forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
+Proof.
+  split; red in |- *;
+    [  (* reflexivity *) reflexivity
+      |  (* transitivity *) intros; transitivity (f y); assumption
+      |  (* symmetry *) intros; symmetry  in |- *; assumption ].
+Qed.
+
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
index eda581e8d..8dfacf2cf 100644
--- a/theories/Relations/Rstar.v
+++ b/theories/Relations/Rstar.v
@@ -11,77 +11,84 @@
 (** Properties of a binary relation [R] on type [A] *)
 
 Section Rstar.
+  
+  Variable A : Type.  
+  Variable R : A -> A -> Prop.  
 
-Variable A : Type.  
-Variable R : A -> A -> Prop.  
-
-(** Definition of the reflexive-transitive closure [R*] of [R] *)
-(** Smallest reflexive [P] containing [R o P] *)
-
-Definition Rstar (x y:A) :=
-  forall P:A -> A -> Prop,
-    (forall u:A, P u u) -> (forall u v w:A, R u v -> P v w -> P u w) -> P x y.  
+  (** Definition of the reflexive-transitive closure [R*] of [R] *)
+  (** Smallest reflexive [P] containing [R o P] *)
 
-Theorem Rstar_reflexive : forall x:A, Rstar x x.
- Proof
-   fun (x:A) (P:A -> A -> Prop) (h1:forall u:A, P u u)
-     (h2:forall u v w:A, R u v -> P v w -> P u w) => 
-     h1 x.  
+  Definition Rstar (x y:A) :=
+    forall P:A -> A -> Prop,
+      (forall u:A, P u u) -> (forall u v w:A, R u v -> P v w -> P u w) -> P x y.  
   
-Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z.
- Proof
-   fun (x y z:A) (t1:R x y) (t2:Rstar y z) (P:A -> A -> Prop)
-     (h1:forall u:A, P u u) (h2:forall u v w:A, R u v -> P v w -> P u w) =>
-     h2 x y z t1 (t2 P h1 h2).  
+  Theorem Rstar_reflexive : forall x:A, Rstar x x.
+  Proof.
+    unfold Rstar. intros x P P_refl RoP. apply P_refl.
+  Qed.
+
+  Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z.
+  Proof.
+    intros x y z R_xy Rstar_yz.
+    unfold Rstar.
+    intros P P_refl RoP. apply RoP with (v:=y).
+      assumption.
+      apply Rstar_yz; assumption.
+  Qed.
+
+  (** We conclude with transitivity of [Rstar] : *)
+
+  Theorem Rstar_transitive :
+    forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z.
+  Proof.
+    intros x y z Rstar_xy; unfold Rstar in Rstar_xy.
+    apply Rstar_xy; trivial.
+    intros u v w R_uv fz Rstar_wz.
+    apply Rstar_R with (y:=v); auto.
+  Qed.
+
+  (** Another characterization of [R*] *)
+  (** Smallest reflexive [P] containing [R o R*] *)
+
+  Definition Rstar' (x y:A) :=
+    forall P:A -> A -> Prop,
+      P x x -> (forall u:A, R x u -> Rstar u y -> P x y) -> P x y.  
+
+  Theorem Rstar'_reflexive : forall x:A, Rstar' x x.
+  Proof.
+    unfold Rstar'; intros; assumption.
+  Qed.
   
-(** We conclude with transitivity of [Rstar] : *)
-
-Theorem Rstar_transitive :
- forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z.
- Proof
-   fun (x y z:A) (h:Rstar x y) =>
-     h (fun u v:A => Rstar v z -> Rstar u z) (fun (u:A) (t:Rstar u z) => t)
-       (fun (u v w:A) (t1:R u v) (t2:Rstar w z -> Rstar v z)
-          (t3:Rstar w z) => Rstar_R u v z t1 (t2 t3)).  
-
-(** Another characterization of [R*] *)
-(** Smallest reflexive [P] containing [R o R*] *)
-
-Definition Rstar' (x y:A) :=
-  forall P:A -> A -> Prop,
-    P x x -> (forall u:A, R x u -> Rstar u y -> P x y) -> P x y.  
-
-Theorem Rstar'_reflexive : forall x:A, Rstar' x x.
- Proof
-   fun (x:A) (P:A -> A -> Prop) (h:P x x)
-     (h':forall u:A, R x u -> Rstar u x -> P x x) => h.
+  Theorem Rstar'_R : forall x y z:A, R x z -> Rstar z y -> Rstar' x y.
+  Proof.
+    unfold Rstar'. intros x y z Rxz Rstar_zy P Pxx RoP.
+    apply RoP with (u:=z); trivial.
+  Qed.
   
-Theorem Rstar'_R : forall x y z:A, R x z -> Rstar z y -> Rstar' x y.
- Proof
-   fun (x y z:A) (t1:R x z) (t2:Rstar z y) (P:A -> A -> Prop) 
-     (h1:P x x) (h2:forall u:A, R x u -> Rstar u y -> P x y) => 
-     h2 z t1 t2.  
+  (** Equivalence of the two definitions: *)
+
+  Theorem Rstar'_Rstar : forall x y:A, Rstar' x y -> Rstar x y.
+  Proof.
+    intros x z Rstar'_xz; unfold Rstar' in Rstar'_xz.
+    apply Rstar'_xz.
+      exact (Rstar_reflexive x).
+      intro y; generalize x y z; exact Rstar_R.
+  Qed.
   
-(** Equivalence of the two definitions: *)
-
-Theorem Rstar'_Rstar : forall x y:A, Rstar' x y -> Rstar x y.
- Proof
-   fun (x y:A) (h:Rstar' x y) =>
-     h Rstar (Rstar_reflexive x) (fun u:A => Rstar_R x u y).  
+  Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y.
+  Proof.
+    intros.
+    apply H.
+      exact Rstar'_reflexive.
+      intros u v  w R_uv Rs'_vw. apply Rstar'_R with (z:=v).
+        assumption.
+        apply Rstar'_Rstar; assumption.
+  Qed.
+
+  (** Property of Commutativity of two relations *)
   
-Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y.
- Proof
-   fun (x y:A) (h:Rstar x y) =>
-     h Rstar' (fun u:A => Rstar'_reflexive u)
-       (fun (u v w:A) (h1:R u v) (h2:Rstar' v w) =>
-          Rstar'_R u w v h1 (Rstar'_Rstar v w h2)).  
-
-
-(** Property of Commutativity of two relations *)
-
-Definition commut (A:Set) (R1 R2:A -> A -> Prop) :=
-  forall x y:A,
-    R1 y x -> forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & R1 z y'.
-
+  Definition commut (A:Set) (R1 R2:A -> A -> Prop) :=
+    forall x y:A,
+      R1 y x -> forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & R1 z y'.
 
 End Rstar.