diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /test-suite/modules |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'test-suite/modules')
-rw-r--r-- | test-suite/modules/Demo.v | 55 | ||||
-rw-r--r-- | test-suite/modules/Nametab.v | 48 | ||||
-rw-r--r-- | test-suite/modules/Nat.v | 19 | ||||
-rw-r--r-- | test-suite/modules/PO.v | 57 | ||||
-rw-r--r-- | test-suite/modules/Przyklad.v | 193 | ||||
-rw-r--r-- | test-suite/modules/Tescik.v | 30 | ||||
-rw-r--r-- | test-suite/modules/fun_objects.v | 32 | ||||
-rw-r--r-- | test-suite/modules/grammar.v | 15 | ||||
-rw-r--r-- | test-suite/modules/ind.v | 13 | ||||
-rw-r--r-- | test-suite/modules/mod_decl.v | 55 | ||||
-rw-r--r-- | test-suite/modules/modeq.v | 22 | ||||
-rw-r--r-- | test-suite/modules/modul.v | 39 | ||||
-rw-r--r-- | test-suite/modules/obj.v | 26 | ||||
-rw-r--r-- | test-suite/modules/objects.v | 33 | ||||
-rw-r--r-- | test-suite/modules/pliczek.v | 3 | ||||
-rw-r--r-- | test-suite/modules/plik.v | 4 | ||||
-rw-r--r-- | test-suite/modules/sig.v | 29 | ||||
-rw-r--r-- | test-suite/modules/sub_objects.v | 33 |
18 files changed, 706 insertions, 0 deletions
diff --git a/test-suite/modules/Demo.v b/test-suite/modules/Demo.v new file mode 100644 index 00000000..1e9273f0 --- /dev/null +++ b/test-suite/modules/Demo.v @@ -0,0 +1,55 @@ +Module M. + Definition t:=nat. + Definition x:=O. +End M. + +Print M.t. + + +Module Type SIG. + Parameter t:Set. + Parameter x:t. +End SIG. + + +Module F[X:SIG]. + Definition t:=X.t->X.t. + Definition x:t. + Intro. + Exact X.x. + Defined. + Definition y:=X.x. +End F. + + +Module N := F M. + +Print N.t. +Eval Compute in N.t. + + +Module N' : SIG := N. + +Print N'.t. +Eval Compute in N'.t. + + +Module N'' <: SIG := F N. + +Print N''.t. +Eval Compute in N''.t. + +Eval Compute in N''.x. + + +Module N''' : SIG with Definition t:=nat->nat := N. + +Print N'''.t. +Eval Compute in N'''.t. + +Print N'''.x. + + +Import N'''. + +Print t.
\ No newline at end of file diff --git a/test-suite/modules/Nametab.v b/test-suite/modules/Nametab.v new file mode 100644 index 00000000..61966c7c --- /dev/null +++ b/test-suite/modules/Nametab.v @@ -0,0 +1,48 @@ +Module Q. + Module N. + Module K. + Definition id:=Set. + End K. + End N. +End Q. + +(* Bad *) Locate id. +(* Bad *) Locate K.id. +(* Bad *) Locate N.K.id. +(* OK *) Locate Q.N.K.id. +(* OK *) Locate Top.Q.N.K.id. + +(* Bad *) Locate K. +(* Bad *) Locate N.K. +(* OK *) Locate Q.N.K. +(* OK *) Locate Top.Q.N.K. + +(* Bad *) Locate N. +(* OK *) Locate Q.N. +(* OK *) Locate Top.Q.N. + +(* OK *) Locate Q. +(* OK *) Locate Top.Q. + + + +Import Q.N. + + +(* Bad *) Locate id. +(* OK *) Locate K.id. +(* Bad *) Locate N.K.id. +(* OK *) Locate Q.N.K.id. +(* OK *) Locate Top.Q.N.K.id. + +(* OK *) Locate K. +(* Bad *) Locate N.K. +(* OK *) Locate Q.N.K. +(* OK *) Locate Top.Q.N.K. + +(* Bad *) Locate N. +(* OK *) Locate Q.N. +(* OK *) Locate Top.Q.N. + +(* OK *) Locate Q. +(* OK *) Locate Top.Q. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v new file mode 100644 index 00000000..d3e98ae4 --- /dev/null +++ b/test-suite/modules/Nat.v @@ -0,0 +1,19 @@ +Definition T:=nat. + +Definition le:=Peano.le. + +Hints Unfold le. + +Lemma le_refl:(n:nat)(le n n). + Auto. +Qed. + +Require Le. + +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. + EAuto with arith. +Qed. diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v new file mode 100644 index 00000000..9ba3fb2e --- /dev/null +++ b/test-suite/modules/PO.v @@ -0,0 +1,57 @@ +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] <: 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). + Info Auto. + Qed. + + Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3). + 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. + CutRewrite t=t1. + CutRewrite t0=t2. + Reflexivity. + + Info Auto. + + Info Auto. + Qed. + +End Pair. + + + +Read Module Nat. + +Module NN := Pair Nat Nat. + +Lemma zz_min : (p:NN.T)(NN.le (O,O) p). + Info Auto with arith. +Qed. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v new file mode 100644 index 00000000..4f4c2066 --- /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. + +Module Type ELEM. + Parameter T : Set. + Parameter eq_dec : (a,a':T){a=a'}+{~ a=a'}. +End ELEM. + +Module Type 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). + +End SET. + +Module 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. + +End FuncDict. + +Module F : SET := FuncDict. + + +Module Nat. + Definition T:=nat. + Lemma eq_dec : (a,a':T){a=a'}+{~ a=a'}. + Decide Equality. + Qed. +End Nat. + + +Module SetNat:=F Nat. + + +Lemma no_zero_in_empty:(SetNat.find O SetNat.empty)=false. +Apply SetNat.find_empty_false. +Save. + +(***************************************************************************) +Module Lemmas[G:SET][E:ELEM]. + + Module 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. +End Lemmas. + + +Inductive list [A:Set] : Set := nil : (list A) + | cons : A -> (list A) -> (list A). + +Module 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. + + +End ListDict. + + +Module L : SET := ListDict. + + + + + + + + diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v new file mode 100644 index 00000000..13c28418 --- /dev/null +++ b/test-suite/modules/Tescik.v @@ -0,0 +1,30 @@ + +Module Type ELEM. + Parameter A:Set. + Parameter x:A. +End ELEM. + +Module Nat. + Definition A:=nat. + Definition x:=O. +End Nat. + +Module List[X:ELEM]. + 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/fun_objects.v b/test-suite/modules/fun_objects.v new file mode 100644 index 00000000..0f8eef84 --- /dev/null +++ b/test-suite/modules/fun_objects.v @@ -0,0 +1,32 @@ +Implicit Arguments On. + +Module Type SIG. + Parameter id:(A:Set)A->A. +End SIG. + +Module M[X:SIG]. + Definition idid := (X.id X.id). + Definition id := (idid X.id). +End M. + +Module N:=M. + +Module Nat. + Definition T := nat. + Definition x := O. + Definition id := [A:Set][x:A]x. +End Nat. + +Module Z:=(N Nat). + +Check (Z.idid O). + +Module P[Y:SIG] := N. + +Module 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 00000000..fb734b5d --- /dev/null +++ b/test-suite/modules/grammar.v @@ -0,0 +1,15 @@ +Module N. +Definition f:=plus. +Syntax constr level 7: plus [ (f $n $m)] -> [ $n:L "+" $m:E]. +Check (f O O). +End N. +Check (N.f O O). +Import N. +Check (N.f O O). +Check (f O O). +Module M:=N. +Check (f O O). +Check (N.f O O). +Import M. +Check (f O O). +Check (N.f O O). diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v new file mode 100644 index 00000000..94c344bb --- /dev/null +++ b/test-suite/modules/ind.v @@ -0,0 +1,13 @@ +Module Type SIG. + Inductive w:Set:=A:w. + Parameter f : w->w. +End SIG. + +Module M:SIG. + Inductive w:Set:=A:w. + Definition f:=[x]Cases x of A => A end. +End M. + +Module N:=M. + +Check (N.f M.A). diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v new file mode 100644 index 00000000..867b8a11 --- /dev/null +++ b/test-suite/modules/mod_decl.v @@ -0,0 +1,55 @@ +Module Type SIG. + Definition A:Set. (*error*) + Axiom A:Set. +End SIG. + +Module M0. + Definition A:Set. + Exact nat. + Save. +End M0. + +Module M1:SIG. + Definition A:=nat. +End M1. + +Module M2<:SIG. + Definition A:=nat. +End M2. + +Module M3:=M0. + +Module M4:SIG:=M0. + +Module M5<:SIG:=M0. + + +Module F[X:SIG]:=X. + + +Declare Module M6. + + +Module Type T. + + Declare Module M0. + Lemma A:Set (*error*). + Axiom A:Set. + End M0. + + Declare Module M1:SIG. + + Declare Module M2<:SIG. + Definition A:=nat. + End M2. + + Declare Module M3:=M0. + + Declare Module M4:SIG:=M0. (* error *) + + Declare Module M5<:SIG:=M0. + + Declare Module M6:=F M0. (* error *) + + Module M7. +End T.
\ No newline at end of file diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v new file mode 100644 index 00000000..73448dc7 --- /dev/null +++ b/test-suite/modules/modeq.v @@ -0,0 +1,22 @@ +Module M. + Definition T:=nat. + Definition x:T:=O. +End M. + +Module Type SIG. + Declare Module M:=Top.M. + Module Type SIG. + Parameter T:Set. + End SIG. + Declare Module N:SIG. +End SIG. + +Module Z. + Module M:=Top.M. + Module Type SIG. + Parameter T:Set. + End SIG. + Module N:=M. +End Z. + +Module A:SIG:=Z. diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v new file mode 100644 index 00000000..5612ea75 --- /dev/null +++ b/test-suite/modules/modul.v @@ -0,0 +1,39 @@ +Module 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. + +End M. + +(*Lemma w1 : (M.rel O (S O)). +Auto. +*) + +Import M. + +Print Hint *. +Lemma w1 : (O#(S O)). +Print Hint. +Print Hint *. + +Auto. +Save. + +Check (O#O). +Locate rel. + +Locate M. + +Module N:=Top.M. + diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v new file mode 100644 index 00000000..2231e084 --- /dev/null +++ b/test-suite/modules/obj.v @@ -0,0 +1,26 @@ +Implicit Arguments On. + +Module M. + Definition a:=[s:Set]s. + Print a. +End M. + +Print M.a. + +Module K. + Definition app:=[A,B:Set; f:(A->B); x:A](f x). + Module N. + Definition apap:=[A,B:Set](app (app 1!A 2!B)). + Print app. + Print apap. + End N. + Print N.apap. +End K. + +Print K.app. +Print K.N.apap. + +Module 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 00000000..418ece44 --- /dev/null +++ b/test-suite/modules/objects.v @@ -0,0 +1,33 @@ +Module Type SET. + Axiom T:Set. + Axiom x:T. +End SET. + +Implicit Arguments On. + +Module M[X:SET]. + Definition T := nat. + Definition x := O. + Definition f := [A:Set][x:A]X.x. +End M. + +Module N:=M. + +Module Nat. + Definition T := nat. + Definition x := O. +End Nat. + +Module Z:=(N Nat). + +Check (Z.f O). + +Module P[Y:SET] := N. + +Module 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 00000000..6061ace3 --- /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 00000000..f1f59df0 --- /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/sig.v b/test-suite/modules/sig.v new file mode 100644 index 00000000..eb8736bb --- /dev/null +++ b/test-suite/modules/sig.v @@ -0,0 +1,29 @@ +Module M. + Module Type SIG. + Parameter T:Set. + Parameter x:T. + End SIG. + Module N:SIG. + Definition T:=nat. + Definition x:=O. + End N. +End M. + +Module N:=M. + +Module Type SPRYT. + Declare Module N. + Definition T:=M.N.T. + Parameter x:T. + End N. +End SPRYT. + +Module K:SPRYT:=N. +Module K':SPRYT:=M. + +Module Type SIG. + Definition T:Set:=M.N.T. + Parameter x:T. +End SIG. + +Module J:SIG:=M.N. diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v new file mode 100644 index 00000000..1bd4faef --- /dev/null +++ b/test-suite/modules/sub_objects.v @@ -0,0 +1,33 @@ +Set Implicit Arguments. + + +Module M. + Definition id:=[A:Set][x:A]x. + + Module Type SIG. + Parameter idid:(A:Set)A->A. + End SIG. + + Module N. + Definition idid:=[A:Set][x:A](id x). + Grammar constr constr8 := + not_eq [ "#" constr7($b) ] -> [ (idid $b) ]. + Notation inc := (plus (S O)). + End N. + + Definition zero:=(N.idid O). + +End M. + +Definition zero := (M.N.idid O). +Definition jeden := (M.N.inc O). + +Module Goly:=M.N. + +Definition Gole_zero := (Goly.idid O). +Definition Goly_jeden := (Goly.inc O). + +Module Ubrany : M.SIG := M.N. + +Definition Ubrane_zero := (Ubrany.idid O). + |