aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/opened')
-rw-r--r--test-suite/bugs/opened/1501.v96
-rw-r--r--test-suite/bugs/opened/2456.v53
-rw-r--r--test-suite/bugs/opened/2814.v5
-rw-r--r--test-suite/bugs/opened/3100.v9
-rw-r--r--test-suite/bugs/opened/3209.v17
-rw-r--r--test-suite/bugs/opened/3230.v14
-rw-r--r--test-suite/bugs/opened/3263.v232
-rw-r--r--test-suite/bugs/opened/3320.v4
-rw-r--r--test-suite/bugs/opened/3916.v3
-rw-r--r--test-suite/bugs/opened/3948.v25
-rw-r--r--test-suite/bugs/opened/4813.v4
11 files changed, 2 insertions, 460 deletions
diff --git a/test-suite/bugs/opened/1501.v b/test-suite/bugs/opened/1501.v
deleted file mode 100644
index b36f21da1b..0000000000
--- a/test-suite/bugs/opened/1501.v
+++ /dev/null
@@ -1,96 +0,0 @@
-Set Implicit Arguments.
-
-
-Require Export Relation_Definitions.
-Require Export Setoid.
-
-
-Section Essais.
-
-(* Parametrized Setoid *)
-Parameter K : Type -> Type.
-Parameter equiv : forall A : Type, K A -> K A -> Prop.
-Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x.
-Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x.
-Parameter equiv_trans : forall (A : Type) (x y z : K A), equiv x y -> equiv y z
--> equiv x z.
-
-(* basic operations *)
-Parameter val : forall A : Type, A -> K A.
-Parameter bind : forall A B : Type, K A -> (A -> K B) -> K B.
-
-Parameter
- bind_compat :
- forall (A B : Type) (m1 m2 : K A) (f1 f2 : A -> K B),
- equiv m1 m2 ->
- (forall x : A, equiv (f1 x) (f2 x)) -> equiv (bind m1 f1) (bind m2 f2).
-
-(* monad axioms *)
-Parameter
- bind_val_l :
- forall (A B : Type) (a : A) (f : A -> K B), equiv (bind (val a) f) (f a).
-Parameter
- bind_val_r :
- forall (A : Type) (m : K A), equiv (bind m (fun a => val a)) m.
-Parameter
- bind_assoc :
- forall (A B C : Type) (m : K A) (f : A -> K B) (g : B -> K C),
- equiv (bind (bind m f) g) (bind m (fun a => bind (f a) g)).
-
-
-Hint Resolve equiv_refl equiv_sym equiv_trans: monad.
-
-Instance equiv_rel A: Equivalence (@equiv A).
-Proof.
- constructor.
- intros xa; apply equiv_refl.
- intros xa xb; apply equiv_sym.
- intros xa xb xc; apply equiv_trans.
-Defined.
-
-Definition fequiv (A B: Type) (f g: A -> K B) := forall (x:A), (equiv (f x) (g
-x)).
-
-Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f.
-Proof.
- unfold fequiv; auto with monad.
-Qed.
-
-Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y
-x.
-Proof.
- unfold fequiv; auto with monad.
-Qed.
-
-Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y ->
-fequiv
-y z -> fequiv x z.
-Proof.
- unfold fequiv; intros; eapply equiv_trans; auto with monad.
-Qed.
-
-Instance fequiv_re A B: Equivalence (@fequiv A B).
-Proof.
- constructor.
- intros f; apply fequiv_refl.
- intros f g; apply fequiv_sym.
- intros f g h; apply fequiv_trans.
-Defined.
-
-Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B).
-Proof.
- unfold fequiv; intros x y xy_equiv f g fg_equiv; 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 *)
- Fail setoid_rewrite H2.
-Abort.
-(* trivial by equiv_refl.
-Qed.*)
diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v
deleted file mode 100644
index 5294adefd3..0000000000
--- a/test-suite/bugs/opened/2456.v
+++ /dev/null
@@ -1,53 +0,0 @@
-
-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.
-Admitted.
diff --git a/test-suite/bugs/opened/2814.v b/test-suite/bugs/opened/2814.v
deleted file mode 100644
index a740b4384d..0000000000
--- a/test-suite/bugs/opened/2814.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Require Import Program.
-
-Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False.
- intros.
- Fail induction H.
diff --git a/test-suite/bugs/opened/3100.v b/test-suite/bugs/opened/3100.v
deleted file mode 100644
index 6f35a74dc1..0000000000
--- a/test-suite/bugs/opened/3100.v
+++ /dev/null
@@ -1,9 +0,0 @@
-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/opened/3209.v b/test-suite/bugs/opened/3209.v
deleted file mode 100644
index 3203afa139..0000000000
--- a/test-suite/bugs/opened/3209.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Inductive eqT {A} (x : A) : A -> Type :=
- reflT : eqT x x.
-Definition Bi_inv (A B : Type) (f : (A -> B)) :=
- sigT (fun (g : B -> A) =>
- sigT (fun (h : B -> A) =>
- sigT (fun (α : forall b : B, eqT (f (g b)) b) =>
- forall a : A, eqT (h (f a)) a))).
-Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f).
-
-Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B).
-Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B :=
- sigT_rect (fun _ => TEquiv A B)
- (fun (f : TEquiv A B -> eqT A B) H =>
- sigT_rect (fun _ => TEquiv A B)
- (fun g _ => g e)
- H)
- (UA A B).
diff --git a/test-suite/bugs/opened/3230.v b/test-suite/bugs/opened/3230.v
deleted file mode 100644
index 265310b1a3..0000000000
--- a/test-suite/bugs/opened/3230.v
+++ /dev/null
@@ -1,14 +0,0 @@
-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/opened/3263.v b/test-suite/bugs/opened/3263.v
deleted file mode 100644
index f0c707bd10..0000000000
--- a/test-suite/bugs/opened/3263.v
+++ /dev/null
@@ -1,232 +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) *)
-Fail Timeout 60 Defined. (* Timeout! *)
diff --git a/test-suite/bugs/opened/3320.v b/test-suite/bugs/opened/3320.v
deleted file mode 100644
index 05cf73281d..0000000000
--- a/test-suite/bugs/opened/3320.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Goal forall x : nat, True.
- fix 1.
- assumption.
-Fail Qed.
diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v
deleted file mode 100644
index fd95503e6b..0000000000
--- a/test-suite/bugs/opened/3916.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Require Import List.
-
-Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *)
diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v
deleted file mode 100644
index 5c4b4277b2..0000000000
--- a/test-suite/bugs/opened/3948.v
+++ /dev/null
@@ -1,25 +0,0 @@
-Module Type S.
-Parameter t : Type.
-End S.
-
-Module Bar(X : S).
-Proof.
- Definition elt := X.t.
- Axiom fold : elt.
-End Bar.
-
-Module Make (X: S) := Bar(X).
-
-Declare Module X : S.
-
-Module Type Interface.
- Parameter constant : unit.
-End Interface.
-
-Module DepMap : Interface.
- Module Dom := Make(X).
- Definition constant : unit :=
- let _ := @Dom.fold in tt.
-End DepMap.
-
-Print Assumptions DepMap.constant.
diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v
index b75170179b..2ac5535934 100644
--- a/test-suite/bugs/opened/4813.v
+++ b/test-suite/bugs/opened/4813.v
@@ -1,5 +1,5 @@
-(* An example one would like to see succeeding *)
+Require Import Program.Tactics.
Record T := BT { t : Set }.
Record U (x : T) := BU { u : t x -> Prop }.
-Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.
+Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 00:29:23 +0000