summaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /test-suite/success
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/Destruct.v13
-rw-r--r--test-suite/success/Funind.v119
-rw-r--r--test-suite/success/If.v7
-rw-r--r--test-suite/success/Notations.v9
-rw-r--r--test-suite/success/Omega0.v149
-rw-r--r--test-suite/success/ROmega.v98
-rw-r--r--test-suite/success/ROmega0.v149
-rw-r--r--test-suite/success/ROmega2.v28
-rw-r--r--test-suite/success/RecTutorial.v4
-rw-r--r--test-suite/success/destruct.v16
-rw-r--r--test-suite/success/evars.v2
-rw-r--r--test-suite/success/if.v7
-rw-r--r--test-suite/success/refine.v23
-rw-r--r--test-suite/success/unicode_utf8.v3
14 files changed, 541 insertions, 86 deletions
diff --git a/test-suite/success/Destruct.v b/test-suite/success/Destruct.v
deleted file mode 100644
index b909e45e..00000000
--- a/test-suite/success/Destruct.v
+++ /dev/null
@@ -1,13 +0,0 @@
-(* Submitted by Robert Schneck *)
-
-Parameter A B C D : Prop.
-Axiom X : A -> B -> C /\ D.
-
-Lemma foo : A -> B -> C.
-Proof.
-intros.
-destruct X. (* Should find axiom X and should handle arguments of X *)
-assumption.
-assumption.
-assumption.
-Qed.
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 84a58a3a..939d06c7 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -5,25 +5,17 @@ Definition iszero (n : nat) : bool :=
| _ => false
end.
- Functional Scheme iszer_ind := Induction for iszero.
+Functional Scheme iszero_ind := Induction for iszero Sort Prop.
Lemma toto : forall n : nat, n = 0 -> iszero n = true.
intros x eg.
functional induction iszero x; simpl in |- *.
trivial.
- subst x.
-inversion H_eq_.
+inversion eg.
Qed.
-(* We can even reuse the proof as a scheme: *)
-
- Functional Scheme toto_ind := Induction for iszero.
-
-
-
-
-Definition ftest (n m : nat) : nat :=
+Function ftest (n m : nat) : nat :=
match n with
| O => match m with
| O => 0
@@ -32,27 +24,25 @@ Definition ftest (n m : nat) : nat :=
| S p => 0
end.
- Functional Scheme ftest_ind := Induction for ftest.
-
Lemma test1 : forall n m : nat, ftest n m <= 2.
intros n m.
functional induction ftest n m; auto.
Qed.
-
+Require Import Arith.
Lemma test11 : forall m : nat, ftest 0 m <= 2.
intros m.
functional induction ftest 0 m.
auto.
-auto.
+auto.
+auto with *.
Qed.
-
-Definition lamfix (m : nat) :=
- fix trivfun (n : nat) : nat := match n with
- | O => m
- | S p => trivfun p
- end.
+Function lamfix (m n : nat) {struct n } : nat :=
+ match n with
+ | O => m
+ | S p => lamfix m p
+ end.
(* Parameter v1 v2 : nat. *)
@@ -68,12 +58,12 @@ Defined.
(* polymorphic function *)
Require Import List.
- Functional Scheme app_ind := Induction for app.
+Functional Scheme app_ind := Induction for app Sort Prop.
Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
intros A l l'.
functional induction app A l l'; intuition.
- rewrite <- H1; trivial.
+ rewrite <- H0; trivial.
Qed.
@@ -83,7 +73,7 @@ Qed.
Require Export Arith.
-Fixpoint trivfun (n : nat) : nat :=
+Function trivfun (n : nat) : nat :=
match n with
| O => 0
| S m => trivfun m
@@ -97,18 +87,16 @@ Parameter varessai : nat.
Lemma first_try : trivfun varessai = 0.
functional induction trivfun varessai.
trivial.
-simpl in |- *.
assumption.
Defined.
- Functional Scheme triv_ind := Induction for trivfun.
+ Functional Scheme triv_ind := Induction for trivfun Sort Prop.
Lemma bisrepetita : forall n' : nat, trivfun n' = 0.
intros n'.
functional induction trivfun n'.
trivial.
-simpl in |- *.
assumption.
Qed.
@@ -118,14 +106,14 @@ Qed.
-Fixpoint iseven (n : nat) : bool :=
+Function iseven (n : nat) : bool :=
match n with
| O => true
| S (S m) => iseven m
| _ => false
end.
-Fixpoint funex (n : nat) : nat :=
+Function funex (n : nat) : nat :=
match iseven n with
| true => n
| false => match n with
@@ -134,7 +122,7 @@ Fixpoint funex (n : nat) : nat :=
end
end.
-Fixpoint nat_equal_bool (n m : nat) {struct n} : bool :=
+Function nat_equal_bool (n m : nat) {struct n} : bool :=
match n with
| O => match m with
| O => true
@@ -149,6 +137,7 @@ Fixpoint nat_equal_bool (n m : nat) {struct n} : bool :=
Require Export Div2.
+Functional Scheme div2_ind := Induction for div2 Sort Prop.
Lemma div2_inf : forall n : nat, div2 n <= n.
intros n.
functional induction div2 n.
@@ -157,34 +146,27 @@ auto.
apply le_S.
apply le_n_S.
-exact H.
+exact IHn0.
Qed.
(* reuse this lemma as a scheme:*)
- Functional Scheme div2_ind := Induction for div2_inf.
-Fixpoint nested_lam (n : nat) : nat -> nat :=
+Function nested_lam (n : nat) : nat -> nat :=
match n with
| O => fun m : nat => 0
| S n' => fun m : nat => m + nested_lam n' m
end.
- Functional Scheme nested_lam_ind := Induction for nested_lam.
Lemma nest : forall n m : nat, nested_lam n m = n * m.
intros n m.
- functional induction nested_lam n m; auto.
-Qed.
-
-Lemma nest2 : forall n m : nat, nested_lam n m = n * m.
-intros n m. pattern n, m in |- *.
-apply nested_lam_ind; simpl in |- *; intros; auto.
+ functional induction nested_lam n m; simpl;auto.
Qed.
-Fixpoint essai (x : nat) (p : nat * nat) {struct x} : nat :=
- let (n, m) := p in
+Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
+ let (n, m) := (p: nat*nat) in
match n with
| O => 0
| S q => match x with
@@ -198,12 +180,12 @@ Lemma essai_essai :
intros x p.
functional induction essai x p; intros.
inversion H.
-simpl in |- *; try abstract auto with arith.
-simpl in |- *; try abstract auto with arith.
+auto with arith.
+ auto with arith.
Qed.
-Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat :=
+Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
let x := nat_equal_bool m 5 in
let y := 0 in
match n with
@@ -218,21 +200,18 @@ Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat :=
Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
intros a b.
-unfold plus_x_not_five'' in |- *.
functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto.
Qed.
Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
intros n m.
-unfold nat_equal_bool in |- *.
functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
-inversion hyp.
+rewrite <- hyp in H1; simpl in H1;tauto.
inversion hyp.
Qed.
Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
intros n m.
-unfold nat_equal_bool in |- *.
functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto.
inversion eg.
inversion eg.
@@ -242,6 +221,8 @@ Qed.
Inductive istrue : bool -> Prop :=
istrue0 : istrue true.
+Functional Scheme plus_ind := Induction for plus Sort Prop.
+
Lemma inf_x_plusxy' : forall x y : nat, x <= x + y.
intros n m.
functional induction plus n m; intros.
@@ -264,7 +245,7 @@ intros n.
functional induction plus 0 n; intros; auto with arith.
Qed.
-Fixpoint mod2 (n : nat) : nat :=
+Function mod2 (n : nat) : nat :=
match n with
| O => 0
| S (S m) => S (mod2 m)
@@ -276,13 +257,13 @@ intros n.
functional induction mod2 n; simpl in |- *; auto with arith.
Qed.
-Definition isfour (n : nat) : bool :=
+Function isfour (n : nat) : bool :=
match n with
| S (S (S (S O))) => true
| _ => false
end.
-Definition isononeorfour (n : nat) : bool :=
+Function isononeorfour (n : nat) : bool :=
match n with
| S O => true
| S (S (S (S O))) => true
@@ -294,15 +275,22 @@ intros n.
functional induction isononeorfour n; intros istr; simpl in |- *;
inversion istr.
apply istrue0.
+destruct n. inversion istr.
+destruct n. tauto.
+destruct n. inversion istr.
+destruct n. inversion istr.
+destruct n. tauto.
+simpl in *. inversion H1.
Qed.
Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
intros n.
functional induction isononeorfour n; intros m istr; inversion istr.
apply istrue0.
+rewrite H in H0; simpl in H0;tauto.
Qed.
-Definition ftest4 (n m : nat) : nat :=
+Function ftest4 (n m : nat) : nat :=
match n with
| O => match m with
| O => 0
@@ -321,13 +309,20 @@ Qed.
Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2.
intros n m.
- functional induction ftest4 (S n) m.
+assert ({n0 | n0 = S n}).
+exists (S n);reflexivity.
+destruct H as [n0 H1].
+rewrite <- H1;revert H1.
+ functional induction ftest4 n0 m.
+inversion 1.
+inversion 1.
+
auto with arith.
auto with arith.
Qed.
-Definition ftest44 (x : nat * nat) (n m : nat) : nat :=
- let (p, q) := x in
+Function ftest44 (x : nat * nat) (n m : nat) : nat :=
+ let (p, q) := (x: nat*nat) in
match n with
| O => match m with
| O => 0
@@ -349,7 +344,7 @@ auto with arith.
auto with arith.
Qed.
-Fixpoint ftest2 (n m : nat) {struct n} : nat :=
+Function ftest2 (n m : nat) {struct n} : nat :=
match n with
| O => match m with
| O => 0
@@ -363,7 +358,7 @@ intros n m.
functional induction ftest2 n m; simpl in |- *; intros; auto.
Qed.
-Fixpoint ftest3 (n m : nat) {struct n} : nat :=
+Function ftest3 (n m : nat) {struct n} : nat :=
match n with
| O => 0
| S p => match m with
@@ -384,7 +379,7 @@ simpl in |- *.
auto.
Qed.
-Fixpoint ftest5 (n m : nat) {struct n} : nat :=
+Function ftest5 (n m : nat) {struct n} : nat :=
match n with
| O => 0
| S p => match m with
@@ -405,7 +400,7 @@ simpl in |- *.
auto.
Qed.
-Definition ftest7 (n : nat) : nat :=
+Function ftest7 (n : nat) : nat :=
match ftest5 n 0 with
| O => 0
| S r => 0
@@ -416,11 +411,10 @@ Lemma essai7 :
(Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2)
(n : nat), ftest7 n <= 2.
intros hyp1 hyp2 n.
-unfold ftest7 in |- *.
functional induction ftest7 n; auto.
Qed.
-Fixpoint ftest6 (n m : nat) {struct n} : nat :=
+Function ftest6 (n m : nat) {struct n} : nat :=
match n with
| O => 0
| S p => match ftest5 p 0 with
@@ -445,7 +439,6 @@ Qed.
Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
intros n m.
-unfold ftest6 in |- *.
functional induction ftest6 n m; simpl in |- *; auto.
Qed.
diff --git a/test-suite/success/If.v b/test-suite/success/If.v
deleted file mode 100644
index b7f06dcf..00000000
--- a/test-suite/success/If.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* Check correct use of if-then-else predicate annotation (cf bug 690) *)
-
-Check fun b : bool =>
- if b as b0 return (if b0 then b0 = true else b0 = false)
- then refl_equal true
- else refl_equal false.
-
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
new file mode 100644
index 00000000..a9e2c59a
--- /dev/null
+++ b/test-suite/success/Notations.v
@@ -0,0 +1,9 @@
+(* Check that "where" clause behaves as if given independently of the *)
+(* definition (variant of bug #113? submitted by Assia Mahboubi) *)
+
+Fixpoint plus1 (n m:nat) {struct n} : nat :=
+ match n with
+ | O => m
+ | S p => S (p+m)
+ end
+ where "n + m" := (plus1 n m) : nat_scope.
diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v
new file mode 100644
index 00000000..4614c90d
--- /dev/null
+++ b/test-suite/success/Omega0.v
@@ -0,0 +1,149 @@
+Require Import ZArith Omega.
+Open Scope Z_scope.
+
+(* Pierre L: examples gathered while debugging romega. *)
+
+Lemma test_romega_0 :
+ forall m m',
+ 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
+Proof.
+intros.
+(*omega.*)
+Admitted.
+
+Lemma test_romega_0b :
+ forall m m',
+ 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
+Proof.
+intros m m'.
+(*omega.*)
+Admitted.
+
+Lemma test_romega_1 :
+ forall (z z1 z2 : Z),
+ z2 <= z1 ->
+ z1 <= z2 ->
+ z1 >= 0 ->
+ z2 >= 0 ->
+ z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+ z >= 0.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_1b :
+ forall (z z1 z2 : Z),
+ z2 <= z1 ->
+ z1 <= z2 ->
+ z1 >= 0 ->
+ z2 >= 0 ->
+ z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+ z >= 0.
+Proof.
+intros z z1 z2.
+omega.
+Qed.
+
+Lemma test_romega_2 : forall a b c:Z,
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_2b : forall a b c:Z,
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros a b c.
+omega.
+Qed.
+
+Lemma test_romega_3 : forall a b h hl hr ha hb,
+ 0 <= ha - hl <= 1 ->
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a + 1) ->
+ 0 <= hb - h <= 1.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_3b : forall a b h hl hr ha hb,
+ 0 <= ha - hl <= 1 ->
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a + 1) ->
+ 0 <= hb - h <= 1.
+Proof.
+intros a b h hl hr ha hb.
+omega.
+Qed.
+
+
+Lemma test_romega_4 : forall hr ha,
+ ha = 0 ->
+ (ha = 0 -> hr =0) ->
+ hr = 0.
+Proof.
+intros hr ha.
+omega.
+Qed.
+
+Lemma test_romega_5 : forall hr ha,
+ ha = 0 ->
+ (~ha = 0 \/ hr =0) ->
+ hr = 0.
+Proof.
+intros hr ha.
+omega.
+Qed.
+
+Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros z.
+omega.
+Qed.
+
+Lemma test_romega_7 : forall z,
+ 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_7b : forall z,
+ 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+omega.
+Qed.
+
+(* Magaud #240 *)
+
+Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros x y.
+omega.
+Qed.
+
+
+
+
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
new file mode 100644
index 00000000..04b666ed
--- /dev/null
+++ b/test-suite/success/ROmega.v
@@ -0,0 +1,98 @@
+
+Require Import ZArith ROmega.
+
+(* Submitted by Xavier Urbain 18 Jan 2002 *)
+
+Lemma lem1 :
+ forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
+Proof.
+intros x y.
+ (*romega.*)
+Admitted.
+
+(* Proposed by Pierre Crégut *)
+
+Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
+intro.
+ romega.
+Qed.
+
+(* Proposed by Jean-Christophe Filliâtre *)
+
+Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
+Proof.
+intros.
+ (*romega.*)
+Admitted.
+
+(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
+(* internal variable and a section variable (June 2001) *)
+
+Section A.
+Variable x y : Z.
+Hypothesis H : (x > y)%Z.
+Lemma lem4 : (x > y)%Z.
+ romega.
+Qed.
+End A.
+
+(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
+(* May 2002 *)
+
+Section B.
+Variable R1 R2 S1 S2 H S : Z.
+Hypothesis I : (R1 < 0)%Z -> R2 = (R1 + (2 * S1 - 1))%Z.
+Hypothesis J : (R1 < 0)%Z -> S2 = (S1 - 1)%Z.
+Hypothesis K : (R1 >= 0)%Z -> R2 = R1.
+Hypothesis L : (R1 >= 0)%Z -> S2 = S1.
+Hypothesis M : (H <= 2 * S)%Z.
+Hypothesis N : (S < H)%Z.
+Lemma lem5 : (H > 0)%Z.
+ romega.
+Qed.
+End B.
+
+(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
+Lemma lem6 :
+ forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
+intros.
+ romega.
+Qed.
+
+(* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
+Require Import Omega.
+Section C.
+Parameter g : forall m : nat, m <> 0 -> Prop.
+Parameter f : forall (m : nat) (H : m <> 0), g m H.
+Variable n : nat.
+Variable ap_n : n <> 0.
+Let delta := f n ap_n.
+Lemma lem7 : n = n.
+ (*romega.*) (*ROMEGA CANT DEAL WITH NAT*)
+Admitted.
+End C.
+
+(* Problem of dependencies *)
+Require Import Omega.
+Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
+intros.
+(* romega.*) (*ROMEGA CANT DEAL WITH NAT*)
+Admitted.
+
+(* Bug that what caused by the use of intro_using in Omega *)
+Require Import Omega.
+Lemma lem9 :
+ forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
+intros.
+(* romega.*)(*ROMEGA CANT DEAL WITH NAT*)
+Admitted.
+
+(* Check that the interpretation of mult on nat enforces its positivity *)
+(* Submitted by Hubert Thierry (bug #743) *)
+(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z"
+Require Omega.
+Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))).
+Proof.
+Intros; Omega.
+Qed.
+*)
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
new file mode 100644
index 00000000..0efca1e1
--- /dev/null
+++ b/test-suite/success/ROmega0.v
@@ -0,0 +1,149 @@
+Require Import ZArith ROmega.
+Open Scope Z_scope.
+
+(* Pierre L: examples gathered while debugging romega. *)
+
+Lemma test_romega_0 :
+ forall m m',
+ 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
+Proof.
+intros.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_0b :
+ forall m m',
+ 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
+Proof.
+intros m m'.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_1 :
+ forall (z z1 z2 : Z),
+ z2 <= z1 ->
+ z1 <= z2 ->
+ z1 >= 0 ->
+ z2 >= 0 ->
+ z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+ z >= 0.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_1b :
+ forall (z z1 z2 : Z),
+ z2 <= z1 ->
+ z1 <= z2 ->
+ z1 >= 0 ->
+ z2 >= 0 ->
+ z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+ z >= 0.
+Proof.
+intros z z1 z2.
+(* romega. *)
+Admitted.
+
+Lemma test_romega_2 : forall a b c:Z,
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_2b : forall a b c:Z,
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros a b c.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_3 : forall a b h hl hr ha hb,
+ 0 <= ha - hl <= 1 ->
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a + 1) ->
+ 0 <= hb - h <= 1.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_3b : forall a b h hl hr ha hb,
+ 0 <= ha - hl <= 1 ->
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a + 1) ->
+ 0 <= hb - h <= 1.
+Proof.
+intros a b h hl hr ha hb.
+romega.
+Qed.
+
+
+Lemma test_romega_4 : forall hr ha,
+ ha = 0 ->
+ (ha = 0 -> hr =0) ->
+ hr = 0.
+Proof.
+intros hr ha.
+romega.
+Qed.
+
+Lemma test_romega_5 : forall hr ha,
+ ha = 0 ->
+ (~ha = 0 \/ hr =0) ->
+ hr = 0.
+Proof.
+intros hr ha.
+romega.
+Qed.
+
+Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros z.
+(*romega. *)
+Admitted.
+
+Lemma test_romega_7 : forall z,
+ 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_7b : forall z,
+ 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+(*romega.*)
+Admitted.
+
+(* Magaud #240 *)
+
+Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros x y.
+romega.
+Qed.
+
+
+
+
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
new file mode 100644
index 00000000..9d47c9f6
--- /dev/null
+++ b/test-suite/success/ROmega2.v
@@ -0,0 +1,28 @@
+Require Import ZArith ROmega.
+
+(* Submitted by Yegor Bryukhov (#922) *)
+
+Open Scope Z_scope.
+
+Lemma Test46 :
+forall v1 v2 v3 v4 v5 : Z,
+((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
+9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) ->
+((9 * v3) + (2 * v5)) + (5 * v2) = 3 * v4 ->
+0 > 6 * v1 ->
+(0 * v3) + (6 * v2) <> 2 ->
+(0 * v3) + (5 * v5) <> ((4 * v2) + (8 * v2)) + (2 * v5) ->
+7 * v3 > 5 * v5 ->
+0 * v4 >= ((5 * v1) + (4 * v1)) + ((6 * v5) + (3 * v5)) ->
+7 * v2 = ((3 * v2) + (6 * v5)) + (7 * v2) ->
+0 * v3 > 7 * v1 ->
+9 * v2 < 9 * v5 ->
+(2 * v3) + (8 * v1) <= 5 * v4 ->
+5 * v2 = ((5 * v1) + (0 * v5)) + (1 * v2) ->
+0 * v5 <= 9 * v2 ->
+((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
+-> False.
+intros.
+(*romega.*)
+Admitted.
+
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d79b85df..60e170e4 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -1011,7 +1011,7 @@ Implicit Arguments Vnil [A].
Implicit Arguments Vhead [A n].
Implicit Arguments Vtail [A n].
-Definition Vid : forall (A : Set)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
Proof.
destruct n; intro v.
exact Vnil.
@@ -1024,7 +1024,7 @@ Eval simpl in (fun (A:Set)(v:vector A 0) => v).
-Lemma Vid_eq : forall (n:nat) (A:Set)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
Proof.
destruct v.
reflexivity.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index ede573a3..9f938e10 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -1,3 +1,17 @@
+(* Submitted by Robert Schneck *)
+
+Parameter A B C D : Prop.
+Axiom X : A -> B -> C /\ D.
+
+Lemma foo : A -> B -> C.
+Proof.
+intros.
+destruct X. (* Should find axiom X and should handle arguments of X *)
+assumption.
+assumption.
+assumption.
+Qed.
+
(* Simplification of bug 711 *)
Parameter f : true = false.
@@ -7,3 +21,5 @@ set (b := true) in *.
(* Check that it doesn't fail with an anomaly *)
(* Ultimately, adapt destruct to make it succeeding *)
try destruct b.
+Abort.
+
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 64875fba..baeec147 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -59,7 +59,7 @@ Check
(* Check instantiation of nested evars (bug #1089) *)
-Check (fun f:(forall (v:Set->Set), v (v nat) -> nat) => f _ (Some (Some O))).
+Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))).
(* This used to fail with anomaly "evar was not declared" in V8.0pl3 *)
diff --git a/test-suite/success/if.v b/test-suite/success/if.v
index 3f763863..9fde95e8 100644
--- a/test-suite/success/if.v
+++ b/test-suite/success/if.v
@@ -3,3 +3,10 @@
Check (fun b : bool => if b then Type else nat).
+(* Check correct use of if-then-else predicate annotation (cf bug 690) *)
+
+Check fun b : bool =>
+ if b as b0 return (if b0 then b0 = true else b0 = false)
+ then refl_equal true
+ else refl_equal false.
+
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index b61cf275..4346ce9a 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -64,3 +64,26 @@ intro P.
refine (P _ _).
reflexivity.
Abort.
+
+(* Submitted by Jacek Chrzaszcz (bug #1102) *)
+
+(* le problme a t rsolu ici par normalisation des evars prsentes
+ dans les types d'evars, mais le problme reste a priori ouvert dans
+ le cas plus gnral d'evars non instancies dans les types d'autres
+ evars *)
+
+Goal exists n:nat, n=n.
+refine (ex_intro _ _ _).
+Abort.
+
+(* Used to failed with error not clean *)
+
+Definition div :
+ forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) ->
+ forall n:nat, {q:nat | x = q*n}.
+refine
+ (fun m div_rec n =>
+ match div_rec m n with
+ | exist _ _ => _
+ end).
+Abort.
diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v
index e3c4dd30..19e306fe 100644
--- a/test-suite/success/unicode_utf8.v
+++ b/test-suite/success/unicode_utf8.v
@@ -4,6 +4,9 @@
(* Check Greek letters *)
Definition test_greek : nat -> nat := fun Δ => Δ.
+Parameter ℝ : Set.
+Parameter π : ℝ.
(* Check indices *)
Definition test_indices : nat -> nat := fun x₁ => x₁.
+Definition π₂ := snd.