summaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/AdvancedCanonicalStructure.v18
-rw-r--r--test-suite/success/CaseAlias.v70
-rw-r--r--test-suite/success/Cases.v83
-rw-r--r--test-suite/success/CasesDep.v54
-rw-r--r--test-suite/success/Check.v2
-rw-r--r--test-suite/success/Discriminate.v6
-rw-r--r--test-suite/success/Field.v4
-rw-r--r--test-suite/success/Hints.v2
-rw-r--r--test-suite/success/Inductive.v29
-rw-r--r--test-suite/success/Inversion.v15
-rw-r--r--test-suite/success/LegacyField.v4
-rw-r--r--test-suite/success/Notations.v27
-rw-r--r--test-suite/success/Nsatz.v574
-rw-r--r--test-suite/success/PCase.v66
-rw-r--r--test-suite/success/PrintSortedUniverses.v2
-rw-r--r--test-suite/success/ProgramWf.v6
-rw-r--r--test-suite/success/RecTutorial.v98
-rw-r--r--test-suite/success/Scheme.v4
-rw-r--r--test-suite/success/Tauto.v4
-rw-r--r--test-suite/success/TestRefine.v2
-rw-r--r--test-suite/success/apply.v34
-rw-r--r--test-suite/success/auto.v26
-rw-r--r--test-suite/success/autorewrite.v (renamed from test-suite/success/autorewritein.v)6
-rw-r--r--test-suite/success/bullet.v5
-rw-r--r--test-suite/success/change.v8
-rw-r--r--test-suite/success/coercions.v8
-rw-r--r--test-suite/success/conv_pbs.v5
-rw-r--r--test-suite/success/destruct.v19
-rw-r--r--test-suite/success/eauto.v2
-rw-r--r--test-suite/success/eqdecide.v9
-rw-r--r--test-suite/success/eta.v19
-rw-r--r--test-suite/success/evars.v71
-rw-r--r--test-suite/success/extraction.v4
-rw-r--r--test-suite/success/fix.v5
-rw-r--r--test-suite/success/implicit.v17
-rw-r--r--test-suite/success/inds_type_sec.v2
-rw-r--r--test-suite/success/induct.v25
-rw-r--r--test-suite/success/ltac.v27
-rw-r--r--test-suite/success/mutual_ind.v2
-rw-r--r--test-suite/success/polymorphism.v2
-rw-r--r--test-suite/success/proof_using.v61
-rw-r--r--test-suite/success/remember.v8
-rw-r--r--test-suite/success/rewrite.v21
-rw-r--r--test-suite/success/searchabout.v60
-rw-r--r--test-suite/success/setoid_test.v35
-rw-r--r--test-suite/success/simpl_tuning.v149
-rw-r--r--test-suite/success/telescope_canonical.v12
-rw-r--r--test-suite/success/unfold.v2
-rw-r--r--test-suite/success/unification.v50
-rw-r--r--test-suite/success/universes-coercion.v22
50 files changed, 1493 insertions, 293 deletions
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index b533db6e..97cf316c 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -79,19 +79,17 @@ Record interp_pair :Type :=
link: abs = interp repr }.
Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) .
-proof.
-let a:interp_pair,b:interp_pair.
-reconsider thesis as (a * b = interp a * interp b).
-thus thesis by (link a),(link b).
-end proof.
+Proof.
+intros a b.
+change (a * b = interp a * interp b).
+rewrite (link a), (link b); reflexivity.
Qed.
Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b).
-proof.
-let a:interp_pair,b:interp_pair.
-reconsider thesis as ((a -> b) = (interp a -> interp b)).
-thus thesis using rewrite (link a);rewrite (link b);reflexivity.
-end proof.
+Proof.
+intros a b.
+change ((a -> b) = (interp a -> interp b)).
+rewrite (link a), (link b); reflexivity.
Qed.
Canonical Structure ProdCan (a b:interp_pair) :=
diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v
index 32d85779..a9249086 100644
--- a/test-suite/success/CaseAlias.v
+++ b/test-suite/success/CaseAlias.v
@@ -1,3 +1,4 @@
+(*********************************************)
(* This has been a bug reported by Y. Bertot *)
Inductive expr : Set :=
| b : expr -> expr -> expr
@@ -19,3 +20,72 @@ Fixpoint f2 (t : expr) : expr :=
| x => b x a
end.
+(*********************************************)
+(* Test expansion of aliases *)
+(* Originally taken from NMake_gen.v *)
+
+ Local Notation SizePlus n := (S (S (S (S (S (S n)))))).
+ Local Notation Size := (SizePlus O).
+
+ Parameter zn2z : Type -> Type.
+ Parameter w0 : Type.
+ Fixpoint word (w : Type) (n : nat) {struct n} : Type :=
+ match n with
+ | 0 => w
+ | S n0 => zn2z (word w n0)
+ end.
+
+ Definition w1 := zn2z w0.
+ Definition w2 := zn2z w1.
+ Definition w3 := zn2z w2.
+ Definition w4 := zn2z w3.
+ Definition w5 := zn2z w4.
+ Definition w6 := zn2z w5.
+
+ Definition dom_t n := match n with
+ | 0 => w0
+ | 1 => w1
+ | 2 => w2
+ | 3 => w3
+ | 4 => w4
+ | 5 => w5
+ | 6 => w6
+ | SizePlus n => word w6 n
+ end.
+Parameter plus_t : forall n m : nat, word (dom_t n) m -> dom_t (m + n).
+
+(* This used to fail because of a bug in expansion of SizePlus wrongly
+ reusing n as an alias for the subpattern *)
+Definition plus_t1 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+ match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+ | SizePlus (S n') as n => plus_t n
+ | _ as n =>
+ fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+ | SizePlus (S (S m')) as m => plus_t n m
+ | _ => fun x => x
+ end
+ end.
+
+(* Test (useless) intermediate alias *)
+Definition plus_t2 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+ match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+ | S (S (S (S (S (S (S n'))))) as n) as n'' => plus_t n''
+ | _ as n =>
+ fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+ | SizePlus (S (S m')) as m => plus_t n m
+ | _ => fun x => x
+ end
+ end.
+
+(*****************************************************************************)
+(* Check that alias expansion behaves consistently from versions to versions *)
+
+Definition g m :=
+ match pred m with
+ | 0 => 0
+ | n => n (* For compatibility, right-hand side should be (S n), not (pred m) *)
+ end.
+
+Goal forall m, g m = match pred m with 0 => 0 | S n => S n end.
+intro; reflexivity.
+Abort.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e63972ce..745529bf 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -543,7 +543,7 @@ Type
end).
(* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe
- * it has to synthtize the predicate on O (which he can't)
+ * it has to synthesize the predicate on O (which he can't)
*)
Type
match 0 as n return match n with
@@ -611,31 +611,52 @@ Type
| Consn n a (Consn m b l) => n + m
end).
-(*
-Type [A:Set][n:nat][l:(Listn A n)]
- <[_: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
- (Niln as b) => b
- | (Consn n a (Niln as b))=> (Niln A)
- | (Consn n a (Consn m b l)) => (Niln A)
- end.
+(* This example was deactivated in Cristina's code
+
+Type
+ (fun (A:Set) (n:nat) (l:Listn A n) =>
+ match l return Listn A O with
+ | Niln as b => b
+ | Consn n a (Niln as b) => (Niln A)
+ | Consn n a (Consn m b l) => (Niln A)
+ end).
+*)
+
+(* This one is (still) failing: too weak unification
+
+Type
+ (fun (A:Set) (n:nat) (l:Listn A n) =>
+ match l with
+ | Niln as b => b
+ | Consn n a (Niln as b) => (Niln A)
+ | Consn n a (Consn m b l) => (Niln A)
+ end).
+*)
+
+(* This one is failing: alias L not chosen of the right type
+
+Type
+ (fun (A:Set) (n:nat) (l:Listn A n) =>
+ match l return Listn A (S 0) with
+ | Niln as b => Consn A O O b
+ | Consn n a Niln as L => L
+ | Consn n a _ => Consn A O O (Niln A)
+ end).
*)
-(******** This example rises an error unconstrained_variables!
-Type [A:Set][n:nat][l:(Listn A n)]
- Cases l of
- (Niln as b) => (Consn A O O b)
- | ((Consn n a Niln) as L) => L
- | (Consn n a _) => (Consn A O O (Niln A))
- end.
+
+(******** This example (still) failed
+
+Type
+ (fun (A:Set) (n:nat) (l:Listn A n) =>
+ match l return Listn A (S 0) with
+ | Niln as b => Consn A O O b
+ | Consn n a Niln as L => L
+ | Consn n a _ => Consn A O O (Niln A)
+ end).
+
**********)
-(* To test tratement of as-patterns in depth *)
+(* To test treatment of as-patterns in depth *)
Type
(fun (A : Set) (l : List A) =>
match l with
@@ -1064,7 +1085,7 @@ Type
| Consn n a (Consn m b l) => fun _ : nat => n + m
end).
-(* Alsos tests for multiple _ patterns *)
+(* Also tests for multiple _ patterns *)
Type
(fun (A : Set) (n : nat) (l : Listn A n) =>
match l in (Listn _ n) return (Listn A n) with
@@ -1072,14 +1093,14 @@ Type
| Consn _ _ _ as b => b
end).
-(** Horrible error message!
+(** This one was said to raised once an "Horrible error message!" *)
-Type [A:Set][n:nat][l:(Listn A n)]
- Cases l of
- (Niln as b) => b
- | ((Consn _ _ _ ) as b)=> b
- end.
-******)
+Type
+ (fun (A:Set) (n:nat) (l:Listn A n) =>
+ match l with
+ | Niln as b => b
+ | Consn _ _ _ as b => b
+ end).
Type
match niln in (listn n) return (listn n) with
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 29721843..d3b7cf3f 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -26,6 +26,40 @@ Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C :=
end.
End Folding.
+(** Testing post-processing of nested dependencies *)
+
+Check fun x:{x|x=0}*nat+nat => match x with
+ | inl ((exist 0 eq_refl),0) => None
+ | _ => Some 0
+ end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+ | inl (exist (exist 0 eq_refl) I) => None
+ | _ => Some 0
+ end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+ | inl (exist (exist 0 eq_refl) I) => None
+ | _ => Some 0
+ end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with
+ | inl (exist (exist 0 eq_refl) I) => None
+ | _ => Some 0
+ end.
+
+ (* the next two examples were failing from r14703 (Nov 22 2011) to r14732 *)
+ (* due to a bug in dependencies postprocessing (revealed by CoLoR) *)
+
+Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with
+ | exist2 (x,y) eq_refl I => None
+ end.
+
+Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with
+ | inl (exist (exist2 (x,y) eq_refl I) I) => None
+ | _ => Some 0
+ end.
+
(* -------------------------------------------------------------------- *)
(* Example to test patterns matching on dependent families *)
(* This exemple extracted from the developement done by Nacira Chabane *)
@@ -506,3 +540,23 @@ Definition test (s:step E E) :=
| Step nil _ (cons E nil) _ Plus l l' => true
| _ => false
end.
+
+(* Testing regression of bug 2454 ("get" used not be type-checkable when
+ defined with its type constraint) *)
+
+Inductive K : nat -> Type := KC : forall (p q:nat), K p.
+
+Definition get : K O -> nat := fun x => match x with KC p q => q end.
+
+(* Checking correct order of substitution of realargs *)
+(* (was broken from revision 14664 to 14669) *)
+(* Example extracted from contrib CoLoR *)
+
+Inductive EQ : nat -> nat -> Prop := R x y : EQ x y.
+
+Check fun e t (d1 d2:EQ e t) =>
+ match d1 in EQ e1 t1, d2 in EQ e2 t2 return
+ (e1,t1) = (e2,t2) -> (e1,t1) = (e,t) -> 0=0
+ with
+ | R _ _, R _ _ => fun _ _ => eq_refl
+ end.
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index d5b94ab4..47180ef6 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index dffad323..a7596741 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -32,3 +32,9 @@ intros.
ediscriminate (H O).
instantiate (1:=O).
Abort.
+
+(* Check discriminate on identity *)
+
+Goal ~ identity 0 1.
+discriminate.
+Qed.
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index 08e8aed2..0efd90a1 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(**** Tests of Field with real numbers ****)
Require Import Reals RealField.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 4aa00e68..a93f8900 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -24,7 +24,7 @@ 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. exact refl_equal. Defined.
+ Proof. exact @refl_equal. Defined.
Definition Sym := sym_equal.
Let Trans := trans_equal.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 203fbbb7..da5dd5e4 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -54,6 +54,15 @@ Check
| Build_B x0 x1 => f x0 x1
end).
+(* Check inductive types with local definitions (constructors) *)
+
+Inductive I1 : Set := C1 (_:I1) (_:=0).
+
+Check (fun x:I1 =>
+ match x with
+ | C1 i n => (i,n)
+ end).
+
(* Check implicit parameters of inductive types (submitted by Pierre
Casteran and also implicit in #338) *)
@@ -78,3 +87,23 @@ Record P:Type := {PA:Set; PB:Set}.
Definition F (p:P) := (PA p) -> (PB p).
Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F.
+
+(* Check that test for binders capturing implicit arguments is not stronger
+ than needed (problem raised by Cedric Auger) *)
+
+Set Implicit Arguments.
+Inductive bool_comp2 (b: bool): bool -> Prop :=
+| Opp2: forall q, (match b return Prop with
+ | true => match q return Prop with
+ true => False |
+ false => True end
+ | false => match q return Prop with
+ true => True |
+ false => False end end) -> bool_comp2 b q.
+
+(* This one is still to be made acceptable...
+
+Set Implicit Arguments.
+Inductive I A : A->Prop := C a : (forall A, A) -> I a.
+
+ *)
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 5091b44c..b068f729 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -73,15 +73,15 @@ Require Import Bvector.
Inductive I : nat -> Set :=
| C1 : I 1
- | C2 : forall k i : nat, vector (I i) k -> I i.
+ | C2 : forall k i : nat, Vector.t (I i) k -> I i.
-Inductive SI : forall k : nat, I k -> vector nat k -> nat -> Prop :=
+Inductive SI : forall k : nat, I k -> Vector.t nat k -> nat -> Prop :=
SC2 :
- forall (k i vf : nat) (v : vector (I i) k) (xi : vector nat i),
+ forall (k i vf : nat) (v : Vector.t (I i) k) (xi : Vector.t nat i),
SI (C2 v) xi vf.
Theorem SUnique :
- forall (k : nat) (f : I k) (c : vector nat k) v v',
+ forall (k : nat) (f : I k) (c : Vector.t nat k) v v',
SI f c v -> SI f c v' -> v = v'.
Proof.
induction 1.
@@ -129,3 +129,10 @@ Proof.
an inconsistent state that disturbed "inversion" *)
intros. inversion H.
Abort.
+
+(* Bug #2314 (simplified): check that errors do not show as anomalies *)
+
+Goal True -> True.
+intro.
+Fail inversion H using False.
+Fail inversion foo using True_ind.
diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v
index 53bcc63a..df4da431 100644
--- a/test-suite/success/LegacyField.v
+++ b/test-suite/success/LegacyField.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Field.v 7693 2005-12-21 23:50:17Z herbelin $ *)
-
(**** Tests of Field with real numbers ****)
Require Import Reals LegacyRfield.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 661a8757..f5f5a9d1 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -59,3 +59,30 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end).
Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..).
Check [ 0 ].
Check [ 0 # ; 1 ].
+
+(* Check well-scoping of alpha-renaming of private binders *)
+(* see bug #2248 (thanks to Marc Lasson) *)
+
+Notation "{ q , r | P }" := (fun (p:nat*nat) => let (q, r) := p in P).
+Check (fun p => {q,r| q + r = p}).
+
+(* Check that declarations of empty levels are correctly backtracked *)
+
+Section B.
+Notation "*" := 5 (at level 0) : nat_scope.
+Notation "[ h ] p" := (h + p) (at level 8, p at level 9, h at level 7) : nat_scope.
+End B.
+
+(* Should succeed *)
+Definition n := 5 * 5.
+
+(* Check that lonely notations (here FOO) do not modify the visibility
+ of scoped interpretations (bug #2634 fixed in r14819) *)
+
+Notation "x ++++ y" := (mult x y) (at level 40).
+Notation "x ++++ y" := (plus x y) : A_scope.
+Open Scope A_scope.
+Notation "'FOO' x" := (S x) (at level 40).
+Goal (2 ++++ 3) = 5.
+reflexivity.
+Abort.
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index 518d22e9..d316e4a0 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,51 +1,27 @@
-Require Import Nsatz ZArith Reals List Ring_polynom.
+(* compile en user 3m39.915s sur cachalot *)
+Require Import Nsatz.
(* Example with a generic domain *)
-Variable A: Type.
-Variable Ad: Domain A.
+Section test.
-Definition Ari : Ring A:= (@domain_ring A Ad).
-Existing Instance Ari.
-
-Existing Instance ring_setoid.
-Existing Instance ring_plus_comp.
-Existing Instance ring_mult_comp.
-Existing Instance ring_sub_comp.
-Existing Instance ring_opp_comp.
-
-Add Ring Ar: (@ring_ring A (@domain_ring 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}.
-
-Infix "==" := ring_eq (at level 70, no associativity).
-
-Ltac nsatzA := simpl; unfold Ari; nsatz_domain.
-
-Goal forall x y:A, x == y -> x+0 == y*1+0.
-nsatzA.
-Qed.
+Context {A:Type}`{Aid:Integral_domain A}.
Lemma example3 : forall x y z,
x+y+z==0 ->
x*y+x*z+y*z==0->
- x*y*z==0 -> x*x*x==0.
+ x*y*z==0 -> x^3%Z==0.
Proof.
-Time nsatzA.
-Admitted.
+Time nsatz.
+Qed.
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*x*x*x==0.
+ x*y*z*u==0 -> x^4%Z==0.
Proof.
-Time nsatzA.
+Time nsatz.
Qed.
Lemma example5 : forall x y z u v,
@@ -53,15 +29,17 @@ Lemma example5 : forall x y z u v,
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*x*x*x*x ==0.
+ x*y*z*u*v==0 -> x^5%Z==0.
Proof.
-Time nsatzA.
+Time nsatz.
Qed.
Goal forall x y:Z, x = y -> (x+0)%Z = (y*1+0)%Z.
nsatz.
Qed.
+Require Import Reals.
+
Goal forall x y:R, x = y -> (x+0)%R = (y*1+0)%R.
nsatz.
Qed.
@@ -70,85 +48,17 @@ Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
nsatz.
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.
-Qed.
-
-Lemma example2 : forall x, x^2=0 -> x=0.
-Proof.
- nsatz.
-Qed.
-
-(*
-Notation X := (PEX Z 3).
-Notation Y := (PEX Z 2).
-Notation Z_ := (PEX Z 1).
-*)
-Lemma example3b : 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.
-Qed.
-
-(*
-Notation X := (PEX Z 4).
-Notation Y := (PEX Z 3).
-Notation Z_ := (PEX Z 2).
-Notation U := (PEX Z 1).
-*)
-Lemma example4b : 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.
-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 example5b : 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.
-Qed.
-
-End Examples.
+End test.
Section Geometry.
+(* See the interactive pictures of Laurent Théry
+ on http://www-sop.inria.fr/marelle/CertiGeo/
+ and research paper on
+ https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr
+*)
-Open Scope R_scope.
+Require Import List.
+Require Import Reals.
Record point:Type:={
X:R;
@@ -170,60 +80,122 @@ 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.
+ ((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 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).
+ not (((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0).
Definition middle(A B I:point):=
- 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B).
+ 2%R*(X I)=(X A)+(X B) /\ 2%R*(Y I)=(Y A)+(Y B).
Definition distance2(A B:point):=
- (X B - X A)^2 + (Y B - Y A)^2.
+ (X B - X A)^2%Z + (Y B - Y A)^2%Z.
(* 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.
+ (X B - X A)^2%Z + (Y B - Y A)^2%Z = (X D - X C)^2%Z + (Y D - Y C)^2%Z.
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.
+ ((X A - X O)^2%Z+(Y A - Y O)^2%Z)*((X B - X O)^2%Z+(Y B - Y O)^2%Z).
+
+Definition equaldistance(A B C D:point):=
+ ((X B) - (X A))^2%Z + ((Y B) - (Y A))^2%Z =
+ ((X D) - (X C))^2%Z + ((Y D) - (Y C))^2%Z.
+
+Definition equaltangente(A B C D E F:point):=
+ let s1:= determinant A B C in
+ let c1:= scalarproduct A B C in
+ let s2:= determinant D E F in
+ let c2:= scalarproduct D E F in
+ s1 * c2 = s2 * c1.
+
+Ltac cnf2 f :=
+ match f with
+ | ?A \/ (?B /\ ?C) =>
+ let c1 := cnf2 (A\/B) in
+ let c2 := cnf2 (A\/C) in constr:(c1/\c2)
+ | (?B /\ ?C) \/ ?A =>
+ let c1 := cnf2 (B\/A) in
+ let c2 := cnf2 (C\/A) in constr:(c1/\c2)
+ | (?A \/ ?B) \/ ?C =>
+ let c1 := cnf2 (B\/C) in cnf2 (A \/ c1)
+ | _ => f
+ end
+with cnf f :=
+ match f with
+ | ?A \/ ?B =>
+ let c1 := cnf A in
+ let c2 := cnf B in
+ cnf2 (c1 \/ c2)
+ | ?A /\ ?B =>
+ let c1 := cnf A in
+ let c2 := cnf B in
+ constr:(c1 /\ c2)
+ | _ => f
+ end.
+
+Ltac scnf :=
+ match goal with
+ | |- ?f => let c := cnf f in
+ assert c;[repeat split| tauto]
+ end.
+
+Ltac disj_to_pol f :=
+ match f with
+ | ?a = ?b \/ ?g => let p := disj_to_pol g in constr:((a - b)* p)
+ | ?a = ?b => constr:(a - b)
+ end.
+
+Lemma fastnsatz1:forall x y:R, x - y = 0 -> x = y.
+nsatz.
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 fastnsatz:=
+ try trivial; try apply fastnsatz1; try trivial; nsatz.
+
+Ltac proof_pol_disj :=
+ match goal with
+ | |- ?g => let p := disj_to_pol g in
+ let h := fresh "hp" in
+ assert (h:p = 0);
+ [idtac|
+ prod_disj h p]
+ | _ => idtac
+ end
+with prod_disj h p :=
+ match goal with
+ | |- ?a = ?b \/ ?g =>
+ match p with
+ | ?q * ?p1 =>
+ let h0 := fresh "hp" in
+ let h1 := fresh "hp" in
+ let h2 := fresh "hp" in
+ assert (h0:a - b = 0 \/ p1 = 0);
+ [apply Rmult_integral; exact h|
+ destruct h0 as [h1|h2];
+ [left; fastnsatz|
+ right; prod_disj h2 p1]]
+ end
+ | _ => fastnsatz
+ end.
-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.
+(*
+Goal forall a b c d e f:R, a=b \/ c=d \/ e=f \/ e=a.
+intros. scnf; proof_pol_disj .
+admit.*)
-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_unfold :=
+ unfold collinear, parallel, notparallel, orthogonal,
+ equal2, equal3, nequal2, nequal3,
+ middle, samedistance2,
+ determinant, scalarproduct, norm2, distance2,
+ equaltangente, determinant, scalarproduct, equaldistance.
Ltac geo_rewrite_hyps:=
repeat (match goal with
@@ -231,14 +203,41 @@ Ltac geo_rewrite_hyps:=
| h:Y _ = _ |- _ => rewrite h in *; clear h
end).
+Ltac geo_split_hyps:=
+ repeat (match goal with
+ | h:_ /\ _ |- _ => destruct h
+ end).
+
Ltac geo_begin:=
geo_unfold;
intros;
geo_rewrite_hyps;
- geo_end.
+ geo_split_hyps;
+ scnf; proof_pol_disj.
(* Examples *)
+Lemma medians: forall A B C A1 B1 C1 H:point,
+ middle B C A1 ->
+ middle A C B1 ->
+ middle A B C1 ->
+ collinear A A1 H -> collinear B B1 H ->
+ collinear C C1 H
+ \/ collinear A B C.
+Proof. geo_begin.
+idtac "Medians".
+ Time nsatz.
+(*Finished transaction in 2. secs (2.69359u,0.s)
+*) Qed.
+
+Lemma Pythagore: forall A B C:point,
+ orthogonal A B A C ->
+ distance2 A C + distance2 A B = distance2 B C.
+Proof. geo_begin.
+idtac "Pythagore".
+Time nsatz.
+(*Finished transaction in 0. secs (0.354946u,0.s)
+*) Qed.
Lemma Thales: forall O A B C D:point,
collinear O A C -> collinear O B D ->
@@ -246,9 +245,268 @@ Lemma Thales: forall O A B C D:point,
(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.
+geo_begin.
+idtac "Thales".
+Time nsatz. (*Finished transaction in 2. secs (1.598757u,0.s)*)
+Time nsatz.
+Qed.
+
+Lemma segments_of_chords: forall A B C D M O:point,
+ equaldistance O A O B ->
+ equaldistance O A O C ->
+ equaldistance O A O D ->
+ collinear A B M ->
+ collinear C D M ->
+ (distance2 M A) * (distance2 M B) = (distance2 M C) * (distance2 M D)
+ \/ parallel A B C D.
+Proof.
+geo_begin.
+idtac "segments_of_chords".
+Time nsatz.
+(*Finished transaction in 3. secs (2.704589u,0.s)
+*) Qed.
+
+
+Lemma isoceles: forall A B C:point,
+ equaltangente A B C B C A ->
+ distance2 A B = distance2 A C
+ \/ collinear A B C.
+Proof. geo_begin. Time nsatz.
+(*Finished transaction in 1. secs (1.140827u,0.s)*) Qed.
+
+Lemma minh: forall A B C D O E H I:point,
+ X A = 0 -> Y A = 0 -> Y O = 0 ->
+ equaldistance O A O B ->
+ equaldistance O A O C ->
+ equaldistance O A O D ->
+ orthogonal A C B D ->
+ collinear A C E ->
+ collinear B D E ->
+ collinear A B H ->
+ orthogonal E H A B ->
+ collinear C D I ->
+ middle C D I ->
+ collinear H E I
+ \/ (X C)^2%Z * (X B)^5%Z * (X O)^2%Z
+ * (X C - 2%Z * X O)^3%Z * (-2%Z * X O + X B)=0
+ \/ parallel A C B D.
+Proof. geo_begin.
+idtac "minh".
+Time nsatz with radicalmax :=1%N strategy:=1%Z
+ parameters:=(X O::X B::X C::nil)
+ variables:= (@nil R).
+(*Finished transaction in 13. secs (10.102464u,0.s)
+*)
+Qed.
+
+Lemma Pappus: forall A B C A1 B1 C1 P Q S:point,
+ X A = 0 -> Y A = 0 -> Y B = 0 -> Y C = 0 ->
+ collinear A1 B1 C1 ->
+ collinear A B1 P -> collinear A1 B P ->
+ collinear A C1 Q -> collinear A1 C Q ->
+ collinear B C1 S -> collinear B1 C S ->
+ collinear P Q S
+ \/ (Y A1 - Y B1)^2%Z=0 \/ (X A = X B1)
+ \/ (X A1 = X C) \/ (X C = X B1)
+ \/ parallel A B1 A1 B \/ parallel A C1 A1 C \/ parallel B C1 B1 C.
+Proof.
+geo_begin.
+idtac "Pappus".
+Time nsatz with radicalmax :=1%N strategy:=0%Z
+ parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil)
+ variables:= (X B
+ :: X A1
+ :: Y A1
+ :: X B1
+ :: Y B1
+ :: X C
+ :: Y C1
+ :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil).
+(*Finished transaction in 8. secs (7.795815u,0.000999999999999s)
+*)
+Qed.
+
+Lemma Simson: forall A B C O D E F G:point,
+ X A = 0 -> Y A = 0 ->
+ equaldistance O A O B ->
+ equaldistance O A O C ->
+ equaldistance O A O D ->
+ orthogonal E D B C ->
+ collinear B C E ->
+ orthogonal F D A C ->
+ collinear A C F ->
+ orthogonal G D A B ->
+ collinear A B G ->
+ collinear E F G
+ \/ (X C)^2%Z = 0 \/ (Y C)^2%Z = 0 \/ (X B)^2%Z = 0 \/ (Y B)^2%Z = 0 \/ (Y C - Y B)^2%Z = 0
+ \/ equal3 B A
+ \/ equal3 A C \/ (X C - X B)^2%Z = 0
+ \/ equal3 B C.
+Proof.
+geo_begin.
+idtac "Simson".
+Time nsatz with radicalmax :=1%N strategy:=0%Z
+ parameters:=(X B::Y B::X C::Y C::Y D::nil)
+ variables:= (@nil R). (* compute -[X Y]. *)
+(*Finished transaction in 8. secs (7.550852u,0.s)
+*)
+Qed.
+
+Lemma threepoints: forall A B C A1 B1 A2 B2 H1 H2 H3:point,
+ (* H1 intersection of bisections *)
+ middle B C A1 -> orthogonal H1 A1 B C ->
+ middle A C B1 -> orthogonal H1 B1 A C ->
+ (* H2 intersection of medians *)
+ collinear A A1 H2 -> collinear B B1 H2 ->
+ (* H3 intersection of altitudes *)
+ collinear B C A2 -> orthogonal A A2 B C ->
+ collinear A C B2 -> orthogonal B B2 A C ->
+ collinear A A1 H3 -> collinear B B1 H3 ->
+ collinear H1 H2 H3
+ \/ collinear A B C.
+Proof. geo_begin.
+idtac "threepoints".
+Time nsatz.
+(*Finished transaction in 7. secs (6.282045u,0.s)
+*) Qed.
+
+Lemma Feuerbach: forall A B C A1 B1 C1 O A2 B2 C2 O2:point,
+ forall r r2:R,
+ X A = 0 -> Y A = 0 -> X B = 1 -> Y B = 0->
+ middle A B C1 -> middle B C A1 -> middle C A B1 ->
+ distance2 O A1 = distance2 O B1 ->
+ distance2 O A1 = distance2 O C1 ->
+ collinear A B C2 -> orthogonal A B O2 C2 ->
+ collinear B C A2 -> orthogonal B C O2 A2 ->
+ collinear A C B2 -> orthogonal A C O2 B2 ->
+ distance2 O2 A2 = distance2 O2 B2 ->
+ distance2 O2 A2 = distance2 O2 C2 ->
+ r^2%Z = distance2 O A1 ->
+ r2^2%Z = distance2 O2 A2 ->
+ distance2 O O2 = (r + r2)^2%Z
+ \/ distance2 O O2 = (r - r2)^2%Z
+ \/ collinear A B C.
+Proof. geo_begin.
+idtac "Feuerbach".
+Time nsatz.
+(*Finished transaction in 21. secs (19.021109u,0.s)*)
+Qed.
+
+
+
+
+Lemma Euler_circle: forall A B C A1 B1 C1 A2 B2 C2 O:point,
+ middle A B C1 -> middle B C A1 -> middle C A B1 ->
+ orthogonal A B C C2 -> collinear A B C2 ->
+ orthogonal B C A A2 -> collinear B C A2 ->
+ orthogonal A C B B2 -> collinear A C B2 ->
+ distance2 O A1 = distance2 O B1 ->
+ distance2 O A1 = distance2 O C1 ->
+ (distance2 O A2 = distance2 O A1
+ /\distance2 O B2 = distance2 O A1
+ /\distance2 O C2 = distance2 O A1)
+ \/ collinear A B C.
+Proof. geo_begin.
+idtac "Euler_circle 3 goals".
+Time nsatz.
+(*Finished transaction in 13. secs (11.208296u,0.124981s)*)
+Time nsatz.
+(*Finished transaction in 10. secs (8.846655u,0.s)*)
+Time nsatz.
+(*Finished transaction in 11. secs (9.186603u,0.s)*)
+Qed.
+
+
+
+Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point,
+ X S = 0 -> Y S = 0 -> Y A = 0 ->
+ collinear A S A1 -> collinear B S B1 -> collinear C S C1 ->
+ collinear B1 C1 P -> collinear B C P ->
+ collinear A1 C1 Q -> collinear A C Q ->
+ collinear A1 B1 R -> collinear A B R ->
+ collinear P Q R
+ \/ X A = X B \/ X A = X C \/ X B = X C \/ X A = 0 \/ Y B = 0 \/ Y C = 0
+ \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1.
+Proof.
+geo_begin.
+idtac "Desargues".
+Time
+let lv := rev (X A
+ :: X B
+ :: Y B
+ :: X C
+ :: Y C
+ :: Y A1 :: X A1
+ :: Y B1
+ :: Y C1
+ :: X R
+ :: Y R
+ :: X Q
+ :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in
+nsatz with radicalmax :=1%N strategy:=0%Z
+ parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil)
+ variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*)
+Qed.
+
+Lemma chords: forall O A B C D M:point,
+ equaldistance O A O B ->
+ equaldistance O A O C ->
+ equaldistance O A O D ->
+ collinear A B M -> collinear C D M ->
+ scalarproduct A M B = scalarproduct C M D
+ \/ parallel A B C D.
+Proof. geo_begin.
+idtac "chords".
+ Time nsatz.
+(*Finished transaction in 4. secs (3.959398u,0.s)*)
+Qed.
+
+Lemma Ceva: forall A B C D E F M:point,
+ collinear M A D -> collinear M B E -> collinear M C F ->
+ collinear B C D -> collinear E A C -> collinear F A B ->
+ (distance2 D B) * (distance2 E C) * (distance2 F A) =
+ (distance2 D C) * (distance2 E A) * (distance2 F B)
+ \/ collinear A B C.
+Proof. geo_begin.
+idtac "Ceva".
Time nsatz.
+(*Finished transaction in 105. secs (104.121171u,0.474928s)*)
+Qed.
+
+Lemma bissectrices: forall A B C M:point,
+ equaltangente C A M M A B ->
+ equaltangente A B M M B C ->
+ equaltangente B C M M C A
+ \/ equal3 A B.
+Proof. geo_begin.
+idtac "bissectrices".
Time nsatz.
+(*Finished transaction in 2. secs (1.937705u,0.s)*)
+Qed.
+
+Lemma bisections: forall A B C A1 B1 C1 H:point,
+ middle B C A1 -> orthogonal H A1 B C ->
+ middle A C B1 -> orthogonal H B1 A C ->
+ middle A B C1 ->
+ orthogonal H C1 A B
+ \/ collinear A B C.
+Proof. geo_begin.
+idtac "bisections".
+Time nsatz. (*Finished transaction in 2. secs (2.024692u,0.002s)*)
+Qed.
+
+Lemma altitudes: 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
+ \/ equal2 A B
+ \/ collinear A B C.
+Proof. geo_begin.
+idtac "altitudes".
+Time nsatz. (*Finished transaction in 3. secs (3.001544u,0.s)*)
+Time nsatz. (*Finished transaction in 4. secs (3.113527u,0.s)*)
Qed.
Lemma hauteurs:forall A B C A1 B1 C1 H:point,
@@ -261,26 +519,16 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point,
\/ 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! *)
+idtac "hauteurs".
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 :: (@Datatypes.nil R)) in
- nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi;
- discrR.
-(* Finished transaction in 6. secs (5.579152u,0.001s) *)
+ :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C
+ :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
+nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R)
+ variables := lv.
+(*Finished transaction in 5. secs (4.360337u,0.008999s)*)
Qed.
+
End Geometry.
diff --git a/test-suite/success/PCase.v b/test-suite/success/PCase.v
new file mode 100644
index 00000000..67d680ba
--- /dev/null
+++ b/test-suite/success/PCase.v
@@ -0,0 +1,66 @@
+
+(** Some tests of patterns containing matchs ending with joker branches.
+ Cf. the new form of the [constr_pattern] constructor [PCase]
+ in [pretyping/pattern.ml] *)
+
+(* A universal match matcher *)
+
+Ltac kill_match :=
+ match goal with
+ |- context [ match ?x with _ => _ end ] => destruct x
+ end.
+
+(* A match matcher restricted to a given type : nat *)
+
+Ltac kill_match_nat :=
+ match goal with
+ |- context [ match ?x in nat with _ => _ end ] => destruct x
+ end.
+
+(* Another way to restrict to a given type : give a branch *)
+
+Ltac kill_match_nat2 :=
+ match goal with
+ |- context [ match ?x with S _ => _ | _ => _ end ] => destruct x
+ end.
+
+(* This should act only on empty match *)
+
+Ltac kill_match_empty :=
+ match goal with
+ |- context [ match ?x with end ] => destruct x
+ end.
+
+Lemma test1 (b:bool) : if b then True else O=O.
+Proof.
+ Fail kill_match_nat.
+ Fail kill_match_nat2.
+ Fail kill_match_empty.
+ kill_match. exact I. exact eq_refl.
+Qed.
+
+Lemma test2a (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ Fail kill_match_empty.
+ kill_match_nat. exact I. exact eq_refl.
+Qed.
+
+Lemma test2b (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ kill_match_nat2. exact I. exact eq_refl.
+Qed.
+
+Lemma test2c (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ kill_match. exact I. exact eq_refl.
+Qed.
+
+Lemma test3a (f:False) : match f return Prop with end.
+Proof.
+ kill_match_empty.
+Qed.
+
+Lemma test3b (f:False) : match f return Prop with end.
+Proof.
+ kill_match.
+Qed.
diff --git a/test-suite/success/PrintSortedUniverses.v b/test-suite/success/PrintSortedUniverses.v
new file mode 100644
index 00000000..81326580
--- /dev/null
+++ b/test-suite/success/PrintSortedUniverses.v
@@ -0,0 +1,2 @@
+Require Reals.
+Print Sorted Universes.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 81bdbc29..00a13aed 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -1,3 +1,9 @@
+(* Before loading Program, check non-anomaly on missing library Program *)
+
+Fail Program Definition f n (e:n=n): {n|n=0} := match n,e with 0, refl => 0 | _, _ => 0 end.
+
+(* Then we test Program properly speaking *)
+
Require Import Arith Program.
Require Import ZArith Zwf.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d4e6a82e..2602c7e3 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -55,13 +55,13 @@ Check (cons 3 (cons 2 nil)).
Require Import Bvector.
-Print vector.
+Print Vector.t.
-Check (Vnil nat).
+Check (Vector.nil nat).
-Check (fun (A:Set)(a:A)=> Vcons _ a _ (Vnil _)).
+Check (fun (A:Set)(a:A)=> Vector.cons _ a _ (Vector.nil _)).
-Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))).
@@ -315,16 +315,16 @@ Proof.
Qed.
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
-| Vcons _ n0 v0 => v0
+ (A : Set) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):=
+match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with
+| Vector.nil => Vector.nil A
+| Vector.cons _ n0 v0 => v0
end.
-Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
+Definition Vtail' (A:Set)(n:nat)(v:Vector.t A n) : Vector.t A (pred n).
case v.
simpl.
- exact (Vnil A).
+ exact (Vector.nil A).
simpl.
auto.
Defined.
@@ -543,7 +543,7 @@ Inductive ex_Set (P : Set -> Prop) : Type :=
Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
-Goal (comes_from_the_left _ _ (or_introl True I)).
+Goal (comes_from_the_left _ _ (or_introl True I)).
split.
Qed.
@@ -966,37 +966,37 @@ let rec div_aux x y =
| Right -> div_aux (minus x y) y)
*)
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
Proof.
intros A v;inversion v.
Abort.
(*
- Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
+ Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
n= 0 -> v = Vnil A.
Toplevel input, characters 40281-40287
-> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A.
+> Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vnil A.
> ^^^^^^
Error: In environment
A : Set
n : nat
-v : vector A n
+v : Vector.t A n
e : n = 0
-The term "Vnil A" has type "vector A 0" while it is expected to have type
- "vector A n"
+The term "Vnil A" has type "Vector.t A 0" while it is expected to have type
+ "Vector.t A n"
*)
Require Import JMeq.
-Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
- n= 0 -> JMeq v (Vnil A).
+Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
+ n= 0 -> JMeq v (Vector.nil A).
Proof.
destruct v.
auto.
intro; discriminate.
Qed.
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
Proof.
intros a v;apply JMeq_eq.
apply vector0_is_vnil_aux.
@@ -1004,56 +1004,56 @@ Proof.
Qed.
-Implicit Arguments Vcons [A n].
-Implicit Arguments Vnil [A].
-Implicit Arguments Vhead [A n].
-Implicit Arguments Vtail [A n].
+Implicit Arguments Vector.cons [A n].
+Implicit Arguments Vector.nil [A].
+Implicit Arguments Vector.hd [A n].
+Implicit Arguments Vector.tl [A n].
-Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
Proof.
destruct n; intro v.
- exact Vnil.
- exact (Vcons (Vhead v) (Vtail v)).
+ exact Vector.nil.
+ exact (Vector.cons (Vector.hd v) (Vector.tl v)).
Defined.
-Eval simpl in (fun (A:Set)(v:vector A 0) => (Vid _ _ v)).
+Eval simpl in (fun (A:Set)(v:Vector.t A 0) => (Vid _ _ v)).
-Eval simpl in (fun (A:Set)(v:vector A 0) => v).
+Eval simpl in (fun (A:Set)(v:Vector.t A 0) => v).
-Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v).
Proof.
destruct v.
reflexivity.
reflexivity.
Defined.
-Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
+Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil.
Proof.
intros.
- change (Vnil (A:=A)) with (Vid _ 0 v).
+ change (Vector.nil (A:=A)) with (Vid _ 0 v).
apply Vid_eq.
Defined.
Theorem decomp :
- forall (A : Set) (n : nat) (v : vector A (S n)),
- v = Vcons (Vhead v) (Vtail v).
+ forall (A : Set) (n : nat) (v : Vector.t A (S n)),
+ v = Vector.cons (Vector.hd v) (Vector.tl v).
Proof.
intros.
- change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
+ change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _ (S n) v).
apply Vid_eq.
Defined.
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 ->
- P (S n) (Vcons a v1) (Vcons b v2)) ->
- forall n (v1 v2 : vector A n), P n v1 v2.
+ forall (A:Set) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type),
+ P 0 Vector.nil Vector.nil ->
+ (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 ->
+ P (S n) (Vector.cons a v1) (Vector.cons b v2)) ->
+ forall n (v1 v2 : Vector.t A n), P n v1 v2.
induction n.
intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
auto.
@@ -1063,24 +1063,24 @@ Defined.
Require Import Bool.
-Definition bitwise_or n v1 v2 : vector bool n :=
- vector_double_rect bool (fun n v1 v2 => vector bool n)
- Vnil
- (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
+Definition bitwise_or n v1 v2 : Vector.t bool n :=
+ vector_double_rect bool (fun n v1 v2 => Vector.t bool n)
+ Vector.nil
+ (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2.
-Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:vector A p){struct v}
+Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v}
: option A :=
match n,v with
- _ , Vnil => None
- | 0 , Vcons b _ _ => Some b
- | S n', Vcons _ p' v' => vector_nth A n' p' v'
+ _ , Vector.nil => None
+ | 0 , Vector.cons b _ _ => Some b
+ | S n', Vector.cons _ p' v' => vector_nth A n' p' v'
end.
Implicit Arguments vector_nth [A p].
-Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b,
+Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b,
vector_nth i v1 = Some a ->
vector_nth i v2 = Some b ->
vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
new file mode 100644
index 00000000..dd5aa81d
--- /dev/null
+++ b/test-suite/success/Scheme.v
@@ -0,0 +1,4 @@
+(* This failed in 8.3pl2 *)
+
+Scheme Induction for eq Sort Prop.
+Check eq_ind_dep.
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 324d340a..c4e67677 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Tauto.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
(**** Tactics Tauto and Intuition ****)
(**** Tauto:
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 6cc443bb..705bdc45 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index a6f9fa23..e3183ef2 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -202,6 +202,13 @@ try apply H.
unfold ID; apply H0.
Qed.
+(* Test hyp in "apply -> ... in hyp" is correctly instantiated by Ltac *)
+
+Goal (True <-> False) -> True -> False.
+intros Heq H.
+match goal with [ H : True |- _ ] => apply -> Heq in H end.
+Abort.
+
(* Test coercion below product and on non meta-free terms in with bindings *)
(* Cf wishes #1408 from E. Makarov *)
@@ -326,13 +333,12 @@ 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) *)
+(* The following, which was failing badly in bug 1980, is now
+ properly rejected, as descend in conjunctions builds an
+ ill-formed elimination from Prop to Type. *)
Goal True.
-eapply ex_intro.
-instantiate (2:=fun _ :True => True).
-instantiate (1:=I).
+Fail eapply ex_intro.
exact I.
Qed.
@@ -391,3 +397,21 @@ intro x;
apply x.
*)
+
+Section A.
+
+Variable map : forall (T1 T2 : Type) (f : T1 -> T2) (t11 t12 : T1),
+ identity (f t11) (f t12).
+
+Variable mapfuncomp : forall (X Y Z : Type) (f : X -> Y) (g : Y -> Z) (x x' : X),
+ identity (map Y Z g (f x) (f x')) (map X Z (fun x0 : X => g (f x0)) x x').
+
+Goal forall X:Type, forall Y:Type, forall f:X->Y, forall x : X, forall x' : X,
+ forall g : Y -> X,
+ let gf := (fun x : X => g (f x)) : X -> X in
+ identity (map Y X g (f x) (f x')) (map X X gf x x').
+intros.
+apply mapfuncomp.
+Abort.
+
+End A.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
new file mode 100644
index 00000000..9b691e25
--- /dev/null
+++ b/test-suite/success/auto.v
@@ -0,0 +1,26 @@
+(* Wish #2154 by E. van der Weegen *)
+
+(* auto was not using f_equal-style lemmas with metavariables occuring
+ only in the type of an evar of the concl, but not directly in the
+ concl itself *)
+
+Parameters
+ (F: Prop -> Prop)
+ (G: forall T, (T -> Prop) -> Type)
+ (L: forall A (P: A -> Prop), G A P -> forall x, F (P x))
+ (Q: unit -> Prop).
+
+Hint Resolve L.
+
+Goal G unit Q -> F (Q tt).
+ intro.
+ auto.
+Qed.
+
+(* Test implicit arguments in "using" clause *)
+
+Goal forall n:nat, nat * nat.
+auto using (pair O).
+Undo.
+eauto using (pair O).
+Qed.
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewrite.v
index 68f2f7ce..5e9064f8 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewrite.v
@@ -19,5 +19,11 @@ Proof.
apply H;reflexivity.
Qed.
+(* Check autorewrite does not solve existing evars *)
+(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
+Hint Rewrite <- plus_n_O : base1.
+Goal forall y, exists x, y+x = y.
+eexists. autorewrite with base1.
+Fail reflexivity.
diff --git a/test-suite/success/bullet.v b/test-suite/success/bullet.v
new file mode 100644
index 00000000..1099f3e1
--- /dev/null
+++ b/test-suite/success/bullet.v
@@ -0,0 +1,5 @@
+Goal True /\ True.
+split.
+- exact I.
+- exact I.
+Qed.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 5ac6ce82..c65cf303 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -30,3 +30,11 @@ change 3 at 1 with (1+2) in H |- *.
change 3 at 1 with (1+2) in H, H|-.
change 3 in |- * at 1.
*)
+
+(* Test that pretyping checks allowed elimination sorts *)
+
+Goal True.
+Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x).
+Fail change True with
+ match ex_intro _ True (eq_refl True) with ex_intro x _ => x end.
+Abort.
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 908b5f77..001beae7 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -81,3 +81,11 @@ Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
+(* Check that coercions are made visible only when modules are imported *)
+
+Module A.
+ Module B. Coercion b2n (b:bool) := if b then 0 else 1. End B.
+ Fail Check S true.
+End A.
+Import A.
+Fail Check S true.
diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v
index f6ebacae..05d2c98f 100644
--- a/test-suite/success/conv_pbs.v
+++ b/test-suite/success/conv_pbs.v
@@ -221,3 +221,8 @@ with universal_completeness_stoup (Gamma:context)(A:formula){struct A}
(ProofForallL x t (subst_formula (remove_assoc _ x rho) A)
(eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _)))))
end.
+
+
+(* A simple example that raised an uncaught exception at some point *)
+
+Fail Check fun x => @eq_refl x <: true = true.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 8013e1d3..fc40ea96 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -74,3 +74,22 @@ destruct H.
destruct H0.
reflexivity.
Qed.
+
+(* These did not work before 8.4 *)
+
+Goal (exists x, x=0) -> True.
+destruct 1 as (_,_); exact I.
+Abort.
+
+Goal (exists x, x=0 /\ True) -> True.
+destruct 1 as (_,(_,H)); exact H.
+Abort.
+
+Goal (exists x, x=0 /\ True) -> True.
+destruct 1 as (_,(_,x)); exact x.
+Abort.
+
+Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0.
+intros.
+destruct (g _). (* This was failing in at least r14571 *)
+Abort.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 1862ad10..a94d8b1d 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index ff880d00..8c00583e 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -16,12 +16,7 @@ Qed.
Lemma lem2 : forall x y : T, {x = y} + {x <> y}.
intros x y.
- decide equality x y.
-Qed.
-
-Lemma lem3 : forall x y : T, {x = y} + {x <> y}.
-intros x y.
- decide equality y x.
+ decide equality.
Qed.
Lemma lem4 : forall x y : T, {x = y} + {x <> y}.
diff --git a/test-suite/success/eta.v b/test-suite/success/eta.v
new file mode 100644
index 00000000..08078012
--- /dev/null
+++ b/test-suite/success/eta.v
@@ -0,0 +1,19 @@
+(* Kernel test (head term is a constant) *)
+Check (fun a : S = S => a : S = fun x => S x).
+
+(* Kernel test (head term is a variable) *)
+Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => f x).
+
+(* Test type inference (head term is syntactically rigid) *)
+Check (fun (a : list = list) => a : list = fun A => _ A).
+
+(* Test type inference (head term is a variable) *)
+(* This one is still to be done...
+Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => _ x).
+*)
+
+(* Test tactic unification *)
+Goal (forall f:nat->nat, (fun x => f x) = (fun x => f x)) -> S = S.
+intro H; apply H.
+Qed.
+
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 6423ad14..2f1ec757 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -238,3 +238,74 @@ eapply f_equal with (* should fail because ill-typed *)
end) in H
|| injection H.
Abort.
+
+(* A legitimate simple eapply that was failing in coq <= 8.3.
+ Cf. in Unification.w_merge the addition of an extra pose_all_metas_as_evars
+ on 30/9/2010
+*)
+
+Lemma simple_eapply_was_failing :
+ (forall f:nat->nat, exists g, f = g) -> True.
+Proof.
+ assert (modusponens : forall P Q, P -> (P->Q) -> Q) by auto.
+ intros.
+ eapply modusponens.
+ simple eapply H.
+ (* error message with V8.3 :
+ Impossible to unify "?18" with "fun g : nat -> nat => ?6 = g". *)
+Abort.
+
+(* Regression test *)
+
+Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0.
+
+(* This example revealed an incorrect evar restriction at some time
+ around October 2011 *)
+
+Goal forall (A:Type) (a:A) (P:forall A, A -> Prop), (P A a) /\ (P A a).
+intros.
+refine ((fun H => conj (proj1 H) (proj2 H)) _).
+Abort.
+
+(* The argument of e below failed to be inferred from r14219 (Oct 2011) to *)
+(* r14753 after the restrictions made on detecting Miller's pattern in the *)
+(* presence of alias, only the second-order unification procedure was *)
+(* able to solve this problem but it was deactivated for 8.4 in r14219 *)
+
+Definition k0
+ (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+ (j : forall a, exists n : nat, n = a) o :=
+ match o with (* note: match introduces an alias! *)
+ | Some a => e _ (j a)
+ | None => O
+ end.
+
+Definition k1
+ (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+ (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j a).
+
+Definition k2
+ (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+ (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
+
+(* Other examples about aliases involved in pattern unification *)
+
+Definition k3
+ (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+ (j : forall a, exists n : nat, let a' := a in n = a') a (b:=a) := e _ (j b).
+
+Definition k4
+ (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+ (j : forall a, exists n : nat, let a' := S a in n = a') a (b:=a) := e _ (j b).
+
+Definition k5
+ (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+ (j : forall a, let a' := S a in exists n : nat, n = a') a (b:=a) := e _ (j b).
+
+Definition k6
+ (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+ (j : forall a, exists n : nat, let n' := S n in n' = a) a (b:=a) := e _ (j b).
+
+Definition k7
+ (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat)
+ (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 4fec6e7f..3f8a3bc4 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -342,7 +342,7 @@ case H1.
exact H0.
intros.
exact n.
-Qed.
+Defined.
Extraction oups.
(*
let oups h0 =
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index be4e0684..b25b502c 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -9,13 +9,12 @@ Inductive rBoolOp : Set :=
| rAnd : rBoolOp
| rEq : rBoolOp.
-Definition rlt (a b : rNat) : Prop :=
- (a ?= b)%positive Datatypes.Eq = Datatypes.Lt.
+Definition rlt (a b : rNat) : Prop := Pcompare a b Eq = Lt.
Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}.
intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
generalize (nat_of_P_gt_Gt_compare_morphism n m);
- generalize (Pcompare_Eq_eq n m); case ((n ?= m)%positive Datatypes.Eq).
+ generalize (Pcompare_Eq_eq n m); case (Pcompare n m Eq).
intros H' H'0 H'1; right; right; auto.
intros H' H'0 H'1; left; unfold rlt in |- *.
apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index ce3e692f..e8019a90 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -107,3 +107,20 @@ Context {A:Set}.
Definition h (a:A) := a.
End C.
Check h 0.
+
+(* Check implicit arguments in arity of inductive types. The three
+ following examples used to fail before r13671 *)
+
+Inductive I {A} (a:A) : forall {n:nat}, Prop :=
+ | C : I a (n:=0).
+
+Inductive I2 (x:=0) : Prop :=
+ | C2 {p:nat} : p = 0 -> I2.
+Check C2 eq_refl.
+
+Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
+ | C3 : I3 a (n:=0).
+
+(* Check global implicit declaration over ref not in section *)
+
+Section D. Global Arguments eq [A] _ _. End D.
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index 7626ecc4..234c4223 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 3c8d8ea9..b24ed2f1 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -41,3 +41,26 @@ Proof.
auto.
auto.
Qed.
+
+(* Check selection of occurrences by pattern *)
+
+Goal forall x, S x = S (S x).
+intros.
+induction (S _) in |- * at -2.
+now_show (0=1).
+Undo 2.
+induction (S _) in |- * at 1 3.
+now_show (0=1).
+Undo 2.
+induction (S _) in |- * at 1.
+now_show (0=S (S x)).
+Undo 2.
+induction (S _) in |- * at 2.
+now_show (S x=0).
+Undo 2.
+induction (S _) in |- * at 3.
+now_show (S x=1).
+Undo 2.
+Fail induction (S _) in |- * at 4.
+Abort.
+
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 02618c2c..7387add6 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -244,6 +244,29 @@ reflexivity.
apply I.
Qed.
+(* Test binding of open terms with non linear matching *)
+
+Ltac f_non_linear t :=
+ match t with
+ (forall x y, ?u = 0) -> (forall y x, ?u = 0) =>
+ assert (forall x y:nat, u = u)
+ end.
+
+Goal True.
+f_non_linear ((forall x y, x+y = 0) -> (forall x y, y+x = 0)).
+reflexivity.
+f_non_linear ((forall a b, a+b = 0) -> (forall a b, b+a = 0)).
+reflexivity.
+f_non_linear ((forall a b, a+b = 0) -> (forall x y, y+x = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall a b, b+a = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall y x, x+y = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *)
+|| exact I.
+Qed.
+
(* Test regular failure when clear/intro breaks soundness of the
interpretation of terms in current environment *)
@@ -275,3 +298,7 @@ evar(foo:nat).
let evval := eval compute in foo in not_eq evval 1.
let evval := eval compute in foo in not_eq 1 evval.
Abort.
+
+(* Check that this returns an error and not an anomaly (see r13667) *)
+
+Fail Local Tactic Notation "myintro" := intro.
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index 41aa3b3e..fcadd150 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 5a008f18..56cab0f6 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -9,4 +9,4 @@ End S.
(*
Check f nat nat : Set.
*)
-Check I nat nat : Set.
+Check I nat nat : Set. \ No newline at end of file
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
new file mode 100644
index 00000000..93a9ef11
--- /dev/null
+++ b/test-suite/success/proof_using.v
@@ -0,0 +1,61 @@
+Section Foo.
+
+Variable a : nat.
+
+Lemma l1 : True.
+Fail Proof using non_existing.
+Proof using a.
+exact I.
+Qed.
+
+Lemma l2 : True.
+Proof using a.
+Admitted.
+
+Lemma l3 : True.
+Proof using a.
+admit.
+Qed.
+
+End Foo.
+
+Check (l1 3).
+Check (l2 3).
+Check (l3 3).
+
+Section Bar.
+
+Variable T : Type.
+Variable a b : T.
+Variable H : a = b.
+
+Lemma l4 : a = b.
+Proof using H.
+exact H.
+Qed.
+
+End Bar.
+
+Check (l4 _ 1 1 _ : 1 = 1).
+
+Section S1.
+
+Variable v1 : nat.
+
+Section S2.
+
+Variable v2 : nat.
+
+Lemma deep : v1 = v2.
+Proof using v1 v2.
+admit.
+Qed.
+
+End S2.
+
+Check (deep 3 : v1 = 3).
+
+End S1.
+
+Check (deep 3 4 : 3 = 4).
+
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
new file mode 100644
index 00000000..3241e133
--- /dev/null
+++ b/test-suite/success/remember.v
@@ -0,0 +1,8 @@
+(* Testing remember and co *)
+
+Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
+intros.
+Fail remember nat as X.
+Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
+Fail remember nat as X in |- *.
+Abort.
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 3bce52fe..08c406be 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -108,3 +108,24 @@ intros.
rewrite (H _).
reflexivity.
Qed.
+
+(* Example of rewriting of a degenerated pattern using the right-most
+ argument of the goal. This is sometimes used in contribs, even if
+ ad hoc. Here, we have the extra requirement that checking types
+ needs delta-conversion *)
+
+Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p).
+Definition P := (nat * nat)%type.
+Goal forall x:P, x = x.
+intros. rewrite s.
+Abort.
+
+(* Test second-order unification and failure of pattern-unification *)
+
+Goal forall (P: forall Y, Y -> Prop) Y a, Y = nat -> (True -> P Y a) -> False.
+intros.
+(* The next line used to succeed between June and November 2011 *)
+(* causing ill-typed rewriting *)
+Fail rewrite H in H0.
+Abort.
+
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
new file mode 100644
index 00000000..d9ade314
--- /dev/null
+++ b/test-suite/success/searchabout.v
@@ -0,0 +1,60 @@
+
+(** Test of the different syntaxes of SearchAbout, in particular
+ with and without the [ ... ] delimiters *)
+
+SearchAbout plus.
+SearchAbout plus mult.
+SearchAbout "plus_n".
+SearchAbout plus "plus_n".
+SearchAbout "*".
+SearchAbout "*" "+".
+
+SearchAbout plus inside Peano.
+SearchAbout plus mult inside Peano.
+SearchAbout "plus_n" inside Peano.
+SearchAbout plus "plus_n" inside Peano.
+SearchAbout "*" inside Peano.
+SearchAbout "*" "+" inside Peano.
+
+SearchAbout plus outside Peano Logic.
+SearchAbout plus mult outside Peano Logic.
+SearchAbout "plus_n" outside Peano Logic.
+SearchAbout plus "plus_n" outside Peano Logic.
+SearchAbout "*" outside Peano Logic.
+SearchAbout "*" "+" outside Peano Logic.
+
+SearchAbout -"*" "+" outside Logic.
+SearchAbout -"*"%nat "+"%nat outside Logic.
+
+SearchAbout [plus].
+SearchAbout [plus mult].
+SearchAbout ["plus_n"].
+SearchAbout [plus "plus_n"].
+SearchAbout ["*"].
+SearchAbout ["*" "+"].
+
+SearchAbout [plus] inside Peano.
+SearchAbout [plus mult] inside Peano.
+SearchAbout ["plus_n"] inside Peano.
+SearchAbout [plus "plus_n"] inside Peano.
+SearchAbout ["*"] inside Peano.
+SearchAbout ["*" "+"] inside Peano.
+
+SearchAbout [plus] outside Peano Logic.
+SearchAbout [plus mult] outside Peano Logic.
+SearchAbout ["plus_n"] outside Peano Logic.
+SearchAbout [plus "plus_n"] outside Peano Logic.
+SearchAbout ["*"] outside Peano Logic.
+SearchAbout ["*" "+"] outside Peano Logic.
+
+SearchAbout [-"*" "+"] outside Logic.
+SearchAbout [-"*"%nat "+"%nat] outside Logic.
+
+
+(** The example in the Reference Manual *)
+
+Require Import ZArith.
+
+SearchAbout Zmult Zplus "distr".
+SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
+SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 033b3f48..19693d70 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -130,3 +130,38 @@ intros f0 Q H.
setoid_rewrite H.
tauto.
Qed.
+
+(** Check proper refreshing of the lemma application for multiple
+ different instances in a single setoid rewrite. *)
+
+Section mult.
+ Context (fold : forall {A} {B}, (A -> B) -> A -> B).
+ Context (add : forall A, A -> A).
+ Context (fold_lemma : forall {A B f} {eqA : relation B} x, eqA (fold A B f (add A x)) (fold _ _ f x)).
+ Context (ab : forall B, A -> B).
+ Context (anat : forall A, nat -> A).
+
+Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))).
+Proof. intros.
+ setoid_rewrite fold_lemma.
+ change (fold A A (fun x0 : A => ab A x0) x = anat A (fold A nat (ab nat) x)).
+Abort.
+
+End mult.
+
+(** Current semantics for rewriting with typeclass constraints in the lemma
+ does not fix the instance at the first unification, use [at], or simply rewrite for
+ this semantics. *)
+
+Require Import Arith.
+
+Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}.
+Instance: Foo nat. admit. Defined.
+Instance: Foo bool. admit. Defined.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort.
+
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
new file mode 100644
index 00000000..d4191b93
--- /dev/null
+++ b/test-suite/success/simpl_tuning.v
@@ -0,0 +1,149 @@
+(* as it is dynamically inferred by simpl *)
+Arguments minus !n / m.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (match y with O => S x | S _ => _ end = 0) => idtac end.
+Abort.
+
+(* we avoid exposing a match *)
+Arguments minus n m : simpl nomatch.
+
+Lemma foo x : minus 0 x = 0.
+simpl.
+match goal with |- (0 = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* we unfold as soon as we have 1 args, but we avoid exposing a match *)
+Arguments minus n / m : simpl nomatch.
+
+Lemma foo : minus 0 = fun x => 0.
+simpl.
+match goal with |- minus 0 = _ => idtac end.
+Abort.
+(* This does not work as one may expect. The point is that simpl is implemented
+ as "strong (whd_simpl_state)" and after unfolding minus you have
+ (fun m => match 0 => 0 | S n => ...) that is already in whd and exposes
+ a match, that of course "strong" would reduce away but at that stage
+ we don't know, and reducing by hand under the lambda is against whd *)
+
+(* extra tuning for the usual heuristic *)
+Arguments minus !n / m : simpl nomatch.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* full control *)
+Arguments minus !n !m /.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* omitting /, that being immediately after the last ! is irrelevant *)
+Arguments minus !n !m.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) :=
+ fun x => (f (fst x), g (snd x)).
+
+Delimit Scope foo_scope with F.
+Notation "@@" := nat (only parsing) : foo_scope.
+Notation "@@" := (fun x => x) (only parsing).
+
+Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
+
+Lemma foo x : @pf @@ nat @@ nat nat @@ x = pf @@ @@ x.
+Abort.
+
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+
+(* fcomp is unfolded if applied to 6 args *)
+Arguments fcomp {A B C}%type f g x /.
+
+Notation "f \o g" := (fcomp f g) (at level 50).
+
+Lemma foo (f g h : nat -> nat) x : pf (f \o g) h x = pf f h (g (fst x), snd x).
+simpl.
+match goal with |- (pf (f \o g) h x = _) => idtac end.
+case x; intros x1 x2.
+simpl.
+match goal with |- (pf (f \o g) h _ = pf f h _) => idtac end.
+unfold pf; simpl.
+match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
+Abort.
+
+Definition volatile := fun x : nat => x.
+Arguments volatile /.
+
+Lemma foo : volatile = volatile.
+simpl.
+match goal with |- (fun _ => _) = _ => idtac end.
+Abort.
+
+Set Implicit Arguments.
+
+Section S1.
+
+Variable T1 : Type.
+
+Section S2.
+
+Variable T2 : Type.
+
+Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
+ match n, m with
+ | 0,_ => 0
+ | S _, 0 => n
+ | S n', S m' => f x y n' v m' end.
+
+Global Arguments f x y !n !v !m.
+
+Lemma foo x y n m : f x y (S n) tt m = f x y (S n) tt (S m).
+simpl.
+match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
+Abort.
+
+End S2.
+
+Lemma foo T x y n m : @f T x y (S n) tt m = @f T x y (S n) tt (S m).
+simpl.
+match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
+Abort.
+
+End S1.
+
+Arguments f : clear implicits and scopes.
+
diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v
new file mode 100644
index 00000000..8a607c93
--- /dev/null
+++ b/test-suite/success/telescope_canonical.v
@@ -0,0 +1,12 @@
+Structure Inner := mkI { is :> Type }.
+Structure Outer := mkO { os :> Inner }.
+
+Canonical Structure natInner := mkI nat.
+Canonical Structure natOuter := mkO natInner.
+
+Definition hidden_nat := nat.
+
+Axiom P : forall S : Outer, is (os S) -> Prop.
+
+Lemma foo (n : hidden_nat) : P _ n.
+Admitted.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 66c4e080..5649e2f7 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index ddf122e8..997dceb4 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -21,6 +21,12 @@ Proof.
intros; apply H.
Qed.
+ (* Feature introduced June 2011 *)
+
+Lemma l7 : forall x (P:nat->Prop), (forall f, P (f x)) -> P (x+x).
+Proof.
+intros x P H; apply H.
+Qed.
(* Example submitted for Zenon *)
@@ -90,12 +96,14 @@ intros.
apply H.
Qed.
+(* Feature deactivated in commit 14189 (see commit log)
(* Test instanciation of evars by unification *)
Goal (forall x, 0 + x = 0 -> True) -> True.
intros; eapply H.
rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
Abort.
+*)
(* Check handling of identity equation between evars *)
(* The example failed to pass until revision 10623 *)
@@ -135,4 +143,44 @@ 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.
+ rewrite H with (f:=f0).
+Abort.
+
+(* Three tests provided by Dan Grayson as part of a custom patch he
+ made for a more powerful "destruct" for handling Voevodsky's
+ Univalent Foundations. The test checks if second-order matching in
+ tactic unification is able to guess by itself on which dependent
+ terms to abstract so that the elimination predicate is well-typed *)
+
+Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) :
+ identity (fxe x) (fxe x).
+Proof. destruct (fxe x). apply identity_refl. Defined.
+
+(* a harder example *)
+
+Definition UU := Type .
+Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t.
+Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0.
+Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1.
+Proof. intros t. exact t. Defined.
+
+Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k).
+Proof.
+ destruct k.
+ apply idpath.
+Defined.
+
+(* an example with two constructors *)
+
+Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU :=
+| newfoo1 : foo' x0 x0
+| newfoo2 : foo' x0 x0 .
+Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} :
+ foo' x0 x1 -> foo' x0 x1.
+Proof. intros t. exact t. Defined.
+Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k).
+Proof.
+ destruct k.
+ apply idpath.
+ apply idpath.
+Defined.
diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes-coercion.v
new file mode 100644
index 00000000..d7504340
--- /dev/null
+++ b/test-suite/success/universes-coercion.v
@@ -0,0 +1,22 @@
+(* This example used to emphasize the absence of LEGO-style universe
+ polymorphism; Matthieu's improvements of typing on 2011/3/11 now
+ makes (apparently) that Amokrane's automatic eta-expansion in the
+ coercion mechanism works; this makes its illustration as a "weakness"
+ of universe polymorphism obsolete (example submitted by Randy Pollack).
+
+ Note that this example is not an evidence that the current
+ non-kernel eta-expansion behavior is the most expected one.
+*)
+
+Parameter K : forall T : Type, T -> T.
+Check (K (forall T : Type, T -> T) K).
+
+(*
+ note that the inferred term is
+ "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))"
+ which is not eta-equivalent to
+ "(K (forall T : Type, T -> T) K"
+ because the eta-expansion of the latter
+ "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)"
+ assuming K of type "forall T (* u2 *) : Type, T -> T"
+*)