aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/bug_10025.v39
-rw-r--r--test-suite/bugs/closed/bug_10026.v3
-rw-r--r--test-suite/bugs/closed/bug_10031.v9
-rw-r--r--test-suite/bugs/closed/bug_10189.v9
-rw-r--r--test-suite/bugs/closed/bug_3754.v287
-rw-r--r--test-suite/bugs/closed/bug_3890.v12
-rw-r--r--test-suite/bugs/closed/bug_4429.v31
-rw-r--r--test-suite/bugs/closed/bug_4580.v1
-rw-r--r--test-suite/bugs/closed/bug_4638.v12
-rw-r--r--test-suite/bugs/closed/bug_5752.v8
-rw-r--r--test-suite/bugs/closed/bug_9344.v2
-rw-r--r--test-suite/bugs/closed/bug_9348.v3
12 files changed, 384 insertions, 32 deletions
diff --git a/test-suite/bugs/closed/bug_10025.v b/test-suite/bugs/closed/bug_10025.v
new file mode 100644
index 0000000000..1effc771b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10025.v
@@ -0,0 +1,39 @@
+Require Import Program.
+
+Axiom I : Type.
+
+Inductive S : Type := NT : I -> S.
+
+Axiom F : S -> Type.
+
+Axiom G : forall (s : S), F s -> Type.
+
+Section S.
+
+Variable init : I.
+Variable my_s : F (NT init).
+
+Inductive foo : forall (s: S) (hole_sem: F s), Type :=
+| Foo : foo (NT init) my_s.
+
+Goal forall
+ (n : I) (s : F (NT n)) (ptz : foo (NT n) s) (pt : G (NT n) s) (x : unit),
+match
+ match x with tt => tt end
+with
+| tt =>
+ match
+ match ptz in foo x s return (forall _ : G x s, unit) with
+ | Foo => fun _ : G (NT init) my_s => tt
+ end pt
+ with
+ | tt => False
+ end
+end.
+Proof.
+dependent destruction ptz.
+(* Check well-typedness of goal *)
+match goal with [ |- ?P ] => let t := type of P in idtac end.
+Abort.
+
+End S.
diff --git a/test-suite/bugs/closed/bug_10026.v b/test-suite/bugs/closed/bug_10026.v
new file mode 100644
index 0000000000..0d3142d0f2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10026.v
@@ -0,0 +1,3 @@
+Require Import Coq.Lists.List.
+Set Debug RAKAM.
+Check fun _ => fold_right (fun A B => prod A B) unit _.
diff --git a/test-suite/bugs/closed/bug_10031.v b/test-suite/bugs/closed/bug_10031.v
new file mode 100644
index 0000000000..15b53de00d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10031.v
@@ -0,0 +1,9 @@
+Require Import Int63 ZArith.
+
+Open Scope int63_scope.
+
+Goal False.
+cut (let (q, r) := (0, 0) in ([|q|], [|r|]) = (9223372036854775808%Z, 0%Z));
+ [discriminate| ].
+Fail (change (0, 0) with (diveucl_21 1 0 1); apply diveucl_21_spec).
+Abort.
diff --git a/test-suite/bugs/closed/bug_10189.v b/test-suite/bugs/closed/bug_10189.v
new file mode 100644
index 0000000000..d603bff386
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10189.v
@@ -0,0 +1,9 @@
+Definition foo : forall (x := unit) {y : nat}, nat := fun y => y.
+Check foo (y := 3). (*We fail to get implicits in the type past a let-in*)
+Definition foo' : forall (x : Set) {y : nat}, nat := fun _ y => y.
+Check foo' unit (y := 3). (* It works with a function binder *)
+
+Definition bar := let f {x} : nat -> nat := fun y => x in f (x := 3).
+(* Adding bar : nat -> nat gives implicits-in-term warning *)
+Fail Check bar (x := 3).
+(* The implicits from the type of the local definition leak to the outer term *)
diff --git a/test-suite/bugs/closed/bug_3754.v b/test-suite/bugs/closed/bug_3754.v
new file mode 100644
index 0000000000..7031cbf132
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3754.v
@@ -0,0 +1,287 @@
+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.
+ rewrite (concat_Ap ff2).
+ Abort.
+
+End Factorization.
diff --git a/test-suite/bugs/closed/bug_3890.v b/test-suite/bugs/closed/bug_3890.v
new file mode 100644
index 0000000000..e1823ac54c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3890.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+Class Bar := b : Type.
+
+Instance foo : Foo.
+
+Instance bar : Bar.
+exact Type.
+Defined.
+
+Defined.
diff --git a/test-suite/bugs/closed/bug_4429.v b/test-suite/bugs/closed/bug_4429.v
deleted file mode 100644
index bf0e570ab8..0000000000
--- a/test-suite/bugs/closed/bug_4429.v
+++ /dev/null
@@ -1,31 +0,0 @@
-Require Import Arith.Compare_dec.
-Require Import Unicode.Utf8.
-
-Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
- match n with
- | O => x
- | S n' => f (my_nat_iter n' f x)
- end.
-
-Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
- match mn with
- | (0, 0) => 0
- | (0, S n') => S n'
- | (S m', 0) => S m'
- | (S m', S n') =>
- match le_gt_dec (S m') (S n') with
- | left _ => f (S m', S n' - S m')
- | right _ => f (S m' - S n', S n')
- end
- end.
-
-Axiom max_correct_l : ∀ m n : nat, m <= max m n.
-Axiom max_correct_r : ∀ m n : nat, n <= max m n.
-
-Hint Resolve max_correct_l max_correct_r : arith.
-
-Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
-Proof.
- intros.
- Timeout 3 eauto with arith.
-Qed.
diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v
index a8a446cc9b..3f40569d61 100644
--- a/test-suite/bugs/closed/bug_4580.v
+++ b/test-suite/bugs/closed/bug_4580.v
@@ -2,6 +2,5 @@ Require Import Program.
Class Foo (A : Type) := foo : A.
-Unset Refine Instance Mode.
Program Instance f1 : Foo nat := S _.
Next Obligation. exact 0. Defined.
diff --git a/test-suite/bugs/closed/bug_4638.v b/test-suite/bugs/closed/bug_4638.v
new file mode 100644
index 0000000000..951fe5302b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4638.v
@@ -0,0 +1,12 @@
+Set Nested Proofs Allowed.
+
+Class Foo.
+
+Goal True.
+
+Instance foo: Foo.
+Qed.
+
+trivial.
+
+Qed.
diff --git a/test-suite/bugs/closed/bug_5752.v b/test-suite/bugs/closed/bug_5752.v
new file mode 100644
index 0000000000..b4218d66df
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5752.v
@@ -0,0 +1,8 @@
+Class C (A : Type) := c : A.
+
+Hint Mode C ! : typeclass_instances.
+
+Goal forall f : (forall A, C A -> C (list A)), True.
+intros.
+ Check c. (* Loops if modes are ignored. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_9344.v b/test-suite/bugs/closed/bug_9344.v
new file mode 100644
index 0000000000..0d44c9721a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9344.v
@@ -0,0 +1,2 @@
+Compute _ I.
+Eval native_compute in _ I.
diff --git a/test-suite/bugs/closed/bug_9348.v b/test-suite/bugs/closed/bug_9348.v
new file mode 100644
index 0000000000..a4673b5ffc
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9348.v
@@ -0,0 +1,3 @@
+Set Primitive Projections.
+Record r {A} := R {f : A -> A}.
+Compute f _ I.
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-03 19:34:38 +0000