diff options
author | 2015-01-25 14:43:16 +0100 | |
---|---|---|
committer | 2015-01-25 14:43:16 +0100 | |
commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /test-suite/bugs/opened/shouldnotfail | |
parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/opened/shouldnotfail')
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1338.v-disabled | 12 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1501.v | 93 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1596.v | 242 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1671.v | 12 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1811.v | 9 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/2310.v | 17 | ||||
-rw-r--r-- | test-suite/bugs/opened/shouldnotfail/743.v | 12 |
7 files changed, 0 insertions, 397 deletions
diff --git a/test-suite/bugs/opened/shouldnotfail/1338.v-disabled b/test-suite/bugs/opened/shouldnotfail/1338.v-disabled deleted file mode 100644 index f383d534..00000000 --- a/test-suite/bugs/opened/shouldnotfail/1338.v-disabled +++ /dev/null @@ -1,12 +0,0 @@ -Require Import Omega. - -Goal forall x, 0 <= x -> x <= 20 -> -x <> 0 - -> x <> 1 -> x <> 2 -> x <> 3 -> x <>4 -> x <> 5 -> x <> 6 -> x <> 7 -> x <> 8 --> x <> 9 -> x <> 10 - -> x <> 11 -> x <> 12 -> x <> 13 -> x <> 14 -> x <> 15 -> x <> 16 -> x <> 17 --> x <> 18 -> x <> 19 -> x <> 20 -> False. -Proof. - intros. - omega. -Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v deleted file mode 100644 index 1845dd1f..00000000 --- a/test-suite/bugs/opened/shouldnotfail/1501.v +++ /dev/null @@ -1,93 +0,0 @@ -Set Implicit Arguments. - - -Require Export Relation_Definitions. -Require Export Setoid. - - -Section Essais. - -(* Parametrized Setoid *) -Parameter K : Type -> Type. -Parameter equiv : forall A : Type, K A -> K A -> Prop. -Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x. -Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x. -Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z --> equiv x z. - -(* basic operations *) -Parameter val : forall A : Type, A -> K A. -Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B. - -Parameter - bind_compat : - forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B), - equiv m1 m2 -> - (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2). - -(* monad axioms *) -Parameter - bind_val_l : - forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a). -Parameter - bind_val_r : - forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m. -Parameter - bind_assoc : - forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C), - equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)). - - -Hint Resolve equiv_refl equiv_sym equiv_trans: monad. - -Add Relation K equiv - reflexivity proved by (@equiv_refl) - symmetry proved by (@equiv_sym) - transitivity proved by (@equiv_trans) - as equiv_rel. - -Definition fequiv (A B: Type) (f g: A -> K B) := forall (x:A), (equiv (f x) (g -x)). - -Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f. -Proof. - unfold fequiv; auto with monad. -Qed. - -Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y -x. -Proof. - unfold fequiv; auto with monad. -Qed. - -Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y -> -fequiv -y z -> fequiv x z. -Proof. - unfold fequiv; intros; eapply equiv_trans; auto with monad. -Qed. - -Add Relation (fun (A B:Type) => A -> K B) fequiv - reflexivity proved by (@fequiv_refl) - symmetry proved by (@fequiv_sym) - transitivity proved by (@fequiv_trans) - as fequiv_rel. - -Add Morphism bind - with signature equiv ==> fequiv ==> equiv - as bind_mor. -Proof. - unfold fequiv; intros; apply bind_compat; auto. -Qed. - -Lemma test: - forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B), - (equiv m1 m2) -> (equiv m2 m3) -> - equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) - (bind m2 (fun a => bind m3 (fun a' => f a a'))). -Proof. - intros A B m1 m2 m3 f H1 H2. - setoid_rewrite H1. (* this works *) - setoid_rewrite H2. - trivial by equiv_refl. -Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v deleted file mode 100644 index de77e35d..00000000 --- a/test-suite/bugs/opened/shouldnotfail/1596.v +++ /dev/null @@ -1,242 +0,0 @@ - -Require Import Relations. -Require Import FSets. -Require Import Arith. - -Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false. - destruct b;try tauto. -Qed. - -Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with -Definition t := (X.t * Y.t)%type. - Definition t := (X.t * Y.t)%type. - - Definition eq (xy1:t) (xy2:t) := - let (x1,y1) := xy1 in - let (x2,y2) := xy2 in - (X.eq x1 x2) /\ (Y.eq y1 y2). - - Definition lt (xy1:t) (xy2:t) := - let (x1,y1) := xy1 in - let (x2,y2) := xy2 in - (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)). - - Lemma eq_refl : forall (x:t),(eq x x). - destruct x. - unfold eq. - split;[apply X.eq_refl | apply Y.eq_refl]. - Qed. - - Lemma eq_sym : forall (x y:t),(eq x y)->(eq y x). - destruct x;destruct y;unfold eq;intro. - elim H;clear H;intros. - split;[apply X.eq_sym | apply Y.eq_sym];trivial. - Qed. - - Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z). - unfold eq;destruct x;destruct y;destruct z;intros. - elim H;clear H;intros. - elim H0;clear H0;intros. - split;[eapply X.eq_trans | eapply Y.eq_trans];eauto. - Qed. - - Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z). - unfold lt;destruct x;destruct y;destruct z;intros. - case H;clear H;intro. - case H0;clear H0;intro. - left. - eapply X.lt_trans;eauto. - elim H0;clear H0;intros. - left. - case (X.compare t0 t4);trivial;intros. - generalize (X.eq_sym H0);intro. - generalize (X.eq_trans e H2);intro. - elim (X.lt_not_eq H H3). - generalize (X.lt_trans l H);intro. - generalize (X.eq_sym H0);intro. - elim (X.lt_not_eq H2 H3). - elim H;clear H;intros. - case H0;clear H0;intro. - left. - case (X.compare t0 t4);trivial;intros. - generalize (X.eq_sym H);intro. - generalize (X.eq_trans H2 e);intro. - elim (X.lt_not_eq H0 H3). - generalize (X.lt_trans H0 l);intro. - generalize (X.eq_sym H);intro. - elim (X.lt_not_eq H2 H3). - elim H0;clear H0;intros. - right. - split. - eauto. - eauto. - Qed. - - Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). - unfold lt, eq;destruct x;destruct y;intro;intro. - elim H0;clear H0;intros. - case H. - intro. - apply (X.lt_not_eq H2 H0). - intro. - elim H2;clear H2;intros. - apply (Y.lt_not_eq H3 H1). - Qed. - - Definition compare : forall (x y:t),(Compare lt eq x y). - destruct x;destruct y. - case (X.compare t0 t2);intro. - apply LT. - left;trivial. - case (Y.compare t1 t3);intro. - apply LT. - right. - tauto. - apply EQ. - split;trivial. - apply GT. - right;auto. - apply GT. - left;trivial. - Defined. - - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. -End OrderedPair. - -Module MessageSpi. - Inductive message : Set := - | MNam : nat -> message. - - Definition t := message. - - Fixpoint message_lt (m n:message) {struct m} : Prop := - match (m,n) with - | (MNam n1,MNam n2) => n1 < n2 - end. - - Module Ord <: OrderedType with Definition t := message with Definition eq := -@eq message. - Definition t := message. - Definition eq := @eq message. - Definition lt := message_lt. - - Lemma eq_refl : forall (x:t),eq x x. - unfold eq;auto. - Qed. - - Lemma eq_sym : forall (x y:t),(eq x y )->(eq y x). - unfold eq;auto. - Qed. - - Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z). - unfold eq;auto;intros;congruence. - Qed. - - Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z). - unfold lt. - induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros. - omega. - Qed. - - Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y). - unfold eq;unfold lt. - induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate -H0);injection H0;intros. - elim (lt_irrefl n);try omega. - Qed. - - Definition compare : forall (x y:t),(Compare lt eq x y). - unfold lt, eq. - induction x;destruct y;intros;try (apply LT;simpl;trivial;fail);try -(apply -GT;simpl;trivial;fail). - case (lt_eq_lt_dec n n0);intros;try (case s;clear s;intros). - apply LT;trivial. - apply EQ;trivial. - rewrite e;trivial. - apply GT;trivial. - Defined. - - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. - End Ord. - - Theorem eq_dec : forall (m n:message),{m=n}+{~(m=n)}. - intros. - case (Ord.compare m n);intro;[right | left | right];try (red;intro). - elim (Ord.lt_not_eq m n);auto. - rewrite e;auto. - elim (Ord.lt_not_eq n m);auto. - Defined. -End MessageSpi. - -Module MessagePair := OrderedPair MessageSpi.Ord MessageSpi.Ord. - -Module Type Hedge := FSetInterface.S with Module E := MessagePair. - -Module A (H:Hedge). - Definition hedge := H.t. - - Definition message_relation := relation MessageSpi.message. - - Definition relation_of_hedge (h:hedge) (m n:MessageSpi.message) := H.In (m,n) -h. - - Inductive hedge_synthesis_relation (h:message_relation) : message_relation := - | SynInc : forall (m n:MessageSpi.message),(h m -n)->(hedge_synthesis_relation h m n). - - Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message) -(n:MessageSpi.message) {struct m} : bool := - if H.mem (m,n) h - then true - else false. - - Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation -(relation_of_hedge h). - - Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall -(m n:MessageSpi.message),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec -h m n). - unfold hedge_synthesis_spec;unfold relation_of_hedge. - induction m;simpl;intro. - elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros. - apply SynInc;apply H.mem_2;trivial. - rewrite H in H0. (* !! possible here !! *) - discriminate H0. - Qed. -End A. - -Module B (H:Hedge). - Definition hedge := H.t. - - Definition message_relation := relation MessageSpi.t. - - Definition relation_of_hedge (h:hedge) (m n:MessageSpi.t) := H.In (m,n) h. - - Inductive hedge_synthesis_relation (h:message_relation) : message_relation := - | SynInc : forall (m n:MessageSpi.t),(h m n)->(hedge_synthesis_relation h m -n). - - Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t) -{struct m} : bool := - if H.mem (m,n) h - then true - else false. - - Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation -(relation_of_hedge h). - - Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall -(m n:MessageSpi.t),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec h m -n). - unfold hedge_synthesis_spec;unfold relation_of_hedge. - induction m;simpl;intro. - elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros. - apply SynInc;apply H.mem_2;trivial. - - rewrite H in H0. (* !! impossible here !! *) - discriminate H0. - Qed. -End B.
\ No newline at end of file diff --git a/test-suite/bugs/opened/shouldnotfail/1671.v b/test-suite/bugs/opened/shouldnotfail/1671.v deleted file mode 100644 index d95c2108..00000000 --- a/test-suite/bugs/opened/shouldnotfail/1671.v +++ /dev/null @@ -1,12 +0,0 @@ -(* Exemple soumis par Pierre Corbineau (bug #1671) *) - -CoInductive hdlist : unit -> Type := -| cons : hdlist tt -> hdlist tt. - -Variable P : forall bo, hdlist bo -> Prop. -Variable all : forall bo l, P bo l. - -Definition F (l:hdlist tt) : P tt l := -match l in hdlist u return P u l with -| cons (cons l') => all tt _ -end. diff --git a/test-suite/bugs/opened/shouldnotfail/1811.v b/test-suite/bugs/opened/shouldnotfail/1811.v deleted file mode 100644 index 037b7cb2..00000000 --- a/test-suite/bugs/opened/shouldnotfail/1811.v +++ /dev/null @@ -1,9 +0,0 @@ -Require Export Bool. - -Lemma neg2xor : forall b, xorb true b = negb b. -Proof. auto. Qed. - -Goal forall b1 b2, (negb b1 = b2) -> xorb true b1 = b2. -Proof. - intros b1 b2. - rewrite neg2xor.
\ No newline at end of file diff --git a/test-suite/bugs/opened/shouldnotfail/2310.v b/test-suite/bugs/opened/shouldnotfail/2310.v deleted file mode 100644 index 8d1a5149..00000000 --- a/test-suite/bugs/opened/shouldnotfail/2310.v +++ /dev/null @@ -1,17 +0,0 @@ -(* Dependent higher-order hole in "refine" (simplified version) *) - -Set Implicit Arguments. - -Inductive Nest t := Cons : Nest (prod t t) -> Nest t. - -Definition cast A x y Heq P H := @eq_rect A x P H y Heq. - -Definition replace a (y:Nest (prod a a)) : a = a -> Nest a. - -(* This used to raise an anomaly Unknown Meta in 8.2 and 8.3beta. - It raises a regular error in 8.3 and almost succeeds with the new - proof engine: there are two solutions to a unification problem - (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either - leave P as subgoal or choose itself one solution *) - -intros. refine (Cons (cast H _ y)). diff --git a/test-suite/bugs/opened/shouldnotfail/743.v b/test-suite/bugs/opened/shouldnotfail/743.v deleted file mode 100644 index f1eee6c1..00000000 --- a/test-suite/bugs/opened/shouldnotfail/743.v +++ /dev/null @@ -1,12 +0,0 @@ -Require Import Omega. - -Lemma foo : forall n m : Z, (n >= 0)%Z -> (n * m >= 0)%Z -> (n <= n + n * m)%Z. -Proof. - intros. omega. -Qed. - -Lemma foo' : forall n m : nat, n <= n + n * m. -Proof. - intros. omega. -Qed. - |