From f899bf0ca912fef887b7c1ed9781e4c21ec4ec24 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 17 Sep 2023 20:05:05 -0400 Subject: [PATCH 1/3] HITs: fix inconsistencies from several HITs --- theories/Colimits/GraphQuotient.v | 4 ++-- theories/HIT/Flattening.v | 2 +- theories/HIT/Interval.v | 8 -------- theories/HIT/README.txt | 13 ++++--------- theories/Spaces/Torus/Torus.v | 6 ++---- 5 files changed, 9 insertions(+), 24 deletions(-) diff --git a/theories/Colimits/GraphQuotient.v b/theories/Colimits/GraphQuotient.v index 4a803b617b1..8f2f4c0023a 100644 --- a/theories/Colimits/GraphQuotient.v +++ b/theories/Colimits/GraphQuotient.v @@ -22,8 +22,8 @@ Module Export GraphQuotient. (gqglue' : forall a b (s : R a b), gqglue@{i j u} s # gq' a = gq' b) : forall x, P x := fun x => match x with - | gq a => gq' a - end. + | gq a => fun _ => gq' a + end gqglue'. Axiom GraphQuotient_ind_beta_gqglue@{i j u k} : forall {A : Type@{i}} {R : A -> A -> Type@{j}} diff --git a/theories/HIT/Flattening.v b/theories/HIT/Flattening.v index 253b88adc23..755148a531d 100644 --- a/theories/HIT/Flattening.v +++ b/theories/HIT/Flattening.v @@ -29,7 +29,7 @@ Definition Wtil_ind {A B f g C D} (Q : Wtil A B f g C D -> Type) (cct' : forall a x, Q (cct a x)) (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y)) : forall w, Q w - := fun w => match w with cct a x => cct' a x end. + := fun w => match w with cct a x => fun _ => cct' a x end ppt'. Axiom Wtil_ind_beta_ppt : forall {A B f g C D} (Q : Wtil A B f g C D -> Type) diff --git a/theories/HIT/Interval.v b/theories/HIT/Interval.v index 7efcac67c09..b58194bcce3 100644 --- a/theories/HIT/Interval.v +++ b/theories/HIT/Interval.v @@ -30,14 +30,6 @@ Axiom interval_ind_beta_seg : forall (P : interval -> Type) End Interval. -(* Should fail: -Lemma test (P : interval -> Type) (a : P zero) (b : P one) - (p p' : seg # a = b) : - interval_ind P a b p = interval_ind P a b p'. -reflexivity. -*) - - Definition interval_rec (P : Type) (a b : P) (p : a = b) : interval -> P := interval_ind (fun _ => P) a b (transport_const _ _ @ p). diff --git a/theories/HIT/README.txt b/theories/HIT/README.txt index 136590493b8..13a4312ddbd 100644 --- a/theories/HIT/README.txt +++ b/theories/HIT/README.txt @@ -1,10 +1,5 @@ -The files in this directory require Yves Bertot's "private types" -extension to Coq in order to implement higher inductive types (HITs). -The "private types" extension is included in the stable branch of the -HoTT/coq repository, so if you followed the INSTALL instructions you -should be okay. +The files in this directory use "private inductive types" in order to +implement higher inductive types (HITs). -The files which use HITs are currently segregated into this directory -because the "private types" extension is a hack whose details may -change in the future, and we are still hoping to one day have an -actual implementation of HITs. +Many of the files which use HITs are currently segregated into this +directory, but they can also be found in other directories. diff --git a/theories/Spaces/Torus/Torus.v b/theories/Spaces/Torus/Torus.v index 6bff6b6f02c..cefef2a26c4 100644 --- a/theories/Spaces/Torus/Torus.v +++ b/theories/Spaces/Torus/Torus.v @@ -19,10 +19,8 @@ Module Export Torus. (* We define the induction principle for Torus *) Definition Torus_ind (P : Torus -> Type) (pb : P tbase) (pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb) - (ps : DPathSquare P surf pla pla plb plb) (x : Torus) : P x. - Proof. - by destruct x. - Defined. + (ps : DPathSquare P surf pla pla plb plb) (x : Torus) : P x + := (match x with tbase => fun _ _ _ => pb end) pla plb ps. (* We declare propsitional computational rules for loop_a and loop_b *) Axiom Torus_ind_beta_loop_a : forall (P : Torus -> Type) (pb : P tbase) From 9b9c6d7785ad71587f1f9719acc31a8258105d37 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sun, 17 Sep 2023 20:10:17 -0400 Subject: [PATCH 2/3] add github1758.v tests --- test/bugs/github1758.v | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 test/bugs/github1758.v diff --git a/test/bugs/github1758.v b/test/bugs/github1758.v new file mode 100644 index 00000000000..f43e9e4e01c --- /dev/null +++ b/test/bugs/github1758.v @@ -0,0 +1,42 @@ +From HoTT Require Import Basics.Overture HIT.Interval HIT.Flattening Colimits.GraphQuotient + Spaces.Torus.Torus Cubical. + +Fail Definition test_interval (P : interval -> Type) (a : P zero) (b : P one) + (p p' : seg # a = b) : + interval_ind P a b p = interval_ind P a b p' + := 1. + +Fail Definition test_wtil {A B f g C D} (Q : Wtil A B f g C D -> Type) + (cct' : forall a x, Q (cct a x)) + (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y)) + (ppt'' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y)) + : Wtil_ind Q cct' ppt' = Wtil_ind Q cct' ppt'' + := 1. + +Section GraphQuotient_bug. + Local Definition R : Unit -> Unit -> Type := fun x y => Unit. + + (* This should be the circle. *) + Local Definition Q := GraphQuotient R. + + (* This is the identity map. *) + Local Definition id : Q -> Q := GraphQuotient_rec gq (fun a b r => gqglue r). + + (* This is the constant map. *) + Local Definition cst : Q -> Q. + Proof. + refine (GraphQuotient_rec gq _). + intros [] [] r. + reflexivity. + Defined. + + Fail Definition test_graphquotient : id = cst := 1. +End GraphQuotient_bug. + +Fail Definition test_torus (P : Torus -> Type) (pb : P tbase) + (pla pla' : DPath P loop_a pb pb) + (plb : DPath P loop_b pb pb) + (ps : DPathSquare P surf pla pla plb plb) + (ps' : DPathSquare P surf pla' pla' plb plb) + : Torus_ind P pb pla plb ps = Torus_ind P pb pla' plb ps' + := 1. From 5e52ef8ce7e7bc19eb99fcf1f35ab12a642f85af Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 18 Sep 2023 09:45:54 -0400 Subject: [PATCH 3/3] test/bugs/github1758.v: add comment explaining tests --- test/bugs/github1758.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/test/bugs/github1758.v b/test/bugs/github1758.v index f43e9e4e01c..ac341eb1a6f 100644 --- a/test/bugs/github1758.v +++ b/test/bugs/github1758.v @@ -1,6 +1,8 @@ From HoTT Require Import Basics.Overture HIT.Interval HIT.Flattening Colimits.GraphQuotient Spaces.Torus.Torus Cubical. +(* Test that various higher inductive types are defined correctly. If they are defined in the most naive way, two uses of the induction principle that are definitionally equal on the point constructors will be considered definitionally equal, which is inconsistent. There is an idiom that must be used in order to force Coq to regard the supplementary data as being required as well. See, for example, Colimits/GraphQuotient.v for the idiom. *) + Fail Definition test_interval (P : interval -> Type) (a : P zero) (b : P one) (p p' : seg # a = b) : interval_ind P a b p = interval_ind P a b p'