diff options
Diffstat (limited to 'test-suite/bugs/closed')
122 files changed, 4153 insertions, 387 deletions
diff --git a/test-suite/bugs/closed/1850.v b/test-suite/bugs/closed/1850.v new file mode 100644 index 0000000000..26b48093b7 --- /dev/null +++ b/test-suite/bugs/closed/1850.v @@ -0,0 +1,4 @@ +Parameter P : Type -> Type -> Type. +Notation "e |= t --> v" := (P e t v) (at level 100, t at level 54). +Fail Check (nat |= nat --> nat). + diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v new file mode 100644 index 0000000000..13ec5bea9b --- /dev/null +++ b/test-suite/bugs/closed/2016.v @@ -0,0 +1,62 @@ +(* Coq 8.2beta4 *) +Require Import Classical_Prop. + +Record coreSemantics : Type := CoreSemantics { + core: Type; + corestep: core -> core -> Prop; + corestep_fun: forall q q1 q2, corestep q q1 -> corestep q q2 -> q1 = q2 +}. + +Definition state : Type := {sem: coreSemantics & sem.(core)}. + +Inductive step: state -> state -> Prop := + | step_core: forall sem st st' + (Hcs: sem.(corestep) st st'), + step (existT _ sem st) (existT _ sem st'). + +Lemma step_fun: forall st1 st2 st2', step st1 st2 -> step st1 st2' -> st2 = st2'. +Proof. +intros. +inversion H; clear H; subst. inversion H0; clear H0; subst; auto. +generalize (inj_pairT2 _ _ _ _ _ H2); clear H2; intro; subst. +rewrite (corestep_fun _ _ _ _ Hcs Hcs0); auto. +Qed. + +Record oe_core := oe_Core { + in_core: Type; + in_corestep: in_core -> in_core -> Prop; + in_corestep_fun: forall q q1 q2, in_corestep q q1 -> in_corestep q q2 -> q1 = q2; + in_q: in_core +}. + +Definition oe2coreSem (oec : oe_core) : coreSemantics := + CoreSemantics oec.(in_core) oec.(in_corestep) oec.(in_corestep_fun). + +Definition oe_corestep (q q': oe_core) := + step (existT _ (oe2coreSem q) q.(in_q)) (existT _ (oe2coreSem q') q'.(in_q)). + +Lemma inj_pairT1: forall (U: Type) (P: U -> Type) (p1 p2: U) x y, + existT P p1 x = existT P p2 y -> p1=p2. +Proof. intros; injection H; auto. +Qed. + +Definition f := CoreSemantics oe_core. + +Lemma oe_corestep_fun: forall q q1 q2, + oe_corestep q q1 -> oe_corestep q q2 -> q1 = q2. +Proof. +unfold oe_corestep; intros. +assert (HH:= step_fun _ _ _ H H0); clear H H0. +destruct q1; destruct q2; unfold oe2coreSem; simpl in *. +generalize (inj_pairT1 _ _ _ _ _ _ HH); clear HH; intros. +injection H; clear H; intros. +revert in_q1 in_corestep1 in_corestep_fun1 + H. +pattern in_core1. +apply eq_ind_r with (x := in_core0). +admit. +apply sym_eq. +(** good to here **) +Show Universes. +Print Universes. +Fail apply H0.
\ No newline at end of file diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v new file mode 100644 index 0000000000..a5f4ae64a0 --- /dev/null +++ b/test-suite/bugs/closed/2584.v @@ -0,0 +1,89 @@ +Require Import List. + +Set Implicit Arguments. + +Definition err : Type := unit. + +Inductive res (A: Type) : Type := +| OK: A -> res A +| Error: err -> res A. + +Implicit Arguments Error [A]. + +Set Printing Universes. + +Section FOO. + +Inductive ftyp : Type := + | Funit : ftyp + | Ffun : list ftyp -> ftyp + | Fref : area -> ftyp +with area : Type := + | Stored : ftyp -> area +. + +Print ftyp. +(* yields: +Inductive ftyp : Type (* Top.27429 *) := + Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp + with area : Type (* Set *) := Stored : ftyp -> area +*) + +Fixpoint tc_wf_type (ftype: ftyp) {struct ftype}: res unit := + match ftype with + | Funit => OK tt + | Ffun args => + ((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit := + match ftypes with + | nil => OK tt + | t::ts => + match tc_wf_type t with + | OK tt => tc_wf_types ts + | Error m => Error m + end + end) args) + | Fref a => tc_wf_area a + end +with tc_wf_area (ar:area): res unit := + match ar with + | Stored c => tc_wf_type c + end. + +End FOO. + +Print ftyp. +(* yields: +Inductive ftyp : Type (* Top.27465 *) := + Funit : ftyp | Ffun : list ftyp -> ftyp | Fref : area -> ftyp + with area : Set := Stored : ftyp -> area +*) + +Fixpoint tc_wf_type' (ftype: ftyp) {struct ftype}: res unit := + match ftype with + | Funit => OK tt + | Ffun args => + ((fix tc_wf_types (ftypes: list ftyp){struct ftypes}: res unit := + match ftypes with + | nil => OK tt + | t::ts => + match tc_wf_type' t with + | OK tt => tc_wf_types ts + | Error m => Error m + end + end) args) + | Fref a => tc_wf_area' a + end +with tc_wf_area' (ar:area): res unit := + match ar with + | Stored c => tc_wf_type' c + end. + +(* yields: +Error: +Incorrect elimination of "ar" in the inductive type "area": +the return type has sort "Type (* max(Set, Top.27424) *)" while it +should be "Prop" or "Set". +Elimination of an inductive object of sort Set +is not allowed on a predicate in sort Type +because strong elimination on non-small inductive types leads to paradoxes. +*)
\ No newline at end of file diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v new file mode 100644 index 0000000000..2ee438934e --- /dev/null +++ b/test-suite/bugs/closed/2800.v @@ -0,0 +1,6 @@ +Goal False. + +intuition + match goal with + | |- _ => idtac " foo" + end. diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v index ced6d95949..79671ce930 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -56,7 +56,7 @@ Section Finite_nat_set. subst fs1. apply iff_refl. intros H. - eapply counted_list_equal_nth_char. + eapply (counted_list_equal_nth_char _ _ _ _ ?[def]). intros i. destruct (counted_def_nth fs1 i _ ) eqn:H0. (* This was not part of the initial bug report; this is to check that diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v index d41d231739..71d457b002 100644 --- a/test-suite/bugs/closed/3249.v +++ b/test-suite/bugs/closed/3249.v @@ -5,7 +5,7 @@ Ltac ret_and_left T := lazymatch eval hnf in t with | ?a /\ ?b => constr:(proj1 T) | forall x : ?T', @?f x => - constr:(fun x : T' => $(let fx := constr:(T x) in + constr:(fun x : T' => ltac:(let fx := constr:(T x) in let t := ret_and_left fx in - exact t)$) + exact t)) end. diff --git a/test-suite/bugs/closed/3257.v b/test-suite/bugs/closed/3257.v new file mode 100644 index 0000000000..d8aa6a0479 --- /dev/null +++ b/test-suite/bugs/closed/3257.v @@ -0,0 +1,5 @@ +Require Import Setoid Morphisms Basics. +Lemma foo A B (P : B -> Prop) : + pointwise_relation _ impl (fun z => A -> P z) P. +Proof. + Fail reflexivity. diff --git a/test-suite/bugs/closed/3267.v b/test-suite/bugs/closed/3267.v index 5ce1ddf0c4..8175d66ac7 100644 --- a/test-suite/bugs/closed/3267.v +++ b/test-suite/bugs/closed/3267.v @@ -34,3 +34,14 @@ Module d. debug eauto. Defined. End d. + +(* An other variant which was still failing in 8.5 beta2 *) + +Parameter A B : Prop. +Axiom a:B. + +Hint Extern 1 => match goal with H:_ -> id _ |- _ => try (unfold id in H) end. +Goal (B -> id A) -> A. +intros. +eauto using a. +Abort. diff --git a/test-suite/bugs/closed/3285.v b/test-suite/bugs/closed/3285.v index 25162329ef..68e6b7386f 100644 --- a/test-suite/bugs/closed/3285.v +++ b/test-suite/bugs/closed/3285.v @@ -1,7 +1,7 @@ Goal True. Proof. match goal with - | _ => let x := constr:($(fail)$) in idtac + | _ => let x := constr:(ltac:(fail)) in idtac | _ => idtac end. Abort. diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v index b08b7ab3cc..701480fc83 100644 --- a/test-suite/bugs/closed/3286.v +++ b/test-suite/bugs/closed/3286.v @@ -6,20 +6,20 @@ Ltac make_apply_under_binders_in lem H := | forall x : ?T, @?P x => let ret := constr:(fun x' : T => let Hx := H x' in - $(let ret' := tac lem Hx in - exact ret')$) in + ltac:(let ret' := tac lem Hx in + exact ret')) in match eval cbv zeta in ret with | fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in constr:(Some P') end - | _ => let ret := constr:($(match goal with + | _ => let ret := constr:(ltac:(match goal with | _ => (let H' := fresh in pose H as H'; apply lem in H'; exact (Some H')) | _ => exact (@None nat) end - )$) in + )) in let ret' := (eval cbv beta zeta in ret) in constr:(ret') | _ => constr:(@None nat) diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v deleted file mode 100644 index 980431576c..0000000000 --- a/test-suite/bugs/closed/3309.v +++ /dev/null @@ -1,334 +0,0 @@ -Require Import TestSuite.admit. -(* -*- coq-prog-args: ("-emacs" "-impredicative-set") -*- *) -(* File reduced by coq-bug-finder from original input, then from 5968 lines to 11933 lines, then from 11239 lines to 11231 lines, then from 10365 lines to 446 lines, then from 456 lines to 379 lines, then from 391 lines to 373 lines, then from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines *) -Set Universe Polymorphism. -Record sigT' {A} (P : A -> Type) := existT' { projT1' : A; projT2' : P projT1' }. -Notation "{ x : A &' P }" := (sigT' (A := A) (fun x => P)) : type_scope. -Arguments existT' {A} P _ _. -Axiom admit : forall {T}, T. -Notation paths := identity . - -Unset Automatic Introduction. - -Definition UU := Set. - -Definition dirprod ( X Y : UU ) := sigT' ( fun x : X => Y ) . -Definition dirprodpair { X Y : UU } := existT' ( fun x : X => Y ) . - -Definition ddualand { X Y P : UU } (xp : ( X -> P ) -> P ) ( yp : ( Y -> P ) -> P ) : ( dirprod X Y -> P ) -> P. -Proof. - intros X Y P xp yp X0 . - set ( int1 := fun ypp : ( ( Y -> P ) -> P ) => fun x : X => yp ( fun y : Y => X0 ( dirprodpair x y) ) ) . - apply ( xp ( int1 yp ) ) . -Defined . -Definition weq ( X Y : UU ) : UU . -intros; exact ( sigT' (fun f:X->Y => admit) ). -Defined. -Definition pr1weq ( X Y : UU):= @projT1' _ _ : weq X Y -> (X -> Y). -Coercion pr1weq : weq >-> Funclass. - -Definition invweq { X Y : UU } ( w : weq X Y ) : weq Y X . -admit. -Defined. - -Definition hProp := sigT' (fun X : Type => admit). - -Definition hProppair ( X : UU ) ( is : admit ) : hProp@{i j Set k}. -intros; exact (existT' (fun X : UU => admit ) X is ). -Defined. -Definition hProptoType := @projT1' _ _ : hProp -> Type . -Coercion hProptoType: hProp >-> Sortclass. - -Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ). - -Definition ishinh ( X : UU ) : hProp := hProppair ( ishinh_UU X ) admit. - -Definition hinhfun { X Y : UU } ( f : X -> Y ) : ishinh_UU X -> ishinh_UU Y. -intros X Y f; exact ( fun isx : ishinh X => fun P : _ => fun yp : Y -> P => isx P ( fun x : X => yp ( f x ) ) ). -Defined. - -Definition hinhuniv { X : UU } { P : hProp } ( f : X -> P ) ( wit : ishinh_UU X ) : P. -intros; exact ( wit P f ). -Defined. - -Definition hinhand { X Y : UU } ( inx1 : ishinh_UU X ) ( iny1 : ishinh_UU Y) : ishinh ( dirprod X Y ). -intros; exact ( fun P:_ => ddualand (inx1 P) (iny1 P)) . -Defined. - -Definition UU' := Type. -Definition hSet:= sigT' (fun X : UU' => admit) . -Definition hSetpair := existT' (fun X : UU' => admit). -Definition pr1hSet:= @projT1' UU (fun X : UU' => admit) : hSet -> Type. -Coercion pr1hSet: hSet >-> Sortclass. - -Definition hPropset : hSet := existT' _ hProp admit . - -Definition hsubtypes ( X : UU ) : Type. -intros; exact (X -> hProp ). -Defined. -Definition carrier { X : UU } ( A : hsubtypes X ) : Type. -intros; exact (sigT' A). -Defined. -Coercion carrier : hsubtypes >-> Sortclass. - -Definition subtypesdirprod { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) : hsubtypes ( dirprod X Y ). -admit. -Defined. - -Lemma weqsubtypesdirprod { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) : weq ( subtypesdirprod A B ) ( dirprod A B ) . - admit. -Defined. - -Lemma ishinhsubtypesdirprod { X Y : UU } ( A : hsubtypes X ) ( B : hsubtypes Y ) ( isa : ishinh A ) ( isb : ishinh B ) : ishinh ( subtypesdirprod A B ) . -Proof . - intros . - apply ( hinhfun ( invweq ( weqsubtypesdirprod A B ) ) ) . - apply hinhand . - apply isa . - apply isb . -Defined . - -Definition hrel ( X : UU ) : Type. -intros; exact ( X -> X -> hProp). -Defined. - -Definition iseqrel { X : UU } ( R : hrel X ) : Type. -admit. -Defined. - -Definition eqrel ( X : UU ) : Type. -intros; exact ( sigT' ( fun R : hrel X => iseqrel R ) ). -Defined. -Definition pr1eqrel ( X : UU ) : eqrel X -> ( X -> ( X -> hProp ) ) := @projT1' _ _ . -Coercion pr1eqrel : eqrel >-> Funclass . - -Definition hreldirprod { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) : hrel ( dirprod X Y ) . -admit. -Defined. -Set Printing Universes. -Print hProp. -Print ishinh_UU. -Print hProppair. -Definition iseqclass { X : UU } ( R : hrel X ) ( A : hsubtypes X ) : Type. -intros; exact ( dirprod ( ishinh ( carrier A ) ) ( dirprod ( forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( forall x1 x2 : X, A x1 -> A x2 -> R x1 x2 ) )) . -Defined. -Definition iseqclassconstr { X : UU } ( R : hrel X ) { A : hsubtypes X } ( ax0 : ishinh ( carrier A ) ) ( ax1 : forall x1 x2 : X , R x1 x2 -> A x1 -> A x2 ) ( ax2 : forall x1 x2 : X, A x1 -> A x2 -> R x1 x2 ) : iseqclass R A. -intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact ax2. -Defined. - -Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X } : iseqclass R A -> ishinh ( carrier A ) . -intros X R A; exact ( fun is : iseqclass R A => projT1' _ is ). -Defined. - -Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) . -Proof . - intros . - set ( XY := dirprod X Y ) . - set ( AB := subtypesdirprod A B ) . - set ( RQ := hreldirprod R Q ) . - set ( ax0 := ishinhsubtypesdirprod A B ( eqax0 isa ) admit ) . - apply ( iseqclassconstr _ ax0 admit admit ) . -Defined . - -Definition image { X Y : UU } ( f : X -> Y ) : Type. -intros; exact ( sigT' ( fun y : Y => admit ) ). -Defined. -Definition pr1image { X Y : UU } ( f : X -> Y ) : image f -> Y. -intros X Y f; exact ( @projT1' _ ( fun y : Y => admit ) ). -Defined. - -Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f. - admit. -Defined. - -Definition setquot { X : UU } ( R : hrel X ) : Type. -intros; exact ( sigT' ( fun A : _ => iseqclass R A ) ). -Defined. -Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R. -intros; exact (existT' _ A is ). -Defined. -Definition pr1setquot { X : UU } ( R : hrel X ) : setquot R -> ( hsubtypes X ). -intros X R. -exact ( @projT1' _ ( fun A : _ => iseqclass R A ) ). -Defined. -Coercion pr1setquot : setquot >-> hsubtypes . - -Definition setquotinset { X : UU } ( R : hrel X ) : hSet. -intros; exact ( hSetpair (setquot R) admit) . -Defined. - -Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ). -intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2' _ ( projT1' _ cd ) ) ( projT2' _ ( projT2' _ cd ) ) ) ). -Defined. - -Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y ) := forall x x' x0 x0' : X , R x x' -> R x0 x0' -> paths ( f x x0 ) ( f x' x0' ) . - -Definition binop ( X : UU ) : Type. -intros; exact ( X -> X -> X ). -Defined. - -Definition setwithbinop : Type. -exact (sigT' ( fun X : hSet => binop X ) ). -Defined. -Definition pr1setwithbinop : setwithbinop -> hSet@{j k Set l}. -unfold setwithbinop. -exact ( @projT1' _ ( fun X : hSet@{j k Set l} => binop@{Set} X ) ). -Defined. -Coercion pr1setwithbinop : setwithbinop >-> hSet . - -Definition op { X : setwithbinop } : binop X. -intros; exact ( projT2' _ X ). -Defined. - -Definition subsetswithbinop { X : setwithbinop } : Type. -admit. -Defined. - -Definition carrierofasubsetwithbinop { X : setwithbinop } ( A : @subsetswithbinop X ) : setwithbinop . -admit. -Defined. - -Coercion carrierofasubsetwithbinop : subsetswithbinop >-> setwithbinop . - -Definition binopeqrel { X : setwithbinop } : Type. -intros; exact (sigT' ( fun R : eqrel X => admit ) ). -Defined. -Definition binopeqrelpair { X : setwithbinop } := existT' ( fun R : eqrel X => admit ). -Definition pr1binopeqrel ( X : setwithbinop ) : @binopeqrel X -> eqrel X. -intros X; exact ( @projT1' _ ( fun R : eqrel X => admit ) ) . -Defined. -Coercion pr1binopeqrel : binopeqrel >-> eqrel . - -Definition setwithbinopdirprod ( X Y : setwithbinop ) : setwithbinop . -admit. -Defined. - -Definition monoid : Type. -exact ( sigT' ( fun X : setwithbinop => admit ) ). -Defined. -Definition monoidpair := existT' ( fun X : setwithbinop => admit ) . -Definition pr1monoid : monoid -> setwithbinop := @projT1' _ _ . -Coercion pr1monoid : monoid >-> setwithbinop . - -Notation "x + y" := ( op x y ) : addmonoid_scope . - -Definition submonoids { X : monoid } : Type. -admit. -Defined. - -Definition submonoidstosubsetswithbinop ( X : monoid ) : @submonoids X -> @subsetswithbinop X. -admit. -Defined. -Coercion submonoidstosubsetswithbinop : submonoids >-> subsetswithbinop . - -Definition abmonoid : Type. -exact (sigT' ( fun X : setwithbinop => admit ) ). -Defined. - -Definition abmonoidtomonoid : abmonoid -> monoid. -exact (fun X : _ => monoidpair ( projT1' _ X ) admit ). -Defined. -Coercion abmonoidtomonoid : abmonoid >-> monoid . - -Definition subabmonoids { X : abmonoid } := @submonoids X . - -Definition carrierofsubabmonoid { X : abmonoid } ( A : @subabmonoids X ) : abmonoid . -Proof . - intros . - unfold subabmonoids in A . - split with A . - admit. -Defined . - -Coercion carrierofsubabmonoid : subabmonoids >-> abmonoid . - -Definition abmonoiddirprod ( X Y : abmonoid ) : abmonoid . -Proof . - intros . - split with ( setwithbinopdirprod X Y ) . - admit. -Defined . - -Open Scope addmonoid_scope . - -Definition eqrelabmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : eqrel ( setwithbinopdirprod X A ). -admit. -Defined. - -Definition binopeqrelabmonoidfrac ( X : abmonoid ) ( A : @subabmonoids X ) : @binopeqrel ( abmonoiddirprod X A ). -intros; exact ( @binopeqrelpair ( setwithbinopdirprod X A ) ( eqrelabmonoidfrac X A ) admit ). -Defined. - -Theorem setquotuniv { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ) : Y . -Proof. - intros. - apply ( pr1image ( fun x : c => f ( projT1' _ x ) ) ) . - apply ( @hinhuniv ( projT1' _ c ) ( hProppair _ admit ) ( prtoimage ( fun x : c => f ( projT1' _ x ) ) ) ) . - pose ( eqax0 ( projT2' _ c ) ) as h. - simpl in *. - Set Printing Universes. - exact h. -Defined . - -Definition setquotuniv2 { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> X -> Y ) ( is : iscomprelfun2 R f ) ( c c0 : setquot R ) : Y . -Proof. - intros . - set ( RR := hreldirprod R R ) . - apply (setquotuniv RR Y admit). - apply dirprodtosetquot. - apply dirprodpair. - exact c. - exact c0. -Defined . - -Definition setquotfun2 { X Y : UU } ( RX : hrel X ) ( RY : eqrel Y ) ( f : X -> X -> Y ) ( cx cx0 : setquot RX ) : setquot RY . -Proof . - intros . - apply ( setquotuniv2 RX ( setquotinset RY ) admit admit admit admit ) . -Defined . - -Definition quotrel { X : UU } { R : hrel X } : hrel ( setquot R ). -intros; exact ( setquotuniv2 R hPropset admit admit ). -Defined. - -Definition setwithbinopquot { X : setwithbinop } ( R : @binopeqrel X ) : setwithbinop . -Proof . - intros . - split with ( setquotinset R ) . - set ( qtmlt := setquotfun2 R R op ) . - simpl . - unfold binop . - apply qtmlt . -Defined . - -Definition abmonoidquot { X : abmonoid } ( R : @binopeqrel X ) : abmonoid . -Proof . - intros . - split with ( setwithbinopquot R ) . - admit. -Defined . - -Definition abmonoidfrac ( X : abmonoid ) ( A : @submonoids X ) : abmonoid. -intros; exact ( @abmonoidquot (abmonoiddirprod X (@carrierofsubabmonoid X A)) ( binopeqrelabmonoidfrac X A ) ). -Defined. - -Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) : hrel (@setquot (setwithbinopdirprod X A) (eqrelabmonoidfrac X A)). -intros; exact (@quotrel _ _). -Defined. - -Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit. - -Definition ispartlbinopabmonoidfracrel_type : Type := - forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ), - @abmonoidfracrel X A ( ( admit + z ) )admit. - -Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in - ispartlbinopabmonoidfracrel_type in exact t)$. - -Unset Kernel Term Sharing. - -Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit. - -Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in - ispartlbinopabmonoidfracrel_type in exact t)$. - diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v index e63c46da04..a5782298c3 100644 --- a/test-suite/bugs/closed/3314.v +++ b/test-suite/bugs/closed/3314.v @@ -1,9 +1,9 @@ Require Import TestSuite.admit. Set Universe Polymorphism. Definition Lift -: $(let U1 := constr:(Type) in +: ltac:(let U1 := constr:(Type) in let U0 := constr:(Type : U1) in - exact (U0 -> U1))$ + exact (U0 -> U1)) := fun T => T. Fail Check nat:Prop. (* The command has indeed failed with message: @@ -122,12 +122,12 @@ Definition depsort (T : Type) (x : bool) : informative x := end. (** This definition should fail *) -Definition Box (T : Type1) : Prop := Lift T. +Fail Definition Box (T : Type1) : Prop := Lift T. -Definition prop {T : Type1} (t : Box T) : T := t. -Definition wrap {T : Type1} (t : T) : Box T := t. +Fail Definition prop {T : Type1} (t : Box T) : T := t. +Fail Definition wrap {T : Type1} (t : T) : Box T := t. -Definition down (x : Type1) : Prop := Box x. +Fail Definition down (x : Type1) : Prop := Box x. Definition up (x : Prop) : Type1 := x. Fail Definition back A : up (down A) -> A := @prop A. diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index 4cd7c39e88..e3b5e94356 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *) Set Universe Polymorphism. @@ -7,7 +8,7 @@ Inductive foo : Type@{l} := bar : foo . Section MakeEq. Variables (a : foo@{i}) (b : foo@{j}). - Let t := $(let ty := type of b in exact ty)$. + Let t := ltac:(let ty := type of b in exact ty). Definition make_eq (x:=b) := a : t. End MakeEq. diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v index 63d5c7a57b..dcf5394eaf 100644 --- a/test-suite/bugs/closed/3347.v +++ b/test-suite/bugs/closed/3347.v @@ -1,7 +1,7 @@ Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *) Set Universe Polymorphism. -Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). +Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing). Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. Inductive Unit : Type1 := tt : Unit. Fail Check Unit : Set. (* [Check Unit : Set] should fail if [Type1] is defined correctly *) diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index b57b0a0f0b..f8113e4c78 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *) Foo] to mean [IsHProp (* U >= Set *) Foo]. (I think this worked in HoTT/coq, too.) Morally, [IsHProp] has no universe level associated with it distinct from that of its argument, you should never get a universe inconsistency from unifying [IsHProp A] with [IsHProp A]. (The issue is tricker when IsHProp uses [A] elsewhere, as in: diff --git a/test-suite/bugs/closed/3354.v b/test-suite/bugs/closed/3354.v index 14b66db362..a635285f2c 100644 --- a/test-suite/bugs/closed/3354.v +++ b/test-suite/bugs/closed/3354.v @@ -1,5 +1,5 @@ Set Universe Polymorphism. -Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). +Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing). Inductive Empty : Type1 := . Fail Check Empty : Set. (* Toplevel input, characters 15-116: diff --git a/test-suite/bugs/closed/3386.v b/test-suite/bugs/closed/3386.v index 0e236c2172..b8bb8bce09 100644 --- a/test-suite/bugs/closed/3386.v +++ b/test-suite/bugs/closed/3386.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Universe Polymorphism. Set Printing Universes. Record Cat := { Obj :> Type }. diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v index ae212caa5d..cb435e7865 100644 --- a/test-suite/bugs/closed/3387.v +++ b/test-suite/bugs/closed/3387.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Universe Polymorphism. Set Printing Universes. Record Cat := { Obj :> Type }. diff --git a/test-suite/bugs/closed/3467.v b/test-suite/bugs/closed/3467.v index 7e37116249..88ae030578 100644 --- a/test-suite/bugs/closed/3467.v +++ b/test-suite/bugs/closed/3467.v @@ -1,5 +1,5 @@ Module foo. - Notation x := $(exact I)$. + Notation x := ltac:(exact I). End foo. Module bar. Include foo. diff --git a/test-suite/bugs/closed/3487.v b/test-suite/bugs/closed/3487.v index 03c60a8baa..1321a8598c 100644 --- a/test-suite/bugs/closed/3487.v +++ b/test-suite/bugs/closed/3487.v @@ -1,4 +1,4 @@ -Notation bar := $(exact I)$. +Notation bar := ltac:(exact I). Notation foo := bar (only parsing). Class baz := { x : False }. Instance: baz. diff --git a/test-suite/bugs/closed/3554.v b/test-suite/bugs/closed/3554.v new file mode 100644 index 0000000000..13a79cc840 --- /dev/null +++ b/test-suite/bugs/closed/3554.v @@ -0,0 +1 @@ +Example foo (f : forall {_ : Type}, Type) : Type. diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v index 50645090fa..da12b68689 100644 --- a/test-suite/bugs/closed/3559.v +++ b/test-suite/bugs/closed/3559.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* File reduced by coq-bug-finder from original input, then from 8657 lines to 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines, then from 51 lines to 37 lines, then from 43 lines to 30 lines *) diff --git a/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v index b2aa8c3cd6..e2d7976981 100644 --- a/test-suite/bugs/closed/3566.v +++ b/test-suite/bugs/closed/3566.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Notation idmap := (fun x => x). Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. Arguments idpath {A a} , [A] a. diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 324c12525c..a547685070 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -37,6 +37,9 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (r : p..1 = q..1) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. + +Declare ML Module "coretactics". + Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x)) (xx : @paths (@sigT A (fun x0 : A => B x0)) x x), @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v index a5b0e9347d..e69ec10976 100644 --- a/test-suite/bugs/closed/3666.v +++ b/test-suite/bugs/closed/3666.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *) (* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *) diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v index 2a282d221f..9d37d1a2d0 100644 --- a/test-suite/bugs/closed/3682.v +++ b/test-suite/bugs/closed/3682.v @@ -3,4 +3,4 @@ Class Foo. Definition bar `{Foo} (x : Set) := Set. Instance: Foo. Definition bar1 := bar nat. -Definition bar2 := bar $(admit)$. +Definition bar2 := bar ltac:(admit). diff --git a/test-suite/bugs/closed/3684.v b/test-suite/bugs/closed/3684.v index f7b137386b..130d57779d 100644 --- a/test-suite/bugs/closed/3684.v +++ b/test-suite/bugs/closed/3684.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. Definition foo : Set. Proof. - refine ($(abstract admit)$). + refine (ltac:(abstract admit)). Qed. diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v new file mode 100644 index 0000000000..7a0c3e6f1d --- /dev/null +++ b/test-suite/bugs/closed/3685.v @@ -0,0 +1,75 @@ +Require Import TestSuite.admit. +Set Universe Polymorphism. +Class Funext := { }. +Delimit Scope category_scope with category. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Set Implicit Arguments. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d); + identity_of : forall s m, morphism_of s s m = morphism_of s s m }. +Definition sub_pre_cat `{Funext} (P : PreCategory -> Type) : PreCategory. +Proof. + exact (@Build_PreCategory PreCategory Functor). +Defined. +Definition opposite (C : PreCategory) : PreCategory. +Proof. + exact (@Build_PreCategory C (fun s d => morphism C d s)). +Defined. +Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope. +Definition prod (C D : PreCategory) : PreCategory. +Proof. + refine (@Build_PreCategory + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)). +Defined. +Local Infix "*" := prod : category_scope. +Record NaturalTransformation C D (F G : Functor C D) := {}. +Definition functor_category (C D : PreCategory) : PreCategory. +Proof. + exact (@Build_PreCategory (Functor C D) (@NaturalTransformation C D)). +Defined. +Local Notation "C -> D" := (functor_category C D) : category_scope. +Module Export PointwiseCore. + Local Open Scope category_scope. + Definition pointwise + (C C' : PreCategory) + (F : Functor C' C) + (D D' : PreCategory) + (G : Functor D D') + : Functor (C -> D) (C' -> D'). + Proof. + unshelve (refine (Build_Functor + (C -> D) (C' -> D') + _ + _ + _)); + abstract admit. + Defined. +End PointwiseCore. +Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G. +Local Open Scope category_scope. +Module Success. + Definition functor_uncurried `{Funext} (P : PreCategory -> Type) + (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D)) + : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P)) + := Eval cbv zeta in + let object_of := (fun CD => (((fst CD) -> (snd CD)))) + in Build_Functor + ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P) + object_of + (fun CD C'D' FG => pointwise (fst FG) (snd FG)) + (fun _ _ => @Pidentity_of _ _ _ _). +End Success. +Module Bad. + Include PointwiseCore. + Definition functor_uncurried `{Funext} (P : PreCategory -> Type) + (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D)) + : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P)) + := Eval cbv zeta in + let object_of := (fun CD => (((fst CD) -> (snd CD)))) + in Build_Functor + ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P) + object_of + (fun CD C'D' FG => pointwise (fst FG) (snd FG)) + (fun _ _ => @Pidentity_of _ _ _ _). diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v index b650920b26..df5f667480 100644 --- a/test-suite/bugs/closed/3686.v +++ b/test-suite/bugs/closed/3686.v @@ -33,11 +33,11 @@ Module Export PointwiseCore. (G : Functor D D') : Functor (C -> D) (C' -> D'). Proof. - refine (Build_Functor + unshelve (refine (Build_Functor (C -> D) (C' -> D') _ _ - _); + _)); abstract admit. Defined. End PointwiseCore. diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index 4069e38075..c24173abf1 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Printing Universes. Set Universe Polymorphism. Definition foo (a := Type) (b := Type) (c := Type) := Type. @@ -17,7 +18,7 @@ Top.8} Top.6 Top.7 Top.8 |= *) *) -Definition bar := $(let t := eval compute in foo in exact t)$. +Definition bar := ltac:(let t := eval compute in foo in exact t). Check @bar. (* bar@{Top.13 Top.14 Top.15 Top.16} : Type@{Top.16+1} diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 62137f0c06..8dadc2419c 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,8 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +47,8 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intros [a p]. exact (transport P p (d a)). Defined. @@ -65,7 +65,7 @@ Module NonPrim. set (fibermap := fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0)). Set Printing Implicit. - let G := match goal with |- ?G => constr:G end in + let G := match goal with |- ?G => constr:(G) end in first [ match goal with | [ |- (@isconnected_elim n (@hfiber A B f (f a)) (@isconnected_hfiber_conn_map n A B f H (f a)) @@ -111,8 +111,8 @@ Module Prim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +124,8 @@ Module Prim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intros [a p]. exact (transport P p (d a)). Defined. @@ -142,7 +142,7 @@ Module Prim. set (fibermap := fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0)). Set Printing Implicit. - let G := match goal with |- ?G => constr:G end in + let G := match goal with |- ?G => constr:(G) end in first [ match goal with | [ |- (@isconnected_elim n (@hfiber A B f (f a)) (@isconnected_hfiber_conn_map n A B f H (f a)) diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v new file mode 100644 index 0000000000..a50572ace0 --- /dev/null +++ b/test-suite/bugs/closed/3735.v @@ -0,0 +1,4 @@ +Require Import Coq.Program.Tactics. +Class Foo := { bar : Type }. +Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *) +Fail Program Lemma foo : Foo -> bar.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v index 4dfb3380a8..c799d4393f 100644 --- a/test-suite/bugs/closed/3743.v +++ b/test-suite/bugs/closed/3743.v @@ -3,7 +3,7 @@ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *) Require Export Coq.Setoids.Setoid. -Fail Add Parametric Relation A +Add Parametric Relation A : A (@eq A) transitivity proved by transitivity as refine_rel. diff --git a/test-suite/bugs/closed/3746.v b/test-suite/bugs/closed/3746.v new file mode 100644 index 0000000000..a9463f94bb --- /dev/null +++ b/test-suite/bugs/closed/3746.v @@ -0,0 +1,92 @@ + +(* Bug report #3746 : Include and restricted signature *) + +Module Type MT. Parameter p : nat. End MT. +Module Type EMPTY. End EMPTY. +Module Empty. End Empty. + +(* Include of an applied functor with restricted sig : + Used to create axioms (bug report #3746), now forbidden. *) + +Module F (X:EMPTY) : MT. + Definition p := 0. +End F. + +Module InclFunctRestr. + Fail Include F(Empty). +End InclFunctRestr. + +(* A few variants (indirect restricted signature), also forbidden. *) + +Module F1 := F. +Module F2 (X:EMPTY) := F X. + +Module F3a (X:EMPTY). Definition p := 0. End F3a. +Module F3 (X:EMPTY) : MT := F3a X. + +Module InclFunctRestrBis. + Fail Include F1(Empty). + Fail Include F2(Empty). + Fail Include F3(Empty). +End InclFunctRestrBis. + +(* Recommended workaround: manual instance before the include. *) + +Module InclWorkaround. + Module Temp := F(Empty). + Include Temp. +End InclWorkaround. + +Compute InclWorkaround.p. +Print InclWorkaround.p. +Print Assumptions InclWorkaround.p. (* Closed under the global context *) + + + +(* Related situations which are ok, just to check *) + +(* A) Include of non-functor with restricted signature : + creates a proxy to initial stuff *) + +Module M : MT. + Definition p := 0. +End M. + +Module InclNonFunct. + Include M. +End InclNonFunct. + +Definition check : InclNonFunct.p = M.p := eq_refl. +Print Assumptions InclNonFunct.p. (* Closed *) + + +(* B) Include of a module type with opaque content: + The opaque content is "copy-pasted". *) + +Module Type SigOpaque. + Definition p : nat. Proof. exact 0. Qed. +End SigOpaque. + +Module InclSigOpaque. + Include SigOpaque. +End InclSigOpaque. + +Compute InclSigOpaque.p. +Print InclSigOpaque.p. +Print Assumptions InclSigOpaque.p. (* Closed *) + + +(* C) Include of an applied functor with opaque proofs : + opaque proof "copy-pasted" (and substituted). *) + +Module F' (X:EMPTY). + Definition p : nat. Proof. exact 0. Qed. +End F'. + +Module InclFunctOpa. + Include F'(Empty). +End InclFunctOpa. + +Compute InclFunctOpa.p. +Print InclFunctOpa.p. +Print Assumptions InclFunctOpa.p. (* Closed *) diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v new file mode 100644 index 0000000000..e203528fcc --- /dev/null +++ b/test-suite/bugs/closed/3777.v @@ -0,0 +1,17 @@ +Unset Strict Universe Declaration. +Module WithoutPoly. + Unset Universe Polymorphism. + Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B. + Set Printing Universes. + Definition bla := ((@foo : Set -> _ -> _) : _ -> Type -> _). + (* ((fun A : Set => foo A):Set -> Type@{Top.55} -> Type@{Top.55}) +:Set -> Type@{Top.55} -> Type@{Top.55} + : Set -> Type@{Top.55} -> Type@{Top.55} +(* |= Set <= Top.55 + *) *) +End WithoutPoly. +Module WithPoly. + Set Universe Polymorphism. + Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B. + Set Printing Universes. + Fail Check ((@foo : Set -> _ -> _) : _ -> Type -> _). diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v index eb0d206c5c..2b44e225e8 100644 --- a/test-suite/bugs/closed/3779.v +++ b/test-suite/bugs/closed/3779.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Set Universe Polymorphism. Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }. Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T. diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v new file mode 100644 index 0000000000..108ebf592b --- /dev/null +++ b/test-suite/bugs/closed/3807.v @@ -0,0 +1,33 @@ +Set Universe Polymorphism. +Set Printing Universes. +Unset Universe Minimization ToSet. + + +Definition foo : Type := nat. +About foo. +(* foo@{Top.1} : Type@{Top.1}*) +(* Top.1 |= *) + +Definition bar : foo -> nat. +Admitted. +About bar. +(* bar@{Top.2} : foo@{Top.2} -> nat *) +(* Top.2 |= *) + +Lemma baz@{i} : foo@{i} -> nat. +Proof. + exact bar. +Defined. + +Definition bar'@{i} : foo@{i} -> nat. + intros f. exact 0. +Admitted. +About bar'. +(* bar'@{i} : foo@{i} -> nat *) +(* i |= *) + +Axiom f@{i} : Type@{i}. +(* +*** [ f@{i} : Type@{i} ] +(* i |= *) +*)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v index 6e19ddf8dc..a5c84e6856 100644 --- a/test-suite/bugs/closed/3808.v +++ b/test-suite/bugs/closed/3808.v @@ -1,2 +1,3 @@ +Unset Strict Universe Declaration. Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i}) := foo : Foo.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v index 8da4f73626..30261ed266 100644 --- a/test-suite/bugs/closed/3821.v +++ b/test-suite/bugs/closed/3821.v @@ -1,2 +1,3 @@ +Unset Strict Universe Declaration. Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := . diff --git a/test-suite/bugs/closed/3848.v b/test-suite/bugs/closed/3848.v new file mode 100644 index 0000000000..c0ef02f1e8 --- /dev/null +++ b/test-suite/bugs/closed/3848.v @@ -0,0 +1,22 @@ +Require Import TestSuite.admit. +Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing). +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x. +Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }. +Arguments eisretr {A B} f {_} _. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'"). +Generalizable Variables A B f g e n. +Definition functor_forall `{P : A -> Type} `{Q : B -> Type} + (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b) +: (forall a:A, P a) -> (forall b:B, Q b). + admit. +Defined. + +Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type} + `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)} +: (forall b : B, Q b) -> forall a : A, P a. +Proof. + refine (functor_forall + (f^-1) + (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)). +Defined. (* was: Error: Attempt to save an incomplete proof *) diff --git a/test-suite/bugs/closed/3849.v b/test-suite/bugs/closed/3849.v new file mode 100644 index 0000000000..a8dc3af9cf --- /dev/null +++ b/test-suite/bugs/closed/3849.v @@ -0,0 +1,8 @@ +Tactic Notation "foo" hyp_list(hs) := clear hs. + +Tactic Notation "bar" hyp_list(hs) := foo hs. + +Goal True. +do 5 pose proof 0 as ?n0. +foo n1 n2. +bar n3 n4. diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index 4408ab885d..a327bbf2a9 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -8,7 +8,7 @@ Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Notation "A -> B" := (forall (_ : A), B) : type_scope. Axiom admit : forall {T}, T. Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity). -Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *) +Notation "g 'o' f" := ltac:(let g' := g in let f' := f in exact (fun x => g' (f' x))) (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *) Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope. Arguments eq_refl {_ _}. Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end. @@ -23,7 +23,7 @@ Proof. pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H (fun b => ap g (eisretr f b))) as k. revert k. - let x := match goal with |- let k := ?x in _ => constr:x end in + let x := match goal with |- let k := ?x in _ => constr:(x) end in intro k; clear k; pose (x _). pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _ diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 0ccc92067d..5013bc6ac1 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. Set Universe Polymorphism. Notation Type0 := Set. diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v new file mode 100644 index 0000000000..0aa029e73d --- /dev/null +++ b/test-suite/bugs/closed/3923.v @@ -0,0 +1,33 @@ +Module Type TRIVIAL. +Parameter t:Type. +End TRIVIAL. + +Module MkStore (Key : TRIVIAL). + +Module St : TRIVIAL. +Definition t := unit. +End St. + +End MkStore. + + + +Module Type CERTRUNTIMETYPES (B : TRIVIAL). + +Parameter cert_fieldstore : Type. +Parameter empty_fieldstore : cert_fieldstore. + +End CERTRUNTIMETYPES. + + + +Module MkCertRuntimeTypes (B : TRIVIAL) : CERTRUNTIMETYPES B. + +Module FieldStore := MkStore B. + +Definition cert_fieldstore := FieldStore.St.t. +Axiom empty_fieldstore : cert_fieldstore. + +End MkCertRuntimeTypes. + +Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *) diff --git a/test-suite/bugs/closed/3948.v b/test-suite/bugs/closed/3948.v new file mode 100644 index 0000000000..56b1e3ffb4 --- /dev/null +++ b/test-suite/bugs/closed/3948.v @@ -0,0 +1,24 @@ +Module Type S. +Parameter t : Type. +End S. + +Module Bar(X : S). +Definition elt := X.t. +Axiom fold : elt. +End Bar. + +Module Make (Z: S) := Bar(Z). + +Declare Module Y : S. + +Module Type Interface. +Parameter constant : unit. +End Interface. + +Module DepMap : Interface. +Module Dom := Make(Y). +Definition constant : unit := + let _ := @Dom.fold in tt. +End DepMap. + +Print Assumptions DepMap.constant. diff --git a/test-suite/bugs/closed/3956.v b/test-suite/bugs/closed/3956.v new file mode 100644 index 0000000000..c19a2d4a06 --- /dev/null +++ b/test-suite/bugs/closed/3956.v @@ -0,0 +1,143 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter"); mode: visual-line -*- *) +Set Universe Polymorphism. +Set Primitive Projections. +Close Scope nat_scope. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Arguments pair {A B} _ _. +Arguments fst {A B} _ / . +Arguments snd {A B} _ / . +Notation "x * y" := (prod x y) : type_scope. +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. + +Unset Strict Universe Declaration. + +Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. +Definition Type2 := Eval hnf in let gt := (Type1 : Type@{i}) in Type@{i}. + +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 concat {A} {x y z : A} (p : x = y) (q : y = z) : x = z + := match p, q with idpath, idpath => idpath end. + +Definition path_prod {A B : Type} (z z' : A * B) +: (fst z = fst z') -> (snd z = snd z') -> (z = z'). +Proof. + destruct z, z'; simpl; intros [] []; reflexivity. +Defined. + +Module Type TypeM. + Parameter m : Type2. +End TypeM. + +Module ProdM (XM : TypeM) (YM : TypeM) <: TypeM. + Definition m := XM.m * YM.m. +End ProdM. + +Module Type FunctionM (XM YM : TypeM). + Parameter m : XM.m -> YM.m. +End FunctionM. + +Module IdmapM (XM : TypeM) <: FunctionM XM XM. + Definition m := (fun x => x) : XM.m -> XM.m. +End IdmapM. + +Module Type HomotopyM (XM YM : TypeM) (fM gM : FunctionM XM YM). + Parameter m : forall x, fM.m x = gM.m x. +End HomotopyM. + +Module ComposeM (XM YM ZM : TypeM) + (gM : FunctionM YM ZM) (fM : FunctionM XM YM) + <: FunctionM XM ZM. + Definition m := (fun x => gM.m (fM.m x)). +End ComposeM. + +Module Type CorecM (YM ZM : TypeM) (fM : FunctionM YM ZM) + (XM : TypeM) (gM : FunctionM XM ZM). + Parameter m : XM.m -> YM.m. + Parameter m_beta : forall x, fM.m (m x) = gM.m x. +End CorecM. + +Module Type CoindpathsM (YM ZM : TypeM) (fM : FunctionM YM ZM) + (XM : TypeM) (hM kM : FunctionM XM YM). + Module fhM := ComposeM XM YM ZM fM hM. + Module fkM := ComposeM XM YM ZM fM kM. + Declare Module mM (pM : HomotopyM XM ZM fhM fkM) + : HomotopyM XM YM hM kM. +End CoindpathsM. + +Module Type Comodality (XM : TypeM). + Parameter m : Type2. + Module mM <: TypeM. + Definition m := m. + End mM. + Parameter from : m -> XM.m. + Module fromM <: FunctionM mM XM. + Definition m := from. + End fromM. + Declare Module corecM : CorecM mM XM fromM. + Declare Module coindpathsM : CoindpathsM mM XM fromM. +End Comodality. + +Module Comodality_Theory (F : Comodality). + + Module F_functor_M (XM YM : TypeM) (fM : FunctionM XM YM) + (FXM : Comodality XM) (FYM : Comodality YM). + Module f_o_from_M <: FunctionM FXM.mM YM. + Definition m := fun x => fM.m (FXM.from x). + End f_o_from_M. + Module mM := FYM.corecM FXM.mM f_o_from_M. + Definition m := mM.m. + End F_functor_M. + + Module F_prod_cmp_M (XM YM : TypeM) + (FXM : Comodality XM) (FYM : Comodality YM). + Module PM := ProdM XM YM. + Module PFM := ProdM FXM FYM. + Module fstM <: FunctionM PM XM. + Definition m := @fst XM.m YM.m. + End fstM. + Module sndM <: FunctionM PM YM. + Definition m := @snd XM.m YM.m. + End sndM. + Module FPM := F PM. + Module FfstM := F_functor_M PM XM fstM FPM FXM. + Module FsndM := F_functor_M PM YM sndM FPM FYM. + Definition m : FPM.m -> PFM.m + := fun z => (FfstM.m z , FsndM.m z). + End F_prod_cmp_M. + + Module isequiv_F_prod_cmp_M + (XM YM : TypeM) + (FXM : Comodality XM) (FYM : Comodality YM). + (** The comparison map *) + Module cmpM := F_prod_cmp_M XM YM FXM FYM. + Module FPM := cmpM.FPM. + (** We construct an inverse to it using corecursion. *) + Module prod_from_M <: FunctionM cmpM.PFM cmpM.PM. + Definition m : cmpM.PFM.m -> cmpM.PM.m + := fun z => ( FXM.from (fst z) , FYM.from (snd z) ). + End prod_from_M. + Module cmpinvM <: FunctionM cmpM.PFM FPM + := FPM.corecM cmpM.PFM prod_from_M. + (** We prove the first homotopy *) + Module cmpinv_o_cmp_M <: FunctionM FPM FPM + := ComposeM FPM cmpM.PFM FPM cmpinvM cmpM. + Module idmap_FPM <: FunctionM FPM FPM + := IdmapM FPM. + Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM. + Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM. + Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x. + Proof. + intros x. + refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _). + apply path_prod@{i i i}; simpl. + - exact (cmpM.FfstM.mM.m_beta@{i j} x). + - exact (cmpM.FsndM.mM.m_beta@{i j} x). + Defined. + End cip_FPHM. + End isequiv_F_prod_cmp_M. + +End Comodality_Theory.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3974.v b/test-suite/bugs/closed/3974.v new file mode 100644 index 0000000000..b6be159595 --- /dev/null +++ b/test-suite/bugs/closed/3974.v @@ -0,0 +1,7 @@ +Module Type S. +End S. + +Module Type M (X : S). + Fail Module P (X : S). + (* Used to say: Anomaly: X already exists. Please report. *) + (* Should rather say now: Error: X already exists. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3975.v b/test-suite/bugs/closed/3975.v new file mode 100644 index 0000000000..95851c8137 --- /dev/null +++ b/test-suite/bugs/closed/3975.v @@ -0,0 +1,8 @@ +Module Type S. End S. + +Module M (X:S). End M. + +Module Type P (X : S). + Print M. + (* Used to say: Anomaly: X already exists. Please report. *) + (* Should rather : print something :-) *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v new file mode 100644 index 0000000000..ced13839dd --- /dev/null +++ b/test-suite/bugs/closed/3998.v @@ -0,0 +1,24 @@ +Class FieldType (F : Set) := mkFieldType { fldTy: F -> Set }. +Hint Mode FieldType + : typeclass_instances. (* The F parameter is an input *) + +Inductive I1 := C. +Inductive I2 := . + +Instance I1FieldType : FieldType I1 := { fldTy := I1_rect _ bool }. +Instance I2FieldType : FieldType I2 := { fldTy := I2_rect _ }. + +Definition RecordOf F (FT: FieldType F) := forall f:F, fldTy f. + +Class MapOps (M K : Set) := { + tgtTy: K -> Set; + update: M -> forall k:K, tgtTy k -> M +}. + +Instance RecordMapOps F (FT: FieldType F) : MapOps (RecordOf F FT) F := +{ tgtTy := fldTy; update := fun r (f: F) (x: fldTy f) z => r z }. + +Axiom ex : RecordOf _ I1FieldType. + +Definition works := (fun ex' => update ex' C true) (update ex C false). +Set Typeclasses Debug. +Definition doesnt := update (update ex C false) C true.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4034.v b/test-suite/bugs/closed/4034.v new file mode 100644 index 0000000000..3f7be4d1c7 --- /dev/null +++ b/test-suite/bugs/closed/4034.v @@ -0,0 +1,25 @@ +(* This checks compatibility of interpretation scope used for exact + between 8.4 and 8.5. See discussion at + https://coq.inria.fr/bugs/show_bug.cgi?id=4034. It is not clear + what we would like exactly, but certainly, if exact is interpreted + in a special scope, it should be interpreted consistently so also + in ltac code. *) + +Record Foo := {}. +Bind Scope foo_scope with Foo. +Notation "!" := Build_Foo : foo_scope. +Notation "!" := 1 : core_scope. +Open Scope foo_scope. +Open Scope core_scope. + +Goal Foo. + Fail exact !. +(* ... but maybe will we want it to succeed eventually if we ever + would be able to make it working the same in + +Ltac myexact e := exact e. + +Goal Foo. + myexact !. +Defined. +*) diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v new file mode 100644 index 0000000000..21b03ce541 --- /dev/null +++ b/test-suite/bugs/closed/4069.v @@ -0,0 +1,51 @@ + +Lemma test1 : +forall (v : nat) (f g : nat -> nat), +f v = g v. +intros. f_equal. +(* +Goal in v8.5: f v = g v +Goal in v8.4: v = v -> f v = g v +Expected: f = g +*) +Admitted. + +Lemma test2 : +forall (v u : nat) (f g : nat -> nat), +f v = g u. +intros. f_equal. +(* +In both v8.4 And v8.5 +Goal 1: v = u -> f v = g u +Goal 2: v = u + +Expected Goal 1: f = g +Expected Goal 2: v = u +*) +Admitted. + +Lemma test3 : +forall (v : nat) (u : list nat) (f : nat -> nat) (g : list nat -> nat), +f v = g u. +intros. f_equal. +(* +In both v8.4 And v8.5, the goal is unchanged. +*) +Admitted. + +Require Import List. +Lemma foo n (l k : list nat) : k ++ skipn n l = skipn n l. +Proof. f_equal. +(* + 8.4: leaves the goal unchanged, i.e. k ++ skipn n l = skipn n l + 8.5: 2 goals, skipn n l = l -> k ++ skipn n l = skipn n l + and skipn n l = l +*) +Require Import List. +Fixpoint replicate {A} (n : nat) (x : A) : list A := + match n with 0 => nil | S n => x :: replicate n x end. +Lemma bar {A} n m (x : A) : + skipn n (replicate m x) = replicate (m - n) x -> + skipn n (replicate m x) = replicate (m - n) x. +Proof. intros. f_equal. +(* 8.5: one goal, n = m - n *) diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v index c6cb9c35e6..e4d76732a3 100644 --- a/test-suite/bugs/closed/4089.v +++ b/test-suite/bugs/closed/4089.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *) diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v index f808cb45e9..5932c9c56e 100644 --- a/test-suite/bugs/closed/4116.v +++ b/test-suite/bugs/closed/4116.v @@ -110,7 +110,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" := - refine (let __transparent_assert_hypothesis := (_ : type) in _); + unshelve refine (let __transparent_assert_hypothesis := (_ : type) in _); [ | ( let H := match goal with H := _ |- _ => constr:(H) end in @@ -321,7 +321,7 @@ Section Grothendieck. Definition Gcategory : PreCategory. Proof. - refine (@Build_PreCategory + unshelve refine (@Build_PreCategory Pair (fun s d => Gmorphism s d) Gidentity @@ -346,7 +346,7 @@ Section Grothendieck2. Instance iscategory_grothendieck_toset : IsCategory (Gcategory F). Proof. intros s d. - refine (isequiv_adjointify _ _ _ _). + unshelve refine (isequiv_adjointify _ _ _ _). { intro m. transparent assert (H' : (s.(c) = d.(c))). diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v index 5f8c411ca8..d34a2b8b1b 100644 --- a/test-suite/bugs/closed/4121.v +++ b/test-suite/bugs/closed/4121.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (* -*- coq-prog-args: ("-emacs" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *) (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 diff --git a/test-suite/bugs/closed/4149.v b/test-suite/bugs/closed/4149.v new file mode 100644 index 0000000000..b81c680cd7 --- /dev/null +++ b/test-suite/bugs/closed/4149.v @@ -0,0 +1,4 @@ +Goal forall A, A -> Type. +Proof. + intros; eauto. +Qed. diff --git a/test-suite/bugs/closed/4151.v b/test-suite/bugs/closed/4151.v new file mode 100644 index 0000000000..fec64555f4 --- /dev/null +++ b/test-suite/bugs/closed/4151.v @@ -0,0 +1,403 @@ +Lemma foo (H : forall A, A) : forall A, A. + Show Universes. + eexact H. +Qed. + +(* File reduced by coq-bug-finder from original input, then from 6390 lines to 397 lines *) +(* coqc version 8.5beta1 (March 2015) compiled on Mar 17 2015 12:34:25 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (1b3759e78f227eb85a128c58b8ce8c11509dd8c3) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.SetoidList. +Require Export Coq.Program.Program. + +Global Set Implicit Arguments. +Global Set Asymmetric Patterns. + +Fixpoint combine_sig_helper {T} {P : T -> Prop} (ls : list T) : (forall x, In x ls -> P x) -> list (sig P). + admit. +Defined. + +Lemma Forall_forall1_transparent_helper_1 {A P} {x : A} {xs : list A} {l : list A} + (H : Forall P l) (H' : x::xs = l) +: P x. + admit. +Defined. +Lemma Forall_forall1_transparent_helper_2 {A P} {x : A} {xs : list A} {l : list A} + (H : Forall P l) (H' : x::xs = l) +: Forall P xs. + admit. +Defined. + +Fixpoint Forall_forall1_transparent {A} (P : A -> Prop) (l : list A) {struct l} +: Forall P l -> forall x, In x l -> P x + := match l as l return Forall P l -> forall x, In x l -> P x with + | nil => fun _ _ f => match f : False with end + | x::xs => fun H x' H' => + match H' with + | or_introl H'' => eq_rect x + P + (Forall_forall1_transparent_helper_1 H eq_refl) + _ + H'' + | or_intror H'' => @Forall_forall1_transparent A P xs (Forall_forall1_transparent_helper_2 H eq_refl) _ H'' + end + end. + +Definition combine_sig {T P ls} (H : List.Forall P ls) : list (@sig T P) + := combine_sig_helper ls (@Forall_forall1_transparent T P ls H). +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Record string_like (CharType : Type) := + { + String :> Type; + Singleton : CharType -> String where "[ x ]" := (Singleton x); + Empty : String; + Concat : String -> String -> String where "x ++ y" := (Concat x y); + bool_eq : String -> String -> bool; + bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y; + Length : String -> nat; + Associativity : forall x y z, (x ++ y) ++ z = x ++ (y ++ z); + LeftId : forall x, Empty ++ x = x; + RightId : forall x, x ++ Empty = x; + Singleton_Length : forall x, Length (Singleton x) = 1; + Length_correct : forall s1 s2, Length s1 + Length s2 = Length (s1 ++ s2); + Length_Empty : Length Empty = 0; + Empty_Length : forall s1, Length s1 = 0 -> s1 = Empty; + Not_Singleton_Empty : forall x, Singleton x <> Empty; + SplitAt : nat -> String -> String * String; + SplitAt_correct : forall n s, fst (SplitAt n s) ++ snd (SplitAt n s) = s; + SplitAt_concat_correct : forall s1 s2, SplitAt (Length s1) (s1 ++ s2) = (s1, s2); + SplitAtLength_correct : forall n s, Length (fst (SplitAt n s)) = min (Length s) n + }. + +Delimit Scope string_like_scope with string_like. +Bind Scope string_like_scope with String. +Arguments Length {_%type_scope _} _%string_like. +Notation "[[ x ]]" := (@Singleton _ _ x) : string_like_scope. +Infix "++" := (@Concat _ _) : string_like_scope. +Infix "=s" := (@bool_eq _ _) (at level 70, right associativity) : string_like_scope. + +Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String) + := Length s1 < Length s2 \/ s1 = s2. +Infix "≤s" := str_le (at level 70, right associativity). + +Record StringWithSplitState {CharType} (String : string_like CharType) (split_stateT : String -> Type) := + { string_val :> String; + state_val : split_stateT string_val }. + +Module Export ContextFreeGrammar. + Require Import Coq.Strings.String. + + Section cfg. + Variable CharType : Type. + + Section definitions. + + Inductive item := + | Terminal (_ : CharType) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + End cfg. + +End ContextFreeGrammar. +Module Export BaseTypes. + Import Coq.Strings.String. + + Local Open Scope string_like_scope. + + Inductive any_grammar CharType := + | include_item (_ : item CharType) + | include_production (_ : production CharType) + | include_productions (_ : productions CharType) + | include_nonterminal (_ : string). + Global Coercion include_item : item >-> any_grammar. + Global Coercion include_production : production >-> any_grammar. + + Section recursive_descent_parser. + Context {CharType : Type} + {String : string_like CharType} + {G : grammar CharType}. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> string -> bool; + remove_nonterminal : nonterminals_listT -> string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal = true + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_computational_types_dataT := + { predata :> parser_computational_predataT; + split_stateT : String -> nonterminals_listT -> any_grammar CharType -> String -> Type }. + + Class parser_computational_dataT' `{parser_computational_types_dataT} := + { split_string_for_production + : forall (str0 : String) (valid : nonterminals_listT) (it : item CharType) (its : production CharType) (str : StringWithSplitState String (split_stateT str0 valid (it::its : production CharType))), + list (StringWithSplitState String (split_stateT str0 valid it) + * StringWithSplitState String (split_stateT str0 valid its)); + split_string_for_production_correct + : forall str0 valid it its str, + let P f := List.Forall f (@split_string_for_production str0 valid it its str) in + P (fun s1s2 => (fst s1s2 ++ snd s1s2 =s str) = true) }. + End recursive_descent_parser. + +End BaseTypes. +Import Coq.Strings.String. + +Section cfg. + Context CharType (String : string_like CharType) (G : grammar CharType). + Context (names_listT : Type) + (initial_names_data : names_listT) + (is_valid_name : names_listT -> string -> bool) + (remove_name : names_listT -> string -> names_listT) + (names_listT_R : names_listT -> names_listT -> Prop) + (remove_name_dec : forall ls name, + is_valid_name ls name = true + -> names_listT_R (remove_name ls name) ls) + (remove_name_1 + : forall ls ps ps', + is_valid_name (remove_name ls ps) ps' = true + -> is_valid_name ls ps' = true) + (remove_name_2 + : forall ls ps ps', + is_valid_name (remove_name ls ps) ps' = false + <-> is_valid_name ls ps' = false \/ ps = ps') + (ntl_wf : well_founded names_listT_R). + + Inductive minimal_parse_of + : forall (str0 : String) (valid : names_listT) + (str : String), + productions CharType -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : names_listT) + (str : String), + production CharType -> Type := + | MinParseProductionNil : forall str0 valid, + @minimal_parse_of_production str0 valid (Empty _) nil + | MinParseProductionCons : forall str0 valid str strs pat pats, + str ++ strs ≤s str0 + -> @minimal_parse_of_item str0 valid str pat + -> @minimal_parse_of_production str0 valid strs pats + -> @minimal_parse_of_production str0 valid (str ++ strs) (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : names_listT) + (str : String), + item CharType -> Type := + | MinParseTerminal : forall str0 valid x, + @minimal_parse_of_item str0 valid [[ x ]]%string_like (Terminal x) + | MinParseNonTerminal + : forall str0 valid str name, + @minimal_parse_of_name str0 valid str name + -> @minimal_parse_of_item str0 valid str (NonTerminal CharType name) + with minimal_parse_of_name + : forall (str0 : String) (valid : names_listT) + (str : String), + string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid name str, + Length str < Length str0 + -> is_valid_name initial_names_data name = true + -> @minimal_parse_of str initial_names_data str (Lookup G name) + -> @minimal_parse_of_name str0 valid str name + | MinParseNonTerminalStrEq + : forall str valid name, + is_valid_name initial_names_data name = true + -> is_valid_name valid name = true + -> @minimal_parse_of str (remove_name valid name) str (Lookup G name) + -> @minimal_parse_of_name str valid str name. +End cfg. + +Local Coercion is_true : bool >-> Sortclass. + +Local Open Scope string_like_scope. + +Section general. + Context {CharType} {String : string_like CharType} {G : grammar CharType}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_stateT : String -> Type; + data' :> _ := {| BaseTypes.predata := predata ; BaseTypes.split_stateT := fun _ _ _ => split_stateT |}; + split_string_for_production + : forall it its, + StringWithSplitState String split_stateT + -> list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT); + split_string_for_production_correct + : forall it its (str : StringWithSplitState String split_stateT), + let P f := List.Forall f (split_string_for_production it its str) in + P (fun s1s2 => + (fst s1s2 ++ snd s1s2 =s str) = true); + premethods :> parser_computational_dataT' + := @Build_parser_computational_dataT' + _ String data' + (fun _ _ => split_string_for_production) + (fun _ _ => split_string_for_production_correct) }. + + Definition split_list_completeT `{data : boolean_parser_dataT} + {str0 valid} + (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) + (split_list : list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT)) + (it : item CharType) (its : production CharType) + := ({ s1s2 : String * String + & (fst s1s2 ++ snd s1s2 =s str) + * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it) + * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type) + -> ({ s1s2 : StringWithSplitState String split_stateT * StringWithSplitState String split_stateT + & (In s1s2 split_list) + * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it) + * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type). +End general. + +Section recursive_descent_parser. + Context {CharType} + {String : string_like CharType} + {G : grammar CharType}. + Context `{data : @boolean_parser_dataT _ String}. + + Section bool. + Section parts. + Definition parse_item + (str_matches_nonterminal : string -> bool) + (str : StringWithSplitState String split_stateT) + (it : item CharType) + : bool + := match it with + | Terminal ch => [[ ch ]] =s str + | NonTerminal nt => str_matches_nonterminal nt + end. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Fixpoint parse_production + (str : StringWithSplitState String split_stateT) + (pf : str ≤s str0) + (prod : production CharType) + : bool. + Proof. + refine + match prod with + | nil => + + str =s Empty _ + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (let mapF f := map f (combine_sig (split_string_for_production_correct it its str)) in + mapF (fun s1s2p => + (parse_item + (parse_nonterminal (fst (proj1_sig s1s2p)) _) + (fst (proj1_sig s1s2p)) + it) + && parse_production' (snd (proj1_sig s1s2p)) _)%bool) + end; + revert pf; clear; intros; admit. + Defined. + End production. + + End parts. + End bool. +End recursive_descent_parser. + +Section sound. + Context CharType (String : string_like CharType) (G : grammar CharType). + Context `{data : @boolean_parser_dataT CharType String}. + + Section production. + Context (str0 : String) + (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Definition parse_nonterminal_completeT P + := forall valid (str : StringWithSplitState String split_stateT) pf nonterminal (H_sub : P str0 valid nonterminal), + minimal_parse_of_name _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal + -> @parse_nonterminal str pf nonterminal = true. + + Lemma parse_production_complete + valid Pv + (parse_nonterminal_complete : parse_nonterminal_completeT Pv) + (Hinit : forall str (pf : str ≤s str0) nonterminal, + minimal_parse_of_name String G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal + -> Pv str0 valid nonterminal) + (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) + (prod : production CharType) + (split_string_for_production_complete' + : forall str0 valid str pf, + Forall_tails + (fun prod' => + match prod' return Type with + | nil => True + | it::its => split_list_completeT (G := G) (valid := valid) (str0 := str0) str pf (split_string_for_production it its str) it its + end) + prod) + : minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str prod + -> parse_production parse_nonterminal str pf prod = true. + admit. + Defined. + End production. + Context (str0 : String) + (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Goal forall (a : production CharType), + (forall (str1 : String) (valid : nonterminals_listT) + (str : StringWithSplitState String split_stateT) + (pf : str ≤s str1), + Forall_tails + (fun prod' : list (item CharType) => + match prod' with + | [] => True + | it :: its => + split_list_completeT (G := G) (valid := valid) str pf + (split_string_for_production it its str) it its + end) a) -> + forall (str : String) (pf : str ≤s str0) (st : split_stateT str), + parse_production parse_nonterminal + {| string_val := str; state_val := st |} pf a = true. + Proof. + intros a X **. + eapply parse_production_complete. + Focus 3. + exact X. + Undo. + assumption. + Undo. + eassumption. (* no applicable tactic *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4161.v b/test-suite/bugs/closed/4161.v new file mode 100644 index 0000000000..aa2b189b67 --- /dev/null +++ b/test-suite/bugs/closed/4161.v @@ -0,0 +1,27 @@ + + (* Inductive t : Type -> Type := *) + (* | Just : forall (A : Type), t A -> t A. *) + + (* Fixpoint test {A : Type} (x : t A) : t (A + unit) := *) + (* match x in t A return t (A + unit) with *) + (* | Just T x => @test T x *) + (* end. *) + + + Definition Type1 := Type. +Definition Type2 := Type. +Definition cast (x:Type2) := x:Type1. +Axiom f: Type2 -> Prop. +Definition A := + let T := fun A:Type1 => _ in + fun A':Type2 => + eq_refl : T A' = f A' :> Prop. +(* Type2 <= Type1... f A -> Type1 <= Type2 *) + +Inductive t : Type -> Type := + | Just : forall (A : Type), t A -> t A. + +Fixpoint test {A : Type} (x : t A) : t (A + unit) := + match x in t A with + | Just B x => @test B x + end.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4251.v b/test-suite/bugs/closed/4251.v new file mode 100644 index 0000000000..66343d6671 --- /dev/null +++ b/test-suite/bugs/closed/4251.v @@ -0,0 +1,17 @@ + +Inductive array : Type -> Type := +| carray : forall A, array A. + +Inductive Mtac : Type -> Prop := +| bind : forall {A B}, Mtac A -> (A -> Mtac B) -> Mtac B +| array_make : forall {A}, A -> Mtac (array A). + +Definition Ref := array. + +Definition ref : forall {A}, A -> Mtac (Ref A) := + fun A x=> array_make x. +Check array Type. +Check fun A : Type => Ref A. + +Definition abs_val (a : Type) := + bind (ref a) (fun r : array Type => array_make tt).
\ No newline at end of file diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v new file mode 100644 index 0000000000..3cdc4ada02 --- /dev/null +++ b/test-suite/bugs/closed/4256.v @@ -0,0 +1,43 @@ +(* Testing 8.5 regression with type classes not solving evars + redefined while trying to solve them with the type class mechanism *) + +Global Set Universe Polymorphism. +Monomorphic Universe i. +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. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. +Notation "-1" := (trunc_S minus_two) (at level 0). + +Class IsPointed (A : Type) := point : A. +Arguments point A {_}. + +Record pType := + { pointed_type : Type ; + ispointed_type : IsPointed pointed_type }. +Coercion pointed_type : pType >-> Sortclass. +Existing Instance ispointed_type. + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + + + +Record ooGroup := + { classifying_space : pType@{i} }. + +Definition group_loops (X : pType) +: ooGroup. +Proof. + (** This works: *) + pose (x0 := point X). + pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)). + clear H x0. + (** But this doesn't: *) + pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)). diff --git a/test-suite/bugs/closed/4273.v b/test-suite/bugs/closed/4273.v new file mode 100644 index 0000000000..591ea4b5b2 --- /dev/null +++ b/test-suite/bugs/closed/4273.v @@ -0,0 +1,9 @@ + + +Set Primitive Projections. +Record total2 (P : nat -> Prop) := tpair { pr1 : nat; pr2 : P pr1 }. +Theorem onefiber' (q : total2 (fun y => y = 0)) : True. +Proof. assert (foo:=pr2 _ q). simpl in foo. + destruct foo. (* Error: q is used in conclusion. *) exact I. Qed. + +Print onefiber'.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4284.v b/test-suite/bugs/closed/4284.v new file mode 100644 index 0000000000..0fff3026ff --- /dev/null +++ b/test-suite/bugs/closed/4284.v @@ -0,0 +1,6 @@ +Set Primitive Projections. +Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }. +Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True. +Proof. +set (Q1 := total2 (fun f => pr1 P f = x)). +set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)). diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v new file mode 100644 index 0000000000..43c9b51295 --- /dev/null +++ b/test-suite/bugs/closed/4287.v @@ -0,0 +1,123 @@ +Unset Strict Universe Declaration. + +Universe b. + +Universe c. + +Definition U : Type@{b} := Type@{c}. + +Module Type MT. + +Definition T := Prop. +End MT. + +Module M : MT. + Definition T := Type@{b}. + +Print Universes. +Fail End M. + +Set Universe Polymorphism. + +(* This is a modified version of Hurkens with all universes floating *) +Section Hurkens. + +Variable down : Type -> Type. +Variable up : Type -> Type. + +Hypothesis back : forall A, up (down A) -> A. + +Hypothesis forth : forall A, A -> up (down A). + +Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A), + P (back A (forth A a)) -> P a. + +Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A), + P a -> P (back A (forth A a)). + +(** Proof *) +Definition V : Type := forall A:Type, ((up A -> Type) -> up A -> Type) -> up A -> Type. +Definition U : Type := V -> Type. + +Definition sb (z:V) : V := fun A r a => r (z A r) a. +Definition le (i:U -> Type) (x:U) : Type := x (fun A r a => i (fun v => sb v A r a)). +Definition le' (i:up (down U) -> Type) (x:up (down U)) : Type := le (fun a:U => i (forth _ a)) (back _ x). +Definition induct (i:U -> Type) : Type := forall x:U, up (le i x) -> up (i x). +Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))). +Definition I (x:U) : Type := + (forall i:U -> Type, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False. + +Lemma Omega : forall i:U -> Type, induct i -> up (i WF). +Proof. +intros i y. +apply y. +unfold le, WF, induct. +apply forth. +intros x H0. +apply y. +unfold sb, le', le. +compute. +apply backforth_r. +exact H0. +Qed. + +Lemma lemma1 : induct (fun u => down (I u)). +Proof. +unfold induct. +intros x p. +apply forth. +intro q. +generalize (q (fun u => down (I u)) p). +intro r. +apply back in r. +apply r. +intros i j. +unfold le, sb, le', le in j |-. +apply backforth in j. +specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))). +apply q. +exact j. +Qed. + +Lemma lemma2 : (forall i:U -> Type, induct i -> up (i WF)) -> False. +Proof. +intro x. +generalize (x (fun u => down (I u)) lemma1). +intro r; apply back in r. +apply r. +intros i H0. +apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))). +unfold le, WF in H0. +apply back in H0. +exact H0. +Qed. + +Theorem paradox : False. +Proof. +exact (lemma2 Omega). +Qed. + +End Hurkens. + +Polymorphic Record box (T : Type) := wrap {unwrap : T}. + +(* Here we instantiate to Set *) + +Fail Definition down (x : Type) : Prop := box x. +Definition up (x : Prop) : Type := x. + +Fail Definition back A : up (down A) -> A := unwrap A. + +Fail Definition forth A : A -> up (down A) := wrap A. + +Definition id {A : Type} (a : A) := a. +Definition setlt (A : Type@{i}) := + let foo := Type@{i} : Type@{j} in True. + +Definition setle (B : Type@{i}) := + let foo (A : Type@{j}) := A in foo B. + +Fail Check @setlt@{j Prop}. +Fail Definition foo := @setle@{j Prop}. +Check setlt@{Set i}. +Check setlt@{Set j}.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v new file mode 100644 index 0000000000..3671c931b7 --- /dev/null +++ b/test-suite/bugs/closed/4293.v @@ -0,0 +1,7 @@ +Module Type Foo. +Definition T := let X := Type in Type. +End Foo. + +Module M : Foo. +Definition T := let X := Type in Type. +End M.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4294.v b/test-suite/bugs/closed/4294.v new file mode 100644 index 0000000000..1d5e3c71b8 --- /dev/null +++ b/test-suite/bugs/closed/4294.v @@ -0,0 +1,31 @@ +Require Import Hurkens. + +Module NonPoly. +Module Type Foo. + Definition U := Type. + Parameter eq : Type = U. +End Foo. + +Module M : Foo with Definition U := Type. + Definition U := Type. + Definition eq : Type = U := eq_refl. +End M. + +Print Universes. +Fail Definition bad : False := TypeNeqSmallType.paradox M.U M.eq. +End NonPoly. + +Set Universe Polymorphism. + +Module Type Foo. + Definition U := Type. + Monomorphic Parameter eq : Type = U. +End Foo. + +Module M : Foo with Definition U := Type. + Definition U := Type. + Monomorphic Definition eq : Type = U := eq_refl. +End M. + +Fail Definition bad : False := TypeNeqSmallType.paradox Type M.eq. +(* Print Assumptions bad. *) diff --git a/test-suite/bugs/closed/4298.v b/test-suite/bugs/closed/4298.v new file mode 100644 index 0000000000..875612ddf4 --- /dev/null +++ b/test-suite/bugs/closed/4298.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. + +Module Type Foo. + Definition U := Type. +End Foo. + +Fail Module M : Foo with Definition U := Prop. diff --git a/test-suite/bugs/closed/4299.v b/test-suite/bugs/closed/4299.v new file mode 100644 index 0000000000..955c3017d7 --- /dev/null +++ b/test-suite/bugs/closed/4299.v @@ -0,0 +1,12 @@ +Unset Strict Universe Declaration. +Set Universe Polymorphism. + +Module Type Foo. + Definition U := Type : Type. + Parameter eq : Type = U. +End Foo. + +Module M : Foo with Definition U := Type : Type. + Definition U := let X := Type in Type. + Definition eq : Type = U := eq_refl. +Fail End M.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v new file mode 100644 index 0000000000..b4e17c2231 --- /dev/null +++ b/test-suite/bugs/closed/4301.v @@ -0,0 +1,13 @@ +Unset Strict Universe Declaration. +Set Universe Polymorphism. + +Module Type Foo. + Parameter U : Type. +End Foo. + +Module Lower (X : Foo with Definition U := True : Type). +End Lower. + +Module M : Foo. + Definition U := nat : Type@{i}. +End M. diff --git a/test-suite/bugs/closed/4316.v b/test-suite/bugs/closed/4316.v new file mode 100644 index 0000000000..68dec1334a --- /dev/null +++ b/test-suite/bugs/closed/4316.v @@ -0,0 +1,3 @@ +Ltac tac := idtac. +Reset tac. +Ltac tac := idtac. diff --git a/test-suite/bugs/closed/4318.v b/test-suite/bugs/closed/4318.v new file mode 100644 index 0000000000..e3140ed5ab --- /dev/null +++ b/test-suite/bugs/closed/4318.v @@ -0,0 +1,2 @@ +(* Check no anomaly is raised *) +Fail Definition foo p := match p with (x, y) z => tt end. diff --git a/test-suite/bugs/closed/4325.v b/test-suite/bugs/closed/4325.v new file mode 100644 index 0000000000..af69ca04b6 --- /dev/null +++ b/test-suite/bugs/closed/4325.v @@ -0,0 +1,5 @@ +Goal (forall a b : nat, Set = (a = b)) -> Set. +Proof. + clear. + intro H. + erewrite (fun H' => H _ H'). diff --git a/test-suite/bugs/closed/4328.v b/test-suite/bugs/closed/4328.v new file mode 100644 index 0000000000..8e1bb31007 --- /dev/null +++ b/test-suite/bugs/closed/4328.v @@ -0,0 +1,6 @@ +Inductive M (A:Type) : Type := M'. +Axiom pi : forall (P : Prop) (p : P), Prop. +Definition test1 A (x : _) := pi A x. (* success *) +Fail Definition test2 A (x : A) := pi A x. (* failure ??? *) +Fail Definition test3 A (x : A) (_ : M A) := pi A x. (* failure *) +Fail Definition test4 A (_ : M A) (x : A) := pi A x. (* success ??? *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4346.v b/test-suite/bugs/closed/4346.v new file mode 100644 index 0000000000..b50dff2411 --- /dev/null +++ b/test-suite/bugs/closed/4346.v @@ -0,0 +1,2 @@ +Check (Set <: Type). +Check (Set <<: Type). diff --git a/test-suite/bugs/closed/4347.v b/test-suite/bugs/closed/4347.v new file mode 100644 index 0000000000..29686a26c1 --- /dev/null +++ b/test-suite/bugs/closed/4347.v @@ -0,0 +1,17 @@ +Fixpoint demo_recursion(n:nat) := match n with + |0 => Type + |S k => (demo_recursion k) -> Type + end. + +Record Demonstration := mkDemo +{ + demo_law : forall n:nat, demo_recursion n; + demo_stuff : forall n:nat, forall q:(fix demo_recursion (n : nat) : Type := + match n with + | 0 => Type + | S k => demo_recursion k -> Type + end) n, (demo_law (S n)) q +}. + +Theorem DemoError : Demonstration. +Fail apply mkDemo. (*Anomaly: Uncaught exception Not_found. Please report.*) diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v new file mode 100644 index 0000000000..e71ddaf71f --- /dev/null +++ b/test-suite/bugs/closed/4354.v @@ -0,0 +1,11 @@ +Inductive True : Prop := I. +Class Lift (T : Type). +Axiom closed_increment : forall {T} {H : Lift T}, True. +Create HintDb core. +Lemma closed_monotonic T (H : Lift T) : True. +Proof. + Set Printing Universes. + auto using closed_increment. Show Universes. +Qed. +(* also fails with -nois, so the content of the hint database does not matter +*)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v new file mode 100644 index 0000000000..9895548c1d --- /dev/null +++ b/test-suite/bugs/closed/4363.v @@ -0,0 +1,9 @@ +Set Printing Universes. +Definition foo : Type. +Proof. + assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat). + exact bar. +Defined. (* Toplevel input, characters 0-8: +Error: +The term "(fun _ : Set => bar) foo_subproof" has type +"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *) diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v new file mode 100644 index 0000000000..6a5e9a4023 --- /dev/null +++ b/test-suite/bugs/closed/4366.v @@ -0,0 +1,15 @@ +Fixpoint stupid (n : nat) : unit := +match n with +| 0 => tt +| S n => + let () := stupid n in + let () := stupid n in + tt +end. + +Goal True. +Proof. +pose (v := stupid 24). +Timeout 2 vm_compute in v. +exact I. +Qed. diff --git a/test-suite/bugs/closed/4372.v b/test-suite/bugs/closed/4372.v new file mode 100644 index 0000000000..428192a344 --- /dev/null +++ b/test-suite/bugs/closed/4372.v @@ -0,0 +1,20 @@ +(* Tactic inversion was raising an anomaly because of a fake + dependency of TypeDenote into its argument *) + +Inductive expr := +| ETrue. + +Inductive IntermediateType : Set := ITbool. + +Definition TypeDenote (IT : IntermediateType) : Type := + match IT with + | _ => bool + end. + +Inductive ValueDenote : forall (e:expr) it, TypeDenote it -> Prop := +| VT : ValueDenote ETrue ITbool true. + +Goal forall it v, @ValueDenote ETrue it v -> True. + intros it v H. + inversion H. +Abort. diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v new file mode 100644 index 0000000000..03af16535b --- /dev/null +++ b/test-suite/bugs/closed/4375.v @@ -0,0 +1,106 @@ + + +Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + + +Module A. +Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => foo t n + end. +End A. + +Module B. +Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => foo t n + end. +End B. + +Module C. +Fail Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{j} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End C. + +Module D. +Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{i j} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End D. + +Module E. +Fail Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{j i} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End E. + +(* +Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + +Print g. + +Polymorphic Fixpoint a@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t +with b@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + +Print a. +Print b. +*) + +Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} := +| A : foo T -> foo T. + +Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (cg@{i} t). + +Print cg. + +Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (@cb@{i} t) +with cb@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (@ca@{i} t). + +Print ca. +Print cb.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4378.v b/test-suite/bugs/closed/4378.v new file mode 100644 index 0000000000..9d59165562 --- /dev/null +++ b/test-suite/bugs/closed/4378.v @@ -0,0 +1,9 @@ +Tactic Notation "epose" open_constr(a) := + let a' := fresh in + pose a as a'. +Tactic Notation "epose2" open_constr(a) tactic3(tac) := + let a' := fresh in + pose a as a'. +Goal True. + epose _. Undo. + epose2 _ idtac. diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v new file mode 100644 index 0000000000..a96a137001 --- /dev/null +++ b/test-suite/bugs/closed/4390.v @@ -0,0 +1,37 @@ +Module A. +Set Printing All. +Set Printing Universes. + +Module M. +Section foo. +Universe i. +End foo. +End M. + +Check Type@{i}. +(* Succeeds *) + +Fail Check Type@{j}. +(* Error: Undeclared universe: j *) + +Definition foo@{j} : Type@{i} := Type@{j}. +(* ok *) +End A. + +Set Universe Polymorphism. +Fail Universes j. +Monomorphic Universe j. +Section foo. + Universes i. + Constraint i < j. + Definition foo : Type@{j} := Type@{i}. + Definition foo' : Type@{j} := Type@{i}. +End foo. + +Check eq_refl : foo@{i} = foo'@{i}. + +Definition bar := foo. +Monomorphic Definition bar'@{k} := foo@{k}. + +Fail Constraint j = j. +Monomorphic Constraint i = i. diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v new file mode 100644 index 0000000000..60c9354597 --- /dev/null +++ b/test-suite/bugs/closed/4394.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) + +Require Import Equality List. +Inductive Foo (I : Type -> Type) (A : Type) : Type := +| foo (B : Type) : A -> I B -> Foo I A. +Definition Family := Type -> Type. +Definition FooToo : Family -> Family := Foo. +Definition optionize (I : Type -> Type) (A : Type) := option (I A). +Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A. +Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. +Definition barRec : Rec (optionize id) := {| rec := bar id |}. +Inductive Empty {T} : T -> Prop := . +Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) : + Empty (a, b) -> False. +Proof. + intro e. + dependent induction e. +Qed. + diff --git a/test-suite/bugs/closed/4397.v b/test-suite/bugs/closed/4397.v new file mode 100644 index 0000000000..3566353d84 --- /dev/null +++ b/test-suite/bugs/closed/4397.v @@ -0,0 +1,3 @@ +Require Import Equality. +Theorem foo (u : unit) (H : u = u) : True. +dependent destruction H. diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v new file mode 100644 index 0000000000..5c23f8404b --- /dev/null +++ b/test-suite/bugs/closed/4400.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) +Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality. +Set Printing Universes. +Inductive Foo (I : Type -> Type) (A : Type) : Type := +| foo (B : Type) : A -> I B -> Foo I A. +Definition Family := Type -> Type. +Definition FooToo : Family -> Family := Foo. +Definition optionize (I : Type -> Type) (A : Type) := option (I A). +Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A. +Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. +Definition barRec : Rec (optionize id) := {| rec := bar id |}. +Inductive Empty {T} : T -> Prop := . +Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) +nil)) (b : unit) : + Empty (a, b) -> False. +Proof. + intro e. + dependent induction e. +Qed. diff --git a/test-suite/bugs/closed/4404.v b/test-suite/bugs/closed/4404.v new file mode 100644 index 0000000000..27b43a61d4 --- /dev/null +++ b/test-suite/bugs/closed/4404.v @@ -0,0 +1,4 @@ +Inductive Foo : Type -> Type := foo A : Foo A. +Goal True. + remember Foo. + diff --git a/test-suite/bugs/closed/4412.v b/test-suite/bugs/closed/4412.v new file mode 100644 index 0000000000..4b2aae0c7b --- /dev/null +++ b/test-suite/bugs/closed/4412.v @@ -0,0 +1,4 @@ +Require Import Coq.Bool.Bool Coq.Setoids.Setoid. +Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True. + intros. + Fail rewrite Bool.andb_true_iff in H. diff --git a/test-suite/bugs/closed/4420.v b/test-suite/bugs/closed/4420.v new file mode 100644 index 0000000000..0e16cb2399 --- /dev/null +++ b/test-suite/bugs/closed/4420.v @@ -0,0 +1,19 @@ +Module foo. + Context (Char : Type). + Axiom foo : Type -> Type. + Goal foo Char = foo Char. + change foo with (fun x => foo x). + cbv beta. + reflexivity. + Defined. +End foo. + +Inductive foo (A : Type) : Prop := I. (*Top.1*) +Lemma bar : foo Type. (*Top.3*) +Proof. + Set Printing Universes. +change foo with (fun x : Type => foo x). (*Top.4*) +cbv beta. +apply I. (* I Type@{Top.3} : (fun x : Type@{Top.4} => foo x) Type@{Top.3} *) +Defined. + diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v new file mode 100644 index 0000000000..bf0e570ab8 --- /dev/null +++ b/test-suite/bugs/closed/4429.v @@ -0,0 +1,31 @@ +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/4433.v b/test-suite/bugs/closed/4433.v new file mode 100644 index 0000000000..9eeb864689 --- /dev/null +++ b/test-suite/bugs/closed/4433.v @@ -0,0 +1,29 @@ +Require Import Coq.Arith.Arith Coq.Init.Wf. +Axiom proof_admitted : False. +Goal exists x y z : nat, Fix + Wf_nat.lt_wf + (fun _ => nat -> nat) + (fun x' f => match x' as x'0 + return match x'0 with + | 0 => True + | S x'' => x'' < x' + end + -> nat -> nat + with + | 0 => fun _ _ => 0 + | S x'' => f x'' + end + (match x' with + | 0 => I + | S x'' => (Nat.lt_succ_diag_r _) + end)) + z + y + = 0. +Proof. + do 3 (eexists; [ shelve.. | ]). + match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end. + case proof_admitted. + Unshelve. + all:constructor. +Defined.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v new file mode 100644 index 0000000000..66dfa0e685 --- /dev/null +++ b/test-suite/bugs/closed/4443.v @@ -0,0 +1,31 @@ +Set Universe Polymorphism. + +Record TYPE@{i} := cType { + type : Type@{i}; +}. + +Definition PROD@{i j k} + (A : Type@{i}) + (B : A -> Type@{j}) + : TYPE@{k}. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + +Local Unset Strict Universe Declaration. +Definition PRODinj + (A : Type@{i}) + (B : A -> Type) + : TYPE. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + + Monomorphic Universe i j. + Monomorphic Constraint j < i. +Set Printing Universes. +Check PROD@{i i i}. +Check PRODinj@{i j}. +Fail Check PRODinj@{j i}.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4453.v b/test-suite/bugs/closed/4453.v new file mode 100644 index 0000000000..009dd5e3ca --- /dev/null +++ b/test-suite/bugs/closed/4453.v @@ -0,0 +1,8 @@ + +Section Foo. +Variable A : Type. +Lemma foo : A -> True. now intros _. Qed. +Goal Type -> True. +rename A into B. +intros A. +Fail apply foo. diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v new file mode 100644 index 0000000000..a32acf789c --- /dev/null +++ b/test-suite/bugs/closed/4456.v @@ -0,0 +1,647 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *) +(* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0 + coqtop version 8.5beta3 (November 2015) *) +(* Variable P : forall n m : nat, n = m -> Prop. *) +(* Axiom Prefl : forall n : nat, P n n eq_refl. *) +Axiom proof_admitted : False. + +Tactic Notation "admit" := case proof_admitted. + +Require Coq.Program.Program. +Require Coq.Strings.String. +Require Coq.omega.Omega. +Module Export Fiat_DOT_Common. +Module Export Fiat. +Module Common. +Import Coq.Lists.List. +Export Coq.Program.Program. + +Global Set Implicit Arguments. + +Global Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sum {A B} (b : sum A B) : bool := if b then true else false. + +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +End Common. + +End Fiat. + +End Fiat_DOT_Common. +Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export Fiat. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Relations.Relation_Definitions. +Import Coq.Classes.Morphisms. + +Local Coercion is_true : bool >-> Sortclass. + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + get : nat -> String -> option Char; + unsafe_get : nat -> String -> Char; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + singleton_exists : forall s, length s = 1 -> exists ch, s ~= [ ch ]; + get_0 : forall s ch, take 1 s ~= [ ch ] <-> get 0 s = Some ch; + get_S : forall n s, get (S n) s = get n (drop 1 s); + unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str); + bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str' + }. +Global Arguments StringLikeProperties _ {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core. +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Core. +Import Coq.Strings.String. +Import Coq.Lists.List. +Export Fiat.Parsers.StringLike.Core. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End Core. + +End ContextFreeGrammar. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core. + +Module Export Fiat_DOT_Parsers_DOT_BaseTypes. +Module Export Fiat. +Module Export Parsers. +Module Export BaseTypes. +Import Coq.Arith.Wf_nat. + +Local Coercion is_true : bool >-> Sortclass. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + nonterminal_carrierT : Type; + of_nonterminal : String.string -> nonterminal_carrierT; + to_nonterminal : nonterminal_carrierT -> String.string; + initial_nonterminals_data : nonterminals_listT; + nonterminals_length : nonterminals_listT -> nat; + is_valid_nonterminal : nonterminals_listT -> nonterminal_carrierT -> bool; + remove_nonterminal : nonterminals_listT -> nonterminal_carrierT -> nonterminals_listT }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop + := ltof _ nonterminals_length; + nonterminals_length_zero : forall ls, + nonterminals_length ls = 0 + -> forall nt, is_valid_nonterminal ls nt = false; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + remove_nonterminal_noninc : forall ls nonterminal, + ~nonterminals_listT_R ls (remove_nonterminal ls nonterminal); + initial_nonterminals_correct : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) <-> List.In nonterminal (Valid_nonterminals G); + initial_nonterminals_correct' : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data nonterminal <-> List.In (to_nonterminal nonterminal) (Valid_nonterminals G); + to_of_nonterminal : forall nonterminal, + List.In nonterminal (Valid_nonterminals G) + -> to_nonterminal (of_nonterminal nonterminal) = nonterminal; + of_to_nonterminal : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data nonterminal + -> of_nonterminal (to_nonterminal nonterminal) = nonterminal; + ntl_wf : well_founded nonterminals_listT_R + := well_founded_ltof _ _; + remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. + + Class split_dataT := + { split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_data :> split_dataT }. +End recursive_descent_parser. + +End BaseTypes. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_BaseTypes. + +Module Export Fiat_DOT_Common_DOT_List_DOT_Operations. +Module Export Fiat. +Module Export Common. +Module Export List. +Module Export Operations. + +Import Coq.Lists.List. + +Module Export List. + Section InT. + Context {A : Type} (a : A). + + Fixpoint InT (ls : list A) : Set + := match ls return Set with + | nil => False + | b :: m => (b = a) + InT m + end%type. + End InT. + + End List. + +End Operations. + +End List. + +End Common. + +End Fiat. + +End Fiat_DOT_Common_DOT_List_DOT_Operations. + +Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties. +Module Export Fiat. +Module Export Parsers. +Module Export StringLike. +Module Export Properties. + +Section String. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}. + + Lemma take_length {str n} + : length (take n str) = min n (length str). +admit. +Defined. + + End String. + +End Properties. + +End StringLike. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties. + +Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties. +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Properties. + +Local Open Scope list_scope. +Definition production_is_reachableT {Char} (G : grammar Char) (p : production Char) + := { nt : _ + & { prefix : _ + & List.In nt (Valid_nonterminals G) + * List.InT + (prefix ++ p) + (Lookup G nt) } }%type. + +End Properties. + +End ContextFreeGrammar. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties. + +Module Export Fiat_DOT_Parsers_DOT_MinimalParse. +Module Export Fiat. +Module Export Parsers. +Module Export MinimalParse. +Import Coq.Lists.List. +Import Fiat.Parsers.ContextFreeGrammar.Core. + +Local Coercion is_true : bool >-> Sortclass. +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' _ G predata}. + + Inductive minimal_parse_of + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall len0 valid str pat pats, + @minimal_parse_of_production len0 valid str pat + -> @minimal_parse_of len0 valid str (pat::pats) + | MinParseTail : forall len0 valid str pat pats, + @minimal_parse_of len0 valid str pats + -> @minimal_parse_of len0 valid str (pat::pats) + with minimal_parse_of_production + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall len0 valid str, + length str = 0 + -> @minimal_parse_of_production len0 valid str nil + | MinParseProductionCons : forall len0 valid str n pat pats, + length str <= len0 + -> @minimal_parse_of_item len0 valid (take n str) pat + -> @minimal_parse_of_production len0 valid (drop n str) pats + -> @minimal_parse_of_production len0 valid str (pat::pats) + with minimal_parse_of_item + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall len0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item len0 valid str (Terminal ch) + | MinParseNonTerminal + : forall len0 valid str (nt : String.string), + @minimal_parse_of_nonterminal len0 valid str nt + -> @minimal_parse_of_item len0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall len0 valid (nt : String.string) str, + length str < len0 + -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) + -> @minimal_parse_of (length str) initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal len0 valid str nt + | MinParseNonTerminalStrEq + : forall len0 str valid nonterminal, + length str = len0 + -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) + -> is_valid_nonterminal valid (of_nonterminal nonterminal) + -> @minimal_parse_of len0 (remove_nonterminal valid (of_nonterminal nonterminal)) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal len0 valid str nonterminal. + +End cfg. + +End MinimalParse. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_MinimalParse. + +Module Export Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes. +Module Export Fiat. +Module Export Parsers. +Module Export CorrectnessBaseTypes. +Import Coq.Lists.List. +Import Fiat.Parsers.ContextFreeGrammar.Core. +Import Fiat_DOT_Common.Fiat.Common. +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Definition split_list_completeT_for {data : @parser_computational_predataT} + {len0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : length str <= len0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) len0 valid (take n str) it) + * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In (min (length str) n) (map (min (length str)) split_list)) + * (minimal_parse_of_item (G := G) len0 valid (take n str) it) + * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type). + + Definition split_list_completeT {data : @parser_computational_predataT} + (splits : item Char -> production Char -> String -> list nat) + := forall len0 valid str (pf : length str <= len0) nt, + is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT_for data len0 valid it its str pf (splits it its str) + end)) + (Lookup G nt). + + Class boolean_parser_completeness_dataT' {data : boolean_parser_dataT} := + { split_string_for_production_complete + : split_list_completeT split_string_for_production }. +End general. + +End CorrectnessBaseTypes. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes. + +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Valid. +Export Fiat.Parsers.StringLike.Core. + +Section cfg. + Context {Char : Type} {HSL : StringLike Char} (G : grammar Char) + {predata : parser_computational_predataT}. + + Definition item_valid (it : item Char) + := match it with + | Terminal _ => True + | NonTerminal nt' => is_true (is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt')) + end. + + Definition production_valid pat + := List.Forall item_valid pat. + + Definition productions_valid pats + := List.Forall production_valid pats. + + Definition grammar_valid + := forall nt, + List.In nt (Valid_nonterminals G) + -> productions_valid (Lookup G nt). +End cfg. + +End Valid. + +Section app. + Context {Char : Type} {HSL : StringLike Char} (G : grammar Char) + {predata : parser_computational_predataT}. + + Lemma hd_production_valid + (it : item Char) + (its : production Char) + (H : production_valid (it :: its)) + : item_valid it. +admit. +Defined. + + Lemma production_valid_cons + (it : item Char) + (its : production Char) + (H : production_valid (it :: its)) + : production_valid its. +admit. +Defined. + + End app. + +Import Coq.Lists.List. +Import Coq.omega.Omega. +Import Fiat_DOT_Common.Fiat.Common. +Import Fiat.Parsers.ContextFreeGrammar.Valid. +Local Open Scope string_like_scope. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' _ G _} + {gvalid : grammar_valid G}. + + Local Notation dec T := (T + (T -> False))%type (only parsing). + + Local Notation iffT x y := ((x -> y) * (y -> x))%type (only parsing). + + Lemma dec_prod {A B} (HA : dec A) (HB : dec B) : dec (A * B). +admit. +Defined. + + Lemma dec_In {A} {P : A -> Type} (HA : forall a, dec (P a)) ls + : dec { a : _ & (In a ls * P a) }. +admit. +Defined. + + Section item. + Context {len0 valid} + (str : String) + (str_matches_nonterminal' + : nonterminal_carrierT -> bool) + (str_matches_nonterminal + : forall nt : nonterminal_carrierT, + dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))). + + Section valid. + Context (Hmatches + : forall nt, + is_valid_nonterminal initial_nonterminals_data nt + -> str_matches_nonterminal nt = str_matches_nonterminal' nt :> bool) + (it : item Char) + (Hvalid : item_valid it). + + Definition parse_item' + : dec (minimal_parse_of_item (G := G) len0 valid str it). + Proof. + clear Hvalid. + refine (match it return dec (minimal_parse_of_item len0 valid str it) with + | Terminal ch => if Sumbool.sumbool_of_bool (str ~= [ ch ]) + then inl (MinParseTerminal _ _ _ _ _) + else inr (fun _ => !) + | NonTerminal nt => if str_matches_nonterminal (of_nonterminal nt) + then inl (MinParseNonTerminal _) + else inr (fun _ => !) + end); + clear str_matches_nonterminal Hmatches; + admit. + Defined. + End valid. + + End item. + Context {len0 valid} + (parse_nonterminal + : forall (str : String) (len : nat) (Hlen : length str = len) (pf : len <= len0) (nt : nonterminal_carrierT), + dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))). + + Lemma dec_in_helper {ls it its str} + : iffT {n0 : nat & + (In (min (length str) n0) (map (min (length str)) ls) * + minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type} + {n0 : nat & + (In n0 ls * + (minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its))%type}. +admit. +Defined. + + Lemma parse_production'_helper {str it its} (pf : length str <= len0) + : dec {n0 : nat & + (minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type} + -> dec (minimal_parse_of_production (G := G) len0 valid str (it :: its)). +admit. +Defined. + Local Ltac t_parse_production_for := repeat + match goal with + | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H + | _ => progress subst + | _ => solve [ constructor; assumption ] + | [ H : minimal_parse_of_production _ _ _ nil |- _ ] => (inversion H; clear H) + | [ H : minimal_parse_of_production _ _ _ (_::_) |- _ ] => (inversion H; clear H) + | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H' + | _ => progress simpl in * + | _ => discriminate + | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z)) + | _ => solve [ eauto with nocore ] + | _ => solve [ apply Min.min_case_strong; omega ] + | _ => omega + | [ H : production_valid (_::_) |- _ ] + => let H' := fresh in + pose proof H as H'; + apply production_valid_cons in H; + apply hd_production_valid in H' + end. + + Definition parse_production'_for + (splits : item Char -> production Char -> String -> list nat) + (Hsplits : forall str it its (Hreachable : production_is_reachableT G (it::its)) pf', split_list_completeT_for (len0 := len0) (G := G) (valid := valid) it its str pf' (splits it its str)) + (str : String) + (len : nat) + (Hlen : length str = len) + (pf : len <= len0) + (prod : production Char) + (Hreachable : production_is_reachableT G prod) + : dec (minimal_parse_of_production (G := G) len0 valid str prod). + Proof. + revert prod Hreachable str len Hlen pf. + refine + ((fun pf_helper => + list_rect + (fun prod => + forall (Hreachable : production_is_reachableT G prod) + (str : String) + (len : nat) + (Hlen : length str = len) + (pf : len <= len0), + dec (minimal_parse_of_production (G := G) len0 valid str prod)) + ( + fun Hreachable str len Hlen pf + => match Utils.dec (beq_nat len 0) with + | left H => inl _ + | right H => inr (fun p => _) + end) + (fun it its parse_production' Hreachable str len Hlen pf + => parse_production'_helper + _ + (let parse_item := (fun n pf => parse_item' (parse_nonterminal (take n str) (len := min n len) (eq_trans take_length (f_equal (min _) Hlen)) pf) it) in + let parse_item := (fun n => parse_item n (Min.min_case_strong n len (fun k => k <= len0) (fun Hlen => (Nat.le_trans _ _ _ Hlen pf)) (fun Hlen => pf))) in + let parse_production := (fun n => parse_production' (pf_helper it its Hreachable) (drop n str) (len - n) (eq_trans (drop_length _ _) (f_equal (fun x => x - _) Hlen)) (Nat.le_trans _ _ _ (Nat.le_sub_l _ _) pf)) in + match dec_In + (fun n => dec_prod (parse_item n) (parse_production n)) + (splits it its str) + with + | inl p => inl (existT _ (projT1 p) (snd (projT2 p))) + | inr p + => let pf' := (Nat.le_trans _ _ _ (Nat.eq_le_incl _ _ Hlen) pf) in + let H := (_ : split_list_completeT_for (G := G) (len0 := len0) (valid := valid) it its str pf' (splits it its str)) in + inr (fun p' => p (fst dec_in_helper (H p'))) + end) + )) _); + [ clear parse_nonterminal Hsplits splits rdata cdata + | clear parse_nonterminal Hsplits splits rdata cdata + | .. + | admit ]. + abstract t_parse_production_for. + abstract t_parse_production_for. + abstract t_parse_production_for. + abstract t_parse_production_for. + Defined. diff --git a/test-suite/bugs/closed/4462.v b/test-suite/bugs/closed/4462.v new file mode 100644 index 0000000000..c680518c6a --- /dev/null +++ b/test-suite/bugs/closed/4462.v @@ -0,0 +1,7 @@ +Variables P Q : Prop. +Axiom pqrw : P <-> Q. + +Require Setoid. + +Goal P -> Q. +unshelve (rewrite pqrw). diff --git a/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v new file mode 100644 index 0000000000..6f8631d458 --- /dev/null +++ b/test-suite/bugs/closed/4467.v @@ -0,0 +1,15 @@ +(* Fixing missing test for variable shadowing *) + +Definition test (x y:bool*bool) := + match x with + | (e as e1, (true) as e2) + | ((true) as e1, e as e2) => + let '(e, b) := y in + e + | _ => true + end. + +Goal test (true,false) (true,true) = true. +(* used to evaluate to "false = true" in 8.4 *) +reflexivity. +Qed. diff --git a/test-suite/bugs/closed/4479.v b/test-suite/bugs/closed/4479.v new file mode 100644 index 0000000000..921579d1e1 --- /dev/null +++ b/test-suite/bugs/closed/4479.v @@ -0,0 +1,3 @@ +Goal True. +Fail autorewrite with foo. +try autorewrite with foo. diff --git a/test-suite/bugs/closed/4480.v b/test-suite/bugs/closed/4480.v new file mode 100644 index 0000000000..08a86330f2 --- /dev/null +++ b/test-suite/bugs/closed/4480.v @@ -0,0 +1,12 @@ +Require Import Setoid. + +Definition proj (P Q : Prop) := P. + +Lemma foo (P : Prop) : proj P P = P. +Admitted. +Lemma trueI : True <-> True. +Admitted. +Goal True. + Fail setoid_rewrite foo. + Fail setoid_rewrite trueI. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/4484.v b/test-suite/bugs/closed/4484.v new file mode 100644 index 0000000000..f988539d62 --- /dev/null +++ b/test-suite/bugs/closed/4484.v @@ -0,0 +1,10 @@ +(* Testing 8.5 regression with type classes not solving evars + redefined while trying to solve them with the type class mechanism *) + +Class A := {}. +Axiom foo : forall {ac : A}, bool. +Lemma bar (ac : A) : True. +Check (match foo as k return foo = k -> True with + | true => _ + | false => _ + end eq_refl). diff --git a/test-suite/bugs/closed/4495.v b/test-suite/bugs/closed/4495.v new file mode 100644 index 0000000000..8b032db5f5 --- /dev/null +++ b/test-suite/bugs/closed/4495.v @@ -0,0 +1 @@ +Fail Notation "'forall' x .. y ',' P " := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder). diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v new file mode 100644 index 0000000000..f54d6433d8 --- /dev/null +++ b/test-suite/bugs/closed/4503.v @@ -0,0 +1,37 @@ +Require Coq.Classes.RelationClasses. + +Class PreOrder (A : Type) (r : A -> A -> Type) : Type := +{ refl : forall x, r x x }. + +(* FAILURE 1 *) + +Section foo. + Polymorphic Universes A. + Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + + Fail Definition foo := PO. +End foo. + + +Module ILogic. + +Set Universe Polymorphism. + +(* Logical connectives *) +Class ILogic@{L} (A : Type@{L}) : Type := mkILogic +{ + lentails: A -> A -> Prop; + lentailsPre:> RelationClasses.PreOrder lentails +}. + + +End ILogic. + +Set Printing Universes. + +(* There is stil a problem if the class is universe polymorphic *) +Section Embed_ILogic_Pre. + Polymorphic Universes A T. + Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. + +End Embed_ILogic_Pre.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4511.v b/test-suite/bugs/closed/4511.v new file mode 100644 index 0000000000..0cdb3aee4f --- /dev/null +++ b/test-suite/bugs/closed/4511.v @@ -0,0 +1,3 @@ +Goal True. +Fail evar I. + diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v new file mode 100644 index 0000000000..ccbc47d20f --- /dev/null +++ b/test-suite/bugs/closed/4519.v @@ -0,0 +1,21 @@ +Set Universe Polymorphism. +Section foo. + Universe i. + Context (foo : Type@{i}) (bar : Type@{i}). + Definition qux@{i} (baz : Type@{i}) := foo -> bar. +End foo. +Set Printing Universes. +Print qux. (* qux@{Top.42 Top.43} = +fun foo bar _ : Type@{Top.42} => foo -> bar + : Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} +(* Top.42 Top.43 |= *) +(* This is wrong; the first two types are equal, but the last one is not *) + +qux is universe polymorphic +Argument scopes are [type_scope type_scope type_scope] + *) +Check qux nat nat nat : Set. +Check qux nat nat Set : Set. (* Error: +The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is +expected to have type "Set" +(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v new file mode 100644 index 0000000000..ae17fb145d --- /dev/null +++ b/test-suite/bugs/closed/4533.v @@ -0,0 +1,226 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) +(* File reduced by coq-bug-finder from original input, then from 1125 lines to +346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, +then from 285 lines to 271 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml +4.01.0 + coqtop version 8.5 (January 2016) *) +Inductive False := . +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Init.Datatypes. +Import Coq.Init.Notations. +Global Set Universe Polymorphism. +Global Set Primitive Projections. +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Module Export Datatypes. + Set Implicit Arguments. + Notation nat := Coq.Init.Datatypes.nat. + Notation S := Coq.Init.Datatypes.S. + Record prod (A B : Type) := pair { fst : A ; snd : B }. + Notation "x * y" := (prod x y) : type_scope. + Delimit Scope nat_scope with nat. + Open Scope nat_scope. +End Datatypes. +Module Export Specif. + Set Implicit Arguments. + Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P +proj1_sig }. + Notation sigT := sig (only parsing). + Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. + Notation projT1 := proj1_sig (only parsing). + Notation projT2 := proj2_sig (only parsing). +End Specif. +Global Set Keyed Unification. +Global Unset Strict Universe Declaration. +Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. +Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in +Type@{i}. +Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in + let ge := ((fun x => x) : Type1@{j} -> +Type@{i}) in Type@{i}. +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Open Scope fibration_scope. +Open Scope function_scope. +Notation pr1 := projT1. +Notation pr2 := projT2. +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. +Notation compose := (fun g f x => g (f x)). +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left +associativity) : 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 + := match p with idpath => idpath end. +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%path q%path) (at level 20) : path_scope. +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +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 eissect {A B}%type_scope f%function_scope {_} _. +Inductive Unit : Type1 := tt : Unit. +Local Open Scope path_scope. +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. +Section Adjointify. + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). + admit. + Defined. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. +End Adjointify. +Definition ExtensionAlong {A B : Type} (f : A -> B) + (P : B -> Type) (d : forall x:A, P (f x)) + := { s : forall y:B, P y & forall x:A, s (f x) = d x }. +Fixpoint ExtendableAlong@{i j k l} + (n : nat) {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := match n with + | 0 => Unit@{l} + | S n => (forall (g : forall a, C (f a)), + ExtensionAlong@{i j k l l} f C g) * + forall (h k : forall b, C b), + ExtendableAlong n f (fun b => h b = k b) + end. + +Definition ooExtendableAlong@{i j k l} + {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := forall n, ExtendableAlong@{i j k l} n f C. + +Module Type ReflectiveSubuniverses. + + Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : +Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). + +End ReflectiveSubuniverses. + +Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). + Export Os. + Existing Class In. + Module Export Coercions. + Coercion O_reflector : ReflectiveSubuniverse >-> Funclass. + End Coercions. + Global Existing Instance O_inO. + + Section ORecursion. + Context {O : ReflectiveSubuniverse}. + + Definition O_rec {P Q : Type} {Q_inO : In O Q} + (f : P -> Q) + : O P -> Q + := (fst (extendable_to_O O 1%nat) f).1. + + Definition O_rec_beta {P Q : Type} {Q_inO : In O Q} + (f : P -> Q) (x : P) + : O_rec f (to O P x) = f x + := (fst (extendable_to_O O 1%nat) f).2 x. + + Definition O_indpaths {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o to O P == h o to O P) + : g == h + := (fst (snd (extendable_to_O O 2) g h) p).1. + + End ORecursion. + + + Section Reflective_Subuniverse. + Context (O : ReflectiveSubuniverse@{Ou Oa}). + + Definition isequiv_to_O_inO@{u a i} (T : Type@{i}) `{In@{u a i} O T} : +IsEquiv@{i i} (to O T). + Proof. + + pose (g := O_rec@{u a i i i i i} idmap). + refine (isequiv_adjointify (to O T) g _ _). + - + refine (O_indpaths@{u a i i i i i} (to O T o g) idmap _). + intros x. + apply ap. + apply O_rec_beta. + - + intros x. + apply O_rec_beta. + Defined. + Global Existing Instance isequiv_to_O_inO. + + End Reflective_Subuniverse. + +End ReflectiveSubuniverses_Theory. + +Module Type Preserves_Fibers (Os : ReflectiveSubuniverses). + Module Export Os_Theory := ReflectiveSubuniverses_Theory Os. +End Preserves_Fibers. + +Opaque eissect. +Module Lex_Reflective_Subuniverses + (Os : ReflectiveSubuniverses) (Opf : Preserves_Fibers Os). + Import Opf. + Goal forall (O : ReflectiveSubuniverse) (A : Type) (B : A -> Type) (A_inO : +In O A), + + forall g, + forall (x : O {x : A & B x}) v v' v'' (p2 : v'' = v') (p0 : v' = v) (p1 : +v = _) r, + (p2 + @ (p0 + @ p1)) + @ eissect (to O A) (g x) = r. + intros. + cbv zeta. + rewrite concat_p_pp. + match goal with + | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good" + | [ |- ?G ] => fail 1 "bad" G + end. + Fail rewrite concat_p_pp.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v new file mode 100644 index 0000000000..d14cc86fc7 --- /dev/null +++ b/test-suite/bugs/closed/4544.v @@ -0,0 +1,1007 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 + coqtop version 8.5 (January 2016) *) +Inductive False := . +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Init.Datatypes. + +Import Coq.Init.Notations. + +Global Set Universe Polymorphism. + +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Global Set Primitive Projections. + +Inductive sum (A B : Type) : Type := + | inl : A -> sum A B + | inr : B -> sum A B. +Notation nat := Coq.Init.Datatypes.nat. +Notation S := Coq.Init.Datatypes.S. +Notation "x + y" := (sum x y) : type_scope. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. + +Notation "x * y" := (prod x y) : type_scope. +Module Export Specif. + +Set Implicit Arguments. + +Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }. +Arguments proj1_sig {A P} _ / . + +Notation sigT := sig (only parsing). +Notation existT := exist (only parsing). + +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. + +Notation projT1 := proj1_sig (only parsing). +Notation projT2 := proj2_sig (only parsing). + +End Specif. +Module Export HoTT_DOT_Basics_DOT_Overture. +Module Export HoTT. +Module Export Basics. +Module Export Overture. + +Global Set Keyed Unification. + +Global Unset Strict Universe Declaration. + +Notation Type0 := Set. + +Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in Type@{i}. + +Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in + let ge := ((fun x => x) : Type1@{j} -> Type@{i}) in Type@{i}. + +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Delimit Scope trunc_scope with trunc. + +Open Scope trunc_scope. +Open Scope path_scope. +Open Scope fibration_scope. +Open Scope nat_scope. +Open Scope function_scope. + +Notation "( x ; y )" := (existT _ x y) : fibration_scope. + +Notation pr1 := projT1. +Notation pr2 := projT2. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : 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 + := match p with idpath => idpath end. + +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%path q%path) (at level 20) : path_scope. + +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. + +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := + match p with idpath => u end. + +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 + := match p with idpath => idpath end. + +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}%type_scope f%function_scope {_} _. + +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) : type_scope. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Arguments center A {_}. + +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. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. +Notation "0" := (-1.+1) : 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. + +Global Instance istrunc_paths (A : Type) n `{H : IsTrunc n.+1 A} (x y : A) +: IsTrunc n (x = y) + := H x y. + +Notation Contr := (IsTrunc -2). +Notation IsHProp := (IsTrunc -1). + +Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances. + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Inductive Unit : Type1 := + tt : Unit. + +Class IsPointed (A : Type) := point : A. + +Arguments point A {_}. + +Record pType := + { pointed_type : Type ; + ispointed_type : IsPointed pointed_type }. + +Coercion pointed_type : pType >-> Sortclass. + +Global Existing Instance ispointed_type. + +Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }. + +Ltac revert_opaque x := + revert x; + match goal with + | [ |- forall _, _ ] => idtac + | _ => fail 1 "Reverted constant is not an opaque variable" + end. + +End Overture. + +End Basics. + +End HoTT. + +End HoTT_DOT_Basics_DOT_Overture. +Module Export HoTT_DOT_Basics_DOT_PathGroupoids. +Module Export HoTT. +Module Export Basics. +Module Export PathGroupoids. + +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 concat_pV {A : Type} {x y : A} (p : x = y) : + p @ p^ = 1 + := + match p with idpath => 1 end. + +Definition moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) : + p = r @ q -> r^ @ p = q. +admit. +Defined. + +Definition moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) : + r @ q = p -> q = r^ @ p. +admit. +Defined. + +Definition moveR_M1 {A : Type} {x y : A} (p q : x = y) : + 1 = p^ @ q -> p = q. +admit. +Defined. + +Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) : + ap f (p @ q) = (ap f p) @ (ap f q) + := + match q with + idpath => + match p with idpath => 1 end + end. + +Definition ap_V {A B : Type} (f : A -> B) {x y : A} (p : x = y) : + ap f (p^) = (ap f p)^ + := + match p with idpath => 1 end. + +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_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A} (q : x = y) : + (p x) @ (ap f q) = q @ (p y) + := + match q as i in (_ = y) return (p x @ ap f i = i @ p y) with + | idpath => concat_p1 _ @ (concat_1p _)^ + end. + +End PathGroupoids. + +End Basics. + +End HoTT. + +End HoTT_DOT_Basics_DOT_PathGroupoids. +Module Export HoTT_DOT_Basics_DOT_Equivalences. +Module Export HoTT. +Module Export Basics. +Module Export Equivalences. + +Definition isequiv_commsq {A B C D} + (f : A -> B) (g : C -> D) (h : A -> C) (k : B -> D) + (p : k o f == g o h) + `{IsEquiv _ _ f} `{IsEquiv _ _ h} `{IsEquiv _ _ k} +: IsEquiv g. +admit. +Defined. + +Section Adjointify. + + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). + Proof. + unfold issect'. + apply moveR_M1. + repeat rewrite ap_pp, concat_p_pp; rewrite <- ap_compose. + rewrite (concat_pA1 (fun b => (isretr b)^) (ap f (issect a)^)). + repeat rewrite concat_pp_p; rewrite ap_V; apply moveL_Vp; rewrite concat_p1. + rewrite concat_p_pp, <- ap_compose. + rewrite (concat_pA1 (fun b => (isretr b)^) (isretr (f a))). + rewrite concat_pV, concat_1p; reflexivity. + Qed. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. + +End Adjointify. + +End Equivalences. + +End Basics. + +End HoTT. + +End HoTT_DOT_Basics_DOT_Equivalences. +Module Export HoTT_DOT_Basics_DOT_Trunc. +Module Export HoTT. +Module Export Basics. +Module Export Trunc. +Generalizable Variables A B m n f. + +Definition trunc_equiv A {B} (f : A -> B) + `{IsTrunc n A} `{IsEquiv A B f} + : IsTrunc n B. +admit. +Defined. + +Record TruncType (n : trunc_index) := BuildTruncType { + trunctype_type : Type ; + istrunc_trunctype_type : IsTrunc n trunctype_type +}. + +Arguments BuildTruncType _ _ {_}. + +Coercion trunctype_type : TruncType >-> Sortclass. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (-1)-Type. + +Notation BuildhProp := (BuildTruncType -1). + +End Trunc. + +End Basics. + +End HoTT. + +End HoTT_DOT_Basics_DOT_Trunc. +Module Export HoTT_DOT_Types_DOT_Unit. +Module Export HoTT. +Module Export Types. +Module Export Unit. + +Notation unit_name x := (fun (_ : Unit) => x). + +End Unit. + +End Types. + +End HoTT. + +End HoTT_DOT_Types_DOT_Unit. +Module Export HoTT_DOT_Types_DOT_Sigma. +Module Export HoTT. +Module Export Types. +Module Export Sigma. +Local Open Scope path_scope. + +Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) + (pq : {p : u.1 = v.1 & p # u.2 = v.2}) +: u = v + := match pq.2 in (_ = v2) return u = (v.1; v2) with + | 1 => match pq.1 as p in (_ = v1) return u = (v1; p # u.2) with + | 1 => 1 + end + end. + +Definition path_sigma {A : Type} (P : A -> Type) (u v : sigT P) + (p : u.1 = v.1) (q : p # u.2 = v.2) +: u = v + := path_sigma_uncurried P u v (p;q). + +Definition path_sigma' {A : Type} (P : A -> Type) {x x' : A} {y : P x} {y' : P x'} + (p : x = x') (q : p # y = y') +: (x;y) = (x';y') + := path_sigma P (x;y) (x';y') p q. + +Global Instance isequiv_pr1_contr {A} {P : A -> Type} + `{forall a, Contr (P a)} +: IsEquiv (@pr1 A P) | 100. +Proof. + refine (isequiv_adjointify (@pr1 A P) + (fun a => (a ; center (P a))) _ _). + - + intros a; reflexivity. + - + intros [a p]. + refine (path_sigma' P 1 (contr _)). +Defined. + +Definition path_sigma_hprop {A : Type} {P : A -> Type} + `{forall x, IsHProp (P x)} + (u v : sigT P) +: u.1 = v.1 -> u = v + := path_sigma_uncurried P u v o pr1^-1. + +End Sigma. + +End Types. + +End HoTT. + +End HoTT_DOT_Types_DOT_Sigma. +Module Export HoTT_DOT_Extensions. +Module Export HoTT. +Module Export Extensions. + +Section Extensions. + + Definition ExtensionAlong {A B : Type} (f : A -> B) + (P : B -> Type) (d : forall x:A, P (f x)) + := { s : forall y:B, P y & forall x:A, s (f x) = d x }. + + Fixpoint ExtendableAlong@{i j k l} + (n : nat) {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := match n with + | 0 => Unit@{l} + | S n => (forall (g : forall a, C (f a)), + ExtensionAlong@{i j k l l} f C g) * + forall (h k : forall b, C b), + ExtendableAlong n f (fun b => h b = k b) + end. + + Definition ooExtendableAlong@{i j k l} + {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := forall n, ExtendableAlong@{i j k l} n f C. + +End Extensions. + +End Extensions. + +End HoTT. + +End HoTT_DOT_Extensions. +Module Export HoTT. +Module Export Modalities. +Module Export ReflectiveSubuniverse. + +Module Type ReflectiveSubuniverses. + + Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + + let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In@{u a j} O U. + + Parameter hprop_inO@{u a i} + : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + IsHProp (In@{u a i} O T). + + Parameter extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). + +End ReflectiveSubuniverses. + +Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). +Export Os. + +Module Export Coercions. + + Coercion O_reflector : ReflectiveSubuniverse >-> Funclass. + +End Coercions. + +End ReflectiveSubuniverses_Theory. + +Module Type ReflectiveSubuniverses_Restriction_Data (Os : ReflectiveSubuniverses). + + Parameter New_ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter ReflectiveSubuniverses_restriction@{u a} + : New_ReflectiveSubuniverse@{u a} -> Os.ReflectiveSubuniverse@{u a}. + +End ReflectiveSubuniverses_Restriction_Data. + +Module ReflectiveSubuniverses_Restriction + (Os : ReflectiveSubuniverses) + (Res : ReflectiveSubuniverses_Restriction_Data Os) +<: ReflectiveSubuniverses. + + Definition ReflectiveSubuniverse := Res.New_ReflectiveSubuniverse. + + Definition O_reflector@{u a i} (O : ReflectiveSubuniverse@{u a}) + := Os.O_reflector@{u a i} (Res.ReflectiveSubuniverses_restriction O). + Definition In@{u a i} (O : ReflectiveSubuniverse@{u a}) + := Os.In@{u a i} (Res.ReflectiveSubuniverses_restriction O). + Definition O_inO@{u a i} (O : ReflectiveSubuniverse@{u a}) + := Os.O_inO@{u a i} (Res.ReflectiveSubuniverses_restriction O). + Definition to@{u a i} (O : ReflectiveSubuniverse@{u a}) + := Os.to@{u a i} (Res.ReflectiveSubuniverses_restriction O). + Definition inO_equiv_inO@{u a i j k} (O : ReflectiveSubuniverse@{u a}) + := Os.inO_equiv_inO@{u a i j k} (Res.ReflectiveSubuniverses_restriction O). + Definition hprop_inO@{u a i} (H : Funext) (O : ReflectiveSubuniverse@{u a}) + := Os.hprop_inO@{u a i} H (Res.ReflectiveSubuniverses_restriction O). + Definition extendable_to_O@{u a i j k} (O : ReflectiveSubuniverse@{u a}) + := @Os.extendable_to_O@{u a i j k} (Res.ReflectiveSubuniverses_restriction@{u a} O). + +End ReflectiveSubuniverses_Restriction. + +Module ReflectiveSubuniverses_FamUnion + (Os1 Os2 : ReflectiveSubuniverses) +<: ReflectiveSubuniverses. + + Definition ReflectiveSubuniverse@{u a} : Type2@{u a} + := Os1.ReflectiveSubuniverse@{u a} + Os2.ReflectiveSubuniverse@{u a}. + + Definition O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. +admit. +Defined. + + Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + Proof. + intros [O|O]; [ exact (Os1.In@{u a i} O) + | exact (Os2.In@{u a i} O) ]. + Defined. + + Definition O_inO@{u a i} + : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). +admit. +Defined. + + Definition to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + T -> O_reflector@{u a i} O T. +admit. +Defined. + + Definition inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + In@{u a j} O U. + Proof. + intros [O|O]; [ exact (Os1.inO_equiv_inO@{u a i j k} O) + | exact (Os2.inO_equiv_inO@{u a i j k} O) ]. + Defined. + + Definition hprop_inO@{u a i} + : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + IsHProp (In@{u a i} O T). +admit. +Defined. + + Definition extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). +admit. +Defined. + +End ReflectiveSubuniverses_FamUnion. + +End ReflectiveSubuniverse. + +End Modalities. + +End HoTT. + +Module Type Modalities. + + Parameter Modality@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : Modality@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : Modality@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter inO_equiv_inO@{u a i j k} : + forall (O : Modality@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + + let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In@{u a j} O U. + + Parameter hprop_inO@{u a i} + : Funext -> forall (O : Modality@{u a}) (T : Type@{i}), + IsHProp (In@{u a i} O T). + +End Modalities. + +Module Modalities_to_ReflectiveSubuniverses + (Os : Modalities) <: ReflectiveSubuniverses. + + Import Os. + + Fixpoint O_extendable@{u a i j k} (O : Modality@{u a}) + (A : Type@{i}) (B : O_reflector O A -> Type@{j}) + (B_inO : forall a, In@{u a j} O (B a)) (n : nat) + : ExtendableAlong@{i i j k} n (to O A) B. +admit. +Defined. + + Definition ReflectiveSubuniverse := Modality. + + Definition O_reflector := O_reflector. + + Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a} + := In@{u a i}. + Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T) + := O_inO@{u a i}. + Definition to := to. + Definition inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + In@{u a j} O U + := inO_equiv_inO@{u a i j k}. + Definition hprop_inO@{u a i} + : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + IsHProp (In@{u a i} O T) + := hprop_inO@{u a i}. + + Definition extendable_to_O@{u a i j k} (O : ReflectiveSubuniverse@{u a}) + {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q} + : ooExtendableAlong@{i i j k} (to O P) (fun _ => Q) + := fun n => O_extendable O P (fun _ => Q) (fun _ => Q_inO) n. + +End Modalities_to_ReflectiveSubuniverses. + +Module Type EasyModalities. + + Parameter Modality@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : Modality@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter to@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter minO_pathsO@{u a i} + : forall (O : Modality@{u a}) (A : Type@{i}) + (z z' : O_reflector@{u a i} O A), + IsEquiv (to@{u a i} O (z = z')). + +End EasyModalities. + +Module EasyModalities_to_Modalities (Os : EasyModalities) +<: Modalities. + + Import Os. + + Definition Modality := Modality. + + Definition O_reflector@{u a i} := O_reflector@{u a i}. + Definition to@{u a i} := to@{u a i}. + + Definition In@{u a i} + : forall (O : Modality@{u a}), Type@{i} -> Type@{i} + := fun O A => IsEquiv@{i i} (to O A). + + Definition hprop_inO@{u a i} `{Funext} (O : Modality@{u a}) + (T : Type@{i}) + : IsHProp (In@{u a i} O T). +admit. +Defined. + + Definition O_ind_internal@{u a i j k} (O : Modality@{u a}) + (A : Type@{i}) (B : O_reflector@{u a i} O A -> Type@{j}) + (B_inO : forall oa, In@{u a j} O (B oa)) + : let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + (forall a, B (to O A a)) -> forall oa, B oa. +admit. +Defined. + + Definition O_ind_beta_internal@{u a i j k} (O : Modality@{u a}) + (A : Type@{i}) (B : O_reflector@{u a i} O A -> Type@{j}) + (B_inO : forall oa, In@{u a j} O (B oa)) + (f : forall a : A, B (to O A a)) (a:A) + : O_ind_internal@{u a i j k} O A B B_inO f (to O A a) = f a. +admit. +Defined. + + Definition O_inO@{u a i} (O : Modality@{u a}) (A : Type@{i}) + : In@{u a i} O (O_reflector@{u a i} O A). +admit. +Defined. + + Definition inO_equiv_inO@{u a i j k} (O : Modality@{u a}) (A : Type@{i}) (B : Type@{j}) + (A_inO : In@{u a i} O A) (f : A -> B) (feq : IsEquiv f) + : In@{u a j} O B. + Proof. + simple refine (isequiv_commsq (to O A) (to O B) f + (O_ind_internal O A (fun _ => O_reflector O B) _ (fun a => to O B (f a))) _). + - + intros; apply O_inO. + - + intros a; refine (O_ind_beta_internal@{u a i j k} O A (fun _ => O_reflector O B) _ _ a). + - + apply A_inO. + - + simple refine (isequiv_adjointify _ + (O_ind_internal O B (fun _ => O_reflector O A) _ (fun b => to O A (f^-1 b))) _ _); + intros x. + + + apply O_inO. + + + pattern x; refine (O_ind_internal O B _ _ _ x); intros. + * + apply minO_pathsO. + * + simpl; admit. + + + pattern x; refine (O_ind_internal O A _ _ _ x); intros. + * + apply minO_pathsO. + * + simpl; admit. + Defined. + +End EasyModalities_to_Modalities. + +Module Modalities_Theory (Os : Modalities). + +Export Os. +Module Export Os_ReflectiveSubuniverses + := Modalities_to_ReflectiveSubuniverses Os. +Module Export RSU + := ReflectiveSubuniverses_Theory Os_ReflectiveSubuniverses. + +Module Export Coercions. + Coercion modality_to_reflective_subuniverse + := idmap : Modality -> ReflectiveSubuniverse. +End Coercions. + +Class IsConnected (O : Modality@{u a}) (A : Type@{i}) + + := isconnected_contr_O : IsTrunc@{i} -2 (O A). + +Class IsConnMap (O : Modality@{u a}) + {A : Type@{i}} {B : Type@{j}} (f : A -> B) + := isconnected_hfiber_conn_map + + : forall b:B, IsConnected@{u a k} O (hfiber@{i j} f b). + +End Modalities_Theory. + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + +Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i}) +: IsTrunc@{j} n (Trunc@{i} n A). +Admitted. + +Definition Trunc_ind {n A} + (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} + : (forall a, P (tr a)) -> (forall aa, P aa) +:= (fun f aa => match aa with tr a => fun _ => f a end Pt). + +Definition Truncation_Modality := trunc_index. + +Module Truncation_Modalities <: Modalities. + + Definition Modality : Type2@{u a} := Truncation_Modality. + + Definition O_reflector (n : Modality@{u u'}) A := Trunc n A. + + Definition In (n : Modality@{u u'}) A := IsTrunc n A. + + Definition O_inO (n : Modality@{u u'}) A : In n (O_reflector n A). +admit. +Defined. + + Definition to (n : Modality@{u u'}) A := @tr n A. + + Definition inO_equiv_inO (n : Modality@{u u'}) + (A : Type@{i}) (B : Type@{j}) Atr f feq + : let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In n B + := @trunc_equiv A B f n Atr feq. + + Definition hprop_inO `{Funext} (n : Modality@{u u'}) A + : IsHProp (In n A). +admit. +Defined. + +End Truncation_Modalities. + +Module Import TrM := Modalities_Theory Truncation_Modalities. + +Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). + +Notation IsSurjection := (IsConnMap -1). + +Definition BuildIsSurjection {A B} (f : A -> B) : + (forall b, merely (hfiber f b)) -> IsSurjection f. +admit. +Defined. + +Ltac strip_truncations := + + progress repeat match goal with + | [ T : _ |- _ ] + => revert_opaque T; + refine (@Trunc_ind _ _ _ _ _); + + []; + intro T + end. +Local Open Scope trunc_scope. + +Global Instance conn_pointed_type {n : trunc_index} {A : Type} (a0:A) + `{IsConnMap n _ _ (unit_name a0)} : IsConnected n.+1 A | 1000. +admit. +Defined. + +Definition loops (A : pType) : pType := + Build_pType (point A = point A) idpath. + +Record pMap (A B : pType) := + { pointed_fun : A -> B ; + point_eq : pointed_fun (point A) = point B }. + +Arguments point_eq {A B} f : rename. +Coercion pointed_fun : pMap >-> Funclass. + +Infix "->*" := pMap (at level 99) : pointed_scope. +Local Open Scope pointed_scope. + +Definition pmap_compose {A B C : pType} + (g : B ->* C) (f : A ->* B) +: A ->* C + := Build_pMap A C (g o f) + (ap g (point_eq f) @ point_eq g). + +Record pHomotopy {A B : pType} (f g : pMap A B) := + { pointed_htpy : f == g ; + point_htpy : pointed_htpy (point A) @ point_eq g = point_eq f }. +Arguments pointed_htpy {A B f g} p x. + +Infix "==*" := pHomotopy (at level 70, no associativity) : pointed_scope. + +Definition loops_functor {A B : pType} (f : A ->* B) +: (loops A) ->* (loops B). +Proof. + refine (Build_pMap (loops A) (loops B) + (fun p => (point_eq f)^ @ (ap f p @ point_eq f)) _). + apply moveR_Vp; simpl. + refine (concat_1p _ @ (concat_p1 _)^). +Defined. + +Definition loops_functor_compose {A B C : pType} + (g : B ->* C) (f : A ->* B) +: (loops_functor (pmap_compose g f)) + ==* (pmap_compose (loops_functor g) (loops_functor f)). +admit. +Defined. + +Local Open Scope path_scope. + +Record ooGroup := + { classifying_space : pType@{i} ; + isconn_classifying_space : IsConnected@{u a i} 0 classifying_space + }. + +Local Notation B := classifying_space. + +Definition group_type (G : ooGroup) : Type + := point (B G) = point (B G). + +Coercion group_type : ooGroup >-> Sortclass. + +Definition group_loops (X : pType) +: ooGroup. +Proof. + + pose (x0 := point X); + pose (BG := (Build_pType + { x:X & merely (x = point X) } + (existT (fun x:X => merely (x = point X)) x0 (tr 1)))). + + cut (IsConnected 0 BG). + { + exact (Build_ooGroup BG). +} + cut (IsSurjection (unit_name (point BG))). + { + intros; refine (conn_pointed_type (point _)). +} + apply BuildIsSurjection; simpl; intros [x p]. + strip_truncations; apply tr; exists tt. + apply path_sigma_hprop; simpl. + exact (p^). +Defined. + +Definition loops_group (X : pType) +: loops X <~> group_loops X. +admit. +Defined. + +Definition ooGroupHom (G H : ooGroup) + := pMap (B G) (B H). + +Definition grouphom_fun {G H} (phi : ooGroupHom G H) : G -> H + := loops_functor phi. + +Coercion grouphom_fun : ooGroupHom >-> Funclass. + +Definition group_loops_functor + {X Y : pType} (f : pMap X Y) +: ooGroupHom (group_loops X) (group_loops Y). +Proof. + simple refine (Build_pMap _ _ _ _); simpl. + - + intros [x p]. + exists (f x). + strip_truncations; apply tr. + exact (ap f p @ point_eq f). + - + apply path_sigma_hprop; simpl. + apply point_eq. +Defined. + +Definition loops_functor_group + {X Y : pType} (f : pMap X Y) +: loops_functor (group_loops_functor f) o loops_group X + == loops_group Y o loops_functor f. +admit. +Defined. + +Definition grouphom_compose {G H K : ooGroup} + (psi : ooGroupHom H K) (phi : ooGroupHom G H) +: ooGroupHom G K + := pmap_compose psi phi. + +Definition group_loops_functor_compose + {X Y Z : pType} + (psi : pMap Y Z) (phi : pMap X Y) +: grouphom_compose (group_loops_functor psi) (group_loops_functor phi) + == group_loops_functor (pmap_compose psi phi). +Proof. + intros g. + unfold grouphom_fun, grouphom_compose. + refine (pointed_htpy (loops_functor_compose _ _) g @ _). + pose (p := eisretr (loops_group X) g). + change (loops_functor (group_loops_functor psi) + (loops_functor (group_loops_functor phi) g) + = loops_functor (group_loops_functor + (pmap_compose psi phi)) g). + rewrite <- p. + Fail Timeout 1 Time rewrite !loops_functor_group. + (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *) + Timeout 1 do 3 rewrite loops_functor_group. +Abort.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4574.v b/test-suite/bugs/closed/4574.v new file mode 100644 index 0000000000..39ba190369 --- /dev/null +++ b/test-suite/bugs/closed/4574.v @@ -0,0 +1,8 @@ +Require Import Setoid. + +Definition block A (a : A) := a. + +Goal forall A (a : A), block Type nat. +Proof. +Fail reflexivity. + diff --git a/test-suite/bugs/closed/4580.v b/test-suite/bugs/closed/4580.v new file mode 100644 index 0000000000..4ffd5f0f4b --- /dev/null +++ b/test-suite/bugs/closed/4580.v @@ -0,0 +1,6 @@ +Require Import Program. + +Class Foo (A : Type) := foo : A. + +Unset Refine Instance Mode. +Program Instance f1 : Foo nat := S _. diff --git a/test-suite/bugs/closed/4582.v b/test-suite/bugs/closed/4582.v new file mode 100644 index 0000000000..0842fb8fa7 --- /dev/null +++ b/test-suite/bugs/closed/4582.v @@ -0,0 +1,10 @@ +Require List. +Import List.ListNotations. + +Variable Foo : nat -> nat. + +Delimit Scope Foo_scope with F. + +Notation " [ x ] " := (Foo x) : Foo_scope. + +Check ([1] : nat)%F. diff --git a/test-suite/bugs/closed/4588.v b/test-suite/bugs/closed/4588.v new file mode 100644 index 0000000000..ff66277e03 --- /dev/null +++ b/test-suite/bugs/closed/4588.v @@ -0,0 +1,10 @@ +Set Primitive Projections. + +(* This proof was accepted in Coq 8.5 because the subterm specs were not +projected correctly *) +Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }. + +Fail Fixpoint loop (x : foo) : False := + loop (proj2 x _ x). + +Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)). diff --git a/test-suite/bugs/closed/4596.v b/test-suite/bugs/closed/4596.v new file mode 100644 index 0000000000..592fdb6580 --- /dev/null +++ b/test-suite/bugs/closed/4596.v @@ -0,0 +1,14 @@ +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. + +Definition T (x : bool) := x = true. + +Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat) + (s : forall n : nat, bool) + (s0 s1 : nat -> S -> S), + (forall (str0 : S) (n m : nat), + (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) -> + T (b str0 m)) -> + T (b str p). +Proof. +intros ???????? H0. +rewrite H0. diff --git a/test-suite/bugs/closed/4627.v b/test-suite/bugs/closed/4627.v new file mode 100644 index 0000000000..e1206bb37a --- /dev/null +++ b/test-suite/bugs/closed/4627.v @@ -0,0 +1,49 @@ +Class sa (A:Type) := { }. + +Record predicate A (sa:sa A) := + { pred_fun: A->Prop }. +Record ABC : Type := + { abc: Type }. +Record T := + { T_abc: ABC }. + + +(* +sa: forall _ : Type@{Top.179}, Prop +predicate: forall (A : Type@{Top.205}) (_ : sa A), Type@{max(Set+1, Top.205)} +T: Type@{Top.208+1} +ABC: Type@{Top.208+1} +abc: forall _ : ABC, Type@{Top.208} + +Top.205 <= Top.179 predicate <= sa.A +Set < Top.208 Set < abc +Set < Top.205 Set < predicate +*) + +Definition foo : predicate T (Build_sa T) := + {| pred_fun:= fun w => True |}. +(* *) +(* Top.208 < Top.205 <--- added by foo *) +(* *) + +Check predicate nat (Build_sa nat). +(* + +The issue is that the template polymorphic universe of [predicate], Top.205, does not get replaced with the universe of [nat] in the above line. + -Jason Gross + +8.5 -- predicate nat (Build_sa nat): Type@{max(Set+1, Top.205)} +8.5 EXPECTED -- predicate nat (Build_sa nat): Type@{Set+1} +8.4pl4 -- predicate nat {| |}: Type (* max(Set, (Set)+1) *) +*) + +(* This works in 8.4pl4 and SHOULD work in 8.5 *) +Definition bar : ABC := + {| abc:= predicate nat (Build_sa nat) |}. +(* +The term "predicate nat (Build_sa nat)" has type + "Type@{max(Set+1, Top.205)}" +while it is expected to have type "Type@{Top.208}" +(universe inconsistency: Cannot enforce Top.205 <= +Top.208 because Top.208 < Top.205). +*)
\ No newline at end of file diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v index e86b3be64e..ea3347a851 100644 --- a/test-suite/bugs/closed/931.v +++ b/test-suite/bugs/closed/931.v @@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop. Goal Prop. refine (P _ _). - 2:instantiate (1:=0). + instantiate (1:=0). trivial. Qed. diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v index ba69f6b158..dba4d5998f 100644 --- a/test-suite/bugs/closed/HoTT_coq_002.v +++ b/test-suite/bugs/closed/HoTT_coq_002.v @@ -9,7 +9,7 @@ Section SpecializedFunctor. (* Variable objC : Type. *) Context `(C : SpecializedCategory objC). - Polymorphic Record SpecializedFunctor := { + Record SpecializedFunctor := { ObjectOf' : objC -> Type; ObjectC : Object C }. diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v index 0b8bb23534..844ff87566 100644 --- a/test-suite/bugs/closed/HoTT_coq_007.v +++ b/test-suite/bugs/closed/HoTT_coq_007.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. Module Comment1. Set Implicit Arguments. diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v index ae3e50d7ee..223a98de1c 100644 --- a/test-suite/bugs/closed/HoTT_coq_014.v +++ b/test-suite/bugs/closed/HoTT_coq_014.v @@ -3,9 +3,9 @@ Set Implicit Arguments. Generalizable All Variables. Set Universe Polymorphism. -Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' { - Object :> _ := obj; - Morphism' : obj -> obj -> Type; +Polymorphic Record SpecializedCategory@{l k} (obj : Type@{l}) := Build_SpecializedCategory' { + Object :> Type@{l} := obj; + Morphism' : obj -> obj -> Type@{k}; Identity' : forall o, Morphism' o o; Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d' diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 4938b80f9b..008fb72c4e 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -59,8 +59,8 @@ Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C := Build_Functor Cat0 C (fun x => match x with end). Section Law0. - Variable objC : Type. - Variable C : Category objC. + Polymorphic Variable objC : Type. + Polymorphic Variable C : Category objC. Set Printing All. Set Printing Universes. diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v index 4c3e078a50..7a84531a77 100644 --- a/test-suite/bugs/closed/HoTT_coq_036.v +++ b/test-suite/bugs/closed/HoTT_coq_036.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Module Version1. Set Implicit Arguments. Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v index a14fb6aa57..e2bf1dbedb 100644 --- a/test-suite/bugs/closed/HoTT_coq_053.v +++ b/test-suite/bugs/closed/HoTT_coq_053.v @@ -39,7 +39,7 @@ Definition NatCategory (n : nat) := Definition NatCategory' (n : nat) := match n with | 0 => (fun X => @Build_PreCategory X - (fun _ _ => Unit : Prop)) Unit + (fun _ _ => Unit : Set)) Unit | _ => DiscreteCategory Bool end. diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v index b7db22a69e..90d1d18306 100644 --- a/test-suite/bugs/closed/HoTT_coq_062.v +++ b/test-suite/bugs/closed/HoTT_coq_062.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. Require Import TestSuite.admit. (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *) (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *) diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index db3b60edae..017780c1f3 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -30,7 +30,7 @@ Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B) (p : prod A B) : P p := u (fst p) (snd p). -Notation typeof x := ($(let T := type of x in exact T)$) (only parsing). +Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing). (* Check for eta *) Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect'). diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v index 5fa167038d..d77b9b63a2 100644 --- a/test-suite/bugs/closed/HoTT_coq_090.v +++ b/test-suite/bugs/closed/HoTT_coq_090.v @@ -84,7 +84,7 @@ Arguments transport {A} P {x y} p%path_scope u : simpl nomatch. Instance isequiv_path {A B : Type} (p : A = B) : IsEquiv (transport (fun X:Type => X) p) | 0. Proof. - refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _); + unshelve refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _); admit. Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v index 38943ab353..4f8868d538 100644 --- a/test-suite/bugs/closed/HoTT_coq_093.v +++ b/test-suite/bugs/closed/HoTT_coq_093.v @@ -1,3 +1,4 @@ +Unset Strict Universe Declaration. (** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *) Set Printing All. Set Printing Implicit. @@ -21,7 +22,7 @@ Section lift. Definition Lift (A : Type@{i}) : Type@{j} := A. End lift. -Goal forall (A : Type@{i}) (x y : A), @paths@{i} A x y -> @paths@{j} A x y. +Goal forall (A : Type@{i}) (x y : A), @paths@{i j} A x y -> @paths@{j k} A x y. intros A x y p. compute in *. destruct p. exact idpath. Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v index 4f5ef99740..b6c0da76ba 100644 --- a/test-suite/bugs/closed/HoTT_coq_108.v +++ b/test-suite/bugs/closed/HoTT_coq_108.v @@ -107,7 +107,7 @@ Section path_functor. Variable D : PreCategory. Local Notation path_functor'_T F G := { HO : object_of F = object_of G - | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d)) + & transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d)) HO (morphism_of F) = morphism_of G } diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v index 341128338e..3535e6c41f 100644 --- a/test-suite/bugs/closed/HoTT_coq_114.v +++ b/test-suite/bugs/closed/HoTT_coq_114.v @@ -1 +1 @@ -Inductive test : $(let U := type of Type in exact U)$ := t. +Inductive test : ltac:(let U := type of Type in exact U) := t. diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v new file mode 100644 index 0000000000..e46ea58bb3 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_120.v @@ -0,0 +1,138 @@ +Require Import TestSuite.admit. +(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *) +Set Universe Polymorphism. +Generalizable All Variables. +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. + +Class IsEquiv {A B : Type} (f : A -> B) := {}. + +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. + +Fixpoint nat_to_trunc_index (n : nat) : trunc_index + := match n with + | 0 => trunc_S (trunc_S minus_two) + | S n' => trunc_S (nat_to_trunc_index n') + end. + +Coercion nat_to_trunc_index : nat >-> trunc_index. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | minus_two => Contr_internal A + | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Notation minus_one:=(trunc_S minus_two). + +Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. + +Notation Contr := (IsTrunc minus_two). +Notation IsHProp := (IsTrunc minus_one). +Notation IsHSet := (IsTrunc 0). + +Class Funext := {}. +Inductive Unit : Set := tt. + +Instance contr_unit : Contr Unit | 0 := let x := {| + center := tt; + contr := fun t : Unit => match t with tt => idpath end + |} in x. +Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000. +admit. +Defined. +Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}. +Definition Unit_hp:hProp:=(hp Unit _). +Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. +Canonical Structure default_HSet:= fun T P => (@BuildhSet T P). +Definition ismono {X Y} (f : X -> Y) + := forall Z : hSet, + forall g h : Z -> X, (fun x => f (g x)) = (fun x => f (h x)) -> g = h. + +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. +Record PreCategory := + Build_PreCategory { + object :> Type; + morphism : object -> object -> Type; + compose : forall s d d', morphism d d' -> morphism s d -> morphism s d' + }. +Arguments compose [!C s d d'] m1 m2 : rename. + +Infix "o" := compose : morphism_scope. +Local Open Scope morphism_scope. + +Class IsEpimorphism {C} {x y} (m : morphism C x y) := + is_epimorphism : forall z (m1 m2 : morphism C y z), + m1 o m = m2 o m + -> m1 = m2. + +Class IsMonomorphism {C} {x y} (m : morphism C x y) := + is_monomorphism : forall z (m1 m2 : morphism C z x), + m o m1 = m o m2 + -> m1 = m2. +Class Univalence := {}. +Global Instance isset_hProp `{Funext} : IsHSet hProp | 0. Admitted. + +Definition set_cat : PreCategory + := @Build_PreCategory hSet + (fun x y => forall _ : x, y)%core + (fun _ _ _ f g x => f (g x))%core. +Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A. +Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted. +Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT P). +Definition isepi {X Y} `(f:X->Y) := forall Z: hSet, + forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h. +Definition issurj {X Y} (f:X->Y) := forall y:Y , hexists (fun x => (f x) = y). +Lemma isepi_issurj `{fs:Funext} `{ua:Univalence} `{fs' : Funext} {X Y} (f:X->Y): isepi f -> issurj f. +Proof. + intros epif y. + set (g :=fun _:Y => Unit_hp). + set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))). + clear fs'. + hnf in epif. + specialize (epif (BuildhSet hProp _) g h). + admit. +Defined. +Definition isequiv_isepi_ismono `{Univalence, fs0 : Funext} (X Y : hSet) (f : X -> Y) (epif : isepi f) (monof : ismono f) +: IsEquiv f. +Proof. + pose proof (@isepi_issurj _ _ _ _ _ f epif) as surjf. + admit. +Defined. +Section fully_faithful_helpers. + Context `{fs0 : Funext}. + Variables x y : hSet. + Variable m : x -> y. + + Fail Let isequiv_isepi_ismono_helper ua := + (@isequiv_isepi_ismono ua fs0 x y m : isepi m -> ismono m -> IsEquiv m). + + Goal True. + Fail set (isequiv_isepimorphism_ismonomorphism + := fun `{Univalence} + (Hepi : IsEpimorphism (m : morphism set_cat x y)) + (Hmono : IsMonomorphism (m : morphism set_cat x y)) + => (@isequiv_isepi_ismono_helper _ Hepi Hmono : @IsEquiv _ _ m)). + admit. + Undo. + Fail set (isequiv_isepimorphism_ismonomorphism + := fun `{Univalence} + (Hepi : IsEpimorphism (m : morphism set_cat x y)) + (Hmono : IsMonomorphism (m : morphism set_cat x y)) + => ((let _ := @isequiv_isepimorphism_ismonomorphism _ Hepi Hmono in @isequiv_isepi_ismono _ fs0 x y m Hepi Hmono) + : @IsEquiv _ _ m)). + Set Printing Universes. + admit. (* Error: Universe inconsistency (cannot enforce Top.235 <= Set because Set +< Top.235). *) |