Imported Upstream version 8.1~gammaupstream/8.1.gamma

16 files changed, 380 insertions, 23 deletions

diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index 003810cc..44d21b83 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -5,3 +5,10 @@ Structure foo : Type := Foo {
 }.
 
 Canonical Structure unopt_nat := @Foo nat (fun _ => O).
+
+(* Granted wish #1187 *)
+
+Record Silly (X : Set) : Set := mkSilly { x : X }.
+Definition anotherMk := mkSilly.
+Definition struct := anotherMk nat 3.
+Canonical Structure struct.
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index f19e24b8..f14725a8 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -67,3 +67,15 @@ Check (fun x => match x with
                 | D _ => 1
                 end).
 
+(* Check coercions against the type of the term to match *)
+(* Used to fail in V8.1beta *)
+
+Inductive C : Set := c : C.
+Inductive E : Set := e :> C -> E.
+Check fun (x : E) => match x with c => e c end.
+
+(* Check coercions with uniform parameters (cf bug #1168) *)
+
+Inductive C' : bool -> Set := c' : C' true.
+Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
+Check fun (x : E' true) => match x with c' => e' true c' end.
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index 9f4ec79a..b4c06c7b 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -6,62 +6,75 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field.v 7693 2005-12-21 23:50:17Z herbelin $ *)
+(* $Id: Field.v 9197 2006-10-02 15:55:52Z barras $ *)
 
 (**** Tests of Field with real numbers ****)
 
-Require Import Reals.
+Require Import Reals RealField.
+Open Scope R_scope.
 
 (* Example 1 *)
 Goal
 forall eps : R,
-(eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)))%R = (eps * (1 / 2))%R.
+eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)) = eps * (1 / 2).
 Proof.
   intros.
    field.
-Abort.
+Qed.
 
 (* Example 2 *)
 Goal
 forall (f g : R -> R) (x0 x1 : R),
-((f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)))%R =
-((f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)))%R.
+(f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)) =
+(f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)).
 Proof.
   intros.
    field.
 Abort.
  
 (* Example 3 *)
-Goal forall a b : R, (1 / (a * b) * (1 / 1 / b))%R = (1 / a)%R.
+Goal forall a b : R, 1 / (a * b) * (1 / (1 / b)) = 1 / a.
 Proof.
   intros.
    field.
 Abort.
+
+Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a.
+Proof.
+  intros.
+   field_simplify_eq.
+Abort.
  
+Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a.
+Proof.
+  intros.
+   field_simplify (1 / (a * b) * (1 / 1 / b)).
+Abort.
+
 (* Example 4 *)
 Goal
-forall a b : R, a <> 0%R -> b <> 0%R -> (1 / (a * b) / 1 / b)%R = (1 / a)%R.
+forall a b : R, a <> 0 -> b <> 0 -> 1 / (a * b) / (1 / b) = 1 / a.
 Proof.
   intros.
-   field.
-Abort.
+   field; auto.
+Qed.
  
 (* Example 5 *)
-Goal forall a : R, 1%R = (1 * (1 / a) * a)%R.
+Goal forall a : R, 1 = 1 * (1 / a) * a.
 Proof.
   intros.
    field.
 Abort.
  
 (* Example 6 *)
-Goal forall a b : R, b = (b * / a * a)%R.
+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)%R.
+Goal forall a b : R, b = b * (1 / a) * a.
 Proof.
   intros.
    field.
@@ -70,8 +83,8 @@ Abort.
 (* Example 8 *)
 Goal
 forall x y : R,
-(x * (1 / x + x / (x + y)))%R =
-(- (1 / y) * y * (- (x * (x / (x + y))) - 1))%R.
+x * (1 / x + x / (x + y)) =
+- (1 / y) * y * (- (x * (x / (x + y))) - 1).
 Proof.
   intros.
    field.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index f8f7c996..606e884a 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -36,3 +36,29 @@ intros.
 exact (fun H => H).
 Qed.
 
+(* Test injection as *)
+
+Lemma l5 : forall x y z t : nat, (x,y) = (z,t) -> x=z.
+intros; injection H as Hyt Hxz.
+exact Hxz.
+Qed.
+
+(* Injection does not projects at positions in Prop... allow it?
+
+Inductive t (A:Prop) : Set := c : A -> t A.
+Goal forall p q : True\/True, c _ p = c _ q -> False.
+intros.
+injection H.
+Abort.
+
+*)
+
+(* Accept does not project on discriminable positions... allow it?
+
+Goal 1=2 -> 1=0.
+intro H.
+injection H.
+intro; assumption.
+Qed.
+
+ *)
diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v
new file mode 100644
index 00000000..d53e4010
--- /dev/null
+++ b/test-suite/success/LegacyField.v
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \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.
+
+(* Example 1 *)
+Goal
+forall eps : R,
+(eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)))%R = (eps * (1 / 2))%R.
+Proof.
+  intros.
+   legacy field.
+Abort.
+
+(* Example 2 *)
+Goal
+forall (f g : R -> R) (x0 x1 : R),
+((f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)))%R =
+((f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)))%R.
+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.
+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.
+  intros.
+   legacy field.
+Abort.
+
+(* Example 8 *)
+Goal
+forall x y : R,
+(x * (1 / x + x / (x + y)))%R =
+(- (1 / y) * y * (- (x * (x / (x + y))) - 1))%R.
+Proof.
+  intros.
+   legacy field.
+Abort.
diff --git a/test-suite/success/NatRing.v b/test-suite/success/NatRing.v
index 8426c7e4..22d021d5 100644
--- a/test-suite/success/NatRing.v
+++ b/test-suite/success/NatRing.v
@@ -1,10 +1,10 @@
 Require Import ArithRing.
 
 Lemma l1 : 2 = 1 + 1.
