From cf9f4e566b87d2875f757bb7d54ee4421988e315 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 10 May 2019 12:32:07 +0200 Subject: Make detyping robust w.r.t. indexed anonymous variables I don't think there's a reason to treat such variables more severely than unbound variables. This anomaly is often raised by debug printers (e.g. when studying complex scenarios using `Set Unification Debug`), and so makes debugging less convenient. Fixes #3754, fixes #10026. --- test-suite/bugs/opened/bug_3754.v | 285 -------------------------------------- 1 file changed, 285 deletions(-) delete mode 100644 test-suite/bugs/opened/bug_3754.v (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/bug_3754.v b/test-suite/bugs/opened/bug_3754.v deleted file mode 100644 index 18820b1a4c..0000000000 --- a/test-suite/bugs/opened/bug_3754.v +++ /dev/null @@ -1,285 +0,0 @@ -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. - Fail rewrite (concat_Ap ff2). - Abort. -- cgit v1.2.3 From c352873936db93c251c544383853474736f128d6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Jan 2019 00:48:36 +0100 Subject: Remove VtUnknown classification This clean-up removes the dependency of the current proof mode (and hence the parsing state) on unification. The current proof mode can now be known simply by parsing and elaborating attributes. We give access to attributes from the classifier for this purpose. We remove the infamous `VtUnknown` code path in the STM which is known to be buggy. Fixes #3632 #3890 #4638. --- test-suite/bugs/opened/bug_3890.v | 22 ---------------------- 1 file changed, 22 deletions(-) delete mode 100644 test-suite/bugs/opened/bug_3890.v (limited to 'test-suite/bugs/opened') diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v deleted file mode 100644 index 9d83743b2a..0000000000 --- a/test-suite/bugs/opened/bug_3890.v +++ /dev/null @@ -1,22 +0,0 @@ -Set Nested Proofs Allowed. - -Class Foo. -Class Bar := b : Type. - -Set Refine Instance Mode. -Instance foo : Foo := _. -Unset Refine Instance Mode. -(* 1 subgoals, subgoal 1 (ID 4) - - ============================ - Foo *) - -Instance bar : Bar. -exact Type. -Defined. -(* bar is defined *) - -About foo. -(* foo not a defined object. *) - -Fail Defined. -- cgit v1.2.3