generic emulation

TabularTypeInterpreter/F⊗⊕ω/Lemmas/Term.lean

@@ -163,6 +163,12 @@ where
   of_eq {E m n} (Elc : TermVarLocallyClosed E m) (eq : m = n) : E.TermVarLocallyClosed n := by
     rwa [eq] at Elc
 
+theorem TermVar_open_TermVar_close_id
+  : TermVarLocallyClosed E n → (TermVar_close E x n).TermVar_open x n = E := by
+  induction E using rec_uniform generalizing n <;> aesop
+    (add simp [TermVar_open, TermVar_close], 40% cases TermVarLocallyClosed,
+      safe List.map_eq_id_of_eq_id_of_mem)
+
 end TermVarLocallyClosed
 
 theorem Term_open_TermVar_open_comm : TermVarLocallyClosed F m → m ≠ n →

TabularTypeInterpreter/Lemmas/Term.lean

@@ -0,0 +1,93 @@
+import TabularTypeInterpreter.Lemmas.Type.Basic
+import TabularTypeInterpreter.Semantics.Term
+
+namespace TabularTypeInterpreter
+
+open Std
+
+namespace Term
+
+namespace TermVarLocallyClosed
+
+theorem weakening : TermVarLocallyClosed M m → TermVarLocallyClosed M (m + n) := sorry
+
+theorem TermVar_open_id : TermVarLocallyClosed M n → TermVar_open M x n = M := sorry
+
+end TermVarLocallyClosed
+
+namespace TypingAndElaboration
+
+theorem TermVarLocallyClosed_of (Mte : [[Γᵢ; Γc; Γ ⊢ M : σ ⇝ E]]) : M.TermVarLocallyClosed := sorry
+
+theorem weakening (Mte : [[Γᵢ; Γc; Γ, Γ'' ⊢ M : σ ⇝ E]]) (Γwe : [[Γc ⊢ Γ, Γ', Γ'' ⇝ Δ]])
+  : [[Γᵢ; Γc; Γ, Γ', Γ'' ⊢ M : σ ⇝ E]] := by
+  sorry
+  -- generalize Γ'''eq : [[Γ, Γ'']] = Γ''' at Mte
+  -- induction Mte generalizing Δ Γ'' <;> try cases Γ'''eq
+  -- · case var xσinΓ =>
+  --   sorry
+  -- · case lam I _ τ₀ke ih =>
+  --   let τ₀ke' := τ₀ke.weakening Γwe
+  --   apply lam (I ++ [[Γ, Γ', Γ'']].termVarDom) _ τ₀ke'
+  --   intro x xnin
+  --   let ⟨xninI, xninΓ⟩ := List.not_mem_append'.mp xnin
+  --   let Γxwe := Γwe.termExt xninΓ τ₀ke'
+  --   rw [← TypeEnvironment.append, ← TypeEnvironment.append] at Γxwe ⊢
+  --   exact ih x xninI Γxwe rfl
+  -- · case app _ _ M'ih Nih => exact app (M'ih Γwe rfl) (Nih Γwe rfl)
+  -- · case qualI I ψke _ ih =>
+  --   let ψke' := ψke.weakening Γwe
+  --   apply qualI (I ++ [[Γ, Γ', Γ'']].termVarDom) ψke'
+  --   intro x xnin
+  --   let ⟨xninI, xninΓ⟩ := List.not_mem_append'.mp xnin
+  --   let Γxwe := Γwe.constrExt xninΓ ψke'
+  --   rw [← TypeEnvironment.append, ← TypeEnvironment.append] at Γxwe ⊢
+  --   exact ih x xninI Γxwe rfl
+  -- · case qualE ψce _ ih =>
+  --   apply qualE <| ψce.weakening
+
+theorem singleton_prod (Mte : [[Γᵢ; Γc; Γ ⊢ M : ⌊ξ⌋ ⇝ F]]) (Nte : [[Γᵢ; Γc; Γ ⊢ «N» : τ ⇝ E]])
+  (ξke : [[Γc; Γ ⊢ ξ : L ⇝ A₀]]) (τke : [[Γc; Γ ⊢ τ : * ⇝ A₁]]) (μke : [[Γc; Γ ⊢ μ : U ⇝ B]])
+  : [[Γᵢ; Γc; Γ ⊢ {M ▹ «N»} : Π(μ) ⟨ξ ▹ τ⟩ ⇝ ⦅λ x : ⊗ {A₁}. x$0⦆ (E)]] := by
+  let prodte := prod (by
+    intro _ mem
+    cases Nat.eq_of_le_of_lt_succ mem.lower mem.upper
+    exact Mte
+  ) (by rw [Range.map_eq_cons_of_lt Nat.zero_lt_one, Range.map_same_eq_nil]; exact .var) (by
+    intro _ mem
+    cases Nat.eq_of_le_of_lt_succ mem.lower mem.upper
+    exact Nte
+  ) (.inl nofun) (b := false) (n := 1) (Γᵢ := Γᵢ) (Γc := Γc) (Γ := Γ)
+    (M := fun _ => M) («N» := fun _ => «N») (ξ := fun _ => ξ)
+    (τ := fun _ => τ) (E := fun _ => E) (F := fun _ => F)
+  rw [Range.map_eq_cons_of_lt Nat.zero_lt_one, Range.map_eq_cons_of_lt Nat.zero_lt_one,
+      Range.map_eq_cons_of_lt Nat.zero_lt_one, Range.map_same_eq_nil, Range.map_same_eq_nil,
+      Range.map_same_eq_nil, Option.someIf, if_neg nofun] at prodte
+  simp only at prodte
+  let prodte' := prodte.sub <| .decay (.prod .comm <| .singleton_row ξke τke) μke .N
+  exact prodte'
+
+instance : Inhabited Term where
+  default := .prod []
+in
+instance __ : Inhabited Monotype where
+  default := .row [] none
+in
+instance : Inhabited «F⊗⊕ω».Term where
+  default := .prodIntro []
+in
+theorem unit (μke : [[Γc; Γ ⊢ μ : U ⇝ B]])
+  : [[Γᵢ; Γc; Γ ⊢ {} : Π(μ) ⟨ : * ⟩ ⇝ ⦅λ x : ⊗ { }. x$0⦆ ()]] := by
+  let prodte := prod nofun (.concrete nofun) nofun (.inr rfl) (n := 0) (Γᵢ := Γᵢ) (Γc := Γc) (Γ := Γ)
+    (M := fun _ => default) («N» := fun _ => default) (ξ := fun _ => .label .zero)
+    (τ := fun _ => default) (E := fun _ => default) (F := fun _ => default)
+  rw [Range.map_same_eq_nil, Range.map_same_eq_nil, Range.map_same_eq_nil, Option.someIf,
+      if_pos rfl] at prodte
+  let prodte' := prodte.sub <| .decay (.prod .comm .empty_row) μke .N
+  exact prodte'
+
+end TypingAndElaboration
+
+end Term
+
+end TabularTypeInterpreter

TabularTypeInterpreter/Semantics/Term.lean

@@ -40,8 +40,8 @@ x : σ ∈ Γ
 Γᵢ; Γc; Γ ⊢ M «N» : τ₁ ⇝ F E
 
 Γc; Γ ⊢ ψ : C ⇝ A
-∀ x ∉ I, Γᵢ; Γc; Γ, ψ ⇝ x ⊢ M^x : γ ⇝ E^x
-───────────────────────────────────────── qualI (I : List TermVarId)
+∀ x ∉ I, Γᵢ; Γc; Γ, ψ ⇝ x ⊢ M : γ ⇝ E^x
+─────────────────────────────────────── qualI (I : List TermVarId)
 Γᵢ; Γc; Γ ⊢ M : ψ ⇒ γ ⇝ λ x : A. E
 
 Γᵢ; Γc; Γ ⊨ ψ ⇝ E
@@ -118,10 +118,10 @@ notex n ≠ 0 ∨ b
 ──────────────────────────────────────────────────────────────────────── elim
 Γᵢ; Γc; Γ ⊢ M ▿ «N» : (Σ(μ) ρ₂) → τ ⇝ ⦅⦅π 1 F⦆ [λ a : *. a$0] [A] E₀⦆ E₁
 
-Γᵢ; Γc; Γ ⊢ M : τ₀ ⇝ E
-Γc; Γ ⊢ τ₀ <: τ₁ ⇝ F
+Γᵢ; Γc; Γ ⊢ M : σ₀ ⇝ E
+Γc; Γ ⊢ σ₀ <: σ₁ ⇝ F
 ──────────────────────── sub
-Γᵢ; Γc; Γ ⊢ M : τ₁ ⇝ F E
+Γᵢ; Γc; Γ ⊢ M : σ₁ ⇝ F E
 
 (</ TCₛ@i a ⇝ Aₛ@i // i in [:n] notex /> ⇒ TC a : κ) ↦ m : σ ⇝ A ∈ Γc
 Γᵢ; Γc; Γ ⊨ TC τ ⇝ E

TabularTypeInterpreter/Theorems.lean

@@ -1,3 +1,4 @@
+import TabularTypeInterpreter.Theorems.GenericEmulation
 import TabularTypeInterpreter.Theorems.Kind
 import TabularTypeInterpreter.Theorems.Program
 import TabularTypeInterpreter.Theorems.Term