-ring_nat.
+ring.
 Qed.
 
 Lemma l2 : forall x : nat, S (S x) = 1 + S x.
 intro.
-ring_nat.
+ring.
 Qed.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
new file mode 100644
index 00000000..4f260696
--- /dev/null
+++ b/test-suite/success/apply.v
@@ -0,0 +1,14 @@
+(* Test apply in *)
+
+Goal (forall x y, x = S y -> y=y) -> 2 = 4 -> 3=3.
+intros H H0.
+apply H in H0.
+assumption.
+Qed.
+
+Require Import ZArith.
+Open Scope Z_scope.
+Goal forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y.
+intros; apply Znot_le_gt, Zgt_lt in H.
+apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto.
+Qed.
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewritein.v
index 8126e9e4..68f2f7ce 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewritein.v
@@ -12,9 +12,12 @@ Proof.
   autorewrite with base0 in H using try (apply H; reflexivity).
 Qed.
 
-Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), H=H -> False.
+Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False.
 Proof.
   intros.
-  autorewrite with base0 in H using try (apply H1; reflexivity).
+  autorewrite with base0 in *.
+    apply H;reflexivity.
 Qed.
 
+
+
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 8dd48752..d652132e 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -22,7 +22,7 @@ Coercion i : h >-> nat.
 Parameter C : nat -> nat -> nat.
 Coercion C : nat >-> Funclass.
 
-(* Remark: in the following example, it cannot be decide whether C is
+(* 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 
 
@@ -30,3 +30,34 @@ Parameter A : nat -> Prop.
 Parameter C:> forall n:nat, A n -> nat.
 *)
 
+(* Check coercion between products based on eta-expansion *)
+(* (there was a de Bruijn bug until rev 9254) *)
+
+Section P.
+
+Variable E : Set.
+Variables C D : E -> Prop.
+Variable G :> forall x, C x -> D x.
+
+Check fun (H : forall y:E, y = y -> C y) => (H : forall y:E, y = y -> D y).
+
+End P.
+
+(* Check that class arguments are computed the same when looking for a
+   coercion and when applying it (class_args_of) (failed until rev 9255) *)
+
+Section Q.
+
+Variable bool : Set.
+Variables C D : bool -> Prop.
+Variable G :> forall x, C x -> D x.
+Variable f : nat -> bool.
+
+Definition For_all (P : nat -> Prop) := forall x, P x.
+
+Check fun (H : For_all (fun x => C (f x))) => H : forall x, D (f x).
+Check fun (H : For_all (fun x => C (f x))) x => H x : D (f x).
+Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)).
+
+End Q.
+
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index baeec147..ad69ced1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -68,3 +68,9 @@ Proof. trivial. Qed.
 Hint Resolve contradiction.
 Goal False.
 eauto.
+
+(* This used to fail in V8.1beta because first-order unification was
+   used before using type information *)
+
+Check (exist _ O (refl_equal 0) : {n:nat|n=0}).
+Check (exist _ O I : {n:nat|True}).
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 1786424e..47c58f04 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -29,6 +29,10 @@ Check (fun x => fst (f x)).
 Check (fun x => fst (f x)).
 Notation rhs := snd.
 Check (fun x => snd (f x)).
-(* V8 seulement 
-Check (fun x => @ rhs ? ? (f x)).
-*)
+Check (fun x => @ rhs _ _ (f x)).
+
+(* Implicit arguments in fixpoints and inductive declarations *)
+
+Fixpoint g n := match n with O => true | S n => g n end.
+
+Inductive P n : nat -> Prop := c : P n n.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 99cfe017..3f25f703 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -153,3 +153,25 @@ Ltac afi tac := intros; tac.
 Goal 1 = 2.
 afi ltac:auto.
 
