From 407d5003ba58b90aa8ef3cf67f8d6056791adc65 Mon Sep 17 00:00:00 2001 From: Matthew Toohey Date: Tue, 21 Oct 2025 09:48:22 -0400 Subject: [PATCH 1/3] fix tex for IndexedStronglyNormalizing --- .../Semantics/Type/SmallStep.lean" | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git "a/TabularTypes/F\342\212\227\342\212\225\317\211/Semantics/Type/SmallStep.lean" "b/TabularTypes/F\342\212\227\342\212\225\317\211/Semantics/Type/SmallStep.lean" index aad8938..b1d5b38 100644 --- "a/TabularTypes/F\342\212\227\342\212\225\317\211/Semantics/Type/SmallStep.lean" +++ "b/TabularTypes/F\342\212\227\342\212\225\317\211/Semantics/Type/SmallStep.lean" @@ -173,7 +173,7 @@ inductive StronglyNormalizingToList (P : «Type» → Prop) : «Type» → Prop | step : (∀ B, [[ε ⊢ A -> B]] → StronglyNormalizingToList P B) → (∀ As K?, A ≠ Type.list As K?) → StronglyNormalizingToList P A -judgement_syntax "SN" K "(" A ")" : IndexedStronglyNormalizing +judgement_syntax "SN" K "(" A ")" : IndexedStronglyNormalizing (tex := s!"\\lottkw\{SN}_\{{K}}({A})") abbrev IndexedStronglyNormalizing : Kind → «Type» → Prop | [[*]], A => [[ε ⊢ A : *]] ∧ [[SN(A)]] From e2cdea222cd78cbbc23598e8bbc8469ec2c75753 Mon Sep 17 00:00:00 2001 From: Matthew Toohey Date: Tue, 21 Oct 2025 09:48:37 -0400 Subject: [PATCH 2/3] update target theorems in README --- README.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index dc8820b..89bd55a 100644 --- a/README.md +++ b/README.md @@ -7,9 +7,10 @@ This repository contains the proofs for _Extensible Data Types with Ad-Hoc Polym The numbered theorems from the paper correspond to the following Lean theorems: - Theorem 4.1: [`TabularTypes.«F⊗⊕ω».SmallStep.local_confluence`](TabularTypes/F⊗⊕ω/Lemmas/Type/SmallStep.lean) -- Theorem 4.2: [`TabularTypes.«F⊗⊕ω».IndexedStronglyNormalizing.of_Kinding`](TabularTypes/F⊗⊕ω/Lemmas/Type/SmallStep.lean) -- Theorem 4.3: [`TabularTypes.«F⊗⊕ω».progress`](TabularTypes/F⊗⊕ω/Theorems.lean) -- Theorem 4.4: [`TabularTypes.«F⊗⊕ω».preservation`](TabularTypes/F⊗⊕ω/Theorems.lean) +- Theorem 4.2: [`TabularTypes.«F⊗⊕ω».StronglyNormalizing.of_Indexed`](TabularTypes/F⊗⊕ω/Lemmas/Type/SmallStep.lean) +- Theorem 4.3: [`TabularTypes.«F⊗⊕ω».IndexedStronglyNormalizing.of_Kinding`](TabularTypes/F⊗⊕ω/Lemmas/Type/SmallStep.lean) +- Theorem 4.4: [`TabularTypes.«F⊗⊕ω».progress`](TabularTypes/F⊗⊕ω/Theorems.lean) +- Theorem 4.5: [`TabularTypes.«F⊗⊕ω».preservation`](TabularTypes/F⊗⊕ω/Theorems.lean) - Theorem 5.1: - Kinding: [`TabularTypes.TypeScheme.KindingAndElaboration.soundness`](TabularTypes/Theorems/Type/KindingAndElaboration.lean) - Row Equivalence: [`TabularTypes.Monotype.RowEquivalenceAndElaboration.soundness`](TabularTypes/Theorems/Type/Basic.lean) From 78957fc5054debaa6a183d81b3b03cf3fab22631 Mon Sep 17 00:00:00 2001 From: Matthew Toohey Date: Wed, 22 Oct 2025 09:54:42 -0400 Subject: [PATCH 3/3] add lift row equivalence congruence rule --- TabularTypes/Lemmas/Type/ToKinding.lean | 4 + .../Type/RowEquivalenceAndElaboration.lean | 11 ++ TabularTypes/Theorems/Type/Basic.lean | 113 ++++++++++++++++++ .../Monotype/RowEquivalenceAndElaboration.tex | 10 ++ .../RowEquivalenceAndElaboration/noelab.tex | 6 + .../noelabPresentation.tex | 6 + ...wEquivalenceAndElaborationPresentation.tex | 10 ++ 7 files changed, 160 insertions(+) diff --git a/TabularTypes/Lemmas/Type/ToKinding.lean b/TabularTypes/Lemmas/Type/ToKinding.lean index fb9d515..f2736df 100644 --- a/TabularTypes/Lemmas/Type/ToKinding.lean +++ b/TabularTypes/Lemmas/Type/ToKinding.lean @@ -31,6 +31,10 @@ theorem Monotype.RowEquivalenceAndElaboration.to_Kinding (ρee : [[Γc; Γ ⊢ let ⟨_, _, _, ρ₁ke', ρ₂ke⟩ := ρ₁₂ee.to_Kinding Γcw Γwe cases ρ₁ke.deterministic ρ₁ke' |>.left exact ⟨_, _, _, ρ₀ke, ρ₂ke⟩ + | lift I ρ₀₁ee ρ₀ke τke κ₀e _ (κ₀ := κ₀) (κ₁ := κ₁) => + let ⟨_, _, _, ρ₀ke', ρ₁ke⟩ := ρ₀₁ee.to_Kinding Γcw Γwe + cases ρ₀ke.deterministic ρ₀ke' |>.left + exact ⟨_, _, _, .lift I τke κ₀e ρ₀ke, .lift I τke κ₀e ρ₁ke⟩ | liftL _ liftke@(.lift I τ'ke κ₀e ξτke) _ (τ' := τ') (κ₁ := κ₁) => let ⟨⟨_, ξke⟩, uni, ⟨_, _, _, eq, κeq, _, h, _, τke⟩⟩ := ξτke.row_inversion let ⟨_, κ₁e⟩ := κ₁.Elaboration_total diff --git a/TabularTypes/Semantics/Type/RowEquivalenceAndElaboration.lean b/TabularTypes/Semantics/Type/RowEquivalenceAndElaboration.lean index 6d750e6..cff6adf 100644 --- a/TabularTypes/Semantics/Type/RowEquivalenceAndElaboration.lean +++ b/TabularTypes/Semantics/Type/RowEquivalenceAndElaboration.lean @@ -3,6 +3,7 @@ import TabularTypes.Semantics.Type.KindingAndElaboration namespace TabularTypes open «F⊗⊕ω» +open TabularTypes.TypeScheme judgement_syntax Γc "; " Γ " ⊢ " ρ₀ " ≡" "(" μ ") " ρ₁ " ⇝ " Fₚ ", " Fₛ : Monotype.RowEquivalenceAndElaboration (tex := s!"{Γc} \\lottsym\{;} \\, {Γ} \\, \\lottsym\{⊢} \\, {ρ₀} \\, \\rowequivsym_\{{μ}} \\, {ρ₁} \\, \\lottsym\{⇝} \\, {Fₚ} \\lottsym\{,} \\, {Fₛ}") (tex noelab := s!"{Γc} \\lottsym\{;} \\, {Γ} \\, \\lottsym\{⊢} \\, {ρ₀} \\, \\rowequivsym_\{{μ}} \\, {ρ₁}") @@ -38,6 +39,16 @@ notex for noelab Fₛ := Λ a : K ↦ *. λ x : ⊕ (a$0 ⟦{ ⟩ ≡(C) ⟨ ⟩ ⇝ Fₚ, Fₛ +Γc; Γ ⊢ ρ₀ ≡(μ) ρ₁ ⇝ Fₚ', Fₛ' +Γc; Γ ⊢ ρ₀ : R κ₀ +∀ a ∉ I, Γc; Γ, a : κ₀ ⊢ τ^a : κ₁ ⇝ A^a +notex for noelab ⊢ κ₀ ⇝ K₀ +notex for noelab ⊢ κ₁ ⇝ K₁ +notex for noelab Fₚ := Λ a' : K₁ ↦ *. Fₚ' [λ a : K₀. a'$1 A] +notex for noelab Fₛ := Λ a' : K₁ ↦ *. Fₛ' [λ a : K₀. a'$1 A] +───────────────────────────────────────────────────────────────── lift (I : List TypeVarId) +Γc; Γ ⊢ Lift (λ a : κ₀. τ) ρ₀ ≡(μ) Lift (λ a : κ₀. τ) ρ₁ ⇝ Fₚ, Fₛ + Γc; Γ ⊢ Lift (λ a : κ₀. τ') ⟨ ⟩ : R κ₁ ⇝ A notex for noelab ⊢ κ₁ ⇝ K notex for noelab Fₚ := Λ a' : K ↦ *. λ x : ⊗ (a'$0 ⟦A⟧). x$0 diff --git a/TabularTypes/Theorems/Type/Basic.lean b/TabularTypes/Theorems/Type/Basic.lean index 65df250..ea66226 100644 --- a/TabularTypes/Theorems/Type/Basic.lean +++ b/TabularTypes/Theorems/Type/Basic.lean @@ -52,6 +52,11 @@ theorem symm (ρee : [[Γc; Γ ⊢ ρ₀ ≡(μ) ρ₁ ⇝ Fₚ, Fₛ]]) (Γcw : let ⟨κ', _, _, _, ρ₂ke⟩ := ρ₁₂ee.to_Kinding Γcw Γwe let ⟨_, κ'e⟩ := κ'.Elaboration_total ⟨_, _, trans ρ₂ke κ'e ρ₂₁ee ρ₁₀ee⟩ + | lift I ρ₀₁ee ρ₀ke τke κ₀e κ₁e => by + let ⟨_, _, ρ₁₀ee⟩ := ρ₀₁ee.symm Γcw Γwe + let ⟨_, _, _, ρ₀ke', ρ₁ke⟩ := ρ₀₁ee.to_Kinding Γcw Γwe + cases ρ₀ke.deterministic ρ₀ke' |>.left + exact ⟨_, _, lift I ρ₁₀ee ρ₁ke τke κ₀e κ₁e⟩ | liftL μ liftke κe => ⟨_, _, liftR μ liftke κe⟩ | liftR μ liftke κe => ⟨_, _, liftL μ liftke κe⟩ @@ -344,6 +349,114 @@ theorem soundness (ρee : [[Γc; Γ ⊢ ρ₀ ≡(μ) ρ₁ ⇝ Fₚ, Fₛ]]) ( simp only [Function.comp] exact .lam (.app (.var_bound Nat.one_pos) <| A'slc' i mem') <| .sumIntro .var ⟩ + | lift I ρ₀₁'ee ρ₀'ke τke κ₀e κ₁e (A := A') (K₀ := K₀) => + let ⟨_, _, _, ρ₀'ke', ρ₁'ke⟩ := ρ₀₁'ee.to_Kinding Γcw Γwe + rcases ρ₀'ke.deterministic ρ₀'ke' with ⟨κ₀eq, rfl⟩ + cases κ₀eq + + let .lift I' τke' κ₀e' ρ₀'ke'' (A := A'') := ρ₀ke + let .lift I'' τke'' κ₀e'' ρ₁'ke' (A := A''') := ρ₁ke + + rcases ρ₀'ke.deterministic ρ₀'ke'' with ⟨κ₀eq, rfl⟩ + cases κ₀eq + cases κ₀e.deterministic κ₀e' + cases κ₀e.deterministic κ₀e'' + + let ⟨a, anin⟩ := Γ.typeVarDom ++ ↑A'.freeTypeVars ++ ↑A''.freeTypeVars ++ ↑A'''.freeTypeVars ++ + I ++ I' ++ I'' |>.exists_fresh + let ⟨aninΓA'A''A'''II', aninI''⟩ := List.not_mem_append'.mp anin + let ⟨aninΓA'A''A'''I, aninI'⟩ := List.not_mem_append'.mp aninΓA'A''A'''II' + let ⟨aninΓA'A''A''', aninI⟩ := List.not_mem_append'.mp aninΓA'A''A'''I + let ⟨aninΓA'A'', aninA'''⟩ := List.not_mem_append'.mp aninΓA'A''A''' + let ⟨aninΓA', aninA''⟩ := List.not_mem_append'.mp aninΓA'A'' + let ⟨aninΓ, aninA'⟩ := List.not_mem_append'.mp aninΓA' + + rcases τke a aninI |>.deterministic <| τke' a aninI' with ⟨rfl, A'eq⟩ + cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars aninA' aninA'' A'eq + rcases τke a aninI |>.deterministic <| τke'' a aninI'' with ⟨_, A''eq⟩ + cases Type.TypeVar_open_inj_of_not_mem_freeTypeVars aninA' aninA''' A''eq + cases κe.deterministic κ₁e + + rcases ρ₁'ke.deterministic ρ₁'ke' with ⟨_, rfl⟩ + + let Alc := τke a aninI |>.soundness Γcw (Γwe.typeExt aninΓ κ₀e) κ₁e + |>.TypeVarLocallyClosed_of.weaken (n := 1).TypeVar_open_drop Nat.one_pos + let B₀ki := ρ₀'ke.soundness Γcw Γwe κ₀e.row + let B₀lc := B₀ki.TypeVarLocallyClosed_of + let B₁ki := ρ₁'ke.soundness Γcw Γwe κ₀e.row + let B₁lc := B₁ki.TypeVarLocallyClosed_of + let ⟨Fₚ'ty, Fₛ'ty, Fₚ'lc, Fₛ'lc⟩ := ρ₀₁'ee.soundness Γcw Γwe ρ₀'ke ρ₁'ke κ₀e + let Δwf := Γwe.soundness Γcw + exact ⟨ + .typeLam Γ.typeVarDom fun a' a'nin => by + let a'ninΔ := Γwe.TypeVarNotInDom_preservation a'nin + simp [Type.TypeVar_open, Term.TypeVar_open, Fₚ'lc.TypeVar_open_id, Alc.TypeVar_open_id, + B₀lc.TypeVar_open_id, B₁lc.TypeVar_open_id] + let Γa'we := Γwe.typeExt a'nin <| κ₁e.arr .star + let Δa'wf := Γa'we.soundness Γcw + let Fₚ'ty' := Fₚ'ty.weakening (Γa'we.soundness Γcw) (Δ' := .typeExt .empty ..) (Δ'' := .empty) + |>.typeApp (B := [[λ a : K₀. a' A']]) <| .lam ((a' :: Γ.typeVarDom) ++ ↑I) <| + fun a'' a''nin => by + simp [Type.TypeVar_open, Environment.append] + let ⟨a''ninΓa', a''ninI⟩ := List.not_mem_append'.mp a''nin + let ⟨a''ne, _⟩ := List.not_mem_cons.mp a''ninΓa' + refine .app (.var (.typeVarExt .head (.symm a''ne))) ?_ + let Γa'a''we := Γa'we.typeExt a''ninΓa' κ₀e + exact τke _ a''ninI |>.weakening (Γ' := .typeExt .empty ..) + (Γ'' := .typeExt .empty ..) Γa'a''we |>.soundness Γcw Γa'a''we κ₁e + apply Fₚ'ty'.equiv + simp [Type.Type_open, B₀lc.Type_open_id, B₁lc.Type_open_id] + let A'ki : [[Δ ⊢ λ a : K₀. A' : K₀ ↦ K]] := .lam (Γ.typeVarDom ++ I) fun a anin => by + let ⟨aninΓ, aninI⟩ := List.not_mem_append'.mp anin + exact τke _ aninI |>.soundness Γcw (Γwe.typeExt aninΓ κ₀e) κ₁e + refine .arr (.prod (.symm ?_)) (.prod (.symm ?_)) + all_goals ( + replace A'ki := A'ki.weakening (Δ' := .typeExt .empty ..) (Δ'' := .empty) Δa'wf + refine .trans (.listAppComp .var_free A'ki) ?_ + refine .listApp (.lam (a' :: Δ.typeVarDom) ?_) .refl + intro a'' a''nin + simp [Type.TypeVar_open, Alc.TypeVar_open_id] + rw [Type.Type_open_var] + exact .app .refl <| .lamApp + (A'ki.weakening (Δ' := .typeExt .empty ..) (Δ'' := .empty) (Δa'wf.typeVarExt a''nin)) <| + .var .head + ), + .typeLam Γ.typeVarDom fun a' a'nin => by + let a'ninΔ := Γwe.TypeVarNotInDom_preservation a'nin + simp [Type.TypeVar_open, Term.TypeVar_open, Fₛ'lc.TypeVar_open_id, Alc.TypeVar_open_id, + B₀lc.TypeVar_open_id, B₁lc.TypeVar_open_id] + let Γa'we := Γwe.typeExt a'nin <| κ₁e.arr .star + let Δa'wf := Γa'we.soundness Γcw + let Fₛ'ty' := Fₛ'ty.weakening (Γa'we.soundness Γcw) (Δ' := .typeExt .empty ..) (Δ'' := .empty) + |>.typeApp (B := [[λ a : K₀. a' A']]) <| .lam ((a' :: Γ.typeVarDom) ++ ↑I) <| + fun a'' a''nin => by + simp [Type.TypeVar_open, Environment.append] + let ⟨a''ninΓa', a''ninI⟩ := List.not_mem_append'.mp a''nin + let ⟨a''ne, _⟩ := List.not_mem_cons.mp a''ninΓa' + refine .app (.var (.typeVarExt .head (.symm a''ne))) ?_ + let Γa'a''we := Γa'we.typeExt a''ninΓa' κ₀e + exact τke _ a''ninI |>.weakening (Γ' := .typeExt .empty ..) + (Γ'' := .typeExt .empty ..) Γa'a''we |>.soundness Γcw Γa'a''we κ₁e + apply Fₛ'ty'.equiv + simp [Type.Type_open, B₀lc.Type_open_id, B₁lc.Type_open_id] + let A'ki : [[Δ ⊢ λ a : K₀. A' : K₀ ↦ K]] := .lam (Γ.typeVarDom ++ I) fun a anin => by + let ⟨aninΓ, aninI⟩ := List.not_mem_append'.mp anin + exact τke _ aninI |>.soundness Γcw (Γwe.typeExt aninΓ κ₀e) κ₁e + refine .arr (.sum (.symm ?_)) (.sum (.symm ?_)) + all_goals ( + replace A'ki := A'ki.weakening (Δ' := .typeExt .empty ..) (Δ'' := .empty) Δa'wf + refine .trans (.listAppComp .var_free A'ki) ?_ + refine .listApp (.lam (a' :: Δ.typeVarDom) ?_) .refl + intro a'' a''nin + simp [Type.TypeVar_open, Alc.TypeVar_open_id] + rw [Type.Type_open_var] + exact .app .refl <| .lamApp + (A'ki.weakening (Δ' := .typeExt .empty ..) (Δ'' := .empty) (Δa'wf.typeVarExt a''nin)) <| + .var .head + ), + .typeLam <| .typeApp Fₚ'lc.weaken <| .lam <| .app (.var_bound Nat.le.refl) Alc.weaken, + .typeLam <| .typeApp Fₛ'lc.weaken <| .lam <| .app (.var_bound Nat.le.refl) Alc.weaken + ⟩ | liftL μ liftke@(.lift I τ'ke κ₀e ξτke) κe' (τ := τ) (τ' := τ') => rename_i A' _ _ let ⟨κeq, Aeq⟩ := liftke.deterministic ρ₀ke diff --git a/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration.tex b/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration.tex index d47ee4b..1bb9076 100644 --- a/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration.tex +++ b/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration.tex @@ -23,6 +23,16 @@ \lottlet{\targetpre Fₛ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \targetpre K \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre \lottsym{⊕} \, \targetpre \lottsym{(} \targetpre \targetpre \targetpre a \targetpost \targetpost \, \lottsym{⟦} \targetpre \lottsym{\{} \lottsepbycomprehensionpatcollection{\targetpre A_{i} \targetpost}{i}{[:n]} \lottsym{\}} \targetpost \lottsym{⟧} \targetpost \lottsym{)} \targetpost \targetpost \lottsym{.} \, \targetpre \lottkw{case} \, \targetpre \targetpre x \targetpost \targetpost \, \lottsym{\{} \lottsepbycomprehensioncustom{\targetpre \lottsym{λ} \, \targetpre x' \targetpost \, \lottsym{:} \, \targetpre \targetpre \targetpre a \targetpost \targetpost \, \targetpre A_{i} \targetpost \targetpost \lottsym{.} \, \targetpre \lottsym{ι}_{j} \, \targetpre \targetpre x' \targetpost \targetpost \targetpost \targetpost}{i \in [:n], j \in p'} \lottsym{\}} \targetpost \targetpost \targetpost} }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \rowequivsym_{\mathfrak{c}} \, \lottsym{⟨} \lottsepbycomprehensioncustom{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i \in p} \lottsym{⟩} \, \lottsym{⇝} \, \targetpre Fₚ \targetpost \lottsym{,} \, \targetpre Fₛ \targetpost} \lottinferencerulesep +\lottinferencerule{lift}{ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \rowequivsym_{μ} \, ρ₁ \, \lottsym{⇝} \, \targetpre Fₚ' \targetpost \lottsym{,} \, \targetpre Fₛ' \targetpost}\\ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \kindingsym \, \lottkw{R}^{κ₀}}\\ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \lottsym{,} \, a \, \lottsym{:} \, κ₀ \, \lottsym{⊢} \, τ \, \kindingsym \, κ₁ \, \lottsym{⇝} \, \targetpre \targetpre A \targetpost \targetpost}\\ +\lotthypothesis{\lottsym{⊢} \, κ₀ \, \lottsym{⇝} \, \targetpre K₀ \targetpost}\\ +\lotthypothesis{\lottsym{⊢} \, κ₁ \, \lottsym{⇝} \, \targetpre K₁ \targetpost}\\ +\lottlet{\targetpre Fₚ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a' \targetpost \, \lottsym{:} \, \targetpre \targetpre K₁ \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \targetpre Fₚ' \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre K₀ \targetpost \lottsym{.} \, \targetpre \targetpre \targetpre a' \targetpost \targetpost \, \targetpre A \targetpost \targetpost \targetpost \lottsym{]} \targetpost \targetpost}\\ +\lottlet{\targetpre Fₛ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a' \targetpost \, \lottsym{:} \, \targetpre \targetpre K₁ \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \targetpre Fₛ' \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre K₀ \targetpost \lottsym{.} \, \targetpre \targetpre \targetpre a' \targetpost \targetpost \, \targetpre A \targetpost \targetpost \targetpost \lottsym{]} \targetpost \targetpost} +}{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₀ \, \rowequivsym_{μ} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₁ \, \lottsym{⇝} \, \targetpre Fₚ \targetpost \lottsym{,} \, \targetpre Fₛ \targetpost} +\lottinferencerulesep \lottinferencerule{liftL}{ \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ₁} \, \lottsym{⇝} \, \targetpre A \targetpost}\\ \lotthypothesis{\lottsym{⊢} \, κ₁ \, \lottsym{⇝} \, \targetpre K \targetpost}\\ diff --git a/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelab.tex b/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelab.tex index 6d78d85..f1558ec 100644 --- a/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelab.tex +++ b/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelab.tex @@ -14,6 +14,12 @@ \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ}} }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \rowequivsym_{\mathfrak{c}} \, \lottsym{⟨} \lottsepbycomprehensioncustom{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i \in p} \lottsym{⟩}} \lottinferencerulesep +\lottinferencerule{lift}{ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \rowequivsym_{μ} \, ρ₁}\\ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \kindingsym \, \lottkw{R}^{κ₀}}\\ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \lottsym{,} \, a \, \lottsym{:} \, κ₀ \, \lottsym{⊢} \, τ \, \kindingsym \, κ₁} +}{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₀ \, \rowequivsym_{μ} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₁} +\lottinferencerulesep \lottinferencerule{liftL}{ \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ₁}} }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \rowequivsym_{μ} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ'\left[τ_{i}/a\right]} \lottsym{⟩}} diff --git a/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelabPresentation.tex b/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelabPresentation.tex index d2ef9b0..de39eed 100644 --- a/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelabPresentation.tex +++ b/tex/TabularTypes/Monotype/RowEquivalenceAndElaboration/noelabPresentation.tex @@ -14,6 +14,12 @@ \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ}} }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \rowequivsym_{\mathfrak{c}} \, \lottsym{⟨} \lottsepbycomprehensioncustom{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i \in p} \lottsym{⟩}} \lottinferencerulesep +\lottinferencerule{lift}{ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \rowequivsym_{μ} \, ρ₁}\\ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \kindingsym \, \lottkw{R}^{κ₀}}\\ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \lottsym{,} \, a \, \lottsym{:} \, κ₀ \, \lottsym{⊢} \, τ \, \kindingsym \, κ₁} +}{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₀ \, \rowequivsym_{μ} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₁} +\lottinferencerulesep \lottinferencerule{liftL}{ \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ₁}} }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \rowequivsym_{μ} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ'\left[τ_{i}/a\right]} \lottsym{⟩}} diff --git a/tex/TabularTypes/Monotype/RowEquivalenceAndElaborationPresentation.tex b/tex/TabularTypes/Monotype/RowEquivalenceAndElaborationPresentation.tex index 4d8dd35..98bd9f2 100644 --- a/tex/TabularTypes/Monotype/RowEquivalenceAndElaborationPresentation.tex +++ b/tex/TabularTypes/Monotype/RowEquivalenceAndElaborationPresentation.tex @@ -23,6 +23,16 @@ \lottlet{\targetpre Fₛ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre \targetpre K \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \lottsym{λ} \, \targetpre x \targetpost \, \lottsym{:} \, \targetpre \lottsym{⊕} \, \targetpre \lottsym{(} \targetpre \targetpre \targetpre a \targetpost \targetpost \, \lottsym{⟦} \targetpre \lottsym{\{} \lottsepbycomprehensionpatcollection{\targetpre A_{i} \targetpost}{i}{[:n]} \lottsym{\}} \targetpost \lottsym{⟧} \targetpost \lottsym{)} \targetpost \targetpost \lottsym{.} \, \targetpre \lottkw{case} \, \targetpre \targetpre x \targetpost \targetpost \, \lottsym{\{} \lottsepbycomprehensioncustom{\targetpre \lottsym{λ} \, \targetpre x' \targetpost \, \lottsym{:} \, \targetpre \targetpre \targetpre a \targetpost \targetpost \, \targetpre A_{i} \targetpost \targetpost \lottsym{.} \, \targetpre \lottsym{ι}_{j} \, \targetpre \targetpre x' \targetpost \targetpost \targetpost \targetpost}{i \in [:n], j \in p'} \lottsym{\}} \targetpost \targetpost \targetpost} }{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottsym{⟨} \lottsepbycomprehensionpatcollection{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i}{[:n]} \lottsym{⟩} \, \rowequivsym_{\mathfrak{c}} \, \lottsym{⟨} \lottsepbycomprehensioncustom{ξ_{i} \, \lottsym{▹} \, τ_{i}}{i \in p} \lottsym{⟩} \, \lottsym{⇝} \, \targetpre Fₚ \targetpost \lottsym{,} \, \targetpre Fₛ \targetpost} \lottinferencerulesep +\lottinferencerule{lift}{ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \rowequivsym_{μ} \, ρ₁ \, \lottsym{⇝} \, \targetpre Fₚ' \targetpost \lottsym{,} \, \targetpre Fₛ' \targetpost}\\ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, ρ₀ \, \kindingsym \, \lottkw{R}^{κ₀}}\\ +\lotthypothesis{Γ_{C} \lottsym{;} \, Γ \lottsym{,} \, a \, \lottsym{:} \, κ₀ \, \lottsym{⊢} \, τ \, \kindingsym \, κ₁ \, \lottsym{⇝} \, \targetpre \targetpre A \targetpost \targetpost}\\ +\lotthypothesis{\lottsym{⊢} \, κ₀ \, \lottsym{⇝} \, \targetpre K₀ \targetpost}\\ +\lotthypothesis{\lottsym{⊢} \, κ₁ \, \lottsym{⇝} \, \targetpre K₁ \targetpost}\\ +\lottlet{\targetpre Fₚ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a' \targetpost \, \lottsym{:} \, \targetpre \targetpre K₁ \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \targetpre Fₚ' \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre K₀ \targetpost \lottsym{.} \, \targetpre \targetpre \targetpre a' \targetpost \targetpost \, \targetpre A \targetpost \targetpost \targetpost \lottsym{]} \targetpost \targetpost}\\ +\lottlet{\targetpre Fₛ \targetpost}{\targetpre \lottsym{Λ} \, \targetpre a' \targetpost \, \lottsym{:} \, \targetpre \targetpre K₁ \targetpost \, \lottsym{↦} \, \targetpre \lottsym{\star} \targetpost \targetpost \lottsym{.} \, \targetpre \targetpre Fₛ' \targetpost \, \lottsym{[} \targetpre \lottsym{λ} \, \targetpre a \targetpost \, \lottsym{:} \, \targetpre K₀ \targetpost \lottsym{.} \, \targetpre \targetpre \targetpre a' \targetpost \targetpost \, \targetpre A \targetpost \targetpost \targetpost \lottsym{]} \targetpost \targetpost} +}{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₀ \, \rowequivsym_{μ} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ \lottsym{)} \, ρ₁ \, \lottsym{⇝} \, \targetpre Fₚ \targetpost \lottsym{,} \, \targetpre Fₛ \targetpost} +\lottinferencerulesep \lottinferencerule{liftL}{ \lotthypothesis{Γ_{C} \lottsym{;} \, Γ \, \lottsym{⊢} \, \lottkw{Lift} \, \lottsym{(} \lottsym{λ} \, a \, \lottsym{:} \, κ₀ \lottsym{.} \, τ' \lottsym{)} \, \lottsym{⟨} \lottsepbycomprehension{ξ_{i} \, \lottsym{▹} \, τ_{i}} \lottsym{⟩} \, \kindingsym \, \lottkw{R}^{κ₁} \, \lottsym{⇝} \, \targetpre A \targetpost}\\ \lotthypothesis{\lottsym{⊢} \, κ₁ \, \lottsym{⇝} \, \targetpre K \targetpost}\\