From 68aa069172933b875d70a5ef71e9db0ae685a92d Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 17 Feb 2019 18:34:38 +0100 Subject: Method "quantify" converts product inhabitation into Pure universal statements. Also misc. cleanups. --- Equal.thy | 95 +++++++++++++++++++++++++++++++++++++++++++------------- HoTT_Base.thy | 13 +++++--- HoTT_Methods.thy | 29 ++++++++++++----- Prod.thy | 28 +++++++++++++++-- Projections.thy | 4 +-- Sum.thy | 4 +-- 6 files changed, 132 insertions(+), 41 deletions(-) diff --git a/Equal.thy b/Equal.thy index 99ff268..1d8f6ae 100644 --- a/Equal.thy +++ b/Equal.thy @@ -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 \Basic definitions\ +section \Type definitions\ axiomatization - Equal :: "[t, t, t] \ t" and - refl :: "t \ t" and - indEqual :: "[t \ t, t] \ t" ("(1ind\<^sub>=)") + Eq :: "[t, t, t] \ t" and + refl :: "t \ t" and + indEq :: "[[t, t, t] \ t, t \ t, t] \ t" syntax - "_equal" :: "[t, t, t] \ t" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) - "_equal_ascii" :: "[t, t, t] \ t" ("(3_ =[_]/ _)" [101, 0, 101] 100) - + "_Eq" :: "[t, t, t] \ t" ("(3_ =[_]/ _)" [101, 0, 101] 100) translations - "a =[A] b" \ "CONST Equal A a b" - "a =\<^sub>A b" \ "CONST Equal A a b" + "a =[A] b" \ "(CONST Eq) A a b" axiomatization where - Equal_form: "\A: U i; a: A; b: A\ \ a =\<^sub>A b : U i" and + Equal_form: "\A: U i; a: A; b: A\ \ a =[A] b: U i" and - Equal_intro: "a : A \ (refl a): a =\<^sub>A a" and + Equal_intro: "a: A \ (refl a): a =[A] a" and Equal_elim: "\ - p: x =\<^sub>A y; + p: x =[A] y; x: A; y: A; \x. x: A \ f x: C x x (refl x); - \x y. \x: A; y: A\ \ C x y: x =\<^sub>A y \ U i \ \ ind\<^sub>= f p : C x y p" and + \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f p : C x y p" and Equal_comp: "\ a: A; \x. x: A \ f x: C x x (refl x); - \x y. \x: A; y: A\ \ C x y: x =\<^sub>A y \ U i \ \ ind\<^sub>= f (refl a) \ f a" + \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f (refl a) \ f a" lemmas Equal_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim lemmas Equal_comp [comp] +section \Path induction\ + +text \We set up rudimentary automation of path induction:\ + +method path_ind for x y p :: t = + (rule Equal_elim[where ?x=x and ?y=y and ?p=p]; (fact | assumption)?) + + +section \Properties of equality\ + +subsection \Symmetry (path inverse)\ + +definition inv :: "[t, t] \ t" +where "inv A p \ indEq (\x y. ^(y =[A] x)) (\x. refl x) p" + +lemma inv_type: "\A: U i; x: A; y: A; p: x =[A] y\ \ inv A p: y =[A] x" +unfolding inv_def by derive + +lemma inv_comp: "\A: U i; a: A\ \ inv A (refl a) \ refl a" +unfolding inv_def by derive + +declare + inv_type [intro] + inv_comp [comp] + +subsection \Transitivity (path composition)\ + +schematic_goal transitivity: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?p: \z: A. y =[A]z \ x =[A] z" +proof (path_ind x y p, quantify 2) + fix x z show "\p. p: x =[A] z \ p: x =[A] z" . +qed (routine add: assms) + + +syntax "_pathcomp" :: "[t, t] \ t" (infixl "\" 110) +translations "p \ q" \ "CONST pathcomp`p`q" + +lemma pathcomp_type: + assumes "A: U i" "x: A" "y: A" "z: A" + shows "pathcomp: x =\<^sub>A y \ (y =\<^sub>A z) \ (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 \ q: x =\<^sub>A z" +by (routine add: assms pathcomp_type) + +lemma pathcomp_comp: + assumes "A: U i" and "a: A" + shows "(refl a) \ (refl a) \ 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. \ -section \Type families\ +section \Notation\ 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.\ +abbreviation (input) K_combinator :: "'a \ 'b \ 'a" ("^_" [1000]) +where "^A \ \_. A" + section \Named theorems\ 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 \More method combinators\ + +ML \ +(* 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 +\ + + section \Substitution and simplification\ 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 \Induction\ - -text \ -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}. -\ - end diff --git a/Prod.thy b/Prod.thy index 4235793..a843c7a 100644 --- a/Prod.thy +++ b/Prod.thy @@ -9,6 +9,7 @@ imports HoTT_Base HoTT_Methods begin + section \Basic type definitions\ axiomatization @@ -35,14 +36,14 @@ The syntax translations above bind the variable @{term x} in the expressions @{t text \Non-dependent functions are a special case:\ abbreviation Fun :: "[t, t] \ t" (infixr "\" 40) -where "A \ B \ \(_: A). B" +where "A \ B \ \_: A. B" axiomatization where \ \Type rules\ Prod_form: "\A: U i; B: A \ U i\ \ \x: A. B x: U i" and - Prod_intro: "\A: U i; \x. x: A \ b x: B x\ \ \x: A. b x: \x: A. B x" and + Prod_intro: "\\x. x: A \ b x: B x; A: U i\ \ \x: A. b x: \x: A. B x" and Prod_elim: "\f: \x: A. B x; a: A\ \ 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 \Universal quantification\ + +text \ +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: \x1: A1. ... \xn: An. B x1 ... xn"}, +where @{term B} is not a product, to +@{text "\x1 ... xn . \x1: A1; ...; xn: An\ \ ?b x1 ... xn: B x1 ... xn"}. + +Method @{theory_text "quantify k"} does the same, but only for the first k unknowns. +\ + +method_setup quantify = \repeat (fn ctxt => Method.rule_tac ctxt [@{thm Prod_intro}] [] 1)\ + +method quantify_all = (rule Prod_intro)+ + + section \Function composition\ definition compose :: "[t, t, t] \ t" @@ -76,6 +96,7 @@ where "compose A g f \ \x: A. g`(f`x)" declare compose_def [comp] syntax "_compose" :: "[t, t] \ t" (infixr "o" 110) +(* parse_translation \ let fun compose_tr ctxt [g, f] = let @@ -98,6 +119,7 @@ in [("_compose", compose_tr)] end \ +*) text \Pretty-printing switch for composition; hides domain type information.\ @@ -120,7 +142,7 @@ by (derive lems: assms cong) lemma compose_comp: assumes "A: U i" and "\x. x: A \ b x: B" and "\x. x: B \ c x: C x" - shows "(\x: B. c x) o (\x: A. b x) \ \x: A. c (b x)" + shows "compose A (\x: B. c x) (\x: A. b x) \ \x: A. c (b x)" by (derive lems: assms cong) abbreviation id :: "t \ t" where "id A \ \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 \ U i" and "a: A" and "b: B a" shows "snd A B \ 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 diff --git a/Sum.thy b/Sum.thy index 9549a5e..ee132b3 100644 --- a/Sum.thy +++ b/Sum.thy @@ -18,8 +18,8 @@ syntax "_Sum" :: "[idt, t, t] \ t" ("(3\'(_: _')./ _)" 20) "_Sum'" :: "[idt, t, t] \ t" ("(3\_: _./ _)" 20) translations - "\(x: A). B" \ "CONST Sum A (\x. B)" - "\x: A. B" \ "CONST Sum A (\x. B)" + "\(x: A). B" \ "(CONST Sum) A (\x. B)" + "\x: A. B" \ "(CONST Sum) A (\x. B)" abbreviation Pair :: "[t, t] \ t" (infixr "\" 50) where "A \ B \ \_: A. B" -- cgit v1.2.3