From 60f32406e8c9712c0689d54a3dd4f8e17d310d52 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 25 May 2020 18:50:59 +0200 Subject: Lists + more reorganizing --- ROOT | 5 ++- hott/Base.thy | 99 ------------------------------------------------ hott/HoTT.thy | 10 +++++ hott/Identity.thy | 4 +- hott/More_Types.thy | 91 ++++++++++++++++++++++++++++++++++++++++++++ hott/Nat.thy | 2 +- spartan/core/Spartan.thy | 9 ++++- spartan/data/List.thy | 79 ++++++++++++++++++++++++++++++++++++++ 8 files changed, 193 insertions(+), 106 deletions(-) delete mode 100644 hott/Base.thy create mode 100644 hott/HoTT.thy create mode 100644 hott/More_Types.thy diff --git a/ROOT b/ROOT index 1e8017c..b716396 100644 --- a/ROOT +++ b/ROOT @@ -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/Base.thy b/hott/Base.thy deleted file mode 100644 index 610a373..0000000 --- a/hott/Base.thy +++ /dev/null @@ -1,99 +0,0 @@ -theory Base -imports Equivalence - -begin - - -section \Notation\ - -syntax "_dollar" :: \logic \ logic \ logic\ (infixr "$" 3) -translations "a $ b" \ "a (b)" - -abbreviation (input) K where "K x \ \_. x" - - -section \Sum type\ - -axiomatization - Sum :: \o \ o \ o\ and - inl :: \o \ o \ o \ o\ and - inr :: \o \ o \ o \ o\ and - SumInd :: \o \ o \ (o \ o) \ (o \ o) \ (o \ o) \ o \ o\ - -notation Sum (infixl "\" 50) - -axiomatization where - SumF: "\A: U i; B: U i\ \ A \ B: U i" and - - Sum_inl: "\a: A; B: U i\ \ inl A B a: A \ B" and - - Sum_inr: "\b: B; A: U i\ \ inr A B b: A \ B" and - - SumE: "\ - s: A \ B; - \s. s: A \ B \ C s: U i; - \a. a: A \ c a: C (inl A B a); - \b. b: B \ d b: C (inr A B b) - \ \ SumInd A B (\s. C s) (\a. c a) (\b. d b) s: C s" and - - Sum_comp_inl: "\ - a: A; - \s. s: A \ B \ C s: U i; - \a. a: A \ c a: C (inl A B a); - \b. b: B \ d b: C (inr A B b) - \ \ SumInd A B (\s. C s) (\a. c a) (\b. d b) (inl A B a) \ c a" and - - Sum_comp_inr: "\ - b: B; - \s. s: A \ B \ C s: U i; - \a. a: A \ c a: C (inl A B a); - \b. b: B \ d b: C (inr A B b) - \ \ SumInd A B (\s. C s) (\a. c a) (\b. d b) (inr A B b) \ d b" - -lemmas - [intros] = SumF Sum_inl Sum_inr and - [elims] = SumE and - [comps] = Sum_comp_inl Sum_comp_inr - - -section \Empty and unit types\ - -axiomatization - Top :: \o\ and - tt :: \o\ and - TopInd :: \(o \ o) \ o \ o \ o\ -and - Bot :: \o\ and - BotInd :: \(o \ o) \ o \ o\ - -notation Top ("\") and Bot ("\") - -axiomatization where - TopF: "\: U i" and - - TopI: "tt: \" and - - TopE: "\a: \; \x. x: \ \ C x: U i; c: C tt\ \ TopInd (\x. C x) c a: C a" and - - Top_comp: "\\x. x: \ \ C x: U i; c: C tt\ \ TopInd (\x. C x) c tt \ c" -and - BotF: "\: U i" and - - BotE: "\x: \; \x. x: \ \ C x: U i\ \ BotInd (\x. C x) x: C x" - -lemmas - [intros] = TopF TopI BotF and - [elims] = TopE BotE and - [comps] = Top_comp - - -section \Booleans\ - -definition "Bool \ \ \ \" -definition "true \ inl \ \ tt" -definition "false \ inr \ \ tt" - -\ \Can define if-then-else etc.\ - - -end 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; \x y p. \p: x =\<^bsub>A\<^esub> y; x: A; y: A\ \ C x y p: U i; \x. x: A \ f x: C x x (refl x) - \ \ IdInd A (\x y p. C x y p) f a b p: C a b p" and + \ \ IdInd A (\x y p. C x y p) (\x. f x) a b p: C a b p" and Id_comp: "\ a: A; \x y p. \x: A; y: A; p: x =\<^bsub>A\<^esub> y\ \ C x y p: U i; \x. x: A \ f x: C x x (refl x) - \ \ IdInd A (\x y p. C x y p) f a a (refl a) \ f a" + \ \ IdInd A (\x y p. C x y p) (\x. f x) a a (refl a) \ f a" lemmas [intros] = IdF IdI and diff --git a/hott/More_Types.thy b/hott/More_Types.thy new file mode 100644 index 0000000..17789f8 --- /dev/null +++ b/hott/More_Types.thy @@ -0,0 +1,91 @@ +theory More_Types +imports Equivalence + +begin + + +section \Sum type\ + +axiomatization + Sum :: \o \ o \ o\ and + inl :: \o \ o \ o \ o\ and + inr :: \o \ o \ o \ o\ and + SumInd :: \o \ o \ (o \ o) \ (o \ o) \ (o \ o) \ o \ o\ + +notation Sum (infixl "\" 50) + +axiomatization where + SumF: "\A: U i; B: U i\ \ A \ B: U i" and + + Sum_inl: "\a: A; B: U i\ \ inl A B a: A \ B" and + + Sum_inr: "\b: B; A: U i\ \ inr A B b: A \ B" and + + SumE: "\ + s: A \ B; + \s. s: A \ B \ C s: U i; + \a. a: A \ c a: C (inl A B a); + \b. b: B \ d b: C (inr A B b) + \ \ SumInd A B (\s. C s) (\a. c a) (\b. d b) s: C s" and + + Sum_comp_inl: "\ + a: A; + \s. s: A \ B \ C s: U i; + \a. a: A \ c a: C (inl A B a); + \b. b: B \ d b: C (inr A B b) + \ \ SumInd A B (\s. C s) (\a. c a) (\b. d b) (inl A B a) \ c a" and + + Sum_comp_inr: "\ + b: B; + \s. s: A \ B \ C s: U i; + \a. a: A \ c a: C (inl A B a); + \b. b: B \ d b: C (inr A B b) + \ \ SumInd A B (\s. C s) (\a. c a) (\b. d b) (inr A B b) \ d b" + +lemmas + [intros] = SumF Sum_inl Sum_inr and + [elims] = SumE and + [comps] = Sum_comp_inl Sum_comp_inr + + +section \Empty and unit types\ + +axiomatization + Top :: \o\ and + tt :: \o\ and + TopInd :: \(o \ o) \ o \ o \ o\ +and + Bot :: \o\ and + BotInd :: \(o \ o) \ o \ o\ + +notation Top ("\") and Bot ("\") + +axiomatization where + TopF: "\: U i" and + + TopI: "tt: \" and + + TopE: "\a: \; \x. x: \ \ C x: U i; c: C tt\ \ TopInd (\x. C x) c a: C a" and + + Top_comp: "\\x. x: \ \ C x: U i; c: C tt\ \ TopInd (\x. C x) c tt \ c" +and + BotF: "\: U i" and + + BotE: "\x: \; \x. x: \ \ C x: U i\ \ BotInd (\x. C x) x: C x" + +lemmas + [intros] = TopF TopI BotF and + [elims] = TopE BotE and + [comps] = Top_comp + + +section \Booleans\ + +definition "Bool \ \ \ \" +definition "true \ inl \ \ tt" +definition "false \ inr \ \ tt" + +\ \Can define if-then-else etc.\ + + +end 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 \Preamble\ declare [[eta_contract=false]] +syntax "_dollar" :: \logic \ logic \ logic\ (infixr "$" 3) +translations "a $ b" \ "a (b)" + +abbreviation (input) K where "K x \ \_. x" + section \Metatype setup\ @@ -118,8 +123,8 @@ axiomatization where p: \x: A. B x; A: U i; \x. x : A \ B x: U i; - \p. p: \x: A. B x \ C p: U i; - \x y. \x: A; y: B x\ \ f x y: C + \x y. \x: A; y: B x\ \ f x y: C ; + \p. p: \x: A. B x \ C p: U i \ \ SigInd A (\x. B x) (\p. C p) f p: C p" and Sig_comp: "\ 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 :: \o \ o\ and + nil :: \o \ o\ and + cons :: \o \ o \ o \ o\ and + ListInd :: \o \ (o \ o) \ o \ (o \ o \ o \ o) \ o \ o\ +where + ListF: "A: U i \ List A: U i" and + + List_nil: "A: U i \ nil A: List A" and + + List_cons: "\x: A; l: List A\ \ cons A x l: List A" and + + ListE: "\ + xs: List A; + c\<^sub>0: C (nil A); + \x xs c. \x: A; xs: List A; c: C xs\ \ f x xs c: C (cons A x xs); + \xs. xs: List A \ C xs: U i + \ \ ListInd A (\xs. C xs) c\<^sub>0 (\x xs c. f x xs c) xs: C xs" and + + List_comp_nil: "\ + c\<^sub>0: C (nil A); + \x xs c. \x: A; xs: List A; c: C xs\ \ f x xs c: C (cons A x xs); + \xs. xs: List A \ C xs: U i + \ \ ListInd A (\xs. C xs) c\<^sub>0 (\x xs c. f x xs c) (nil A) \ c\<^sub>0" and + + List_comp_cons: "\ + xs: List A; + c\<^sub>0: C (nil A); + \x xs c. \x: A; xs: List A; c: C xs\ \ f x xs c: C (cons A x xs); + \xs. xs: List A \ C xs: U i + \ \ + ListInd A (\xs. C xs) c\<^sub>0 (\x xs c. f x xs c) (cons A x xs) \ + f x xs (ListInd A (\xs. C xs) c\<^sub>0 (\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 \ ListInd A (K C)" + + +section \Implicit notation\ + +definition nil_i ("[]") + where [implicit]: "[] \ nil ?" + +definition cons_i (infixr "#" 50) + where [implicit]: "x # l \ cons ? x l" + + +section \Standard functions\ + +definition "tail A \ \xs: List A. ListRec A (List A) (nil A) (\x xs _. xs) xs" + +definition "map A B \ \f: A \ B. \xs: List A. + ListRec A (List B) (nil B) (\x _ c. cons B (f `x) c) xs" + +definition tail_i ("tail") + where [implicit]: "tail xs \ List.tail ? xs" + +definition map_i ("map") + where [implicit]: "map \ 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 \ B" "xs: List A" + shows "map f xs: List B" + unfolding map_def by typechk + + end -- cgit v1.2.3