+(* Tactic Notation avec listes *)
+
+Tactic Notation "pat" hyp(id) "occs" integer_list(l) := pattern id at l.
+
+Goal forall x, x=0 -> x=x.
+intro x.
+pat x occs 1 3.
+Abort.
+
+Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l.
+
+Goal forall a b c, a=0 -> b=c+a.
+intros.
+revert a b c H.
+Abort.
+
+(* Used to fail until revision 9280 because of a parasitic App node with
+   empty args *)
+
+Goal True.
+match None with @None => exact I end.
+Abort.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
new file mode 100644
index 00000000..5a008f18
--- /dev/null
+++ b/test-suite/success/polymorphism.v
@@ -0,0 +1,12 @@
+(* Some tests of sort-polymorphisme *)
+Section S.
+Variable A:Type.
+(*
+Definition f (B:Type) := (A * B)%type.
+*)
+Inductive I (B:Type) : Type := prod : A->B->I B.
+End S.
+(*
+Check f nat nat : Set.
+*)
+Check I nat nat : Set.
diff --git a/test-suite/success/replace.v b/test-suite/success/replace.v
new file mode 100644
index 00000000..94b75c7f
--- /dev/null
+++ b/test-suite/success/replace.v
@@ -0,0 +1,24 @@
+Goal forall x, x = 0 -> S x = 7 -> x = 22 .
+Proof.
+replace 0 with 33.
+Undo.
+intros x H H0.
+replace x with 0.
+Undo.
+replace x with 0 in  |- *. 
+Undo.
+replace x with 1 in *.
+Undo.
+replace x with 0 in *|- *.
+Undo.
+replace x with 0 in *|-.
+Undo.
+replace x with 0 in H0 .
+Undo.
+replace x with 0 in H0 |- * .
+Undo.
+
+replace x with 0 in H,H0 |- * .
+Undo.
+Admitted.
+
diff --git a/test-suite/success/setoid_ring_module.v b/test-suite/success/setoid_ring_module.v
new file mode 100644
index 00000000..e947c6d9
--- /dev/null
+++ b/test-suite/success/setoid_ring_module.v
@@ -0,0 +1,40 @@
+Require Import Setoid Ring Ring_theory.
+
+Module abs_ring.
+
+Parameters (Coef:Set)(c0 c1 : Coef)
+(cadd cmul csub: Coef -> Coef -> Coef)
+(copp : Coef -> Coef)
+(ceq : Coef -> Coef -> Prop)
+(ceq_sym : forall x y, ceq x y -> ceq y x)
+(ceq_trans : forall x y z, ceq x y -> ceq y z -> ceq x z)
+(ceq_refl : forall x, ceq x x).
+
+
+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.
+
+Add Morphism cmul with signature ceq ==> ceq ==> ceq as cmul_Morphism.
+Admitted.
+
+Add Morphism copp with signature ceq ==> ceq as copp_Morphism.
+Admitted.
+
+Definition cRth : ring_theory c0 c1 cadd cmul csub copp ceq.
+Admitted.
+
+Add Ring CoefRing : cRth.
+
+End abs_ring.
+Import abs_ring.
+
+Theorem check_setoid_ring_modules :
+  forall a b, ceq (cadd a b) (cadd b a).
+intros.
+ring.
+Qed.
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
new file mode 100644
index 00000000..68869621
--- /dev/null
+++ b/test-suite/success/unification.v
@@ -0,0 +1,65 @@
+(* Test patterns unification *)
+
+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), 
+                   (exists x:A, exists y:Q x, P x y /\ P x y) -> False.
+Proof.
+intros; apply (H _ H0).
+Qed.
+
+
+(* Example submitted for Zenon *)
+
+Axiom zenon_noteq : forall T : Type, forall t : T, ((t <> t) -> False).
+Axiom zenon_notall : forall T : Type, forall P : T -> Prop,
+  (forall z : T, (~(P z) -> False)) -> (~(forall x : T, (P x)) -> False).
+
+  (* Must infer "P := fun x => x=x" in zenon_notall *)
+Check (fun _h1 => (zenon_notall nat _ (fun _T_0 =>
+          (fun _h2 => (zenon_noteq _ _T_0 _h2))) _h1)).
+
+
+(* Core of an example submitted by Ralph Matthes (#849)
+
+   It used to fail because of the K-variable x in the type of "sum_rec ..."
+   which was not in the scope of the evar ?B. Solved by a head
+   beta-reduction of the type "(fun _ : unit + unit => L unit) x" of
+   "sum_rec ...". Shall we used more reduction when solving evars (in
+   real_clean)?? Is there a risk of starting too long reductions?
+
+   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).  
+*)
+
+Set Implicit Arguments.
+Inductive L (A:Set) : Set := c : A -> L A.
+Parameter f: forall (A:Set)(B:Set), (A->B) -> L A -> L B.
+Parameter t: L (unit + unit).
+
+Check (f (fun x : unit + unit =>
+  sum_rec (fun _ : unit + unit => L unit)
+    (fun y => c y) (fun y => c y) x) t).
+
+
+(* Test patterns unification in apply *)
+
+Require Import Arith.
+Parameter x y : nat.
+Parameter G:x=y->x=y->Prop.
+Parameter K:x<>y->x<>y->Prop.
+Lemma l3 : (forall f:x=y->Prop, forall g:x<>y->Prop,
+            match eq_nat_dec x y with left a => f a | right a => g a end)
+   -> match eq_nat_dec x y with left a => G a a | right a => K a a end.
+Proof.
+intros.
+apply H.
+Qed.