From 302279e6d1e19d757b64d656b1528faada313c28 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 24 Oct 2023 19:58:32 +1100 Subject: [PATCH] =?UTF-8?q?Some=20progress=20towards=20subformula=20proper?= =?UTF-8?q?ty=20of=20simply-typed=20=CE=BB-calculus?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- examples/lambda/typing/sttScript.sml | 342 +++++++++++++++++++++++++-- 1 file changed, 323 insertions(+), 19 deletions(-) diff --git a/examples/lambda/typing/sttScript.sml b/examples/lambda/typing/sttScript.sml index 3904619a1f..6ca5a6bc4d 100644 --- a/examples/lambda/typing/sttScript.sml +++ b/examples/lambda/typing/sttScript.sml @@ -3,10 +3,12 @@ open binderLib nomsetTheory metisLib termTheory contextlistsTheory open chap3Theory open sortingTheory open appFOLDLTheory standardisationTheory +open pred_setTheory val _ = new_theory "stt"; val _ = remove_ovl_mapping "B" {Name="B", Thy="chap2"} +val _ = remove_ovl_mapping "C" {Name="C", Thy="chap2"} (* define simple types, the "funspace" constructor will get to be written as infix "-->". @@ -15,7 +17,7 @@ Datatype: stype = base | funspace stype stype End Overload "-->" = “funspace” -val _ = Unicode.unicode_version{u = Unicode.UChar.rightarrow, tmnm = "-->"} +val _ = Parse.Unicode.unicode_version{u = Unicode.UChar.rightarrow,tmnm = "-->"} (* set up parsing/pretty-printing for the typing relation. Can't use ":" to the right of the turnstile, because it's already taken @@ -280,10 +282,36 @@ Proof Induct_on ‘A’ >> simp[] QED +Theorem subtype_trans: + ∀A B C. subtype A B ∧ subtype B C ⇒ subtype A C +Proof + Induct_on ‘C’ >> simp[] >> rw[] >> gvs[] >> metis_tac[] +QED + +Theorem subtype_size: + ∀A B. subtype A B ⇒ stype_size A ≤ stype_size B +Proof + Induct_on ‘B’ >> simp[] >> rpt strip_tac >> + res_tac >> simp[definition "stype_size_def"] +QED + +Theorem subtype_eqsize: + ∀A B. subtype A B ∧ stype_size A = stype_size B ⇒ A = B +Proof + Induct_on ‘B’ >> simp[definition "stype_size_def"] >> rw[] >> + drule_then strip_assume_tac subtype_size >> gvs[] +QED + +Theorem subtype_antisym: + ∀A B. subtype A B ∧ subtype B A ⇒ B = A +Proof + metis_tac[subtype_eqsize, subtype_size, arithmeticTheory.LESS_EQUAL_ANTISYM] +QED + Theorem FV_tpm_EQ_EMPTY[simp,local]: FV (tpm pi t) = ∅ ⇔ FV t = ∅ Proof - simp[EQ_IMP_THM, pred_setTheory.EXTENSION] >> rpt strip_tac >~ + simp[EQ_IMP_THM, EXTENSION] >> rpt strip_tac >~ [‘v ∈ FV M’, ‘π⁻¹ · _ # _’] >> first_x_assum $ qspec_then ‘π · v’ mp_tac >> simp[] QED @@ -292,7 +320,7 @@ Theorem FVEMPTY_DELETE_tpm[simp,local]: FV (tpm [(x,y)] t) DELETE swapstr x y v = ∅ ⇔ FV t DELETE v = ∅ Proof - simp[EQ_IMP_THM, pred_setTheory.EXTENSION,basic_swapTheory.swapstr_def] >> + simp[EQ_IMP_THM, EXTENSION,basic_swapTheory.swapstr_def] >> metis_tac[] QED @@ -317,7 +345,7 @@ Proof Cases_on ‘u = v’ >> simp[] >> strip_tac >> rw[basic_swapTheory.swapstr_def] >> rename [‘FV M DELETE v = ∅’] >> - ‘∀x. x ≠ v ⇒ x # M’ by (gs[pred_setTheory.EXTENSION] >> metis_tac[]) >> + ‘∀x. x ≠ v ⇒ x # M’ by (gs[EXTENSION] >> metis_tac[]) >> first_assum $ C (resolve_then Any (assume_tac o GSYM)) tpm_ALPHA >> simp[tpm_fresh] >> rename [‘LAM y (tpm [(v,y)] M)’] >> @@ -325,26 +353,302 @@ Proof metis_tac[pmact_flip_args] QED -val (ground_subterms_def, _) = define_recursive_term_function ‘ - ground_subterms (VAR s : term) = ∅ ∧ - ground_subterms (M @@ N) = - (if FV (M @@ N) = ∅ then {M @@ N} else ∅) ∪ ground_subterms M ∪ - ground_subterms N ∧ - ground_subterms (LAM v M) = - (if FV (LAM v M) = ∅ then {LAM v M} else ∅) ∪ ground_subterms M -’ -val _ = export_rewrites ["ground_subterms_def"] +Inductive gentype: +[~VAR:] + (∀Γ s τ. + valid_ctxt Γ ∧ MEM (s,τ) Γ ⇒ gentype Γ (VAR s : term) τ {(Γ,VAR s,τ)}) ∧ +[~APP:] + (∀Γ M N A B fs xs. + gentype Γ M (A → B) fs ∧ gentype Γ N A xs ⇒ + gentype Γ (M @@ N) B ({(Γ,M @@ N,B)} ∪ fs ∪ xs)) ∧ +[~LAM:] + (∀Γ v M A B bs. + gentype ((v,A) :: Γ) M B bs ⇒ + gentype Γ (LAM v M) (A → B) ({(Γ,LAM v M, A → B)} ∪ bs)) +End + +Theorem gentype_hastype: + gentype Γ M τ s ⇒ Γ ⊢ M ⦂ τ +Proof + Induct_on ‘gentype’ >> metis_tac[hastype_rules] +QED + +Theorem gentype_member_set: + gentype Γ M τ s ⇒ (Γ,M,τ) ∈ s +Proof + Induct_on ‘gentype’ >> simp[] +QED + +Theorem gentype_members_hastype: + gentype Γ M τ s ⇒ ∀Γ' M' τ'. (Γ',M',τ') ∈ s ⇒ Γ' ⊢ M' ⦂ τ' +Proof + Induct_on ‘gentype’ >> rw[] >> + metis_tac[hastype_rules, gentype_member_set] +QED + +Theorem hastype_gentype: + Γ ⊢ M ⦂ τ ⇒ ∃s. gentype Γ M τ s +Proof + Induct_on ‘hastype’ >> qexists ‘∅’ >> simp[] >> metis_tac[gentype_rules] +QED + +Inductive subterm: +[~refl:] + (∀M:term Γ. FINITE Γ ∧ FV M ⊆ Γ ⇒ (subterm (Γ, M) (Γ, M))) ∧ +[~appL:] + (∀Γ Γ₀ M0 M N. + FV N ⊆ Γ ∧ subterm (Γ₀, M0) (Γ, M) ⇒ subterm (Γ₀, M0) (Γ, M @@ N)) ∧ +[~appR:] + (∀Γ₀ Γ N0 M N. + FV M ⊆ Γ ∧ subterm (Γ₀, N0) (Γ, N) ⇒ subterm (Γ₀, N0) (Γ, M @@ N)) ∧ +[~lam:] + (∀Γ₀ Γ v M N. + v ∉ Γ ∧ + subterm (Γ₀, M) (v INSERT Γ, N) ⇒ subterm (Γ₀, M) (Γ, LAM v N)) +End + +Theorem subterm_FV: + ∀Γ₀ Γ M N. subterm (Γ₀, M) (Γ, N) ⇒ FV N ⊆ Γ ∧ FV M ⊆ Γ₀ ∧ Γ ⊆ Γ₀ +Proof + Induct_on ‘subterm’ >> simp[] >> rw[] >> + rename [‘FV N ⊆ v INSERT Γ’, ‘FV N DELETE v ⊆ Γ’] >> + qpat_x_assum ‘FV N ⊆ v INSERT Γ’ mp_tac >> + simp[SUBSET_DEF] >> metis_tac[] +QED + +Theorem subterm_VAR[simp]: + ∀Γ₁ Γ₂ t s. + subterm (Γ₁, t) (Γ₂, VAR s) ⇔ Γ₁ = Γ₂ ∧ t = VAR s ∧ s ∈ Γ₁ ∧ FINITE Γ₁ +Proof + simp[EQ_IMP_THM, FORALL_AND_THM, subterm_refl] >> + Induct_on ‘subterm’ >> rw[] >> gvs[] +QED + +Theorem subterm_size: + ∀Γ₁ Γ₂ t₁ t₂. subterm (Γ₁, t₁) (Γ₂, t₂) ⇒ size t₁ ≤ size t₂ +Proof + Induct_on ‘subterm’ >> rw[] +QED + +Theorem subterm_ID[simp]: + subterm (Γ₁, t) (Γ₂, t) ⇔ Γ₁ = Γ₂ ∧ FV t ⊆ Γ₂ ∧ FINITE Γ₂ +Proof + simp[Once subterm_cases] >> rw[EQ_IMP_THM, DISJ_IMP_THM] >> + drule subterm_size >> simp[] +QED + +Theorem subterm_FINITE: + ∀S0 S1 M0 M1. subterm (S0,M0) (S1,M1) ⇒ FINITE S0 ∧ FINITE S1 +Proof + Induct_on ‘subterm’ >> simp[] +QED + +Theorem appstar_EQ_LAMl: + t @* Ms = LAMl vs M ⇔ + Ms = [] ∧ t = LAMl vs M ∨ + vs = [] ∧ M = t @* Ms +Proof + Cases_on ‘Ms’ using listTheory.SNOC_CASES >> simp[] >> + Cases_on ‘vs’ >> simp[] >> metis_tac[] +QED + +Theorem appstar_EQ_APP: + t @* Ms = M1 @@ M2 ⇔ + (∃Ms0. Ms = SNOC M2 Ms0 ∧ t @* Ms0 = M1) ∨ Ms = [] ∧ t = M1 @@ M2 +Proof + Cases_on ‘Ms’ using listTheory.SNOC_CASES >> simp[] >> metis_tac[] +QED + +Theorem term_laml_cases: + ∀X. FINITE X ⇒ + ∀t. (∃s. t = VAR s) ∨ (∃M1 M2. t = M1 @@ M2) ∨ + ∃v vs Body. t = LAM v (LAMl vs Body) ∧ ¬is_abs Body ∧ v ∉ X ∧ + ¬MEM v vs ∧ ALL_DISTINCT vs ∧ DISJOINT (set vs) X +Proof + gen_tac >> strip_tac >> ho_match_mp_tac nc_INDUCTION2 >> simp[] >> + qexists ‘X’ >> simp[] >> rw[] >~ + [‘LAM v (VAR u)’, ‘v ∉ X’] + >- (qexistsl [‘v’, ‘[]’, ‘VAR u’] >> simp[]) >~ + [‘LAM v (M1 @@ M2)’, ‘v ∉ X’] + >- (qexistsl [‘v’, ‘[]’, ‘M1 @@ M2’] >> simp[]) >~ + [‘LAM u (LAM v (LAMl vs Body))’, ‘u ∉ X’, ‘v ∉ X’] >> + Cases_on ‘u = v’ >> gvs[] + >- (Q_TAC (NEW_TAC "z") ‘u INSERT set vs ∪ FV Body ∪ X’ >> + ‘z # LAM u (LAMl vs Body)’ by simp[FV_LAMl] >> + drule_then (qspec_then ‘u’ assume_tac) SIMPLE_ALPHA >> simp[lemma14b] >> + qexistsl [‘z’, ‘u::vs’, ‘Body’] >> simp[]) >> + Cases_on ‘MEM u vs’ + >- (Q_TAC (NEW_TAC "z") ‘{u;v} ∪ set vs ∪ FV Body ∪ X’ >> + ‘z # LAM v (LAMl vs Body)’ by simp[FV_LAMl] >> + drule_then (qspec_then ‘u’ assume_tac) SIMPLE_ALPHA >> + simp[lemma14b, FV_LAMl] >> + qexistsl [‘z’, ‘v::vs’, ‘Body’] >> simp[]) >> + Q_TAC (NEW_TAC "z") ‘{u;v} ∪ set vs ∪ X ∪ FV Body’ >> + ‘z # LAM v (LAMl vs Body)’ by simp[FV_LAMl] >> + drule_then (qspec_then ‘u’ assume_tac) tpm_ALPHA >> simp[] >> + qexists ‘z’ >> Q.REFINE_EXISTS_TAC ‘x::xs’ >> simp[tpm_LAMl] >> + irule_at Any EQ_REFL >> simp[DISJOINT_DEF, EXTENSION, MEM_listpm] >> + qx_gen_tac ‘a’ >> Cases_on ‘a ∈ X’ >> simp[] >> + Cases_on ‘a = u’ >> gvs[] >> + Cases_on ‘a = z’ >> gvs[] >> + gvs[DISJOINT_DEF, EXTENSION] >> metis_tac[] +QED -(* +Theorem bnf_LAMl[simp]: + bnf (LAMl vs M) = bnf M +Proof + Induct_on ‘vs’ >> simp[] +QED +Theorem EQ_LAML_E: + ∀us vs M N. (LAMl us M = LAMl vs N) ∧ ¬is_abs M ∧ ¬is_abs N ⇒ + ∃pi. N = tpm pi M +Proof + Induct >> simp[] + >- metis_tac[pmact_nil] >> + simp[] >> rpt gen_tac >> rename [‘LAM x (LAMl xs _) = LAMl ys _’] >> + Cases_on ‘ys’ >> simp[] >- (rw[] >> gvs[]) >> + rename [‘LAM x (LAMl xs M) = LAM y (LAMl ys N)’] >> + simp[LAM_eq_thm] >> rw[] >> gvs[tpm_LAMl] + >- metis_tac[] >> + first_x_assum drule >> simp[] >> rename [‘tpm [(a,b)] N = _’] >> + rw[] >> pop_assum (mp_tac o Q.AP_TERM ‘tpm [(a,b)]’) >> + REWRITE_TAC [pmact_sing_inv] >> metis_tac[pmact_decompose] +QED -Theorem subformula_property: +Theorem bnf_characterisation': + ∀M X. FINITE X ⇒ + (bnf M ⇔ + ∃vs v Ms. DISJOINT (set vs) X ∧ M = LAMl vs (VAR v @* Ms) ∧ + ALL_DISTINCT vs ∧ ∀M. MEM M Ms ⇒ bnf M) +Proof + completeInduct_on ‘size M’ >> rw[] >> gvs[GSYM RIGHT_FORALL_IMP_THM] >> + drule_then (qspec_then ‘M’ strip_assume_tac) term_laml_cases >> simp[] >~ + [‘M1 @@ M2’] + >- (first_assum $ qspec_then ‘M1’ assume_tac >> + first_x_assum $ qspec_then ‘M2’ assume_tac >> gs[]>> + rpt (first_x_assum $ drule_then assume_tac) >> + simp[] >> iff_tac >> rw[] >> + gvs[appstar_EQ_APP, appstar_EQ_LAMl, DISJ_IMP_THM, FORALL_AND_THM] >> + dsimp[PULL_EXISTS] >> metis_tac[]) >~ + [‘LAM u $ LAMl us Body’] + >- (gvs[] >> + first_x_assum $ qspec_then ‘Body’ mp_tac >> simp[]>> + disch_then $ qspec_then ‘∅’ mp_tac >> simp[] >> + disch_then kall_tac >> + ‘∀xs M. Body = LAMl xs M ⇔ xs = [] ∧ M = Body’ + by (rpt gen_tac >> Cases_on ‘xs’ >> simp[] >- metis_tac[] >> + strip_tac >> gvs[]) >> + simp[] >> iff_tac >> rw[] + >- (qexistsl [‘u::us’, ‘v’, ‘Ms’] >> simp[]) >> + rename [‘LAM u (LAMl us Body) = LAMl vs (VAR v @* Ms)’] >> + ‘LAMl vs (VAR v @* Ms) = LAMl (u::us) Body’ by simp[] >> + drule EQ_LAML_E >> simp[PULL_EXISTS, tpm_appstar, MEM_listpm_EXISTS]) +QED + +Theorem bnf_appstar[simp]: + ∀M Ns. bnf (M @* Ns) ⇔ bnf M ∧ (∀N. MEM N Ns ⇒ bnf N) ∧ (is_abs M ⇒ Ns = []) +Proof + Induct_on ‘Ns’ using listTheory.SNOC_INDUCT >> + simp[DISJ_IMP_THM, FORALL_AND_THM] >> metis_tac[] +QED + +Theorem subterm_perm: + ∀G0 M0 G M. + subterm (G0,M0) (G,M) ⇒ + ∀pi. subterm (ssetpm pi G0, tpm pi M0) (ssetpm pi G, tpm pi M) +Proof + Induct_on ‘subterm’ >> simp[] >> rw[] + >- gvs[SUBSET_DEF] + >- (irule subterm_appL >> gvs[SUBSET_DEF]) + >- (irule subterm_appR >> gvs[SUBSET_DEF]) >> + irule subterm_lam >> gvs[pmact_INSERT] +QED + +Theorem subterm_lam_inv: + ∀v Γ Γ0 M M0. + v ∉ Γ ⇒ + (subterm (Γ0, M0) (Γ, LAM v M) ⇔ + M0 = LAM v M ∧ Γ0 = Γ ∧ FINITE Γ0 ∧ FV (LAM v M) ⊆ Γ0 ∨ + ∃u. u ∉ Γ ∧ (u = v ∨ u ∉ FV M) ∧ + subterm (ssetpm [(u,v)] Γ0, tpm [(u,v)] M0) (v INSERT Γ, M)) +Proof + simp[SimpLHS, Once subterm_cases] >> + rw[] >> iff_tac >> rw[] + >- gvs[] + >- (rename [‘LAM u M = LAM v N’] >> disj2_tac >> + gvs[LAM_eq_thm] >- (first_assum $ irule_at Any >> simp[]) >> + drule_then (qspec_then ‘[(v,u)]’ assume_tac) subterm_perm>> + ‘tpm [(v,u)] N = tpm [(u,v)] N’ by simp[pmact_flip_args] >> + qexists ‘v’ >> simp[] >> + ‘ssetpm [(v,u)] (v INSERT Γ) = u INSERT Γ’ suffices_by metis_tac[] >> + simp[pmact_INSERT] >> + ‘ssetpm [(v,u)] Γ = Γ’ suffices_by simp[] >> + irule supp_fresh >> drule subterm_FINITE >> simp[supp_FINITE_strings]) + >- (gvs[] >> metis_tac[]) + >- (drule_then (qspec_then ‘[(u,v)]’ mp_tac) subterm_perm >> + simp[pmact_INSERT] >> strip_tac >> disj2_tac >> + ‘ssetpm [(u,v)] Γ = Γ’ by (irule supp_fresh >> drule subterm_FINITE >> + simp[supp_FINITE_strings]) >> + gvs[] >> first_assum $ irule_at Any >> simp[] >> + simp[LAM_eq_thm, SF CONJ_ss] >> + simp[pmact_flip_args]) +QED + +(* Theorem subformula_property: ∀Γ t A. Γ ⊢ t ⦂ A ∧ bnf t ⇒ - ∀t0. t0 ∈ ground_subterms t ⇒ - ∃B B'. subtype B B' ∧ B' ∈ A INSERT (set $ MAP SND Γ) ∧ Γ ⊢ t0 ⦂ B -Proof - Induct_on ‘hastype’ >> qexists ‘∅’ >> simp[] >> rpt strip_tac >> gvs[] >>~- + ∀S0 t0. subterm (S0, t0) (set (MAP FST Γ), t) ⇒ + ∃Γ0 A0 A1. + set (MAP FST Γ0) = S0 ∧ Γ0 ⊢ t0 ⦂ A0 ∧ + subtype A0 A1 ∧ + (A1 = A ∨ ∃v. MEM (v,A1) Γ) +Proof[exclude_simps = subtype_def] + completeInduct_on ‘size t’ >> rw[] >> gs[PULL_FORALL] >> + Cases_on ‘t0 = t’ + >- (gvs[] >> dsimp[] >> metis_tac[subtype_refl]) >> + qpat_x_assum ‘bnf _’ mp_tac >> + ‘FINITE (ctxtFV Γ)’ by simp[] >> + drule_then (qspec_then ‘t’ (simp o single o Once)) bnf_characterisation' >> + rw[] >> reverse $ Cases_on ‘vs’ + >- (gvs[] >> + qpat_x_assum ‘Γ ⊢ LAM _ (LAMl _ _) ⦂ A’ mp_tac >> + simp[hastype_lam_inv, PULL_EXISTS] >> rw[] >> + first_x_assum $ drule_at (Pat ‘hastype _ _ _ ’) >> + simp[] + Induct_on ‘hastype’ >> qexists ‘∅’ >> simp[] >> rw[] >> gvs[] + >- (irule_at Any EQ_REFL >> simp[]>> first_assum $ irule_at Any >> + simp[] >> rw[] >> + gvs[valid_ctxt_ALL_DISTINCT] >> + rename [‘subtype A B’, ‘MEM (v,A) Γ’] >> + ‘A = B’ suffices_by simp[] >> + dxrule_then strip_assume_tac + (iffLR listTheory.MEM_SPLIT_APPEND_first) >> gvs[] >> + rename [‘MEM (vn,B) lp’] >> + qpat_x_assum ‘MEM _ lp’ + $ mp_then Any strip_assume_tac + $ iffLR listTheory.MEM_SPLIT_APPEND_first >> + gvs[listTheory.ALL_DISTINCT_APPEND] >> metis_tac[]) + >- (qpat_x_assum ‘subterm _ _ ’ mp_tac >> + ONCE_REWRITE_TAC [subterm_cases] >> rw[] >~ + [‘FV (M @@ N) ⊆ _’, ‘Γ ⊢ M ⦂ A → B’] + >- ( + + + ‘Γ = [(s,A)]’ suffices_by simp[] >> + Cases_on ‘Γ’ >> gvs[] >~ + [‘s # t’] + >- (Cases_on ‘t’ >> fs[DISJ_IMP_THM, FORALL_AND_THM] >> + rename [‘valid_ctxt (h::ts)’] >> Cases_on ‘h’ >> fs[]) >> + rename [‘valid_ctxt (h::t)’] >> + Cases_on ‘h’ >> fs[DISJ_IMP_THM, FORALL_AND_THM] >> gvs[] >> + rename [‘vn # t’] >> Cases_on ‘t’ >> fs[DISJ_IMP_THM, FORALL_AND_THM] >> + rename [‘valid_ctxt (h::t)’] >> Cases_on ‘h’ >> fs[]) + >- ( + +valid_ctxt_def + >- metis_tac[] + >- ([‘¬is_abs M’, ‘bnf M’, ‘_ ⊢ M ⦂ τ1 → τ2’], drule_all progress >> metis_tac[corollary3_2_1, beta_normal_form_bnf]) >~