Modules dans COQ\!\!\!\!

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

13 files changed, 644 insertions, 0 deletions

diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v
new file mode 100644
index 000000000..9d8c49ef7
--- /dev/null
+++ b/test-suite/modules/Nametab.v
@@ -0,0 +1,100 @@
+Module M.
+  Definition id:=[x:Set]x.
+  Module M.
+    Definition zero:(id nat):= O.
+    Definition id:=Set.
+    Definition nacik:id:=nat.
+  End M.
+End M.
+
+Module M.
+Module N.
+Module K.
+Definition id:=Set.
+End K.
+End N.
+End M.
+
+
+Locate id.
+Locate K.id.
+Locate N.K.id.
+Locate M.N.K.id.
+Locate Top.M.N.K.id.
+Locate K.
+Locate N.K.
+Locate M.N.K.
+Locate Scratch.M.N.K.
+Locate N.
+Locate M.N.
+Locate Scratch.M.N.
+Locate M.
+Locate Scratch.M.
+
+(*
+#trace Nametab.push;;
+#trace Nametab.push_short_name;;
+#trace Nametab.freeze;;
+#trace Nametab.unfreeze;;
+#trace Nametab.exists_cci;;
+*)
+
+Module M.
+Module M[X:SIG].
+Module M[X,Y:SIG].
+Module M[X:SIG;Y:SIG].
+Module M[X,Y:SIG;X,Z:SIG].
+Module M[X:SIG][Y:SIG].
+Module M[X,Y:SIG][X,Z:SIG].
+Module M:SIG.
+Module M[X:SIG]:SIG.
+Module M[X,Y:SIG]:SIG.
+Module M[X:SIG;Y:SIG]:SIG.
+Module M[X,Y:SIG;X,Z:SIG]:SIG.
+Module M[X:SIG][Y:SIG]:SIG.
+Module M[X,Y:SIG][X,Z:SIG]:SIG.
+Module M:=(M N).
+Module M[X:SIG]:=(M N).
+Module M[X,Y:SIG]:=(M N).
+Module M[X:SIG;Y:SIG]:=(M N).
+Module M[X,Y:SIG;X,Z:SIG]:=(M N).
+Module M[X:SIG][Y:SIG]:=(M N).
+Module M[X,Y:SIG][X,Z:SIG]:=(M N).
+Module M:SIG:=(M N).
+Module M[X:SIG]:SIG:=(M N).
+Module M[X,Y:SIG]:SIG:=(M N).
+Module M[X:SIG;Y:SIG]:SIG:=(M N).
+Module M[X,Y:SIG;X,Z:SIG]:SIG:=(M N).
+Module M[X:SIG][Y:SIG]:SIG:=(M N).
+Module M[X,Y:SIG][X,Z:SIG]:SIG:=(M N).
+
+
+Moduletype SIG.
+  Parameter A:Set.
+  Parameter x:A.
+EndT SIG.
+
+Module Nat.
+    Definition A:=nat.
+    Definition x:=O.
+End Nat. 
+
+Module List[X:SIG].
+  Inductive list : Set := nil : list 
+		       | cons : X.A -> list -> list.
+ 
+  Definition head := 
+     [l:list]Cases l of 
+	  nil => X.x 
+	| (cons x _) => x
+     end.
+
+  Definition singl := [x:X.A] (cons x nil).
+  
+  Lemma head_singl : (x:X.A)(head (singl x))=x.
+  Auto.
+  Qed.
+
+End List.
+
+Module N:=(List Nat).
diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v
new file mode 100644
index 000000000..d0ad6a5e2
--- /dev/null
+++ b/test-suite/modules/Nat.v
@@ -0,0 +1,68 @@
+Definition T:=nat.
+
+Definition le:=Peano.le.
+
+Hints Unfold le.
+
+Lemma le_refl:(n:nat)(le n n).
+  Auto.
+Save.
+
+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.
+
+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_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.
+
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
new file mode 100644
index 000000000..da098a420
--- /dev/null
+++ b/test-suite/modules/PO.v
@@ -0,0 +1,89 @@
+Implicit Arguments On.
+
+Implicits fst.
+Implicits snd.
+
+Module Type PO.
+  Parameter T:Set.
+  Parameter le:T->T->Prop.
+  
+  Axiom le_refl : (x:T)(le x x).
+  Axiom le_trans : (x,y,z:T)(le x y) -> (le y z) -> (le x z).
+  Axiom le_antis : (x,y:T)(le x y) -> (le y x) -> (x=y).
+  
+  Hints Resolve le_refl le_trans le_antis.
+End PO.
+
+
+Module Pair[X:PO][Y:PO].
+  Definition T:=X.T*Y.T.
+  Definition le:=[p1,p2]
+    (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)).
+
+  Hints Unfold le.
+
+  Lemma le_refl : (p:T)(le p p).
+  Auto.
+  Save.
+
+  Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3).
+    Unfold le.
+    Intuition; EAuto.
+  Save.    
+
+  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.
+    Reflexivity.
+  Save.
+
+  Hints Resolve le_refl le_trans le_antis.
+
+End Pair.
+
+Module Check_Pair [X:PO][Y:PO] : PO := (Pair X Y).
+
+
+Module Type Fmono.
+  Module X:PO.
+  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 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.
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
new file mode 100644
index 000000000..ecf9a8c25
--- /dev/null
+++ b/test-suite/modules/Przyklad.v
@@ -0,0 +1,193 @@
+Definition ifte := [T:Set][A:Prop][B:Prop][s:(sumbool A B)][th:T][el:T] 
+	   	   if s then [_]th else [_]el.
+
+Implicits ifte.
+
+Lemma Reflexivity_provable : 
+  (A:Set)(a:A)(s:{a=a}+{~a=a})(EXT x| s==(left ? ? x)).
+Intros.
+Elim s.
+Intro x.
+Split with x; Reflexivity.
+
+Intro.
+Absurd a=a; Auto.
+
+Save.
+
+Lemma Disequality_provable : 
+  (A:Set)(a,b:A)(~a=b)->(s:{a=b}+{~a=b})(EXT x| s==(right ? ? x)).
+Intros.
+Elim s.
+Intro.
+Absurd a=a; Auto.
+
+Intro.
+Split with b0; Reflexivity.
+
+Save.
+
+Modtype ELEM.
+  Parameter T : Set.
+  Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}.
+EndT ELEM.
+                                        
+Modtype SET[Elt : ELEM].
+  Parameter T : Set.
+  Parameter empty : T.
+  Parameter add : Elt.T -> T -> T.
+  Parameter find : Elt.T -> T -> bool.
+
+  (* Axioms *)
+
+  Axiom find_empty_false : 
+      (e:Elt.T) (find e empty) = false.
+
+  Axiom find_add_true : 
+        (s:T) (e:Elt.T) (find e (add e s)) = true.
+
+  Axiom find_add_false :
+        (s:T) (e:Elt.T) (e':Elt.T) ~(e=e') -> 
+	(find e (add e' s))=(find e s).
+
+EndT SET.
+
+Mod FuncDict[E : ELEM].
+  Definition T := E.T -> bool.
+  Definition empty := [e':E.T] false.
+  Definition find := [e':E.T] [s:T] (s e').
+  Definition add := [e:E.T][s:T][e':E.T]
+        (ifte (E.eq_dec e e') true (find e' s)).
+
+  Lemma find_empty_false : (e:E.T) (find e empty) = false.
+    Auto.
+  Qed.
+
+  Lemma find_add_true : 
+        (s:T) (e:E.T) (find e (add e s)) = true.
+
+    Intros.
+    Unfold find add.
+    Elim (Reflexivity_provable ? ? (E.eq_dec e e)).
+    Intros.
+    Rewrite H.
+    Auto.
+
+  Qed.
+
+  Lemma find_add_false :
+        (s:T) (e:E.T) (e':E.T) ~(e=e') -> 
+	(find e (add e' s))=(find e s).
+    Intros.
+    Unfold add find.
+    Cut (EXT x:? | (E.eq_dec e' e)==(right ? ? x)).
+    Intros.
+    Elim H0.
+    Intros.
+    Rewrite H1.
+    Unfold ifte.
+    Reflexivity.
+
+    Apply Disequality_provable.
+    Auto.
+
+  Qed.
+
+EndM FuncDict.
+
+Mod F : SET := FuncDict.
+
+
+Mod Nat.
+  Definition T:=nat.
+  Lemma eq_dec :  (a,a':T){a=a'}+{~ a=a'}.
+    Decide Equality.
+  Qed.
+EndM Nat.
+
+
+Mod SetNat:=F Nat. 
+
+
+Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. 
+Apply SetNat.find_empty_false. 
+Save.
+
+(***************************************************************************)
+Mod Lemmas[G:SET][E:ELEM].
+
+  Mod ESet:=G E.
+
+  Lemma commute : (S:ESet.T)(a1,a2:E.T) 
+    let S1 = (ESet.add a1 (ESet.add a2 S)) in 
+    let S2 = (ESet.add a2 (ESet.add a1 S)) in
+      (a:E.T)(ESet.find a S1)=(ESet.find a S2). 
+  
+    Intros.
+    Unfold S1 S2.
+    Elim (E.eq_dec a a1); Elim (E.eq_dec a a2); Intros H1 H2;
+    Try Rewrite <- H1; Try Rewrite <- H2;
+    Repeat 
+      (Try (Rewrite ESet.find_add_true; Auto);
+       Try (Rewrite ESet.find_add_false; Auto); 
+       Auto).
+  Save.
+EndM Lemmas.
+
+
+Inductive list [A:Set] : Set := nil : (list A) 
+                             | cons : A -> (list A) -> (list A).
+
+Mod ListDict[E : ELEM]. 
+  Definition T := (list E.T).
+  Definition elt := E.T.
+   
+  Definition empty := (nil elt).
+  Definition add := [e:elt][s:T] (cons elt e s).
+  Fixpoint find [e:elt; s:T] : bool :=
+        Cases s of 
+          nil => false
+        | (cons e' s') => (ifte (E.eq_dec e e') 
+                                true
+                                (find e s'))
+        end.
+
+  Definition find_empty_false := [e:elt] (refl_equal bool false).
+
+  Lemma find_add_true : 
+        (s:T) (e:E.T) (find e (add e s)) = true.
+    Intros.
+    Simpl.
+    Elim (Reflexivity_provable ? ? (E.eq_dec e e)).
+    Intros.
+    Rewrite H.
+    Auto.
+
+  Qed.
+  
+
+  Lemma find_add_false :
+        (s:T) (e:E.T) (e':E.T) ~(e=e') -> 
+	(find e (add e' s))=(find e s).
+    Intros.
+    Simpl.
+    Elim (Disequality_provable ? ? ? H (E.eq_dec e e')).
+    Intros.
+    Rewrite H0.
+    Simpl.
+    Reflexivity.
+  Save.    
+  
+
+EndM ListDict.
+
+
+Mod L : SET := ListDict.
+
+
+
+
+
+
+
+
diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v
new file mode 100644
index 000000000..b14c3f793
--- /dev/null
+++ b/test-suite/modules/fun_objects.v
@@ -0,0 +1,32 @@
+Implicit Arguments On.
+
+Modtype SIG.
+  Parameter id:(A:Set)A->A.
+EndT SIG.
+ 
+Mod M[X:SIG].
+  Definition idid := (X.id X.id).
+  Definition id := (idid X.id).
+EndM M.
+
+Mod N:=M.
+
+Mod Nat.
+  Definition T := nat.
+  Definition x := O.
+  Definition id := [A:Set][x:A]x.
+EndM Nat.
+
+Mod Z:=(N Nat).
+
+Check (Z.idid O).
+
+Mod P[Y:SIG] := N.
+
+Mod Y:=P Nat Z.
+
+Check (Y.id O).
+
+
+
+
diff --git a/test-suite/modules/grammar.v b/test-suite/modules/grammar.v
new file mode 100644
index 000000000..7751e9f38
--- /dev/null
+++ b/test-suite/modules/grammar.v
@@ -0,0 +1,15 @@
+Mod N.
+Definition f:=plus.
+Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E].
+Check (f O O).
+EndM N.
+Check (N.f O O).
+Imp N.
+Check (N.f O O).
+Check (f O O).
+Mod M:=N.
+Check (f O O).
+Check (N.f O O).
+Imp M.
+Check (f O O).
+Check (N.f O O).
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
new file mode 100644
index 000000000..ba333c525
--- /dev/null
+++ b/test-suite/modules/modul.v
@@ -0,0 +1,39 @@
+Mod M.
+  Parameter rel:nat -> nat -> Prop.
+
+  Axiom w : (n:nat)(rel O (S n)).
+
+  Hints Resolve w.
+
+  Grammar constr constr8 := 
+     not_eq [ constr7($a) "#" constr7($b) ] -> [ (rel $a $b) ].
+  
+  Print Hint *.
+
+  Lemma w1 : (O#(S O)).
+  Auto.
+  Save.
+
+EndM M.
+
+(*Lemma w1 : (M.rel O (S O)).
+Auto.
+*)
+
+Imp M.
+
+Print Hint *.
+Lemma w1 : (O#(S O)).
+Print Hint.
+Print Hint *.
+
+Auto.
+Save.
+
+Check (O#O).
+Locate rel.
+
+Locate M.
+
+Mod N:=Scratch.M.
+
diff --git a/test-suite/modules/modulik.v b/test-suite/modules/modulik.v
new file mode 100644
index 000000000..50d985e52
--- /dev/null
+++ b/test-suite/modules/modulik.v
@@ -0,0 +1,5 @@
+Definition toto := Set.
+
+Mod M.
+  Definition id:=[X:Set]X.
+EndM M.
diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v
new file mode 100644
index 000000000..b02bdf189
--- /dev/null
+++ b/test-suite/modules/obj.v
@@ -0,0 +1,26 @@
+Implicit Arguments On.
+
+Mod M. 
+  Definition a:=[s:Set]s.
+  Print a.
+EndM M.
+
+Print M.a.
+
+Mod K.
+  Definition app:=[A,B:Set; f:(A->B); x:A](f x).
+  Mod N.
+    Definition apap:=[A,B:Set](app (app 1!A 2!B)).
+    Print app.
+    Print apap.
+  EndM N.
+  Print N.apap.
+EndM K.
+
+Print K.app.
+Print K.N.apap.
+
+Mod W:=K.N.
+
+Print W.apap.
+
diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v
new file mode 100644
index 000000000..8183c67c6
--- /dev/null
+++ b/test-suite/modules/objects.v
@@ -0,0 +1,35 @@
+Reset Initial.
+
+Modtype SET.
+  Axiom T:Set.
+  Axiom x:T.
+EndT SET.
+ 
+Implicit Arguments On.
+
+Mod M[X:SET].
+  Definition T := nat.
+  Definition x := O.
+  Definition f := [A:Set][x:A]X.x.
+EndM M.
+
+Mod N:=M.
+
+Mod Nat.
+  Definition T := nat.
+  Definition x := O.
+EndM Nat.
+
+Mod Z:=(N Nat).
+
+Check (Z.f O).
+
+Mod P[Y:SET] := N.
+
+Mod Y:=P Z Nat.
+
+Check (Y.f O).
+
+
+
+
diff --git a/test-suite/modules/pliczek.v b/test-suite/modules/pliczek.v
new file mode 100644
index 000000000..6061ace34
--- /dev/null
+++ b/test-suite/modules/pliczek.v
@@ -0,0 +1,3 @@
+Require Export plik.
+
+Definition tutu := [X:Set](toto X).
diff --git a/test-suite/modules/plik.v b/test-suite/modules/plik.v
new file mode 100644
index 000000000..f1f59df0f
--- /dev/null
+++ b/test-suite/modules/plik.v
@@ -0,0 +1,4 @@
+Definition toto:=[x:Set]x.
+
+Grammar constr constr8 := 
+     toto [ "#" constr7($b) ] -> [ (toto $b) ].
diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v
new file mode 100644
index 000000000..f800dec52
--- /dev/null
+++ b/test-suite/modules/sub_objects.v
@@ -0,0 +1,35 @@
+Reset Initial.
+
+Set Implicit Arguments.
+
+
+Mod M.
+  Definition id:=[A:Set][x:A]x.
+
+  Modtype SIG.
+    Parameter idid:(A:Set)A->A.
+  EndT SIG.
+
+  Mod N.
+    Definition idid:=[A:Set][x:A](id x).
+    Grammar constr constr8 := 
+      not_eq [ "#"  constr7($b) ] -> [ (idid $b) ].
+    Syntactic Definition inc := (plus (S O)). 
+  EndM N.
+
+  Definition zero:=(N.idid O).
+
+EndM M.
+
+Definition zero := (M.N.idid O).
+Definition jeden := (M.N.inc O).
+
+Mod Goly:=M.N.
+
+Definition Gole_zero := (Goly.idid O).
+Definition Goly_jeden := (Goly.inc O).
+
+Mod Ubrany : M.SIG := M.N.
+
+Definition Ubrane_zero := (Ubrany.idid O).
+