From 3bcaf5d1c40b513f8e4590f7d38d3eef8393092e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 16 Jul 2020 16:46:09 +0200 Subject: Checkpoint. THIS BUILD WILL FAIL --- spartan/core/Spartan.thy | 105 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 75 insertions(+), 30 deletions(-) (limited to 'spartan/core/Spartan.thy') diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 8fa6cfe..1b9093b 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -10,22 +10,29 @@ keywords "focus" "\" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and "congruence" "print_coercions" :: thy_decl and "rhs" "derive" "prems" "vars" :: quasi_command - begin section \Prelude\ +paragraph \Set up the meta-logic just so.\ + +paragraph \Notation.\ + declare [[eta_contract=false]] +text \ + Rebind notation for meta-lambdas since we want to use `\` for the object + lambdas. Meta-functions now use the binder `fn`. +\ setup \ let val typ = Simple_Syntax.read_typ fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range) in Sign.del_syntax (Print_Mode.ASCII, true) - [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3fn _./ _)", [0, 3], 3))] + [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3%_./ _)", [0, 3], 3))] #> Sign.del_syntax Syntax.mode_default [("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3\_./ _)", [0, 3], 3))] #> Sign.add_syntax Syntax.mode_default @@ -38,11 +45,16 @@ translations "a $ b" \ "a (b)" abbreviation (input) K where "K x \ fn _. x" +paragraph \ + Deeply embed dependent type theory: meta-type of expressions, and typing + judgment. +\ + typedecl o judgment has_type :: \o \ o \ prop\ ("(2_:/ _)" 999) -text \Type annotations:\ +text \Type annotations for type-checking and inference.\ definition anno :: \o \ o \ o\ ("'(_ : _')") where "(a : A) \ a" if "a: A" @@ -51,7 +63,9 @@ lemma anno: "a: A \ (a : A): A" by (unfold anno_def) -section \Universes\ +section \Axioms\ + +subsection \Universes\ typedecl lvl \ \Universe levels\ @@ -77,7 +91,7 @@ lemma lift_U: by (erule U_cumulative, rule lt_S) -section \\-type\ +subsection \\-type\ axiomatization Pi :: \o \ (o \ o) \ o\ and @@ -100,9 +114,9 @@ translations abbreviation Fn (infixr "\" 40) where "A \ B \ \_: A. B" axiomatization where - PiF: "\\x. x: A \ B x: U i; A: U i\ \ \x: A. B x: U i" and + PiF: "\A: U i; \x. x: A \ B x: U i\ \ \x: A. B x: U i" and - PiI: "\\x. x: A \ b x: B x; A: U i\ \ \x: A. b x: \x: A. B x" and + PiI: "\A: U i; \x. x: A \ b x: B x\ \ \x: A. b x: \x: A. B x" and PiE: "\f: \x: A. B x; a: A\ \ f `a: B a" and @@ -113,14 +127,14 @@ axiomatization where Pi_cong: "\ \x. x: A \ B x \ B' x; A: U i; - \x. x: A \ B x: U i; - \x. x: A \ B' x: U i + \x. x: A \ B x: U j; + \x. x: A \ B' x: U j \ \ \x: A. B x \ \x: A. B' x" and lam_cong: "\\x. x: A \ b x \ c x; A: U i\ \ \x: A. b x \ \x: A. c x" -section \\-type\ +subsection \\-type\ axiomatization Sig :: \o \ (o \ o) \ o\ and @@ -138,16 +152,16 @@ abbreviation "and" (infixl "\" 60) where "A \ B \ A \ B" axiomatization where - SigF: "\\x. x: A \ B x: U i; A: U i\ \ \x: A. B x: U i" and + SigF: "\A: U i; \x. x: A \ B x: U i\ \ \x: A. B x: U i" and SigI: "\\x. x: A \ B x: U i; a: A; b: B a\ \ : \x: A. B x" and SigE: "\ p: \x: A. B x; A: U i; - \x. x : A \ B x: U i; - \x y. \x: A; y: B x\ \ f x y: C ; - \p. p: \x: A. B x \ C p: U i + \x. x : A \ B x: U j; + \p. p: \x: A. B x \ C p: U k; + \x y. \x: A; y: B x\ \ f x y: C \ \ SigInd A (fn x. B x) (fn p. C p) f p: C p" and Sig_comp: "\ @@ -161,22 +175,23 @@ axiomatization where Sig_cong: "\ \x. x: A \ B x \ B' x; A: U i; - \x. x : A \ B x: U i; - \x. x : A \ B' x: U i + \x. x : A \ B x: U j; + \x. x : A \ B' x: U j \ \ \x: A. B x \ \x: A. B' x" section \Infrastructure\ ML_file \lib.ML\ -ML_file \typechecking.ML\ +ML_file \context_tactical.ML\ subsection \Proof commands\ +ML_file \focus.ML\ + named_theorems typechk ML_file \goals.ML\ -ML_file \focus.ML\ subsection \Congruence automation\ @@ -184,19 +199,22 @@ consts "rhs" :: \'a\ ("..") ML_file \congruence.ML\ +subsection \Theorem attributes, type-checking and proof methods\ + +named_theorems intros and comps + ML_file \elimination.ML\ \ \elimination rules\ ML_file \cases.ML\ \ \case reasoning rules\ -subsection \Methods\ - -named_theorems intros and comps lemmas - [intros] = PiF PiI SigF SigI and + [intros] = anno PiF PiI SigF SigI and [elims "?f"] = PiE and [elims "?p"] = SigE and [comps] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong +ML_file \typechecking.ML\ +ML_file \tactics2.ML\ ML_file \tactics.ML\ method_setup assumptions = @@ -223,12 +241,12 @@ method_setup cases = \Args.term >> (fn tm => fn ctxt => SIMPLE_METHOD' (cases_tac tm ctxt))\ (*This could possibly use additional simplification hints via a simp: modifier*) -method_setup typechk = +method_setup typechk' = \Scan.succeed (fn ctxt => SIMPLE_METHOD' ( SIDE_CONDS (typechk_tac ctxt) ctxt)) (* CHANGED (ALLGOALS (TRY o typechk_tac ctxt)))) *)\ -method_setup rule = +method_setup rule' = \Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (rule_tac ths ctxt) ctxt)))\ @@ -237,6 +255,16 @@ method_setup dest = >> (fn (opt_n, ths) => fn ctxt => SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (dest_tac opt_n ths ctxt) ctxt)))\ +(*NEW*) +method_setup typechk = + \Scan.succeed (K (CONTEXT_METHOD ( + CHEADGOAL o Types.check_infer)))\ + +method_setup rule = + \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( + CHEADGOAL o Tactics2.SIDE_CONDS (Tactics2.rule_tac ths))))\ + + subsection \Reflexivity\ named_theorems refl @@ -348,12 +376,21 @@ lemma eta_exp: shows "f \ \x: A. f x" by (rule eta[symmetric]) +lemma refine_codomain: + assumes + "A: U i" + "f: \x: A. B x" + "\x. x: A \ f `x: C x" + shows "f: \x: A. C x" + by (subst eta_exp) + lemma lift_universe_codomain: assumes "A: U i" "f: A \ U j" shows "f: A \ U (S j)" - apply (sub eta_exp) - apply known - apply (Pure.rule intros; rule lift_U) + (*FIXME: Temporary; should be fixed once all methods are rewritten to use + the new typechk*) + apply (Pure.rule refine_codomain, typechk, typechk) + apply (Pure.rule lift_U, typechk) done subsection \Function composition\ @@ -472,7 +509,7 @@ definition fst_i ("fst") definition snd_i ("snd") where [implicit]: "snd \ Spartan.snd ? ?" -translations +no_translations "fst" \ "CONST Spartan.fst A B" "snd" \ "CONST Spartan.snd A B" @@ -483,14 +520,22 @@ Lemma fst [typechk]: "p: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" shows "fst p: A" - by typechk + \ \This can't be solved by a single application of `typechk`; it needs + multiple (two) passes. Something to do with constraint/subgoal reordering.\ + apply (Pure.rule elims) + apply (Pure.rule typechk) + apply known [1] + defer \ \The deferred subgoal is an inhabitation problem.\ + apply known [1] + by known + Lemma snd [typechk]: assumes "p: \x: A. B x" "A: U i" "\x. x: A \ B x: U i" shows "snd p: B (fst p)" - by typechk + by typechk+ method fst for p::o = rule fst[of p] method snd for p::o = rule snd[of p] -- cgit v1.2.3