aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/4306.v32
-rw-r--r--test-suite/bugs/closed/5377.v54
-rw-r--r--test-suite/bugs/closed/5449.v6
-rw-r--r--test-suite/bugs/closed/5476.v28
-rw-r--r--test-suite/bugs/closed/5501.v21
-rw-r--r--test-suite/failure/proofirrelevance.v5
-rw-r--r--test-suite/output/Search.out8
-rw-r--r--test-suite/output/Search.v10
-rw-r--r--test-suite/success/Case19.v2
-rw-r--r--test-suite/success/ImplicitArguments.v6
-rw-r--r--test-suite/success/boundvars.v14
-rw-r--r--test-suite/success/polymorphism.v32
-rw-r--r--test-suite/success/transparent_abstract.v21
13 files changed, 233 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v
new file mode 100644
index 000000000..4aef5bb95
--- /dev/null
+++ b/test-suite/bugs/closed/4306.v
@@ -0,0 +1,32 @@
+Require Import List.
+Require Import Arith.
+Require Import Recdef.
+Require Import Omega.
+
+Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
+ match xys with
+ | (nil, _) => snd xys
+ | (_, nil) => fst xys
+ | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+ | Lt => x :: foo (xs', y :: ys')
+ | Eq => x :: foo (xs', ys')
+ | Gt => y :: foo (x :: xs', ys')
+ end
+ end.
+Proof.
+ intros; simpl; omega.
+ intros; simpl; omega.
+ intros; simpl; omega.
+Qed.
+
+Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
+ let (xs, ys) := xys in
+ match (xs, ys) with
+ | (nil, _) => ys
+ | (_, nil) => xs
+ | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+ | Lt => x :: foo (xs', ys)
+ | Eq => x :: foo (xs', ys')
+ | Gt => y :: foo (xs, ys')
+ end
+ end. \ No newline at end of file
diff --git a/test-suite/bugs/closed/5377.v b/test-suite/bugs/closed/5377.v
new file mode 100644
index 000000000..130d9f9ab
--- /dev/null
+++ b/test-suite/bugs/closed/5377.v
@@ -0,0 +1,54 @@
+Goal ((forall (t : Type) (x y : t),
+ True ->
+ x = y)) -> False.
+Proof.
+ intro HG.
+ let P := lazymatch goal with
+ | [ H : forall t x y, True -> @?P t x y
+ |- _ ]
+ => P
+ end in
+ pose (f := P).
+ unify f (fun (t : Type) (x y : t) => x = y).
+Abort.
+
+Goal True.
+Proof.
+let c := lazymatch constr:(fun (T : nat -> Type) (y : nat) (_ : T y) => y) with
+ | fun _ y _ => @?C y => C
+ end in
+pose (f := c).
+unify f (fun n : nat => n).
+Abort.
+
+Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
+Proof.
+intro.
+let P := lazymatch goal with
+| [ H : forall y, @?P y -> @?P y \/ _ |- _ ]
+ => P
+end in
+pose (f := P).
+unify f (fun x : nat => x = x).
+Abort.
+
+Goal (forall x : nat, x = x -> x = x \/ x = x) -> True.
+Proof.
+intro.
+lazymatch goal with
+| [ H : forall y, @?P y -> @?Q y \/ _ |- _ ]
+ => idtac
+end.
+Abort.
+
+Axiom eq : forall {T} (_ : T), Prop.
+
+Goal forall _ : (forall t (_ : eq t) (x : t), eq x), Prop.
+Proof.
+intro.
+let P := lazymatch goal with
+| [ H : forall t _ x, @?P t x |- _ ]
+ => P
+end in
+pose (f := P).
+Abort.
diff --git a/test-suite/bugs/closed/5449.v b/test-suite/bugs/closed/5449.v
new file mode 100644
index 000000000..d7fc2aaa0
--- /dev/null
+++ b/test-suite/bugs/closed/5449.v
@@ -0,0 +1,6 @@
+(* An example of decide equality which was failing due to a lhs dep into the rhs *)
+
+Require Import Coq.PArith.BinPos.
+Goal forall x y, {Pos.compare_cont Gt x y = Gt} + {Pos.compare_cont Gt x y <> Gt}.
+intros.
+decide equality.
diff --git a/test-suite/bugs/closed/5476.v b/test-suite/bugs/closed/5476.v
new file mode 100644
index 000000000..b2d9d943b
--- /dev/null
+++ b/test-suite/bugs/closed/5476.v
@@ -0,0 +1,28 @@
+Require Setoid.
+
+Goal forall (P : Prop) (T : Type) (m m' : T) (T0 T1 : Type) (P2 : forall _ :
+Prop, Prop)
+ (P0 : Set) (x0 : P0) (P1 : forall (_ : P0) (_ : T), Prop)
+ (P3 : forall (_ : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (_ :
+T) (_ : Prop), Prop)
+ (o : forall _ : P0, option T1)
+ (_ : P3
+ (fun (k : P0) (_ : T0) (_ : Prop) =>
+ match o k return Prop with
+ | Some _ => True
+ | None => False
+ end) m' P) (_ : P2 (P1 x0 m))
+ (_ : forall (f : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (m1 m2
+: T)
+ (k : P0) (e : T0) (_ : P2 (P1 k m1)), iff (P3 f m2 P)
+(f k e (P3 f m1 P))), False.
+Proof.
+ intros ???????????? H0 H H1.
+ rewrite H1 in H0; eauto with nocore.
+ { lazymatch goal with
+ | H : match ?X with _ => _ end |- _
+ => first [ lazymatch goal with
+ | [ H' : context[X] |- _ ] => idtac H
+ end
+ | fail 1 "could not find" X ]
+ end.
diff --git a/test-suite/bugs/closed/5501.v b/test-suite/bugs/closed/5501.v
new file mode 100644
index 000000000..24739a365
--- /dev/null
+++ b/test-suite/bugs/closed/5501.v
@@ -0,0 +1,21 @@
+Set Universe Polymorphism.
+
+Record Pred@{A} :=
+ { car :> Type@{A}
+ ; P : car -> Prop
+ }.
+
+Class All@{A} (A : Pred@{A}) : Type :=
+ { proof : forall (a : A), P A a
+ }.
+
+Record Pred_All@{A} : Type :=
+ { P' :> Pred@{A}
+ ; P'_All : All P'
+ }.
+
+Global Instance Pred_All_instance (A : Pred_All) : All A := P'_All A.
+
+Definition Pred_All_proof {A : Pred_All} (a : A) : P A a.
+Proof.
+solve[auto using proof].
diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v
index b62f9b686..bb9579d48 100644
--- a/test-suite/failure/proofirrelevance.v
+++ b/test-suite/failure/proofirrelevance.v
@@ -1,6 +1,5 @@
-(* This was working in version 8.1beta (bug in the Sort-polymorphism
- of inductive types), but this is inconsistent with classical logic
- in Prop *)
+(* This was working in version 8.1beta (bug in template polymorphism),
+ but this is inconsistent with classical logic in Prop *)
Inductive bool_in_prop : Type := hide : bool -> bool_in_prop
with bool : Type := true : bool | false : bool.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 81fda176e..7446c17d9 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -98,6 +98,14 @@ h: n <> newdef n
h': newdef n <> n
h: n <> newdef n
h: n <> newdef n
+h: n <> newdef n
+h': newdef n <> n
+The command has indeed failed with message:
+No such goal.
+The command has indeed failed with message:
+Query commands only support the single numbered goal selector.
+The command has indeed failed with message:
+Query commands only support the single numbered goal selector.
h: P n
h': ~ P n
h: P n
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 2a0f0b407..82096f29b 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro". (* andb_prop *)
Definition newdef := fun x:nat => x.
Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
- intros n h h'.
+ cut False.
+ intros _ n h h'.
Search n. (* search hypothesis *)
Search newdef. (* search hypothesis *)
Search ( _ <> newdef _). (* search hypothesis, pattern *)
Search ( _ <> newdef _) -"h'". (* search hypothesis, pattern *)
+
+ 1:Search newdef.
+ 2:Search newdef.
+
+ Fail 3:Search newdef.
+ Fail 1-2:Search newdef.
+ Fail all:Search newdef.
Abort.
Goal forall n (P:nat -> Prop), P n -> ~P n -> False.
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
index c29e52978..e59828def 100644
--- a/test-suite/success/Case19.v
+++ b/test-suite/success/Case19.v
@@ -1,5 +1,5 @@
(* This used to fail in Coq version 8.1 beta due to a non variable
- universe (issued by the inductive sort-polymorphism) being sent by
+ universe (issued by template polymorphism) being sent by
pretyping to the kernel (bug #1182) *)
Variable T : Type.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f702aa62f..f07773f8b 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -21,3 +21,9 @@ Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A
(* Test sharing information between different hypotheses *)
Parameters (a:_) (b:a=0).
+
+(* These examples were failing due to a lifting wrongly taking let-in into account *)
+
+Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
+
+Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
new file mode 100644
index 000000000..fafe27292
--- /dev/null
+++ b/test-suite/success/boundvars.v
@@ -0,0 +1,14 @@
+(* An example showing a bug in the detection of free variables *)
+(* "x" is not free in the common type of "x" and "y" *)
+
+Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
+
+(* An example showing a bug in the detection of bound variables *)
+
+Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl.
+intro.
+match goal with
+|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end.
+intro.
+Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *)
+Abort.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 878875bd9..66ff55edc 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
Type)) eq_refl.
-End Hurkens'. \ No newline at end of file
+End Hurkens'.
+
+Module Anonymous.
+ Set Universe Polymorphism.
+
+ Definition defaultid := (fun x => x) : Type -> Type.
+ Definition collapseid := defaultid@{_ _}.
+ Check collapseid@{_}.
+
+ Definition anonid := (fun x => x) : Type -> Type@{_}.
+ Check anonid@{_}.
+
+ Definition defaultalg := (fun x : Type => x) (Type : Type).
+ Definition usedefaultalg := defaultalg@{_ _ _}.
+ Check usedefaultalg@{_ _}.
+
+ Definition anonalg := (fun x : Type@{_} => x) (Type : Type).
+ Check anonalg@{_ _}.
+
+ Definition unrelated@{i j} := nat.
+ Definition useunrelated := unrelated@{_ _}.
+ Check useunrelated@{_ _}.
+
+ Definition inthemiddle@{i j k} :=
+ let _ := defaultid@{i j} in
+ anonalg@{k j}.
+ (* i <= j < k *)
+ Definition collapsethemiddle := inthemiddle@{i _ j}.
+ Check collapsethemiddle@{_ _}.
+
+End Anonymous.
diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v
new file mode 100644
index 000000000..ff4509c4a
--- /dev/null
+++ b/test-suite/success/transparent_abstract.v
@@ -0,0 +1,21 @@
+Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T.
+Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances.
+
+Goal True /\ True.
+Proof.
+ split.
+ transparent_abstract exact I using foo.
+ let x := (eval hnf in foo) in constr_eq x I.
+ let x := constr:(ltac:(constructor) : True) in
+ let T := type of x in
+ let x := constr:(_ : by_transparent_abstract x) in
+ let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in
+ pose x as x'.
+ simpl in x'.
+ let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac.
+ hnf in x'.
+ let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0.
+ exact x'.
+Defined.
+Check eq_refl : I = foo.
+Eval compute in foo.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:11:03 +0000