From 76b57317d7568f4dcd673b1b8085601c6c723355 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 11 Feb 2019 22:44:21 +0100 Subject: Organize this commit as a backup of the work on type inference done so far; learnt that I probably need to take a different approach. In particular, should first make the constants completely monomorphic, and then work on full proper type inference, rather than the heuristic approach taken here. --- Prod.thy | 24 ++++++++++++------------ Projections.thy | 46 ++++++++++++++++++++++++---------------------- Sum.thy | 51 ++++++++++++++++++++++++--------------------------- 3 files changed, 60 insertions(+), 61 deletions(-) diff --git a/Prod.thy b/Prod.thy index 05eff43..4235793 100644 --- a/Prod.thy +++ b/Prod.thy @@ -18,13 +18,13 @@ axiomatization \ \Application should bind tighter than abstraction.\ syntax - "_Prod" :: "[idt, t, t] \ t" ("(3TT '(_: _')./ _)" 30) - "_Prod'" :: "[idt, t, t] \ t" ("(3TT _: _./ _)" 30) + "_Prod" :: "[idt, t, t] \ t" ("(3\'(_: _')./ _)" 30) + "_Prod'" :: "[idt, t, t] \ t" ("(3\_: _./ _)" 30) "_lam" :: "[idt, t, t] \ t" ("(3\'(_: _')./ _)" 30) "_lam'" :: "[idt, t, t] \ t" ("(3\_: _./ _)" 30) translations - "TT(x: A). B" \ "(CONST Prod) A (\x. B)" - "TT x: A. B" \ "(CONST Prod) A (\x. B)" + "\(x: A). B" \ "(CONST Prod) A (\x. B)" + "\x: A. B" \ "(CONST Prod) A (\x. B)" "\(x: A). b" \ "(CONST lam) A (\x. b)" "\x: A. b" \ "(CONST lam) A (\x. b)" @@ -35,25 +35,25 @@ 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 \ TT(_: A). B" +where "A \ B \ \(_: A). B" axiomatization where \ \Type rules\ - Prod_form: "\A: U i; B: A \ U i\ \ TT x: A. B x: U i" and + 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: TT x: A. B x" and + Prod_intro: "\A: U i; \x. x: A \ b x: B x\ \ \x: A. b x: \x: A. B x" and - Prod_elim: "\f: TT x: A. B x; a: A\ \ f`a: B a" and + Prod_elim: "\f: \x: A. B x; a: A\ \ f`a: B a" and Prod_cmp: "\\x. x: A \ b x: B x; a: A\ \ (\x: A. b x)`a \ b a" and - Prod_uniq: "f: TT x: A. B x \ \x: A. f`x \ f" and + Prod_uniq: "f: \x: A. B x \ \x: A. f`x \ f" and \ \Congruence rules\ Prod_form_eq: "\A: U i; B: A \ U i; C: A \ U i; \x. x: A \ B x \ C x\ - \ TT x: A. B x \ TT x: A. C x" and + \ \x: A. B x \ \x: A. C x" and Prod_intro_eq: "\\x. x: A \ b x \ c x; A: U i\ \ \x: A. b x \ \x: A. c x" @@ -107,14 +107,14 @@ print_translation \ let fun compose_tr' ctxt [A, g, f] = if Config.get ctxt pretty_compose then Syntax.const @{syntax_const "_compose"} $ g $ f - else Const ("compose", Syntax.read_typ ctxt "t \ t \ t") $ A $ g $ f + else @{const compose} $ A $ g $ f in [(@{const_syntax compose}, compose_tr')] end \ lemma compose_assoc: - assumes "A: U i" and "f: A \ B" and "g: B \ C" and "h: TT x: C. D x" + assumes "A: U i" and "f: A \ B" and "g: B \ C" and "h: \x: C. D x" shows "compose A (compose B h g) f \ compose A h (compose A g f)" by (derive lems: assms cong) diff --git a/Projections.thy b/Projections.thy index 509402b..c819240 100644 --- a/Projections.thy +++ b/Projections.thy @@ -1,43 +1,45 @@ -(* -Title: Projections.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Projections +Feb 2019 -Projection functions \fst\ and \snd\ for the dependent sum type. -*) +Projection functions for the dependent sum type. + +********) theory Projections imports HoTT_Methods Prod Sum begin - -definition fst :: "t \ t" where "fst p \ ind\<^sub>\ (\x y. x) p" -definition snd :: "t \ t" where "snd p \ ind\<^sub>\ (\x y. y) p" +definition fst :: "[t, t] \ t" where "fst A p \ indSum (\_. A) (\x y. x) p" lemma fst_type: - assumes "A: U i" and "B: A \ U i" and "p: \x:A. B x" shows "fst p: A" + assumes "A: U i" and "p: \x: A. B x" shows "fst A p: A" unfolding fst_def by (derive lems: assms) -lemma fst_comp: - assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "fst \ a" +declare fst_type [intro] + +lemma fst_cmp: + assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "fst A \ a" unfolding fst_def by compute (derive lems: assms) -lemma snd_type: - assumes "A: U i" and "B: A \ U i" and "p: \x:A. B x" shows "snd p: B (fst p)" -unfolding snd_def proof (derive lems: assms) - show "\p. p: \x:A. B x \ fst p: A" using assms(1-2) by (rule fst_type) +declare fst_cmp [comp] - fix x y assume asm: "x: A" "y: B x" - show "y: B (fst )" by (derive lems: asm assms fst_comp) +definition snd :: "[t, t \ t, t] \ t" where "snd A B p \ indSum (\p. B (fst A p)) (\x y. y) p" + +lemma snd_type: + assumes "A: U i" and "B: A \ U i" and "p: \x: A. B x" shows "snd A B p: B (fst A p)" +unfolding snd_def proof (routine add: assms) + fix x y assume "x: A" and "y: B x" + with assms have [comp]: "fst A \ x" by derive + note \y: B x\ then show "y: B (fst A )" by compute qed -lemma snd_comp: - assumes "A: U i" and "B: A \ U i" and "a: A" and "b: B a" shows "snd \ b" +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_comp snd_comp - +lemmas Proj_comps [comp] = fst_cmp snd_cmp end diff --git a/Sum.thy b/Sum.thy index 2646c97..9549a5e 100644 --- a/Sum.thy +++ b/Sum.thy @@ -1,59 +1,56 @@ -(* -Title: Sum.thy -Author: Joshua Chen -Date: 2018 +(******** +Isabelle/HoTT: Dependent sum (dependent pair) +Feb 2019 -Dependent sum type -*) +********) theory Sum imports HoTT_Base begin - axiomatization - Sum :: "[t, tf] \ t" and + Sum :: "[t, t \ t] \ t" and pair :: "[t, t] \ t" ("(1<_,/ _>)") and - indSum :: "[[t, t] \ t, t] \ t" ("(1ind\<^sub>\)") + indSum :: "[t \ t, [t, t] \ t, t] \ t" syntax - "_sum" :: "[idt, t, t] \ t" ("(3\_:_./ _)" 20) - "_sum_ascii" :: "[idt, t, t] \ t" ("(3SUM _:_./ _)" 20) - + "_Sum" :: "[idt, t, t] \ t" ("(3\'(_: _')./ _)" 20) + "_Sum'" :: "[idt, t, t] \ t" ("(3\_: _./ _)" 20) translations - "\x:A. B" \ "CONST Sum A (\x. B)" - "SUM 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" + where "A \ B \ \_: A. B" axiomatization where \ \Type rules\ - Sum_form: "\A: U i; B: A \ U i\ \ \x:A. B x: U i" and + Sum_form: "\A: U i; \x. x: A \ B x: U i\ \ \x: A. B x: U i" and - Sum_intro: "\B: A \ U i; a: A; b: B a\ \ : \x:A. B x" and + Sum_intro: "\\x. x: A \ B x: U i; a: A; b: B a\ \ : \x: A. B x" and Sum_elim: "\ - p: \x:A. B x; - C: \x:A. B x \ U i; - \x y. \x: A; y: B x\ \ f x y: C \ \ ind\<^sub>\ f p: C p" and + p: \x: A. B x; + C: \x: A. B x \ U i; + \x y. \x: A; y: B x\ \ f x y: C \ \ indSum C f p: C p" and - Sum_comp: "\ + Sum_cmp: "\ a: A; b: B a; - B: A \ U i; - C: \x:A. B x \ U i; - \x y. \x: A; y: B(x)\ \ f x y: C \ \ ind\<^sub>\ f \ f a b" and + B: A \ U i; + C: \x: A. B x \ U i; + \x y. \x: A; y: B x\ \ f x y: C \ \ indSum C f \ f a b" and \ \Congruence rules\ - Sum_form_eq: "\A: U i; B: A \ U i; C: A \ U i; \x. x: A \ B x \ C x\ \ \x:A. B x \ \x:A. C x" + Sum_form_eq: "\A: U i; B: A \ U i; C: A \ U i; \x. x: A \ B x \ C x\ + \ \x: A. B x \ \x: A. C x" lemmas Sum_form [form] lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim -lemmas Sum_comp [comp] - +lemmas Sum_comp [comp] = Sum_cmp +lemmas Sum_cong [cong] = Sum_form_eq end -- cgit v1.2.3