From 76deb7ae15fa00b5498ab43db020a0364499251e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 6 Jul 2018 10:48:41 +0200 Subject: Added attributes to type elimination rules, not sure if these will actually be needed or useful later. Added [comp] attribute to be used by simplification met methods. --- Equal.thy | 2 ++ EqualProps.thy | 21 --------------------- HoTT_Base.thy | 10 +++++++--- HoTT_Methods.thy | 47 +++++++++++++++++++++++++++++++++++++++++++---- Prod.thy | 2 ++ Sum.thy | 2 ++ scratch.thy | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- 7 files changed, 110 insertions(+), 29 deletions(-) diff --git a/Equal.thy b/Equal.thy index 51a69ae..cb4d4f1 100644 --- a/Equal.thy +++ b/Equal.thy @@ -53,7 +53,9 @@ and \ \ indEqual[A] C f a a refl(a) \ 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) \ refl(a)" -proof (unfold rcompose_def) - show "(\<^bold>\p:a =[A] a. - lambda (a =[A] a) - (op ` - ((\<^bold>\x:A. - \<^bold>\y:A. - lambda (x =[A] y) - (indEqual[A] - (\x y _. \z:A. y =[A] z \ x =[A] z) - (\x. \<^bold>\z:A. - lambda (x =[A] z) - (indEqual[A] (\x z _. x =[A] z) refl x z)) - x y)) ` - a ` - a ` - p ` - a))) ` - refl(a) ` - refl(a) \ - refl(a)" - sorry \ \Long and tedious proof if the Simplifier is not set up.\ 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 \Setup\ -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). + +\wellform\ declares necessary wellformedness conditions for type and inhabitation judgments, while +\comp\ declares computation rules used when simplifying function application." named_theorems wellform +named_theorems comp section \Metalogical definitions\ @@ -32,8 +36,8 @@ text "We formalize the judgments \a : A\ and \A : U\ s For judgmental equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it." consts - is_a_type :: "Term \ prop" ("(1_ :/ U)" [0] 1000) - is_of_type :: "[Term, Term] \ prop" ("(1_ :/ _)" [0, 0] 1000) + is_a_type :: "Term \ prop" ("(1_ : U)" [0] 1000) + is_of_type :: "[Term, Term] \ 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 \A : U\ and inhabitation judgments \ \\wellform\ is declared in HoTT_Base.thy\ +method wellformed uses jdgmt declares wellform = match wellform in rl: "PROP ?P" \ \( catch \rule rl[OF jdgmt]\ \fail\ | catch \wellformed jdgmt: rl[OF jdgmt]\ \fail\ )\ - ) text "Combine \simple\ and \wellformed\ 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>\x:?A. ?b x)`?a" \ \ + print_term "Single application", + rule Prod_comp, + derive lems: lems + \ \ + "(F`a)`b" for F a b \ \ + print_term "Repeated application", + simplify "F`a" + \ + + + +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 \ x" for F a b x \ \ + print_term "Chained application", + print_term F, + print_term a, + print_term b, + print_term x, + match (F) in + "\<^bold>\x:A. f x" for A f \ \ + print_term "Matched abstraction", + print_fact Prod_comp[where ?A = A and ?b = f and ?a = a] + \ \ + "?x" \ \ + print_term "Constant application", + print_fact comp + \ + \ + ) end \ No newline at end of file diff --git a/Prod.thy b/Prod.thy index 7155a10..9e1c1c3 100644 --- a/Prod.thy +++ b/Prod.thy @@ -59,7 +59,9 @@ This is what the additional formation rules \Prod_form_cond1\ 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." diff --git a/Sum.thy b/Sum.thy index 1e6e6b0..93fa791 100644 --- a/Sum.thy +++ b/Sum.thy @@ -51,7 +51,9 @@ and \ \ indSum[A,B] C f (a,b) \ f a b" lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp +lemmas Sum_elims [dest] = Sum_elim \ \Declaring positively-presented dependent elimination rule as [dest] instead of [elim] arguably makes more sense.\ lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2 +lemmas Sum_comps [comp] = Sum_comp \ \Nondependent pair\ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 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 "\a : A; b : B\ \ ?x : A \ B" by simple +(* Typechecking *) +schematic_goal "\a : A; b : B\ \ (a,b) : ?A" by simple + + +(* Simplification *) + +notepad begin + +assume asm: + "f`a \ g" + "g`b \ \<^bold>\x:A. d" + "c : A" + "d : B" + +have "f`a`b`c \ d" by (simp add: asm | rule comp | derive lems: asm)+ + +end + +lemma "a : A \ indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a) \ refl(a)" + by verify_simp + +lemma "\a : A; \x. x : A \ b x : X\ \ (\<^bold>\x:A. b x)`a \ b a" + by verify_simp + +lemma + assumes "a : A" and "\x. x : A \ b x : B x" + shows "(\<^bold>\x:A. b x)`a \ b a" + by (verify_simp lems: assms) + +lemma "\a : A; b : B a; B: A \ U\ \ (\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" +oops + +lemma + assumes + "(\<^bold>\x:A. \<^bold>\y:B x. c x y)`a \ \<^bold>\y:B a. c a y" + "(\<^bold>\y:B a. c a y)`b \ c a b" + shows "(\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" +apply (simp add: assms) +done + +lemmas lems = + Prod_comp[where ?A = "B a" and ?b = "\b. c a b" and ?a = b] + Prod_comp[where ?A = A and ?b = "\x. \<^bold>\y:B x. c x y" and ?a = a] + +lemma + assumes + "a : A" + "b : B a" + "B: A \ U" + "\x y. \x : A; y : B x\ \ c x y : D x y" + shows "(\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" +apply (verify_simp lems: assms) + + end \ No newline at end of file -- cgit v1.2.3