diff options
| -rw-r--r-- | Equal.thy | 95 | ||||
| -rw-r--r-- | HoTT_Base.thy | 13 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 29 | ||||
| -rw-r--r-- | Prod.thy | 28 | ||||
| -rw-r--r-- | Projections.thy | 4 | ||||
| -rw-r--r-- | Sum.thy | 4 |
6 files changed, 132 insertions, 41 deletions
@@ -1,52 +1,105 @@ -(* -Title: Equal.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Equality +Feb 2019 -Equality type -*) +********) theory Equal -imports HoTT_Base +imports Prod HoTT_Methods begin -section \<open>Basic definitions\<close> +section \<open>Type definitions\<close> axiomatization - Equal :: "[t, t, t] \<Rightarrow> t" and - refl :: "t \<Rightarrow> t" and - indEqual :: "[t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>=)") + Eq :: "[t, t, t] \<Rightarrow> t" and + refl :: "t \<Rightarrow> t" and + indEq :: "[[t, t, t] \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" syntax - "_equal" :: "[t, t, t] \<Rightarrow> t" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) - "_equal_ascii" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) - + "_Eq" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) translations - "a =[A] b" \<rightleftharpoons> "CONST Equal A a b" - "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b" + "a =[A] b" \<rightleftharpoons> "(CONST Eq) A a b" axiomatization where - Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i" and + Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =[A] b: U i" and - Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a" and + Equal_intro: "a: A \<Longrightarrow> (refl a): a =[A] a" and Equal_elim: "\<lbrakk> - p: x =\<^sub>A y; + p: x =[A] y; x: A; y: A; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= f p : C x y p" and + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f p : C x y p" and Equal_comp: "\<lbrakk> a: A; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= f (refl a) \<equiv> f a" + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =[A] y \<leadsto> U i \<rbrakk> \<Longrightarrow> indEq C f (refl a) \<equiv> f a" lemmas Equal_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim lemmas Equal_comp [comp] +section \<open>Path induction\<close> + +text \<open>We set up rudimentary automation of path induction:\<close> + +method path_ind for x y p :: t = + (rule Equal_elim[where ?x=x and ?y=y and ?p=p]; (fact | assumption)?) + + +section \<open>Properties of equality\<close> + +subsection \<open>Symmetry (path inverse)\<close> + +definition inv :: "[t, t] \<Rightarrow> t" +where "inv A p \<equiv> indEq (\<lambda>x y. ^(y =[A] x)) (\<lambda>x. refl x) p" + +lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =[A] y\<rbrakk> \<Longrightarrow> inv A p: y =[A] x" +unfolding inv_def by derive + +lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> inv A (refl a) \<equiv> refl a" +unfolding inv_def by derive + +declare + inv_type [intro] + inv_comp [comp] + +subsection \<open>Transitivity (path composition)\<close> + +schematic_goal transitivity: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?p: \<Prod>z: A. y =[A]z \<rightarrow> x =[A] z" +proof (path_ind x y p, quantify 2) + fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" . +qed (routine add: assms) + + +syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 110) +translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q" + +lemma pathcomp_type: + assumes "A: U i" "x: A" "y: A" "z: A" + shows "pathcomp: x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)" +unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms) + +corollary pathcomp_trans: + assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z" + shows "p \<bullet> q: x =\<^sub>A z" +by (routine add: assms pathcomp_type) + +lemma pathcomp_comp: + assumes "A: U i" and "a: A" + shows "(refl a) \<bullet> (refl a) \<equiv> refl a" +unfolding pathcomp_def by (derive lems: assms) + +declare + pathcomp_type [intro] + pathcomp_trans [intro] + pathcomp_comp [comp] + end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9dcf6d0..1dcf61c 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -2,11 +2,11 @@ Isabelle/HoTT: Basic logical definitions and notation Feb 2019 -This file completes the basic logical and functional setup of the HoTT logic. -Among other things, it: +This file completes the basic logical and functional setup of the HoTT logic. It defines: -* Defines the universe hierarchy and its governing rules. -* Defines named theorems for later use by proof methods. +* The universe hierarchy and its governing rules. +* Some notational abbreviations. +* Named theorems for later use by proof methods. ********) @@ -50,13 +50,16 @@ Instead use @{method elim}, or instantiate the rules suitably. \<close> -section \<open>Type families\<close> +section \<open>Notation\<close> abbreviation (input) constraint :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop" ("(1_:/ _ \<leadsto> _)") where "f: A \<leadsto> B \<equiv> (\<And>x. x: A \<Longrightarrow> f x: B)" text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type families.\<close> +abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" ("^_" [1000]) +where "^A \<equiv> \<lambda>_. A" + section \<open>Named theorems\<close> diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 088c1fa..d93680a 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -2,6 +2,8 @@ Isabelle/HoTT: Proof methods Jan 2019 +Setup various proof methods and auxiliary functionality. + ********) theory HoTT_Methods @@ -10,6 +12,25 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" begin +section \<open>More method combinators\<close> + +ML \<open> +(* Use as "repeat n tac" *) +fun repeat tac = + let + fun cparser_of parser (ctxt, toks) = parser toks ||> (fn toks => (ctxt, toks)) + in + cparser_of Args.text >> + (fn n => fn ctxt => fn facts => + SIMPLE_METHOD ( + REPEAT_DETERM_N + (the (Int.fromString n)) + (tac ctxt)) + facts) + end +\<close> + + section \<open>Substitution and simplification\<close> ML_file "~~/src/Tools/misc_legacy.ML" @@ -67,12 +88,4 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}. method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ - -section \<open>Induction\<close> - -text \<open> -Placeholder section for the automation of induction, i.e. using the type elimination rules. -At the moment one must directly apply them with @{method rule} or @{method elim}. -\<close> - end @@ -9,6 +9,7 @@ imports HoTT_Base HoTT_Methods begin + section \<open>Basic type definitions\<close> axiomatization @@ -35,14 +36,14 @@ The syntax translations above bind the variable @{term x} in the expressions @{t text \<open>Non-dependent functions are a special case:\<close> abbreviation Fun :: "[t, t] \<Rightarrow> t" (infixr "\<rightarrow>" 40) -where "A \<rightarrow> B \<equiv> \<Prod>(_: A). B" +where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" axiomatization where \<comment> \<open>Type rules\<close> Prod_form: "\<lbrakk>A: U i; B: A \<leadsto> U i\<rbrakk> \<Longrightarrow> \<Prod>x: A. B x: U i" and - Prod_intro: "\<lbrakk>A: U i; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and + Prod_intro: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; A: U i\<rbrakk> \<Longrightarrow> \<lambda>x: A. b x: \<Prod>x: A. B x" and Prod_elim: "\<lbrakk>f: \<Prod>x: A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and @@ -68,6 +69,25 @@ lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim lemmas Prod_comp [comp] = Prod_cmp Prod_uniq lemmas Prod_cong [cong] = Prod_form_eq Prod_intro_eq + +section \<open>Universal quantification\<close> + +text \<open> +It will often be useful to convert a proof goal asserting the inhabitation of a dependent product to one that instead uses Pure universal quantification. + +Method @{theory_text quantify} converts the goal +@{text "t: \<Prod>x1: A1. ... \<Prod>xn: An. B x1 ... xn"}, +where @{term B} is not a product, to +@{text "\<And>x1 ... xn . \<lbrakk>x1: A1; ...; xn: An\<rbrakk> \<Longrightarrow> ?b x1 ... xn: B x1 ... xn"}. + +Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. +\<close> + +method_setup quantify = \<open>repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\<close> + +method quantify_all = (rule Prod_intro)+ + + section \<open>Function composition\<close> definition compose :: "[t, t, t] \<Rightarrow> t" @@ -76,6 +96,7 @@ where "compose A g f \<equiv> \<lambda>x: A. g`(f`x)" declare compose_def [comp] syntax "_compose" :: "[t, t] \<Rightarrow> t" (infixr "o" 110) +(* parse_translation \<open> let fun compose_tr ctxt [g, f] = let @@ -98,6 +119,7 @@ in [("_compose", compose_tr)] end \<close> +*) text \<open>Pretty-printing switch for composition; hides domain type information.\<close> @@ -120,7 +142,7 @@ by (derive lems: assms cong) lemma compose_comp: assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x" - shows "(\<lambda>x: B. c x) o (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)" + shows "compose A (\<lambda>x: B. c x) (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)" by (derive lems: assms cong) abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x" diff --git a/Projections.thy b/Projections.thy index c819240..8ff6b30 100644 --- a/Projections.thy +++ b/Projections.thy @@ -39,7 +39,7 @@ lemma snd_cmp: assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "snd A B <a,b> \<equiv> b" unfolding snd_def by (derive lems: assms) -lemmas Proj_types [intro] = fst_type snd_type -lemmas Proj_comps [comp] = fst_cmp snd_cmp +lemmas Proj_type [intro] = fst_type snd_type +lemmas Proj_comp [comp] = fst_cmp snd_cmp end @@ -18,8 +18,8 @@ syntax "_Sum" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>'(_: _')./ _)" 20) "_Sum'" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_: _./ _)" 20) translations - "\<Sum>(x: A). B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" - "\<Sum>x: A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" + "\<Sum>(x: A). B" \<rightleftharpoons> "(CONST Sum) A (\<lambda>x. B)" + "\<Sum>x: A. B" \<rightleftharpoons> "(CONST Sum) A (\<lambda>x. B)" abbreviation Pair :: "[t, t] \<Rightarrow> t" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_: A. B" |