From a245a3e2194b4d5a6e7fbac8fa10598e96307e57 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 30 Jan 2019 15:43:47 +0100 Subject: Begin refactor --- HoTT_Base.thy | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) (limited to 'HoTT_Base.thy') diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9e8fee7..93ef70e 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,9 +1,7 @@ (* -Title: HoTT_Base.thy -Author: Joshua Chen -Date: 2018 +Homotopy Type Theory -Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy. +Foundational setup and definitions *) theory HoTT_Base @@ -11,13 +9,12 @@ imports Pure begin - section \Basic setup\ declare[[eta_contract=false]] -typedecl t \ \Type of object types and terms\ -typedecl ord \ \Type of meta-level numerals\ +typedecl t \ \Type of object-logic terms (which includes the types)\ +typedecl ord \ \Type of meta-numerals\ axiomatization O :: ord and @@ -34,12 +31,10 @@ declare leq_min [intro!] lt_trans [intro] - -section \Judgment\ +section \Typing judgment\ judgment hastype :: "[t, t] \ prop" ("(3_:/ _)") - section \Universes\ axiomatization @@ -50,8 +45,8 @@ where U_cumulative': "\A: U i; i \ j\ \ A: U j" text \ -Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination. -One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. +Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination. +Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. @{thm U_cumulative'} is an alternative rule used by the method \cumulativity\ in @{file HoTT_Methods.thy}. \ -- cgit v1.2.3 From 843d53d64983593d765a203605cd2aab00ed8361 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 30 Jan 2019 16:09:50 +0100 Subject: Remove "constrained" notation for type families. Clean and document. --- HoTT_Base.thy | 33 +++++++++++++-------------------- 1 file changed, 13 insertions(+), 20 deletions(-) (limited to 'HoTT_Base.thy') diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 93ef70e..99ab5ce 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,8 +1,15 @@ -(* -Homotopy Type Theory +(******** +Isabelle/HoTT: Foundational definitions and notation +Jan 2019 -Foundational setup and definitions -*) +This file is the starting point, and contains the base setup and definitions of the object logic. +Among other things, it defines: + +* Meta-numerals to index the universe hierarchy, and related axioms. +* The universe hierarchy and its governing rules. +* Named theorems for later use by proof methods. + +********) theory HoTT_Base imports Pure @@ -11,7 +18,7 @@ begin section \Basic setup\ -declare[[eta_contract=false]] +declare[[eta_contract=false]] (* I'm not actually sure this does anything... *) typedecl t \ \Type of object-logic terms (which includes the types)\ typedecl ord \ \Type of meta-numerals\ @@ -51,26 +58,13 @@ Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. @{thm U_cumulative'} is an alternative rule used by the method \cumulativity\ in @{file HoTT_Methods.thy}. \ - -section \Type families\ - -abbreviation (input) constrained :: "[t \ t, t, t] \ prop" ("(1_:/ _ \ _)") - where "f: A \ B \ (\x. x : A \ f x: B)" - -text \ -The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \ B"}, where @{term "A::t"} and @{term "B::t"} are small types. -\ - -type_synonym tf = "t \ t" \ \Type of type families\ - - section \Named theorems\ named_theorems comp named_theorems form text \ -Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}. +The named theorems above will be used by proof methods defined in @{file HoTT_Methods.thy}. @{attribute comp} declares computation rules, which are used by the \compute\ method, and may also be passed to invocations of the method \subst\ to perform equational rewriting. @@ -80,5 +74,4 @@ These are mainly used by the \cumulativity\ method, which lifts typ (* Todo: Set up the Simplifier! *) - end -- cgit v1.2.3 From 07d312b312c3058551353bcf403a1dc7c7c83311 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 31 Jan 2019 15:51:24 +0100 Subject: Text remarks --- HoTT_Base.thy | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'HoTT_Base.thy') diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 99ab5ce..bb47a74 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -2,7 +2,7 @@ Isabelle/HoTT: Foundational definitions and notation Jan 2019 -This file is the starting point, and contains the base setup and definitions of the object logic. +This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions. Among other things, it defines: * Meta-numerals to index the universe hierarchy, and related axioms. @@ -18,7 +18,7 @@ begin section \Basic setup\ -declare[[eta_contract=false]] (* I'm not actually sure this does anything... *) +declare[[eta_contract=false]] (* Does this option actually do anything? *) typedecl t \ \Type of object-logic terms (which includes the types)\ typedecl ord \ \Type of meta-numerals\ @@ -55,9 +55,13 @@ text \ Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination. Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. -@{thm U_cumulative'} is an alternative rule used by the method \cumulativity\ in @{file HoTT_Methods.thy}. +@{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}. \ +section \Type families\ + +abbrev (input) + section \Named theorems\ named_theorems comp -- cgit v1.2.3 From 7a7e27f4a1efd69e9ab43b95d3c7ead61a743e55 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 4 Feb 2019 11:53:47 +0100 Subject: 1. Change syntax to rely less on unicode/control symbols. 2. Begin work on object-level type inference and input syntax help. --- HoTT_Base.thy | 65 ++++++++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 53 insertions(+), 12 deletions(-) (limited to 'HoTT_Base.thy') diff --git a/HoTT_Base.thy b/HoTT_Base.thy index bb47a74..a5280ce 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -5,7 +5,7 @@ Jan 2019 This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions. Among other things, it defines: -* Meta-numerals to index the universe hierarchy, and related axioms. +* Containers for storing type information of object-level terms. * The universe hierarchy and its governing rules. * Named theorems for later use by proof methods. @@ -16,12 +16,56 @@ imports Pure begin -section \Basic setup\ +section \Terms and typing\ -declare[[eta_contract=false]] (* Does this option actually do anything? *) +typedecl t \ \Type of object-logic terms (which includes the types)\ -typedecl t \ \Type of object-logic terms (which includes the types)\ -typedecl ord \ \Type of meta-numerals\ +consts has_type :: "[t, t] \ prop" \ \The judgment coercion\ + +text \ +We create a dedicated container in which to store object-level typing information whenever a typing judgment that does not depend on assumptions is proved. +\ + +ML \ +signature TYPINGS = +sig + val get: term -> term +end + +structure Typings: TYPINGS = +struct + +structure Typing_Data = Theory_Data +( + type T = term Symtab.table + val empty = Symtab.empty + val extend = I + + fun merge (tbl, tbl') = + let + val key_vals = map (Symtab.lookup_key tbl') (Symtab.keys tbl') + val updates = map (fn SOME kv => Symtab.update kv) key_vals + fun f u t = u t + in fold f updates tbl end +) + +fun get tm = + case Symtab.lookup (Typing_Data.get @{theory}) (Syntax.string_of_term @{context} tm) of + SOME tm' => tm' + | NONE => raise Fail "No typing information available" + +end +\ + +syntax "_has_type" :: "[t, t] \ prop" ("3(_:/ _)") + +parse_translation \ + +\ + +section \Universes\ + +typedecl ord \ \Type of meta-numerals\ axiomatization O :: ord and @@ -38,12 +82,6 @@ declare leq_min [intro!] lt_trans [intro] -section \Typing judgment\ - -judgment hastype :: "[t, t] \ prop" ("(3_:/ _)") - -section \Universes\ - axiomatization U :: "ord \ t" where @@ -60,7 +98,10 @@ Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. section \Type families\ -abbrev (input) +abbreviation (input) constraint :: "[t \ t, t, t] \ prop" ("(1_:/ _ \ _)") +where "f: A \ B \ (\x. x: A \ f x: B)" + +text \We use the notation @{prop "B: A \ U i"} to abbreviate type families.\ section \Named theorems\ -- cgit v1.2.3 From d70da13b7fd36509c1d843d139a0b99c6acb8cc6 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 5 Feb 2019 18:15:58 +0100 Subject: Type inference setup begun - first use-case for function composition. --- HoTT_Base.thy | 57 +++++++++------------------------------------------------ 1 file changed, 9 insertions(+), 48 deletions(-) (limited to 'HoTT_Base.thy') diff --git a/HoTT_Base.thy b/HoTT_Base.thy index a5280ce..aa13815 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -3,11 +3,11 @@ Isabelle/HoTT: Foundational definitions and notation Jan 2019 This file is the starting point of the Isabelle/HoTT object logic, and contains the basic setup and definitions. -Among other things, it defines: +Among other things, it: -* Containers for storing type information of object-level terms. -* The universe hierarchy and its governing rules. -* Named theorems for later use by proof methods. +* Sets up object-level type inference functionality (via typing.ML). +* Defines the universe hierarchy and its governing rules. +* Defines named theorems for later use by proof methods. ********) @@ -20,48 +20,9 @@ section \Terms and typing\ typedecl t \ \Type of object-logic terms (which includes the types)\ -consts has_type :: "[t, t] \ prop" \ \The judgment coercion\ +judgment has_type :: "[t, t] \ prop" ("(3_:/ _)") -text \ -We create a dedicated container in which to store object-level typing information whenever a typing judgment that does not depend on assumptions is proved. -\ - -ML \ -signature TYPINGS = -sig - val get: term -> term -end - -structure Typings: TYPINGS = -struct - -structure Typing_Data = Theory_Data -( - type T = term Symtab.table - val empty = Symtab.empty - val extend = I - - fun merge (tbl, tbl') = - let - val key_vals = map (Symtab.lookup_key tbl') (Symtab.keys tbl') - val updates = map (fn SOME kv => Symtab.update kv) key_vals - fun f u t = u t - in fold f updates tbl end -) - -fun get tm = - case Symtab.lookup (Typing_Data.get @{theory}) (Syntax.string_of_term @{context} tm) of - SOME tm' => tm' - | NONE => raise Fail "No typing information available" - -end -\ - -syntax "_has_type" :: "[t, t] \ prop" ("3(_:/ _)") - -parse_translation \ - -\ +ML_file "typing.ML" section \Universes\ @@ -85,13 +46,13 @@ declare axiomatization U :: "ord \ t" where - U_hierarchy: "i < j \ U i: U j" and + U_hierarchy: "i < j \ U i: U j" and U_cumulative: "\A: U i; i < j\ \ A: U j" and U_cumulative': "\A: U i; i \ j\ \ A: U j" text \ -Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will very easily lead to non-termination. -Instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. +Using method @{method rule} with @{thm U_cumulative} and @{thm U_cumulative'} is unsafe: if applied blindly it will very easily lead to non-termination. +Instead use @{method elim}, or instantiate the rules suitably. @{thm U_cumulative'} is an alternative rule used by the method @{theory_text cumulativity} in @{file HoTT_Methods.thy}. \ -- cgit v1.2.3 From 8759a6ff0dbe5f0e9dbc28ab2711c54bed7ffa44 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 5 Feb 2019 18:29:10 +0100 Subject: Decided to keep terms eta-expanded --- HoTT_Base.thy | 2 ++ 1 file changed, 2 insertions(+) (limited to 'HoTT_Base.thy') diff --git a/HoTT_Base.thy b/HoTT_Base.thy index aa13815..88cf986 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -18,6 +18,8 @@ begin section \Terms and typing\ +declare[[eta_contract=false]] + typedecl t \ \Type of object-logic terms (which includes the types)\ judgment has_type :: "[t, t] \ prop" ("(3_:/ _)") -- cgit v1.2.3 From 64d2a5c60acce40113362c9d7eca8cd633362d23 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 5 Feb 2019 18:32:43 +0100 Subject: Add cong named theorem for congruence rules --- HoTT_Base.thy | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'HoTT_Base.thy') diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 88cf986..e74ef31 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -68,16 +68,19 @@ text \We use the notation @{prop "B: A \ U i"} to abbreviate type section \Named theorems\ -named_theorems comp named_theorems form +named_theorems comp +named_theorems cong text \ The named theorems above will be used by proof methods defined in @{file HoTT_Methods.thy}. -@{attribute comp} declares computation rules, which are used by the \compute\ method, and may also be passed to invocations of the method \subst\ to perform equational rewriting. - @{attribute form} declares type formation rules. These are mainly used by the \cumulativity\ method, which lifts types into higher universes. + +@{attribute comp} declares computation rules, which are used by the \compute\ method, and may also be passed to invocations of the method \subst\ to perform equational rewriting. + +@{attribute cong} declares congruence rules, the definitional equality rules of the type theory. \ (* Todo: Set up the Simplifier! *) -- cgit v1.2.3