diff options
| -rw-r--r-- | ROOT | 5 | ||||
| -rw-r--r-- | hott/HoTT.thy | 10 | ||||
| -rw-r--r-- | hott/Identity.thy | 4 | ||||
| -rw-r--r-- | hott/More_Types.thy (renamed from hott/Base.thy) | 10 | ||||
| -rw-r--r-- | hott/Nat.thy | 2 | ||||
| -rw-r--r-- | spartan/core/Spartan.thy | 9 | ||||
| -rw-r--r-- | spartan/data/List.thy | 79 |
7 files changed, 103 insertions, 16 deletions
@@ -17,7 +17,7 @@ session Spartan in spartan = Spartan_Core + directories data theories - "data/List" + List session HoTT in hott = Spartan + description " @@ -28,8 +28,9 @@ session HoTT in hott = Spartan + Available online at https://homotopytypetheory.org/book. " theories - Base + HoTT (global) Identity Equivalence + More_Types Nat diff --git a/hott/HoTT.thy b/hott/HoTT.thy new file mode 100644 index 0000000..0b3040c --- /dev/null +++ b/hott/HoTT.thy @@ -0,0 +1,10 @@ +theory HoTT +imports + Identity + Equivalence + More_Types + Nat + +begin + +end diff --git a/hott/Identity.thy b/hott/Identity.thy index 3a982f6..3fef536 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -30,13 +30,13 @@ axiomatization where b: A; \<And>x y p. \<lbrakk>p: x =\<^bsub>A\<^esub> y; x: A; y: A\<rbrakk> \<Longrightarrow> C x y p: U i; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) - \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a b p: C a b p" and + \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a b p: C a b p" and Id_comp: "\<lbrakk> a: A; \<And>x y p. \<lbrakk>x: A; y: A; p: x =\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow> C x y p: U i; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x) - \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a a (refl a) \<equiv> f a" + \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a a (refl a) \<equiv> f a" lemmas [intros] = IdF IdI and diff --git a/hott/Base.thy b/hott/More_Types.thy index 610a373..17789f8 100644 --- a/hott/Base.thy +++ b/hott/More_Types.thy @@ -1,17 +1,9 @@ -theory Base +theory More_Types imports Equivalence begin -section \<open>Notation\<close> - -syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3) -translations "a $ b" \<rightharpoonup> "a (b)" - -abbreviation (input) K where "K x \<equiv> \<lambda>_. x" - - section \<open>Sum type\<close> axiomatization diff --git a/hott/Nat.thy b/hott/Nat.thy index 311f2d9..e129be0 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -1,5 +1,5 @@ theory Nat -imports Base +imports Equivalence begin diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index b4f7772..50002a6 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -18,6 +18,11 @@ section \<open>Preamble\<close> declare [[eta_contract=false]] +syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3) +translations "a $ b" \<rightharpoonup> "a (b)" + +abbreviation (input) K where "K x \<equiv> \<lambda>_. x" + section \<open>Metatype setup\<close> @@ -118,8 +123,8 @@ axiomatization where p: \<Sum>x: A. B x; A: U i; \<And>x. x : A \<Longrightarrow> B x: U i; - \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i; - \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y> + \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>; + \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i \<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f p: C p" and Sig_comp: "\<lbrakk> diff --git a/spartan/data/List.thy b/spartan/data/List.thy index 71a879b..323ef7e 100644 --- a/spartan/data/List.thy +++ b/spartan/data/List.thy @@ -3,4 +3,83 @@ imports Spartan begin +(*TODO: Inductive type and recursive function definitions. The ad-hoc + axiomatization below should be subsumed once general inductive types are + properly implemented.*) + +axiomatization + List :: \<open>o \<Rightarrow> o\<close> and + nil :: \<open>o \<Rightarrow> o\<close> and + cons :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and + ListInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close> +where + ListF: "A: U i \<Longrightarrow> List A: U i" and + + List_nil: "A: U i \<Longrightarrow> nil A: List A" and + + List_cons: "\<lbrakk>x: A; l: List A\<rbrakk> \<Longrightarrow> cons A x l: List A" and + + ListE: "\<lbrakk> + xs: List A; + c\<^sub>0: C (nil A); + \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs); + \<And>xs. xs: List A \<Longrightarrow> C xs: U i + \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) xs: C xs" and + + List_comp_nil: "\<lbrakk> + c\<^sub>0: C (nil A); + \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs); + \<And>xs. xs: List A \<Longrightarrow> C xs: U i + \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) (nil A) \<equiv> c\<^sub>0" and + + List_comp_cons: "\<lbrakk> + xs: List A; + c\<^sub>0: C (nil A); + \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs); + \<And>xs. xs: List A \<Longrightarrow> C xs: U i + \<rbrakk> \<Longrightarrow> + ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) (cons A x xs) \<equiv> + f x xs (ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) xs)" + +lemmas + [intros] = ListF List_nil List_cons and + [elims "?xs"] = ListE and + [comps] = List_comp_nil List_comp_cons + +abbreviation "ListRec A C \<equiv> ListInd A (K C)" + + +section \<open>Implicit notation\<close> + +definition nil_i ("[]") + where [implicit]: "[] \<equiv> nil ?" + +definition cons_i (infixr "#" 50) + where [implicit]: "x # l \<equiv> cons ? x l" + + +section \<open>Standard functions\<close> + +definition "tail A \<equiv> \<lambda>xs: List A. ListRec A (List A) (nil A) (\<lambda>x xs _. xs) xs" + +definition "map A B \<equiv> \<lambda>f: A \<rightarrow> B. \<lambda>xs: List A. + ListRec A (List B) (nil B) (\<lambda>x _ c. cons B (f `x) c) xs" + +definition tail_i ("tail") + where [implicit]: "tail xs \<equiv> List.tail ? xs" + +definition map_i ("map") + where [implicit]: "map \<equiv> List.map ? ?" + +Lemma tail_type [typechk]: + assumes "A: U i" "xs: List A" + shows "tail xs: List A" + unfolding tail_def by typechk + +Lemma map_type [typechk]: + assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A" + shows "map f xs: List B" + unfolding map_def by typechk + + end |