diff options
Diffstat (limited to 'test-suite/output')
28 files changed, 679 insertions, 14 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 1f0e12d3..1ec02c56 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -9,10 +9,9 @@ fix F (t : t) : P t := proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match eq_nat_dec x y with -| left eqprf => - match eqprf in (_ = z) return (P z) with - | refl_equal => def - end +| left eqprf => match eqprf in (_ = z) return (P z) with + | eq_refl => def + end | right _ => prf end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 37ee71e9..b6337586 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -12,7 +12,7 @@ Require Import Arith. Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y := match eq_nat_dec x y return P y with - | left eqprf => + | left eqprf => match eqprf in (_ = z) return (P z) with | refl_equal => def end diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out index 4b8aa355..6edc9e09 100644 --- a/test-suite/output/Coercions.out +++ b/test-suite/output/Coercions.out @@ -4,3 +4,5 @@ R x x : Prop fun (x : foo) (n : nat) => x n : foo -> nat -> nat +"1" 0 + : PAIR diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v index c88b143f..0e84bf39 100644 --- a/test-suite/output/Coercions.v +++ b/test-suite/output/Coercions.v @@ -13,3 +13,12 @@ End testSection. Record foo : Type := {D :> nat -> nat}. Check (fun (x : foo) (n : nat) => x n). + +(* Check both removal of coercions with target Funclass and mixing + string and numeral scopes *) + +Require Import String. +Open Scope string_scope. +Inductive PAIR := P (s:string) (n:nat). +Coercion P : string >-> Funclass. +Check ("1" 0). diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out new file mode 100644 index 00000000..ca79ba69 --- /dev/null +++ b/test-suite/output/Existentials.out @@ -0,0 +1 @@ +Existential 1 = ?9 : [n : nat m : nat |- nat] diff --git a/test-suite/output/Existentials.v b/test-suite/output/Existentials.v new file mode 100644 index 00000000..73884683 --- /dev/null +++ b/test-suite/output/Existentials.v @@ -0,0 +1,14 @@ +(* Test propagation of clear/clearbody in existential variables *) + +Section Test. + +Variable p:nat. +Let q := S p. + +Goal forall n m:nat, n = m. +intros. +eapply eq_trans. +clearbody q. +clear p. (* Error ... *) + +Show Existentials. diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 2b13c204..af5f05f6 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -1,7 +1,7 @@ Require Import List. Check - (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : + (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B := match l with | nil => nil | a :: l => f a :: F _ _ f l diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out new file mode 100644 index 00000000..105940a4 --- /dev/null +++ b/test-suite/output/Naming.out @@ -0,0 +1,83 @@ +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, x + x1 = x4 + x3 + ============================ + x + x1 = x4 + x0 +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> + x + x1 = x4 + x0 -> foo (S x) +1 subgoal + + x3 : nat + ============================ + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + ============================ + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H0 : x + x1 = x4 + x0 + ============================ + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H0 : x + x1 = x4 + x0 + x5 : nat + x6 : nat + x7 : nat + S : nat + ============================ + x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + a : nat + H : a = 0 -> forall a : nat, a = 0 + ============================ + a = 0 diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v new file mode 100644 index 00000000..327643dc --- /dev/null +++ b/test-suite/output/Naming.v @@ -0,0 +1,91 @@ +(* This file checks the compatibility of naming strategy *) +(* This does not mean that the given naming strategy is good *) + +Parameter x2:nat. +Definition foo y := forall x x3 x4 S, x + S = x3 + x4 + y. +Section A. +Variable x3:nat. +Goal forall x x1 x2 x3:nat, + (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3. +Show. +intros. +Show. + +(* Remark: in V8.2, this used to be printed + + x3 : nat + ============================ + forall x x1 x4 x5 : nat, + (forall x0 x6 : nat, x0 + x1 = x4 + x6) -> x + x1 = x4 + x5 + +before intro and + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, x + x1 = x4 + x3 + ============================ + x + x1 = x4 + x0 + +after. From V8.3, the quantified hypotheses are printed the sames as +they would be intro. However the hypothesis H remains printed +differently to avoid using the same name in autonomous but nested +subterms *) + +Abort. + +Goal forall x x1 x2 x3:nat, + (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) -> + x+x1 = x2+x3 -> foo (S x). +Show. +unfold foo. +Show. +do 4 intro. (* --> x, x1, x4, x0, ... *) +Show. +do 2 intro. +Show. +do 4 intro. +Show. + +(* Remark: in V8.2, this used to be printed + + x3 : nat + ============================ + forall x x1 x4 x5 : nat, + (forall x0 x6 : nat, + x0 + x1 = x4 + x6 -> + forall x7 x8 x9 S0 : nat, x7 + S0 = x8 + x9 + (S x0 + x1)) -> + x + x1 = x4 + x5 -> forall x0 x6 x7 S0 : nat, x0 + S0 = x6 + x7 + S x + +before the intros and + + x3 : nat + x : nat + x1 : nat + x4 : nat + x0 : nat + H : forall x x3 : nat, + x + x1 = x4 + x3 -> + forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) + H0 : x + x1 = x4 + x0 + x5 : nat + x6 : nat + x7 : nat + S : nat + ============================ + x5 + S = x6 + x7 + Datatypes.S x + +after (note the x5/x0 and the S0/S) *) + +Abort. + +(* Check naming in hypotheses *) + +Goal forall a, (a = 0 -> forall a, a = 0) -> a = 0. +intros. +Show. +apply H with (a:=a). (* test compliance with printing *) +Abort. + diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 42858304..924030ba 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -1,7 +1,7 @@ true ? 0; 1 : nat if true as x return (x ? nat; bool) then 0 else true - : true ? nat; bool + : nat Defining 'proj1' as keyword fun e : nat * nat => proj1 e : nat * nat -> nat @@ -46,6 +46,10 @@ fun x : nat => ifn x is succ n then n else 0 : bool -4 : Z +SUM (nat * nat) nat + : Set +FST (0; 1) + : Z Nil : forall A : Type, list A NIL:list nat @@ -57,3 +61,34 @@ Defining 'I' as keyword : Z * Z * Z * (Z * Z * Z) fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z : (Z -> Z -> Z -> Z) -> Z +plus + : nat -> nat -> nat +S + : nat -> nat +mult + : nat -> nat -> nat +le + : nat -> nat -> Prop +plus + : nat -> nat -> nat +succ + : nat -> nat +mult + : nat -> nat -> nat +le + : nat -> nat -> Prop +fun x : option Z => match x with + | SOME x0 => x0 + | NONE => 0 + end + : option Z -> Z +fun x : option Z => match x with + | SOME2 x0 => x0 + | NONE2 => 0 + end + : option Z -> Z +fun x : option Z => match x with + | SOME3 x0 => x0 + | NONE3 => 0 + end + : option Z -> Z diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index b37c3638..f041b9b7 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -64,26 +64,26 @@ Open Scope nat_scope. Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). Coercion Zpos: nat >-> znat. - + Delimit Scope znat_scope with znat. Open Scope znat_scope. - + Variable addz : znat -> znat -> znat. Notation "z1 + z2" := (addz z1 z2) : znat_scope. (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit, - is printed the same way, and not "S 2 + S 2" as if numeral printing was + is printed the same way, and not "S 2 + S 2" as if numeral printing was only tested with coercion still present *) Check (3+3). (**********************************************************************) (* Check recursive notations *) - + Require Import List. Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). Check [1;2;4]. - + Reserved Notation "( x ; y , .. , z )" (at level 0). Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z). Check (1;2,4). @@ -102,7 +102,7 @@ Check (pred 3). Check (fun n => match n with 0 => 0 | S n => n end). Check (fun n => match n with S p as x => p | y => 0 end). -Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" := +Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" := (match x with O => u | S n => t end) (at level 0, u at level 0). Check fun x => ifn x is succ n then n else 0. @@ -121,6 +121,18 @@ Notation "- 4" := (-2 + -2). Check -4. (**********************************************************************) +(* Check preservation of scopes at printing time *) + +Notation SUM := sum. +Check SUM (nat*nat) nat. + +(**********************************************************************) +(* Check preservation of implicit arguments at printing time *) + +Notation FST := fst. +Check FST (0;1). + +(**********************************************************************) (* Check notations for references with activated or deactivated *) (* implicit arguments *) @@ -159,3 +171,38 @@ Check [|1,2,3;4,5,6|]. Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y). Check fun f => {| f; 0; 1; 2 |} : Z. + +(**********************************************************************) +(* Check printing of notations from other modules *) + +(* 1- Non imported case *) + +Require make_notation. + +Check plus. +Check S. +Check mult. +Check le. + +(* 2- Imported case *) + +Import make_notation. + +Check plus. +Check S. +Check mult. +Check le. + +(* Check notations in cases patterns *) + +Notation SOME := Some. +Notation NONE := None. +Check (fun x => match x with SOME x => x | NONE => 0 end). + +Notation NONE2 := (@None _). +Notation SOME2 := (@Some _). +Check (fun x => match x with SOME2 x => x | NONE2 => 0 end). + +Notation NONE3 := @None. +Notation SOME3 := @Some. +Check (fun x => match x with SOME3 x => x | NONE3 => 0 end). diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out new file mode 100644 index 00000000..20d20d82 --- /dev/null +++ b/test-suite/output/Notations2.out @@ -0,0 +1,12 @@ +2 3 + : PAIR +2[+]3 + : nat +forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x + : Prop +match (0, 0, 0) with +| (x, y, z) => x + y + z +end + : nat +let '(a, _, _) := (2, 3, 4) in a + : nat diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v new file mode 100644 index 00000000..2e136edf --- /dev/null +++ b/test-suite/output/Notations2.v @@ -0,0 +1,26 @@ +(**********************************************************************) +(* Test call to primitive printers in presence of coercion to *) +(* functions (cf bug #2044) *) + +Inductive PAIR := P (n1:nat) (n2:nat). +Coercion P : nat >-> Funclass. +Check (2 3). + +(* Check that notations with coercions to functions inserted still work *) +(* (were not working from revision 11886 to 12951) *) + +Record Binop := { binop :> nat -> nat -> nat }. +Class Plusop := { plusop : Binop; zero : nat }. +Infix "[+]" := plusop (at level 40). +Instance Plus : Plusop := {| plusop := {| binop := plus |} ; zero := 0 |}. +Check 2[+]3. + +(* Test bug #2091 (variable le was printed using <= !) *) + +Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x. + +(* Test recursive notations in cases pattern *) + +Remove Printing Let prod. +Check match (0,0,0) with (x,y,z) => x+y+z end. +Check let '(a,b,c) := ((2,3),4) in a. diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out new file mode 100644 index 00000000..b2a44fb7 --- /dev/null +++ b/test-suite/output/NumbersSyntax.out @@ -0,0 +1,67 @@ +I31 + : digits31 int31 +2 + : int31 +660865024 + : int31 +2 + 2 + : int31 +2 + 2 + : int31 + = 4 + : int31 + = 710436486 + : int31 +2 + : BigN.t_ +1000000000000000000 + : BigN.t_ +2 + 2 + : BigN.t_ +2 + 2 + : BigN.t_ + = 4 + : BigN.t_ + = 37151199385380486 + : BigN.t_ + = 1267650600228229401496703205376 + : BigN.t_ +2 + : BigZ.t_ +-1000000000000000000 + : BigZ.t_ +2 + 2 + : BigZ.t_ +2 + 2 + : BigZ.t_ + = 4 + : BigZ.t_ + = 37151199385380486 + : BigZ.t_ + = 1267650600228229401496703205376 + : BigZ.t_ +2 + : BigQ.t_ +-1000000000000000000 + : BigQ.t_ +2 + 2 + : bigQ +2 + 2 + : bigQ + = 4 + : bigQ + = 37151199385380486 + : bigQ +6562 # 456 + : BigQ.t_ + = 3281 # 228 + : bigQ + = -1 # 10000 + : bigQ + = 100 + : bigQ + = 515377520732011331036461129765621272702107522001 + # 1267650600228229401496703205376 + : bigQ + = 1 + : bigQ diff --git a/test-suite/output/NumbersSyntax.v b/test-suite/output/NumbersSyntax.v new file mode 100644 index 00000000..4fbf56ab --- /dev/null +++ b/test-suite/output/NumbersSyntax.v @@ -0,0 +1,50 @@ + +Require Import BigQ. + +Open Scope int31_scope. +Check I31. (* Would be nice to have I31 : digits->digits->...->int31 + For the moment, I31 : digits31 int31, which is better + than (fix nfun .....) size int31 *) +Check 2. +Check 1000000000000000000. (* = 660865024, after modulo 2^31 *) +Check (add31 2 2). +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. +Close Scope int31_scope. + +Open Scope bigN_scope. +Check 2. +Check 1000000000000000000. +Check (BigN.add 2 2). +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. +Eval vm_compute in 2^100. +Close Scope bigN_scope. + +Open Scope bigZ_scope. +Check 2. +Check -1000000000000000000. +Check (BigZ.add 2 2). +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. +Eval vm_compute in (-2)^100. +Close Scope bigZ_scope. + +Open Scope bigQ_scope. +Check 2. +Check -1000000000000000000. +Check (BigQ.add 2 2). +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. +(* fractions *) +Check (6562 # 456). (* Nota: # is BigQ.Qq i.e. base fractions *) +Eval vm_compute in (BigQ.red (6562 # 456)). +Eval vm_compute in (1/-10000). +Eval vm_compute in (BigQ.red (1/(1/100))). (* back to integers... *) +Eval vm_compute in ((2/3)^(-100)). +Eval vm_compute in BigQ.red ((2/3)^(-1000) * (2/3)^(1000)). +Close Scope bigQ_scope. diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out new file mode 100644 index 00000000..ca7fc362 --- /dev/null +++ b/test-suite/output/Quote.out @@ -0,0 +1,24 @@ +(interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx)) +(interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) + (f_and (f_const A) + (f_and (f_or (f_atom End_idx) (f_const A)) + (f_or (f_const A) (f_not (f_atom End_idx)))))) +1 subgoal + + H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ + B + ============================ + interp_f + (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop)) + (f_and (f_atom (Left_idx End_idx)) + (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx))) + (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx))))) +1 subgoal + + H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ + B + ============================ + interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) + (f_and (f_const A) + (f_and (f_or (f_atom End_idx) (f_const A)) + (f_or (f_const A) (f_not (f_atom End_idx))))) diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v new file mode 100644 index 00000000..2c373d50 --- /dev/null +++ b/test-suite/output/Quote.v @@ -0,0 +1,36 @@ +Require Import Quote. + +Parameter A B : Prop. + +Inductive formula : Type := + | f_and : formula -> formula -> formula + | f_or : formula -> formula -> formula + | f_not : formula -> formula + | f_true : formula + | f_atom : index -> formula + | f_const : Prop -> formula. + +Fixpoint interp_f (vm: + varmap Prop) (f:formula) {struct f} : Prop := + match f with + | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 + | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 + | f_not f1 => ~ interp_f vm f1 + | f_true => True + | f_atom i => varmap_find True i vm + | f_const c => c + end. + +Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B). +intro H. +match goal with + | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H) +end. +match goal with + |- ?g => quote interp_f [ A ] in g using (fun x => idtac x) +end. +quote interp_f. +Show. +simpl; quote interp_f [ A ]. +Show. +Admitted. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out new file mode 100644 index 00000000..99e736dd --- /dev/null +++ b/test-suite/output/Search.out @@ -0,0 +1,36 @@ +le_S: forall n m : nat, n <= m -> n <= S m +le_n: forall n : nat, n <= n +false: bool +true: bool +sumor_beq: + forall (A : Type) (B : Prop), + (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool +sumbool_beq: + forall A B : Prop, + (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool +xorb: bool -> bool -> bool +sum_beq: + forall A B : Type, + (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool +prod_beq: + forall A B : Type, + (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool +orb: bool -> bool -> bool +option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool +negb: bool -> bool +nat_beq: nat -> nat -> bool +list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool +implb: bool -> bool -> bool +comparison_beq: comparison -> comparison -> bool +bool_beq: bool -> bool -> bool +andb: bool -> bool -> bool +Empty_set_beq: Empty_set -> Empty_set -> bool +pred_Sn: forall n : nat, n = pred (S n) +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +plus_n_O: forall n : nat, n = n + 0 +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +plus_O_n: forall n : nat, 0 + n = n +mult_n_Sm: forall n m : nat, n * m + n = n * S m +mult_n_O: forall n : nat, 0 = n * 0 +eq_add_S: forall n m : nat, S n = S m -> n = m +eq_S: forall x y : nat, x = y -> S x = S y diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v new file mode 100644 index 00000000..f1489f22 --- /dev/null +++ b/test-suite/output/Search.v @@ -0,0 +1,5 @@ +(* Some tests of the Search command *) + +Search le. (* app nodes *) +Search bool. (* no apps *) +Search (@eq nat). (* complex pattern *) diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out new file mode 100644 index 00000000..1a87f4cc --- /dev/null +++ b/test-suite/output/SearchPattern.out @@ -0,0 +1,44 @@ +false: bool +true: bool +sumor_beq: + forall (A : Type) (B : Prop), + (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool +sumbool_beq: + forall A B : Prop, + (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool +xorb: bool -> bool -> bool +sum_beq: + forall A B : Type, + (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool +prod_beq: + forall A B : Type, + (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool +orb: bool -> bool -> bool +option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool +negb: bool -> bool +nat_beq: nat -> nat -> bool +list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool +implb: bool -> bool -> bool +comparison_beq: comparison -> comparison -> bool +bool_beq: bool -> bool -> bool +andb: bool -> bool -> bool +Empty_set_beq: Empty_set -> Empty_set -> bool +S: nat -> nat +O: nat +pred: nat -> nat +plus: nat -> nat -> nat +mult: nat -> nat -> nat +minus: nat -> nat -> nat +length: forall A : Type, list A -> nat +S: nat -> nat +pred: nat -> nat +plus: nat -> nat -> nat +mult: nat -> nat -> nat +minus: nat -> nat -> nat +mult_n_Sm: forall n m : nat, n * m + n = n * S m +le_n: forall n : nat, n <= n +eq_refl: forall (A : Type) (x : A), x = x +identity_refl: forall (A : Type) (a : A), identity a a +iff_refl: forall A : Prop, A <-> A +conj: forall A B : Prop, A -> B -> A /\ B +pair: forall A B : Type, A -> B -> A * B diff --git a/test-suite/output/SearchPattern.v b/test-suite/output/SearchPattern.v new file mode 100644 index 00000000..802d8c97 --- /dev/null +++ b/test-suite/output/SearchPattern.v @@ -0,0 +1,19 @@ +(* Some tests of the SearchPattern command *) + +(* Simple, random tests *) +SearchPattern bool. +SearchPattern nat. +SearchPattern le. + +(* With some hypothesis *) +SearchPattern (nat -> nat). +SearchPattern (?n * ?m + ?n = ?n * S ?m). + +(* Non-linearity *) +SearchPattern (_ ?X ?X). + +(* Non-linearity with hypothesis *) +SearchPattern (forall (x:?A) (y:?B), _ ?A ?B). + +(* No delta-reduction *) +SearchPattern (Exc _). diff --git a/test-suite/output/SearchRewrite.out b/test-suite/output/SearchRewrite.out new file mode 100644 index 00000000..f87aea1c --- /dev/null +++ b/test-suite/output/SearchRewrite.out @@ -0,0 +1,2 @@ +plus_n_O: forall n : nat, n = n + 0 +plus_O_n: forall n : nat, 0 + n = n diff --git a/test-suite/output/SearchRewrite.v b/test-suite/output/SearchRewrite.v new file mode 100644 index 00000000..171a7363 --- /dev/null +++ b/test-suite/output/SearchRewrite.v @@ -0,0 +1,4 @@ +(* Some tests of the SearchRewrite command *) + +SearchRewrite (_+0). (* left *) +SearchRewrite (0+_). (* right *) diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v index 4a460a83..c4592369 100644 --- a/test-suite/output/reduction.v +++ b/test-suite/output/reduction.v @@ -9,5 +9,5 @@ Eval simpl in (fix plus (n m : nat) {struct n} : nat := | S p => S (p + m) end) a a. -Eval hnf in match (plus (S n) O) with S n => n | _ => O end. +Eval hnf in match (plus (S n) O) with S n => n | _ => O end. diff --git a/test-suite/output/set.out b/test-suite/output/set.out new file mode 100644 index 00000000..333fbb86 --- /dev/null +++ b/test-suite/output/set.out @@ -0,0 +1,21 @@ +1 subgoal + + y1 := 0 : nat + x := 0 + 0 : nat + ============================ + x = x +1 subgoal + + y1 := 0 : nat + y2 := 0 : nat + x := y2 + 0 : nat + ============================ + x = x +1 subgoal + + y1 := 0 : nat + y2 := 0 : nat + y3 := 0 : nat + x := y2 + y3 : nat + ============================ + x = x diff --git a/test-suite/output/set.v b/test-suite/output/set.v new file mode 100644 index 00000000..0e745354 --- /dev/null +++ b/test-suite/output/set.v @@ -0,0 +1,10 @@ +Goal let x:=O+O in x=x. +intro. +set (y1:=O) in (type of x). +Show. +set (y2:=O) in (value of x) at 1. +Show. +set (y3:=O) in (value of x). +Show. +trivial. +Qed. diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out new file mode 100644 index 00000000..73888da9 --- /dev/null +++ b/test-suite/output/simpl.out @@ -0,0 +1,15 @@ +1 subgoal + + x : nat + ============================ + x = S x +1 subgoal + + x : nat + ============================ + 0 + x = S x +1 subgoal + + x : nat + ============================ + x = 1 + x diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v new file mode 100644 index 00000000..5f1926f1 --- /dev/null +++ b/test-suite/output/simpl.v @@ -0,0 +1,13 @@ +(* Simpl with patterns *) + +Goal forall x, 0+x = 1+x. +intro x. +simpl (_ + x). +Show. +Undo. +simpl (_ + x) at 2. +Show. +Undo. +simpl (0 + _). +Show. +Undo. |