L'exemple phare de modules - simplifie pour TPHOLs

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

2 files changed, 22 insertions, 102 deletions

diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
index d0ad6a5e2..d3e98ae4d 100644
--- a/test-suite/modules/Nat.v
+++ b/test-suite/modules/Nat.v
@@ -6,63 +6,14 @@ Hints Unfold le.
 
 Lemma le_refl:(n:nat)(le n n).
   Auto.
-Save.
+Qed.
 
-Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
-  Unfold le.
-  Intros.
-  Generalize H.
-  Clear H.
-  Elim H0.
-  Auto.
-  Auto.  
-Save.
-
-Lemma le_mono_S : (n,m:nat)(le n m) -> (le (S n) (S m)).
-  Unfold le.
-  NewInduction 1.
-  Auto.
-  Auto.
-Save.
-
-Hints Resolve le_mono_S.
-
-Lemma le_pred_mono : (n,m:nat) (le n m) -> (le (pred n) (pred m)).
-  Unfold le.
-  Induction 1.
-  Auto.
-  Intro.
-  Case m0.
-  Auto.
-  Intro.
-  Simpl.
-  Auto.
-Save.
+Require Le.
 
-Hints Resolve le_pred_mono.  
-
-Lemma le_S_mono : (m,n:nat)(le (S n) (S m)) -> (le n m).
-  Intros.
-  Change (le (pred (S n)) (pred (S m))).
-  Auto.
-Save.
-
-Hints Resolve le_S_mono.
+Lemma le_trans:(n,m,k:nat)(le n m) -> (le m k) -> (le n k).
+  EAuto with arith.
+Qed.
 
 Lemma le_antis:(n,m:nat)(le n m) -> (le m n) -> n=m.
-  NewInduction n.
-  Intros.
-  Inversion H0.
-  Reflexivity.
-
-  Intros.
-  Inversion H.
-  Auto.
-  Rewrite (IHn m0).
-  Auto.
-  Rewrite <- H2 in H.
-  Auto.
-  Rewrite <- H2 in H0.
-  Auto.
-Save.
-
+  EAuto with arith.
+Qed.
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index b16ab2809..9ba3fb2e6 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -15,7 +15,7 @@ Module Type PO.
 End PO.
 
 
-Module Pair[X:PO][Y:PO]<:PO.
+Module Pair[X:PO][Y:PO] <: PO.
   Definition T:=X.T*Y.T.
   Definition le:=[p1,p2]
     (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)).
@@ -23,66 +23,35 @@ Module Pair[X:PO][Y:PO]<:PO.
   Hints Unfold le.
 
   Lemma le_refl : (p:T)(le p p).
-  Info Auto.
-  Save.
+    Info Auto.
+  Qed.
 
   Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3).
-    Unfold le.
-    Intuition; Info EAuto.
-  Save.    
+    Unfold le; Intuition; Info EAuto.
+  Qed.    
 
   Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2).
     NewDestruct p1.  
     NewDestruct p2.
     Unfold le.
     Intuition.
-    Cut t=t1;Auto.
-    Cut t0=t2;Auto.
-    Intros.
-    Rewrite H0.
-    Rewrite H4.
+    CutRewrite t=t1.
+    CutRewrite t0=t2.
     Reflexivity.
-  Save.
-
-  Hints Resolve le_refl le_trans le_antis.
 
-End Pair.
+    Info Auto.
 
-Module Check_Pair [X:PO][Y:PO] : PO := (Pair X Y).
+    Info Auto.
+  Qed.
 
+End Pair.
 
-Module Type Fmono.
-  Declare Module X:PO.
-  Declare Module Y:PO.
 
-  Parameter f : X.T -> Y.T.
-  
-  Axiom f_mono : (x1,x2:X.T)(X.le x1 x2) -> (Y.le (f x1) (f x2)).
-End Fmono.
 
 Read Module Nat.
 
+Module NN := Pair Nat Nat.
 
-Module PlusMono:Fmono.
-  Module Y:=Nat.
-  Module X:=Pair Nat Nat.
-  
-  Definition f:=[p] (plus (fst p) (snd p)).
-
-  Lemma f_mono : (p1,p2:nat*nat)(X.le p1 p2) -> (le (f p1) (f p2)).
-    NewDestruct p1;NewDestruct p2.
-    Unfold X.le Nat.le f.
-    Simpl.
-    NewDestruct 1.
-    Induction H.
-  
-    Induction n.
-    Auto.
-    Simpl.
-    Apply Nat.le_mono_S.
-    Auto.
-
-    Simpl.
-    Auto.
-  Save.
-End PlusMono.
+Lemma zz_min : (p:NN.T)(NN.le (O,O) p).
+  Info Auto with arith.
+Qed.