From db22ae6140259dd065fdd80af4cb3c3bab41c184 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 2 Oct 2018 13:44:46 +0000 Subject: rename test files (do not start by a digit) --- test-suite/bugs/opened/1338.v-disabled | 12 -- test-suite/bugs/opened/1596.v | 260 -------------------------- test-suite/bugs/opened/1615.v | 12 -- test-suite/bugs/opened/1671.v | 12 -- test-suite/bugs/opened/1811.v | 10 - test-suite/bugs/opened/2572.v-disabled | 187 ------------------- test-suite/bugs/opened/3010.v-disabled | 1 - test-suite/bugs/opened/3092.v | 9 - test-suite/bugs/opened/3166.v | 83 --------- test-suite/bugs/opened/3186.v-disabled | 4 - test-suite/bugs/opened/3248.v | 17 -- test-suite/bugs/opened/3277.v | 7 - test-suite/bugs/opened/3278.v | 25 --- test-suite/bugs/opened/3283.v | 28 --- test-suite/bugs/opened/3295.v | 104 ----------- test-suite/bugs/opened/3304.v | 3 - test-suite/bugs/opened/3311.v | 10 - test-suite/bugs/opened/3312.v | 5 - test-suite/bugs/opened/3343.v | 46 ----- test-suite/bugs/opened/3345.v | 145 --------------- test-suite/bugs/opened/3357.v | 9 - test-suite/bugs/opened/3363.v | 26 --- test-suite/bugs/opened/3370.v | 12 -- test-suite/bugs/opened/3395.v | 231 ----------------------- test-suite/bugs/opened/3424.v | 24 --- test-suite/bugs/opened/3459.v | 31 ---- test-suite/bugs/opened/3463.v | 13 -- test-suite/bugs/opened/3478.v-disabled | 8 - test-suite/bugs/opened/3626.v | 7 - test-suite/bugs/opened/3655.v | 9 - test-suite/bugs/opened/3754.v | 284 ----------------------------- test-suite/bugs/opened/3794.v | 7 - test-suite/bugs/opened/3889.v | 11 -- test-suite/bugs/opened/3890.v | 18 -- test-suite/bugs/opened/3919.v-disabled | 13 -- test-suite/bugs/opened/3922.v-disabled | 83 --------- test-suite/bugs/opened/3928.v-disabled | 12 -- test-suite/bugs/opened/3938.v | 6 - test-suite/bugs/opened/3946.v | 11 -- test-suite/bugs/opened/4701.v | 23 --- test-suite/bugs/opened/4721.v | 13 -- test-suite/bugs/opened/4728.v | 72 -------- test-suite/bugs/opened/4755.v | 34 ---- test-suite/bugs/opened/4771.v | 22 --- test-suite/bugs/opened/4778.v | 35 ---- test-suite/bugs/opened/4781.v | 94 ---------- test-suite/bugs/opened/4813.v | 5 - test-suite/bugs/opened/6393.v | 11 -- test-suite/bugs/opened/6602.v | 17 -- test-suite/bugs/opened/bug_1338.v-disabled | 12 ++ test-suite/bugs/opened/bug_1596.v | 260 ++++++++++++++++++++++++++ test-suite/bugs/opened/bug_1615.v | 11 ++ test-suite/bugs/opened/bug_1671.v | 12 ++ test-suite/bugs/opened/bug_1811.v | 10 + test-suite/bugs/opened/bug_2572.v-disabled | 187 +++++++++++++++++++ test-suite/bugs/opened/bug_3010.v-disabled | 1 + test-suite/bugs/opened/bug_3092.v | 9 + test-suite/bugs/opened/bug_3166.v | 83 +++++++++ test-suite/bugs/opened/bug_3186.v-disabled | 4 + test-suite/bugs/opened/bug_3248.v | 17 ++ test-suite/bugs/opened/bug_3277.v | 7 + test-suite/bugs/opened/bug_3278.v | 25 +++ test-suite/bugs/opened/bug_3283.v | 28 +++ test-suite/bugs/opened/bug_3295.v | 104 +++++++++++ test-suite/bugs/opened/bug_3304.v | 3 + test-suite/bugs/opened/bug_3311.v | 10 + test-suite/bugs/opened/bug_3312.v | 5 + test-suite/bugs/opened/bug_3343.v | 46 +++++ test-suite/bugs/opened/bug_3345.v | 145 +++++++++++++++ test-suite/bugs/opened/bug_3357.v | 9 + test-suite/bugs/opened/bug_3363.v | 26 +++ test-suite/bugs/opened/bug_3370.v | 12 ++ test-suite/bugs/opened/bug_3395.v | 231 +++++++++++++++++++++++ test-suite/bugs/opened/bug_3424.v | 24 +++ test-suite/bugs/opened/bug_3459.v | 31 ++++ test-suite/bugs/opened/bug_3463.v | 12 ++ test-suite/bugs/opened/bug_3478.v-disabled | 8 + test-suite/bugs/opened/bug_3626.v | 7 + test-suite/bugs/opened/bug_3655.v | 9 + test-suite/bugs/opened/bug_3754.v | 284 +++++++++++++++++++++++++++++ test-suite/bugs/opened/bug_3794.v | 7 + test-suite/bugs/opened/bug_3889.v | 11 ++ test-suite/bugs/opened/bug_3890.v | 18 ++ test-suite/bugs/opened/bug_3919.v-disabled | 13 ++ test-suite/bugs/opened/bug_3922.v-disabled | 83 +++++++++ test-suite/bugs/opened/bug_3928.v-disabled | 12 ++ test-suite/bugs/opened/bug_3938.v | 6 + test-suite/bugs/opened/bug_3946.v | 11 ++ test-suite/bugs/opened/bug_4701.v | 23 +++ test-suite/bugs/opened/bug_4721.v | 13 ++ test-suite/bugs/opened/bug_4728.v | 72 ++++++++ test-suite/bugs/opened/bug_4755.v | 34 ++++ test-suite/bugs/opened/bug_4771.v | 22 +++ test-suite/bugs/opened/bug_4778.v | 35 ++++ test-suite/bugs/opened/bug_4781.v | 94 ++++++++++ test-suite/bugs/opened/bug_4813.v | 5 + test-suite/bugs/opened/bug_6393.v | 11 ++ test-suite/bugs/opened/bug_6602.v | 17 ++ 98 files changed, 2119 insertions(+), 2121 deletions(-) delete mode 100644 test-suite/bugs/opened/1338.v-disabled delete mode 100644 test-suite/bugs/opened/1596.v delete mode 100644 test-suite/bugs/opened/1615.v delete mode 100644 test-suite/bugs/opened/1671.v delete mode 100644 test-suite/bugs/opened/1811.v delete mode 100644 test-suite/bugs/opened/2572.v-disabled delete mode 100644 test-suite/bugs/opened/3010.v-disabled delete mode 100644 test-suite/bugs/opened/3092.v delete mode 100644 test-suite/bugs/opened/3166.v delete mode 100644 test-suite/bugs/opened/3186.v-disabled delete mode 100644 test-suite/bugs/opened/3248.v delete mode 100644 test-suite/bugs/opened/3277.v delete mode 100644 test-suite/bugs/opened/3278.v delete mode 100644 test-suite/bugs/opened/3283.v delete mode 100644 test-suite/bugs/opened/3295.v delete mode 100644 test-suite/bugs/opened/3304.v delete mode 100644 test-suite/bugs/opened/3311.v delete mode 100644 test-suite/bugs/opened/3312.v delete mode 100644 test-suite/bugs/opened/3343.v delete mode 100644 test-suite/bugs/opened/3345.v delete mode 100644 test-suite/bugs/opened/3357.v delete mode 100644 test-suite/bugs/opened/3363.v delete mode 100644 test-suite/bugs/opened/3370.v delete mode 100644 test-suite/bugs/opened/3395.v delete mode 100644 test-suite/bugs/opened/3424.v delete mode 100644 test-suite/bugs/opened/3459.v delete mode 100644 test-suite/bugs/opened/3463.v delete mode 100644 test-suite/bugs/opened/3478.v-disabled delete mode 100644 test-suite/bugs/opened/3626.v delete mode 100644 test-suite/bugs/opened/3655.v delete mode 100644 test-suite/bugs/opened/3754.v delete mode 100644 test-suite/bugs/opened/3794.v delete mode 100644 test-suite/bugs/opened/3889.v delete mode 100644 test-suite/bugs/opened/3890.v delete mode 100644 test-suite/bugs/opened/3919.v-disabled delete mode 100644 test-suite/bugs/opened/3922.v-disabled delete mode 100644 test-suite/bugs/opened/3928.v-disabled delete mode 100644 test-suite/bugs/opened/3938.v delete mode 100644 test-suite/bugs/opened/3946.v delete mode 100644 test-suite/bugs/opened/4701.v delete mode 100644 test-suite/bugs/opened/4721.v delete mode 100644 test-suite/bugs/opened/4728.v delete mode 100644 test-suite/bugs/opened/4755.v delete mode 100644 test-suite/bugs/opened/4771.v delete mode 100644 test-suite/bugs/opened/4778.v delete mode 100644 test-suite/bugs/opened/4781.v delete mode 100644 test-suite/bugs/opened/4813.v delete mode 100644 test-suite/bugs/opened/6393.v delete mode 100644 test-suite/bugs/opened/6602.v create mode 100644 test-suite/bugs/opened/bug_1338.v-disabled create mode 100644 test-suite/bugs/opened/bug_1596.v create mode 100644 test-suite/bugs/opened/bug_1615.v create mode 100644 test-suite/bugs/opened/bug_1671.v create mode 100644 test-suite/bugs/opened/bug_1811.v create mode 100644 test-suite/bugs/opened/bug_2572.v-disabled create mode 100644 test-suite/bugs/opened/bug_3010.v-disabled create mode 100644 test-suite/bugs/opened/bug_3092.v create mode 100644 test-suite/bugs/opened/bug_3166.v create mode 100644 test-suite/bugs/opened/bug_3186.v-disabled create mode 100644 test-suite/bugs/opened/bug_3248.v create mode 100644 test-suite/bugs/opened/bug_3277.v create mode 100644 test-suite/bugs/opened/bug_3278.v create mode 100644 test-suite/bugs/opened/bug_3283.v create mode 100644 test-suite/bugs/opened/bug_3295.v create mode 100644 test-suite/bugs/opened/bug_3304.v create mode 100644 test-suite/bugs/opened/bug_3311.v create mode 100644 test-suite/bugs/opened/bug_3312.v create mode 100644 test-suite/bugs/opened/bug_3343.v create mode 100644 test-suite/bugs/opened/bug_3345.v create mode 100644 test-suite/bugs/opened/bug_3357.v create mode 100644 test-suite/bugs/opened/bug_3363.v create mode 100644 test-suite/bugs/opened/bug_3370.v create mode 100644 test-suite/bugs/opened/bug_3395.v create mode 100644 test-suite/bugs/opened/bug_3424.v create mode 100644 test-suite/bugs/opened/bug_3459.v create mode 100644 test-suite/bugs/opened/bug_3463.v create mode 100644 test-suite/bugs/opened/bug_3478.v-disabled create mode 100644 test-suite/bugs/opened/bug_3626.v create mode 100644 test-suite/bugs/opened/bug_3655.v create mode 100644 test-suite/bugs/opened/bug_3754.v create mode 100644 test-suite/bugs/opened/bug_3794.v create mode 100644 test-suite/bugs/opened/bug_3889.v create mode 100644 test-suite/bugs/opened/bug_3890.v create mode 100644 test-suite/bugs/opened/bug_3919.v-disabled create mode 100644 test-suite/bugs/opened/bug_3922.v-disabled create mode 100644 test-suite/bugs/opened/bug_3928.v-disabled create mode 100644 test-suite/bugs/opened/bug_3938.v create mode 100644 test-suite/bugs/opened/bug_3946.v create mode 100644 test-suite/bugs/opened/bug_4701.v create mode 100644 test-suite/bugs/opened/bug_4721.v create mode 100644 test-suite/bugs/opened/bug_4728.v create mode 100644 test-suite/bugs/opened/bug_4755.v create mode 100644 test-suite/bugs/opened/bug_4771.v create mode 100644 test-suite/bugs/opened/bug_4778.v create mode 100644 test-suite/bugs/opened/bug_4781.v create mode 100644 test-suite/bugs/opened/bug_4813.v create mode 100644 test-suite/bugs/opened/bug_6393.v create mode 100644 test-suite/bugs/opened/bug_6602.v (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/1338.v-disabled b/test-suite/bugs/opened/1338.v-disabled deleted file mode 100644 index ab0f98202d..0000000000 --- a/test-suite/bugs/opened/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. - Fail omega. -Abort. diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v deleted file mode 100644 index 820022d995..0000000000 --- a/test-suite/bugs/opened/1596.v +++ /dev/null @@ -1,260 +0,0 @@ -Require Import Relations. -Require Import FSets. -Require Import Arith. -Require Import Omega. - -Set Keyed Unification. - -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. - - Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}. - Proof. - intros [xa xb] [ya yb]; simpl. - destruct (X.eq_dec xa ya). - destruct (Y.eq_dec xb yb). - + left; now split. - + right. now intros [eqa eqb]. - + right. now intros [eqa eqb]. - 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. - - Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}. - Proof. - intros [i] [j]. unfold eq. - destruct (eq_nat_dec i j). - + left. now f_equal. - + right. intros meq; now inversion meq. - 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. discriminate. (* !! impossible here !! *) - Qed. -End B. diff --git a/test-suite/bugs/opened/1615.v b/test-suite/bugs/opened/1615.v deleted file mode 100644 index 2825701410..0000000000 --- a/test-suite/bugs/opened/1615.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. Fail omega. -Abort. - diff --git a/test-suite/bugs/opened/1671.v b/test-suite/bugs/opened/1671.v deleted file mode 100644 index b4e653f687..0000000000 --- a/test-suite/bugs/opened/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. - -Fail 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/1811.v b/test-suite/bugs/opened/1811.v deleted file mode 100644 index 57c1744313..0000000000 --- a/test-suite/bugs/opened/1811.v +++ /dev/null @@ -1,10 +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. - Fail rewrite neg2xor. -Abort. diff --git a/test-suite/bugs/opened/2572.v-disabled b/test-suite/bugs/opened/2572.v-disabled deleted file mode 100644 index 3f6c6a0d14..0000000000 --- a/test-suite/bugs/opened/2572.v-disabled +++ /dev/null @@ -1,187 +0,0 @@ -Require Import List. -Definition is_dec (P:Prop) := {P}+{~P}. -Definition eq_dec (T:Type) := forall (t1 t2:T), is_dec (t1=t2). - -Record Label : Type := mkLabel { - LabElem: Type; - LabProd: LabElem -> LabElem -> option LabElem; - LabBot: LabElem -> Prop; - LabError: LabElem -> Prop -}. - -Definition LProd (L1 L2: Label): Label := {| - LabElem := LabElem L1 * LabElem L2; - LabProd := fun lg ld => let (lg1,lg2) := lg in let (ld1,ld2) := ld in - match LabProd L1 lg1 ld1, LabProd L2 lg2 ld2 with - Some g, Some d => Some (g,d) - | _,_ => None - end; - LabBot l := let (l1,l2) := l in LabBot L1 l1 \/ LabBot L2 l2; - LabError l := let (l1,l2) := l in LabError L1 l1 \/ LabError L2 l2 -|}. - -Definition Lrestrict (L: Label) (S: LabElem L -> bool): Label := {| - LabElem := LabElem L; - LabProd l1 l2 := if andb (S l1) (S l2) then LabProd L l1 l2 else None; - LabBot l := LabBot L l; - LabError l := LabError L l -|}. - -Notation "l1 ^* l2" := (LProd l1 l2) (at level 50). - -Record LTS(L:Type): Type := mkLTS { - State: Type; - Init: State -> Prop; - Next: State -> L -> State -> Prop -}. -Implicit Arguments State. -Implicit Arguments Init. -Implicit Arguments Next. - -Definition sound L (S: LTS (LabElem L)): Prop := - forall s s' l, Next S s l s' -> ~LabError L l. - -Inductive PNext L (S1 S2:LTS (LabElem L)): State S1 * State S2 -> (LabElem L) -> State S1 * State S2 -> Prop := - LNext: forall s1 s2 l1 s'1, Next S1 s1 l1 s'1 -> (forall l2, LabProd L l1 l2 = None) -> - PNext L S1 S2 (s1,s2) l1 (s'1,s2) -| RNext: forall s1 s2 l2 s'2, (forall l1, LabProd L l1 l2 = None) -> Next S2 s2 l2 s'2 -> - PNext L S1 S2 (s1,s2) l2 (s1,s'2) -| SNext: forall s1 s2 l1 l2 l s'1 s'2, Next S1 s1 l1 s'1 -> Next S2 s2 l2 s'2 -> - Some l = LabProd L l1 l2 -> PNext L S1 S2 (s1,s2) l (s'1,s'2). - -Definition Produit (L:Label) (S1 S2: LTS (LabElem L)): LTS (LabElem L) := {| - State := State S1 * State S2; - Init := fun s => let (s1,s2) := s in Init S1 s1 /\ Init S2 s2; - Next :=PNext L S1 S2 -|}. - -Parameter Time: Type. -Parameter teq: forall t1 t2:Time, {t1=t2}+{t1<>t2}. - -Inductive TLabElem(L:Type): Type := - Tdiscrete: L -> TLabElem L -| Tdelay: Time -> TLabElem L -| Tbot: TLabElem L. - -Definition TLabel L: Label := {| - LabElem := TLabElem (LabElem L); - LabProd lt1 lt2 := - match lt1, lt2 with - Tdiscrete l1, Tdiscrete l2 => match (LabProd L l1 l2) with Some l => Some (Tdiscrete (LabElem L) l) | None => None end - | Tdelay t1, Tdelay t2 => if teq t1 t2 then Some (Tdelay (LabElem L) t1) else Some (Tbot (LabElem L)) - | _,_ => None - end; - LabBot lt := match lt with - Tdiscrete l => LabBot L l - | Tbot => True - | _ => False - end; - LabError lt := match lt with - Tdiscrete l => LabError L l - | _ => False - end - |}. - -Parameter Var: Type. -Parameter allv: forall P, (forall (v:Var), is_dec (P v)) -> is_dec (forall v, P v). -Parameter DType: Type. -Parameter Data: DType -> Type. -Parameter vtype: Var -> DType. -Parameter Deq: forall t (d1 d2: Data t), is_dec (d1=d2). - -Inductive Vctr(v:Var): Type := - Wctr: Data (vtype v) -> Vctr v -| Rctr: Data (vtype v) -> Vctr v -| Fctr: Vctr v -| Nctr: Vctr v. - -Definition isCmp v (c1 c2: Vctr v): Prop := - match c1,c2 with - Wctr _, Nctr => True - | Rctr _, Rctr _ => True - | Rctr _, Nctr => True - | Rctr _, Fctr => True - | Nctr, _ => True - | _,_ => False - end. - -Lemma isCmp_dec: forall v (c1 c2: Vctr v), is_dec (isCmp v c1 c2). -intros. -induction c1; induction c2; simpl; intros; try (left; tauto); try (right; tauto). -Qed. - -Definition Vprod v (c1 c2: Vctr v): (isCmp v c1 c2) -> Vctr v := - match c1,c2 return isCmp v c1 c2 -> Vctr v with - | Wctr d, Nctr => fun h => Wctr v d - | Rctr d1, Rctr d2 => fun h => if Deq (vtype v) d1 d2 then Rctr v d1 else Fctr v - | Rctr d1, Nctr => fun h => Rctr v d1 - | Rctr d1, Fctr => fun h => Fctr v - | Fctr, Rctr _ => fun h => Fctr v - | Fctr, Fctr => fun h => Fctr v - | Fctr, Nctr => fun h => Fctr v - | Nctr, c2 => fun h => c2 - | _,_ => fun h => match h with end - end. - -Inductive MLabElem: Type := - Mctr: (forall v, Vctr v) -> MLabElem -| Merr: MLabElem. - -Definition MProd (m1 m2: MLabElem): MLabElem := - match m1,m2 with - Mctr c1, Mctr c2 => match allv (fun v => isCmp v (c1 v) (c2 v)) (fun v => isCmp_dec v (c1 v) (c2 v)) with - left h => Mctr (fun v => Vprod v (c1 v) (c2 v) (h v)) - | _ => Merr - end - | _,_ => Merr - end. - -Definition MLabel: Label := {| - LabElem := MLabElem; - LabProd m1 m2 := Some (MProd m1 m2); - LabBot m := exists c, m = Mctr c /\ exists v, c v = Fctr v; - LabError m := m = Merr -|}. - -Parameter Chan: Type. -Parameter ch_eq: eq_dec Chan. - -Definition CLabel(S: Chan->bool): Label := {| - LabElem := Chan; - LabProd := fun c1 c2 => if ch_eq c1 c2 then if S c1 then Some c1 else None else None; - LabBot := fun _ => False; - LabError := fun _ => False -|}. - -Definition FLabel(S: Chan->bool): Label := - TLabel (CLabel S ^* MLabel ^* MLabel ^* MLabel). - -Definition FTS := LTS (LabElem (FLabel (fun _ => true))). -Check (fun S (T1 T2: FTS) => Produit (FLabel S) T1 T2). -(* -Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS. -unfold FTS in *; simpl in *. -apply (Produit (FLabel S)). -apply T1. -apply T2. -Defined. - -Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS := - Produit (FLabel S) T1 T2. -*) -Lemma FTSirrel (S: Chan -> bool): FTS = LTS (LabElem (FLabel S)). -Proof. - unfold FTS. - simpl. - reflexivity. -Qed. - -Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS. -revert T2; revert T1. -rewrite (FTSirrel S). -apply (Produit (FLabel S)). -Defined. - -Record HTTS: Type := mkHTTS { - -}. diff --git a/test-suite/bugs/opened/3010.v-disabled b/test-suite/bugs/opened/3010.v-disabled deleted file mode 100644 index f2906bd6a6..0000000000 --- a/test-suite/bugs/opened/3010.v-disabled +++ /dev/null @@ -1 +0,0 @@ -Definition em {A R} (k : forall s : sum A _, match s with inl x => R x | inr y => R end) := k (inr (fun x => k (inl x))). \ No newline at end of file diff --git a/test-suite/bugs/opened/3092.v b/test-suite/bugs/opened/3092.v deleted file mode 100644 index 9db21d156e..0000000000 --- a/test-suite/bugs/opened/3092.v +++ /dev/null @@ -1,9 +0,0 @@ -Fail Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 := - match H1 with - | le_n => le_n (pred _) - | le_S _ H2 => - match n2 with - | 0 => fun H3 => H3 - | S _ => le_S _ _ - end (le_pred _ _ H2) - end. diff --git a/test-suite/bugs/opened/3166.v b/test-suite/bugs/opened/3166.v deleted file mode 100644 index e1c29a954c..0000000000 --- a/test-suite/bugs/opened/3166.v +++ /dev/null @@ -1,83 +0,0 @@ -Set Asymmetric Patterns. - -Section eq. - Let A := { X : Type & X }. - Let B := (fun x : A => projT1 x). - Let T := (fun (a' : A) (b' : B a') => projT2 a' = b'). - Let T' := T. - Let t1T := (fun _ : A => unit). - Let f1 := (fun x (_ : t1T x) => projT2 x). - Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)). - Let t1T' := t1T. - Let f1' := f1. - Let t1' := t1. - - Theorem eq_matches_commute - a' b' (t' : T a' b') - (rta : forall b'', T' a' b'' -> A) - (rtb : forall b'' t'', B (rta b'' t'')) - (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y))) - (R : forall (b : B (rta b' t')), T _ b -> Type) - (r1 : forall y, R (f1 _ y) (@t1 _ y)) - : match - match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with - | eq_refl => rt1 tt - end - as t0 in (@eq _ _ b0) - return R b0 t0 - with - | eq_refl => r1 tt - end - = - match t' - as t0' in (@eq _ _ b0') - return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type) - (r1 : forall y, R (f1 _ y) (@t1 _ y)), - R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with - | eq_refl => rt1 tt - end)) - with - | eq_refl => fun _ r1 => - match rt1 tt with - | eq_refl => r1 tt - end - end R r1. - Proof. - destruct t'; reflexivity. - Defined. - - Theorem eq_match_beta2 - a b (t : T a b) - X - (R : forall b' (t' : T a b'), X b' -> Type) - (r1 : forall y x, R _ (@t1 _ y) x) - x - : match t as t' in (@eq _ _ b') return forall x, R b' t' x with - | eq_refl => r1 tt - end (x b) - = - match t as t' in (@eq _ _ b') return R b' t' (x b') with - | eq_refl => r1 tt (x _) - end. - Proof. - destruct t; reflexivity. - Defined. -End eq. - -Definition typeof {T} (_ : T) := T. - -Eval compute in (eq_sym (eq_sym _)). -Goal forall T (x y : T) (p : x = y), True. - intros. - pose proof - (@eq_matches_commute - (existT (fun T => T) T x) y p - (fun b'' _ => existT (fun T => T) T b'') - (fun _ _ => x) - (fun _ => eq_refl) - (fun x' _ => x' = y) - (fun _ => eq_refl) - ) as H0. - compute in H0. - change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. - Fail pose proof (fun k => @eq_trans _ _ _ k H0). diff --git a/test-suite/bugs/opened/3186.v-disabled b/test-suite/bugs/opened/3186.v-disabled deleted file mode 100644 index d0bcb920cc..0000000000 --- a/test-suite/bugs/opened/3186.v-disabled +++ /dev/null @@ -1,4 +0,0 @@ -Fixpoint a (_:unit):= -match eq_refl with -|eq_refl => a -end. \ No newline at end of file diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v deleted file mode 100644 index 33c408a28c..0000000000 --- a/test-suite/bugs/opened/3248.v +++ /dev/null @@ -1,17 +0,0 @@ -Ltac ret_and_left f := - let tac := ret_and_left in - let T := type of f in - lazymatch eval hnf in T with - | ?T' -> _ => - let ret := constr:(fun x' : T' => ltac:(tac (f x'))) in - exact ret - | ?T' => exact f - end. - -Goal forall A B : Prop, forall x y : A, True. -Proof. - intros A B x y. - pose (f := fun (x y : A) => conj x y). - pose (a := ltac:(ret_and_left f)). - Fail unify (a x y) (conj x y). -Abort. diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v deleted file mode 100644 index 5f4231363a..0000000000 --- a/test-suite/bugs/opened/3277.v +++ /dev/null @@ -1,7 +0,0 @@ -Tactic Notation "evarr" open_constr(x) := let y := constr:(x) in exact y. - -Goal True. - evarr _. -Admitted. -Goal True. - Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *) diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v deleted file mode 100644 index 1c6deae94b..0000000000 --- a/test-suite/bugs/opened/3278.v +++ /dev/null @@ -1,25 +0,0 @@ -Module a. - Check let x' := _ in - ltac:(exact x'). - - Notation foo x := (let x' := x in ltac:(exact x')). - - Fail Check foo _. (* Error: -Cannot infer an internal placeholder of type "Type" in environment: - -x' := ?42 : ?41 -. *) -End a. - -Module b. - Notation foo x := (let x' := x in let y := (ltac:(exact I) : True) in I). - Notation bar x := (let x' := x in let y := (I : True) in I). - - Check let x' := _ in ltac:(exact I). (* let x' := ?5 in I *) - Check bar _. (* let x' := ?9 in let y := I in I *) - Fail Check foo _. (* Error: -Cannot infer an internal placeholder of type "Type" in environment: - -x' := ?42 : ?41 -. *) -End b. diff --git a/test-suite/bugs/opened/3283.v b/test-suite/bugs/opened/3283.v deleted file mode 100644 index 3ab5416e8c..0000000000 --- a/test-suite/bugs/opened/3283.v +++ /dev/null @@ -1,28 +0,0 @@ -Notation "P |-- Q" := (@eq nat P Q) (at level 80, Q at level 41, no associativity) . -Notation "x &&& y" := (plus x y) (at level 40, left associativity, y at next level) . -Notation "'Ex' x , P " := (plus x P) (at level 65, x at level 99, P at level 80). - -(* Succeed *) -Check _ |-- _ &&& _ -> _. -Check _ |-- _ &&& (Ex _, _ ) -> _. -Check _ |-- (_ &&& Ex _, _ ) -> _. - -(* Why does this fail? *) -Fail Check _ |-- _ &&& Ex _, _ -> _. -(* The command has indeed failed with message: -=> Error: The term "Ex ?17, ?18" has type "nat" -which should be Set, Prop or Type. *) - -(* Just in case something is strange with -> *) -Notation "P ----> Q" := (P -> Q) (right associativity, at level 99, Q at next level). - -(* Succeed *) -Check _ |-- _ &&& _ ----> _. -Check _ |-- _ &&& (Ex _, _ ) ----> _. -Check _ |-- (_ &&& Ex _, _ ) ----> _. - -(* Why does this fail? *) -Fail Check _ |-- _ &&& Ex _, _ ----> _. -(* The command has indeed failed with message: -=> Error: The term "Ex ?31, ?32" has type "nat" -which should be Set, Prop or Type.*) diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v deleted file mode 100644 index c09649de73..0000000000 --- a/test-suite/bugs/opened/3295.v +++ /dev/null @@ -1,104 +0,0 @@ -Require Export Morphisms Setoid. - -Class lops := lmk_ops { - car: Type; - weq: relation car -}. - -Arguments car : clear implicits. - -Coercion car: lops >-> Sortclass. - -Instance weq_Equivalence `{lops}: Equivalence weq. -Proof. -Admitted. - -Module lset. -Canonical Structure lset_ops A := lmk_ops (list A) (fun h k => True). -End lset. - -Class ops := mk_ops { - ob: Type; - mor: ob -> ob -> lops; - dot: forall n m p, mor n m -> mor m p -> mor n p -}. -Coercion mor: ops >-> Funclass. -Arguments ob : clear implicits. - -Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p). -Proof. -Admitted. - -Section s. - -Import lset. - -Context `{X:lops} {I: Type}. - -Axiom sup : forall (f: I -> X) (J : list I), X. - -Global Instance sup_weq: Proper (pointwise_relation _ weq ==> weq ==> weq) sup. -Proof. -Admitted. - -End s. - -Axiom ord : forall (n : nat), Type. -Axiom seq : forall n, list (ord n). - -Infix "==" := weq (at level 79). -Infix "*" := (dot _ _ _) (left associativity, at level 40). - -Notation "∑_ ( i ∈ l ) f" := (@sup (mor _ _) _ (fun i => f) l) - (at level 41, f at level 41, i, l at level 50). - -Axiom dotxsum : forall `{X : ops} I J n m p (f: I -> X m n) (x: X p m) y, - x * (∑_(i∈ J) f i) == y. - -Definition mx X n m := ord n -> ord m -> X. - -Section bsl. -Context `{X : ops} {u: ob X}. -Notation U := (car (@mor X u u)). - -Lemma toto n m p q (M : mx U n m) N (P : mx U p q) Q i j : ∑_(j0 ∈ seq m) M i j0 * (∑_(j1 ∈ seq p) N j0 j1 * P j1 j) == Q. -Proof. - Fail setoid_rewrite dotxsum. - (* Toplevel input, characters 0-22: -Error: -Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints. -Unable to satisfy the following constraints: -UNDEFINED EVARS: - ?101==[X u n m p q M N P Q i j j0 |- U] (goal evar) - ?106==[X u n m p q M N P Q i j |- relation (X u u)] (internal placeholder) - ?107==[X u n m p q M N P Q i j |- relation (list (ord m))] - (internal placeholder) - ?108==[X u n m p q M N P Q i j (do_subrelation:=do_subrelation) - |- Proper (pointwise_relation (ord m) weq ==> ?107 ==> ?106) sup] - (internal placeholder) - ?109==[X u n m p q M N P Q i j |- ProperProxy ?107 (seq m)] - (internal placeholder) - ?110==[X u n m p q M N P Q i j |- relation (X u u)] (internal placeholder) - ?111==[X u n m p q M N P Q i j (do_subrelation:=do_subrelation) - |- Proper (?106 ==> ?110 ==> Basics.flip Basics.impl) weq] - (internal placeholder) - ?112==[X u n m p q M N P Q i j |- ProperProxy ?110 Q] (internal placeholder)UNIVERSES: - {} |= Top.14 <= Top.37 - Top.25 <= Top.24 - Top.25 <= Top.32 - -ALGEBRAIC UNIVERSES:{} -UNDEFINED UNIVERSES:METAS: - 470[y] := ?101 : car (?99 ?467 ?465) - 469[x] := M i _UNBOUND_REL_1 : car (?99 ?467 ?466) [type is checked] - 468[f] := fun i : ?463 => N _UNBOUND_REL_2 i * P i j : - ?463 -> ?99 ?466 ?465 [type is checked] - 467[p] := u : ob ?99 [type is checked] - 466[m] := u : ob ?99 [type is checked] - 465[n] := u : ob ?99 [type is checked] - 464[J] := seq p : list ?463 [type is checked] - 463[I] := ord p : Type [type is checked] - *) -Abort. - -End bsl. diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v deleted file mode 100644 index 66668930c7..0000000000 --- a/test-suite/bugs/opened/3304.v +++ /dev/null @@ -1,3 +0,0 @@ -Fail Notation "( x , y , .. , z )" := ltac:(let r := constr:(prod .. (prod x y) .. z) in r). -(* The command has indeed failed with message: -=> Error: Special token .. is for use in the Notation command. *) diff --git a/test-suite/bugs/opened/3311.v b/test-suite/bugs/opened/3311.v deleted file mode 100644 index 1c66bc1e55..0000000000 --- a/test-suite/bugs/opened/3311.v +++ /dev/null @@ -1,10 +0,0 @@ -Require Import Setoid. -Axiom bar : True = False. -Goal True. - Fail setoid_rewrite bar. (* Toplevel input, characters 15-33: -Error: -Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints. - -Could not find an instance for "subrelation eq (Basics.flip Basics.impl)". -With the following constraints: -?3 : "True" *) diff --git a/test-suite/bugs/opened/3312.v b/test-suite/bugs/opened/3312.v deleted file mode 100644 index 749921e2f6..0000000000 --- a/test-suite/bugs/opened/3312.v +++ /dev/null @@ -1,5 +0,0 @@ -Require Import Setoid. -Axiom bar : 0 = 1. -Goal 0 = 1. - Fail rewrite_strat bar. (* Toplevel input, characters 15-32: -Error: Tactic failure:setoid rewrite failed: Nothing to rewrite. *) diff --git a/test-suite/bugs/opened/3343.v b/test-suite/bugs/opened/3343.v deleted file mode 100644 index 6c5a85f9cf..0000000000 --- a/test-suite/bugs/opened/3343.v +++ /dev/null @@ -1,46 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 13699 lines to 656 lines, then from 584 lines to 200 lines *) -Set Asymmetric Patterns. -Require Export Coq.Lists.List. -Export List.ListNotations. - -Record CFGV := { Terminal : Type; VarSym : Type }. - -Section Gram. - Context {G : CFGV}. - - Inductive Pattern : (Terminal G) -> Type := - | ptleaf : forall (T : Terminal G), - nat -> Pattern T - with Mixture : list (Terminal G) -> Type := - | mtcons : forall {h: Terminal G} - {tl: list (Terminal G)}, - Pattern h -> Mixture tl -> Mixture (h::tl). - - Variable vc : VarSym G. - - Fixpoint pBVars {gs} (p : Pattern gs) : (list nat) := - match p with - | ptleaf _ _ => [] - end - with mBVars {lgs} (pts : Mixture lgs) : (list nat) := - match pts with - | mtcons _ _ _ tl => mBVars tl - end. - - Lemma mBndngVarsAsNth : - forall mp (m : @Mixture mp), - mBVars m = [2]. - Proof. - intros. - induction m. progress simpl. - Admitted. -End Gram. - -Lemma mBndngVarsAsNth' {G : CFGV} { vc : VarSym G} : - forall mp (m : @Mixture G mp), - mBVars m = [2]. -Proof. - intros. - induction m. - Fail progress simpl. - (* simpl did nothing here, while it does something inside the section; this is probably a bug*) diff --git a/test-suite/bugs/opened/3345.v b/test-suite/bugs/opened/3345.v deleted file mode 100644 index 3e3da6df71..0000000000 --- a/test-suite/bugs/opened/3345.v +++ /dev/null @@ -1,145 +0,0 @@ -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from original input, then from 1972 lines to 136 lines, then from 119 lines to 105 lines *) -Global Set Implicit Arguments. -Require Import Coq.Lists.List Program. -Section IndexBound. - Context {A : Set}. - Class IndexBound (a : A) (Bound : list A) := - { ibound :> nat; - boundi : nth_error Bound ibound = Some a}. - Global Arguments ibound [a Bound] _ . - Global Arguments boundi [a Bound] _. - Record BoundedIndex (Bound : list A) := { bindex :> A; indexb :> IndexBound bindex Bound }. -End IndexBound. -Context {A : Type} {C : Set}. -Variable (projAC : A -> C). -Lemma None_neq_Some -: forall (AnyT AnyT' : Type) (a : AnyT), - None = Some a -> AnyT'. - admit. -Defined. -Program Definition nth_Bounded' - (Bound : list A) - (c : C) - (a_opt : option A) - (nth_n : option_map projAC a_opt = Some c) -: A := match a_opt as x - return (option_map projAC x = Some c) -> A with - | Some a => fun _ => a - | None => fun f : None = Some _ => ! - end nth_n. -Lemma nth_error_map : - forall n As c_opt, - nth_error (map projAC As) n = c_opt - -> option_map projAC (nth_error As n) = c_opt. - admit. -Defined. -Definition nth_Bounded - (Bound : list A) - (idx : BoundedIndex (map projAC Bound)) -: A := nth_Bounded' Bound (nth_error Bound (ibound idx)) - (nth_error_map _ _ (boundi idx)). -Program Definition nth_Bounded_ind2 - (P : forall As, BoundedIndex (map projAC As) - -> BoundedIndex (map projAC As) - -> A -> A -> Prop) -: forall (Bound : list A) - (idx : BoundedIndex (map projAC Bound)) - (idx' : BoundedIndex (map projAC Bound)), - match nth_error Bound (ibound idx), nth_error Bound (ibound idx') with - | Some a, Some a' => P Bound idx idx' a a' - | _, _ => True - end - -> P Bound idx idx' (nth_Bounded _ idx) (nth_Bounded _ idx'):= - fun Bound idx idx' => - match (nth_error Bound (ibound idx)) as e, (nth_error Bound (ibound idx')) as e' - return - (forall (f : option_map _ e = Some (bindex idx)) - (f' : option_map _ e' = Some (bindex idx')), - (match e, e' with - | Some a, Some a' => P Bound idx idx' a a' - | _, _ => True - end) - -> P Bound idx idx' - (match e as e'' return - option_map _ e'' = Some (bindex idx) - -> A - with - | Some a => fun _ => a - | _ => fun f => _ - end f) - (match e' as e'' return - option_map _ e'' = Some (bindex idx') - -> A - with - | Some a => fun _ => a - | _ => fun f => _ - end f')) with - | Some a, Some a' => fun _ _ H => _ - | _, _ => fun f => _ - end (nth_error_map _ _ (boundi idx)) - (nth_error_map _ _ (boundi idx')). - -Lemma nth_Bounded_eq -: forall (Bound : list A) - (idx idx' : BoundedIndex (map projAC Bound)), - ibound idx = ibound idx' - -> nth_Bounded Bound idx = nth_Bounded Bound idx'. -Proof. - intros. - eapply nth_Bounded_ind2 with (idx := idx) (idx' := idx'). - simpl. - (* The [case_eq] should not Fail. More importantly, [Fail case_eq ...] should succeed if [case_eq ...] fails. It doesn't!!! So I resort to [Fail Fail try (case_eq ...)]. *) - Fail Fail try (case_eq (nth_error Bound (ibound idx'))). -(* Toplevel input, characters 15-54: -In nested Ltac calls to "case_eq" and "pattern x at - 1", last call failed. -Error: The abstracted term -"fun e : Exc A => - forall e0 : nth_error Bound (ibound idx') = e, - match - nth_error Bound (ibound idx) as anonymous'0 - return (anonymous'0 = nth_error Bound (ibound idx) -> e = e -> Prop) - with - | Some a => - match - e as anonymous' - return - (Some a = nth_error Bound (ibound idx) -> anonymous' = e -> Prop) - with - | Some a' => - fun (_ : Some a = nth_error Bound (ibound idx)) (_ : Some a' = e) => - a = a' - | None => - fun (_ : Some a = nth_error Bound (ibound idx)) (_ : None = e) => - True - end - | None => fun (_ : None = nth_error Bound (ibound idx)) (_ : e = e) => True - end eq_refl e0" is not well typed. -Illegal application: -The term - "match - nth_error Bound (ibound idx) as anonymous'0 - return (anonymous'0 = nth_error Bound (ibound idx) -> e = e -> Prop) - with - | Some a => - match - e as anonymous' - return - (Some a = nth_error Bound (ibound idx) -> anonymous' = e -> Prop) - with - | Some a' => - fun (_ : Some a = nth_error Bound (ibound idx)) (_ : Some a' = e) => - a = a' - | None => - fun (_ : Some a = nth_error Bound (ibound idx)) (_ : None = e) => - True - end - | None => fun (_ : None = nth_error Bound (ibound idx)) (_ : e = e) => True - end" of type - "nth_error Bound (ibound idx) = nth_error Bound (ibound idx) -> - e = e -> Prop" -cannot be applied to the terms - "eq_refl" : "nth_error Bound (ibound idx) = nth_error Bound (ibound idx)" - "e0" : "nth_error Bound (ibound idx') = e" -The 2nd term has type "nth_error Bound (ibound idx') = e" -which should be coercible to "e = e". *) diff --git a/test-suite/bugs/opened/3357.v b/test-suite/bugs/opened/3357.v deleted file mode 100644 index c479158877..0000000000 --- a/test-suite/bugs/opened/3357.v +++ /dev/null @@ -1,9 +0,0 @@ -Notation D1 := (forall {T : Type} ( x : T ) , Type). - -Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1. -Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33: -Error: In environment -A : forall T : Type, T -> Type -The term "1" has type "nat" while it is expected to have type -"Type". - *) diff --git a/test-suite/bugs/opened/3363.v b/test-suite/bugs/opened/3363.v deleted file mode 100644 index 800d89573c..0000000000 --- a/test-suite/bugs/opened/3363.v +++ /dev/null @@ -1,26 +0,0 @@ -(** In this file, either all four [Check]s should fail, or all four should succeed. *) -Module A. - Section HexStrings. - Require Import String. - End HexStrings. - Fail Check string. -End A. - -Module B. - Section HexStrings. - Require String. - Import String. - End HexStrings. - Fail Check string. -End B. - -Section HexStrings. - Require String. - Import String. -End HexStrings. -Fail Check string. - -Section HexStrings'. - Require Import String. -End HexStrings'. -Check string. diff --git a/test-suite/bugs/opened/3370.v b/test-suite/bugs/opened/3370.v deleted file mode 100644 index 4964bf96c0..0000000000 --- a/test-suite/bugs/opened/3370.v +++ /dev/null @@ -1,12 +0,0 @@ -Require Import String. - -Local Ltac set_strings := - let s := match goal with |- context[String ?s1 ?s2] => constr:(String s1 s2) end in - let H := fresh s in - set (H := s). - -Local Open Scope string_scope. - -Goal "asdf" = "bds". -Fail set_strings. (* Error: Ltac variable s is bound to "asdf" which cannot be coerced to -a fresh identifier. *) diff --git a/test-suite/bugs/opened/3395.v b/test-suite/bugs/opened/3395.v deleted file mode 100644 index 5ca48fc9d6..0000000000 --- a/test-suite/bugs/opened/3395.v +++ /dev/null @@ -1,231 +0,0 @@ -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) -Generalizable All Variables. -Set Implicit Arguments. - -Arguments fst {_ _} _. -Arguments snd {_ _} _. - -Axiom cheat : forall {T}, T. - -Reserved Notation "g 'o' f" (at level 40, left associativity). - -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. -Arguments idpath {A a} , [A] a. -Notation "x = y" := (paths x y) : type_scope. - -Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x - := match p with idpath => idpath end. - -Delimit Scope morphism_scope with morphism. -Delimit Scope category_scope with category. -Delimit Scope object_scope with object. -Record PreCategory (object : Type) := - Build_PreCategory' { - object :> Type := object; - morphism : object -> object -> Type; - identity : forall x, morphism x x; - compose : forall s d d', - morphism d d' - -> morphism s d - -> morphism s d' - where "f 'o' g" := (compose f g); - associativity : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - (m3 o m2) o m1 = m3 o (m2 o m1); - associativity_sym : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - m3 o (m2 o m1) = (m3 o m2) o m1; - left_identity : forall a b (f : morphism a b), identity b o f = f; - right_identity : forall a b (f : morphism a b), f o identity a = f; - identity_identity : forall x, identity x o identity x = identity x - }. -Bind Scope category_scope with PreCategory. -Arguments PreCategory {_}. -Arguments identity {_} [!C%category] x%object : rename. - -Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. - -Infix "o" := compose : morphism_scope. - -Delimit Scope functor_scope with functor. -Local Open Scope morphism_scope. -Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := - { - object_of :> C -> D; - morphism_of : forall s d, morphism C s d - -> morphism D (object_of s) (object_of d); - composition_of : forall s d d' - (m1 : morphism C s d) (m2: morphism C d d'), - morphism_of _ _ (m2 o m1) - = (morphism_of _ _ m2) o (morphism_of _ _ m1); - identity_of : forall x, morphism_of _ _ (identity x) - = identity (object_of x) - }. -Bind Scope functor_scope with Functor. - -Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. - -Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. - -Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := - { - morphism_inverse : morphism C d s; - left_inverse : morphism_inverse o m = identity _; - right_inverse : m o morphism_inverse = identity _ - }. - -Definition opposite `(C : @PreCategory objC) : PreCategory - := @Build_PreCategory' - C - (fun s d => morphism C d s) - (identity (C := C)) - (fun _ _ _ m1 m2 => m2 o m1) - (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) - (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) - (fun _ _ => @right_identity _ _ _ _) - (fun _ _ => @left_identity _ _ _ _) - (@identity_identity _ C). - -Notation "C ^op" := (opposite C) (at level 3) : category_scope. - -Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). - refine (@Build_PreCategory' - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) - * morphism D (snd s) (snd d))%type) - (fun x => (identity (fst x), identity (snd x))) - (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) - _ - _ - _ - _ - _); admit. -Defined. -Infix "*" := prod : category_scope. - -Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E - := Build_Functor - C E - (fun c => G (F c)) - (fun _ _ m => morphism_of G (morphism_of F m)) - cheat - cheat. - -Infix "o" := compose_functor : functor_scope. - -Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := - Build_NaturalTransformation' { - components_of :> forall c, morphism D (F c) (G c); - commutes : forall s d (m : morphism C s d), - components_of d o F _1 m = G _1 m o components_of s; - - commutes_sym : forall s d (m : C.(morphism) s d), - G _1 m o components_of s = components_of d o F _1 m - }. -Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory - := @Build_PreCategory' (Functor C D) - (@NaturalTransformation _ C _ D) - cheat - cheat - cheat - cheat - cheat - cheat - cheat. - -Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op - := Build_Functor (C^op) (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). - -Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op - := Build_Functor C (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). -Notation "F ^op" := (opposite_functor F) : functor_scope. - -Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. -Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C - := Build_Functor (C * D) C - (@fst _ _) - (fun _ _ => @fst _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). - -Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D - := Build_Functor (C * D) D - (@snd _ _) - (fun _ _ => @snd _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). -Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') -: Functor C (D * D') - := Build_Functor - C (D * D') - (fun c => (F c, F' c)) - (fun s d m => (F _1 m, F' _1 m))%morphism - cheat - cheat. -Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') - := (prod_functor (F o fst) (F' o snd))%functor. -Notation cat_of obj := - (@Build_PreCategory' obj - (fun x y => forall _ : x, y) - (fun _ x => x) - (fun _ _ _ f g x => f (g x))%core - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ => idpath)). - -Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) - := Build_Functor _ _ cheat cheat cheat cheat. - -Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) -: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) - := Build_NaturalTransformation' _ _ cheat cheat cheat. - -Class IsFullyFaithful `(F : @Functor objC C objD D) - := is_fully_faithful - : forall x y : C, - IsIsomorphism (induced_hom_natural_transformation F (x, y)). - -Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) - := cheat. - -Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) - := (((coyoneda A^op)^op'L)^op'L)%functor. -Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). -Admitted. - -Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda. - Time let t := (type of CYE) in - let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) - Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). - Time let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) -Fail Timeout 2 Defined. -Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) - -Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda; simpl in *. - Fail Timeout 1 exact CYE. - Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) diff --git a/test-suite/bugs/opened/3424.v b/test-suite/bugs/opened/3424.v deleted file mode 100644 index d1c5bb68f9..0000000000 --- a/test-suite/bugs/opened/3424.v +++ /dev/null @@ -1,24 +0,0 @@ -Set Universe Polymorphism. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }. -Inductive trunc_index : Type := minus_two | trunc_S (x : trunc_index). -Bind Scope trunc_scope with trunc_index. -Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := - match n with - | minus_two => Contr_internal A - | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) - end. -Notation minus_one:=(trunc_S minus_two). -Notation "0" := (trunc_S minus_one) : trunc_scope. -Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. -Notation IsHProp := (IsTrunc minus_one). -Notation IsHSet := (IsTrunc 0). -Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. -Proof. -intros. -eexists. -(* exact (H' a b). *) -(* Undo. *) -Fail apply (H' a b). -exact (H' a b). -Qed. diff --git a/test-suite/bugs/opened/3459.v b/test-suite/bugs/opened/3459.v deleted file mode 100644 index 762611f751..0000000000 --- a/test-suite/bugs/opened/3459.v +++ /dev/null @@ -1,31 +0,0 @@ -(* Bad interaction between clear and the typability of ltac constr bindings *) - -(* Original report *) - -Goal 1 = 2. -Proof. -(* This line used to fail with a Not_found up to some point, and then - to produce an ill-typed term *) -match goal with - | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in - clear x; - exact r)) in - pose y -end. -(* Add extra test for typability (should not fail when bug closed) *) -Fail match goal with P:?c |- _ => try (let x := type of c in idtac) || fail 2 end. -Abort. - -(* Second report raising a Not_found at the time of 21 Oct 2014 *) - -Section F. - -Variable x : nat. - -Goal True. -evar (e : Prop). -assert e. -Fail let r := constr:(eq_refl x) in clear x; exact r. -Abort. - -End F. diff --git a/test-suite/bugs/opened/3463.v b/test-suite/bugs/opened/3463.v deleted file mode 100644 index 541db37fb7..0000000000 --- a/test-suite/bugs/opened/3463.v +++ /dev/null @@ -1,13 +0,0 @@ -Tactic Notation "test1" open_constr(t) ident(r):= - pose t. -Tactic Notation "test2" constr(r) open_constr(t):= - pose t. -Tactic Notation "test3" open_constr(t) constr(r):= - pose t. - -Goal True. - test1 (1 + _) nat. - test2 nat (1 + _). - test3 (1 + _) nat. - test3 (1 + _ : nat) nat. - diff --git a/test-suite/bugs/opened/3478.v-disabled b/test-suite/bugs/opened/3478.v-disabled deleted file mode 100644 index cc926b2167..0000000000 --- a/test-suite/bugs/opened/3478.v-disabled +++ /dev/null @@ -1,8 +0,0 @@ -Set Primitive Projections. -Record foo := { foom :> Type }. -Canonical Structure default_foo := fun T => {| foom := T |}. -Record bar T := { bar1 : T }. -Goal forall (s : foo) (x : foom s), True. -Proof. - intros. - Timeout 1 pose (x : bar _) as x'. \ No newline at end of file diff --git a/test-suite/bugs/opened/3626.v b/test-suite/bugs/opened/3626.v deleted file mode 100644 index 46a6c009eb..0000000000 --- a/test-suite/bugs/opened/3626.v +++ /dev/null @@ -1,7 +0,0 @@ -Set Implicit Arguments. -Set Primitive Projections. -Record prod A B := pair { fst : A ; snd : B }. - -Fail Goal forall x y : prod Set Set, x.(@fst) = y.(@fst). -(* intros. - apply f_equal. *) diff --git a/test-suite/bugs/opened/3655.v b/test-suite/bugs/opened/3655.v deleted file mode 100644 index 841f77febb..0000000000 --- a/test-suite/bugs/opened/3655.v +++ /dev/null @@ -1,9 +0,0 @@ -Ltac bar x := pose x. -Tactic Notation "foo" open_constr(x) := bar x. -Class baz := { baz' : Type }. -Goal True. -(* Original error was an anomaly which is fixed; now, it succeeds but - leaving an evar, while calling pose would not leave an evar, so I - guess it is still a bug in the sense that the semantics of pose is - not preserved *) - foo baz'. diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v deleted file mode 100644 index a717bbe735..0000000000 --- a/test-suite/bugs/opened/3754.v +++ /dev/null @@ -1,284 +0,0 @@ -Unset Strict Universe Declaration. -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *) -(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1 - coqtop version trunk (October 2014) *) - -Notation Type0 := Set. - -Notation idmap := (fun x => x). - -Notation "( x ; y )" := (existT _ x y) : fibration_scope. -Open Scope fibration_scope. - -Notation pr1 := projT1. - -Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. - -Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := - fun x => g (f x). - -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. -Open Scope function_scope. - -Inductive paths {A : Type} (a : A) : A -> Type := - idpath : paths a a. - -Arguments idpath {A a} , [A] a. - -Notation "x = y :> A" := (@paths A x y) : type_scope. -Notation "x = y" := (x = y :>_) : type_scope. -Definition inverse {A : Type} {x y : A} (p : x = y) : y = x. -admit. -Defined. - -Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := - match p, q with idpath, idpath => idpath end. - -Notation "1" := idpath : path_scope. - -Notation "p @ q" := (concat p q) (at level 20) : path_scope. - -Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope. - -Notation "p @' q" := (concat p q) (at level 21, left associativity, - format "'[v' p '/' '@'' q ']'") : long_path_scope. -Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y. -exact (match p with idpath => u end). -Defined. - -Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. -Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y. -exact (match p with idpath => idpath end). -Defined. - -Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) - := forall x:A, f x = g x. - -Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. - -Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := - forall x : A, r (s x) = x. - -Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { - equiv_inv : B -> A ; - eisretr : Sect equiv_inv f; - eissect : Sect f equiv_inv; - eisadj : forall x : A, eisretr (f x) = ap f (eissect x) -}. - -Arguments eisretr {A B} f {_} _. - -Record Equiv A B := BuildEquiv { - equiv_fun : A -> B ; - equiv_isequiv : IsEquiv equiv_fun -}. - -Coercion equiv_fun : Equiv >-> Funclass. - -Global Existing Instance equiv_isequiv. - -Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope. - -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. - -Class Contr_internal (A : Type) := BuildContr { - center : A ; - contr : (forall y : A, center = y) -}. - -Inductive trunc_index : Type := -| minus_two : trunc_index -| trunc_S : trunc_index -> trunc_index. - -Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. -Local Open Scope trunc_scope. -Notation "-2" := minus_two (at level 0) : trunc_scope. -Notation "-1" := (-2.+1) (at level 0) : trunc_scope. - -Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := - match n with - | -2 => Contr_internal A - | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) - end. - -Class IsTrunc (n : trunc_index) (A : Type) : Type := - Trunc_is_trunc : IsTrunc_internal n A. -Notation IsHProp := (IsTrunc -1). - -Monomorphic Axiom dummy_funext_type : Type0. -Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. - -Local Open Scope path_scope. - -Definition concat_p1 {A : Type} {x y : A} (p : x = y) : - p @ 1 = p - := - match p with idpath => 1 end. - -Definition concat_1p {A : Type} {x y : A} (p : x = y) : - 1 @ p = p - := - match p with idpath => 1 end. - -Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : - p @ (q @ r) = (p @ q) @ r := - match r with idpath => - match q with idpath => - match p with idpath => 1 - end end end. - -Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : - (p @ q) @ r = p @ (q @ r) := - match r with idpath => - match q with idpath => - match p with idpath => 1 - end end end. - -Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : - r^ @ q = p -> q = r @ p. -admit. -Defined. - -Ltac with_rassoc tac := - repeat rewrite concat_pp_p; - tac; - - repeat rewrite concat_p_pp. - -Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp). - -Definition ap_p_pp {A B : Type} (f : A -> B) {w : B} {x y z : A} - (r : w = f x) (p : x = y) (q : y = z) : - r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q). -admit. -Defined. - -Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) : - ap (g o f) p = ap g (ap f p) - := - match p with idpath => 1 end. - -Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) : - (ap f q) @ (p y) = (p x) @ (ap g q) - := - match q with - | idpath => concat_1p _ @ ((concat_p1 _) ^) - end. - -Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type) - {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) - : D x2 (p # y) (p # z) - := - match p with idpath => w end. -Local Open Scope equiv_scope. - -Definition transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} - {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) (y : B x2) - : (transport (fun x => B x -> C) p f) y = f (p^ # y). -admit. -Defined. - -Definition transport_arrow_fromconst {A B : Type} {C : A -> Type} - {x1 x2 : A} (p : x1 = x2) (f : B -> C x1) (y : B) - : (transport (fun x => B -> C x) p f) y = p # (f y). -admit. -Defined. - -Definition ap_transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} - {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2) - : ap (transport (fun x => B x -> C) p f) q - @ transport_arrow_toconst p f y2 - = transport_arrow_toconst p f y1 - @ ap (fun y => f (p^ # y)) q. -admit. -Defined. - -Class Univalence. -Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B). -admit. -Defined. -Definition transport_path_universe - {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A) - : transport (fun X:Type => X) (path_universe f) z = f z. -admit. -Defined. -Definition transport_path_universe_V `{Funext} - {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B) - : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z. -admit. -Defined. - -Ltac simpl_do_clear tac term := - let H := fresh in - assert (H := term); - simpl in H |- *; - tac H; - clear H. - -Tactic Notation "simpl" "rewrite" constr(term) := simpl_do_clear ltac:(fun H => rewrite H) term. - -Global Instance Univalence_implies_Funext `{Univalence} : Funext. -Admitted. - -Section Factorization. - - Context {class1 class2 : forall (X Y : Type@{i}), (X -> Y) -> Type@{i}} - `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class1 _ _ g)} - `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class2 _ _ g)} - {A B : Type@{i}} {f : A -> B}. - - Record Factorization := - { intermediate : Type ; - factor1 : A -> intermediate ; - factor2 : intermediate -> B ; - fact_factors : factor2 o factor1 == f ; - inclass1 : class1 _ _ factor1 ; - inclass2 : class2 _ _ factor2 - }. - - Record PathFactorization {fact fact' : Factorization} := - { path_intermediate : intermediate fact <~> intermediate fact' ; - path_factor1 : path_intermediate o factor1 fact == factor1 fact' ; - path_factor2 : factor2 fact == factor2 fact' o path_intermediate ; - path_fact_factors : forall a, path_factor2 (factor1 fact a) - @ ap (factor2 fact') (path_factor1 a) - @ fact_factors fact' a - = fact_factors fact a - }. - Context `{Univalence} {fact fact' : Factorization} - (pf : @PathFactorization fact fact'). - - Let II := path_intermediate pf. - Let ff1 := path_factor1 pf. - Let ff2 := path_factor2 pf. -Local Definition II' : intermediate fact = intermediate fact'. -admit. -Defined. - - Local Definition fff' (a : A) - : (transportD2 (fun X => A -> X) (fun X => X -> B) - (fun X g h => {_ : forall a : A, h (g a) = f a & - {_ : class1 A X g & class2 X B h}}) - II' (factor1 fact) (factor2 fact) - (fact_factors fact; (inclass1 fact; inclass2 fact))).1 a = - ap (transport (fun X => X -> B) II' (factor2 fact)) - (transport_arrow_fromconst II' (factor1 fact) a - @ transport_path_universe II (factor1 fact a) - @ ff1 a) - @ transport_arrow_toconst II' (factor2 fact) (factor1 fact' a) - @ ap (factor2 fact) (transport_path_universe_V II (factor1 fact' a)) - @ ff2 (II^-1 (factor1 fact' a)) - @ ap (factor2 fact') (eisretr II (factor1 fact' a)) - @ fact_factors fact' a. - Proof. - - Open Scope long_path_scope. - - rewrite (ap_transport_arrow_toconst (B := idmap) (C := B)). - - simpl rewrite (@ap_compose _ _ _ (transport idmap (path_universe II)^) - (factor2 fact)). - rewrite <- ap_p_pp; rewrite_moveL_Mp_p. - Set Debug Tactic Unification. - Fail rewrite (concat_Ap ff2). diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v deleted file mode 100644 index e4711a38c0..0000000000 --- a/test-suite/bugs/opened/3794.v +++ /dev/null @@ -1,7 +0,0 @@ -Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate. -Hint Unfold not : core. - -Goal true<>false. -Set Typeclasses Debug. -Fail typeclasses eauto with core. -Abort. diff --git a/test-suite/bugs/opened/3889.v b/test-suite/bugs/opened/3889.v deleted file mode 100644 index 6b287324cc..0000000000 --- a/test-suite/bugs/opened/3889.v +++ /dev/null @@ -1,11 +0,0 @@ -Require Import Program. - -Inductive Even : nat -> Prop := -| evenO : Even O -| evenS : forall n, Odd n -> Even (S n) -with Odd : nat -> Prop := -| oddS : forall n, Even n -> Odd (S n). -Axiom admit : forall {T}, T. -Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) := admit -with doubleO {n} (o : Odd n) : Odd (S (2 * n)) := _. -Next Obligation of doubleE. diff --git a/test-suite/bugs/opened/3890.v b/test-suite/bugs/opened/3890.v deleted file mode 100644 index f9ac9be2c8..0000000000 --- a/test-suite/bugs/opened/3890.v +++ /dev/null @@ -1,18 +0,0 @@ -Class Foo. -Class Bar := b : Type. - -Instance foo : Foo := _. -(* 1 subgoals, subgoal 1 (ID 4) - - ============================ - Foo *) - -Instance bar : Bar. -exact Type. -Defined. -(* bar is defined *) - -About foo. -(* foo not a defined object. *) - -Fail Defined. diff --git a/test-suite/bugs/opened/3919.v-disabled b/test-suite/bugs/opened/3919.v-disabled deleted file mode 100644 index 0d661de9c4..0000000000 --- a/test-suite/bugs/opened/3919.v-disabled +++ /dev/null @@ -1,13 +0,0 @@ -Require Import MSets. -Require Import Orders. - -Declare Module Signal : OrderedType. - -Module S := MSetAVL.Make(Signal). -Module Sdec := Decide(S). -Export Sdec. - -Hint Extern 0 (Signal.eq ?x ?y) => now symmetry. - -Goal forall o s, Signal.eq o s. -Proof. fsetdec. Qed. diff --git a/test-suite/bugs/opened/3922.v-disabled b/test-suite/bugs/opened/3922.v-disabled deleted file mode 100644 index ce4f509cad..0000000000 --- a/test-suite/bugs/opened/3922.v-disabled +++ /dev/null @@ -1,83 +0,0 @@ -Set Universe Polymorphism. -Notation Type0 := Set. - -Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. - -Notation compose := (fun g f x => g (f x)). - -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. -Open Scope function_scope. - -Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) - := forall x:A, f x = g x. - -Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. - -Class Contr_internal (A : Type) := BuildContr { - center : A ; - contr : (forall y : A, center = y) -}. - -Inductive trunc_index : Type := -| minus_two : trunc_index -| trunc_S : trunc_index -> trunc_index. - -Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. -Local Open Scope trunc_scope. -Notation "-2" := minus_two (at level 0) : trunc_scope. -Notation "-1" := (-2.+1) (at level 0) : trunc_scope. - -Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := - match n with - | -2 => Contr_internal A - | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) - end. - -Class IsTrunc (n : trunc_index) (A : Type) : Type := - Trunc_is_trunc : IsTrunc_internal n A. - -Notation Contr := (IsTrunc -2). -Notation IsHProp := (IsTrunc -1). - -Monomorphic Axiom dummy_funext_type : Type0. -Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. - -Inductive Unit : Type1 := - tt : Unit. - -Record TruncType (n : trunc_index) := BuildTruncType { - trunctype_type : Type ; - istrunc_trunctype_type : IsTrunc n trunctype_type -}. - -Arguments BuildTruncType _ _ {_}. - -Coercion trunctype_type : TruncType >-> Sortclass. - -Notation "n -Type" := (TruncType n) (at level 1) : type_scope. -Notation hProp := (-1)-Type. - -Notation BuildhProp := (BuildTruncType -1). - -Private Inductive Trunc (n : trunc_index) (A :Type) : Type := - tr : A -> Trunc n A. -Arguments tr {n A} a. - -Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i}) -: IsTrunc@{j} n (Trunc@{i} n A). -Admitted. - -Definition Trunc_ind {n A} - (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} - : (forall a, P (tr a)) -> (forall aa, P aa) -:= (fun f aa => match aa with tr a => fun _ => f a end Pt). -Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). -Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y) - (P : Type) `{Pc : X -> Contr P} - (g : X -> P) (h : P -> Y) (p : h o g == f) -: Unit. -Proof. - assert (merely X -> IsHProp P) by admit. - refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _); - [ assumption.. | ]. - Fail pose (g' := Trunc_ind (fun _ => P) g : merely X -> P). diff --git a/test-suite/bugs/opened/3928.v-disabled b/test-suite/bugs/opened/3928.v-disabled deleted file mode 100644 index b470eb229b..0000000000 --- a/test-suite/bugs/opened/3928.v-disabled +++ /dev/null @@ -1,12 +0,0 @@ -Typeclasses eauto := bfs. - -Class Foo := {}. -Class Bar := {}. - -Instance: Bar. -Instance: Foo -> Bar -> Foo -> Foo | 1. -Instance: Bar -> Foo | 100. -Instance: Foo -> Bar -> Foo -> Foo | 1. - -Set Typeclasses Debug. -Timeout 1 Check (_ : Foo). (* timeout *) diff --git a/test-suite/bugs/opened/3938.v b/test-suite/bugs/opened/3938.v deleted file mode 100644 index 2d0d1930f1..0000000000 --- a/test-suite/bugs/opened/3938.v +++ /dev/null @@ -1,6 +0,0 @@ -Require Import Coq.Arith.PeanoNat. -Hint Extern 1 => admit : typeclass_instances. -Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. - intros a b f H. - rewrite H. (* Toplevel input, characters 15-25: -Anomaly: Evar ?X11 was not declared. Please report. *) diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/3946.v deleted file mode 100644 index e77bdbc652..0000000000 --- a/test-suite/bugs/opened/3946.v +++ /dev/null @@ -1,11 +0,0 @@ -Require Import ZArith. - -Inductive foo := Foo : Z.le 0 1 -> foo. - -Definition bar (f : foo) := let (f) := f in f. - -(* Doesn't work: *) -(* Arguments bar f.*) - -(* Does work *) -Arguments bar f _. diff --git a/test-suite/bugs/opened/4701.v b/test-suite/bugs/opened/4701.v deleted file mode 100644 index 9286f0f1f0..0000000000 --- a/test-suite/bugs/opened/4701.v +++ /dev/null @@ -1,23 +0,0 @@ -(*Suppose we have*) - - Inductive my_if {A B} : bool -> Type := - | then_case (_ : A) : my_if true - | else_case (_ : B) : my_if false. - Notation "'If' b 'Then' A 'Else' B" := (@my_if A B b) (at level 10). - -(*then here are three inductive type declarations that work:*) - - Inductive I1 := - | i1 (x : I1). - Inductive I2 := - | i2 (x : nat). - Inductive I3 := - | i3 (b : bool) (x : If b Then I3 Else nat). - -(*and here is one that does not, despite being equivalent to [I3]:*) - - Fail Inductive I4 := - | i4 (b : bool) (x : if b then I4 else nat). (* Error: Non strictly positive occurrence of "I4" in - "forall b : bool, (if b then I4 else nat) -> I4". *) - -(*I think this one should work. I believe this is a conservative extension over CIC: Since [match] statements returning types can always be re-encoded as inductive type families, the analysis should be independent of whether the constructor uses an inductive or a [match] statement.*) diff --git a/test-suite/bugs/opened/4721.v b/test-suite/bugs/opened/4721.v deleted file mode 100644 index 1f184b3930..0000000000 --- a/test-suite/bugs/opened/4721.v +++ /dev/null @@ -1,13 +0,0 @@ -Variables S1 S2 : Set. - -Goal @eq Type S1 S2 -> @eq Type S1 S2. -intro H. -Fail tauto. -assumption. -Qed. - -(*This is in 8.5pl1, and Matthieq Sozeau says: "That's a regression in tauto indeed, which now requires exact equality of the universes, through a non linear goal pattern matching: -match goal with ?X1 |- ?X1 forces both instances of X1 to be convertible, -with no additional universe constraints currently, but the two types are -initially different. This can be fixed easily to allow the same flexibility -as in 8.4 (or assumption) to unify the universes as well."*) diff --git a/test-suite/bugs/opened/4728.v b/test-suite/bugs/opened/4728.v deleted file mode 100644 index 230b4beb6c..0000000000 --- a/test-suite/bugs/opened/4728.v +++ /dev/null @@ -1,72 +0,0 @@ -(*I'd like the final [Check] in the following to work:*) - -Ltac fin_eta_expand := - [ > lazymatch goal with - | [ H : _ |- _ ] => clear H - end.. - | lazymatch goal with - | [ H : ?T |- ?T ] - => exact H - | [ |- ?G ] - => fail 0 "No hypothesis matching" G - end ]; - let n := numgoals in - tryif constr_eq numgoals 0 - then idtac - else fin_eta_expand. - -Ltac pre_eta_expand x := - let T := type of x in - let G := match goal with |- ?G => G end in - unify T G; - unshelve econstructor; - destruct x; - fin_eta_expand. - -Ltac eta_expand x := - let v := constr:(ltac:(pre_eta_expand x)) in - idtac v; - let v := (eval cbv beta iota zeta in v) in - exact v. - -Notation eta_expand x := (ltac:(eta_expand x)) (only parsing). - -Ltac partial_unify eqn := - lazymatch eqn with - | ?x = ?x => idtac - | ?f ?x = ?g ?y - => partial_unify (f = g); - (tryif unify x y then - idtac - else tryif has_evar x then - unify x y - else tryif has_evar y then - unify x y - else - idtac) - | ?x = ?y - => idtac; - (tryif unify x y then - idtac - else tryif has_evar x then - unify x y - else tryif has_evar y then - unify x y - else - idtac) - end. - -Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" := - let old_record' := eta_expand old_record in - partial_unify (old_record = new_record); - eexact new_record. - -Set Implicit Arguments. -Record prod A B := pair { fst : A ; snd : B }. -Infix "*" := prod : type_scope. -Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. - -Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing). - -Check ltac:({ (1, 1) with {| snd := 2 |} }). -Fail Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type"; should succeed *) diff --git a/test-suite/bugs/opened/4755.v b/test-suite/bugs/opened/4755.v deleted file mode 100644 index 9cc0d361ea..0000000000 --- a/test-suite/bugs/opened/4755.v +++ /dev/null @@ -1,34 +0,0 @@ -(*I'm not sure which behavior is better. But if the change is intentional, it should be documented (I don't think it is), and it'd be nice if there were a flag for this, or if -compat 8.4 restored the old behavior.*) - -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. -Definition f (v : option nat) := match v with - | Some k => Some k - | None => None - end. - -Axioms F G : (option nat -> option nat) -> Prop. -Axiom FG : forall f, f None = None -> F f = G f. - -Axiom admit : forall {T}, T. - -Existing Instance eq_Reflexive. - -Global Instance foo (A := nat) - : Proper ((pointwise_relation _ eq) - ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) - (@option_rect A (fun _ => Prop)) | 0. -exact admit. -Qed. - -Global Instance bar (A := nat) - : Proper ((pointwise_relation _ eq) - ==> eq ==> eq ==> Basics.flip Basics.impl) - (@option_rect A (fun _ => Prop)) | 0. -exact admit. -Qed. - -Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. -Proof. - intro. - pose proof (_ : (Proper (_ ==> eq ==> _) and)). - Fail setoid_rewrite (FG _ _); []. (* In 8.5: Error: Tactic failure: Incorrect number of goals (expected 2 tactics); works in 8.4 *) diff --git a/test-suite/bugs/opened/4771.v b/test-suite/bugs/opened/4771.v deleted file mode 100644 index 396d74bdbf..0000000000 --- a/test-suite/bugs/opened/4771.v +++ /dev/null @@ -1,22 +0,0 @@ -Module Type Foo. - -Parameter Inline t : nat. - -End Foo. - -Module F(X : Foo). - -Tactic Notation "foo" ref(x) := idtac. - -Ltac g := foo X.t. - -End F. - -Module N. -Definition t := 0 + 0. -End N. - -Module K := F(N). - -(* Was -Anomaly: Uncaught exception Not_found. Please report. *) diff --git a/test-suite/bugs/opened/4778.v b/test-suite/bugs/opened/4778.v deleted file mode 100644 index 633d158e96..0000000000 --- a/test-suite/bugs/opened/4778.v +++ /dev/null @@ -1,35 +0,0 @@ -Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. -Definition f (v : option nat) := match v with - | Some k => Some k - | None => None - end. - -Axioms F G : (option nat -> option nat) -> Prop. -Axiom FG : forall f, f None = None -> F f = G f. - -Axiom admit : forall {T}, T. - -Existing Instance eq_Reflexive. - -(* This instance is needed in 8.4, but is useless in 8.5 *) -Global Instance foo (A := nat) - : Proper ((pointwise_relation _ eq) - ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) - (@option_rect A (fun _ => Prop)) | 0. -exact admit. -Qed. - -(* -(* This is required in 8.5, but useless in 8.4 *) -Global Instance bar (A := nat) - : Proper ((pointwise_relation _ eq) - ==> eq ==> eq ==> Basics.flip Basics.impl) - (@option_rect A (fun _ => Prop)) | 0. -exact admit. -Qed. -*) - -Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. Proof. - intro. - pose proof (_ : (Proper (_ ==> eq ==> _) and)). - Fail setoid_rewrite (FG _ _); [ | reflexivity.. ]. (* this should succeed without [Fail], as it does in 8.4 *) diff --git a/test-suite/bugs/opened/4781.v b/test-suite/bugs/opened/4781.v deleted file mode 100644 index 8b651ac22e..0000000000 --- a/test-suite/bugs/opened/4781.v +++ /dev/null @@ -1,94 +0,0 @@ -Ltac force_clear := - clear; - repeat match goal with - | [ H : _ |- _ ] => clear H - | [ H := _ |- _ ] => clearbody H - end. - -Class abstract_term {T} (x : T) := by_abstract_term : T. -Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances. - -Goal True. -(* These work: *) - let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - pose x. - let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let x := (eval cbv iota in (let v : T := x in v)) in - pose x. - let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let x := match constr:(Set) with ?y => constr:(y) end in - pose x. -(* This fails with an error: *) - Fail let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let x := match constr:(x) with ?y => constr:(y) end in - pose x. (* The command has indeed failed with message: -Error: Variable y should be bound to a term. *) -(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *) - Fail let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let x := match constr:(x) with ?y => y end in - pose x. - Fail let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let x := (eval cbv iota in x) in - pose x. - Fail let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let x := type of x in - pose x. (* should succeed *) - Fail let term := constr:(I) in - let T := type of term in - let x := constr:(_ : abstract_term term) in - let x := type of x in - pose x. (* should succeed *) - -(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time. - -Even stranger, consider:*) - let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let y := (eval cbv iota in (let v : T := x in v)) in - pose y; - let x' := fresh "x'" in - pose x as x'. - let x := (eval cbv delta [x'] in x') in - pose x; - let z := (eval cbv iota in x) in - pose z. - -(*This works fine. But if I change the period to a semicolon, I get:*) - - Fail let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let y := (eval cbv iota in (let v : T := x in v)) in - pose y; - let x' := fresh "x'" in - pose x as x'; - let x := (eval cbv delta [x'] in x') in - pose x. (* Anomaly: Uncaught exception Not_found. Please report. *) - (* should succeed *) -(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*) - - Fail let term := constr:(I) in - let T := type of term in - let x := constr:((_ : abstract_term term) : T) in - let y := (eval cbv iota in (let v : T := x in v)) in - pose y; - let x' := fresh "x'" in - pose x as x'; - let x := (eval cbv delta [x'] in x') in - let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *) - idtac. (* should succeed *) diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v deleted file mode 100644 index 2ac5535934..0000000000 --- a/test-suite/bugs/opened/4813.v +++ /dev/null @@ -1,5 +0,0 @@ -Require Import Program.Tactics. - -Record T := BT { t : Set }. -Record U (x : T) := BU { u : t x -> Prop }. -Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. diff --git a/test-suite/bugs/opened/6393.v b/test-suite/bugs/opened/6393.v deleted file mode 100644 index 8d5d092333..0000000000 --- a/test-suite/bugs/opened/6393.v +++ /dev/null @@ -1,11 +0,0 @@ -(* These always worked. *) -Goal prod True True. firstorder. Qed. -Goal True -> @sigT True (fun _ => True). firstorder. Qed. -Goal prod True True. dtauto. Qed. -Goal prod True True. tauto. Qed. - -(* These should work. *) -Goal @sigT True (fun _ => True). dtauto. Qed. -(* These should work, but don't *) -(* Goal @sigT True (fun _ => True). firstorder. Qed. *) -(* Goal @sigT True (fun _ => True). tauto. Qed. *) diff --git a/test-suite/bugs/opened/6602.v b/test-suite/bugs/opened/6602.v deleted file mode 100644 index 3690adf90a..0000000000 --- a/test-suite/bugs/opened/6602.v +++ /dev/null @@ -1,17 +0,0 @@ -Require Import Omega. - -Lemma test_nat: - forall n, (5 + pred n <= 5 + n). -Proof. - intros. - zify. - omega. -Qed. - -Lemma test_N: - forall n, (5 + N.pred n <= 5 + n)%N. -Proof. - intros. - zify. - omega. -Qed. diff --git a/test-suite/bugs/opened/bug_1338.v-disabled b/test-suite/bugs/opened/bug_1338.v-disabled new file mode 100644 index 0000000000..ab0f98202d --- /dev/null +++ b/test-suite/bugs/opened/bug_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. + Fail omega. +Abort. diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v new file mode 100644 index 0000000000..820022d995 --- /dev/null +++ b/test-suite/bugs/opened/bug_1596.v @@ -0,0 +1,260 @@ +Require Import Relations. +Require Import FSets. +Require Import Arith. +Require Import Omega. + +Set Keyed Unification. + +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. + + Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}. + Proof. + intros [xa xb] [ya yb]; simpl. + destruct (X.eq_dec xa ya). + destruct (Y.eq_dec xb yb). + + left; now split. + + right. now intros [eqa eqb]. + + right. now intros [eqa eqb]. + 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. + + Definition eq_dec : forall (x y: t), { eq x y } + { ~ eq x y}. + Proof. + intros [i] [j]. unfold eq. + destruct (eq_nat_dec i j). + + left. now f_equal. + + right. intros meq; now inversion meq. + 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. discriminate. (* !! impossible here !! *) + Qed. +End B. diff --git a/test-suite/bugs/opened/bug_1615.v b/test-suite/bugs/opened/bug_1615.v new file mode 100644 index 0000000000..c045335410 --- /dev/null +++ b/test-suite/bugs/opened/bug_1615.v @@ -0,0 +1,11 @@ +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. Fail omega. +Abort. diff --git a/test-suite/bugs/opened/bug_1671.v b/test-suite/bugs/opened/bug_1671.v new file mode 100644 index 0000000000..b4e653f687 --- /dev/null +++ b/test-suite/bugs/opened/bug_1671.v @@ -0,0 +1,12 @@ +(* 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. + +Fail 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/bug_1811.v b/test-suite/bugs/opened/bug_1811.v new file mode 100644 index 0000000000..57c1744313 --- /dev/null +++ b/test-suite/bugs/opened/bug_1811.v @@ -0,0 +1,10 @@ +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. + Fail rewrite neg2xor. +Abort. diff --git a/test-suite/bugs/opened/bug_2572.v-disabled b/test-suite/bugs/opened/bug_2572.v-disabled new file mode 100644 index 0000000000..3f6c6a0d14 --- /dev/null +++ b/test-suite/bugs/opened/bug_2572.v-disabled @@ -0,0 +1,187 @@ +Require Import List. +Definition is_dec (P:Prop) := {P}+{~P}. +Definition eq_dec (T:Type) := forall (t1 t2:T), is_dec (t1=t2). + +Record Label : Type := mkLabel { + LabElem: Type; + LabProd: LabElem -> LabElem -> option LabElem; + LabBot: LabElem -> Prop; + LabError: LabElem -> Prop +}. + +Definition LProd (L1 L2: Label): Label := {| + LabElem := LabElem L1 * LabElem L2; + LabProd := fun lg ld => let (lg1,lg2) := lg in let (ld1,ld2) := ld in + match LabProd L1 lg1 ld1, LabProd L2 lg2 ld2 with + Some g, Some d => Some (g,d) + | _,_ => None + end; + LabBot l := let (l1,l2) := l in LabBot L1 l1 \/ LabBot L2 l2; + LabError l := let (l1,l2) := l in LabError L1 l1 \/ LabError L2 l2 +|}. + +Definition Lrestrict (L: Label) (S: LabElem L -> bool): Label := {| + LabElem := LabElem L; + LabProd l1 l2 := if andb (S l1) (S l2) then LabProd L l1 l2 else None; + LabBot l := LabBot L l; + LabError l := LabError L l +|}. + +Notation "l1 ^* l2" := (LProd l1 l2) (at level 50). + +Record LTS(L:Type): Type := mkLTS { + State: Type; + Init: State -> Prop; + Next: State -> L -> State -> Prop +}. +Implicit Arguments State. +Implicit Arguments Init. +Implicit Arguments Next. + +Definition sound L (S: LTS (LabElem L)): Prop := + forall s s' l, Next S s l s' -> ~LabError L l. + +Inductive PNext L (S1 S2:LTS (LabElem L)): State S1 * State S2 -> (LabElem L) -> State S1 * State S2 -> Prop := + LNext: forall s1 s2 l1 s'1, Next S1 s1 l1 s'1 -> (forall l2, LabProd L l1 l2 = None) -> + PNext L S1 S2 (s1,s2) l1 (s'1,s2) +| RNext: forall s1 s2 l2 s'2, (forall l1, LabProd L l1 l2 = None) -> Next S2 s2 l2 s'2 -> + PNext L S1 S2 (s1,s2) l2 (s1,s'2) +| SNext: forall s1 s2 l1 l2 l s'1 s'2, Next S1 s1 l1 s'1 -> Next S2 s2 l2 s'2 -> + Some l = LabProd L l1 l2 -> PNext L S1 S2 (s1,s2) l (s'1,s'2). + +Definition Produit (L:Label) (S1 S2: LTS (LabElem L)): LTS (LabElem L) := {| + State := State S1 * State S2; + Init := fun s => let (s1,s2) := s in Init S1 s1 /\ Init S2 s2; + Next :=PNext L S1 S2 +|}. + +Parameter Time: Type. +Parameter teq: forall t1 t2:Time, {t1=t2}+{t1<>t2}. + +Inductive TLabElem(L:Type): Type := + Tdiscrete: L -> TLabElem L +| Tdelay: Time -> TLabElem L +| Tbot: TLabElem L. + +Definition TLabel L: Label := {| + LabElem := TLabElem (LabElem L); + LabProd lt1 lt2 := + match lt1, lt2 with + Tdiscrete l1, Tdiscrete l2 => match (LabProd L l1 l2) with Some l => Some (Tdiscrete (LabElem L) l) | None => None end + | Tdelay t1, Tdelay t2 => if teq t1 t2 then Some (Tdelay (LabElem L) t1) else Some (Tbot (LabElem L)) + | _,_ => None + end; + LabBot lt := match lt with + Tdiscrete l => LabBot L l + | Tbot => True + | _ => False + end; + LabError lt := match lt with + Tdiscrete l => LabError L l + | _ => False + end + |}. + +Parameter Var: Type. +Parameter allv: forall P, (forall (v:Var), is_dec (P v)) -> is_dec (forall v, P v). +Parameter DType: Type. +Parameter Data: DType -> Type. +Parameter vtype: Var -> DType. +Parameter Deq: forall t (d1 d2: Data t), is_dec (d1=d2). + +Inductive Vctr(v:Var): Type := + Wctr: Data (vtype v) -> Vctr v +| Rctr: Data (vtype v) -> Vctr v +| Fctr: Vctr v +| Nctr: Vctr v. + +Definition isCmp v (c1 c2: Vctr v): Prop := + match c1,c2 with + Wctr _, Nctr => True + | Rctr _, Rctr _ => True + | Rctr _, Nctr => True + | Rctr _, Fctr => True + | Nctr, _ => True + | _,_ => False + end. + +Lemma isCmp_dec: forall v (c1 c2: Vctr v), is_dec (isCmp v c1 c2). +intros. +induction c1; induction c2; simpl; intros; try (left; tauto); try (right; tauto). +Qed. + +Definition Vprod v (c1 c2: Vctr v): (isCmp v c1 c2) -> Vctr v := + match c1,c2 return isCmp v c1 c2 -> Vctr v with + | Wctr d, Nctr => fun h => Wctr v d + | Rctr d1, Rctr d2 => fun h => if Deq (vtype v) d1 d2 then Rctr v d1 else Fctr v + | Rctr d1, Nctr => fun h => Rctr v d1 + | Rctr d1, Fctr => fun h => Fctr v + | Fctr, Rctr _ => fun h => Fctr v + | Fctr, Fctr => fun h => Fctr v + | Fctr, Nctr => fun h => Fctr v + | Nctr, c2 => fun h => c2 + | _,_ => fun h => match h with end + end. + +Inductive MLabElem: Type := + Mctr: (forall v, Vctr v) -> MLabElem +| Merr: MLabElem. + +Definition MProd (m1 m2: MLabElem): MLabElem := + match m1,m2 with + Mctr c1, Mctr c2 => match allv (fun v => isCmp v (c1 v) (c2 v)) (fun v => isCmp_dec v (c1 v) (c2 v)) with + left h => Mctr (fun v => Vprod v (c1 v) (c2 v) (h v)) + | _ => Merr + end + | _,_ => Merr + end. + +Definition MLabel: Label := {| + LabElem := MLabElem; + LabProd m1 m2 := Some (MProd m1 m2); + LabBot m := exists c, m = Mctr c /\ exists v, c v = Fctr v; + LabError m := m = Merr +|}. + +Parameter Chan: Type. +Parameter ch_eq: eq_dec Chan. + +Definition CLabel(S: Chan->bool): Label := {| + LabElem := Chan; + LabProd := fun c1 c2 => if ch_eq c1 c2 then if S c1 then Some c1 else None else None; + LabBot := fun _ => False; + LabError := fun _ => False +|}. + +Definition FLabel(S: Chan->bool): Label := + TLabel (CLabel S ^* MLabel ^* MLabel ^* MLabel). + +Definition FTS := LTS (LabElem (FLabel (fun _ => true))). +Check (fun S (T1 T2: FTS) => Produit (FLabel S) T1 T2). +(* +Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS. +unfold FTS in *; simpl in *. +apply (Produit (FLabel S)). +apply T1. +apply T2. +Defined. + +Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS := + Produit (FLabel S) T1 T2. +*) +Lemma FTSirrel (S: Chan -> bool): FTS = LTS (LabElem (FLabel S)). +Proof. + unfold FTS. + simpl. + reflexivity. +Qed. + +Definition PAR (S: Chan -> bool) (T1 T2: FTS): FTS. +revert T2; revert T1. +rewrite (FTSirrel S). +apply (Produit (FLabel S)). +Defined. + +Record HTTS: Type := mkHTTS { + +}. diff --git a/test-suite/bugs/opened/bug_3010.v-disabled b/test-suite/bugs/opened/bug_3010.v-disabled new file mode 100644 index 0000000000..f2906bd6a6 --- /dev/null +++ b/test-suite/bugs/opened/bug_3010.v-disabled @@ -0,0 +1 @@ +Definition em {A R} (k : forall s : sum A _, match s with inl x => R x | inr y => R end) := k (inr (fun x => k (inl x))). \ No newline at end of file diff --git a/test-suite/bugs/opened/bug_3092.v b/test-suite/bugs/opened/bug_3092.v new file mode 100644 index 0000000000..9db21d156e --- /dev/null +++ b/test-suite/bugs/opened/bug_3092.v @@ -0,0 +1,9 @@ +Fail Fixpoint le_pred (n1 n2 : nat) (H1 : n1 <= n2) : pred n1 <= pred n2 := + match H1 with + | le_n => le_n (pred _) + | le_S _ H2 => + match n2 with + | 0 => fun H3 => H3 + | S _ => le_S _ _ + end (le_pred _ _ H2) + end. diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v new file mode 100644 index 0000000000..e1c29a954c --- /dev/null +++ b/test-suite/bugs/opened/bug_3166.v @@ -0,0 +1,83 @@ +Set Asymmetric Patterns. + +Section eq. + Let A := { X : Type & X }. + Let B := (fun x : A => projT1 x). + Let T := (fun (a' : A) (b' : B a') => projT2 a' = b'). + Let T' := T. + Let t1T := (fun _ : A => unit). + Let f1 := (fun x (_ : t1T x) => projT2 x). + Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)). + Let t1T' := t1T. + Let f1' := f1. + Let t1' := t1. + + Theorem eq_matches_commute + a' b' (t' : T a' b') + (rta : forall b'', T' a' b'' -> A) + (rtb : forall b'' t'', B (rta b'' t'')) + (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y))) + (R : forall (b : B (rta b' t')), T _ b -> Type) + (r1 : forall y, R (f1 _ y) (@t1 _ y)) + : match + match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with + | eq_refl => rt1 tt + end + as t0 in (@eq _ _ b0) + return R b0 t0 + with + | eq_refl => r1 tt + end + = + match t' + as t0' in (@eq _ _ b0') + return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type) + (r1 : forall y, R (f1 _ y) (@t1 _ y)), + R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with + | eq_refl => rt1 tt + end)) + with + | eq_refl => fun _ r1 => + match rt1 tt with + | eq_refl => r1 tt + end + end R r1. + Proof. + destruct t'; reflexivity. + Defined. + + Theorem eq_match_beta2 + a b (t : T a b) + X + (R : forall b' (t' : T a b'), X b' -> Type) + (r1 : forall y x, R _ (@t1 _ y) x) + x + : match t as t' in (@eq _ _ b') return forall x, R b' t' x with + | eq_refl => r1 tt + end (x b) + = + match t as t' in (@eq _ _ b') return R b' t' (x b') with + | eq_refl => r1 tt (x _) + end. + Proof. + destruct t; reflexivity. + Defined. +End eq. + +Definition typeof {T} (_ : T) := T. + +Eval compute in (eq_sym (eq_sym _)). +Goal forall T (x y : T) (p : x = y), True. + intros. + pose proof + (@eq_matches_commute + (existT (fun T => T) T x) y p + (fun b'' _ => existT (fun T => T) T b'') + (fun _ _ => x) + (fun _ => eq_refl) + (fun x' _ => x' = y) + (fun _ => eq_refl) + ) as H0. + compute in H0. + change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0. + Fail pose proof (fun k => @eq_trans _ _ _ k H0). diff --git a/test-suite/bugs/opened/bug_3186.v-disabled b/test-suite/bugs/opened/bug_3186.v-disabled new file mode 100644 index 0000000000..d0bcb920cc --- /dev/null +++ b/test-suite/bugs/opened/bug_3186.v-disabled @@ -0,0 +1,4 @@ +Fixpoint a (_:unit):= +match eq_refl with +|eq_refl => a +end. \ No newline at end of file diff --git a/test-suite/bugs/opened/bug_3248.v b/test-suite/bugs/opened/bug_3248.v new file mode 100644 index 0000000000..33c408a28c --- /dev/null +++ b/test-suite/bugs/opened/bug_3248.v @@ -0,0 +1,17 @@ +Ltac ret_and_left f := + let tac := ret_and_left in + let T := type of f in + lazymatch eval hnf in T with + | ?T' -> _ => + let ret := constr:(fun x' : T' => ltac:(tac (f x'))) in + exact ret + | ?T' => exact f + end. + +Goal forall A B : Prop, forall x y : A, True. +Proof. + intros A B x y. + pose (f := fun (x y : A) => conj x y). + pose (a := ltac:(ret_and_left f)). + Fail unify (a x y) (conj x y). +Abort. diff --git a/test-suite/bugs/opened/bug_3277.v b/test-suite/bugs/opened/bug_3277.v new file mode 100644 index 0000000000..5f4231363a --- /dev/null +++ b/test-suite/bugs/opened/bug_3277.v @@ -0,0 +1,7 @@ +Tactic Notation "evarr" open_constr(x) := let y := constr:(x) in exact y. + +Goal True. + evarr _. +Admitted. +Goal True. + Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *) diff --git a/test-suite/bugs/opened/bug_3278.v b/test-suite/bugs/opened/bug_3278.v new file mode 100644 index 0000000000..1c6deae94b --- /dev/null +++ b/test-suite/bugs/opened/bug_3278.v @@ -0,0 +1,25 @@ +Module a. + Check let x' := _ in + ltac:(exact x'). + + Notation foo x := (let x' := x in ltac:(exact x')). + + Fail Check foo _. (* Error: +Cannot infer an internal placeholder of type "Type" in environment: + +x' := ?42 : ?41 +. *) +End a. + +Module b. + Notation foo x := (let x' := x in let y := (ltac:(exact I) : True) in I). + Notation bar x := (let x' := x in let y := (I : True) in I). + + Check let x' := _ in ltac:(exact I). (* let x' := ?5 in I *) + Check bar _. (* let x' := ?9 in let y := I in I *) + Fail Check foo _. (* Error: +Cannot infer an internal placeholder of type "Type" in environment: + +x' := ?42 : ?41 +. *) +End b. diff --git a/test-suite/bugs/opened/bug_3283.v b/test-suite/bugs/opened/bug_3283.v new file mode 100644 index 0000000000..3ab5416e8c --- /dev/null +++ b/test-suite/bugs/opened/bug_3283.v @@ -0,0 +1,28 @@ +Notation "P |-- Q" := (@eq nat P Q) (at level 80, Q at level 41, no associativity) . +Notation "x &&& y" := (plus x y) (at level 40, left associativity, y at next level) . +Notation "'Ex' x , P " := (plus x P) (at level 65, x at level 99, P at level 80). + +(* Succeed *) +Check _ |-- _ &&& _ -> _. +Check _ |-- _ &&& (Ex _, _ ) -> _. +Check _ |-- (_ &&& Ex _, _ ) -> _. + +(* Why does this fail? *) +Fail Check _ |-- _ &&& Ex _, _ -> _. +(* The command has indeed failed with message: +=> Error: The term "Ex ?17, ?18" has type "nat" +which should be Set, Prop or Type. *) + +(* Just in case something is strange with -> *) +Notation "P ----> Q" := (P -> Q) (right associativity, at level 99, Q at next level). + +(* Succeed *) +Check _ |-- _ &&& _ ----> _. +Check _ |-- _ &&& (Ex _, _ ) ----> _. +Check _ |-- (_ &&& Ex _, _ ) ----> _. + +(* Why does this fail? *) +Fail Check _ |-- _ &&& Ex _, _ ----> _. +(* The command has indeed failed with message: +=> Error: The term "Ex ?31, ?32" has type "nat" +which should be Set, Prop or Type.*) diff --git a/test-suite/bugs/opened/bug_3295.v b/test-suite/bugs/opened/bug_3295.v new file mode 100644 index 0000000000..c09649de73 --- /dev/null +++ b/test-suite/bugs/opened/bug_3295.v @@ -0,0 +1,104 @@ +Require Export Morphisms Setoid. + +Class lops := lmk_ops { + car: Type; + weq: relation car +}. + +Arguments car : clear implicits. + +Coercion car: lops >-> Sortclass. + +Instance weq_Equivalence `{lops}: Equivalence weq. +Proof. +Admitted. + +Module lset. +Canonical Structure lset_ops A := lmk_ops (list A) (fun h k => True). +End lset. + +Class ops := mk_ops { + ob: Type; + mor: ob -> ob -> lops; + dot: forall n m p, mor n m -> mor m p -> mor n p +}. +Coercion mor: ops >-> Funclass. +Arguments ob : clear implicits. + +Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p). +Proof. +Admitted. + +Section s. + +Import lset. + +Context `{X:lops} {I: Type}. + +Axiom sup : forall (f: I -> X) (J : list I), X. + +Global Instance sup_weq: Proper (pointwise_relation _ weq ==> weq ==> weq) sup. +Proof. +Admitted. + +End s. + +Axiom ord : forall (n : nat), Type. +Axiom seq : forall n, list (ord n). + +Infix "==" := weq (at level 79). +Infix "*" := (dot _ _ _) (left associativity, at level 40). + +Notation "∑_ ( i ∈ l ) f" := (@sup (mor _ _) _ (fun i => f) l) + (at level 41, f at level 41, i, l at level 50). + +Axiom dotxsum : forall `{X : ops} I J n m p (f: I -> X m n) (x: X p m) y, + x * (∑_(i∈ J) f i) == y. + +Definition mx X n m := ord n -> ord m -> X. + +Section bsl. +Context `{X : ops} {u: ob X}. +Notation U := (car (@mor X u u)). + +Lemma toto n m p q (M : mx U n m) N (P : mx U p q) Q i j : ∑_(j0 ∈ seq m) M i j0 * (∑_(j1 ∈ seq p) N j0 j1 * P j1 j) == Q. +Proof. + Fail setoid_rewrite dotxsum. + (* Toplevel input, characters 0-22: +Error: +Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints. +Unable to satisfy the following constraints: +UNDEFINED EVARS: + ?101==[X u n m p q M N P Q i j j0 |- U] (goal evar) + ?106==[X u n m p q M N P Q i j |- relation (X u u)] (internal placeholder) + ?107==[X u n m p q M N P Q i j |- relation (list (ord m))] + (internal placeholder) + ?108==[X u n m p q M N P Q i j (do_subrelation:=do_subrelation) + |- Proper (pointwise_relation (ord m) weq ==> ?107 ==> ?106) sup] + (internal placeholder) + ?109==[X u n m p q M N P Q i j |- ProperProxy ?107 (seq m)] + (internal placeholder) + ?110==[X u n m p q M N P Q i j |- relation (X u u)] (internal placeholder) + ?111==[X u n m p q M N P Q i j (do_subrelation:=do_subrelation) + |- Proper (?106 ==> ?110 ==> Basics.flip Basics.impl) weq] + (internal placeholder) + ?112==[X u n m p q M N P Q i j |- ProperProxy ?110 Q] (internal placeholder)UNIVERSES: + {} |= Top.14 <= Top.37 + Top.25 <= Top.24 + Top.25 <= Top.32 + +ALGEBRAIC UNIVERSES:{} +UNDEFINED UNIVERSES:METAS: + 470[y] := ?101 : car (?99 ?467 ?465) + 469[x] := M i _UNBOUND_REL_1 : car (?99 ?467 ?466) [type is checked] + 468[f] := fun i : ?463 => N _UNBOUND_REL_2 i * P i j : + ?463 -> ?99 ?466 ?465 [type is checked] + 467[p] := u : ob ?99 [type is checked] + 466[m] := u : ob ?99 [type is checked] + 465[n] := u : ob ?99 [type is checked] + 464[J] := seq p : list ?463 [type is checked] + 463[I] := ord p : Type [type is checked] + *) +Abort. + +End bsl. diff --git a/test-suite/bugs/opened/bug_3304.v b/test-suite/bugs/opened/bug_3304.v new file mode 100644 index 0000000000..66668930c7 --- /dev/null +++ b/test-suite/bugs/opened/bug_3304.v @@ -0,0 +1,3 @@ +Fail Notation "( x , y , .. , z )" := ltac:(let r := constr:(prod .. (prod x y) .. z) in r). +(* The command has indeed failed with message: +=> Error: Special token .. is for use in the Notation command. *) diff --git a/test-suite/bugs/opened/bug_3311.v b/test-suite/bugs/opened/bug_3311.v new file mode 100644 index 0000000000..1c66bc1e55 --- /dev/null +++ b/test-suite/bugs/opened/bug_3311.v @@ -0,0 +1,10 @@ +Require Import Setoid. +Axiom bar : True = False. +Goal True. + Fail setoid_rewrite bar. (* Toplevel input, characters 15-33: +Error: +Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting constraints. + +Could not find an instance for "subrelation eq (Basics.flip Basics.impl)". +With the following constraints: +?3 : "True" *) diff --git a/test-suite/bugs/opened/bug_3312.v b/test-suite/bugs/opened/bug_3312.v new file mode 100644 index 0000000000..749921e2f6 --- /dev/null +++ b/test-suite/bugs/opened/bug_3312.v @@ -0,0 +1,5 @@ +Require Import Setoid. +Axiom bar : 0 = 1. +Goal 0 = 1. + Fail rewrite_strat bar. (* Toplevel input, characters 15-32: +Error: Tactic failure:setoid rewrite failed: Nothing to rewrite. *) diff --git a/test-suite/bugs/opened/bug_3343.v b/test-suite/bugs/opened/bug_3343.v new file mode 100644 index 0000000000..6c5a85f9cf --- /dev/null +++ b/test-suite/bugs/opened/bug_3343.v @@ -0,0 +1,46 @@ +(* File reduced by coq-bug-finder from original input, then from 13699 lines to 656 lines, then from 584 lines to 200 lines *) +Set Asymmetric Patterns. +Require Export Coq.Lists.List. +Export List.ListNotations. + +Record CFGV := { Terminal : Type; VarSym : Type }. + +Section Gram. + Context {G : CFGV}. + + Inductive Pattern : (Terminal G) -> Type := + | ptleaf : forall (T : Terminal G), + nat -> Pattern T + with Mixture : list (Terminal G) -> Type := + | mtcons : forall {h: Terminal G} + {tl: list (Terminal G)}, + Pattern h -> Mixture tl -> Mixture (h::tl). + + Variable vc : VarSym G. + + Fixpoint pBVars {gs} (p : Pattern gs) : (list nat) := + match p with + | ptleaf _ _ => [] + end + with mBVars {lgs} (pts : Mixture lgs) : (list nat) := + match pts with + | mtcons _ _ _ tl => mBVars tl + end. + + Lemma mBndngVarsAsNth : + forall mp (m : @Mixture mp), + mBVars m = [2]. + Proof. + intros. + induction m. progress simpl. + Admitted. +End Gram. + +Lemma mBndngVarsAsNth' {G : CFGV} { vc : VarSym G} : + forall mp (m : @Mixture G mp), + mBVars m = [2]. +Proof. + intros. + induction m. + Fail progress simpl. + (* simpl did nothing here, while it does something inside the section; this is probably a bug*) diff --git a/test-suite/bugs/opened/bug_3345.v b/test-suite/bugs/opened/bug_3345.v new file mode 100644 index 0000000000..3e3da6df71 --- /dev/null +++ b/test-suite/bugs/opened/bug_3345.v @@ -0,0 +1,145 @@ +Require Import TestSuite.admit. +(* File reduced by coq-bug-finder from original input, then from 1972 lines to 136 lines, then from 119 lines to 105 lines *) +Global Set Implicit Arguments. +Require Import Coq.Lists.List Program. +Section IndexBound. + Context {A : Set}. + Class IndexBound (a : A) (Bound : list A) := + { ibound :> nat; + boundi : nth_error Bound ibound = Some a}. + Global Arguments ibound [a Bound] _ . + Global Arguments boundi [a Bound] _. + Record BoundedIndex (Bound : list A) := { bindex :> A; indexb :> IndexBound bindex Bound }. +End IndexBound. +Context {A : Type} {C : Set}. +Variable (projAC : A -> C). +Lemma None_neq_Some +: forall (AnyT AnyT' : Type) (a : AnyT), + None = Some a -> AnyT'. + admit. +Defined. +Program Definition nth_Bounded' + (Bound : list A) + (c : C) + (a_opt : option A) + (nth_n : option_map projAC a_opt = Some c) +: A := match a_opt as x + return (option_map projAC x = Some c) -> A with + | Some a => fun _ => a + | None => fun f : None = Some _ => ! + end nth_n. +Lemma nth_error_map : + forall n As c_opt, + nth_error (map projAC As) n = c_opt + -> option_map projAC (nth_error As n) = c_opt. + admit. +Defined. +Definition nth_Bounded + (Bound : list A) + (idx : BoundedIndex (map projAC Bound)) +: A := nth_Bounded' Bound (nth_error Bound (ibound idx)) + (nth_error_map _ _ (boundi idx)). +Program Definition nth_Bounded_ind2 + (P : forall As, BoundedIndex (map projAC As) + -> BoundedIndex (map projAC As) + -> A -> A -> Prop) +: forall (Bound : list A) + (idx : BoundedIndex (map projAC Bound)) + (idx' : BoundedIndex (map projAC Bound)), + match nth_error Bound (ibound idx), nth_error Bound (ibound idx') with + | Some a, Some a' => P Bound idx idx' a a' + | _, _ => True + end + -> P Bound idx idx' (nth_Bounded _ idx) (nth_Bounded _ idx'):= + fun Bound idx idx' => + match (nth_error Bound (ibound idx)) as e, (nth_error Bound (ibound idx')) as e' + return + (forall (f : option_map _ e = Some (bindex idx)) + (f' : option_map _ e' = Some (bindex idx')), + (match e, e' with + | Some a, Some a' => P Bound idx idx' a a' + | _, _ => True + end) + -> P Bound idx idx' + (match e as e'' return + option_map _ e'' = Some (bindex idx) + -> A + with + | Some a => fun _ => a + | _ => fun f => _ + end f) + (match e' as e'' return + option_map _ e'' = Some (bindex idx') + -> A + with + | Some a => fun _ => a + | _ => fun f => _ + end f')) with + | Some a, Some a' => fun _ _ H => _ + | _, _ => fun f => _ + end (nth_error_map _ _ (boundi idx)) + (nth_error_map _ _ (boundi idx')). + +Lemma nth_Bounded_eq +: forall (Bound : list A) + (idx idx' : BoundedIndex (map projAC Bound)), + ibound idx = ibound idx' + -> nth_Bounded Bound idx = nth_Bounded Bound idx'. +Proof. + intros. + eapply nth_Bounded_ind2 with (idx := idx) (idx' := idx'). + simpl. + (* The [case_eq] should not Fail. More importantly, [Fail case_eq ...] should succeed if [case_eq ...] fails. It doesn't!!! So I resort to [Fail Fail try (case_eq ...)]. *) + Fail Fail try (case_eq (nth_error Bound (ibound idx'))). +(* Toplevel input, characters 15-54: +In nested Ltac calls to "case_eq" and "pattern x at - 1", last call failed. +Error: The abstracted term +"fun e : Exc A => + forall e0 : nth_error Bound (ibound idx') = e, + match + nth_error Bound (ibound idx) as anonymous'0 + return (anonymous'0 = nth_error Bound (ibound idx) -> e = e -> Prop) + with + | Some a => + match + e as anonymous' + return + (Some a = nth_error Bound (ibound idx) -> anonymous' = e -> Prop) + with + | Some a' => + fun (_ : Some a = nth_error Bound (ibound idx)) (_ : Some a' = e) => + a = a' + | None => + fun (_ : Some a = nth_error Bound (ibound idx)) (_ : None = e) => + True + end + | None => fun (_ : None = nth_error Bound (ibound idx)) (_ : e = e) => True + end eq_refl e0" is not well typed. +Illegal application: +The term + "match + nth_error Bound (ibound idx) as anonymous'0 + return (anonymous'0 = nth_error Bound (ibound idx) -> e = e -> Prop) + with + | Some a => + match + e as anonymous' + return + (Some a = nth_error Bound (ibound idx) -> anonymous' = e -> Prop) + with + | Some a' => + fun (_ : Some a = nth_error Bound (ibound idx)) (_ : Some a' = e) => + a = a' + | None => + fun (_ : Some a = nth_error Bound (ibound idx)) (_ : None = e) => + True + end + | None => fun (_ : None = nth_error Bound (ibound idx)) (_ : e = e) => True + end" of type + "nth_error Bound (ibound idx) = nth_error Bound (ibound idx) -> + e = e -> Prop" +cannot be applied to the terms + "eq_refl" : "nth_error Bound (ibound idx) = nth_error Bound (ibound idx)" + "e0" : "nth_error Bound (ibound idx') = e" +The 2nd term has type "nth_error Bound (ibound idx') = e" +which should be coercible to "e = e". *) diff --git a/test-suite/bugs/opened/bug_3357.v b/test-suite/bugs/opened/bug_3357.v new file mode 100644 index 0000000000..c479158877 --- /dev/null +++ b/test-suite/bugs/opened/bug_3357.v @@ -0,0 +1,9 @@ +Notation D1 := (forall {T : Type} ( x : T ) , Type). + +Definition DD1 ( A : forall {T : Type} (x : T), Type ) := A 1. +Fail Definition DD1' ( A : D1 ) := A 1. (* Toplevel input, characters 32-33: +Error: In environment +A : forall T : Type, T -> Type +The term "1" has type "nat" while it is expected to have type +"Type". + *) diff --git a/test-suite/bugs/opened/bug_3363.v b/test-suite/bugs/opened/bug_3363.v new file mode 100644 index 0000000000..800d89573c --- /dev/null +++ b/test-suite/bugs/opened/bug_3363.v @@ -0,0 +1,26 @@ +(** In this file, either all four [Check]s should fail, or all four should succeed. *) +Module A. + Section HexStrings. + Require Import String. + End HexStrings. + Fail Check string. +End A. + +Module B. + Section HexStrings. + Require String. + Import String. + End HexStrings. + Fail Check string. +End B. + +Section HexStrings. + Require String. + Import String. +End HexStrings. +Fail Check string. + +Section HexStrings'. + Require Import String. +End HexStrings'. +Check string. diff --git a/test-suite/bugs/opened/bug_3370.v b/test-suite/bugs/opened/bug_3370.v new file mode 100644 index 0000000000..4964bf96c0 --- /dev/null +++ b/test-suite/bugs/opened/bug_3370.v @@ -0,0 +1,12 @@ +Require Import String. + +Local Ltac set_strings := + let s := match goal with |- context[String ?s1 ?s2] => constr:(String s1 s2) end in + let H := fresh s in + set (H := s). + +Local Open Scope string_scope. + +Goal "asdf" = "bds". +Fail set_strings. (* Error: Ltac variable s is bound to "asdf" which cannot be coerced to +a fresh identifier. *) diff --git a/test-suite/bugs/opened/bug_3395.v b/test-suite/bugs/opened/bug_3395.v new file mode 100644 index 0000000000..5ca48fc9d6 --- /dev/null +++ b/test-suite/bugs/opened/bug_3395.v @@ -0,0 +1,231 @@ +Require Import TestSuite.admit. +(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) +Generalizable All Variables. +Set Implicit Arguments. + +Arguments fst {_ _} _. +Arguments snd {_ _} _. + +Axiom cheat : forall {T}, T. + +Reserved Notation "g 'o' f" (at level 40, left associativity). + +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (paths x y) : type_scope. + +Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. +Record PreCategory (object : Type) := + Build_PreCategory' { + object :> Type := object; + morphism : object -> object -> Type; + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' + where "f 'o' g" := (compose f g); + associativity : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + (m3 o m2) o m1 = m3 o (m2 o m1); + associativity_sym : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + m3 o (m2 o m1) = (m3 o m2) o m1; + left_identity : forall a b (f : morphism a b), identity b o f = f; + right_identity : forall a b (f : morphism a b), f o identity a = f; + identity_identity : forall x, identity x o identity x = identity x + }. +Bind Scope category_scope with PreCategory. +Arguments PreCategory {_}. +Arguments identity {_} [!C%category] x%object : rename. + +Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. + +Infix "o" := compose : morphism_scope. + +Delimit Scope functor_scope with functor. +Local Open Scope morphism_scope. +Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := + { + object_of :> C -> D; + morphism_of : forall s d, morphism C s d + -> morphism D (object_of s) (object_of d); + composition_of : forall s d d' + (m1 : morphism C s d) (m2: morphism C d d'), + morphism_of _ _ (m2 o m1) + = (morphism_of _ _ m2) o (morphism_of _ _ m1); + identity_of : forall x, morphism_of _ _ (identity x) + = identity (object_of x) + }. +Bind Scope functor_scope with Functor. + +Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. + +Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. + +Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := + { + morphism_inverse : morphism C d s; + left_inverse : morphism_inverse o m = identity _; + right_inverse : m o morphism_inverse = identity _ + }. + +Definition opposite `(C : @PreCategory objC) : PreCategory + := @Build_PreCategory' + C + (fun s d => morphism C d s) + (identity (C := C)) + (fun _ _ _ m1 m2 => m2 o m1) + (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) + (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) + (fun _ _ => @right_identity _ _ _ _) + (fun _ _ => @left_identity _ _ _ _) + (@identity_identity _ C). + +Notation "C ^op" := (opposite C) (at level 3) : category_scope. + +Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). + refine (@Build_PreCategory' + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) + * morphism D (snd s) (snd d))%type) + (fun x => (identity (fst x), identity (snd x))) + (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) + _ + _ + _ + _ + _); admit. +Defined. +Infix "*" := prod : category_scope. + +Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E + := Build_Functor + C E + (fun c => G (F c)) + (fun _ _ m => morphism_of G (morphism_of F m)) + cheat + cheat. + +Infix "o" := compose_functor : functor_scope. + +Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := + Build_NaturalTransformation' { + components_of :> forall c, morphism D (F c) (G c); + commutes : forall s d (m : morphism C s d), + components_of d o F _1 m = G _1 m o components_of s; + + commutes_sym : forall s d (m : C.(morphism) s d), + G _1 m o components_of s = components_of d o F _1 m + }. +Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory + := @Build_PreCategory' (Functor C D) + (@NaturalTransformation _ C _ D) + cheat + cheat + cheat + cheat + cheat + cheat + cheat. + +Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op + := Build_Functor (C^op) (D^op) + (object_of F) + (fun s d => morphism_of F (s := d) (d := s)) + (fun d' d s m1 m2 => composition_of F s d d' m2 m1) + (identity_of F). + +Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op + := Build_Functor C (D^op) + (object_of F) + (fun s d => morphism_of F (s := d) (d := s)) + (fun d' d s m1 m2 => composition_of F s d d' m2 m1) + (identity_of F). +Notation "F ^op" := (opposite_functor F) : functor_scope. + +Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. +Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C + := Build_Functor (C * D) C + (@fst _ _) + (fun _ _ => @fst _ _) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). + +Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D + := Build_Functor (C * D) D + (@snd _ _) + (fun _ _ => @snd _ _) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). +Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') +: Functor C (D * D') + := Build_Functor + C (D * D') + (fun c => (F c, F' c)) + (fun s d m => (F _1 m, F' _1 m))%morphism + cheat + cheat. +Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') + := (prod_functor (F o fst) (F' o snd))%functor. +Notation cat_of obj := + (@Build_PreCategory' obj + (fun x y => forall _ : x, y) + (fun _ x => x) + (fun _ _ _ f g x => f (g x))%core + (fun _ _ _ _ _ _ _ => idpath) + (fun _ _ _ _ _ _ _ => idpath) + (fun _ _ _ => idpath) + (fun _ _ _ => idpath) + (fun _ => idpath)). + +Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) + := Build_Functor _ _ cheat cheat cheat cheat. + +Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) +: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) + := Build_NaturalTransformation' _ _ cheat cheat cheat. + +Class IsFullyFaithful `(F : @Functor objC C objD D) + := is_fully_faithful + : forall x y : C, + IsIsomorphism (induced_hom_natural_transformation F (x, y)). + +Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) + := cheat. + +Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) + := (((coyoneda A^op)^op'L)^op'L)%functor. +Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). +Admitted. + +Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). +Proof. + intros a b. + pose proof (coyoneda_embedding A^op a b) as CYE. + unfold yoneda. + Time let t := (type of CYE) in + let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) + Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in + let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). + Time let t := match goal with |- ?G => constr:(G) end in + let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) +Fail Timeout 2 Defined. +Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) + +Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). +Proof. + intros a b. + pose proof (coyoneda_embedding A^op a b) as CYE. + unfold yoneda; simpl in *. + Fail Timeout 1 exact CYE. + Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) diff --git a/test-suite/bugs/opened/bug_3424.v b/test-suite/bugs/opened/bug_3424.v new file mode 100644 index 0000000000..d1c5bb68f9 --- /dev/null +++ b/test-suite/bugs/opened/bug_3424.v @@ -0,0 +1,24 @@ +Set Universe Polymorphism. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }. +Inductive trunc_index : Type := minus_two | trunc_S (x : trunc_index). +Bind Scope trunc_scope with trunc_index. +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | minus_two => Contr_internal A + | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) + end. +Notation minus_one:=(trunc_S minus_two). +Notation "0" := (trunc_S minus_one) : trunc_scope. +Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. +Notation IsHProp := (IsTrunc minus_one). +Notation IsHSet := (IsTrunc 0). +Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. +Proof. +intros. +eexists. +(* exact (H' a b). *) +(* Undo. *) +Fail apply (H' a b). +exact (H' a b). +Qed. diff --git a/test-suite/bugs/opened/bug_3459.v b/test-suite/bugs/opened/bug_3459.v new file mode 100644 index 0000000000..762611f751 --- /dev/null +++ b/test-suite/bugs/opened/bug_3459.v @@ -0,0 +1,31 @@ +(* Bad interaction between clear and the typability of ltac constr bindings *) + +(* Original report *) + +Goal 1 = 2. +Proof. +(* This line used to fail with a Not_found up to some point, and then + to produce an ill-typed term *) +match goal with + | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in + clear x; + exact r)) in + pose y +end. +(* Add extra test for typability (should not fail when bug closed) *) +Fail match goal with P:?c |- _ => try (let x := type of c in idtac) || fail 2 end. +Abort. + +(* Second report raising a Not_found at the time of 21 Oct 2014 *) + +Section F. + +Variable x : nat. + +Goal True. +evar (e : Prop). +assert e. +Fail let r := constr:(eq_refl x) in clear x; exact r. +Abort. + +End F. diff --git a/test-suite/bugs/opened/bug_3463.v b/test-suite/bugs/opened/bug_3463.v new file mode 100644 index 0000000000..124f2bcc03 --- /dev/null +++ b/test-suite/bugs/opened/bug_3463.v @@ -0,0 +1,12 @@ +Tactic Notation "test1" open_constr(t) ident(r):= + pose t. +Tactic Notation "test2" constr(r) open_constr(t):= + pose t. +Tactic Notation "test3" open_constr(t) constr(r):= + pose t. + +Goal True. + test1 (1 + _) nat. + test2 nat (1 + _). + test3 (1 + _) nat. + test3 (1 + _ : nat) nat. diff --git a/test-suite/bugs/opened/bug_3478.v-disabled b/test-suite/bugs/opened/bug_3478.v-disabled new file mode 100644 index 0000000000..cc926b2167 --- /dev/null +++ b/test-suite/bugs/opened/bug_3478.v-disabled @@ -0,0 +1,8 @@ +Set Primitive Projections. +Record foo := { foom :> Type }. +Canonical Structure default_foo := fun T => {| foom := T |}. +Record bar T := { bar1 : T }. +Goal forall (s : foo) (x : foom s), True. +Proof. + intros. + Timeout 1 pose (x : bar _) as x'. \ No newline at end of file diff --git a/test-suite/bugs/opened/bug_3626.v b/test-suite/bugs/opened/bug_3626.v new file mode 100644 index 0000000000..46a6c009eb --- /dev/null +++ b/test-suite/bugs/opened/bug_3626.v @@ -0,0 +1,7 @@ +Set Implicit Arguments. +Set Primitive Projections. +Record prod A B := pair { fst : A ; snd : B }. + +Fail Goal forall x y : prod Set Set, x.(@fst) = y.(@fst). +(* intros. + apply f_equal. *) diff --git a/test-suite/bugs/opened/bug_3655.v b/test-suite/bugs/opened/bug_3655.v new file mode 100644 index 0000000000..841f77febb --- /dev/null +++ b/test-suite/bugs/opened/bug_3655.v @@ -0,0 +1,9 @@ +Ltac bar x := pose x. +Tactic Notation "foo" open_constr(x) := bar x. +Class baz := { baz' : Type }. +Goal True. +(* Original error was an anomaly which is fixed; now, it succeeds but + leaving an evar, while calling pose would not leave an evar, so I + guess it is still a bug in the sense that the semantics of pose is + not preserved *) + foo baz'. diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v new file mode 100644 index 0000000000..a717bbe735 --- /dev/null +++ b/test-suite/bugs/opened/bug_3754.v @@ -0,0 +1,284 @@ +Unset Strict Universe Declaration. +Require Import TestSuite.admit. +(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *) +(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1 + coqtop version trunk (October 2014) *) + +Notation Type0 := Set. + +Notation idmap := (fun x => x). + +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. + +Notation pr1 := projT1. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. + +Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := + fun x => g (f x). + +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x. +admit. +Defined. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "1" := idpath : path_scope. + +Notation "p @ q" := (concat p q) (at level 20) : path_scope. + +Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope. + +Notation "p @' q" := (concat p q) (at level 21, left associativity, + format "'[v' p '/' '@'' q ']'") : long_path_scope. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y. +exact (match p with idpath => u end). +Defined. + +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y. +exact (match p with idpath => idpath end). +Defined. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Arguments eisretr {A B} f {_} _. + +Record Equiv A B := BuildEquiv { + equiv_fun : A -> B ; + equiv_isequiv : IsEquiv equiv_fun +}. + +Coercion equiv_fun : Equiv >-> Funclass. + +Global Existing Instance equiv_isequiv. + +Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. +Notation IsHProp := (IsTrunc -1). + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Local Open Scope path_scope. + +Definition concat_p1 {A : Type} {x y : A} (p : x = y) : + p @ 1 = p + := + match p with idpath => 1 end. + +Definition concat_1p {A : Type} {x y : A} (p : x = y) : + 1 @ p = p + := + match p with idpath => 1 end. + +Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : + p @ (q @ r) = (p @ q) @ r := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. + +Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : + (p @ q) @ r = p @ (q @ r) := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. + +Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) : + r^ @ q = p -> q = r @ p. +admit. +Defined. + +Ltac with_rassoc tac := + repeat rewrite concat_pp_p; + tac; + + repeat rewrite concat_p_pp. + +Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp). + +Definition ap_p_pp {A B : Type} (f : A -> B) {w : B} {x y z : A} + (r : w = f x) (p : x = y) (q : y = z) : + r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q). +admit. +Defined. + +Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) : + ap (g o f) p = ap g (ap f p) + := + match p with idpath => 1 end. + +Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) : + (ap f q) @ (p y) = (p x) @ (ap g q) + := + match q with + | idpath => concat_1p _ @ ((concat_p1 _) ^) + end. + +Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type) + {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) + : D x2 (p # y) (p # z) + := + match p with idpath => w end. +Local Open Scope equiv_scope. + +Definition transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} + {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) (y : B x2) + : (transport (fun x => B x -> C) p f) y = f (p^ # y). +admit. +Defined. + +Definition transport_arrow_fromconst {A B : Type} {C : A -> Type} + {x1 x2 : A} (p : x1 = x2) (f : B -> C x1) (y : B) + : (transport (fun x => B -> C x) p f) y = p # (f y). +admit. +Defined. + +Definition ap_transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type} + {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2) + : ap (transport (fun x => B x -> C) p f) q + @ transport_arrow_toconst p f y2 + = transport_arrow_toconst p f y1 + @ ap (fun y => f (p^ # y)) q. +admit. +Defined. + +Class Univalence. +Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B). +admit. +Defined. +Definition transport_path_universe + {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A) + : transport (fun X:Type => X) (path_universe f) z = f z. +admit. +Defined. +Definition transport_path_universe_V `{Funext} + {A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B) + : transport (fun X:Type => X) (path_universe f)^ z = f^-1 z. +admit. +Defined. + +Ltac simpl_do_clear tac term := + let H := fresh in + assert (H := term); + simpl in H |- *; + tac H; + clear H. + +Tactic Notation "simpl" "rewrite" constr(term) := simpl_do_clear ltac:(fun H => rewrite H) term. + +Global Instance Univalence_implies_Funext `{Univalence} : Funext. +Admitted. + +Section Factorization. + + Context {class1 class2 : forall (X Y : Type@{i}), (X -> Y) -> Type@{i}} + `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class1 _ _ g)} + `{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class2 _ _ g)} + {A B : Type@{i}} {f : A -> B}. + + Record Factorization := + { intermediate : Type ; + factor1 : A -> intermediate ; + factor2 : intermediate -> B ; + fact_factors : factor2 o factor1 == f ; + inclass1 : class1 _ _ factor1 ; + inclass2 : class2 _ _ factor2 + }. + + Record PathFactorization {fact fact' : Factorization} := + { path_intermediate : intermediate fact <~> intermediate fact' ; + path_factor1 : path_intermediate o factor1 fact == factor1 fact' ; + path_factor2 : factor2 fact == factor2 fact' o path_intermediate ; + path_fact_factors : forall a, path_factor2 (factor1 fact a) + @ ap (factor2 fact') (path_factor1 a) + @ fact_factors fact' a + = fact_factors fact a + }. + Context `{Univalence} {fact fact' : Factorization} + (pf : @PathFactorization fact fact'). + + Let II := path_intermediate pf. + Let ff1 := path_factor1 pf. + Let ff2 := path_factor2 pf. +Local Definition II' : intermediate fact = intermediate fact'. +admit. +Defined. + + Local Definition fff' (a : A) + : (transportD2 (fun X => A -> X) (fun X => X -> B) + (fun X g h => {_ : forall a : A, h (g a) = f a & + {_ : class1 A X g & class2 X B h}}) + II' (factor1 fact) (factor2 fact) + (fact_factors fact; (inclass1 fact; inclass2 fact))).1 a = + ap (transport (fun X => X -> B) II' (factor2 fact)) + (transport_arrow_fromconst II' (factor1 fact) a + @ transport_path_universe II (factor1 fact a) + @ ff1 a) + @ transport_arrow_toconst II' (factor2 fact) (factor1 fact' a) + @ ap (factor2 fact) (transport_path_universe_V II (factor1 fact' a)) + @ ff2 (II^-1 (factor1 fact' a)) + @ ap (factor2 fact') (eisretr II (factor1 fact' a)) + @ fact_factors fact' a. + Proof. + + Open Scope long_path_scope. + + rewrite (ap_transport_arrow_toconst (B := idmap) (C := B)). + + simpl rewrite (@ap_compose _ _ _ (transport idmap (path_universe II)^) + (factor2 fact)). + rewrite <- ap_p_pp; rewrite_moveL_Mp_p. + Set Debug Tactic Unification. + Fail rewrite (concat_Ap ff2). diff --git a/test-suite/bugs/opened/bug_3794.v b/test-suite/bugs/opened/bug_3794.v new file mode 100644 index 0000000000..e4711a38c0 --- /dev/null +++ b/test-suite/bugs/opened/bug_3794.v @@ -0,0 +1,7 @@ +Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate. +Hint Unfold not : core. + +Goal true<>false. +Set Typeclasses Debug. +Fail typeclasses eauto with core. +Abort. diff --git a/test-suite/bugs/opened/bug_3889.v b/test-suite/bugs/opened/bug_3889.v new file mode 100644 index 0000000000..6b287324cc --- /dev/null +++ b/test-suite/bugs/opened/bug_3889.v @@ -0,0 +1,11 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). +Axiom admit : forall {T}, T. +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) := admit +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) := _. +Next Obligation of doubleE. diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v new file mode 100644 index 0000000000..5c74addb62 --- /dev/null +++ b/test-suite/bugs/opened/bug_3890.v @@ -0,0 +1,18 @@ +Class Foo. +Class Bar := b : Type. + +Instance foo : Foo := _. +(* 1 subgoals, subgoal 1 (ID 4) + + ============================ + Foo *) + +Instance bar : Bar. +exact Type. +Defined. +(* bar is defined *) + +About foo. +(* foo not a defined object. *) + +Fail Defined. diff --git a/test-suite/bugs/opened/bug_3919.v-disabled b/test-suite/bugs/opened/bug_3919.v-disabled new file mode 100644 index 0000000000..0d661de9c4 --- /dev/null +++ b/test-suite/bugs/opened/bug_3919.v-disabled @@ -0,0 +1,13 @@ +Require Import MSets. +Require Import Orders. + +Declare Module Signal : OrderedType. + +Module S := MSetAVL.Make(Signal). +Module Sdec := Decide(S). +Export Sdec. + +Hint Extern 0 (Signal.eq ?x ?y) => now symmetry. + +Goal forall o s, Signal.eq o s. +Proof. fsetdec. Qed. diff --git a/test-suite/bugs/opened/bug_3922.v-disabled b/test-suite/bugs/opened/bug_3922.v-disabled new file mode 100644 index 0000000000..ce4f509cad --- /dev/null +++ b/test-suite/bugs/opened/bug_3922.v-disabled @@ -0,0 +1,83 @@ +Set Universe Polymorphism. +Notation Type0 := Set. + +Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. + +Notation Contr := (IsTrunc -2). +Notation IsHProp := (IsTrunc -1). + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Inductive Unit : Type1 := + tt : Unit. + +Record TruncType (n : trunc_index) := BuildTruncType { + trunctype_type : Type ; + istrunc_trunctype_type : IsTrunc n trunctype_type +}. + +Arguments BuildTruncType _ _ {_}. + +Coercion trunctype_type : TruncType >-> Sortclass. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (-1)-Type. + +Notation BuildhProp := (BuildTruncType -1). + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + +Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i}) +: IsTrunc@{j} n (Trunc@{i} n A). +Admitted. + +Definition Trunc_ind {n A} + (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} + : (forall a, P (tr a)) -> (forall aa, P aa) +:= (fun f aa => match aa with tr a => fun _ => f a end Pt). +Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). +Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y) + (P : Type) `{Pc : X -> Contr P} + (g : X -> P) (h : P -> Y) (p : h o g == f) +: Unit. +Proof. + assert (merely X -> IsHProp P) by admit. + refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _); + [ assumption.. | ]. + Fail pose (g' := Trunc_ind (fun _ => P) g : merely X -> P). diff --git a/test-suite/bugs/opened/bug_3928.v-disabled b/test-suite/bugs/opened/bug_3928.v-disabled new file mode 100644 index 0000000000..b470eb229b --- /dev/null +++ b/test-suite/bugs/opened/bug_3928.v-disabled @@ -0,0 +1,12 @@ +Typeclasses eauto := bfs. + +Class Foo := {}. +Class Bar := {}. + +Instance: Bar. +Instance: Foo -> Bar -> Foo -> Foo | 1. +Instance: Bar -> Foo | 100. +Instance: Foo -> Bar -> Foo -> Foo | 1. + +Set Typeclasses Debug. +Timeout 1 Check (_ : Foo). (* timeout *) diff --git a/test-suite/bugs/opened/bug_3938.v b/test-suite/bugs/opened/bug_3938.v new file mode 100644 index 0000000000..2d0d1930f1 --- /dev/null +++ b/test-suite/bugs/opened/bug_3938.v @@ -0,0 +1,6 @@ +Require Import Coq.Arith.PeanoNat. +Hint Extern 1 => admit : typeclass_instances. +Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. + intros a b f H. + rewrite H. (* Toplevel input, characters 15-25: +Anomaly: Evar ?X11 was not declared. Please report. *) diff --git a/test-suite/bugs/opened/bug_3946.v b/test-suite/bugs/opened/bug_3946.v new file mode 100644 index 0000000000..e77bdbc652 --- /dev/null +++ b/test-suite/bugs/opened/bug_3946.v @@ -0,0 +1,11 @@ +Require Import ZArith. + +Inductive foo := Foo : Z.le 0 1 -> foo. + +Definition bar (f : foo) := let (f) := f in f. + +(* Doesn't work: *) +(* Arguments bar f.*) + +(* Does work *) +Arguments bar f _. diff --git a/test-suite/bugs/opened/bug_4701.v b/test-suite/bugs/opened/bug_4701.v new file mode 100644 index 0000000000..9286f0f1f0 --- /dev/null +++ b/test-suite/bugs/opened/bug_4701.v @@ -0,0 +1,23 @@ +(*Suppose we have*) + + Inductive my_if {A B} : bool -> Type := + | then_case (_ : A) : my_if true + | else_case (_ : B) : my_if false. + Notation "'If' b 'Then' A 'Else' B" := (@my_if A B b) (at level 10). + +(*then here are three inductive type declarations that work:*) + + Inductive I1 := + | i1 (x : I1). + Inductive I2 := + | i2 (x : nat). + Inductive I3 := + | i3 (b : bool) (x : If b Then I3 Else nat). + +(*and here is one that does not, despite being equivalent to [I3]:*) + + Fail Inductive I4 := + | i4 (b : bool) (x : if b then I4 else nat). (* Error: Non strictly positive occurrence of "I4" in + "forall b : bool, (if b then I4 else nat) -> I4". *) + +(*I think this one should work. I believe this is a conservative extension over CIC: Since [match] statements returning types can always be re-encoded as inductive type families, the analysis should be independent of whether the constructor uses an inductive or a [match] statement.*) diff --git a/test-suite/bugs/opened/bug_4721.v b/test-suite/bugs/opened/bug_4721.v new file mode 100644 index 0000000000..1f184b3930 --- /dev/null +++ b/test-suite/bugs/opened/bug_4721.v @@ -0,0 +1,13 @@ +Variables S1 S2 : Set. + +Goal @eq Type S1 S2 -> @eq Type S1 S2. +intro H. +Fail tauto. +assumption. +Qed. + +(*This is in 8.5pl1, and Matthieq Sozeau says: "That's a regression in tauto indeed, which now requires exact equality of the universes, through a non linear goal pattern matching: +match goal with ?X1 |- ?X1 forces both instances of X1 to be convertible, +with no additional universe constraints currently, but the two types are +initially different. This can be fixed easily to allow the same flexibility +as in 8.4 (or assumption) to unify the universes as well."*) diff --git a/test-suite/bugs/opened/bug_4728.v b/test-suite/bugs/opened/bug_4728.v new file mode 100644 index 0000000000..230b4beb6c --- /dev/null +++ b/test-suite/bugs/opened/bug_4728.v @@ -0,0 +1,72 @@ +(*I'd like the final [Check] in the following to work:*) + +Ltac fin_eta_expand := + [ > lazymatch goal with + | [ H : _ |- _ ] => clear H + end.. + | lazymatch goal with + | [ H : ?T |- ?T ] + => exact H + | [ |- ?G ] + => fail 0 "No hypothesis matching" G + end ]; + let n := numgoals in + tryif constr_eq numgoals 0 + then idtac + else fin_eta_expand. + +Ltac pre_eta_expand x := + let T := type of x in + let G := match goal with |- ?G => G end in + unify T G; + unshelve econstructor; + destruct x; + fin_eta_expand. + +Ltac eta_expand x := + let v := constr:(ltac:(pre_eta_expand x)) in + idtac v; + let v := (eval cbv beta iota zeta in v) in + exact v. + +Notation eta_expand x := (ltac:(eta_expand x)) (only parsing). + +Ltac partial_unify eqn := + lazymatch eqn with + | ?x = ?x => idtac + | ?f ?x = ?g ?y + => partial_unify (f = g); + (tryif unify x y then + idtac + else tryif has_evar x then + unify x y + else tryif has_evar y then + unify x y + else + idtac) + | ?x = ?y + => idtac; + (tryif unify x y then + idtac + else tryif has_evar x then + unify x y + else tryif has_evar y then + unify x y + else + idtac) + end. + +Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" := + let old_record' := eta_expand old_record in + partial_unify (old_record = new_record); + eexact new_record. + +Set Implicit Arguments. +Record prod A B := pair { fst : A ; snd : B }. +Infix "*" := prod : type_scope. +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. + +Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing). + +Check ltac:({ (1, 1) with {| snd := 2 |} }). +Fail Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type"; should succeed *) diff --git a/test-suite/bugs/opened/bug_4755.v b/test-suite/bugs/opened/bug_4755.v new file mode 100644 index 0000000000..9cc0d361ea --- /dev/null +++ b/test-suite/bugs/opened/bug_4755.v @@ -0,0 +1,34 @@ +(*I'm not sure which behavior is better. But if the change is intentional, it should be documented (I don't think it is), and it'd be nice if there were a flag for this, or if -compat 8.4 restored the old behavior.*) + +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. +Definition f (v : option nat) := match v with + | Some k => Some k + | None => None + end. + +Axioms F G : (option nat -> option nat) -> Prop. +Axiom FG : forall f, f None = None -> F f = G f. + +Axiom admit : forall {T}, T. + +Existing Instance eq_Reflexive. + +Global Instance foo (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Global Instance bar (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> eq ==> Basics.flip Basics.impl) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. +Proof. + intro. + pose proof (_ : (Proper (_ ==> eq ==> _) and)). + Fail setoid_rewrite (FG _ _); []. (* In 8.5: Error: Tactic failure: Incorrect number of goals (expected 2 tactics); works in 8.4 *) diff --git a/test-suite/bugs/opened/bug_4771.v b/test-suite/bugs/opened/bug_4771.v new file mode 100644 index 0000000000..396d74bdbf --- /dev/null +++ b/test-suite/bugs/opened/bug_4771.v @@ -0,0 +1,22 @@ +Module Type Foo. + +Parameter Inline t : nat. + +End Foo. + +Module F(X : Foo). + +Tactic Notation "foo" ref(x) := idtac. + +Ltac g := foo X.t. + +End F. + +Module N. +Definition t := 0 + 0. +End N. + +Module K := F(N). + +(* Was +Anomaly: Uncaught exception Not_found. Please report. *) diff --git a/test-suite/bugs/opened/bug_4778.v b/test-suite/bugs/opened/bug_4778.v new file mode 100644 index 0000000000..633d158e96 --- /dev/null +++ b/test-suite/bugs/opened/bug_4778.v @@ -0,0 +1,35 @@ +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. +Definition f (v : option nat) := match v with + | Some k => Some k + | None => None + end. + +Axioms F G : (option nat -> option nat) -> Prop. +Axiom FG : forall f, f None = None -> F f = G f. + +Axiom admit : forall {T}, T. + +Existing Instance eq_Reflexive. + +(* This instance is needed in 8.4, but is useless in 8.5 *) +Global Instance foo (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +(* +(* This is required in 8.5, but useless in 8.4 *) +Global Instance bar (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> eq ==> Basics.flip Basics.impl) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. +*) + +Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. Proof. + intro. + pose proof (_ : (Proper (_ ==> eq ==> _) and)). + Fail setoid_rewrite (FG _ _); [ | reflexivity.. ]. (* this should succeed without [Fail], as it does in 8.4 *) diff --git a/test-suite/bugs/opened/bug_4781.v b/test-suite/bugs/opened/bug_4781.v new file mode 100644 index 0000000000..8b651ac22e --- /dev/null +++ b/test-suite/bugs/opened/bug_4781.v @@ -0,0 +1,94 @@ +Ltac force_clear := + clear; + repeat match goal with + | [ H : _ |- _ ] => clear H + | [ H := _ |- _ ] => clearbody H + end. + +Class abstract_term {T} (x : T) := by_abstract_term : T. +Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances. + +Goal True. +(* These work: *) + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + pose x. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := (eval cbv iota in (let v : T := x in v)) in + pose x. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(Set) with ?y => constr:(y) end in + pose x. +(* This fails with an error: *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => constr:(y) end in + pose x. (* The command has indeed failed with message: +Error: Variable y should be bound to a term. *) +(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => y end in + pose x. + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := (eval cbv iota in x) in + pose x. + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := type of x in + pose x. (* should succeed *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:(_ : abstract_term term) in + let x := type of x in + pose x. (* should succeed *) + +(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time. + +Even stranger, consider:*) + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'. + let x := (eval cbv delta [x'] in x') in + pose x; + let z := (eval cbv iota in x) in + pose z. + +(*This works fine. But if I change the period to a semicolon, I get:*) + + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'; + let x := (eval cbv delta [x'] in x') in + pose x. (* Anomaly: Uncaught exception Not_found. Please report. *) + (* should succeed *) +(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*) + + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'; + let x := (eval cbv delta [x'] in x') in + let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *) + idtac. (* should succeed *) diff --git a/test-suite/bugs/opened/bug_4813.v b/test-suite/bugs/opened/bug_4813.v new file mode 100644 index 0000000000..2ac5535934 --- /dev/null +++ b/test-suite/bugs/opened/bug_4813.v @@ -0,0 +1,5 @@ +Require Import Program.Tactics. + +Record T := BT { t : Set }. +Record U (x : T) := BU { u : t x -> Prop }. +Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. diff --git a/test-suite/bugs/opened/bug_6393.v b/test-suite/bugs/opened/bug_6393.v new file mode 100644 index 0000000000..8d5d092333 --- /dev/null +++ b/test-suite/bugs/opened/bug_6393.v @@ -0,0 +1,11 @@ +(* These always worked. *) +Goal prod True True. firstorder. Qed. +Goal True -> @sigT True (fun _ => True). firstorder. Qed. +Goal prod True True. dtauto. Qed. +Goal prod True True. tauto. Qed. + +(* These should work. *) +Goal @sigT True (fun _ => True). dtauto. Qed. +(* These should work, but don't *) +(* Goal @sigT True (fun _ => True). firstorder. Qed. *) +(* Goal @sigT True (fun _ => True). tauto. Qed. *) diff --git a/test-suite/bugs/opened/bug_6602.v b/test-suite/bugs/opened/bug_6602.v new file mode 100644 index 0000000000..3690adf90a --- /dev/null +++ b/test-suite/bugs/opened/bug_6602.v @@ -0,0 +1,17 @@ +Require Import Omega. + +Lemma test_nat: + forall n, (5 + pred n <= 5 + n). +Proof. + intros. + zify. + omega. +Qed. + +Lemma test_N: + forall n, (5 + N.pred n <= 5 + n)%N. +Proof. + intros. + zify. + omega. +Qed. -- cgit v1.2.3