From 4ae315f92e4a9849a56d3d9b0da33027f362d6e8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 10:55:15 +0200 Subject: Univs/Program/Function: Fix bug #4725 - In Program, a check_evars_are_solved was introduced too early. Program does it's checking of evars by itself. - In Function, the universe environments were not threaded correctly. --- test-suite/bugs/closed/4725.v | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 test-suite/bugs/closed/4725.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v new file mode 100644 index 0000000000..fd5e0fb60d --- /dev/null +++ b/test-suite/bugs/closed/4725.v @@ -0,0 +1,38 @@ +Require Import EquivDec Equivalence List Program. +Require Import Relation_Definitions. +Import ListNotations. +Generalizable All Variables. + +Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V +:= + match l with + | nil => nil + | y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl) + end. + +Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (xs : list V) (x : V) : + length (removeV x xs) < length (x :: xs). + Proof. Admitted. + +(* Function version *) +Set Printing Universes. + +Require Import Recdef. + +Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (l : list V) { measure length l} := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) + end. +Proof. intros. apply remove_le. Qed. + +(* Program version *) + +Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V) + { measure (@length V l) lt } := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _ + end. -- cgit v1.2.3 From 1e389def84cc3eafc8aa5d1a1505f078a58234bd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 23 May 2016 19:47:38 +0200 Subject: Univs/(e)auto: fix bug #4450 polymorphic exact hints The exact and e_exact tactics were not registering the universes and constraints of the hint correctly. Now using the same connect_hint_clenv as unify_resolve, they do. Also correct the implementation of prepare_hint to normalize the universes of the hint before abstracting its undefined universes. They are going to be refreshed at each application. This means that eauto using term can use multiple different instantiations of the universes of term if term introduces new universes. If we want just one instantiation then the term should be abbreviated in the goal first. --- test-suite/bugs/closed/4450.v | 58 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 58 insertions(+) create mode 100644 test-suite/bugs/closed/4450.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v new file mode 100644 index 0000000000..ecebaba812 --- /dev/null +++ b/test-suite/bugs/closed/4450.v @@ -0,0 +1,58 @@ +Polymorphic Axiom inhabited@{u} : Type@{u} -> Prop. + +Polymorphic Axiom unit@{u} : Type@{u}. +Polymorphic Axiom tt@{u} : inhabited unit@{u}. + +Polymorphic Hint Resolve tt : the_lemmas. +Set Printing All. +Set Printing Universes. +Goal inhabited unit. +Proof. + eauto with the_lemmas. +Qed. + +Universe u. +Axiom f : Type@{u} -> Prop. +Lemma fapp (X : Type) : f X -> False. +Admitted. +Polymorphic Axiom funi@{i} : f unit@{i}. + +Goal (forall U, f U) -> (*(f unit -> False) -> *)False /\ False. + eauto using (fapp unit funi). (* The two fapp's have different universes *) +Qed. + +Hint Resolve (fapp unit funi) : mylems. + +Goal (forall U, f U) -> (*(f unit -> False) -> *)False /\ False. + eauto with mylems. (* Forces the two fapps at the same level *) +Qed. + +Goal (forall U, f U) -> (f unit -> False) -> False /\ False. + eauto. (* Forces the two fapps at the same level *) +Qed. + +Polymorphic Definition MyType@{i} := Type@{i}. +Universes l m n. +Constraint l < m. +Polymorphic Axiom maketype@{i} : MyType@{i}. + +Goal MyType@{l}. +Proof. + Fail solve [ eauto using maketype@{m} ]. + eauto using maketype. + Undo. + eauto using maketype@{n}. +Qed. + +Axiom foo : forall (A : Type), list A. +Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A. + +Universe x y. +Goal list Type@{x}. +Proof. + eauto using (foo Type). (* Refreshes the term *) + Undo. + eauto using foo. Show Universes. + Undo. + eauto using foop. Show Proof. Show Universes. +Qed. \ No newline at end of file -- cgit v1.2.3 From 784d82dc1a709c4c262665a4cd4eb0b1bd1487a0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Jun 2016 18:36:58 +0200 Subject: Univs: fix for part #2 of bug #4816. Check that the polymorphic status of everything that is parameterized in nested sections is coherent. --- test-suite/bugs/closed/4816.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 test-suite/bugs/closed/4816.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v new file mode 100644 index 0000000000..ef79b9869b --- /dev/null +++ b/test-suite/bugs/closed/4816.v @@ -0,0 +1,18 @@ +Section foo. +Polymorphic Universes A B. +Constraint A <= B. +End foo. +(* gives an anomaly Universe undefined *) + +or even, a refinement of #4503: +Require Coq.Classes.RelationClasses. + +Class PreOrder (A : Type) (r : A -> A -> Type) : Type := +{ refl : forall x, r x x }. + +Section foo. + Polymorphic Universes A. + Section bar. + Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + End bar. +End foo. \ No newline at end of file -- cgit v1.2.3 From 3bb0753d1589489b0e33f6a116a84c4fa72ed49f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Jun 2016 22:28:14 +0200 Subject: Fix test-suite file, only part 2 is fixed in 8.5 --- test-suite/bugs/closed/4816.v | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v index ef79b9869b..5ba0787ee7 100644 --- a/test-suite/bugs/closed/4816.v +++ b/test-suite/bugs/closed/4816.v @@ -1,10 +1,3 @@ -Section foo. -Polymorphic Universes A B. -Constraint A <= B. -End foo. -(* gives an anomaly Universe undefined *) - -or even, a refinement of #4503: Require Coq.Classes.RelationClasses. Class PreOrder (A : Type) (r : A -> A -> Type) : Type := @@ -13,6 +6,6 @@ Class PreOrder (A : Type) (r : A -> A -> Type) : Type := Section foo. Polymorphic Universes A. Section bar. - Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. End foo. \ No newline at end of file -- cgit v1.2.3 From 2b19f0923a314a6df0a9cfed0f56cf2405e6591c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 14 Jun 2016 11:40:24 +0200 Subject: Admitted: fix #4818 return initial stmt and univs --- test-suite/bugs/closed/4818.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test-suite/bugs/closed/4818.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v new file mode 100644 index 0000000000..904abb2287 --- /dev/null +++ b/test-suite/bugs/closed/4818.v @@ -0,0 +1,24 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *) +(* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *) +(* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3 + coqtop version 8.5pl1 (June 2016) *) +Set Universe Polymorphism. + +Inductive GCov (I : Type) : Type := | Foo : I -> GCov I. + +Section Product. + +Variables S IS : Type. +Variable locS : IS -> True. + +Goal GCov (IS * S) -> GCov IS. +intros X0. induction X0; intros. +destruct i. +specialize (locS i). +clear -locS. +destruct locS. Show Universes. +Admitted. + +(* +Anomaly: Universe Product.5189 undefined. Please report. +*) -- cgit v1.2.3 From a7ea32fbf3829d1ce39ce9cc24b71791727090c5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 26 Jun 2016 23:29:55 +0200 Subject: More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause). When typing a "with clause fails, type classes are used to possibly help to insert coercions. If this heuristic fails, do not consider it anymore to be the best failure since it has made type classes choices which may be inconsistent with other constraints and on which no backtracking is possible anymore (see new example in test suite file 4782.v). This does not mean that using type classes at this point is good. It may find an instance which help to find a coercion, but which might still be a choice of instance and coercion which is incompatible with other constraints. I tend to think that a convenient way to go to deal with the absence of backtracking in inserting coercions would be to have special For the record, here is a some comments of what happens regarding f9695eb4b and 827663982. In the presence of an instance (x:=t) given in a "with" clause, with t:T, and x expected of type T', the situation is the following: Before f9695eb4b: - If T and T' are closed and T <= T' is not satisfiable (no coercion or not convertible), the test for possible insertion of a coercion is postponed to w_merge, even though there is no way to get more information since T ant T' are closed. As a result, t may be ill-typed and the unification may try to unify ill-formed terms, leading to #4872. - If T and T' are not closed and contains evars of type a type class, inference of type classes is tried. If it fails, e.g. because a wrong type class instance is found, it was postponed to w_merge as above, and the test for coercion is retried now interleaved with type classes. After f9695eb4b and 827663982e: - If T and T' are closed and T <= T' is not satisfiable (no coercion or not convertible), the test for possible insertion of a coercion is an immediate failure. This fixes #4872. - However, If T and T' are not closed and contains evars of type a type class, inference of type classes is tried. If it gives closed terms and fails, this is immediate failure without backtracking on type classes, resulting in the problem added here to file 4872.v. The current fix does not consider the result of the use of type classes while trying to insert a coercion to be the last word on it. So, it fails with an error which is not the error for conversion of closed terms (ConversionFailed), therefore in a way expected by f9695eb4b and 827663982e, and the "with" typing problem is then postponed again. --- test-suite/bugs/closed/4782.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v index ed44437861..dbd71035dc 100644 --- a/test-suite/bugs/closed/4782.v +++ b/test-suite/bugs/closed/4782.v @@ -7,3 +7,18 @@ 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. +(* A simplification of an example from coquelicot, which was failing + at some time after a fix #4782 was committed. *) + +Record T := { dom : Type }. +Definition pairT A B := {| dom := (dom A * dom B)%type |}. +Class C (A:Type). +Parameter B:T. +Instance c (A:T) : C (dom A). +Instance cn : C (dom B). +Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A. +Set Typeclasses Debug. +Goal forall (A:T) (x:dom A), pairT A A = pairT A A. +intros. +apply (F _ _) with (x,x). + -- cgit v1.2.3