From f49137b917fa7561eb53a87155ed57b3dbc70d90 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 13 Jun 2014 14:38:18 +0200 Subject: HoTT/coq bug #7 is closed, and the definitions can be made to go through using explicit universes. The behavior of Hint Rewrite still differs from Hint Resolve though. --- test-suite/bugs/closed/HoTT_coq_007.v | 112 +++++++++++++++++++++++++++++++++ test-suite/bugs/opened/HoTT_coq_007.v | 115 ---------------------------------- 2 files changed, 112 insertions(+), 115 deletions(-) create mode 100644 test-suite/bugs/closed/HoTT_coq_007.v delete mode 100644 test-suite/bugs/opened/HoTT_coq_007.v diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v new file mode 100644 index 0000000000..8592c729d0 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_007.v @@ -0,0 +1,112 @@ +Module Comment1. + Set Implicit Arguments. + + Polymorphic Record Category (obj : Type) := + { + Morphism : obj -> obj -> Type; + Identity : forall o, Morphism o o + }. + + Polymorphic Record Functor objC (C :Category objC) objD (D : Category objD) := + { + ObjectOf :> objC -> objD; + MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d); + FIdentityOf : forall o, MorphismOf _ _ (C.(Identity) o) = D.(Identity) (ObjectOf o) + }. + + Create HintDb functor discriminated. + + Hint Rewrite @FIdentityOf : functor. + + Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E. + refine {| ObjectOf := (fun c => G (F c)); + MorphismOf := (fun _ _ m => G.(MorphismOf) _ _ (F.(MorphismOf) _ _ m)) + |}; + intros; autorewrite with functor; reflexivity. + Defined. + + Definition Cat0 : Category@{i j} Empty_set. + refine {| + Morphism := fun s d : Empty_set => s = d; + Identity := fun o : Empty_set => eq_refl + |}; + admit. + Defined. + + Set Printing All. + Set Printing Universes. + + Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) + : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). + intro. intro. + unfold ComposeFunctors. + Abort. +End Comment1. + +Module Comment2. + Set Implicit Arguments. + + Polymorphic Record Category (obj : Type) := + { + Morphism : obj -> obj -> Type; + + Identity : forall o, Morphism o o; + Compose : forall s d d2, Morphism d d2 -> Morphism s d -> Morphism s d2; + + LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f + }. + + Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) := + { + ObjectOf : objC -> objD; + MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) + }. + + Create HintDb morphism discriminated. + + Polymorphic Hint Resolve @LeftIdentity : morphism. + + Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type. + refine {| + Morphism := (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type); + Identity := (fun o => (Identity _ (fst o), Identity _ (snd o))); + Compose := (fun (s d d2 : (objC * objD)%type) m2 m1 => (C.(Compose) _ _ _ (fst m2) (fst m1), D.(Compose) _ _ _ (snd m2) (snd m1))) + |}; + intros; apply injective_projections; simpl; auto with morphism. (* Replacing [auto with morphism] with [apply @LeftIdentity] removes the error *) + Defined. + + Polymorphic Definition Cat0 : Category Empty_set. + refine {| + Morphism := fun s d : Empty_set => s = d; + Identity := fun o : Empty_set => eq_refl; + Compose := fun s d d2 m0 m1 => eq_trans m1 m0 + |}; + admit. + Defined. + + Set Printing All. + Set Printing Universes. + Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0. + refine (Build_Functor (ProductCategory C Cat0) Cat0 _ _). (* Toplevel input, characters 15-71: +Error: Refiner was given an argument + "prod (* Top.2289 Top.2289 *) objC Empty_set" of type +"Type (* Top.2289 *)" instead of "Set". *) + Abort. + Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0. + econstructor. (* Toplevel input, characters 0-12: +Error: No applicable tactic. + *) + Abort. +End Comment2. + + +Module Comment3. + Polymorphic Lemma foo {obj : Type} : 1 = 1. + trivial. + Qed. + + Polymorphic Hint Resolve foo. (* success *) + Polymorphic Hint Rewrite @foo. (* Success *) + Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *) + Fail Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *) +End Comment3. diff --git a/test-suite/bugs/opened/HoTT_coq_007.v b/test-suite/bugs/opened/HoTT_coq_007.v deleted file mode 100644 index f609aff5d7..0000000000 --- a/test-suite/bugs/opened/HoTT_coq_007.v +++ /dev/null @@ -1,115 +0,0 @@ -Module Comment1. - Set Implicit Arguments. - - Polymorphic Record Category (obj : Type) := - { - Morphism : obj -> obj -> Type; - Identity : forall o, Morphism o o - }. - - Polymorphic Record Functor objC (C :Category objC) objD (D : Category objD) := - { - ObjectOf :> objC -> objD; - MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d); - FIdentityOf : forall o, MorphismOf _ _ (C.(Identity) o) = D.(Identity) (ObjectOf o) - }. - - Create HintDb functor discriminated. - - Hint Rewrite @FIdentityOf : functor. - - Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E. - refine {| ObjectOf := (fun c => G (F c)); - MorphismOf := (fun _ _ m => G.(MorphismOf) _ _ (F.(MorphismOf) _ _ m)) - |}; - intros; autorewrite with functor; reflexivity. - Defined. - - Definition Cat0 : Category Empty_set. - refine {| - Morphism := fun s d : Empty_set => s = d; - Identity := fun o : Empty_set => eq_refl - |}; - admit. - Defined. - - Set Printing All. - Set Printing Universes. - - Fail Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x). (** ??? The term "y" has type - "@Functor (* Top.448 Top.449 Top.450 Top.451 *) - (@Functor (* Set Top.441 Top.442 Top.336 *) Empty_set Cat0 objC C) C0 - Empty_set Cat0" while it is expected to have type - "@Functor (* Top.295 Top.296 Top.295 Top.296 *) ?46 ?47 ?48 ?49" -(Universe inconsistency: Cannot enforce Set = Top.295)). *) - Fail intro. (* Illegal application (Type Error) *) - Fail Abort. -End Comment1. - -Module Comment2. - Set Implicit Arguments. - - Polymorphic Record Category (obj : Type) := - { - Morphism : obj -> obj -> Type; - - Identity : forall o, Morphism o o; - Compose : forall s d d2, Morphism d d2 -> Morphism s d -> Morphism s d2; - - LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f - }. - - Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) := - { - ObjectOf : objC -> objD; - MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) - }. - - Create HintDb morphism discriminated. - - Polymorphic Hint Resolve @LeftIdentity : morphism. - - Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type. - refine {| - Morphism := (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type); - Identity := (fun o => (Identity _ (fst o), Identity _ (snd o))); - Compose := (fun (s d d2 : (objC * objD)%type) m2 m1 => (C.(Compose) _ _ _ (fst m2) (fst m1), D.(Compose) _ _ _ (snd m2) (snd m1))) - |}; - intros; apply injective_projections; simpl; auto with morphism. (* Replacing [auto with morphism] with [apply @LeftIdentity] removes the error *) - Defined. - - Polymorphic Definition Cat0 : Category Empty_set. - refine {| - Morphism := fun s d : Empty_set => s = d; - Identity := fun o : Empty_set => eq_refl; - Compose := fun s d d2 m0 m1 => eq_trans m1 m0 - |}; - admit. - Defined. - - Set Printing All. - Set Printing Universes. - Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0. - refine (Build_Functor (ProductCategory C Cat0) Cat0 _ _). (* Toplevel input, characters 15-71: -Error: Refiner was given an argument - "prod (* Top.2289 Top.2289 *) objC Empty_set" of type -"Type (* Top.2289 *)" instead of "Set". *) - Abort. - Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0. - econstructor. (* Toplevel input, characters 0-12: -Error: No applicable tactic. - *) - Abort. -End Comment2. - - -Module Comment3. - Polymorphic Lemma foo {obj : Type} : 1 = 1. - trivial. - Qed. - - Polymorphic Hint Resolve foo. (* success *) - Polymorphic Hint Rewrite @foo. (* Success *) - Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *) - Fail Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *) -End Comment3. -- cgit v1.2.3