diff options
| -rw-r--r-- | Equal.thy | 2 | ||||
| -rw-r--r-- | EqualProps.thy | 21 | ||||
| -rw-r--r-- | HoTT_Base.thy | 10 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 47 | ||||
| -rw-r--r-- | Prod.thy | 2 | ||||
| -rw-r--r-- | Sum.thy | 2 | ||||
| -rw-r--r-- | scratch.thy | 55 |
7 files changed, 110 insertions, 29 deletions
@@ -53,7 +53,9 @@ and \<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> f a" lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp +lemmas Equal_elims [dest] = Equal_elim lemmas Equal_form_conds [elim, wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 +lemmas Equal_comps [comp] = Equal_comp end
\ No newline at end of file diff --git a/EqualProps.thy b/EqualProps.thy index 8960a90..2807587 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -66,27 +66,6 @@ lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" -proof (unfold rcompose_def) - show "(\<^bold>\<lambda>p:a =[A] a. - lambda (a =[A] a) - (op ` - ((\<^bold>\<lambda>x:A. - \<^bold>\<lambda>y:A. - lambda (x =[A] y) - (indEqual[A] - (\<lambda>x y _. \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z) - (\<lambda>x. \<^bold>\<lambda>z:A. - lambda (x =[A] z) - (indEqual[A] (\<lambda>x z _. x =[A] z) refl x z)) - x y)) ` - a ` - a ` - p ` - a))) ` - refl(a) ` - refl(a) \<equiv> - refl(a)" - sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close> diff --git a/HoTT_Base.thy b/HoTT_Base.thy index eaebfb0..cfced79 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -12,9 +12,13 @@ begin section \<open>Setup\<close> -text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments, to be used by proof methods later (see HoTT_Methods.thy)." +text "Named theorems to be used by proof methods later (see HoTT_Methods.thy). + +\<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while +\<open>comp\<close> declares computation rules used when simplifying function application." named_theorems wellform +named_theorems comp section \<open>Metalogical definitions\<close> @@ -32,8 +36,8 @@ text "We formalize the judgments \<open>a : A\<close> and \<open>A : U\<close> s For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it." consts - is_a_type :: "Term \<Rightarrow> prop" ("(1_ :/ U)" [0] 1000) - is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) + is_a_type :: "Term \<Rightarrow> prop" ("(1_ : U)" [0] 1000) + is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ : _)" [0, 0] 1000) text "The following fact is used to make explicit the assumption of well-formed contexts." diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 20f3ece..81e2055 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -10,6 +10,7 @@ theory HoTT_Methods "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" HoTT_Base + Prod begin @@ -19,17 +20,17 @@ text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<ope Can also perform typechecking, and search for elements of a type." -method simple uses lems = (assumption|standard|rule lems)+ +method simple uses lems = (assumption | standard | rule lems)+ text "Find a proof of any valid typing judgment derivable from a given wellformed judgment." -method wellformed uses jdgmt = ( +\<comment> \<open>\<open>wellform\<close> is declared in HoTT_Base.thy\<close> +method wellformed uses jdgmt declares wellform = match wellform in rl: "PROP ?P" \<Rightarrow> \<open>( catch \<open>rule rl[OF jdgmt]\<close> \<open>fail\<close> | catch \<open>wellformed jdgmt: rl[OF jdgmt]\<close> \<open>fail\<close> )\<close> - ) text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations. @@ -45,7 +46,45 @@ method derive uses lems unfolds = ( )+ -text "Simplify function applications." +text "Simplify a function application." + +method simplify for expr::Term uses lems = match (expr) in + "(\<^bold>\<lambda>x:?A. ?b x)`?a" \<Rightarrow> \<open> + print_term "Single application", + rule Prod_comp, + derive lems: lems + \<close> \<bar> + "(F`a)`b" for F a b \<Rightarrow> \<open> + print_term "Repeated application", + simplify "F`a" + \<close> + + + +text "Verify a function application simplification." + +method verify_simp uses lems = ( + print_term "Attempting simplification", + ( rule comp | derive lems: lems | simp add: lems )+ + | print_fact lems, + match conclusion in + "F`a`b \<equiv> x" for F a b x \<Rightarrow> \<open> + print_term "Chained application", + print_term F, + print_term a, + print_term b, + print_term x, + match (F) in + "\<^bold>\<lambda>x:A. f x" for A f \<Rightarrow> \<open> + print_term "Matched abstraction", + print_fact Prod_comp[where ?A = A and ?b = f and ?a = a] + \<close> \<bar> + "?x" \<Rightarrow> \<open> + print_term "Constant application", + print_fact comp + \<close> + \<close> + ) end
\ No newline at end of file @@ -59,7 +59,9 @@ This is what the additional formation rules \<open>Prod_form_cond1\<close> and \ text "The type rules should be able to be used as introduction and elimination rules by the standard reasoner:" lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +lemmas Prod_elims [elim] = Prod_elim lemmas Prod_form_conds [elim, wellform] = Prod_form_cond1 Prod_form_cond2 +lemmas Prod_comps [comp] = Prod_comp Prod_uniq text "Nondependent functions are a special case." @@ -51,7 +51,9 @@ and \<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b" lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp +lemmas Sum_elims [dest] = Sum_elim \<comment> \<open>Declaring positively-presented dependent elimination rule as [dest] instead of [elim] arguably makes more sense.\<close> lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2 +lemmas Sum_comps [comp] = Sum_comp \<comment> \<open>Nondependent pair\<close> abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) diff --git a/scratch.thy b/scratch.thy index b90fd59..1c921bd 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,6 +3,59 @@ theory scratch begin -schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" by simple +(* Typechecking *) +schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A" by simple + + +(* Simplification *) + +notepad begin + +assume asm: + "f`a \<equiv> g" + "g`b \<equiv> \<^bold>\<lambda>x:A. d" + "c : A" + "d : B" + +have "f`a`b`c \<equiv> d" by (simp add: asm | rule comp | derive lems: asm)+ + +end + +lemma "a : A \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" + by verify_simp + +lemma "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" + by verify_simp + +lemma + assumes "a : A" and "\<And>x. x : A \<Longrightarrow> b x : B x" + shows "(\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" + by (verify_simp lems: assms) + +lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" +oops + +lemma + assumes + "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a \<equiv> \<^bold>\<lambda>y:B a. c a y" + "(\<^bold>\<lambda>y:B a. c a y)`b \<equiv> c a b" + shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" +apply (simp add: assms) +done + +lemmas lems = + Prod_comp[where ?A = "B a" and ?b = "\<lambda>b. c a b" and ?a = b] + Prod_comp[where ?A = A and ?b = "\<lambda>x. \<^bold>\<lambda>y:B x. c x y" and ?a = a] + +lemma + assumes + "a : A" + "b : B a" + "B: A \<rightarrow> U" + "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y" + shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" +apply (verify_simp lems: assms) + + end
\ No newline at end of file |