summaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/Abstract.v2
-rw-r--r--test-suite/success/AdvancedCanonicalStructure.v27
-rw-r--r--test-suite/success/AdvancedTypeClasses.v78
-rw-r--r--test-suite/success/Case12.v4
-rw-r--r--test-suite/success/Case15.v6
-rw-r--r--test-suite/success/Case17.v12
-rw-r--r--test-suite/success/Case3.v29
-rw-r--r--test-suite/success/Cases.v37
-rw-r--r--test-suite/success/CasesDep.v82
-rw-r--r--test-suite/success/Discriminate.v4
-rw-r--r--test-suite/success/Equations.v321
-rw-r--r--test-suite/success/Field.v26
-rw-r--r--test-suite/success/Fixpoint.v45
-rw-r--r--test-suite/success/Fourier.v4
-rw-r--r--test-suite/success/Funind.v98
-rw-r--r--test-suite/success/Generalization.v1
-rw-r--r--test-suite/success/Hints.v27
-rw-r--r--test-suite/success/Import.v11
-rw-r--r--test-suite/success/Inductive.v36
-rw-r--r--test-suite/success/Injection.v2
-rw-r--r--test-suite/success/Inversion.v36
-rw-r--r--test-suite/success/LegacyField.v10
-rw-r--r--test-suite/success/LetPat.v12
-rw-r--r--test-suite/success/Notations.v32
-rw-r--r--test-suite/success/Nsatz.v216
-rw-r--r--test-suite/success/Nsatz_domain.v274
-rw-r--r--test-suite/success/Omega0.v44
-rw-r--r--test-suite/success/Omega2.v2
-rw-r--r--test-suite/success/OmegaPre.v2
-rw-r--r--test-suite/success/ProgramWf.v99
-rw-r--r--test-suite/success/Projection.v6
-rw-r--r--test-suite/success/ROmega.v2
-rw-r--r--test-suite/success/ROmega0.v44
-rw-r--r--test-suite/success/ROmega2.v4
-rw-r--r--test-suite/success/ROmegaPre.v2
-rw-r--r--test-suite/success/RecTutorial.v208
-rw-r--r--test-suite/success/Record.v23
-rw-r--r--test-suite/success/Section.v6
-rw-r--r--test-suite/success/Simplify_eq.v4
-rw-r--r--test-suite/success/Tauto.v2
-rw-r--r--test-suite/success/TestRefine.v17
-rw-r--r--test-suite/success/Typeclasses.v60
-rw-r--r--test-suite/success/apply.v163
-rw-r--r--test-suite/success/autointros.v15
-rw-r--r--test-suite/success/cc.v19
-rw-r--r--test-suite/success/change.v26
-rw-r--r--test-suite/success/clear.v2
-rw-r--r--test-suite/success/coercions.v3
-rw-r--r--test-suite/success/conv_pbs.v48
-rw-r--r--test-suite/success/decl_mode.v40
-rw-r--r--test-suite/success/dependentind.v63
-rw-r--r--test-suite/success/destruct.v29
-rw-r--r--test-suite/success/eauto.v2
-rw-r--r--test-suite/success/evars.v54
-rw-r--r--test-suite/success/extraction.v106
-rw-r--r--test-suite/success/fix.v4
-rw-r--r--test-suite/success/hyps_inclusion.v6
-rw-r--r--test-suite/success/implicit.v44
-rw-r--r--test-suite/success/import_lib.v50
-rw-r--r--test-suite/success/induct.v28
-rw-r--r--test-suite/success/ltac.v33
-rw-r--r--test-suite/success/mutual_ind.v6
-rw-r--r--test-suite/success/parsing.v2
-rw-r--r--test-suite/success/pattern.v42
-rw-r--r--test-suite/success/refine.v12
-rw-r--r--test-suite/success/replace.v10
-rw-r--r--test-suite/success/rewrite.v70
-rw-r--r--test-suite/success/setoid_ring_module.v4
-rw-r--r--test-suite/success/setoid_test.v2
-rw-r--r--test-suite/success/setoid_test2.v4
-rw-r--r--test-suite/success/setoid_test_function_space.v8
-rw-r--r--test-suite/success/simpl.v8
-rw-r--r--test-suite/success/specialize.v2
-rw-r--r--test-suite/success/unfold.v2
-rw-r--r--test-suite/success/unification.v26
-rw-r--r--test-suite/success/univers.v6
76 files changed, 1985 insertions, 911 deletions
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index fc8800a5..ffd50f6e 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -18,7 +18,7 @@ Proof.
induction n.
simpl ; apply Dummy0.
replace (2 * S n0) with (2*n0 + 2) ; auto with arith.
- apply DummyApp.
+ apply DummyApp.
2:exact Dummy2.
apply IHn0 ; abstract omega.
Defined.
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index 8e613dca..b533db6e 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -21,7 +21,6 @@ Parameter eq_img : forall (i1:img) (i2:img),
eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2).
Lemma phi_img (a:A) : img.
- intro a.
exists a (phi a).
refine ( refl_equal _).
Defined.
@@ -54,7 +53,7 @@ Open Scope type_scope.
Section type_reification.
-Inductive term :Type :=
+Inductive term :Type :=
Fun : term -> term -> term
| Prod : term -> term -> term
| Bool : term
@@ -63,18 +62,18 @@ Inductive term :Type :=
| TYPE :term
| Var : Type -> term.
-Fixpoint interp (t:term) :=
- match t with
+Fixpoint interp (t:term) :=
+ match t with
Bool => bool
| SET => Set
| PROP => Prop
- | TYPE => Type
+ | TYPE => Type
| Fun a b => interp a -> interp b
| Prod a b => interp a * interp b
| Var x => x
end.
-Record interp_pair :Type :=
+Record interp_pair :Type :=
{ repr:>term;
abs:>Type;
link: abs = interp repr }.
@@ -95,25 +94,25 @@ thus thesis using rewrite (link a);rewrite (link b);reflexivity.
end proof.
Qed.
-Canonical Structure ProdCan (a b:interp_pair) :=
+Canonical Structure ProdCan (a b:interp_pair) :=
Build_interp_pair (Prod a b) (a * b) (prod_interp a b).
-Canonical Structure FunCan (a b:interp_pair) :=
+Canonical Structure FunCan (a b:interp_pair) :=
Build_interp_pair (Fun a b) (a -> b) (fun_interp a b).
-Canonical Structure BoolCan :=
+Canonical Structure BoolCan :=
Build_interp_pair Bool bool (refl_equal _).
-Canonical Structure VarCan (x:Type) :=
+Canonical Structure VarCan (x:Type) :=
Build_interp_pair (Var x) x (refl_equal _).
-Canonical Structure SetCan :=
+Canonical Structure SetCan :=
Build_interp_pair SET Set (refl_equal _).
-Canonical Structure PropCan :=
+Canonical Structure PropCan :=
Build_interp_pair PROP Prop (refl_equal _).
-Canonical Structure TypeCan :=
+Canonical Structure TypeCan :=
Build_interp_pair TYPE Type (refl_equal _).
(* Print Canonical Projections. *)
@@ -140,5 +139,5 @@ End type_reification.
-
+
diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
new file mode 100644
index 00000000..b4efa7ed
--- /dev/null
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -0,0 +1,78 @@
+Generalizable All Variables.
+
+Open Scope type_scope.
+
+Section type_reification.
+
+Inductive term :Type :=
+ Fun : term -> term -> term
+ | Prod : term -> term -> term
+ | Bool : term
+ | SET :term
+ | PROP :term
+ | TYPE :term
+ | Var : Type -> term.
+
+Fixpoint interp (t:term) :=
+ match t with
+ Bool => bool
+ | SET => Set
+ | PROP => Prop
+ | TYPE => Type
+ | Fun a b => interp a -> interp b
+ | Prod a b => interp a * interp b
+ | Var x => x
+end.
+
+Class interp_pair (abs : Type) :=
+ { repr : term;
+ link: abs = interp repr }.
+
+Implicit Arguments repr [[interp_pair]].
+Implicit Arguments link [[interp_pair]].
+
+Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)).
+ simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity.
+Qed.
+
+Lemma fun_interp :forall `{interp_pair a, interp_pair b}, (a -> b) = interp (Fun (repr a) (repr b)).
+ simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity.
+Qed.
+
+Coercion repr : interp_pair >-> term.
+
+Definition abs `{interp_pair a} : Type := a.
+Coercion abs : interp_pair >-> Sortclass.
+
+Lemma fun_interp' :forall `{ia : interp_pair, ib : interp_pair}, (ia -> ib) = interp (Fun ia ib).
+ simpl. intros a ia b ib. rewrite <- link. rewrite <- (link b). reflexivity.
+Qed.
+
+Instance ProdCan `(interp_pair a, interp_pair b) : interp_pair (a * b) :=
+ { repr := Prod (repr a) (repr b) ; link := prod_interp }.
+
+Instance FunCan `(interp_pair a, interp_pair b) : interp_pair (a -> b) :=
+ { link := fun_interp }.
+
+Instance BoolCan : interp_pair bool :=
+ { repr := Bool ; link := refl_equal _ }.
+
+Instance VarCan x : interp_pair x | 10 := { repr := Var x ; link := refl_equal _ }.
+Instance SetCan : interp_pair Set := { repr := SET ; link := refl_equal _ }.
+Instance PropCan : interp_pair Prop := { repr := PROP ; link := refl_equal _ }.
+Instance TypeCan : interp_pair Type := { repr := TYPE ; link := refl_equal _ }.
+
+(* Print Canonical Projections. *)
+
+Variable A:Type.
+
+Variable Inhabited: term -> Prop.
+
+Variable Inhabited_correct: forall `{interp_pair p}, Inhabited (repr p) -> p.
+
+Lemma L : Prop * A -> bool * (Type -> Set) .
+apply (Inhabited_correct _ _).
+change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))).
+Admitted.
+
+End type_reification.
diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v
index f6a0d578..729ab824 100644
--- a/test-suite/success/Case12.v
+++ b/test-suite/success/Case12.v
@@ -62,10 +62,10 @@ Check
Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set :=
| nil''' : list''' A a (a,a)
- | cons''' :
+ | cons''' :
forall a' : A, let m := (a',a) in list''' A a m -> list''' A a (a,a).
-Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m)
+Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m)
{struct l} : nat :=
match l with
| nil''' => 0
diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v
index 8431880d..69fca48e 100644
--- a/test-suite/success/Case15.v
+++ b/test-suite/success/Case15.v
@@ -12,7 +12,7 @@ Check
(* Suggested by Pierre Letouzey (PR#207) *)
Inductive Boite : Set :=
- boite : forall b : bool, (if b then nat else (nat * nat)%type) -> Boite.
+ boite : forall b : bool, (if b then nat else (nat * nat)%type) -> Boite.
Definition test (B : Boite) :=
match B return nat with
@@ -30,7 +30,7 @@ Check [x]
end.
Check [x]
- Cases x of
+ Cases x of
(c true true) => true
| (c false O) => true
| _ => false
@@ -40,7 +40,7 @@ Check [x]
Check
[x:I]
Cases x of
- (c b y) =>
+ (c b y) =>
(<[b:bool](if b then bool else nat)->bool>if b
then [y](if y then true else false)
else [y]Cases y of
diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v
index 061e136e..66af9e0d 100644
--- a/test-suite/success/Case17.v
+++ b/test-suite/success/Case17.v
@@ -11,7 +11,7 @@ Variables (l0 : list bool)
(rec :
forall l' : list bool,
length l' <= S (length l0) ->
- {l'' : list bool &
+ {l'' : list bool &
{t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
{(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}).
@@ -25,17 +25,17 @@ Check
| inleft (existS _ _) => inright _ (HHH _)
| inright Hnp => inright _ (HHH _)
end
- :{l'' : list bool &
+ :{l'' : list bool &
{t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} +
{(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}).
-
+
(* The same but with relative links to l0 and rec *)
-
+
Check
(fun (l0 : list bool)
(rec : forall l' : list bool,
length l' <= S (length l0) ->
- {l'' : list bool &
+ {l'' : list bool &
{t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
{(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) =>
match rec l0 (HHH _) with
@@ -45,6 +45,6 @@ Check
| inleft (existS _ _) => inright _ (HHH _)
| inright Hnp => inright _ (HHH _)
end
- :{l'' : list bool &
+ :{l'' : list bool &
{t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} +
{(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}).
diff --git a/test-suite/success/Case3.v b/test-suite/success/Case3.v
new file mode 100644
index 00000000..de7784ae
--- /dev/null
+++ b/test-suite/success/Case3.v
@@ -0,0 +1,29 @@
+Inductive Le : nat -> nat -> Set :=
+ | LeO : forall n : nat, Le 0 n
+ | LeS : forall n m : nat, Le n m -> Le (S n) (S m).
+
+Parameter discr_l : forall n : nat, S n <> 0.
+
+Type
+ (fun n : nat =>
+ match n return (n = 0 \/ n <> 0) with
+ | O => or_introl (0 <> 0) (refl_equal 0)
+ | S O => or_intror (1 = 0) (discr_l 0)
+ | S (S x) => or_intror (S (S x) = 0) (discr_l (S x))
+ end).
+
+Parameter iguales : forall (n m : nat) (h : Le n m), Prop.
+
+Type
+ match LeO 0 as h in (Le n m) return Prop with
+ | LeO O => True
+ | LeS (S x) (S y) H => iguales (S x) (S y) H
+ | _ => False
+ end.
+
+Type
+ match LeO 0 as h in (Le n m) return Prop with
+ | LeO O => True
+ | LeS (S x) O H => iguales (S x) 0 H
+ | _ => False
+ end.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 499c0660..e63972ce 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -31,10 +31,11 @@ Type
(* Interaction with coercions *)
Parameter bool2nat : bool -> nat.
Coercion bool2nat : bool >-> nat.
-Check (fun x => match x with
- | O => true
- | S _ => 0
- end:nat).
+Definition foo : nat -> nat :=
+ fun x => match x with
+ | O => true
+ | S _ => 0
+ end.
(****************************************************************************)
(* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *)
@@ -255,7 +256,7 @@ Type match 0, 1 return nat with
Type match 0, 1 with
| x, y => x + y
end.
-
+
Type match 0, 1 return nat with
| O, y => y
| S x, y => x + y
@@ -522,7 +523,7 @@ Type
| O, _ => 0
| S _, _ => c
end).
-
+
(* Rows of pattern variables: some tricky cases *)
Axioms (P : nat -> Prop) (f : forall n : nat, P n).
@@ -612,14 +613,14 @@ Type
(*
Type [A:Set][n:nat][l:(Listn A n)]
- <[_:nat](Listn A O)>Cases l of
+ <[_:nat](Listn A O)>Cases l of
(Niln as b) => b
| (Consn n a (Niln as b))=> (Niln A)
| (Consn n a (Consn m b l)) => (Niln A)
end.
Type [A:Set][n:nat][l:(Listn A n)]
- Cases l of
+ Cases l of
(Niln as b) => b
| (Consn n a (Niln as b))=> (Niln A)
| (Consn n a (Consn m b l)) => (Niln A)
@@ -627,9 +628,9 @@ Type [A:Set][n:nat][l:(Listn A n)]
*)
(******** This example rises an error unconstrained_variables!
Type [A:Set][n:nat][l:(Listn A n)]
- Cases l of
+ Cases l of
(Niln as b) => (Consn A O O b)
- | ((Consn n a Niln) as L) => L
+ | ((Consn n a Niln) as L) => L
| (Consn n a _) => (Consn A O O (Niln A))
end.
**********)
@@ -956,7 +957,7 @@ Definition length3 (n : nat) (l : listn n) :=
| _ => 0
end.
-
+
Type match LeO 0 return nat with
| LeS n m h => n + m
| x => 0
@@ -1071,10 +1072,10 @@ Type
| Consn _ _ _ as b => b
end).
-(** Horrible error message!
+(** Horrible error message!
Type [A:Set][n:nat][l:(Listn A n)]
- Cases l of
+ Cases l of
(Niln as b) => b
| ((Consn _ _ _ ) as b)=> b
end.
@@ -1179,7 +1180,7 @@ Type (fun n : nat => match test n with
Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}.
Type
match compare 0 0 return nat with
-
+
(* k<i *) | inleft (left _) => 0
(* k=i *) | inleft _ => 0
(* k>i *) | inright _ => 0
@@ -1187,7 +1188,7 @@ Type
Type
match compare 0 0 with
-
+
(* k<i *) | inleft (left _) => 0
(* k=i *) | inleft _ => 0
(* k>i *) | inright _ => 0
@@ -1374,7 +1375,7 @@ Type
| var, var => True
| oper op1 l1, oper op2 l2 => False
| _, _ => False
- end.
+ end.
Reset LTERM.
@@ -1660,7 +1661,7 @@ Type
| Cons a x, Cons b y => V4 a x b y
end).
-
+
(* ===================================== *)
Inductive Eqlong :
@@ -1724,7 +1725,7 @@ Parameter
-Fixpoint Eqlongdec (n : nat) (x : listn n) (m : nat)
+Fixpoint Eqlongdec (n : nat) (x : listn n) (m : nat)
(y : listn m) {struct x} : Eqlong n x m y \/ ~ Eqlong n x m y :=
match
x in (listn n), y in (listn m)
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 49bd77fc..29721843 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -38,29 +38,29 @@ Require Import Logic_Type.
Section Orderings.
Variable U : Type.
-
+
Definition Relation := U -> U -> Prop.
Variable R : Relation.
-
+
Definition Reflexive : Prop := forall x : U, R x x.
-
+
Definition Transitive : Prop := forall x y z : U, R x y -> R y z -> R x z.
-
+
Definition Symmetric : Prop := forall x y : U, R x y -> R y x.
-
+
Definition Antisymmetric : Prop := forall x y : U, R x y -> R y x -> x = y.
-
+
Definition contains (R R' : Relation) : Prop :=
forall x y : U, R' x y -> R x y.
Definition same_relation (R R' : Relation) : Prop :=
contains R R' /\ contains R' R.
Inductive Equivalence : Prop :=
Build_Equivalence : Reflexive -> Transitive -> Symmetric -> Equivalence.
-
+
Inductive PER : Prop :=
Build_PER : Symmetric -> Transitive -> PER.
-
+
End Orderings.
(***** Setoid *******)
@@ -105,7 +105,7 @@ Definition Map_setoid := Build_Setoid Map ext Equiv_map_eq.
End Maps.
-Notation ap := (explicit_ap _ _).
+Notation ap := (explicit_ap _ _).
(* <Warning> : Grammar is replaced by Notation *)
@@ -128,8 +128,8 @@ Axiom eq_Suc : forall n m : posint, n = m -> Suc n = Suc m.
Definition pred (n : posint) : posint :=
match n return posint with
- | Z => (* Z *) Z
- (* Suc u *)
+ | Z => (* Z *) Z
+ (* Suc u *)
| Suc u => u
end.
@@ -141,7 +141,7 @@ Axiom not_eq_Suc : forall n m : posint, n <> m -> Suc n <> Suc m.
Definition IsSuc (n : posint) : Prop :=
match n return Prop with
| Z => (* Z *) False
- (* Suc p *)
+ (* Suc p *)
| Suc p => True
end.
Definition IsZero (n : posint) : Prop :=
@@ -163,7 +163,7 @@ Definition Decidable (A : Type) (R : Relation A) :=
forall x y : A, R x y \/ ~ R x y.
-Record DSetoid : Type :=
+Record DSetoid : Type :=
{Set_of : Setoid; prf_decid : Decidable (elem Set_of) (equal Set_of)}.
(* example de Dsetoide d'entiers *)
@@ -190,7 +190,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci.
Section Sig.
-Record Signature : Type :=
+Record Signature : Type :=
{Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}.
Variable S : Signature.
@@ -268,8 +268,8 @@ Reset equalT.
Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
match t1 return (TERM -> Prop) with
- | var v1 =>
- (*var*)
+ | var v1 =>
+ (*var*)
fun t2 : TERM =>
match t2 return Prop with
| var v2 =>
@@ -289,12 +289,12 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2
end
end
-
+
with EqListT (n1 : posint) (l1 : LTERM n1) {struct l1} :
forall n2 : posint, LTERM n2 -> Prop :=
match l1 in (LTERM _) return (forall n2 : posint, LTERM n2 -> Prop) with
| nil =>
- (*nil*)
+ (*nil*)
fun (n2 : posint) (l2 : LTERM n2) =>
match l2 in (LTERM _) return Prop with
| nil =>
@@ -336,7 +336,7 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2
end
end
-
+
with EqListT (n1 : posint) (l1 : LTERM n1) {struct l1} :
forall n2 : posint, LTERM n2 -> Prop :=
match l1 return (forall n2 : posint, LTERM n2 -> Prop) with
@@ -374,8 +374,8 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2
end
end
-
- with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint)
+
+ with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint)
(l2 : LTERM n2) {struct l1} : Prop :=
match l1 with
| nil => match l2 with
@@ -401,8 +401,8 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop :=
equal _ op1 op2 /\ EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2
| _, _ => False
end
-
- with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint)
+
+ with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint)
(l2 : LTERM n2) {struct l1} : Prop :=
match l1, l2 with
| nil, nil => True
@@ -433,16 +433,16 @@ Inductive I : unit -> Type :=
| C : forall a, I a -> I tt.
(*
-Definition F (l:I tt) : l = l :=
+Definition F (l:I tt) : l = l :=
match l return l = l with
| C tt (C _ l') => refl_equal (C tt (C _ l'))
end.
one would expect that the compilation of F (this involves
-some kind of pattern-unification) would produce:
+some kind of pattern-unification) would produce:
*)
-Definition F (l:I tt) : l = l :=
+Definition F (l:I tt) : l = l :=
match l return l = l with
| C tt l' => match l' return C _ l' = C _ l' with C _ l'' => refl_equal (C tt (C _ l'')) end
end.
@@ -451,7 +451,7 @@ Inductive J : nat -> Type :=
| D : forall a, J (S a) -> J a.
(*
-Definition G (l:J O) : l = l :=
+Definition G (l:J O) : l = l :=
match l return l = l with
| D O (D 1 l') => refl_equal (D O (D 1 l'))
| D _ _ => refl_equal _
@@ -461,7 +461,7 @@ one would expect that the compilation of G (this involves inversion)
would produce:
*)
-Definition G (l:J O) : l = l :=
+Definition G (l:J O) : l = l :=
match l return l = l with
| D 0 l'' =>
match l'' as _l'' in J n return
@@ -480,3 +480,29 @@ Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) :=
| niln => w
| consn a n' v' => consn _ a _ (app v' w)
end.
+
+(* Testing regression of bug 2106 *)
+
+Set Implicit Arguments.
+Require Import List.
+
+Inductive nt := E.
+Definition root := E.
+Inductive ctor : list nt -> nt -> Type :=
+ Plus : ctor (cons E (cons E nil)) E.
+
+Inductive term : nt -> Type :=
+| Term : forall s n, ctor s n -> spine s -> term n
+with spine : list nt -> Type :=
+| EmptySpine : spine nil
+| ConsSpine : forall n s, term n -> spine s -> spine (n :: s).
+
+Inductive step : nt -> nt -> Type :=
+ | Step : forall l n r n' (c:ctor (l++n::r) n'), spine l -> spine r -> step n
+n'.
+
+Definition test (s:step E E) :=
+ match s with
+ | Step nil _ (cons E nil) _ Plus l l' => true
+ | _ => false
+ end.
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index b57c5478..dffad323 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -2,11 +2,11 @@
(* Check that Discriminate tries Intro until *)
-Lemma l1 : 0 = 1 -> False.
+Lemma l1 : 0 = 1 -> False.
discriminate 1.
Qed.
-Lemma l2 : forall H : 0 = 1, H = H.
+Lemma l2 : forall H : 0 = 1, H = H.
discriminate H.
Qed.
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
deleted file mode 100644
index e31135c2..00000000
--- a/test-suite/success/Equations.v
+++ /dev/null
@@ -1,321 +0,0 @@
-Require Import Program.
-
-Equations neg (b : bool) : bool :=
-neg true := false ;
-neg false := true.
-
-Eval compute in neg.
-
-Require Import Coq.Lists.List.
-
-Equations head A (default : A) (l : list A) : A :=
-head A default nil := default ;
-head A default (cons a v) := a.
-
-Eval compute in head.
-
-Equations tail {A} (l : list A) : (list A) :=
-tail A nil := nil ;
-tail A (cons a v) := v.
-
-Eval compute in @tail.
-
-Eval compute in (tail (cons 1 nil)).
-
-Reserved Notation " x ++ y " (at level 60, right associativity).
-
-Equations app' {A} (l l' : list A) : (list A) :=
-app' A nil l := l ;
-app' A (cons a v) l := cons a (app' v l).
-
-Equations app (l l' : list nat) : list nat :=
- [] ++ l := l ;
- (a :: v) ++ l := a :: (v ++ l)
-
-where " x ++ y " := (app x y).
-
-Eval compute in @app'.
-
-Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) :=
-zip' A f nil nil := nil ;
-zip' A f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ;
-zip' A f nil (cons b w) := nil ;
-zip' A f (cons a v) nil := nil.
-
-
-Eval compute in @zip'.
-
-Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) :=
-zip'' A f nil nil def := nil ;
-zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' f v w def) ;
-zip'' A f nil (cons b w) def := def ;
-zip'' A f (cons a v) nil def := def.
-
-Eval compute in @zip''.
-
-Inductive fin : nat -> Set :=
-| fz : Π {n}, fin (S n)
-| fs : Π {n}, fin n -> fin (S n).
-
-Inductive finle : Π (n : nat) (x : fin n) (y : fin n), Prop :=
-| leqz : Π {n j}, finle (S n) fz j
-| leqs : Π {n i j}, finle n i j -> finle (S n) (fs i) (fs j).
-
-Scheme finle_ind_dep := Induction for finle Sort Prop.
-
-Instance finle_ind_pack n x y : DependentEliminationPackage (finle n x y) :=
- { elim_type := _ ; elim := finle_ind_dep }.
-
-Implicit Arguments finle [[n]].
-
-Require Import Bvector.
-
-Implicit Arguments Vnil [[A]].
-Implicit Arguments Vcons [[A] [n]].
-
-Equations vhead {A n} (v : vector A (S n)) : A :=
-vhead A n (Vcons a v) := a.
-
-Equations vmap {A B} (f : A -> B) {n} (v : vector A n) : (vector B n) :=
-vmap A B f 0 Vnil := Vnil ;
-vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap f v).
-
-Eval compute in (vmap id (@Vnil nat)).
-Eval compute in (vmap id (@Vcons nat 2 _ Vnil)).
-Eval compute in @vmap.
-
-Equations Below_nat (P : nat -> Type) (n : nat) : Type :=
-Below_nat P 0 := unit ;
-Below_nat P (S n) := prod (P n) (Below_nat P n).
-
-Equations below_nat (P : nat -> Type) n (step : Π (n : nat), Below_nat P n -> P n) : Below_nat P n :=
-below_nat P 0 step := tt ;
-below_nat P (S n) step := let rest := below_nat P n step in
- (step n rest, rest).
-
-Class BelowPack (A : Type) :=
- { Below : Type ; below : Below }.
-
-Instance nat_BelowPack : BelowPack nat :=
- { Below := Π P n step, Below_nat P n ;
- below := λ P n step, below_nat P n (step P) }.
-
-Definition rec_nat (P : nat -> Type) n (step : Π n, Below_nat P n -> P n) : P n :=
- step n (below_nat P n step).
-
-Fixpoint Below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) : Type :=
- match v with Vnil => unit | Vcons a n' v' => prod (P A n' v') (Below_vector P A n' v') end.
-
-Equations below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n)
- (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : Below_vector P A n v :=
-below_vector P A ?(0) Vnil step := tt ;
-below_vector P A ?(S n) (Vcons a v) step :=
- let rest := below_vector P A n v step in
- (step A n v rest, rest).
-
-Instance vector_BelowPack : BelowPack (Π A n, vector A n) :=
- { Below := Π P A n v step, Below_vector P A n v ;
- below := λ P A n v step, below_vector P A n v (step P) }.
-
-Instance vector_noargs_BelowPack A n : BelowPack (vector A n) :=
- { Below := Π P v step, Below_vector P A n v ;
- below := λ P v step, below_vector P A n v (step P) }.
-
-Definition rec_vector (P : Π A n, vector A n -> Type) A n v
- (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : P A n v :=
- step A n v (below_vector P A n v step).
-
-Class Recursor (A : Type) (BP : BelowPack A) :=
- { rec_type : Π x : A, Type ; rec : Π x : A, rec_type x }.
-
-Instance nat_Recursor : Recursor nat nat_BelowPack :=
- { rec_type := λ n, Π P step, P n ;
- rec := λ n P step, rec_nat P n (step P) }.
-
-(* Instance vect_Recursor : Recursor (Π A n, vector A n) vector_BelowPack := *)
-(* rec_type := Π (P : Π A n, vector A n -> Type) step A n v, P A n v; *)
-(* rec := λ P step A n v, rec_vector P A n v step. *)
-
-Instance vect_Recursor_noargs A n : Recursor (vector A n) (vector_noargs_BelowPack A n) :=
- { rec_type := λ v, Π (P : Π A n, vector A n -> Type) step, P A n v;
- rec := λ v P step, rec_vector P A n v step }.
-
-Implicit Arguments Below_vector [P A n].
-
-Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
-
-(** Won't pass the guardness check which diverges anyway. *)
-
-(* Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k := *)
-(* trans ?(S n) ?(fz) ?(j) ?(k) leqz q := leqz ; *)
-(* trans ?(S n) ?(fs i) ?(fs j) ?(fs k) (leqs p) (leqs q) := leqs (trans p q). *)
-
-(* Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz. *)
-(* Proof. intros. simplify_equations ; reflexivity. Qed. *)
-
-(* Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q). *)
-(* Proof. intros. simplify_equations ; reflexivity. Qed. *)
-
-Section Image.
- Context {S T : Type}.
- Variable f : S -> T.
-
- Inductive Imf : T -> Type := imf (s : S) : Imf (f s).
-
- Equations inv (t : T) (im : Imf t) : S :=
- inv (f s) (imf s) := s.
-
-End Image.
-
-Section Univ.
-
- Inductive univ : Set :=
- | ubool | unat | uarrow (from:univ) (to:univ).
-
- Equations interp (u : univ) : Type :=
- interp ubool := bool ; interp unat := nat ;
- interp (uarrow from to) := interp from -> interp to.
-
- Equations foo (u : univ) (el : interp u) : interp u :=
- foo ubool true := false ;
- foo ubool false := true ;
- foo unat t := t ;
- foo (uarrow from to) f := id ∘ f.
-
- Eval lazy beta delta [ foo foo_obligation_1 foo_obligation_2 ] iota zeta in foo.
-
-End Univ.
-
-Eval compute in (foo ubool false).
-Eval compute in (foo (uarrow ubool ubool) negb).
-Eval compute in (foo (uarrow ubool ubool) id).
-
-Inductive foobar : Set := bar | baz.
-
-Equations bla (f : foobar) : bool :=
-bla bar := true ;
-bla baz := false.
-
-Eval simpl in bla.
-Print refl_equal.
-
-Notation "'refl'" := (@refl_equal _ _).
-
-Equations K {A} (x : A) (P : x = x -> Type) (p : P (refl_equal x)) (p : x = x) : P p :=
-K A x P p refl := p.
-
-Equations eq_sym {A} (x y : A) (H : x = y) : y = x :=
-eq_sym A x x refl := refl.
-
-Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z :=
-eq_trans A x x x refl refl := refl.
-
-Lemma eq_trans_eq A x : @eq_trans A x x x refl refl = refl.
-Proof. reflexivity. Qed.
-
-Equations nth {A} {n} (v : vector A n) (f : fin n) : A :=
-nth A (S n) (Vcons a v) fz := a ;
-nth A (S n) (Vcons a v) (fs f) := nth v f.
-
-Equations tabulate {A} {n} (f : fin n -> A) : vector A n :=
-tabulate A 0 f := Vnil ;
-tabulate A (S n) f := Vcons (f fz) (tabulate (f ∘ fs)).
-
-Equations vlast {A} {n} (v : vector A (S n)) : A :=
-vlast A 0 (Vcons a Vnil) := a ;
-vlast A (S n) (Vcons a (n:=S n) v) := vlast v.
-
-Print Assumptions vlast.
-
-Equations vlast' {A} {n} (v : vector A (S n)) : A :=
-vlast' A ?(0) (Vcons a Vnil) := a ;
-vlast' A ?(S n) (Vcons a (n:=S n) v) := vlast' v.
-
-Lemma vlast_equation1 A (a : A) : vlast' (Vcons a Vnil) = a.
-Proof. intros. simplify_equations. reflexivity. Qed.
-
-Lemma vlast_equation2 A n a v : @vlast' A (S n) (Vcons a v) = vlast' v.
-Proof. intros. simplify_equations ; reflexivity. Qed.
-
-Print Assumptions vlast'.
-Print Assumptions nth.
-Print Assumptions tabulate.
-
-Extraction vlast.
-Extraction vlast'.
-
-Equations vliat {A} {n} (v : vector A (S n)) : vector A n :=
-vliat A 0 (Vcons a Vnil) := Vnil ;
-vliat A (S n) (Vcons a v) := Vcons a (vliat v).
-
-Eval compute in (vliat (Vcons 2 (Vcons 5 (Vcons 4 Vnil)))).
-
-Equations vapp' {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
-vapp' A ?(0) m Vnil w := w ;
-vapp' A ?(S n) m (Vcons a v) w := Vcons a (vapp' v w).
-
-Eval compute in @vapp'.
-
-Fixpoint vapp {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
- match v with
- | Vnil => w
- | Vcons a n' v' => Vcons a (vapp v' w)
- end.
-
-Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x y -> JMeq (Vcons a x) (Vcons a y).
-Proof. intros until y. simplify_dep_elim. reflexivity. Qed.
-
-Equations NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop :=
-NoConfusion_fin P (S n) fz fz := P -> P ;
-NoConfusion_fin P (S n) fz (fs y) := P ;
-NoConfusion_fin P (S n) (fs x) fz := P ;
-NoConfusion_fin P (S n) (fs x) (fs y) := (x = y -> P) -> P.
-
-Eval compute in NoConfusion_fin.
-Eval compute in NoConfusion_fin_comp.
-
-Print Assumptions NoConfusion_fin.
-
-Eval compute in (fun P n => NoConfusion_fin P (n:=S n) fz fz).
-
-(* Equations noConfusion_fin P (n : nat) (x y : fin n) (H : x = y) : NoConfusion_fin P x y := *)
-(* noConfusion_fin P (S n) fz fz refl := λ p _, p ; *)
-(* noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl. *)
-
-Equations_nocomp NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop :=
-NoConfusion_vect P A 0 Vnil Vnil := P -> P ;
-NoConfusion_vect P A (S n) (Vcons a x) (Vcons b y) := (a = b -> x = y -> P) -> P.
-
-Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y :=
-noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ;
-noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl.
-
-(* Instance fin_noconf n : NoConfusionPackage (fin n) := *)
-(* NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ; *)
-(* noConfusion := λ P x y, noConfusion_fin P n x y. *)
-
-Instance vect_noconf A n : NoConfusionPackage (vector A n) :=
- { NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ;
- noConfusion := λ P x y, noConfusion_vect P A n x y }.
-
-Equations fog {n} (f : fin n) : nat :=
-fog (S n) fz := 0 ; fog (S n) (fs f) := S (fog f).
-
-Inductive Split {X : Set}{m n : nat} : vector X (m + n) -> Set :=
- append : Π (xs : vector X m)(ys : vector X n), Split (vapp xs ys).
-
-Implicit Arguments Split [[X]].
-
-Equations_nocomp split {X : Set}(m n : nat) (xs : vector X (m + n)) : Split m n xs :=
-split X 0 n xs := append Vnil xs ;
-split X (S m) n (Vcons x xs) :=
- let 'append xs' ys' in Split _ _ vec := split m n xs return Split (S m) n (Vcons x vec) in
- append (Vcons x xs') ys'.
-
-Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))).
-Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))).
-
-Extraction Inline split_obligation_1 split_obligation_2.
-Recursive Extraction split.
-
-Eval compute in @split.
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index b4c06c7b..dd82036e 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field.v 9197 2006-10-02 15:55:52Z barras $ *)
+(* $Id$ *)
(**** Tests of Field with real numbers ****)
@@ -31,7 +31,7 @@ Proof.
intros.
field.
Abort.
-
+
(* Example 3 *)
Goal forall a b : R, 1 / (a * b) * (1 / (1 / b)) = 1 / a.
Proof.
@@ -44,7 +44,7 @@ Proof.
intros.
field_simplify_eq.
Abort.
-
+
Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a.
Proof.
intros.
@@ -58,21 +58,21 @@ Proof.
intros.
field; auto.
Qed.
-
+
(* Example 5 *)
Goal forall a : R, 1 = 1 * (1 / a) * a.
Proof.
intros.
field.
Abort.
-
+
(* Example 6 *)
Goal forall a b : R, b = b * / a * a.
Proof.
intros.
field.
Abort.
-
+
(* Example 7 *)
Goal forall a b : R, b = b * (1 / a) * a.
Proof.
@@ -81,11 +81,17 @@ Proof.
Abort.
(* Example 8 *)
-Goal
-forall x y : R,
-x * (1 / x + x / (x + y)) =
-- (1 / y) * y * (- (x * (x / (x + y))) - 1).
+Goal forall x y : R,
+ x * (1 / x + x / (x + y)) =
+ - (1 / y) * y * (- (x * (x / (x + y))) - 1).
Proof.
intros.
field.
Abort.
+
+(* Example 9 *)
+Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a -> False.
+Proof.
+intros.
+field_simplify_eq in H.
+Abort.
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index cf821073..3a4f8899 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -5,7 +5,7 @@ Inductive listn : nat -> Set :=
| consn : forall n:nat, nat -> listn n -> listn (S n).
Fixpoint f (n:nat) (m:=pred n) (l:listn m) (p:=S n) {struct l} : nat :=
- match n with O => p | _ =>
+ match n with O => p | _ =>
match l with niln => p | consn q _ l => f (S q) l end
end.
@@ -48,3 +48,46 @@ Fixpoint foldrn n bs :=
End folding.
+(* Check definition by tactics *)
+
+Set Automatic Introduction.
+
+Inductive even : nat -> Type :=
+ | even_O : even 0
+ | even_S : forall n, odd n -> even (S n)
+with odd : nat -> Type :=
+ odd_S : forall n, even n -> odd (S n).
+
+Fixpoint even_div2 n (H:even n) : nat :=
+ match H with
+ | even_O => 0
+ | even_S n H => S (odd_div2 n H)
+ end
+with odd_div2 n H : nat.
+destruct H.
+apply even_div2 with n.
+assumption.
+Qed.
+
+Fixpoint even_div2' n (H:even n) : nat with odd_div2' n (H:odd n) : nat.
+destruct H.
+exact 0.
+apply odd_div2' with n.
+assumption.
+destruct H.
+apply even_div2' with n.
+assumption.
+Qed.
+
+CoInductive Stream1 (A B:Type) := Cons1 : A -> Stream2 A B -> Stream1 A B
+with Stream2 (A B:Type) := Cons2 : B -> Stream1 A B -> Stream2 A B.
+
+CoFixpoint ex1 (n:nat) (b:bool) : Stream1 nat bool
+with ex2 (n:nat) (b:bool) : Stream2 nat bool.
+apply Cons1.
+exact n.
+apply (ex2 n b).
+apply Cons2.
+exact b.
+apply (ex1 (S n) (negb b)).
+Defined.
diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v
index 2d184fef..b63bead4 100644
--- a/test-suite/success/Fourier.v
+++ b/test-suite/success/Fourier.v
@@ -1,10 +1,10 @@
Require Import Rfunctions.
Require Import Fourier.
-
+
Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
intros; split_Rabs; fourier.
Qed.
-
+
Lemma l2 :
forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
intros.
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 1c3e56f2..b17adef6 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -6,7 +6,7 @@ Definition iszero (n : nat) : bool :=
end.
Functional Scheme iszero_ind := Induction for iszero Sort Prop.
-
+
Lemma toto : forall n : nat, n = 0 -> iszero n = true.
intros x eg.
functional induction iszero x; simpl in |- *.
@@ -14,7 +14,7 @@ trivial.
inversion eg.
Qed.
-
+
Function ftest (n m : nat) : nat :=
match n with
| O => match m with
@@ -30,7 +30,7 @@ intros n m.
Qed.
Lemma test2 : forall m n, ~ 2 = ftest n m.
-Proof.
+Proof.
intros n m;intro H.
functional inversion H ftest.
Qed.
@@ -45,9 +45,9 @@ Require Import Arith.
Lemma test11 : forall m : nat, ftest 0 m <= 2.
intros m.
functional induction ftest 0 m.
-auto.
auto.
-auto with *.
+auto.
+auto with *.
Qed.
Function lamfix (m n : nat) {struct n } : nat :=
@@ -92,7 +92,7 @@ Function trivfun (n : nat) : nat :=
end.
-(* essaie de parametre variables non locaux:*)
+(* essaie de parametre variables non locaux:*)
Parameter varessai : nat.
@@ -101,7 +101,7 @@ Lemma first_try : trivfun varessai = 0.
trivial.
assumption.
Defined.
-
+
Functional Scheme triv_ind := Induction for trivfun Sort Prop.
@@ -134,7 +134,7 @@ Function funex (n : nat) : nat :=
| S r => funex r
end
end.
-
+
Function nat_equal_bool (n m : nat) {struct n} : bool :=
match n with
@@ -150,7 +150,7 @@ Function nat_equal_bool (n m : nat) {struct n} : bool :=
Require Export Div2.
-
+
Functional Scheme div2_ind := Induction for div2 Sort Prop.
Lemma div2_inf : forall n : nat, div2 n <= n.
intros n.
@@ -177,7 +177,7 @@ intros n m.
functional induction nested_lam n m; simpl;auto.
Qed.
-
+
Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
let (n, m) := (p: nat*nat) in
match n with
@@ -187,7 +187,7 @@ Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
| S r => S (essai r (q, m))
end
end.
-
+
Lemma essai_essai :
forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p.
intros x p.
@@ -209,30 +209,30 @@ Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
| false => S recapp
end
end.
-
+
Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
intros a b.
functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto.
Qed.
-
+
Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
intros n m.
functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
-rewrite <- hyp in y; simpl in y;tauto.
+rewrite <- hyp in y; simpl in y;tauto.
inversion hyp.
Qed.
-
+
Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
intros n m.
functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto.
inversion eg.
inversion eg.
Qed.
-
-
+
+
Inductive istrue : bool -> Prop :=
istrue0 : istrue true.
-
+
Functional Scheme plus_ind := Induction for plus Sort Prop.
Lemma inf_x_plusxy' : forall x y : nat, x <= x + y.
@@ -242,7 +242,7 @@ auto with arith.
auto with arith.
Qed.
-
+
Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0.
intros n.
unfold plus in |- *.
@@ -251,7 +251,7 @@ auto with arith.
apply le_n_S.
assumption.
Qed.
-
+
Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x.
intros n.
functional induction plus 0 n; intros; auto with arith.
@@ -263,25 +263,25 @@ Function mod2 (n : nat) : nat :=
| S (S m) => S (mod2 m)
| _ => 0
end.
-
+
Lemma princ_mod2 : forall n : nat, mod2 n <= n.
intros n.
functional induction mod2 n; simpl in |- *; auto with arith.
Qed.
-
+
Function isfour (n : nat) : bool :=
match n with
| S (S (S (S O))) => true
| _ => false
end.
-
+
Function isononeorfour (n : nat) : bool :=
match n with
| S O => true
| S (S (S (S O))) => true
| _ => false
end.
-
+
Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n).
intros n.
functional induction isononeorfour n; intros istr; simpl in |- *;
@@ -294,14 +294,14 @@ destruct n. inversion istr.
destruct n. tauto.
simpl in *. inversion H0.
Qed.
-
+
Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
intros n.
functional induction isononeorfour n; intros m istr; inversion istr.
apply istrue0.
rewrite H in y; simpl in y;tauto.
Qed.
-
+
Function ftest4 (n m : nat) : nat :=
match n with
| O => match m with
@@ -313,12 +313,12 @@ Function ftest4 (n m : nat) : nat :=
| S r => 1
end
end.
-
+
Lemma test4 : forall n m : nat, ftest n m <= 2.
intros n m.
functional induction ftest n m; auto with arith.
Qed.
-
+
Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2.
intros n m.
assert ({n0 | n0 = S n}).
@@ -332,7 +332,7 @@ inversion 1.
auto with arith.
auto with arith.
Qed.
-
+
Function ftest44 (x : nat * nat) (n m : nat) : nat :=
let (p, q) := (x: nat*nat) in
match n with
@@ -345,7 +345,7 @@ Function ftest44 (x : nat * nat) (n m : nat) : nat :=
| S r => 1
end
end.
-
+
Lemma test44 :
forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2.
intros pq n m o r s.
@@ -355,7 +355,7 @@ auto with arith.
auto with arith.
auto with arith.
Qed.
-
+
Function ftest2 (n m : nat) {struct n} : nat :=
match n with
| O => match m with
@@ -364,12 +364,12 @@ Function ftest2 (n m : nat) {struct n} : nat :=
end
| S p => ftest2 p m
end.
-
+
Lemma test2' : forall n m : nat, ftest2 n m <= 2.
intros n m.
functional induction ftest2 n m; simpl in |- *; intros; auto.
Qed.
-
+
Function ftest3 (n m : nat) {struct n} : nat :=
match n with
| O => 0
@@ -378,7 +378,7 @@ Function ftest3 (n m : nat) {struct n} : nat :=
| S r => 0
end
end.
-
+
Lemma test3' : forall n m : nat, ftest3 n m <= 2.
intros n m.
functional induction ftest3 n m.
@@ -390,7 +390,7 @@ intros.
simpl in |- *.
auto.
Qed.
-
+
Function ftest5 (n m : nat) {struct n} : nat :=
match n with
| O => 0
@@ -399,7 +399,7 @@ Function ftest5 (n m : nat) {struct n} : nat :=
| S r => ftest5 p r
end
end.
-
+
Lemma test5 : forall n m : nat, ftest5 n m <= 2.
intros n m.
functional induction ftest5 n m.
@@ -411,21 +411,21 @@ intros.
simpl in |- *.
auto.
Qed.
-
+
Function ftest7 (n : nat) : nat :=
match ftest5 n 0 with
| O => 0
| S r => 0
end.
-
+
Lemma essai7 :
forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2)
- (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2)
+ (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2)
(n : nat), ftest7 n <= 2.
intros hyp1 hyp2 n.
functional induction ftest7 n; auto.
Qed.
-
+
Function ftest6 (n m : nat) {struct n} : nat :=
match n with
| O => 0
@@ -435,7 +435,7 @@ Function ftest6 (n m : nat) {struct n} : nat :=
end
end.
-
+
Lemma princ6 :
(forall n m : nat, n = 0 -> ftest6 0 m <= 2) ->
(forall n m p : nat,
@@ -448,16 +448,16 @@ generalize hyp1 hyp2 hyp3.
clear hyp1 hyp2 hyp3.
functional induction ftest6 n m; auto.
Qed.
-
+
Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
intros n m.
functional induction ftest6 n m; simpl in |- *; auto.
Qed.
-(* Some tests with modules *)
+(* Some tests with modules *)
Module M.
-Function test_m (n:nat) : nat :=
- match n with
+Function test_m (n:nat) : nat :=
+ match n with
| 0 => 0
| S n => S (S (test_m n))
end.
@@ -470,14 +470,14 @@ reflexivity.
simpl;rewrite IHn0;reflexivity.
Qed.
End M.
-(* We redefine a new Function with the same name *)
-Function test_m (n:nat) : nat :=
+(* We redefine a new Function with the same name *)
+Function test_m (n:nat) : nat :=
pred n.
Lemma test_m_is_pred : forall n, test_m n = pred n.
-Proof.
+Proof.
intro n.
-functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*)
+functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*)
reflexivity.
Qed.
diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
index 6b503e95..de34e007 100644
--- a/test-suite/success/Generalization.v
+++ b/test-suite/success/Generalization.v
@@ -1,3 +1,4 @@
+Generalizable All Variables.
Check `(a = 0).
Check `(a = 0)%type.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index e1c74048..4aa00e68 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -23,11 +23,11 @@ Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H.
(* Checks that local names are accepted *)
Section A.
- Remark Refl : forall (A : Set) (x : A), x = x.
- Proof refl_equal.
+ Remark Refl : forall (A : Set) (x : A), x = x.
+ Proof. exact refl_equal. Defined.
Definition Sym := sym_equal.
Let Trans := trans_equal.
-
+
Hint Resolve Refl: foo.
Hint Resolve Sym: bar.
Hint Resolve Trans: foo2.
@@ -46,3 +46,24 @@ Section A.
End A.
+Axiom a : forall n, n=0 <-> n<=0.
+
+Hint Resolve -> a.
+Goal forall n, n=0 -> n<=0.
+auto.
+Qed.
+
+
+(* This example comes from Chlipala's ltamer *)
+(* It used to fail from r12902 to r13112 since type_of started to call *)
+(* e_cumul (instead of conv_leq) which was not able to unify "?id" and *)
+(* "(fun x => x) ?id" *)
+
+Notation "e :? pf" := (eq_rect _ (fun X : Set => X) e _ pf)
+ (no associativity, at level 90).
+
+Axiom cast_coalesce :
+ forall (T1 T2 T3 : Set) (e : T1) (pf1 : T1 = T2) (pf2 : T2 = T3),
+ ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2).
+
+Hint Rewrite cast_coalesce : ltamer.
diff --git a/test-suite/success/Import.v b/test-suite/success/Import.v
new file mode 100644
index 00000000..ff5c1ed7
--- /dev/null
+++ b/test-suite/success/Import.v
@@ -0,0 +1,11 @@
+(* Test visibility of imported objects *)
+
+Require Import make_local.
+
+(* Check local implicit arguments are not imported *)
+
+Check (f nat 0).
+
+(* Check local arguments scopes are not imported *)
+
+Check (f nat (0*0)).
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 1adcbd39..203fbbb7 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -1,4 +1,32 @@
-(* Check local definitions in context of inductive types *)
+(* Test des definitions inductives imbriquees *)
+
+Require Import List.
+
+Inductive X : Set :=
+ cons1 : list X -> X.
+
+Inductive Y : Set :=
+ cons2 : list (Y * Y) -> Y.
+
+(* Test inductive types with local definitions (arity) *)
+
+Inductive eq1 : forall A:Type, let B:=A in A -> Prop :=
+ refl1 : eq1 True I.
+
+Check
+ fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
+ let B := A in
+ fun (a : A) (e : eq1 A a) =>
+ match e in (eq1 A0 B0 a0) return (P A0 a0) with
+ | refl1 => f
+ end.
+
+Inductive eq2 (A:Type) (a:A)
+ : forall B C:Type, let D:=(A*B*C)%type in D -> Prop :=
+ refl2 : eq2 A a unit bool (a,tt,true).
+
+(* Check inductive types with local definitions (parameters) *)
+
Inductive A (C D : Prop) (E:=C) (F:=D) (x y : E -> F) : E -> Set :=
I : forall z : E, A C D x y z.
@@ -7,9 +35,9 @@ Check
let E := C in
let F := D in
fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type)
- (f : forall z : C, P z (I C D x y z)) (y0 : C)
+ (f : forall z : C, P z (I C D x y z)) (y0 : C)
(a : A C D x y y0) =>
- match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with
+ match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with
| I x0 => f x0
end).
@@ -20,7 +48,7 @@ Check
let E := C in
let F := D in
fun (x y : E -> F) (P : B C D x y -> Type)
- (f : forall p0 q0 : C, P (Build_B C D x y p0 q0))
+ (f : forall p0 q0 : C, P (Build_B C D x y p0 q0))
(b : B C D x y) =>
match b as b0 return (P b0) with
| Build_B x0 x1 => f x0 x1
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 867d7374..c5cd7380 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -17,7 +17,7 @@ Qed.
Lemma l3 :
forall x y : nat,
existS (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) =
- existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) ->
+ existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) ->
x = y.
intros x y H.
injection H.
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index b08ffcc3..5091b44c 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -5,13 +5,13 @@ Fixpoint T (n : nat) : Type :=
match n with
| O => nat -> Prop
| S n' => T n'
- end.
+ end.
Inductive R : forall n : nat, T n -> nat -> Prop :=
| RO : forall (Psi : T 0) (l : nat), Psi l -> R 0 Psi l
| RS :
- forall (n : nat) (Psi : T (S n)) (l : nat), R n Psi l -> R (S n) Psi l.
-Definition Psi00 (n : nat) : Prop := False.
-Definition Psi0 : T 0 := Psi00.
+ forall (n : nat) (Psi : T (S n)) (l : nat), R n Psi l -> R (S n) Psi l.
+Definition Psi00 (n : nat) : Prop := False.
+Definition Psi0 : T 0 := Psi00.
Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l.
inversion 1.
Abort.
@@ -39,14 +39,14 @@ extension I -> Type :=
| super_add :
forall r (e' : extension I),
in_extension r e ->
- super_extension e e' -> super_extension e (add_rule r e').
+ super_extension e e' -> super_extension e (add_rule r e').
Lemma super_def :
forall (I : Set) (e1 e2 : extension I),
super_extension e2 e1 -> forall ru, in_extension ru e1 -> in_extension ru e2.
-Proof.
+Proof.
simple induction 1.
inversion 1; auto.
elim magic.
@@ -105,5 +105,27 @@ Abort.
Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t).
Goal forall o, foo2 o -> 0 = 1.
intros.
-eapply trans_eq.
+eapply trans_eq.
inversion H.
+
+(* Check that the part of "injection" that is called by "inversion"
+ does the same number of intros as the number of equations
+ introduced, even in presence of dependent equalities that
+ "injection" renounces to split *)
+
+Fixpoint prodn (n : nat) :=
+ match n with
+ | O => unit
+ | (S m) => prod (prodn m) nat
+ end.
+
+Inductive U : forall n : nat, prodn n -> bool -> Prop :=
+| U_intro : U 0 tt true.
+
+Lemma foo3 : forall n (t : prodn n), U n t true -> False.
+Proof.
+(* used to fail because dEqThen thought there were 2 new equations but
+ inject_at_positions actually introduced only one; leading then to
+ an inconsistent state that disturbed "inversion" *)
+intros. inversion H.
+Abort.
diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v
index d53e4010..fada3bd5 100644
--- a/test-suite/success/LegacyField.v
+++ b/test-suite/success/LegacyField.v
@@ -30,14 +30,14 @@ Proof.
intros.
legacy field.
Abort.
-
+
(* Example 3 *)
Goal forall a b : R, (1 / (a * b) * (1 / 1 / b))%R = (1 / a)%R.
Proof.
intros.
legacy field.
Abort.
-
+
(* Example 4 *)
Goal
forall a b : R, a <> 0%R -> b <> 0%R -> (1 / (a * b) / 1 / b)%R = (1 / a)%R.
@@ -45,21 +45,21 @@ Proof.
intros.
legacy field.
Abort.
-
+
(* Example 5 *)
Goal forall a : R, 1%R = (1 * (1 / a) * a)%R.
Proof.
intros.
legacy field.
Abort.
-
+
(* Example 6 *)
Goal forall a b : R, b = (b * / a * a)%R.
Proof.
intros.
legacy field.
Abort.
-
+
(* Example 7 *)
Goal forall a b : R, b = (b * (1 / a) * a)%R.
Proof.
diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v
index 545b8aeb..4c790680 100644
--- a/test-suite/success/LetPat.v
+++ b/test-suite/success/LetPat.v
@@ -13,16 +13,16 @@ Definition l4 A (t : someT A) : nat := let 'mkT x y := t in x.
Print l4.
Print sigT.
-Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
+Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
let 'existT x y := t return B (projT1 t) in y.
-Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
+Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
let 'existT x y as t' := t return B (projT1 t') in y.
-Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
+Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
let 'existT x y as t' in sigT _ := t return B (projT1 t') in y.
-Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
+Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) :=
match t with
existT x y => y
end.
@@ -47,9 +47,9 @@ Definition identity_functor (c : category) : functor c c :=
let 'A :& homA :& CA := c in
fun x => x.
-Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c :=
+Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c :=
let 'A :& homA :& CA := a in
let 'B :& homB :& CB := b in
let 'C :& homB :& CB := c in
- fun f g =>
+ fun f g =>
fun x => g (f x).
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 4bdd579a..661a8757 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -14,7 +14,7 @@ Parameter P : Type -> Type -> Type -> Type.
Notation "e |= t --> v" := (P e t v) (at level 100, t at level 54).
Check (nat |= nat --> nat).
-(* Check that first non empty definition at an empty level can be of any
+(* Check that first non empty definition at an empty level can be of any
associativity *)
Definition marker := O.
@@ -30,4 +30,32 @@ Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2).
(* Check import of notations from within a section *)
Notation "+1 x" := (S x) (at level 25, x at level 9).
-Section A. Global Notation "'Z'" := O (at level 9). End A.
+Section A. Require Import make_notation. End A.
+
+(* Check use of "$" (see bug #1961) *)
+
+Notation "$ x" := (id x) (at level 30).
+Check ($ 5).
+
+(* Check regression of bug #2087 *)
+
+Notation "'exists' x , P" := (x, P)
+ (at level 200, x ident, right associativity, only parsing).
+
+Definition foo P := let '(exists x, Q) := P in x = Q :> nat.
+
+(* Check empty levels when extending binder_constr *)
+
+Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat
+ (at level 200, x ident, right associativity, y at level 69).
+
+(* This used to loop at some time before r12491 *)
+
+Notation R x := (@pair _ _ x).
+Check (fun x:nat*nat => match x with R x y => (x,y) end).
+
+(* Check multi-tokens recursive notations *)
+
+Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..).
+Check [ 0 ].
+Check [ 0 # ; 1 ].
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
new file mode 100644
index 00000000..fde9f470
--- /dev/null
+++ b/test-suite/success/Nsatz.v
@@ -0,0 +1,216 @@
+Require Import NsatzR ZArith Reals List Ring_polynom.
+
+Section Examples.
+
+Delimit Scope PE_scope with PE.
+Infix "+" := PEadd : PE_scope.
+Infix "*" := PEmul : PE_scope.
+Infix "-" := PEsub : PE_scope.
+Infix "^" := PEpow : PE_scope.
+Notation "[ n ]" := (@PEc Z n) (at level 0).
+
+Open Scope R_scope.
+
+Lemma example1 : forall x y,
+ x+y=0 ->
+ x*y=0 ->
+ x^2=0.
+Proof.
+ nsatzR.
+Qed.
+
+Lemma example2 : forall x, x^2=0 -> x=0.
+Proof.
+ nsatzR.
+Qed.
+
+(*
+Notation X := (PEX Z 3).
+Notation Y := (PEX Z 2).
+Notation Z_ := (PEX Z 1).
+*)
+Lemma example3 : forall x y z,
+ x+y+z=0 ->
+ x*y+x*z+y*z=0->
+ x*y*z=0 -> x^3=0.
+Proof.
+Time nsatzR.
+Qed.
+
+(*
+Notation X := (PEX Z 4).
+Notation Y := (PEX Z 3).
+Notation Z_ := (PEX Z 2).
+Notation U := (PEX Z 1).
+*)
+Lemma example4 : forall x y z u,
+ x+y+z+u=0 ->
+ x*y+x*z+x*u+y*z+y*u+z*u=0->
+ x*y*z+x*y*u+x*z*u+y*z*u=0->
+ x*y*z*u=0 -> x^4=0.
+Proof.
+Time nsatzR.
+Qed.
+
+(*
+Notation x_ := (PEX Z 5).
+Notation y_ := (PEX Z 4).
+Notation z_ := (PEX Z 3).
+Notation u_ := (PEX Z 2).
+Notation v_ := (PEX Z 1).
+Notation "x :: y" := (List.cons x y)
+(at level 60, right associativity, format "'[hv' x :: '/' y ']'").
+Notation "x :: y" := (List.app x y)
+(at level 60, right associativity, format "x :: y").
+*)
+
+Lemma example5 : forall x y z u v,
+ x+y+z+u+v=0 ->
+ x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
+ x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0->
+ x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 ->
+ x*y*z*u*v=0 -> x^5=0.
+Proof.
+Time nsatzR.
+Qed.
+
+End Examples.
+
+Section Geometry.
+Require Export Reals NsatzR.
+Open Scope R_scope.
+
+Record point:Type:={
+ X:R;
+ Y:R}.
+
+Definition collinear(A B C:point):=
+ (X A - X B)*(Y C - Y B)-(Y A - Y B)*(X C - X B)=0.
+
+Definition parallel (A B C D:point):=
+ ((X A)-(X B))*((Y C)-(Y D))=((Y A)-(Y B))*((X C)-(X D)).
+
+Definition notparallel (A B C D:point)(x:R):=
+ x*(((X A)-(X B))*((Y C)-(Y D))-((Y A)-(Y B))*((X C)-(X D)))=1.
+
+Definition orthogonal (A B C D:point):=
+ ((X A)-(X B))*((X C)-(X D))+((Y A)-(Y B))*((Y C)-(Y D))=0.
+
+Definition equal2(A B:point):=
+ (X A)=(X B) /\ (Y A)=(Y B).
+
+Definition equal3(A B:point):=
+ ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0.
+
+Definition nequal2(A B:point):=
+ (X A)<>(X B) \/ (Y A)<>(Y B).
+
+Definition nequal3(A B:point):=
+ not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0).
+
+Definition middle(A B I:point):=
+ 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B).
+
+Definition distance2(A B:point):=
+ (X B - X A)^2 + (Y B - Y A)^2.
+
+(* AB = CD *)
+Definition samedistance2(A B C D:point):=
+ (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2.
+Definition determinant(A O B:point):=
+ (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O).
+Definition scalarproduct(A O B:point):=
+ (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O).
+Definition norm2(A O B:point):=
+ ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2).
+
+
+Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)).
+intuition.
+Qed.
+
+Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C).
+intuition.
+Qed.
+
+Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d).
+intros.
+assert ( (a-b = 0) \/ (c-d = 0)).
+apply Rmult_integral.
+trivial.
+destruct H0.
+left; nsatz.
+right; nsatz.
+Qed.
+
+Ltac geo_unfold :=
+ unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal;
+ unfold equal2; unfold equal3; unfold nequal2; unfold nequal3;
+ unfold middle; unfold samedistance2;
+ unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2.
+
+Ltac geo_end :=
+ repeat (
+ repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end);
+ repeat (apply a1 || apply a2 || apply a3);
+ repeat split).
+
+Ltac geo_rewrite_hyps:=
+ repeat (match goal with
+ | h:X _ = _ |- _ => rewrite h in *; clear h
+ | h:Y _ = _ |- _ => rewrite h in *; clear h
+ end).
+
+Ltac geo_begin:=
+ geo_unfold;
+ intros;
+ geo_rewrite_hyps;
+ geo_end.
+
+(* Examples *)
+
+Lemma Thales: forall O A B C D:point,
+ collinear O A C -> collinear O B D ->
+ parallel A B C D ->
+ (distance2 O B * distance2 O C = distance2 O D * distance2 O A
+ /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
+ \/ collinear O A B.
+repeat geo_begin.
+(*
+Time nsatz.
+*)
+Time nsatz without sugar.
+(*
+Time nsatz with lexico sugar.
+Time nsatz with lexico.
+*)
+(*
+Time nsatzRpv 1%N 1%Z (@nil R) (@nil R). (* revlex, sugar, no div *)
+(*Finished transaction in 1. secs (0.479927u,0.s)*)
+Time nsatzRpv 1%N 0%Z (@nil R) (@nil R). (* revlex, no sugar, no div *)
+(*Finished transaction in 0. secs (0.543917u,0.s)*)
+Time nsatzRpv 1%N 2%Z (@nil R) (@nil R). (* lex, no sugar, no div *)
+(*Finished transaction in 0. secs (0.586911u,0.s)*)
+Time nsatzRpv 1%N 3%Z (@nil R) (@nil R). (* lex, sugar, no div *)
+(*Finished transaction in 0. secs (0.481927u,0.s)*)
+Time nsatzRpv 1%N 5%Z (@nil R) (@nil R). (* revlex, sugar, div *)
+(*Finished transaction in 1. secs (0.601909u,0.s)*)
+*)
+Time nsatz.
+Qed.
+
+Lemma hauteurs:forall A B C A1 B1 C1 H:point,
+ collinear B C A1 -> orthogonal A A1 B C ->
+ collinear A C B1 -> orthogonal B B1 A C ->
+ collinear A B C1 -> orthogonal C C1 A B ->
+ collinear A A1 H -> collinear B B1 H ->
+
+ collinear C C1 H
+ \/ collinear A B C.
+
+geo_begin.
+Time nsatz.
+(*Finished transaction in 3. secs (2.43263u,0.010998s)*)
+Qed.
+
+End Geometry.
diff --git a/test-suite/success/Nsatz_domain.v b/test-suite/success/Nsatz_domain.v
new file mode 100644
index 00000000..8a30b47f
--- /dev/null
+++ b/test-suite/success/Nsatz_domain.v
@@ -0,0 +1,274 @@
+Require Import Nsatz_domain ZArith Reals List Ring_polynom.
+
+Variable A: Type.
+Variable Ad: Domain A.
+
+Add Ring Ar1: (@ring_ring A (@domain_ring _ Ad)).
+
+Instance Ari : Ring A := {
+ ring0 := @ring0 A (@domain_ring _ Ad);
+ ring1 := @ring1 A (@domain_ring _ Ad);
+ ring_plus := @ring_plus A (@domain_ring _ Ad);
+ ring_mult := @ring_mult A (@domain_ring _ Ad);
+ ring_sub := @ring_sub A (@domain_ring _ Ad);
+ ring_opp := @ring_opp A (@domain_ring _ Ad);
+ ring_ring := @ring_ring A (@domain_ring _ Ad)}.
+
+Instance Adi : Domain A := {
+ domain_ring := Ari;
+ domain_axiom_product := @domain_axiom_product A Ad;
+ domain_axiom_one_zero := @domain_axiom_one_zero A Ad}.
+
+Instance zero_ring2 : Zero A := {zero := ring0}.
+Instance one_ring2 : One A := {one := ring1}.
+Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}.
+Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}.
+Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}.
+Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}.
+
+Goal forall x y:A, x = y -> x+0 = y*1+0.
+nsatz_domain.
+Qed.
+
+Goal forall a b c:A, a = b -> b = c -> c = a.
+nsatz_domain.
+Qed.
+
+Goal forall a b c:A, a = b -> b = c -> a = c.
+nsatz_domain.
+Qed.
+
+Goal forall a b c x:A, a = b -> b = c -> a*a = c*c.
+nsatz_domain.
+Qed.
+
+Goal forall x y:Z, x = y -> (x+0)%Z = (y*1+0)%Z.
+nsatz_domainZ.
+Qed.
+
+Goal forall x y:R, x = y -> (x+0)%R = (y*1+0)%R.
+nsatz_domainR.
+Qed.
+
+Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
+nsatz_domainR.
+Qed.
+
+Section Examples.
+
+Delimit Scope PE_scope with PE.
+Infix "+" := PEadd : PE_scope.
+Infix "*" := PEmul : PE_scope.
+Infix "-" := PEsub : PE_scope.
+Infix "^" := PEpow : PE_scope.
+Notation "[ n ]" := (@PEc Z n) (at level 0).
+
+Open Scope R_scope.
+
+Lemma example1 : forall x y,
+ x+y=0 ->
+ x*y=0 ->
+ x^2=0.
+Proof.
+ nsatz_domainR.
+Qed.
+
+Lemma example2 : forall x, x^2=0 -> x=0.
+Proof.
+ nsatz_domainR.
+Qed.
+
+(*
+Notation X := (PEX Z 3).
+Notation Y := (PEX Z 2).
+Notation Z_ := (PEX Z 1).
+*)
+Lemma example3 : forall x y z,
+ x+y+z=0 ->
+ x*y+x*z+y*z=0->
+ x*y*z=0 -> x^3=0.
+Proof.
+Time nsatz_domainR.
+simpl.
+discrR.
+Qed.
+
+(*
+Notation X := (PEX Z 4).
+Notation Y := (PEX Z 3).
+Notation Z_ := (PEX Z 2).
+Notation U := (PEX Z 1).
+*)
+Lemma example4 : forall x y z u,
+ x+y+z+u=0 ->
+ x*y+x*z+x*u+y*z+y*u+z*u=0->
+ x*y*z+x*y*u+x*z*u+y*z*u=0->
+ x*y*z*u=0 -> x^4=0.
+Proof.
+Time nsatz_domainR.
+Qed.
+
+(*
+Notation x_ := (PEX Z 5).
+Notation y_ := (PEX Z 4).
+Notation z_ := (PEX Z 3).
+Notation u_ := (PEX Z 2).
+Notation v_ := (PEX Z 1).
+Notation "x :: y" := (List.cons x y)
+(at level 60, right associativity, format "'[hv' x :: '/' y ']'").
+Notation "x :: y" := (List.app x y)
+(at level 60, right associativity, format "x :: y").
+*)
+
+Lemma example5 : forall x y z u v,
+ x+y+z+u+v=0 ->
+ x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
+ x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0->
+ x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 ->
+ x*y*z*u*v=0 -> x^5=0.
+Proof.
+Time nsatz_domainR.
+Qed.
+
+End Examples.
+
+Section Geometry.
+
+Open Scope R_scope.
+
+Record point:Type:={
+ X:R;
+ Y:R}.
+
+Definition collinear(A B C:point):=
+ (X A - X B)*(Y C - Y B)-(Y A - Y B)*(X C - X B)=0.
+
+Definition parallel (A B C D:point):=
+ ((X A)-(X B))*((Y C)-(Y D))=((Y A)-(Y B))*((X C)-(X D)).
+
+Definition notparallel (A B C D:point)(x:R):=
+ x*(((X A)-(X B))*((Y C)-(Y D))-((Y A)-(Y B))*((X C)-(X D)))=1.
+
+Definition orthogonal (A B C D:point):=
+ ((X A)-(X B))*((X C)-(X D))+((Y A)-(Y B))*((Y C)-(Y D))=0.
+
+Definition equal2(A B:point):=
+ (X A)=(X B) /\ (Y A)=(Y B).
+
+Definition equal3(A B:point):=
+ ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0.
+
+Definition nequal2(A B:point):=
+ (X A)<>(X B) \/ (Y A)<>(Y B).
+
+Definition nequal3(A B:point):=
+ not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0).
+
+Definition middle(A B I:point):=
+ 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B).
+
+Definition distance2(A B:point):=
+ (X B - X A)^2 + (Y B - Y A)^2.
+
+(* AB = CD *)
+Definition samedistance2(A B C D:point):=
+ (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2.
+Definition determinant(A O B:point):=
+ (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O).
+Definition scalarproduct(A O B:point):=
+ (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O).
+Definition norm2(A O B:point):=
+ ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2).
+
+
+Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)).
+intuition.
+Qed.
+
+Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C).
+intuition.
+Qed.
+
+Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d).
+intros.
+assert ( (a-b = 0) \/ (c-d = 0)).
+apply Rmult_integral.
+trivial.
+destruct H0.
+left; nsatz_domainR.
+right; nsatz_domainR.
+Qed.
+
+Ltac geo_unfold :=
+ unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal;
+ unfold equal2; unfold equal3; unfold nequal2; unfold nequal3;
+ unfold middle; unfold samedistance2;
+ unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2.
+
+Ltac geo_end :=
+ repeat (
+ repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end);
+ repeat (apply a1 || apply a2 || apply a3);
+ repeat split).
+
+Ltac geo_rewrite_hyps:=
+ repeat (match goal with
+ | h:X _ = _ |- _ => rewrite h in *; clear h
+ | h:Y _ = _ |- _ => rewrite h in *; clear h
+ end).
+
+Ltac geo_begin:=
+ geo_unfold;
+ intros;
+ geo_rewrite_hyps;
+ geo_end.
+
+(* Examples *)
+
+Lemma Thales: forall O A B C D:point,
+ collinear O A C -> collinear O B D ->
+ parallel A B C D ->
+ (distance2 O B * distance2 O C = distance2 O D * distance2 O A
+ /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
+ \/ collinear O A B.
+repeat geo_begin.
+
+Time nsatz_domainR.
+simpl;discrR.
+Time nsatz_domainR.
+simpl;discrR.
+Qed.
+
+Require Import NsatzR.
+
+Lemma hauteurs:forall A B C A1 B1 C1 H:point,
+ collinear B C A1 -> orthogonal A A1 B C ->
+ collinear A C B1 -> orthogonal B B1 A C ->
+ collinear A B C1 -> orthogonal C C1 A B ->
+ collinear A A1 H -> collinear B B1 H ->
+
+ collinear C C1 H
+ \/ collinear A B C.
+
+geo_begin.
+(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*)
+(*Finished transaction in 3. secs (2.363641u,0.s)*)
+(*Time nsatz_domainR. trop long! *)
+(* en fait nsatz_domain ne tient pas encore compte de la liste des variables! ;-) *)
+Time
+ let lv := constr:(Y A1
+ :: X A1
+ :: Y B1
+ :: X B1
+ :: Y A0
+ :: Y B
+ :: X B
+ :: X A0
+ :: X H
+ :: Y C
+ :: Y C1 :: Y H :: X C1 :: X C ::nil) in
+ nsatz_domainpv 2%N 1%Z (@List.nil R) lv ltac:simplR Rdi.
+(* Finished transaction in 6. secs (5.579152u,0.001s) *)
+Qed.
+
+End Geometry.
diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v
index accaec41..b8f8660e 100644
--- a/test-suite/success/Omega0.v
+++ b/test-suite/success/Omega0.v
@@ -3,24 +3,24 @@ Open Scope Z_scope.
(* Pierre L: examples gathered while debugging romega. *)
-Lemma test_romega_0 :
- forall m m',
+Lemma test_romega_0 :
+ forall m m',
0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
Proof.
intros.
omega.
Qed.
-Lemma test_romega_0b :
- forall m m',
+Lemma test_romega_0b :
+ forall m m',
0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
Proof.
intros m m'.
omega.
Qed.
-Lemma test_romega_1 :
- forall (z z1 z2 : Z),
+Lemma test_romega_1 :
+ forall (z z1 z2 : Z),
z2 <= z1 ->
z1 <= z2 ->
z1 >= 0 ->
@@ -32,8 +32,8 @@ intros.
omega.
Qed.
-Lemma test_romega_1b :
- forall (z z1 z2 : Z),
+Lemma test_romega_1b :
+ forall (z z1 z2 : Z),
z2 <= z1 ->
z1 <= z2 ->
z1 >= 0 ->
@@ -45,42 +45,42 @@ intros z z1 z2.
omega.
Qed.
-Lemma test_romega_2 : forall a b c:Z,
+Lemma test_romega_2 : forall a b c:Z,
0<=a-b<=1 -> b-c<=2 -> a-c<=3.
Proof.
intros.
omega.
Qed.
-Lemma test_romega_2b : forall a b c:Z,
+Lemma test_romega_2b : forall a b c:Z,
0<=a-b<=1 -> b-c<=2 -> a-c<=3.
Proof.
intros a b c.
omega.
Qed.
-Lemma test_romega_3 : forall a b h hl hr ha hb,
- 0 <= ha - hl <= 1 ->
+Lemma test_romega_3 : forall a b h hl hr ha hb,
+ 0 <= ha - hl <= 1 ->
-2 <= hl - hr <= 2 ->
h =b+1 ->
(ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
(hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
(-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
- (-2 <= ha-hr <=2 -> hb = a + 1) ->
+ (-2 <= ha-hr <=2 -> hb = a + 1) ->
0 <= hb - h <= 1.
Proof.
intros.
omega.
Qed.
-Lemma test_romega_3b : forall a b h hl hr ha hb,
- 0 <= ha - hl <= 1 ->
+Lemma test_romega_3b : forall a b h hl hr ha hb,
+ 0 <= ha - hl <= 1 ->
-2 <= hl - hr <= 2 ->
h =b+1 ->
(ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
(hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
(-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
- (-2 <= ha-hr <=2 -> hb = a + 1) ->
+ (-2 <= ha-hr <=2 -> hb = a + 1) ->
0 <= hb - h <= 1.
Proof.
intros a b h hl hr ha hb.
@@ -88,18 +88,18 @@ omega.
Qed.
-Lemma test_romega_4 : forall hr ha,
+Lemma test_romega_4 : forall hr ha,
ha = 0 ->
- (ha = 0 -> hr =0) ->
+ (ha = 0 -> hr =0) ->
hr = 0.
Proof.
intros hr ha.
omega.
Qed.
-Lemma test_romega_5 : forall hr ha,
+Lemma test_romega_5 : forall hr ha,
ha = 0 ->
- (~ha = 0 \/ hr =0) ->
+ (~ha = 0 \/ hr =0) ->
hr = 0.
Proof.
intros hr ha.
@@ -118,14 +118,14 @@ intros z.
omega.
Qed.
-Lemma test_romega_7 : forall z,
+Lemma test_romega_7 : forall z,
0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
Proof.
intros.
omega.
Qed.
-Lemma test_romega_7b : forall z,
+Lemma test_romega_7b : forall z,
0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
Proof.
intros.
diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v
index 54b13702..c4d086a3 100644
--- a/test-suite/success/Omega2.v
+++ b/test-suite/success/Omega2.v
@@ -4,7 +4,7 @@ Require Import ZArith Omega.
Open Scope Z_scope.
-Lemma Test46 :
+Lemma Test46 :
forall v1 v2 v3 v4 v5 : Z,
((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) ->
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
index bb800b7a..f4996734 100644
--- a/test-suite/success/OmegaPre.v
+++ b/test-suite/success/OmegaPre.v
@@ -4,7 +4,7 @@ Open Scope Z_scope.
(** Test of the zify preprocessor for (R)Omega *)
(* More details in file PreOmega.v
-
+
(r)omega with Z : starts with zify_op
(r)omega with nat : starts with zify_nat
(r)omega with positive : starts with zify_positive
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
new file mode 100644
index 00000000..81bdbc29
--- /dev/null
+++ b/test-suite/success/ProgramWf.v
@@ -0,0 +1,99 @@
+Require Import Arith Program.
+Require Import ZArith Zwf.
+
+Set Implicit Arguments.
+(* Set Printing All. *)
+Print sigT_rect.
+Obligation Tactic := program_simplify ; auto with *.
+About MR.
+
+Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
+ match n with
+ | 0 => 0
+ | S n' => merge n' m
+ end.
+
+Print merge.
+
+
+Print Zlt.
+Print Zwf.
+
+Open Local Scope Z_scope.
+
+Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z :=
+ match n ?= m with
+ | Lt => Zwfrec n (Zpred m)
+ | _ => 0
+ end.
+
+Next Obligation.
+ red. Admitted.
+
+Close Scope Z_scope.
+
+Program Fixpoint merge_wf (n m : nat) {wf lt m} : nat :=
+ match n with
+ | 0 => 0
+ | S n' => merge n' m
+ end.
+
+Print merge_wf.
+
+Program Fixpoint merge_one (n : nat) {measure n} : nat :=
+ match n with
+ | 0 => 0
+ | S n' => merge_one n'
+ end.
+
+Print Hint well_founded.
+Print merge_one. Eval cbv delta [merge_one] beta zeta in merge_one.
+
+Import WfExtensionality.
+
+Lemma merge_unfold n m : merge n m =
+ match n with
+ | 0 => 0
+ | S n' => merge n' m
+ end.
+Proof. intros. unfold merge at 1. unfold merge_func.
+ unfold_sub merge (merge n m).
+ simpl. destruct n ; reflexivity.
+Qed.
+
+Print merge.
+
+Require Import Arith.
+Unset Implicit Arguments.
+
+Time Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat)
+ (H : forall (i : { i | i < n }), i < p -> P i = true)
+ {measure (n - p)} :
+ Exc (forall (p : { i | i < n}), P p = true) :=
+ match le_lt_dec n p with
+ | left _ => value _
+ | right cmp =>
+ if dec (P p) then
+ check_n n P (S p) _
+ else
+ error
+ end.
+
+Require Import Omega Setoid.
+
+Next Obligation.
+ intros ; simpl in *. apply H.
+ simpl in * ; omega.
+Qed.
+
+Next Obligation. simpl in *; intros.
+ revert H0 ; clear_subset_proofs. intros.
+ case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by omega. subst.
+ revert H0 ; clear_subset_proofs ; tauto.
+
+ apply H. simpl. omega.
+Qed.
+
+Program Fixpoint check_n' (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p)
+ {measure (p - n) p} : nat :=
+ _.
diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v
index 88da6013..d8faa88a 100644
--- a/test-suite/success/Projection.v
+++ b/test-suite/success/Projection.v
@@ -12,7 +12,7 @@ Check fun (s:S) (a b:s.(Dom)) => s.(Op) a b.
Set Implicit Arguments.
Unset Strict Implicit.
-Unset Strict Implicit.
+Unset Strict Implicit.
Structure S' (A : Set) : Type := {Dom' : Type; Op' : A -> Dom' -> Dom'}.
@@ -29,9 +29,9 @@ Check fun (s:S') (a b:s.(Dom')) => _.(Op') a b.
Check fun (s:S') (a b:s.(Dom')) => s.(Op') a b.
Set Implicit Arguments.
-Unset Strict Implicits.
+Unset Strict Implicits.
-Structure S' (A:Set) : Type :=
+Structure S' (A:Set) : Type :=
{Dom' : Type;
Op' : A -> Dom' -> Dom'}.
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
index 0c37c59a..801ece9e 100644
--- a/test-suite/success/ROmega.v
+++ b/test-suite/success/ROmega.v
@@ -22,7 +22,7 @@ Qed.
Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
Proof.
intros.
-romega.
+romega.
Qed.
(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
index 86cf49cb..1348bb62 100644
--- a/test-suite/success/ROmega0.v
+++ b/test-suite/success/ROmega0.v
@@ -3,24 +3,24 @@ Open Scope Z_scope.
(* Pierre L: examples gathered while debugging romega. *)
-Lemma test_romega_0 :
- forall m m',
+Lemma test_romega_0 :
+ forall m m',
0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
Proof.
intros.
romega.
Qed.
-Lemma test_romega_0b :
- forall m m',
+Lemma test_romega_0b :
+ forall m m',
0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
Proof.
intros m m'.
romega.
Qed.
-Lemma test_romega_1 :
- forall (z z1 z2 : Z),
+Lemma test_romega_1 :
+ forall (z z1 z2 : Z),
z2 <= z1 ->
z1 <= z2 ->
z1 >= 0 ->
@@ -32,8 +32,8 @@ intros.
romega.
Qed.
-Lemma test_romega_1b :
- forall (z z1 z2 : Z),
+Lemma test_romega_1b :
+ forall (z z1 z2 : Z),
z2 <= z1 ->
z1 <= z2 ->
z1 >= 0 ->
@@ -45,42 +45,42 @@ intros z z1 z2.
romega.
Qed.
-Lemma test_romega_2 : forall a b c:Z,
+Lemma test_romega_2 : forall a b c:Z,
0<=a-b<=1 -> b-c<=2 -> a-c<=3.
Proof.
intros.
romega.
Qed.
-Lemma test_romega_2b : forall a b c:Z,
+Lemma test_romega_2b : forall a b c:Z,
0<=a-b<=1 -> b-c<=2 -> a-c<=3.
Proof.
intros a b c.
romega.
Qed.
-Lemma test_romega_3 : forall a b h hl hr ha hb,
- 0 <= ha - hl <= 1 ->
+Lemma test_romega_3 : forall a b h hl hr ha hb,
+ 0 <= ha - hl <= 1 ->
-2 <= hl - hr <= 2 ->
h =b+1 ->
(ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
(hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
(-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
- (-2 <= ha-hr <=2 -> hb = a + 1) ->
+ (-2 <= ha-hr <=2 -> hb = a + 1) ->
0 <= hb - h <= 1.
Proof.
intros.
romega.
Qed.
-Lemma test_romega_3b : forall a b h hl hr ha hb,
- 0 <= ha - hl <= 1 ->
+Lemma test_romega_3b : forall a b h hl hr ha hb,
+ 0 <= ha - hl <= 1 ->
-2 <= hl - hr <= 2 ->
h =b+1 ->
(ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
(hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
(-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
- (-2 <= ha-hr <=2 -> hb = a + 1) ->
+ (-2 <= ha-hr <=2 -> hb = a + 1) ->
0 <= hb - h <= 1.
Proof.
intros a b h hl hr ha hb.
@@ -88,18 +88,18 @@ romega.
Qed.
-Lemma test_romega_4 : forall hr ha,
+Lemma test_romega_4 : forall hr ha,
ha = 0 ->
- (ha = 0 -> hr =0) ->
+ (ha = 0 -> hr =0) ->
hr = 0.
Proof.
intros hr ha.
romega.
Qed.
-Lemma test_romega_5 : forall hr ha,
+Lemma test_romega_5 : forall hr ha,
ha = 0 ->
- (~ha = 0 \/ hr =0) ->
+ (~ha = 0 \/ hr =0) ->
hr = 0.
Proof.
intros hr ha.
@@ -118,14 +118,14 @@ intros z.
romega.
Qed.
-Lemma test_romega_7 : forall z,
+Lemma test_romega_7 : forall z,
0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
Proof.
intros.
romega.
Qed.
-Lemma test_romega_7b : forall z,
+Lemma test_romega_7b : forall z,
0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
Proof.
intros.
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
index a3be2898..87e8c8e3 100644
--- a/test-suite/success/ROmega2.v
+++ b/test-suite/success/ROmega2.v
@@ -6,7 +6,7 @@ Open Scope Z_scope.
(* First a simplified version used during debug of romega on Test46 *)
-Lemma Test46_simplified :
+Lemma Test46_simplified :
forall v1 v2 v5 : Z,
0 = v2 + v5 ->
0 < v5 ->
@@ -18,7 +18,7 @@ Qed.
(* The complete problem *)
-Lemma Test46 :
+Lemma Test46 :
forall v1 v2 v3 v4 v5 : Z,
((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) ->
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
index 550edca5..bd473fa6 100644
--- a/test-suite/success/ROmegaPre.v
+++ b/test-suite/success/ROmegaPre.v
@@ -4,7 +4,7 @@ Open Scope Z_scope.
(** Test of the zify preprocessor for (R)Omega *)
(* More details in file PreOmega.v
-
+
(r)omega with Z : starts with zify_op
(r)omega with nat : starts with zify_nat
(r)omega with positive : starts with zify_positive
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 60e170e4..d4e6a82e 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -1,5 +1,5 @@
-Inductive nat : Set :=
- | O : nat
+Inductive nat : Set :=
+ | O : nat
| S : nat->nat.
Check nat.
Check O.
@@ -14,8 +14,8 @@ Print le.
Theorem zero_leq_three: 0 <= 3.
Proof.
- constructor 2.
- constructor 2.
+ constructor 2.
+ constructor 2.
constructor 2.
constructor 1.
@@ -32,7 +32,7 @@ Qed.
Lemma zero_lt_three : 0 < 3.
Proof.
unfold lt.
- repeat constructor.
+ repeat constructor.
Qed.
@@ -132,7 +132,7 @@ Require Import Compare_dec.
Check le_lt_dec.
-Definition max (n p :nat) := match le_lt_dec n p with
+Definition max (n p :nat) := match le_lt_dec n p with
| left _ => p
| right _ => n
end.
@@ -152,9 +152,9 @@ Extraction max.
Inductive tree(A:Set) : Set :=
- node : A -> forest A -> tree A
+ node : A -> forest A -> tree A
with
- forest (A: Set) : Set :=
+ forest (A: Set) : Set :=
nochild : forest A |
addchild : tree A -> forest A -> forest A.
@@ -162,7 +162,7 @@ with
-Inductive
+Inductive
even : nat->Prop :=
evenO : even O |
evenS : forall n, odd n -> even (S n)
@@ -176,11 +176,11 @@ Qed.
-Definition nat_case :=
+Definition nat_case :=
fun (Q : Type)(g0 : Q)(g1 : nat -> Q)(n:nat) =>
match n return Q with
- | 0 => g0
- | S p => g1 p
+ | 0 => g0
+ | S p => g1 p
end.
Eval simpl in (nat_case nat 0 (fun p => p) 34).
@@ -200,7 +200,7 @@ Eval simpl in fun p => pred (S p).
Definition xorb (b1 b2:bool) :=
-match b1, b2 with
+match b1, b2 with
| false, true => true
| true, false => true
| _ , _ => false
@@ -208,7 +208,7 @@ end.
Definition pred_spec (n:nat) := {m:nat | n=0 /\ m=0 \/ n = S m}.
-
+
Definition predecessor : forall n:nat, pred_spec n.
intro n;case n.
@@ -220,7 +220,7 @@ Print predecessor.
Extraction predecessor.
-Theorem nat_expand :
+Theorem nat_expand :
forall n:nat, n = match n with 0 => 0 | S p => S p end.
intro n;case n;simpl;auto.
Qed.
@@ -228,7 +228,7 @@ Qed.
Check (fun p:False => match p return 2=3 with end).
Theorem fromFalse : False -> 0=1.
- intro absurd.
+ intro absurd.
contradiction.
Qed.
@@ -244,12 +244,12 @@ Section equality_elimination.
End equality_elimination.
-
+
Theorem trans : forall n m p:nat, n=m -> m=p -> n=p.
Proof.
- intros n m p eqnm.
+ intros n m p eqnm.
case eqnm.
- trivial.
+ trivial.
Qed.
Lemma Rw : forall x y: nat, y = y * x -> y * x * x = y.
@@ -282,7 +282,7 @@ Lemma four_n : forall n:nat, n+n+n+n = 4*n.
Undo.
intro n; pattern n at 1.
-
+
rewrite <- mult_1_l.
repeat rewrite mult_distr_S.
@@ -314,7 +314,7 @@ Proof.
intros m Hm; exists m;trivial.
Qed.
-Definition Vtail_total
+Definition Vtail_total
(A : Set) (n : nat) (v : vector A n) : vector A (pred n):=
match v in (vector _ n0) return (vector A (pred n0)) with
| Vnil => Vnil A
@@ -322,7 +322,7 @@ match v in (vector _ n0) return (vector A (pred n0)) with
end.
Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
- intros A n v; case v.
+ case v.
simpl.
exact (Vnil A).
simpl.
@@ -331,7 +331,7 @@ Defined.
(*
Inductive Lambda : Set :=
- lambda : (Lambda -> False) -> Lambda.
+ lambda : (Lambda -> False) -> Lambda.
Error: Non strictly positive occurrence of "Lambda" in
@@ -347,7 +347,7 @@ Section Paradox.
(*
understand matchL Q l (fun h : Lambda -> False => t)
- as match l return Q with lambda h => t end
+ as match l return Q with lambda h => t end
*)
Definition application (f x: Lambda) :False :=
@@ -377,26 +377,26 @@ Definition isingle l := inode l (fun i => ileaf).
Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
-Definition t2 := inode 0
- (fun n : nat =>
+Definition t2 := inode 0
+ (fun n : nat =>
inode (Z_of_nat n)
(fun p => isingle (Z_of_nat (n*p)))).
Inductive itree_le : itree-> itree -> Prop :=
| le_leaf : forall t, itree_le ileaf t
- | le_node : forall l l' s s',
- Zle l l' ->
- (forall i, exists j:nat, itree_le (s i) (s' j)) ->
+ | le_node : forall l l' s s',
+ Zle l l' ->
+ (forall i, exists j:nat, itree_le (s i) (s' j)) ->
itree_le (inode l s) (inode l' s').
-Theorem itree_le_trans :
+Theorem itree_le_trans :
forall t t', itree_le t t' ->
forall t'', itree_le t' t'' -> itree_le t t''.
induction t.
constructor 1.
-
+
intros t'; case t'.
inversion 1.
intros z0 i0 H0.
@@ -409,20 +409,20 @@ Theorem itree_le_trans :
inversion_clear H0.
intro i2; case (H4 i2).
intros.
- generalize (H i2 _ H0).
+ generalize (H i2 _ H0).
intros.
case (H3 x);intros.
generalize (H5 _ H6).
exists x0;auto.
Qed.
-
+
Inductive itree_le' : itree-> itree -> Prop :=
| le_leaf' : forall t, itree_le' ileaf t
- | le_node' : forall l l' s s' g,
- Zle l l' ->
- (forall i, itree_le' (s i) (s' (g i))) ->
+ | le_node' : forall l l' s s' g,
+ Zle l l' ->
+ (forall i, itree_le' (s i) (s' (g i))) ->
itree_le' (inode l s) (inode l' s').
@@ -434,7 +434,7 @@ Lemma t1_le_t2 : itree_le t1 t2.
constructor.
auto with zarith.
intro i; exists (2 * i).
- unfold isingle.
+ unfold isingle.
constructor.
auto with zarith.
exists i;constructor.
@@ -455,7 +455,7 @@ Qed.
Require Import List.
-Inductive ltree (A:Set) : Set :=
+Inductive ltree (A:Set) : Set :=
lnode : A -> list (ltree A) -> ltree A.
Inductive prop : Prop :=
@@ -482,8 +482,8 @@ Qed.
Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
match p with exP_intro X HX => X end).
Error:
-Incorrect elimination of "p" in the inductive type
-"ex_Prop", the return type has sort "Type" while it should be
+Incorrect elimination of "p" in the inductive type
+"ex_Prop", the return type has sort "Type" while it should be
"Prop"
Elimination of an inductive object of sort "Prop"
@@ -496,8 +496,8 @@ because proofs can be eliminated only to build proofs
Check (match prop_inject with (prop_intro P p) => P end).
Error:
-Incorrect elimination of "prop_inject" in the inductive type
-"prop", the return type has sort "Type" while it should be
+Incorrect elimination of "prop_inject" in the inductive type
+"prop", the return type has sort "Type" while it should be
"Prop"
Elimination of an inductive object of sort "Prop"
@@ -508,17 +508,17 @@ because proofs can be eliminated only to build proofs
Print prop_inject.
(*
-prop_inject =
+prop_inject =
prop_inject = prop_intro prop (fun H : prop => H)
: prop
*)
-Inductive typ : Type :=
- typ_intro : Type -> typ.
+Inductive typ : Type :=
+ typ_intro : Type -> typ.
Definition typ_inject: typ.
-split.
+split.
exact typ.
(*
Defined.
@@ -564,13 +564,13 @@ Reset comes_from_the_left.
Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
match H with
- | or_introl p => True
+ | or_introl p => True
| or_intror q => False
end.
Error:
-Incorrect elimination of "H" in the inductive type
-"or", the return type has sort "Type" while it should be
+Incorrect elimination of "H" in the inductive type
+"or", the return type has sort "Type" while it should be
"Prop"
Elimination of an inductive object of sort "Prop"
@@ -582,41 +582,41 @@ because proofs can be eliminated only to build proofs
Definition comes_from_the_left_sumbool
(P Q:Prop)(x:{P}+{Q}): Prop :=
match x with
- | left p => True
+ | left p => True
| right q => False
end.
-
+
Close Scope Z_scope.
-Theorem S_is_not_O : forall n, S n <> 0.
+Theorem S_is_not_O : forall n, S n <> 0.
-Definition Is_zero (x:nat):= match x with
- | 0 => True
+Definition Is_zero (x:nat):= match x with
+ | 0 => True
| _ => False
end.
Lemma O_is_zero : forall m, m = 0 -> Is_zero m.
Proof.
intros m H; subst m.
- (*
+ (*
============================
Is_zero 0
*)
simpl;trivial.
Qed.
-
+
red; intros n Hn.
apply O_is_zero with (m := S n).
assumption.
Qed.
-Theorem disc2 : forall n, S (S n) <> 1.
+Theorem disc2 : forall n, S (S n) <> 1.
Proof.
intros n Hn; discriminate.
Qed.
@@ -632,7 +632,7 @@ Qed.
Theorem inj_succ : forall n m, S n = S m -> n = m.
Proof.
-
+
Lemma inj_pred : forall n m, n = m -> pred n = pred m.
Proof.
@@ -666,9 +666,9 @@ Proof.
intros n p H; case H ;
intros; discriminate.
Qed.
-
+
eapply not_le_Sn_0_with_constraints; eauto.
-Qed.
+Qed.
Theorem not_le_Sn_0' : forall n:nat, ~ (S n <= 0).
@@ -681,7 +681,7 @@ Check le_Sn_0_inv.
Theorem le_Sn_0'' : forall n p : nat, ~ S n <= 0 .
Proof.
- intros n p H;
+ intros n p H;
inversion H using le_Sn_0_inv.
Qed.
@@ -689,9 +689,9 @@ Derive Inversion_clear le_Sn_0_inv' with (forall n :nat, S n <= 0).
Check le_Sn_0_inv'.
-Theorem le_reverse_rules :
- forall n m:nat, n <= m ->
- n = m \/
+Theorem le_reverse_rules :
+ forall n m:nat, n <= m ->
+ n = m \/
exists p, n <= p /\ m = S p.
Proof.
intros n m H; inversion H.
@@ -704,21 +704,21 @@ Restart.
Qed.
Inductive ArithExp : Set :=
- Zero : ArithExp
+ Zero : ArithExp
| Succ : ArithExp -> ArithExp
| Plus : ArithExp -> ArithExp -> ArithExp.
Inductive RewriteRel : ArithExp -> ArithExp -> Prop :=
RewSucc : forall e1 e2 :ArithExp,
- RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2)
+ RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2)
| RewPlus0 : forall e:ArithExp,
- RewriteRel (Plus Zero e) e
+ RewriteRel (Plus Zero e) e
| RewPlusS : forall e1 e2:ArithExp,
RewriteRel e1 e2 ->
RewriteRel (Plus (Succ e1) e2) (Succ (Plus e1 e2)).
-
+
Fixpoint plus (n p:nat) {struct n} : nat :=
match n with
| 0 => p
@@ -739,7 +739,7 @@ Fixpoint plus'' (n p:nat) {struct n} : nat :=
Fixpoint even_test (n:nat) : bool :=
- match n
+ match n
with 0 => true
| 1 => false
| S (S p) => even_test p
@@ -749,20 +749,20 @@ Fixpoint even_test (n:nat) : bool :=
Reset even_test.
Fixpoint even_test (n:nat) : bool :=
- match n
- with
+ match n
+ with
| 0 => true
| S p => odd_test p
end
with odd_test (n:nat) : bool :=
match n
- with
+ with
| 0 => false
| S p => even_test p
end.
-
+
Eval simpl in even_test.
@@ -779,11 +779,11 @@ Section Principle_of_Induction.
Variable P : nat -> Prop.
Hypothesis base_case : P 0.
Hypothesis inductive_step : forall n:nat, P n -> P (S n).
-Fixpoint nat_ind (n:nat) : (P n) :=
+Fixpoint nat_ind (n:nat) : (P n) :=
match n return P n with
| 0 => base_case
| S m => inductive_step m (nat_ind m)
- end.
+ end.
End Principle_of_Induction.
@@ -803,9 +803,9 @@ Variable P : nat -> nat ->Prop.
Hypothesis base_case1 : forall x:nat, P 0 x.
Hypothesis base_case2 : forall x:nat, P (S x) 0.
Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
-Fixpoint nat_double_ind (n m:nat){struct n} : P n m :=
- match n, m return P n m with
- | 0 , x => base_case1 x
+Fixpoint nat_double_ind (n m:nat){struct n} : P n m :=
+ match n, m return P n m with
+ | 0 , x => base_case1 x
| (S x), 0 => base_case2 x
| (S x), (S y) => inductive_step x y (nat_double_ind x y)
end.
@@ -816,15 +816,15 @@ Variable P : nat -> nat -> Set.
Hypothesis base_case1 : forall x:nat, P 0 x.
Hypothesis base_case2 : forall x:nat, P (S x) 0.
Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
-Fixpoint nat_double_rec (n m:nat){struct n} : P n m :=
- match n, m return P n m with
- | 0 , x => base_case1 x
+Fixpoint nat_double_rec (n m:nat){struct n} : P n m :=
+ match n, m return P n m with
+ | 0 , x => base_case1 x
| (S x), 0 => base_case2 x
| (S x), (S y) => inductive_step x y (nat_double_rec x y)
end.
End Principle_of_Double_Recursion.
-Definition min : nat -> nat -> nat :=
+Definition min : nat -> nat -> nat :=
nat_double_rec (fun (x y:nat) => nat)
(fun (x:nat) => 0)
(fun (y:nat) => 0)
@@ -868,7 +868,7 @@ Require Import Minus.
(*
Fixpoint div (x y:nat){struct x}: nat :=
- if eq_nat_dec x 0
+ if eq_nat_dec x 0
then 0
else if eq_nat_dec y 0
then x
@@ -901,18 +901,18 @@ Qed.
Lemma minus_smaller_positive : forall x y:nat, x <>0 -> y <> 0 ->
x - y < x.
Proof.
- destruct x; destruct y;
- ( simpl;intros; apply minus_smaller_S ||
+ destruct x; destruct y;
+ ( simpl;intros; apply minus_smaller_S ||
intros; absurd (0=0); auto).
Qed.
-Definition minus_decrease : forall x y:nat, Acc lt x ->
- x <> 0 ->
+Definition minus_decrease : forall x y:nat, Acc lt x ->
+ x <> 0 ->
y <> 0 ->
Acc lt (x-y).
Proof.
intros x y H; case H.
- intros Hz posz posy.
+ intros Hz posz posy.
apply Hz; apply minus_smaller_positive; assumption.
Defined.
@@ -920,21 +920,19 @@ Print minus_decrease.
-Definition div_aux (x y:nat)(H: Acc lt x):nat.
- fix 3.
- intros.
- refine (if eq_nat_dec x 0
- then 0
- else if eq_nat_dec y 0
+Fixpoint div_aux (x y:nat)(H: Acc lt x):nat.
+ refine (if eq_nat_dec x 0
+ then 0
+ else if eq_nat_dec y 0
then y
else div_aux (x-y) y _).
- apply (minus_decrease x y H);assumption.
+ apply (minus_decrease x y H);assumption.
Defined.
Print div_aux.
(*
-div_aux =
+div_aux =
(fix div_aux (x y : nat) (H : Acc lt x) {struct H} : nat :=
match eq_nat_dec x 0 with
| left _ => 0
@@ -948,7 +946,7 @@ div_aux =
*)
Require Import Wf_nat.
-Definition div x y := div_aux x y (lt_wf x).
+Definition div x y := div_aux x y (lt_wf x).
Extraction div.
(*
@@ -974,7 +972,7 @@ Proof.
Abort.
(*
- Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
+ Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
n= 0 -> v = Vnil A.
Toplevel input, characters 40281-40287
@@ -990,7 +988,7 @@ The term "Vnil A" has type "vector A 0" while it is expected to have type
*)
Require Import JMeq.
-Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
+Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
n= 0 -> JMeq v (Vnil A).
Proof.
destruct v.
@@ -1026,7 +1024,7 @@ Eval simpl in (fun (A:Set)(v:vector A 0) => v).
Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
Proof.
- destruct v.
+ destruct v.
reflexivity.
reflexivity.
Defined.
@@ -1034,7 +1032,7 @@ Defined.
Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
Proof.
intros.
- change (Vnil (A:=A)) with (Vid _ 0 v).
+ change (Vnil (A:=A)) with (Vid _ 0 v).
apply Vid_eq.
Defined.
@@ -1050,7 +1048,7 @@ Defined.
-Definition vector_double_rect :
+Definition vector_double_rect :
forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
P 0 Vnil Vnil ->
(forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
@@ -1105,7 +1103,7 @@ Qed.
| LCons : A -> LList A -> LList A.
-
+
Definition head (A:Set)(s : Stream A) := match s with Cons a s' => a end.
@@ -1144,7 +1142,7 @@ Hypothesis bisim2 : forall s1 s2:Stream A, R s1 s2 ->
CoFixpoint park_ppl : forall s1 s2:Stream A, R s1 s2 ->
EqSt s1 s2 :=
fun s1 s2 (p : R s1 s2) =>
- eqst s1 s2 (bisim1 p)
+ eqst s1 s2 (bisim1 p)
(park_ppl (bisim2 p)).
End Parks_Principle.
@@ -1154,7 +1152,7 @@ Theorem map_iterate : forall (A:Set)(f:A->A)(x:A),
Proof.
intros A f x.
apply park_ppl with
- (R:= fun s1 s2 => exists x: A,
+ (R:= fun s1 s2 => exists x: A,
s1 = iterate f (f x) /\ s2 = map f (iterate f x)).
intros s1 s2 (x0,(eqs1,eqs2));rewrite eqs1;rewrite eqs2;reflexivity.
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 885fff48..8334322c 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -17,34 +17,34 @@ Obligation Tactic := crush.
Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}.
-Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) :=
+Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) :=
{| vec_list := cons a (vec_list v) |}.
Hint Rewrite map_length rev_length : datatypes.
-Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n :=
+Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n :=
{| vec_list := map f v |}.
-Program Definition vreverse {A n} (v : vector A n) : vector A n :=
+Program Definition vreverse {A n} (v : vector A n) : vector A n :=
{| vec_list := rev v |}.
-Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B :=
+Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B :=
match v, w with
| nil, nil => nil
| cons f fs, cons x xs => cons (f x) (va_list fs xs)
| _, _ => nil
end.
-Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n :=
+Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n :=
{| vec_list := va_list v w |}.
-Next Obligation.
+Next Obligation.
destruct v as [v Hv]; destruct w as [w Hw] ; simpl.
- subst n. revert w Hw. induction v ; destruct w ; crush.
+ subst n. revert w Hw. induction v ; destruct w ; crush.
rewrite IHv ; auto.
Qed.
-(* Correct type inference of record notation. Initial example by Spiwack. *)
+(* Correct type inference of record notation. Initial example by Spiwack. *)
Inductive Machin := {
Bazar : option Machin
@@ -80,3 +80,10 @@ Record DecidableOrder : Type :=
; le_trans : transitive _ le
; le_total : forall x y, {x <= y}+{y <= x}
}.
+
+(* Test syntactic sugar suggested by wish report #2138 *)
+
+Record R : Type := {
+ P (A : Type) : Prop := exists x : A -> A, x = x;
+ Q A : P A -> P A
+}.
diff --git a/test-suite/success/Section.v b/test-suite/success/Section.v
new file mode 100644
index 00000000..8e9e79b3
--- /dev/null
+++ b/test-suite/success/Section.v
@@ -0,0 +1,6 @@
+(* Test bug 2168: ending section of some name was removing objects of the
+ same name *)
+
+Require Import make_notation.
+
+Check add2 3.
diff --git a/test-suite/success/Simplify_eq.v b/test-suite/success/Simplify_eq.v
index 5b856e3d..d9abdbf5 100644
--- a/test-suite/success/Simplify_eq.v
+++ b/test-suite/success/Simplify_eq.v
@@ -2,11 +2,11 @@
(* Check that Simplify_eq tries Intro until *)
-Lemma l1 : 0 = 1 -> False.
+Lemma l1 : 0 = 1 -> False.
simplify_eq 1.
Qed.
-Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False.
+Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False.
simplify_eq H.
intros.
apply (n_Sn x H0).
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index f0809839..42898b8d 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Tauto.v 7693 2005-12-21 23:50:17Z herbelin $ *)
+(* $Id$ *)
(**** Tactics Tauto and Intuition ****)
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 82c5cf2e..5f44c752 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -9,13 +9,11 @@
(************************************************************************)
Lemma essai : forall x : nat, x = x.
-
refine
((fun x0 : nat => match x0 with
| O => _
| S p => _
- end)
- :forall x : nat, x = x). (* x0=x0 et x0=x0 *)
+ end)).
Restart.
@@ -44,7 +42,7 @@ Abort.
(************************************************************************)
-Lemma T : nat.
+Lemma T : nat.
refine (S _).
@@ -97,7 +95,7 @@ Abort.
(************************************************************************)
-Parameter f : nat * nat -> nat -> nat.
+Parameter f : nat * nat -> nat -> nat.
Lemma essai : nat.
@@ -145,11 +143,10 @@ Lemma essai : forall n : nat, {x : nat | x = S n}.
Restart.
refine
- ((fun n : nat => match n with
+ (fun n : nat => match n with
| O => _
| S p => _
- end)
- :forall n : nat, {x : nat | x = S n}).
+ end).
Restart.
@@ -178,10 +175,10 @@ Restart.
| S p => _
end).
-exists 1. trivial.
+exists 1. trivial.
elim (f0 p).
refine
- (fun (x : nat) (h : x = S p) => exist (fun x : nat => x = S (S p)) (S x) _).
+ (fun (x : nat) (h : x = S p) => exist (fun x : nat => x = S (S p)) (S x) _).
rewrite h. auto.
Qed.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
new file mode 100644
index 00000000..55351a47
--- /dev/null
+++ b/test-suite/success/Typeclasses.v
@@ -0,0 +1,60 @@
+Generalizable All Variables.
+
+Module mon.
+
+Reserved Notation "'return' t" (at level 0).
+Reserved Notation "x >>= y" (at level 65, left associativity).
+
+
+
+Record Monad {m : Type -> Type} := {
+ unit : Π {α}, α -> m α where "'return' t" := (unit t) ;
+ bind : Π {α β}, m α -> (α -> m β) -> m β where "x >>= y" := (bind x y) ;
+ bind_unit_left : Π {α β} (a : α) (f : α -> m β), return a >>= f = f a }.
+
+Print Visibility.
+Print unit.
+Implicit Arguments unit [[m] [m0] [α]].
+Implicit Arguments Monad [].
+Notation "'return' t" := (unit t).
+
+(* Test correct handling of existentials and defined fields. *)
+
+Class A `(e: T) := { a := True }.
+Class B `(e_: T) := { e := e_; sg_ass :> A e }.
+
+Goal forall `{B T}, a.
+ intros. exact I.
+Defined.
+
+Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }.
+
+Goal forall `{B' T}, a.
+ intros. exact I.
+Defined.
+
+End mon.
+
+(* Correct treatment of dependent goals *)
+
+(* First some preliminaries: *)
+
+Section sec.
+ Context {N: Type}.
+ Class C (f: N->N) := {}.
+ Class E := { e: N -> N }.
+ Context
+ (g: N -> N) `(E) `(C e)
+ `(forall (f: N -> N), C f -> C (fun x => f x))
+ (U: forall f: N -> N, C f -> False).
+
+(* Now consider the following: *)
+
+ Let foo := U (fun x => e x).
+ Check foo _.
+
+(* This type checks fine, so far so good. But now
+ let's try to get rid of the intermediate constant foo.
+ Surely we can just expand it inline, right? Wrong!: *)
+ Check U (fun x => e x) _.
+End sec. \ No newline at end of file
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 952890ee..a6f9fa23 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -135,7 +135,7 @@ Qed.
Definition apply (f:nat->Prop) := forall x, f x.
Goal apply (fun n => n=0) -> 1=0.
intro H.
-auto.
+auto.
Qed.
(* The following fails if the coercion Zpos is not introduced around p
@@ -157,10 +157,10 @@ Qed.
Definition succ x := S x.
Goal forall (I : nat -> Set) (P : nat -> Prop) (Q : forall n:nat, I n -> Prop),
- (forall x y, P x -> Q x y) ->
+ (forall x y, P x -> Q x y) ->
(forall x, P (S x)) -> forall y: I (S 0), Q (succ 0) y.
intros.
-apply H with (y:=y).
+apply H with (y:=y).
(* [x] had two possible instances: [S 0], coming from unifying the
type of [y] with [I ?n] and [succ 0] coming from the unification with
the goal; only the first one allows to make the next apply (which
@@ -171,14 +171,14 @@ Qed.
(* A similar example with a arbitrary long conversion between the two
possible instances *)
-Fixpoint compute_succ x :=
+Fixpoint compute_succ x :=
match x with O => S 0 | S n => S (compute_succ n) end.
Goal forall (I : nat -> Set) (P : nat -> Prop) (Q : forall n:nat, I n -> Prop),
- (forall x y, P x -> Q x y) ->
+ (forall x y, P x -> Q x y) ->
(forall x, P (S x)) -> forall y: I (S 100), Q (compute_succ 100) y.
intros.
-apply H with (y:=y).
+apply H with (y:=y).
apply H0.
Qed.
@@ -187,10 +187,10 @@ Qed.
subgoal which precisely fails) *)
Definition ID (A:Type) := A.
-Goal forall f:Type -> Type,
- forall (P : forall A:Type, A -> Prop),
- (forall (B:Type) x, P (f B) x -> P (f B) x) ->
- (forall (A:Type) x, P (f (f A)) x) ->
+Goal forall f:Type -> Type,
+ forall (P : forall A:Type, A -> Prop),
+ (forall (B:Type) x, P (f B) x -> P (f B) x) ->
+ (forall (A:Type) x, P (f (f A)) x) ->
forall (A:Type) (x:f (f A)), P (f (ID (f A))) x.
intros.
apply H.
@@ -239,6 +239,28 @@ Axiom silly_axiom : forall v : exp, v = v -> False.
Lemma silly_lemma : forall x : atom, False.
intros x.
apply silly_axiom with (v := x). (* fails *)
+reflexivity.
+Qed.
+
+(* Check that unification does not commit too early to a representative
+ of an eta-equivalence class that would be incompatible with other
+ unification constraints *)
+
+Lemma eta : forall f : (forall P, P 1),
+ (forall P, f P = f P) ->
+ forall Q, f (fun x => Q x) = f (fun x => Q x).
+intros.
+apply H.
+Qed.
+
+(* Test propagation of evars from subgoal to brother subgoals *)
+
+ (* This works because unfold calls clos_norm_flags which calls nf_evar *)
+
+Lemma eapply_evar_unfold : let x:=O in O=x -> 0=O.
+intros x H; eapply trans_equal;
+[apply H | unfold x;match goal with |- ?x = ?x => reflexivity end].
+Qed.
(* Test non-regression of (temporary) bug 1981 *)
@@ -248,9 +270,124 @@ exact O.
trivial.
Qed.
-(* Test non-regression of (temporary) bug 1980 *)
+(* Check pattern-unification on evars in apply unification *)
+
+Lemma evar : exists f : nat -> nat, forall x, f x = 0 -> x = 0.
+Proof.
+eexists; intros x H.
+apply H.
+Qed.
+
+(* Check that "as" clause applies to main premise only and leave the
+ side conditions away *)
+
+Lemma side_condition :
+ forall (A:Type) (B:Prop) x, (True -> B -> x=0) -> B -> x=x.
+Proof.
+intros.
+apply H in H0 as ->.
+reflexivity.
+exact I.
+Qed.
+
+(* Check that "apply" is chained on the last subgoal of each lemma and
+ that side conditions come first (as it is the case since 8.2) *)
+
+Lemma chaining :
+ forall A B C : Prop,
+ (1=1 -> (2=2 -> A -> B) /\ True) ->
+ (3=3 -> (True /\ (4=4 -> C -> A))) -> C -> B.
+Proof.
+intros.
+apply H, H0.
+exact (refl_equal 1).
+exact (refl_equal 2).
+exact (refl_equal 3).
+exact (refl_equal 4).
+assumption.
+Qed.
+
+(* Check that the side conditions of "apply in", even when chained and
+ used through conjunctions, come last (as it is the case for single
+ calls to "apply in" w/o destruction of conjunction since 8.2) *)
+
+Lemma chaining_in :
+ forall A B C : Prop,
+ (1=1 -> True /\ (B -> 2=2 -> 5=0)) ->
+ (3=3 -> (A -> 4=4 -> B) /\ True) -> A -> 0=5.
+Proof.
+intros.
+apply H0, H in H1 as ->.
+exact (refl_equal 0).
+exact (refl_equal 1).
+exact (refl_equal 2).
+exact (refl_equal 3).
+exact (refl_equal 4).
+Qed.
+
+(* From 12612, descent in conjunctions is more powerful *)
+(* The following, which was failing badly in bug 1980, is now accepted
+ (even if somehow surprising) *)
Goal True.
-try eapply ex_intro.
-trivial.
+eapply ex_intro.
+instantiate (2:=fun _ :True => True).
+instantiate (1:=I).
+exact I.
Qed.
+
+(* The following, which were not accepted, are now accepted as
+ expected by descent in conjunctions *)
+
+Goal True.
+eapply (ex_intro (fun _ => True) I).
+exact I.
+Qed.
+
+Goal True.
+eapply (fun (A:Prop) (x:A) => conj I x).
+exact I.
+Qed.
+
+(* The following was not accepted from r12612 to r12657 *)
+
+Record sig0 := { p1 : nat; p2 : p1 = 0 }.
+
+Goal forall x : sig0, p1 x = 0.
+intro x;
+apply x.
+Qed.
+
+(* The following worked in 8.2 but was not accepted from r12229 to
+ r12926 because "simple apply" started to use pattern unification of
+ evars. Evars pattern unification for simple (e)apply was disabled
+ in 12927 but "simple eapply" below worked from 12898 to 12926
+ because pattern-unification also started supporting abstraction
+ over Metas. However it did not find the "simple" solution and hence
+ the subsequent "assumption" failed. *)
+
+Goal exists f:nat->nat, forall x y, x = y -> f x = f y.
+intros; eexists; intros.
+simple eapply (@f_equal nat).
+assumption.
+Existential 1 := fun x => x.
+Qed.
+
+(* The following worked in 8.2 but was not accepted from r12229 to
+ r12897 for the same reason because eauto uses "simple apply". It
+ worked from 12898 to 12926 because eauto uses eassumption and not
+ assumption. *)
+
+Goal exists f:nat->nat, forall x y, x = y -> f x = f y.
+intros; eexists; intros.
+eauto.
+Existential 1 := fun x => x.
+Qed.
+
+(* The following was accepted before r12612 but is still not accepted in r12658
+
+Goal forall x : { x:nat | x = 0}, proj1_sig x = 0.
+intro x;
+apply x.
+
+*)
diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v
new file mode 100644
index 00000000..0a081271
--- /dev/null
+++ b/test-suite/success/autointros.v
@@ -0,0 +1,15 @@
+Set Automatic Introduction.
+
+Inductive even : nat -> Prop :=
+| even_0 : even 0
+| even_odd : forall n, odd n -> even (S n)
+with odd : nat -> Prop :=
+| odd_1 : odd 1
+| odd_even : forall n, even n -> odd (S n).
+
+Lemma foo {n : nat} (E : even n) : even (S (S n))
+with bar {n : nat} (O : odd n) : odd (S (S n)).
+Proof. destruct E. constructor. constructor. apply even_odd. apply (bar _ H).
+ destruct O. repeat constructor. apply odd_even. apply (foo _ H).
+Defined.
+
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index 94d827fd..b565183b 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -22,12 +22,12 @@ intros.
congruence.
Qed.
-(* Examples that fail due to dependencies *)
+(* Examples that fail due to dependencies *)
(* yields transitivity problem *)
Theorem dep :
- forall (A : Set) (P : A -> Set) (f g : forall x : A, P x)
+ forall (A : Set) (P : A -> Set) (f g : forall x : A, P x)
(x y : A) (e : x = y) (e0 : f y = g y), f x = g x.
intros; dependent rewrite e; exact e0.
Qed.
@@ -42,12 +42,12 @@ intros; rewrite e; reflexivity.
Qed.
-(* example that Congruence. can solve
- (dependent function applied to the same argument)*)
+(* example that Congruence. can solve
+ (dependent function applied to the same argument)*)
Theorem dep3 :
forall (A : Set) (P : A -> Set) (f g : forall x : A, P x),
- f = g -> forall x : A, f x = g x. intros.
+ f = g -> forall x : A, f x = g x. intros.
congruence.
Qed.
@@ -61,7 +61,7 @@ Qed.
Theorem inj2 :
forall (A : Set) (a c d : A) (f : A -> A * A),
- f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d.
+ f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d.
intros.
congruence.
Qed.
@@ -80,7 +80,7 @@ Qed.
(* example with implications *)
-Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D ->
+Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D ->
(A -> C) = (B -> D).
congruence.
Qed.
@@ -101,7 +101,6 @@ Proof.
congruence.
auto.
Qed.
-
-
- \ No newline at end of file
+
+
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index cea01712..5ac6ce82 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -4,3 +4,29 @@ Goal let a := 0+0 in a=a.
intro.
change 0 in (value of a).
change ((fun A:Type => A) nat) in (type of a).
+Abort.
+
+Goal forall x, 2 + S x = 1 + S x.
+intro.
+change (?u + S x) with (S (u + x)).
+Abort.
+
+(* Check the combination of at, with and in (see bug #2146) *)
+
+Goal 3=3 -> 3=3. intro H.
+change 3 at 2 with (1+2) in |- *.
+change 3 at 2 with (1+2) in H |-.
+change 3 with (1+2) in H at 1 |- * at 1.
+(* Now check that there are no more 3's *)
+change 3 with (1+2) in * || reflexivity.
+Qed.
+
+(* Note: the following is invalid and must fail
+change 3 at 1 with (1+2) at 3.
+change 3 at 1 with (1+2) in *.
+change 3 at 1 with (1+2) in H at 2 |-.
+change 3 at 1 with (1+2) in |- * at 3.
+change 3 at 1 with (1+2) in H |- *.
+change 3 at 1 with (1+2) in H, H|-.
+change 3 in |- * at 1.
+ *)
diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v
index 8169361c..976bec73 100644
--- a/test-suite/success/clear.v
+++ b/test-suite/success/clear.v
@@ -1,7 +1,7 @@
Goal forall x:nat, (forall x, x=0 -> True)->True.
intros; eapply H.
instantiate (1:=(fun y => _) (S x)).
- simpl.
+ simpl.
clear x. trivial.
Qed.
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 525348de..908b5f77 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -24,7 +24,7 @@ Coercion C : nat >-> Funclass.
(* Remark: in the following example, it cannot be decided whether C is
from nat to Funclass or from A to nat. An explicit Coercion command is
- expected
+ expected
Parameter A : nat -> Prop.
Parameter C:> forall n:nat, A n -> nat.
@@ -71,7 +71,6 @@ Record Morphism (X Y:Setoid) : Type :=
{evalMorphism :> X -> Y}.
Definition extSetoid (X Y:Setoid) : Setoid.
-intros X Y.
constructor.
exact (Morphism X Y).
Defined.
diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v
index 062c3ee5..f6ebacae 100644
--- a/test-suite/success/conv_pbs.v
+++ b/test-suite/success/conv_pbs.v
@@ -30,7 +30,7 @@ Fixpoint remove_assoc (A:Set)(x:variable)(rho: substitution A){struct rho}
: substitution A :=
match rho with
| nil => rho
- | (y,t) :: rho => if var_eq_dec x y then remove_assoc A x rho
+ | (y,t) :: rho => if var_eq_dec x y then remove_assoc A x rho
else (y,t) :: remove_assoc A x rho
end.
@@ -38,7 +38,7 @@ Fixpoint assoc (A:Set)(x:variable)(rho:substitution A){struct rho}
: option A :=
match rho with
| nil => None
- | (y,t) :: rho => if var_eq_dec x y then Some t
+ | (y,t) :: rho => if var_eq_dec x y then Some t
else assoc A x rho
end.
@@ -126,34 +126,34 @@ Inductive in_context (A:formula) : list formula -> Prop :=
| OmWeak : forall Gamma B, in_context A Gamma -> in_context A (cons B Gamma).
Inductive prove : list formula -> formula -> Type :=
- | ProofImplyR : forall A B Gamma, prove (cons A Gamma) B
+ | ProofImplyR : forall A B Gamma, prove (cons A Gamma) B
-> prove Gamma (A --> B)
- | ProofForallR : forall x A Gamma, (forall y, fresh y (A::Gamma)
+ | ProofForallR : forall x A Gamma, (forall y, fresh y (A::Gamma)
-> prove Gamma (subst A x (Var y))) -> prove Gamma (Forall x A)
- | ProofCont : forall A Gamma Gamma' C, context_prefix (A::Gamma) Gamma'
+ | ProofCont : forall A Gamma Gamma' C, context_prefix (A::Gamma) Gamma'
-> (prove_stoup Gamma' A C) -> (Gamma' |- C)
where "Gamma |- A" := (prove Gamma A)
with prove_stoup : list formula -> formula -> formula -> Type :=
| ProofAxiom Gamma C: Gamma ; C |- C
- | ProofImplyL Gamma C : forall A B, (Gamma |- A)
+ | ProofImplyL Gamma C : forall A B, (Gamma |- A)
-> (prove_stoup Gamma B C) -> (prove_stoup Gamma (A --> B) C)
- | ProofForallL Gamma C : forall x t A, (prove_stoup Gamma (subst A x t) C)
+ | ProofForallL Gamma C : forall x t A, (prove_stoup Gamma (subst A x t) C)
-> (prove_stoup Gamma (Forall x A) C)
where " Gamma ; B |- A " := (prove_stoup Gamma B A).
-Axiom context_prefix_trans :
+Axiom context_prefix_trans :
forall Gamma Gamma' Gamma'',
- context_prefix Gamma Gamma'
+ context_prefix Gamma Gamma'
-> context_prefix Gamma' Gamma''
-> context_prefix Gamma Gamma''.
-Axiom Weakening :
+Axiom Weakening :
forall Gamma Gamma' A,
context_prefix Gamma Gamma' -> Gamma |- A -> Gamma' |- A.
-
+
Axiom universal_weakening :
forall Gamma Gamma', context_prefix Gamma Gamma'
-> forall P, Gamma |- Atom P -> Gamma' |- Atom P.
@@ -170,20 +170,20 @@ Canonical Structure Universal := Build_Kripke
universal_weakening.
Axiom subst_commute :
- forall A rho x t,
+ forall A rho x t,
subst_formula ((x,t)::rho) A = subst (subst_formula rho A) x t.
Axiom subst_formula_atom :
- forall rho p t,
+ forall rho p t,
Atom (p, sem _ rho t) = subst_formula rho (Atom (p,t)).
Fixpoint universal_completeness (Gamma:context)(A:formula){struct A}
- : forall rho:substitution term,
+ : forall rho:substitution term,
force _ rho Gamma A -> Gamma |- subst_formula rho A
:=
- match A
- return forall rho, force _ rho Gamma A
- -> Gamma |- subst_formula rho A
+ match A
+ return forall rho, force _ rho Gamma A
+ -> Gamma |- subst_formula rho A
with
| Atom (p,t) => fun rho H => eq_rect _ (fun A => Gamma |- A) H _ (subst_formula_atom rho p t)
| A --> B => fun rho HImplyAB =>
@@ -192,21 +192,21 @@ Fixpoint universal_completeness (Gamma:context)(A:formula){struct A}
(HImplyAB (A'::Gamma)(CtxPrefixTrans A' (CtxPrefixRefl Gamma))
(universal_completeness_stoup A rho (fun C Gamma' Hle p
=> ProofCont Hle p))))
- | Forall x A => fun rho HForallA
- => ProofForallR x (fun y Hfresh
- => eq_rect _ _ (universal_completeness Gamma A _
+ | Forall x A => fun rho HForallA
+ => ProofForallR x (fun y Hfresh
+ => eq_rect _ _ (universal_completeness Gamma A _
(HForallA Gamma (CtxPrefixRefl Gamma)(Var y))) _ (subst_commute _ _ _ _ ))
end
with universal_completeness_stoup (Gamma:context)(A:formula){struct A}
: forall rho, (forall C Gamma', context_prefix Gamma Gamma'
-> Gamma' ; subst_formula rho A |- C -> Gamma' |- C)
-> force _ rho Gamma A
- :=
- match A return forall rho,
- (forall C Gamma', context_prefix Gamma Gamma'
+ :=
+ match A return forall rho,
+ (forall C Gamma', context_prefix Gamma Gamma'
-> Gamma' ; subst_formula rho A |- C
-> Gamma' |- C)
- -> force _ rho Gamma A
+ -> force _ rho Gamma A
with
| Atom (p,t) as C => fun rho H
=> H _ Gamma (CtxPrefixRefl Gamma)(ProofAxiom _ _)
diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v
index fede31a8..bc1757fd 100644
--- a/test-suite/success/decl_mode.v
+++ b/test-suite/success/decl_mode.v
@@ -8,10 +8,10 @@ proof.
assume n:nat.
per induction on n.
suppose it is 0.
- suffices (0=0) to show thesis.
+ suffices (0=0) to show thesis.
thus thesis.
suppose it is (S m) and Hrec:thesis for m.
- have (div2 (double (S m))= div2 (S (S (double m)))).
+ have (div2 (double (S m))= div2 (S (S (double m)))).
~= (S (div2 (double m))).
thus ~= (S m) by Hrec.
end induction.
@@ -56,12 +56,12 @@ proof.
end proof.
Qed.
-Lemma main_thm_aux: forall n,even n ->
+Lemma main_thm_aux: forall n,even n ->
double (double (div2 n *div2 n))=n*n.
proof.
given n such that H:(even n).
- *** have (double (double (div2 n * div2 n))
- = double (div2 n) * double (div2 n))
+ *** have (double (double (div2 n * div2 n))
+ = double (div2 n) * double (div2 n))
by double_mult_l,double_mult_r.
thus ~= (n*n) by H,even_double.
end proof.
@@ -75,14 +75,14 @@ proof.
per induction on m.
suppose it is 0.
thus thesis.
- suppose it is (S mm) and thesis for mm.
+ suppose it is (S mm) and thesis for mm.
then H:(even (S (S (mm+mm)))).
have (S (S (mm + mm)) = S mm + S mm) using omega.
hence (even (S mm +S mm)) by H.
end induction.
end proof.
Qed.
-
+
Theorem main_theorem: forall n p, n*n=double (p*p) -> p=0.
proof.
assume n0:nat.
@@ -95,7 +95,7 @@ proof.
suppose it is (S p').
assume (n * n = double (S p' * S p')).
=~ 0 by H1,mult_n_O.
- ~= (S ( p' + p' * S p' + S p'* S p'))
+ ~= (S ( p' + p' * S p' + S p'* S p'))
by plus_n_Sm.
hence thesis .
suppose it is 0.
@@ -106,19 +106,19 @@ proof.
have (even (double (p*p))) by even_double_n .
then (even (n*n)) by H0.
then H2:(even n) by even_is_even_times_even.
- then (double (double (div2 n *div2 n))=n*n)
+ then (double (double (div2 n *div2 n))=n*n)
by main_thm_aux.
~= (double (p*p)) by H0.
- then H':(double (div2 n *div2 n)= p*p) by double_inv.
+ then H':(double (div2 n *div2 n)= p*p) by double_inv.
have (even (double (div2 n *div2 n))) by even_double_n.
then (even (p*p)) by even_double_n,H'.
then H3:(even p) by even_is_even_times_even.
- have (double(double (div2 n * div2 n)) = n*n)
+ have (double(double (div2 n * div2 n)) = n*n)
by H2,main_thm_aux.
~= (double (p*p)) by H0.
- ~= (double(double (double (div2 p * div2 p))))
+ ~= (double(double (double (div2 p * div2 p))))
by H3,main_thm_aux.
- then H'':(div2 n * div2 n = double (div2 p * div2 p))
+ then H'':(div2 n * div2 n = double (div2 p * div2 p))
by double_inv.
then (div2 n < n) by lt_div2,neq_O_lt,H1.
then H4:(div2 p=0) by (H (div2 n)),H''.
@@ -137,8 +137,8 @@ Coercion IZR: Z >->R.*)
Open Scope R_scope.
-Lemma square_abs_square:
- forall p,(INR (Zabs_nat p) * INR (Zabs_nat p)) = (IZR p * IZR p).
+Lemma square_abs_square:
+ forall p,(INR (Zabs_nat p) * INR (Zabs_nat p)) = (IZR p * IZR p).
proof.
assume p:Z.
per cases on p.
@@ -147,7 +147,7 @@ proof.
suppose it is (Zpos z).
thus thesis.
suppose it is (Zneg z).
- have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (Zneg z))) =
+ have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (Zneg z))) =
(IZR (Zpos z) * IZR (Zpos z))).
~= ((- IZR (Zpos z)) * (- IZR (Zpos z))).
thus ~= (IZR (Zneg z) * IZR (Zneg z)).
@@ -160,19 +160,19 @@ Definition irrational (x:R):Prop :=
Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)).
proof.
- let p:Z,q:nat be such that H:(q<>0%nat)
+ let p:Z,q:nat be such that H:(q<>0%nat)
and H0:(sqrt (INR 2%nat)=(IZR p/INR q)).
have H_in_R:(INR q<>0:>R) by H.
have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field.
have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def.
- have (INR (Zabs_nat p * Zabs_nat p)
- = (INR (Zabs_nat p) * INR (Zabs_nat p)))
+ have (INR (Zabs_nat p * Zabs_nat p)
+ = (INR (Zabs_nat p) * INR (Zabs_nat p)))
by mult_INR.
~= (IZR p* IZR p) by square_abs_square.
~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *)
~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring.
~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0.
- ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR.
+ ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR.
then (Zabs_nat p * Zabs_nat p = 2* (q * q))%nat.
~= ((q*q)+(q*q))%nat.
~= (Div2.double (q*q)).
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 46dd0cb6..fe0165d0 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,5 +1,4 @@
-Require Import Coq.Program.Program.
-
+Require Import Coq.Program.Program Coq.Program.Equality.
Variable A : Set.
@@ -39,7 +38,7 @@ Delimit Scope context_scope with ctx.
Arguments Scope snoc [context_scope].
-Notation " Γ ,, τ " := (snoc Γ τ) (at level 25, t at next level, left associativity).
+Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope.
Fixpoint conc (Δ Γ : ctx) : ctx :=
match Δ with
@@ -47,60 +46,64 @@ Fixpoint conc (Δ Γ : ctx) : ctx :=
| snoc Δ' x => snoc (conc Δ' Γ) x
end.
-Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
+Notation " Γ ; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
+
+Reserved Notation " Γ ⊢ τ " (at level 30, no associativity).
+
+Generalizable All Variables.
Inductive term : ctx -> type -> Type :=
-| ax : forall Γ τ, term (snoc Γ τ) τ
-| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ ,, τ') τ
-| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ')
-| app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'.
+| ax : `(Γ, τ ⊢ τ)
+| weak : `{Γ ⊢ τ -> Γ, τ' ⊢ τ}
+| abs : `{Γ, τ ⊢ τ' -> Γ ⊢ τ --> τ'}
+| app : `{Γ ⊢ τ --> τ' -> Γ ⊢ τ -> Γ ⊢ τ'}
+
+where " Γ ⊢ τ " := (term Γ τ) : type_scope.
Hint Constructors term : lambda.
Open Local Scope context_scope.
-Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope.
+Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps.
-Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ ->
- forall τ', term (Γ ,, τ' ;; Δ) τ.
-Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda.
+Lemma weakening : forall Γ Δ τ, Γ ; Δ ⊢ τ ->
+ forall τ', Γ , τ' ; Δ ⊢ τ.
+Proof with simpl in * ; eqns ; eauto with lambda.
intros Γ Δ τ H.
dependent induction H.
- destruct Δ...
+ destruct Δ as [|Δ τ'']...
- destruct Δ...
+ destruct Δ as [|Δ τ'']...
- destruct Δ...
- apply abs...
-
- specialize (IHterm (Δ,, t,, τ)%ctx Γ0)...
+ destruct Δ as [|Δ τ'']...
+ apply abs.
+ specialize (IHterm Γ (Δ, τ'', τ))...
- intro.
- apply app with Ï„...
-Qed.
+ intro. eapply app...
+Defined.
-Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ.
-Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto.
+Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
+Proof with simpl in * ; eqns ; eauto.
intros until 1.
dependent induction H.
- destruct Δ...
+ destruct Δ ; eqns.
apply weak ; apply ax.
apply ax.
destruct Δ...
- pose (weakening Γ0 (empty,, α))...
+ pose (weakening Γ (empty, α))...
apply weak...
- apply abs...
- specialize (IHterm (Δ ,, τ))...
+ apply abs...
+ specialize (IHterm Γ (Δ, τ))...
- eapply app with Ï„...
-Save.
+ eapply app...
+Defined.
(** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *)
@@ -124,5 +127,5 @@ Inductive Ev : forall t, Exp t -> Exp t -> Prop :=
Ev (Fst e) e1.
Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2).
-intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption.
+intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption.
Qed.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 5aa78816..8013e1d3 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -1,11 +1,11 @@
(* Submitted by Robert Schneck *)
-Parameter A B C D : Prop.
+Parameters A B C D : Prop.
Axiom X : A -> B -> C /\ D.
Lemma foo : A -> B -> C.
Proof.
-intros.
+intros.
destruct X. (* Should find axiom X and should handle arguments of X *)
assumption.
assumption.
@@ -45,9 +45,9 @@ Require Import List.
Definition alist R := list (nat * R)%type.
Section Properties.
- Variables A : Type.
- Variables a : A.
- Variables E : alist A.
+ Variable A : Type.
+ Variable a : A.
+ Variable E : alist A.
Lemma silly : E = E.
Proof.
@@ -55,3 +55,22 @@ Section Properties.
Abort.
End Properties.
+
+(* This used not to work before revision 11944 *)
+
+Goal forall P:(forall n, 0=n -> Prop), forall H: 0=0, P 0 H.
+destruct H.
+Abort.
+
+(* The calls to "destruct" below did not work before revision 12356 *)
+
+Variable A0:Type.
+Variable P:A0->Type.
+Require Import JMeq.
+Goal forall a b (p:P a) (q:P b),
+ forall H:a = b, eq_rect a P p b H = q -> JMeq (existT _ a p) (existT _ b q).
+intros.
+destruct H.
+destruct H0.
+reflexivity.
+Qed.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 26339d51..c7a2a6c9 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -56,5 +56,5 @@ Lemma simpl_plus_l_rr1 :
(forall m p : Nat, plus' n m = plus' n p -> m = p) ->
forall m p : Nat, S' (plus' n m) = S' (plus' n p) -> m = p.
intros.
- eauto. (* does EApply H *)
+ eauto. (* does EApply H *)
Qed.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 082cbfbe..6423ad14 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -10,7 +10,7 @@ Definition c A (Q : (nat * A -> Prop) -> Prop) P :=
(* What does this test ? *)
Require Import List.
-Definition list_forall_bool (A : Set) (p : A -> bool)
+Definition list_forall_bool (A : Set) (p : A -> bool)
(l : list A) : bool :=
fold_right (fun a r => if p a then r else false) true l.
@@ -109,21 +109,21 @@ Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
avl m -> avl (map f m).
Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt),
bst m -> bst (map f m).
-Record bbst (elt:Set) : Set :=
+Record bbst (elt:Set) : Set :=
Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}.
Definition t' := bbst.
Section B.
Variables elt elt': Set.
-Definition map' f (m:t' elt) : t' elt' :=
+Definition map' f (m:t' elt) : t' elt' :=
Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
End B.
Unset Implicit Arguments.
-(* An example from Lexicographic_Exponentiation that tests the
+(* An example from Lexicographic_Exponentiation that tests the
contraction of reducible fixpoints in type inference *)
Require Import List.
-Check (fun (A:Set) (a b x:A) (l:list A)
+Check (fun (A:Set) (a b x:A) (l:list A)
(H : l ++ cons x nil = cons b (cons a nil)) =>
app_inj_tail l (cons b nil) _ _ H).
@@ -133,14 +133,14 @@ Parameter h:(nat->nat)->(nat->nat).
Fixpoint G p cont {struct p} :=
h (fun n => match p with O => cont | S p => G p cont end n).
-(* An example from Bordeaux/Cantor that applies evar restriction
+(* An example from Bordeaux/Cantor that applies evar restriction
below a binder *)
Require Import Relations.
Parameter lex : forall (A B : Set), (forall (a1 a2:A), {a1=a2}+{a1<>a2})
-> relation A -> relation B -> A * B -> A * B -> Prop.
-Check
- forall (A B : Set) eq_A_dec o1 o2,
+Check
+ forall (A B : Set) eq_A_dec o1 o2,
antisymmetric A o1 -> transitive A o1 -> transitive B o2 ->
transitive _ (lex _ _ eq_A_dec o1 o2).
@@ -198,10 +198,26 @@ Goal forall x : nat, F1 x -> G1 x.
refine (fun x H => proj2 (_ x H) _).
Abort.
-(* Remark: the following example does not succeed any longer in 8.2 because,
- the algorithm is more general and does exclude a solution that it should
- exclude for typing reason. Handling of types and backtracking is still to
- be done
+(* An example from y-not that was failing in 8.2rc1 *)
+
+Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) :=
+ match l with
+ | nil => nil
+ | (existT k v)::l' => (existT _ k v):: (filter A l')
+ end.
+
+(* Bug #2000: used to raise Out of memory in 8.2 while it should fail by
+ lack of information on the conclusion of the type of j *)
+
+Goal True.
+set (p:=fun j => j (or_intror _ (fun a:True => j (or_introl _ a)))) || idtac.
+Abort.
+
+(* Remark: the following example stopped succeeding at some time in
+ the development of 8.2 but it works again (this was because 8.2
+ algorithm was more general and did not exclude a solution that it
+ should have excluded for typing reason; handling of types and
+ backtracking is still to be done) *)
Section S.
Variables A B : nat -> Prop.
@@ -209,4 +225,16 @@ Goal forall x : nat, A x -> B x.
refine (fun x H => proj2 (_ x H) _).
Abort.
End S.
-*)
+
+(* Check that constraints are taken into account by tactics that instantiate *)
+
+Lemma inj : forall n m, S n = S m -> n = m.
+intros n m H.
+eapply f_equal with (* should fail because ill-typed *)
+ (f := fun n =>
+ match n return match n with S _ => nat | _ => unit end with
+ | S n => n
+ | _ => tt
+ end) in H
+|| injection H.
+Abort.
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 74d87ffa..d3bdb1b6 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -9,10 +9,10 @@
Require Import Arith.
Require Import List.
-(**** A few tests for the extraction mechanism ****)
+(**** A few tests for the extraction mechanism ****)
-(* Ideally, we should monitor the extracted output
- for changes, but this is painful. For the moment,
+(* Ideally, we should monitor the extracted output
+ for changes, but this is painful. For the moment,
we just check for failures of this script. *)
(*** STANDARD EXAMPLES *)
@@ -23,7 +23,7 @@ Definition idnat (x:nat) := x.
Extraction idnat.
(* let idnat x = x *)
-Definition id (X:Type) (x:X) := x.
+Definition id (X:Type) (x:X) := x.
Extraction id. (* let id x = x *)
Definition id' := id Set nat.
Extraction id'. (* type id' = nat *)
@@ -47,7 +47,7 @@ Extraction test5.
Definition cf (x:nat) (_:x <= 0) := S x.
Extraction NoInline cf.
Definition test6 := cf 0 (le_n 0).
-Extraction test6.
+Extraction test6.
(* let test6 = cf O *)
Definition test7 := (fun (X:Set) (x:X) => x) nat.
@@ -60,9 +60,9 @@ Definition d2 := d Set.
Extraction d2. (* type d2 = __ d *)
Definition d3 (x:d Set) := 0.
Extraction d3. (* let d3 _ = O *)
-Definition d4 := d nat.
+Definition d4 := d nat.
Extraction d4. (* type d4 = nat d *)
-Definition d5 := (fun x:d Type => 0) Type.
+Definition d5 := (fun x:d Type => 0) Type.
Extraction d5. (* let d5 = O *)
Definition d6 (x:d Type) := x.
Extraction d6. (* type 'x d6 = 'x *)
@@ -80,7 +80,7 @@ Definition test11 := let n := 0 in let p := S n in S p.
Extraction test11. (* let test11 = S (S O) *)
Definition test12 := forall x:forall X:Type, X -> X, x Type Type.
-Extraction test12.
+Extraction test12.
(* type test12 = (__ -> __ -> __) -> __ *)
@@ -115,14 +115,14 @@ Extraction test20.
(** Simple inductive type and recursor. *)
Extraction nat.
-(*
-type nat =
- | O
- | S of nat
+(*
+type nat =
+ | O
+ | S of nat
*)
Extraction sumbool_rect.
-(*
+(*
let sumbool_rect f f0 = function
| Left -> f __
| Right -> f0 __
@@ -134,7 +134,7 @@ Inductive c (x:nat) : nat -> Set :=
| refl : c x x
| trans : forall y z:nat, c x y -> y <= z -> c x z.
Extraction c.
-(*
+(*
type c =
| Refl
| Trans of nat * nat * c
@@ -150,7 +150,7 @@ Inductive Finite (U:Type) : Ensemble U -> Type :=
forall A:Ensemble U,
Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x).
Extraction Finite.
-(*
+(*
type 'u finite =
| Empty_is_finite
| Union_is_finite of 'u finite * 'u
@@ -166,7 +166,7 @@ with forest : Set :=
| Cons : tree -> forest -> forest.
Extraction tree.
-(*
+(*
type tree =
| Node of nat * forest
and forest =
@@ -178,7 +178,7 @@ Fixpoint tree_size (t:tree) : nat :=
match t with
| Node a f => S (forest_size f)
end
-
+
with forest_size (f:forest) : nat :=
match f with
| Leaf b => 1
@@ -186,7 +186,7 @@ Fixpoint tree_size (t:tree) : nat :=
end.
Extraction tree_size.
-(*
+(*
let rec tree_size = function
| Node (a, f) -> S (forest_size f)
and forest_size = function
@@ -203,13 +203,13 @@ Definition test14 := tata 0.
Extraction test14.
(* let test14 x x0 x1 = Tata (O, x, x0, x1) *)
Definition test15 := tata 0 1.
-Extraction test15.
+Extraction test15.
(* let test15 x x0 = Tata (O, (S O), x, x0) *)
Inductive eta : Type :=
eta_c : nat -> Prop -> nat -> Prop -> eta.
Extraction eta_c.
-(*
+(*
type eta =
| Eta_c of nat * nat
*)
@@ -220,15 +220,15 @@ Definition test17 := eta_c 0 True.
Extraction test17.
(* let test17 x = Eta_c (O, x) *)
Definition test18 := eta_c 0 True 0.
-Extraction test18.
+Extraction test18.
(* let test18 _ = Eta_c (O, O) *)
(** Example of singleton inductive type *)
Inductive bidon (A:Prop) (B:Type) : Type :=
- tb : forall (x:A) (y:B), bidon A B.
-Definition fbidon (A B:Type) (f:A -> B -> bidon True nat)
+ tb : forall (x:A) (y:B), bidon A B.
+Definition fbidon (A B:Type) (f:A -> B -> bidon True nat)
(x:A) (y:B) := f x y.
Extraction bidon.
(* type 'b bidon = 'b *)
@@ -252,11 +252,11 @@ Extraction fbidon2.
Inductive test_0 : Prop :=
ctest0 : test_0
with test_1 : Set :=
- ctest1 : test_0 -> test_1.
+ ctest1 : test_0 -> test_1.
Extraction test_0.
(* test0 : logical inductive *)
-Extraction test_1.
-(*
+Extraction test_1.
+(*
type test1 =
| Ctest1
*)
@@ -277,19 +277,19 @@ Inductive tp1 : Type :=
with tp2 : Type :=
T' : tp1 -> tp2.
Extraction tp1.
-(*
+(*
type tp1 =
| T of __ * tp2
and tp2 =
| T' of tp1
-*)
+*)
Inductive tp1bis : Type :=
Tbis : tp2bis -> tp1bis
with tp2bis : Type :=
T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis.
Extraction tp1bis.
-(*
+(*
type tp1bis =
| Tbis of tp2bis
and tp2bis =
@@ -344,8 +344,8 @@ intros.
exact n.
Qed.
Extraction oups.
-(*
-let oups h0 =
+(*
+let oups h0 =
match Obj.magic h0 with
| Nil -> h0
| Cons0 (n, l) -> n
@@ -357,7 +357,7 @@ let oups h0 =
Definition horibilis (b:bool) :=
if b as b return (if b then Type else nat) then Set else 0.
Extraction horibilis.
-(*
+(*
let horibilis = function
| True -> Obj.magic __
| False -> Obj.magic O
@@ -370,8 +370,8 @@ Definition natbool (b:bool) := if b then nat else bool.
Extraction natbool. (* type natbool = __ *)
Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true.
-Extraction zerotrue.
-(*
+Extraction zerotrue.
+(*
let zerotrue = function
| True -> Obj.magic O
| False -> Obj.magic True
@@ -383,7 +383,7 @@ Definition natTrue (b:bool) := if b return Type then nat else True.
Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True.
Extraction zeroTrue.
-(*
+(*
let zeroTrue = function
| True -> Obj.magic O
| False -> Obj.magic __
@@ -393,7 +393,7 @@ Definition natTrue2 (b:bool) := if b return Type then nat else True.
Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I.
Extraction zeroprop.
-(*
+(*
let zeroprop = function
| True -> Obj.magic O
| False -> Obj.magic __
@@ -410,8 +410,8 @@ Extraction test21.
Definition test22 :=
(fun f:forall X:Type, X -> X => (f nat 0, f bool true))
(fun (X:Type) (x:X) => x).
-Extraction test22.
-(* let test22 =
+Extraction test22.
+(* let test22 =
let f = fun x -> x in Pair ((f O), (f True)) *)
(* still ok via optim beta -> let *)
@@ -461,8 +461,8 @@ Extraction f_normal.
(* inductive with magic needed *)
Inductive Boite : Set :=
- boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite.
-Extraction Boite.
+ boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite.
+Extraction Boite.
(*
type boite =
| Boite of bool * __
@@ -482,8 +482,8 @@ Definition test_boite (B:Boite) :=
| boite true n => n
| boite false n => fst n + snd n
end.
-Extraction test_boite.
-(*
+Extraction test_boite.
+(*
let test_boite = function
| Boite (b0, n) ->
(match b0 with
@@ -494,23 +494,23 @@ let test_boite = function
(* singleton inductive with magic needed *)
Inductive Box : Type :=
- box : forall A:Set, A -> Box.
+ box : forall A:Set, A -> Box.
Extraction Box.
(* type box = __ *)
-Definition box1 := box nat 0.
+Definition box1 := box nat 0.
Extraction box1. (* let box1 = Obj.magic O *)
(* applied constant, magic needed *)
Definition idzarb (b:bool) (x:if b then nat else bool) := x.
Definition zarb := idzarb true 0.
-Extraction NoInline idzarb.
-Extraction zarb.
+Extraction NoInline idzarb.
+Extraction zarb.
(* let zarb = Obj.magic idzarb True (Obj.magic O) *)
(** function of variable arity. *)
-(** Fun n = nat -> nat -> ... -> nat *)
+(** Fun n = nat -> nat -> ... -> nat *)
Fixpoint Fun (n:nat) : Set :=
match n with
@@ -532,20 +532,20 @@ Fixpoint proj (k n:nat) {struct n} : Fun n :=
| O => fun x => Const x n
| S k => fun x => proj k n
end
- end.
+ end.
Definition test_proj := proj 2 4 0 1 2 3.
-Eval compute in test_proj.
+Eval compute in test_proj.
-Recursive Extraction test_proj.
+Recursive Extraction test_proj.
-(*** TO SUM UP: ***)
+(*** TO SUM UP: ***)
(* Was previously producing a "test_extraction.ml" *)
-Recursive Extraction
+Recursive Extraction
idnat id id' test2 test3 test4 test5 test6 test7 d d2
d3 d4 d5 d6 test8 id id' test9 test10 test11 test12
test13 test19 test20 nat sumbool_rect c Finite tree
@@ -581,7 +581,7 @@ Recursive Extraction
zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop
f_arity f_normal Boite boite1 boite2 test_boite Box box1
zarb test_proj.
-
+
(*** Finally, a test more focused on everyday's life situations ***)
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index 78b01f3e..be4e0684 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -47,10 +47,10 @@ Fixpoint maxVar (e : rExpr) : rNat :=
Require Import Streams.
-Definition decomp (s:Stream nat) : Stream nat :=
+Definition decomp (s:Stream nat) : Stream nat :=
match s with Cons _ s => s end.
-CoFixpoint bx0 : Stream nat := Cons 0 bx1
+CoFixpoint bx0 : Stream nat := Cons 0 bx1
with bx1 : Stream nat := Cons 1 bx0.
Lemma bx0bx : decomp bx0 = bx1.
diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v
index 21bfc075..af81e53d 100644
--- a/test-suite/success/hyps_inclusion.v
+++ b/test-suite/success/hyps_inclusion.v
@@ -8,7 +8,7 @@
tactics were using Typing.type_of and not Typeops.typing; the former
was not checking hyps inclusion so that the discrepancy in the types
of section variables seen as goal variables was not a problem (at the
- end, when the proof is completed, the section variable recovers its
+ end, when the proof is completed, the section variable recovers its
original type and all is correct for Typeops) *)
Section A.
@@ -16,9 +16,9 @@ Variable H:not True.
Lemma f:nat->nat. destruct H. exact I. Defined.
Goal f 0=f 1.
red in H.
-(* next tactic was failing wrt bug #1325 because type-checking the goal
+(* next tactic was failing wrt bug #1325 because type-checking the goal
detected a syntactically different type for the section variable H *)
-case 0.
+case 0.
Reset A.
(* Variant with polymorphic inductive types for bug #1325 *)
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 9034d6a6..59e1a935 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -1,3 +1,5 @@
+(* Testing the behavior of implicit arguments *)
+
(* Implicit on section variables *)
Set Implicit Arguments.
@@ -12,15 +14,53 @@ Infix "#" := op (at level 70).
Check (forall x : A, x # x).
(* Example submitted by Christine *)
-Record stack : Type :=
+
+Record stack : Type :=
{type : Set; elt : type; empty : type -> bool; proof : empty elt = true}.
Check
(forall (type : Set) (elt : type) (empty : type -> bool),
empty elt = true -> stack).
+(* Nested sections and manual/automatic implicit arguments *)
+
+Variable op' : forall A : Set, A -> A -> Set.
+Variable op'' : forall A : Set, A -> A -> Set.
+
+Section B.
+
+Definition eq1 := fun (A:Type) (x y:A) => x=y.
+Definition eq2 := fun (A:Type) (x y:A) => x=y.
+Definition eq3 := fun (A:Type) (x y:A) => x=y.
+
+Implicit Arguments op' [].
+Global Implicit Arguments op'' [].
+
+Implicit Arguments eq2 [].
+Global Implicit Arguments eq3 [].
+
+Check (op 0 0).
+Check (op' nat 0 0).
+Check (op'' nat 0 0).
+Check (eq1 0 0).
+Check (eq2 nat 0 0).
+Check (eq3 nat 0 0).
+
+End B.
+
+Check (op 0 0).
+Check (op' 0 0).
+Check (op'' nat 0 0).
+Check (eq1 0 0).
+Check (eq2 0 0).
+Check (eq3 nat 0 0).
+
End Spec.
+Check (eq1 0 0).
+Check (eq2 0 0).
+Check (eq3 nat 0 0).
+
(* Example submitted by Frédéric (interesting in v8 syntax) *)
Parameter f : nat -> nat * nat.
@@ -42,7 +82,7 @@ Inductive P n : nat -> Prop := c : P n n.
Require Import List.
Fixpoint plus n m {struct n} :=
- match n with
+ match n with
| 0 => m
| S p => S (plus p m)
end.
diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v
index c3dc2fc6..fcedb2b1 100644
--- a/test-suite/success/import_lib.v
+++ b/test-suite/success/import_lib.v
@@ -1,8 +1,8 @@
Definition le_trans := 0.
-Module Test_Read.
- Module M.
+Module Test_Read.
+ Module M.
Require Le. (* Reading without importing *)
Check Le.le_trans.
@@ -12,7 +12,7 @@ Module Test_Read.
Qed.
End M.
- Check Le.le_trans.
+ Check Le.le_trans.
Lemma th0 : le_trans = 0.
reflexivity.
@@ -32,84 +32,84 @@ Definition le_decide := 1. (* from Arith/Compare *)
Definition min := 0. (* from Arith/Min *)
Module Test_Require.
-
+
Module M.
Require Import Compare. (* Imports Min as well *)
-
+
Lemma th1 : le_decide = le_decide.
reflexivity.
Qed.
-
+
Lemma th2 : min = min.
reflexivity.
Qed.
-
+
End M.
-
+
(* Checks that Compare and List are loaded *)
Check Compare.le_decide.
Check Min.min.
-
-
+
+
(* Checks that Compare and List are _not_ imported *)
Lemma th1 : le_decide = 1.
reflexivity.
Qed.
-
+
Lemma th2 : min = 0.
reflexivity.
Qed.
-
+
(* It should still be the case after Import M *)
Import M.
-
+
Lemma th3 : le_decide = 1.
reflexivity.
Qed.
-
+
Lemma th4 : min = 0.
reflexivity.
Qed.
-End Test_Require.
+End Test_Require.
(****************************************************************)
Module Test_Import.
Module M.
Import Compare. (* Imports Min as well *)
-
+
Lemma th1 : le_decide = le_decide.
reflexivity.
Qed.
-
+
Lemma th2 : min = min.
reflexivity.
Qed.
-
+
End M.
-
+
(* Checks that Compare and List are loaded *)
Check Compare.le_decide.
Check Min.min.
-
-
+
+
(* Checks that Compare and List are _not_ imported *)
Lemma th1 : le_decide = 1.
reflexivity.
Qed.
-
+
Lemma th2 : min = 0.
reflexivity.
Qed.
-
+
(* It should still be the case after Import M *)
Import M.
-
+
Lemma th3 : le_decide = 1.
reflexivity.
Qed.
-
+
Lemma th4 : min = 0.
reflexivity.
Qed.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 2aec6e9b..8e1a8d18 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -5,7 +5,8 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* Teste des definitions inductives imbriquees *)
+
+(* Test des definitions inductives imbriquees *)
Require Import List.
@@ -15,3 +16,28 @@ Inductive X : Set :=
Inductive Y : Set :=
cons2 : list (Y * Y) -> Y.
+(* Test inductive types with local definitions *)
+
+Inductive eq1 : forall A:Type, let B:=A in A -> Prop :=
+ refl1 : eq1 True I.
+
+Check
+ fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) =>
+ let B := A in
+ fun (a : A) (e : eq1 A a) =>
+ match e in (eq1 A0 B0 a0) return (P A0 a0) with
+ | refl1 => f
+ end.
+
+Inductive eq2 (A:Type) (a:A)
+ : forall B C:Type, let D:=(A*B*C)%type in D -> Prop :=
+ refl2 : eq2 A a unit bool (a,tt,true).
+
+(* Check that induction variables are cleared even with in clause *)
+
+Lemma foo : forall n m : nat, n + m = n + m.
+Proof.
+ intros; induction m as [|m] in n |- *.
+ auto.
+ auto.
+Qed.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 757cf6a4..dfa41c82 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -3,7 +3,7 @@
(* Submitted by Pierre Crégut *)
(* Checks substitution of x *)
Ltac f x := unfold x in |- *; idtac.
-
+
Lemma lem1 : 0 + 0 = 0.
f plus.
reflexivity.
@@ -25,7 +25,7 @@ U.
Qed.
(* Check that Match giving non-tactic arguments are evaluated at Let-time *)
-
+
Ltac B := let y := (match goal with
| z:_ |- _ => z
end) in
@@ -152,6 +152,7 @@ Abort.
Ltac afi tac := intros; tac.
Goal 1 = 2.
afi ltac:auto.
+Abort.
(* Tactic Notation avec listes *)
@@ -179,8 +180,8 @@ Abort.
(* Check second-order pattern unification *)
Ltac to_exist :=
- match goal with
- |- forall x y, @?P x y =>
+ match goal with
+ |- forall x y, @?P x y =>
let Q := eval lazy beta in (exists x, forall y, P x y) in
assert (Q->Q)
end.
@@ -201,7 +202,7 @@ Abort.
(* Utilisation de let rec sans arguments *)
-Ltac is :=
+Ltac is :=
let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
i.
@@ -220,3 +221,25 @@ Z1 O.
Z2 ltac:O.
exact I.
Qed.
+
+(* Illegal application used to make Ltac loop. *)
+
+Section LtacLoopTest.
+ Ltac f x := idtac.
+ Goal True.
+ Timeout 1 try f()().
+ Abort.
+End LtacLoopTest.
+
+(* Test binding of open terms *)
+
+Ltac test_open_match z :=
+ match z with
+ (forall y x, ?h = 0) => assert (forall x y, h = x + y)
+ end.
+
+Goal True.
+test_open_match (forall z y, y + z = 0).
+reflexivity.
+apply I.
+Qed.
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index 463efed3..f63dfc38 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -9,7 +9,7 @@
Require Export List.
- Record signature : Type :=
+ Record signature : Type :=
{sort : Set;
sort_beq : sort -> sort -> bool;
sort_beq_refl : forall f : sort, true = sort_beq f f;
@@ -20,14 +20,14 @@ Require Export List.
fsym_beq_refl : forall f : fsym, true = fsym_beq f f;
fsym_beq_eq : forall f1 f2 : fsym, true = fsym_beq f1 f2 -> f1 = f2}.
-
+
Variable F : signature.
Definition vsym := (sort F * nat)%type.
Definition vsym_sort := fst (A:=sort F) (B:=nat).
Definition vsym_nat := snd (A:=sort F) (B:=nat).
-
+
Inductive term : sort F -> Set :=
| term_var : forall v : vsym, term (vsym_sort v)
diff --git a/test-suite/success/parsing.v b/test-suite/success/parsing.v
index d1b679d5..3d06d1d0 100644
--- a/test-suite/success/parsing.v
+++ b/test-suite/success/parsing.v
@@ -2,7 +2,7 @@ Section A.
Notation "*" := O (at level 8).
Notation "**" := O (at level 99).
Notation "***" := O (at level 9).
-End A.
+End A.
Notation "*" := O (at level 8).
Notation "**" := O (at level 99).
Notation "***" := O (at level 9).
diff --git a/test-suite/success/pattern.v b/test-suite/success/pattern.v
index 28d0bd55..72f84052 100644
--- a/test-suite/success/pattern.v
+++ b/test-suite/success/pattern.v
@@ -5,3 +5,45 @@
Goal (id true,id false)=(id true,id true).
generalize bool at 2 4 6 8 10 as B, true at 3 as tt, false as ff.
+Abort.
+
+(* Check use of occurrences in hypotheses for a reduction tactic such
+ as pattern *)
+
+(* Did not work in 8.2 *)
+Goal 0=0->True.
+intro H.
+pattern 0 in H at 2.
+set (f n := 0 = n) in H. (* check pattern worked correctly *)
+Abort.
+
+(* Syntactic variant which was working in 8.2 *)
+Goal 0=0->True.
+intro H.
+pattern 0 at 2 in H.
+set (f n := 0 = n) in H. (* check pattern worked correctly *)
+Abort.
+
+(* Ambiguous occurrence selection *)
+Goal 0=0->True.
+intro H.
+pattern 0 at 1 in H at 2 || exact I. (* check pattern fails *)
+Qed.
+
+(* Ambiguous occurrence selection *)
+Goal 0=1->True.
+intro H.
+pattern 0, 1 in H at 1 2 || exact I. (* check pattern fails *)
+Qed.
+
+(* Occurrence selection shared over hypotheses is difficult to advocate and
+ hence no longer allowed *)
+Goal 0=1->1=0->True.
+intros H1 H2.
+pattern 0 at 1, 1 in H1, H2 || exact I. (* check pattern fails *)
+Qed.
+
+(* Test catching of reduction tactics errors (was not the case in 8.2) *)
+Goal eq_refl 0 = eq_refl 0.
+pattern 0 at 1 || reflexivity.
+Qed.
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index b654277c..4d743a6d 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -7,7 +7,7 @@ exists y; auto.
Save test1.
Goal exists x : nat, x = 0.
- refine (let y := 0 + 0 in ex_intro _ (y + y) _).
+ refine (let y := 0 + 0 in ex_intro _ (y + y) _).
auto.
Save test2.
@@ -79,7 +79,7 @@ Abort.
(* Used to failed with error not clean *)
Definition div :
- forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) ->
+ forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) ->
forall n:nat, {q:nat | x = q*n}.
refine
(fun m div_rec n =>
@@ -94,7 +94,7 @@ Abort.
Goal
forall f : forall a (H:a=a), Prop,
- (forall a (H:a = a :> nat), f a H -> True /\ True) ->
+ (forall a (H:a = a :> nat), f a H -> True /\ True) ->
True.
intros.
refine (@proj1 _ _ (H 0 _ _)).
@@ -105,13 +105,13 @@ Abort.
Require Import Peano_dec.
-Definition fact_F :
+Definition fact_F :
forall (n:nat),
(forall m, m<n -> nat) ->
nat.
-refine
+refine
(fun n fact_rec =>
- if eq_nat_dec n 0 then
+ if eq_nat_dec n 0 then
1
else
let fn := fact_rec (n-1) _ in
diff --git a/test-suite/success/replace.v b/test-suite/success/replace.v
index 94b75c7f..0b112937 100644
--- a/test-suite/success/replace.v
+++ b/test-suite/success/replace.v
@@ -5,7 +5,7 @@ Undo.
intros x H H0.
replace x with 0.
Undo.
-replace x with 0 in |- *.
+replace x with 0 in |- *.
Undo.
replace x with 1 in *.
Undo.
@@ -22,3 +22,11 @@ replace x with 0 in H,H0 |- * .
Undo.
Admitted.
+(* This failed at some point when "replace" started to support arguments
+ with evars but "abstract" did not supported any evars even defined ones *)
+
+Class U.
+Lemma l (u : U) (f : U -> nat) (H : 0 = f u) : f u = 0.
+replace (f _) with 0 by abstract apply H.
+reflexivity.
+Qed.
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 86e55922..3bce52fe 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -38,3 +38,73 @@ Goal forall n, 0 + n = n -> True.
intros n H.
rewrite plus_0_l in H.
Abort.
+
+(* Rewrite dependent proofs from left-to-right *)
+
+Lemma l1 :
+ forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
+intros x y H P H0.
+rewrite H.
+rewrite H in H0.
+assumption.
+Qed.
+
+(* Rewrite dependent proofs from right-to-left *)
+
+Lemma l2 :
+ forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
+intros x y H P H0.
+rewrite <- H.
+rewrite <- H in H0.
+assumption.
+Qed.
+
+(* Check rewriting dependent proofs with non-symmetric equalities *)
+
+Lemma l3:forall x (H:eq_true x) (P:forall x, eq_true x -> Type), P x H -> P x H.
+intros x H P H0.
+rewrite H.
+rewrite H in H0.
+assumption.
+Qed.
+
+(* Dependent rewrite *)
+
+Require Import JMeq.
+
+Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True.
+inversion 1; (* Goal is now [JMeq a a -> True] *) dependent rewrite H3.
+Undo.
+intros; inversion H; dependent rewrite H4 in H0.
+Undo.
+intros; inversion H; dependent rewrite <- H4 in H0.
+Abort.
+
+(* Test conversion between terms with evars that both occur in K-redexes and
+ are elsewhere solvable.
+
+ This is quite an artificial example, but it used to work in 8.2.
+
+ Since rewrite supports conversion on terms without metas, it
+ was successively unifying (id 0 ?y) and 0 where ?y was not a
+ meta but, because coming from a "_", an evar.
+
+ After commit r12440 which unified the treatment of metas and
+ evars, it stopped to work. Chung-Kil Hur's Heq package used
+ this feature. Solved in r13...
+*)
+
+Parameter g : nat -> nat -> nat.
+Definition K (x y:nat) := x.
+
+Goal (forall y, g y (K 0 y) = 0) -> g 0 0 = 0.
+intros.
+rewrite (H _).
+reflexivity.
+Qed.
+
+Goal (forall y, g (K 0 y) y = 0) -> g 0 0 = 0.
+intros.
+rewrite (H _).
+reflexivity.
+Qed.
diff --git a/test-suite/success/setoid_ring_module.v b/test-suite/success/setoid_ring_module.v
index e947c6d9..2d9e85b5 100644
--- a/test-suite/success/setoid_ring_module.v
+++ b/test-suite/success/setoid_ring_module.v
@@ -11,11 +11,11 @@ Parameters (Coef:Set)(c0 c1 : Coef)
(ceq_refl : forall x, ceq x x).
-Add Relation Coef ceq
+Add Relation Coef ceq
reflexivity proved by ceq_refl symmetry proved by ceq_sym
transitivity proved by ceq_trans
as ceq_relation.
-
+
Add Morphism cadd with signature ceq ==> ceq ==> ceq as cadd_Morphism.
Admitted.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index be5999df..033b3f48 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -124,7 +124,7 @@ Goal forall
(f : Prop -> Prop)
(Q : (nat -> Prop) -> Prop)
(H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True)
- (h:nat -> Prop),
+ (h:nat -> Prop),
Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True.
intros f0 Q H.
setoid_rewrite H.
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index b89787bb..6baf7970 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -205,7 +205,7 @@ Theorem test6:
rewrite H.
assumption.
Qed.
-
+
Theorem test7:
forall E1 E2 y y', (eqS1 E1 E2) -> (eqS2 y y') ->
(f_test6 (g_test6 (h_test6 E2))) ->
@@ -228,7 +228,7 @@ Add Morphism f_test8 : f_compat_test8. Admitted.
Axiom eqS1_test8': S1_test8 -> S1_test8 -> Prop.
Axiom SetoidS1_test8' : Setoid_Theory S1_test8 eqS1_test8'.
Add Setoid S1_test8 eqS1_test8' SetoidS1_test8' as S1_test8setoid'.
-
+
(*CSC: for test8 to be significant I want to choose the setoid
(S1_test8, eqS1_test8'). However this does not happen and
there is still no syntax for it ;-( *)
diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v
index ead93d91..381cda2c 100644
--- a/test-suite/success/setoid_test_function_space.v
+++ b/test-suite/success/setoid_test_function_space.v
@@ -9,11 +9,11 @@ Hint Unfold feq.
Lemma feq_refl: forall f, f =f f.
intuition.
Qed.
-
+
Lemma feq_sym: forall f g, f =f g-> g =f f.
intuition.
Qed.
-
+
Lemma feq_trans: forall f g h, f =f g-> g =f h -> f =f h.
unfold feq. intuition.
rewrite H.
@@ -22,7 +22,7 @@ Qed.
End feq.
Infix "=f":= feq (at level 80, right associativity).
Hint Unfold feq. Hint Resolve feq_refl feq_sym feq_trans.
-
+
Variable K:(nat -> nat)->Prop.
Variable K_ext:forall a b, (K a)->(a =f b)->(K b).
@@ -30,7 +30,7 @@ Add Parametric Relation (A B : Type) : (A -> B) (@feq A B)
reflexivity proved by (@feq_refl A B)
symmetry proved by (@feq_sym A B)
transitivity proved by (@feq_trans A B) as funsetoid.
-
+
Add Morphism K with signature (@feq nat nat) ==> iff as K_ext1.
intuition. apply (K_ext H0 H).
intuition. assert (y =f x);auto. apply (K_ext H0 H1).
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index b4de4932..271e6ef7 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -2,12 +2,12 @@
(* (cf bug #1031) *)
Inductive tree : Set :=
-| node : nat -> forest -> tree
+| node : nat -> forest -> tree
with forest : Set :=
-| leaf : forest
-| cons : tree -> forest -> forest
+| leaf : forest
+| cons : tree -> forest -> forest
.
-Definition copy_of_compute_size_forest :=
+Definition copy_of_compute_size_forest :=
fix copy_of_compute_size_forest (f:forest) : nat :=
match f with
| leaf => 1
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 4929ae4c..57837321 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -2,7 +2,7 @@
Goal forall a b c : nat, a = b -> b = c -> forall d, a+d=c+d.
intros.
-(* "compatibility" mode: specializing a global name
+(* "compatibility" mode: specializing a global name
means a kind of generalize *)
specialize trans_equal. intros _.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 35910011..0a1d4657 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -8,7 +8,7 @@
(* Test le Hint Unfold sur des var locales *)
Section toto.
-Let EQ := eq.
+Let EQ := @eq.
Goal EQ nat 0 0.
Hint Unfold EQ.
auto.
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 91ee18ea..ddf122e8 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -1,15 +1,15 @@
(* Test patterns unification *)
-Lemma l1 : (forall P, (exists x:nat, P x) -> False)
+Lemma l1 : (forall P, (exists x:nat, P x) -> False)
-> forall P, (exists x:nat, P x /\ P x) -> False.
Proof.
intros; apply (H _ H0).
Qed.
Lemma l2 : forall A:Set, forall Q:A->Set,
- (forall (P: forall x:A, Q x -> Prop),
- (exists x:A, exists y:Q x, P x y) -> False)
- -> forall (P: forall x:A, Q x -> Prop),
+ (forall (P: forall x:A, Q x -> Prop),
+ (exists x:A, exists y:Q x, P x y) -> False)
+ -> forall (P: forall x:A, Q x -> Prop),
(exists x:A, exists y:Q x, P x y /\ P x y) -> False.
Proof.
intros; apply (H _ H0).
@@ -43,7 +43,7 @@ Check (fun _h1 => (zenon_notall nat _ (fun _T_0 =>
Note that the example originally came from a non re-typable
pretty-printed term (the checked term is actually re-printed the
- same form it is checked).
+ same form it is checked).
*)
Set Implicit Arguments.
@@ -73,10 +73,10 @@ Qed.
(* Test unification modulo eta-expansion (if possible) *)
-(* In this example, two instances for ?P (argument of hypothesis H) can be
+(* In this example, two instances for ?P (argument of hypothesis H) can be
inferred (one is by unifying the type [Q true] and [?P true] of the
goal and type of [H]; the other is by unifying the argument of [f]);
- we need to unify both instances up to allowed eta-expansions of the
+ we need to unify both instances up to allowed eta-expansions of the
instances (eta is allowed if the meta was applied to arguments)
This used to fail before revision 9389 in trunk
@@ -92,7 +92,7 @@ Qed.
(* Test instanciation of evars by unification *)
-Goal (forall x, 0 * x = 0 -> True) -> True.
+Goal (forall x, 0 + x = 0 -> True) -> True.
intros; eapply H.
rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
Abort.
@@ -126,3 +126,13 @@ intros.
exists (fun n => match n with O => a | S n' => f' n' end).
constructor.
Qed.
+
+(* Check use of types in unification (see Andrej Bauer's mail on
+ coq-club, June 1 2009; it did not work in 8.2, probably started to
+ work after Sozeau improved support for the use of types in unification) *)
+
+Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) ->
+ forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f.
+Proof.
+ intros.
+ rewrite H.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 3c2c0883..469cbeb7 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -29,9 +29,9 @@ Inductive dep_eq : forall X : Type, X -> X -> Prop :=
forall (A : Type) (B : A -> Type),
let T := forall x : A, B x in
forall (f g : T) (x : A), dep_eq (B x) (f x) (g x) -> dep_eq T f g.
-
+
Require Import Relations.
-
+
Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X).
Proof.
unfold transitive in |- *.
@@ -51,7 +51,7 @@ Abort.
Especially, universe refreshing was not done for "set/pose" *)
-Lemma ind_unsec : forall Q : nat -> Type, True.
+Lemma ind_unsec : forall Q : nat -> Type, True.
intro.
set (C := forall m, Q m -> Q m).
exact I.