diff options
Diffstat (limited to 'test-suite/bugs/closed')
25 files changed, 271 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/1501.v b/test-suite/bugs/closed/1501.v new file mode 100644 index 000000000..e771e192d --- /dev/null +++ b/test-suite/bugs/closed/1501.v @@ -0,0 +1,67 @@ +Set Implicit Arguments. + + +Require Export Relation_Definitions. +Require Export Setoid. +Require Import Morphisms. + + +Section Essais. + +(* Parametrized Setoid *) +Parameter K : Type -> Type. +Parameter equiv : forall A : Type, K A -> K A -> Prop. +Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x. +Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x. +Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z +-> equiv x z. + +(* basic operations *) +Parameter val : forall A : Type, A -> K A. +Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B. + +Parameter + bind_compat : + forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B), + equiv m1 m2 -> + (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2). + +(* monad axioms *) +Parameter + bind_val_l : + forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a). +Parameter + bind_val_r : + forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m. +Parameter + bind_assoc : + forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C), + equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)). + + +Hint Resolve equiv_refl equiv_sym equiv_trans: monad. + +Add Parametric Relation A : (K A) (@equiv A) + reflexivity proved by (@equiv_refl A) + symmetry proved by (@equiv_sym A) + transitivity proved by (@equiv_trans A) + as equiv_rel. + +Add Parametric Morphism A B : (@bind A B) + with signature (@equiv A) ==> (pointwise_relation A (@equiv B)) ==> (@equiv B) + as bind_mor. +Proof. + unfold pointwise_relation; intros; apply bind_compat; auto. +Qed. + +Lemma test: + forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B), + (equiv m1 m2) -> (equiv m2 m3) -> + equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) + (bind m2 (fun a => bind m3 (fun a' => f a a'))). +Proof. + intros A B m1 m2 m3 f H1 H2. + setoid_rewrite H1. (* this works *) + setoid_rewrite H2. + reflexivity. +Qed. diff --git a/test-suite/bugs/closed/2001.v b/test-suite/bugs/closed/2001.v index d0b3bf173..652c65706 100644 --- a/test-suite/bugs/closed/2001.v +++ b/test-suite/bugs/closed/2001.v @@ -7,7 +7,7 @@ Inductive T : Set := | v : T. Definition f (s:nat) (t:T) : nat. -fix 2. +fix f 2. intros s t. refine match t with diff --git a/test-suite/bugs/closed/2456.v b/test-suite/bugs/closed/2456.v new file mode 100644 index 000000000..e5a392c4d --- /dev/null +++ b/test-suite/bugs/closed/2456.v @@ -0,0 +1,58 @@ + +Require Import Equality. + +Parameter Patch : nat -> nat -> Set. + +Inductive Catch (from to : nat) : Type + := MkCatch : forall (p : Patch from to), + Catch from to. +Arguments MkCatch [from to]. + +Inductive CatchCommute5 + : forall {from mid1 mid2 to : nat}, + Catch from mid1 + -> Catch mid1 to + -> Catch from mid2 + -> Catch mid2 to + -> Prop + := MkCatchCommute5 : + forall {from mid1 mid2 to : nat} + (p : Patch from mid1) + (q : Patch mid1 to) + (q' : Patch from mid2) + (p' : Patch mid2 to), + CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p'). + +Inductive CatchCommute {from mid1 mid2 to : nat} + (p : Catch from mid1) + (q : Catch mid1 to) + (q' : Catch from mid2) + (p' : Catch mid2 to) + : Prop + := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'), + CatchCommute p q q' p'. +Notation "<< p , q >> <~> << q' , p' >>" + := (CatchCommute p q q' p') + (at level 60, no associativity). + +Lemma CatchCommuteUnique2 : + forall {from mid mid' to : nat} + {p : Catch from mid} {q : Catch mid to} + {q' : Catch from mid'} {p' : Catch mid' to} + {q'' : Catch from mid'} {p'' : Catch mid' to} + (commute1 : <<p, q>> <~> <<q', p'>>) + (commute2 : <<p, q>> <~> <<q'', p''>>), + (p' = p'') /\ (q' = q''). +Proof with auto. +intros. +set (X := commute2). +Fail dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails generalizing X. +revert X. +dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails. +Abort. diff --git a/test-suite/bugs/closed/2814.v b/test-suite/bugs/closed/2814.v new file mode 100644 index 000000000..99da1e3e4 --- /dev/null +++ b/test-suite/bugs/closed/2814.v @@ -0,0 +1,6 @@ +Require Import Program. + +Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False. + intros. + Fail induction H. +Abort. diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v index a03adbd73..7b1a26178 100644 --- a/test-suite/bugs/closed/2969.v +++ b/test-suite/bugs/closed/2969.v @@ -12,6 +12,7 @@ eexists. reflexivity. Grab Existential Variables. admit. +Admitted. (* Alternative variant which failed but without raising anomaly *) @@ -24,3 +25,4 @@ clearbody n n0. exact I. Grab Existential Variables. admit. +Admitted. diff --git a/test-suite/bugs/closed/3100.v b/test-suite/bugs/closed/3100.v new file mode 100644 index 000000000..6f35a74dc --- /dev/null +++ b/test-suite/bugs/closed/3100.v @@ -0,0 +1,9 @@ +Fixpoint F (n : nat) (A : Type) : Type := + match n with + | 0 => True + | S n => forall (x : A), F n (x = x) + end. + +Goal forall A n, (forall (x : A) (e : x = x), F n (e = e)). +intros A n. +Fail change (forall x, F n (x = x)) with (F (S n)). diff --git a/test-suite/bugs/closed/3230.v b/test-suite/bugs/closed/3230.v new file mode 100644 index 000000000..265310b1a --- /dev/null +++ b/test-suite/bugs/closed/3230.v @@ -0,0 +1,14 @@ +Structure type : Type := Pack { ob : Type }. +Polymorphic Record category := { foo : Type }. +Definition FuncComp := Pack category. +Axiom C : category. + +Check (C : ob FuncComp). (* OK *) + +Canonical Structure FuncComp. + +Check (C : ob FuncComp). +(* Toplevel input, characters 15-39: +Error: +The term "C" has type "category" while it is expected to have type + "ob FuncComp". *) diff --git a/test-suite/bugs/closed/3320.v b/test-suite/bugs/closed/3320.v new file mode 100644 index 000000000..a5c243d8e --- /dev/null +++ b/test-suite/bugs/closed/3320.v @@ -0,0 +1,5 @@ +Goal forall x : nat, True. + fix goal 1. + assumption. +Fail Qed. +Undo. diff --git a/test-suite/bugs/closed/3350.v b/test-suite/bugs/closed/3350.v index c041c401f..c1ff292b3 100644 --- a/test-suite/bugs/closed/3350.v +++ b/test-suite/bugs/closed/3350.v @@ -55,7 +55,7 @@ Lemma lower_ind (P: forall n (p i:Fin.t (S n)), option (Fin.t n) -> Prop) P (S n) (Fin.FS p) (Fin.FS i) None) : forall n (p i:Fin.t (S n)), P n p i (lower p i). Proof. - fix 2. intros n p. + fix lower_ind 2. intros n p. refine (match p as p1 in Fin.t (S n1) return forall (i1:Fin.t (S n1)), P n1 p1 i1 (lower p1 i1) with diff --git a/test-suite/bugs/closed/3377.v b/test-suite/bugs/closed/3377.v index 8e9e3933c..abfcf1d35 100644 --- a/test-suite/bugs/closed/3377.v +++ b/test-suite/bugs/closed/3377.v @@ -5,6 +5,7 @@ Record prod A B := pair { fst : A; snd : B}. Goal fst (@pair Type Type Type Type). Set Printing All. match goal with |- ?f ?x => set (foo := f x) end. +Abort. Goal forall x : prod Set Set, x = @pair _ _ (fst x) (snd x). Proof. @@ -12,6 +13,6 @@ Proof. lazymatch goal with | [ |- ?x = @pair _ _ (?f ?x) (?g ?x) ] => pose f end. - (* Toplevel input, characters 7-44: Error: No matching clauses for match. *) +Abort. diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 606c6e084..668f6bb42 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -41,6 +41,8 @@ Proof. f_equal. 8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l and skipn n l = l *) +Abort. + Require Import List. Fixpoint replicate {A} (n : nat) (x : A) : list A := match n with 0 => nil | S n => x :: replicate n x end. diff --git a/test-suite/bugs/closed/4198.v b/test-suite/bugs/closed/4198.v index eb37141bc..28800ac05 100644 --- a/test-suite/bugs/closed/4198.v +++ b/test-suite/bugs/closed/4198.v @@ -13,6 +13,7 @@ Goal forall A (x x' : A) (xs xs' : list A) (H : x::xs = x'::xs'), match goal with | [ |- context G[@hd] ] => idtac end. +Abort. (* This second example comes from CFGV where inspecting subterms of a match is expecting to inspect first the term to match (even though @@ -35,3 +36,4 @@ Ltac mydestruct := Goal forall x, match x with 0 => 0 | _ => 0 end = 0. intros. mydestruct. +Abort. diff --git a/test-suite/bugs/closed/4403.v b/test-suite/bugs/closed/4403.v new file mode 100644 index 000000000..a80f38fe2 --- /dev/null +++ b/test-suite/bugs/closed/4403.v @@ -0,0 +1,3 @@ +(* -*- coq-prog-args: ("-type-in-type"); -*- *) + +Definition some_prop : Prop := Type. diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v deleted file mode 100644 index 2d41828f1..000000000 --- a/test-suite/bugs/closed/4722.v +++ /dev/null @@ -1 +0,0 @@ -(* -*- coq-prog-args: ("-R" "4722" "Foo") -*- *) diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata deleted file mode 120000 index b38e66e75..000000000 --- a/test-suite/bugs/closed/4722/tata +++ /dev/null @@ -1 +0,0 @@ -toto
\ No newline at end of file diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v index dbd71035d..1e1a4cb9c 100644 --- a/test-suite/bugs/closed/4782.v +++ b/test-suite/bugs/closed/4782.v @@ -6,6 +6,7 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. Goal p. Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. +Abort. (* A simplification of an example from coquelicot, which was failing at some time after a fix #4782 was committed. *) @@ -21,4 +22,5 @@ Set Typeclasses Debug. Goal forall (A:T) (x:dom A), pairT A A = pairT A A. intros. apply (F _ _) with (x,x). +Abort. diff --git a/test-suite/bugs/closed/5539.v b/test-suite/bugs/closed/5539.v new file mode 100644 index 000000000..48e5568e9 --- /dev/null +++ b/test-suite/bugs/closed/5539.v @@ -0,0 +1,15 @@ +Set Universe Polymorphism. + +Inductive D : nat -> Type := +| DO : D O +| DS n : D n -> D (S n). + +Fixpoint follow (n : nat) : D n -> Prop := + match n with + | O => fun d => let 'DO := d in True + | S n' => fun d => (let 'DS _ d' := d in fun f => f d') (follow n') + end. + +Definition step (n : nat) (d : D n) (H : follow n d) : + follow (S n) (DS n d) + := H. diff --git a/test-suite/bugs/closed/6770.v b/test-suite/bugs/closed/6770.v new file mode 100644 index 000000000..9bcc74083 --- /dev/null +++ b/test-suite/bugs/closed/6770.v @@ -0,0 +1,7 @@ +Section visibility. + + Let Fixpoint by_proof (n:nat) : True. + Proof. exact I. Defined. +End visibility. + +Fail Check by_proof. diff --git a/test-suite/bugs/closed/6951.v b/test-suite/bugs/closed/6951.v new file mode 100644 index 000000000..419f8d7c4 --- /dev/null +++ b/test-suite/bugs/closed/6951.v @@ -0,0 +1,2 @@ +Record float2 : Set := Float2 { Fnum : unit }. +Scheme Equality for float2. diff --git a/test-suite/bugs/closed/6956.v b/test-suite/bugs/closed/6956.v new file mode 100644 index 000000000..ee21adbbf --- /dev/null +++ b/test-suite/bugs/closed/6956.v @@ -0,0 +1,13 @@ +(** Used to trigger an anomaly with VM compilation *) + +Set Universe Polymorphism. + +Inductive t A : nat -> Type := +| nil : t A 0 +| cons : forall (h : A) (n : nat), t A n -> t A (S n). + +Definition case0 {A} (P : t A 0 -> Type) (H : P (nil A)) v : P v := +match v with +| nil _ => H +| _ => fun devil => False_ind (@IDProp) devil +end. diff --git a/test-suite/bugs/closed/7011.v b/test-suite/bugs/closed/7011.v new file mode 100644 index 000000000..296e4e11e --- /dev/null +++ b/test-suite/bugs/closed/7011.v @@ -0,0 +1,16 @@ +(* Fix and Cofix were missing in tactic unification *) + +Goal exists e, (fix foo (n : nat) : nat := match n with O => e | S n' => foo n' end) + = (fix foo (n : nat) : nat := match n with O => O | S n' => foo n' end). +Proof. + eexists. + reflexivity. +Qed. + +CoInductive stream := cons : nat -> stream -> stream. + +Goal exists e, (cofix foo := cons e foo) = (cofix foo := cons 0 foo). +Proof. + eexists. + reflexivity. +Qed. diff --git a/test-suite/bugs/closed/7113.v b/test-suite/bugs/closed/7113.v new file mode 100644 index 000000000..976e60f20 --- /dev/null +++ b/test-suite/bugs/closed/7113.v @@ -0,0 +1,10 @@ +Require Import Program.Tactics. +Section visibility. + + (* used to anomaly *) + Program Let Fixpoint ev' (n : nat) : bool := _. + Next Obligation. exact true. Qed. + + Check ev'. +End visibility. +Fail Check ev'. diff --git a/test-suite/bugs/closed/7392.v b/test-suite/bugs/closed/7392.v new file mode 100644 index 000000000..cf465c658 --- /dev/null +++ b/test-suite/bugs/closed/7392.v @@ -0,0 +1,9 @@ +Inductive R : nat -> Prop := ER : forall n, R n -> R (S n). + +Goal (forall (n : nat), R n -> False) -> True -> False. +Proof. +intros H0 H1. +eapply H0. +clear H1. +apply ER. +simpl. diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v new file mode 100644 index 000000000..40ca39e38 --- /dev/null +++ b/test-suite/bugs/closed/7462.v @@ -0,0 +1,13 @@ +(* Adding an only-printing notation should not override existing + interpretations for the same notation. *) + +Notation "$ x" := (@id nat x) (only parsing, at level 0). +Notation "$ x" := (@id bool x) (only printing, at level 0). +Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *) + +(* Adding an only-printing notation should not let believe + that a parsing rule has been given *) + +Notation "$ x" := (@id bool x) (only printing, at level 0). +Notation "$ x" := (@id nat x) (only parsing, at level 0). +Check $1. (* Was: Error: Syntax Error: Lexer: Undefined token *) diff --git a/test-suite/bugs/closed/7554.v b/test-suite/bugs/closed/7554.v new file mode 100644 index 000000000..12b0aa2cb --- /dev/null +++ b/test-suite/bugs/closed/7554.v @@ -0,0 +1,12 @@ +Require Import Coq.Program.Tactics. + +(* these should not result in anomalies *) + +Fail Program Lemma foo: + forall P, forall H, forall (n:nat), P n. + +Fail Program Lemma foo: + forall a (P : list a -> Prop), forall H, forall (n:list a), P n. + +Fail Program Lemma foo: + forall (a : Type) (P : list a -> Prop), forall H, forall (n:list a), P n. |