From 12965209478bd99dfbe57f07d5b525e51b903f22 Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 2 Aug 2002 17:17:42 +0000 Subject: Modules dans COQ\!\!\!\! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/modules/Nametab.v | 100 ++++++++++++++++++++ test-suite/modules/Nat.v | 68 ++++++++++++++ test-suite/modules/PO.v | 89 ++++++++++++++++++ test-suite/modules/Przyklad.v | 193 +++++++++++++++++++++++++++++++++++++++ test-suite/modules/fun_objects.v | 32 +++++++ test-suite/modules/grammar.v | 15 +++ test-suite/modules/modul.v | 39 ++++++++ test-suite/modules/modulik.v | 5 + test-suite/modules/obj.v | 26 ++++++ test-suite/modules/objects.v | 35 +++++++ test-suite/modules/pliczek.v | 3 + test-suite/modules/plik.v | 4 + test-suite/modules/sub_objects.v | 35 +++++++ 13 files changed, 644 insertions(+) create mode 100644 test-suite/modules/Nametab.v create mode 100644 test-suite/modules/Nat.v create mode 100644 test-suite/modules/PO.v create mode 100644 test-suite/modules/Przyklad.v create mode 100644 test-suite/modules/fun_objects.v create mode 100644 test-suite/modules/grammar.v create mode 100644 test-suite/modules/modul.v create mode 100644 test-suite/modules/modulik.v create mode 100644 test-suite/modules/obj.v create mode 100644 test-suite/modules/objects.v create mode 100644 test-suite/modules/pliczek.v create mode 100644 test-suite/modules/plik.v create mode 100644 test-suite/modules/sub_objects.v (limited to 'test-suite/modules') 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). + -- cgit v1.2.3