diff options
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/1773.v | 10 | ||||
| -rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1338.v-disabled | 12 | ||||
| -rw-r--r-- | test-suite/bugs/opened/shouldnotfail/1416.v | 27 | ||||
| -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/1811.v | 9 | ||||
| -rw-r--r-- | test-suite/bugs/opened/shouldnotfail/743.v | 12 |
7 files changed, 405 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/1773.v b/test-suite/bugs/opened/1773.v new file mode 100644 index 00000000..4aabf19c --- /dev/null +++ b/test-suite/bugs/opened/1773.v @@ -0,0 +1,10 @@ +Goal forall B C : nat -> nat -> Prop, forall k, C 0 k -> + (exists A, (forall k', C A k' -> B A k') -> B A k). +Proof. + intros B C k H. + econstructor. + intros X. + apply X. + apply H. +Qed. + diff --git a/test-suite/bugs/opened/shouldnotfail/1338.v-disabled b/test-suite/bugs/opened/shouldnotfail/1338.v-disabled new file mode 100644 index 00000000..f383d534 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1338.v-disabled @@ -0,0 +1,12 @@ +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/1416.v b/test-suite/bugs/opened/shouldnotfail/1416.v new file mode 100644 index 00000000..c6f4302d --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1416.v @@ -0,0 +1,27 @@ +Set Implicit Arguments. + +Record Place (Env A: Type) : Type := { + read: Env -> A ; + write: Env -> A -> Env ; + write_read: forall (e:Env), (write e (read e))=e +}. + +Hint Rewrite -> write_read: placeeq. + +Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type := + { + mkEnv: A -> B -> Env ; + mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x) + }. + +(* when the following line is commented, the bug does not appear *) +Hint Rewrite -> mkEnv2writeL: placeeq. + +Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A), + (exists e1:Env, e=(write p e1 (read p e))). +Proof. + intros Env A e p; eapply ex_intro. + autorewrite with placeeq. (* Here is the bug *) + auto. +Qed. + diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v new file mode 100644 index 00000000..85c09dbd --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1501.v @@ -0,0 +1,93 @@ +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 new file mode 100644 index 00000000..766bf524 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1596.v @@ -0,0 +1,242 @@ + +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/1811.v b/test-suite/bugs/opened/shouldnotfail/1811.v new file mode 100644 index 00000000..037b7cb2 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1811.v @@ -0,0 +1,9 @@ +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/743.v b/test-suite/bugs/opened/shouldnotfail/743.v new file mode 100644 index 00000000..f1eee6c1 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/743.v @@ -0,0 +1,12 @@ +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. + |