From 568794f47bb3c25ec9470d04544750297b5b5f0a Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Wed, 3 Jul 2024 16:16:20 +0100 Subject: [PATCH] Tensor product lore --- .../BinSyntax/Rewrite/Categorical.lean | 202 +++++++++++++++++- .../BinSyntax/Rewrite/Definitions.lean | 44 +++- DeBruijnSSA/BinSyntax/Rewrite/Subst.lean | 46 ++++ DeBruijnSSA/BinSyntax/Subst.lean | 101 +++++++-- DeBruijnSSA/BinSyntax/Typing.lean | 49 +++++ 5 files changed, 423 insertions(+), 19 deletions(-) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Categorical.lean b/DeBruijnSSA/BinSyntax/Rewrite/Categorical.lean index 5d1163c..df780a2 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Categorical.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Categorical.lean @@ -13,17 +13,44 @@ theorem Wf.ret {tyIn tyOut : Ty α} {rest: Ctx α ε} {targets : LCtx α} def InS.ret {tyIn tyOut : Ty α} {rest: Ctx α ε} {targets : LCtx α} (t : Term.InS φ (⟨tyIn, ⊥⟩::rest) ⟨tyOut, ⊥⟩) - : InS φ (⟨tyIn, ⊥⟩::rest) (tyOut::targets) := ⟨Region.ret t, Wf.ret t.prop⟩ + : InS φ (⟨tyIn, ⊥⟩::rest) (tyOut::targets) := InS.br 0 t ⟨by simp, le_refl _⟩ + +theorem InS.ret_eq {tyIn tyOut : Ty α} {rest: Ctx α ε} {targets : LCtx α} + (t : Term.InS φ (⟨tyIn, ⊥⟩::rest) ⟨tyOut, ⊥⟩) + : InS.ret (targets := targets) t = ⟨Region.ret t, Wf.ret t.prop⟩ := rfl + +theorem InS.vwk_ret {tyIn tyOut : Ty α} {rest: Ctx α ε} {targets : LCtx α} + (ρ : Ctx.InS (⟨tyIn, ⊥⟩::rest') _) + (t : Term.InS φ (⟨tyIn, ⊥⟩::rest) ⟨tyOut, ⊥⟩) + : (InS.ret (targets := targets) t).vwk ρ = InS.ret (t.wk ρ) := rfl abbrev Eqv.ret {tyIn tyOut : Ty α} {rest: Ctx α ε} {targets : LCtx α} (t : Term.InS φ (⟨tyIn, ⊥⟩::rest) ⟨tyOut, ⊥⟩) : Eqv φ (⟨tyIn, ⊥⟩::rest) (tyOut::targets) := ⟦InS.ret t⟧ +theorem Eqv.vwk_ret {tyIn tyOut : Ty α} {rest: Ctx α ε} {targets : LCtx α} + (ρ : Ctx.InS (⟨tyIn, ⊥⟩::rest') _) + (t : Term.InS φ (⟨tyIn, ⊥⟩::rest) ⟨tyOut, ⊥⟩) + : (Eqv.ret (targets := targets) t).vwk ρ = Eqv.ret (t.wk ρ) := rfl + theorem Wf.nil {ty : Ty α} {rest: Ctx α ε} {targets : LCtx α} : Region.nil.Wf (φ := φ) (⟨ty, ⊥⟩::rest) (ty::targets) := Wf.ret (by simp) def InS.nil {ty : Ty α} {rest: Ctx α ε} {targets : LCtx α} - : InS φ (⟨ty, ⊥⟩::rest) (ty::targets) := ⟨Region.nil, Wf.nil⟩ + : InS φ (⟨ty, ⊥⟩::rest) (ty::targets) := InS.ret (Term.InS.var 0 (by simp)) + +theorem InS.nil_eq {ty : Ty α} {rest: Ctx α ε} {targets : LCtx α} + : InS.nil (φ := φ) (ty := ty) (rest := rest) (targets := targets) = ⟨Region.nil, Wf.nil⟩ := rfl + +@[simp] +theorem InS.nil_vwk_lift (ρ : Ctx.InS rest _) + : (InS.nil (φ := φ) (ty := ty) (rest := rest') (targets := targets)).vwk (ρ.lift h) = InS.nil + := rfl + +@[simp] +theorem InS.nil_vwk1 + : (InS.nil (φ := φ) (ty := ty) (rest := rest) (targets := targets)).vwk1 (right := right) + = InS.nil := rfl -- theorem InS.coe_nil {ty : Ty α} {rest: Ctx α ε} {targets : LCtx α} -- : (InS.nil (ty := ty) (rest := rest) (targets := targets) : Region φ) = Region.nil := rfl @@ -31,6 +58,26 @@ def InS.nil {ty : Ty α} {rest: Ctx α ε} {targets : LCtx α} abbrev Eqv.nil {ty : Ty α} {rest: Ctx α ε} {targets : LCtx α} : Eqv φ (⟨ty, ⊥⟩::rest) (ty::targets) := ⟦InS.nil⟧ +@[simp] +theorem Eqv.nil_vwk_lift (ρ : Ctx.InS rest _) + : (Eqv.nil (φ := φ) (ty := ty) (rest := rest') (targets := targets)).vwk (ρ.lift h) = Eqv.nil + := rfl + +@[simp] +theorem Eqv.nil_vwk_liftn₂ (ρ : Ctx.InS rest _) + : (Eqv.nil (φ := φ) (ty := ty) (rest := (head'::rest')) (targets := targets)).vwk (ρ.liftn₂ h h') + = Eqv.nil + := rfl + +theorem Eqv.nil_vwk1 {Γ : Ctx α ε} {L : LCtx α} + : (Eqv.nil (φ := φ) (ty := ty) (rest := Γ) (targets := L)).vwk1 (inserted := inserted) + = Eqv.nil := rfl + +theorem Eqv.let1_0_nil + : Eqv.let1 (Term.InS.var 0 ⟨by simp, le_refl _⟩) Eqv.nil + = Eqv.nil (φ := φ) (ty := ty) (rest := rest) (targets := targets) + := by rw [let1_beta]; rfl + def Wf.lsubst0 {Γ : Ctx α ε} {L : LCtx α} {r : Region φ} (hr : r.Wf (⟨A, ⊥⟩::Γ) L) : r.lsubst0.Wf Γ (A::L) L := Fin.cases hr (λi => Wf.br ⟨i.prop, le_refl _⟩ (by simp)) @@ -59,10 +106,25 @@ theorem InS.alpha0_congr {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} {r r' : In (h : r ≈ r') : InS.alpha0 r ≈ InS.alpha0 r' := sorry +theorem InS.vlift_alpha0 {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (r : InS φ (⟨A, ⊥⟩::Γ) (B::L)) + : (InS.alpha0 r).vlift = InS.alpha0 (r.vwk1 (right := X)) := by + simp only [Subst.InS.vlift, Set.mem_setOf_eq, alpha0, vlift_alpha] + rfl + def Eqv.alpha0 {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) : Subst.Eqv φ Γ (A::L) (B::L) := Quot.liftOn r (λr => ⟦InS.alpha0 r⟧) (λ_ _ h => Quotient.sound $ InS.alpha0_congr h) +@[simp] +theorem Eqv.alpha0_quot {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (r : InS φ (⟨A, ⊥⟩::Γ) (B::L)) + : Eqv.alpha0 ⟦r⟧ = ⟦InS.alpha0 r⟧ := rfl + +theorem Eqv.vlift_alpha0 {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) + : (Eqv.alpha0 r).vlift = Eqv.alpha0 (r.vwk1 (inserted := X)) := by + induction r using Quotient.inductionOn; + rw [alpha0_quot, Subst.Eqv.vlift_quot, InS.vlift_alpha0] + rfl + def InS.seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} (left : InS φ (⟨A, ⊥⟩::Γ) (B::L)) (right : InS φ (⟨B, ⊥⟩::Γ) (C::L)) : InS φ (⟨A, ⊥⟩::Γ) (C::L) := left.lsubst right.vwk1.alpha0 @@ -89,13 +151,13 @@ theorem InS.append_mk {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} theorem InS.append_nil {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} {l : InS φ (⟨A, ⊥⟩::Γ) (B::L)} : (l ++ InS.nil (φ := φ) (ty := B) (rest := Γ) (targets := L)) = l := by - cases l; simp [InS.nil, append_mk, Region.append_nil] + cases l; simp [nil_eq, append_mk, Region.append_nil] @[simp] theorem InS.nil_append {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} {l : InS φ (⟨A, ⊥⟩::Γ) (B::L)} : (InS.nil (φ := φ) (ty := A) (rest := Γ) (targets := L) ++ l) = l := by - cases l; simp [InS.nil, append_mk, Region.nil_append] + cases l; simp [nil_eq, append_mk, Region.nil_append] theorem InS.append_assoc {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α} (left : InS φ (⟨A, ⊥⟩::Γ) (B::L)) @@ -105,6 +167,14 @@ theorem InS.append_assoc {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α} cases left; cases middle; cases right; simp [append_mk, Region.append_assoc] +-- theorem InS.let1_seq {Γ : Ctx α ε} {L : LCtx α} +-- (a : Term.InS φ (⟨A, ⊥⟩::Γ) ⟨X, e⟩) +-- (r : InS φ (⟨X, ⊥⟩::⟨A, ⊥⟩::Γ) (B::L)) (s : InS φ (⟨B, ⊥⟩::Γ) (C::L)) +-- : (let1 a r) ++ s = let1 a (r ++ (s.vwk1 (right := ⟨X, ⊥⟩))) := by +-- induction r using Quotient.inductionOn; +-- induction s using Quotient.inductionOn; +-- sorry + def Eqv.seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} (left : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (right : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) : Eqv φ (⟨A, ⊥⟩::Γ) (C::L) := left.lsubst right.vwk1.alpha0 @@ -159,6 +229,80 @@ theorem Eqv.seq_assoc {A B C D : Ty α} {Γ : Ctx α ε} {L : LCtx α} induction right using Quotient.inductionOn; simp [InS.append_assoc] +theorem Eqv.ret_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} + (a : Term.InS φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩) + (r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) + : (Eqv.ret a) ;; r = r.vwk1.vsubst a.subst0 := by + induction r using Quotient.inductionOn; + simp only [ret, seq_def, vwk1_quot, alpha0_quot, lsubst_quot, vsubst_quot] + rfl + +theorem Eqv.ret_seq_let {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} + (a : Term.InS φ (⟨A, ⊥⟩::Γ) ⟨B, ⊥⟩) + (r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) + : (Eqv.ret a) ;; r = let1 a r.vwk1 := by rw [ret_seq, let1_beta] + +theorem Eqv.let1_seq {Γ : Ctx α ε} {L : LCtx α} + (a : Term.InS φ (⟨A, ⊥⟩::Γ) ⟨X, e⟩) + (r : Eqv φ (⟨X, ⊥⟩::⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) + : (Eqv.let1 a r) ;; s = Eqv.let1 a (r ;; s.vwk1) := by + simp only [seq_def, lsubst_let1, vlift_alpha0] + +theorem Eqv.let2_seq {Γ : Ctx α ε} {L : LCtx α} + (a : Term.InS φ (⟨A, ⊥⟩::Γ) ⟨X.prod Y, e⟩) + (r : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨A, ⊥⟩::Γ) (C::L)) (s : Eqv φ (⟨C, ⊥⟩::Γ) (D::L)) + : (Eqv.let2 a r) ;; s = Eqv.let2 a (r ;; s.vwk1.vwk1) := by + simp only [seq_def, lsubst_let2, Subst.Eqv.vliftn₂_eq_vlift_vlift, vlift_alpha0] + +theorem Eqv.case_seq {Γ : Ctx α ε} {L : LCtx α} + (a : Term.InS φ (⟨A, ⊥⟩::Γ) ⟨X.coprod Y, e⟩) + (r : Eqv φ (⟨X, ⊥⟩::⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨Y, ⊥⟩::⟨A, ⊥⟩::Γ) (B::L)) + (t : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) + : (Eqv.case a r s) ;; t = Eqv.case a (r ;; t.vwk1) (s ;; t.vwk1) := by + simp only [seq_def, lsubst_case, vlift_alpha0] + +theorem Eqv.vwk_lift_seq {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} + (ρ : Ctx.InS Γ Δ) + (left : Eqv φ (⟨A, ⊥⟩::Δ) (B::L)) + (right : Eqv φ (⟨B, ⊥⟩::Δ) (C::L)) + : (left ;; right).vwk (ρ.lift (le_refl _)) + = left.vwk (ρ.lift (le_refl _)) ;; right.vwk (ρ.lift (le_refl _)) := by + induction left using Quotient.inductionOn; + induction right using Quotient.inductionOn; + sorry + +theorem Eqv.vwk_liftn₂_seq {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} + (ρ : Ctx.InS Γ Δ) + (left : Eqv φ (⟨A, ⊥⟩::X::Δ) (B::L)) + (right : Eqv φ (⟨B, ⊥⟩::X::Δ) (C::L)) + : (left ;; right).vwk (ρ.liftn₂ (le_refl _) (le_refl _)) + = left.vwk (ρ.liftn₂ (le_refl _) (le_refl _)) ;; right.vwk (ρ.liftn₂ (le_refl _) (le_refl _)) + := by simp only [<-Ctx.InS.lift_lift, vwk_lift_seq] + +theorem Eqv.vwk1_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} + (left : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) + (right : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) + : (left ;; right).vwk1 (inserted := inserted) + = left.vwk1 ;; right.vwk1 := vwk_lift_seq ⟨Nat.succ, (by simp)⟩ left right + +theorem Eqv.vsubst_lift_seq {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} + (σ : Term.Subst.InS φ Γ Δ) + (left : Eqv φ (⟨A, ⊥⟩::Δ) (B::L)) + (right : Eqv φ (⟨B, ⊥⟩::Δ) (C::L)) + : (left ;; right).vsubst (σ.lift (le_refl _)) + = left.vsubst (σ.lift (le_refl _)) ;; right.vsubst (σ.lift (le_refl _)) := by + induction left using Quotient.inductionOn; + induction right using Quotient.inductionOn; + sorry + +theorem Eqv.vsubst_liftn₂_seq {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α} + (σ : Term.Subst.InS φ Γ Δ) + (left : Eqv φ (⟨A, ⊥⟩::X::Δ) (B::L)) + (right : Eqv φ (⟨B, ⊥⟩::X::Δ) (C::L)) + : (left ;; right).vsubst (σ.liftn₂ (le_refl _) (le_refl _)) + = left.vsubst (σ.liftn₂ (le_refl _) (le_refl _)) ;; right.vsubst (σ.liftn₂ (le_refl _) (le_refl _)) + := by simp only [<-Term.Subst.InS.lift_lift, vsubst_lift_seq] + open Term.InS def Eqv.rtimes {tyIn tyOut : Ty α} {Γ : Ctx α ε} {L : LCtx α} @@ -173,14 +317,46 @@ def Eqv.swap {left right : Ty α} {Γ : Ctx α ε} {L : LCtx α} := Eqv.let2 (var 0 Ctx.Var.shead) $ ret (pair (var 0 (by simp)) (var 1 (by simp))) +theorem Eqv.repack {left right : Ty α} {rest : Ctx α ε} {targets : LCtx α} + : Eqv.let2 (Term.InS.var 0 ⟨by simp, le_refl _⟩) + (Eqv.ret (Term.InS.pair (Term.InS.var 1 (by simp)) (Term.InS.var 0 (by simp)))) + = Eqv.nil (φ := φ) (ty := left.prod right) (rest := rest) (targets := targets) := by + rw [<-let1_0_nil, <-let2_eta, let1_beta] + rfl + theorem Eqv.swap_swap {left right : Ty α} : Eqv.swap ;; Eqv.swap = (Eqv.nil (φ := φ) (ty := left.prod right) (rest := rest) (targets := targets)) := by - rw [Eqv.seq_def, swap, vwk1, swap] - sorry + simp only [ + swap, let2_seq, vwk1, vwk_let2, wk_var, wk_pair, Nat.liftWk, vwk_ret, Ctx.InS.liftn₂, + Nat.liftnWk, Nat.one_lt_ofNat, Nat.ofNat_pos, ↓reduceIte, ret_seq, vsubst_let2, + subst_pair, subst_var, Term.Subst.InS.get_0_subst0, let2_pair, let1_beta, vsubst_vsubst + ] + apply Eqv.repack infixl:70 " ⋊ " => Eqv.rtimes +theorem Eqv.rtimes_nil {ty : Ty α} {Γ : Ctx α ε} {L : LCtx α} + (tyLeft : Ty α) + : tyLeft ⋊ Eqv.nil = (Eqv.nil (φ := φ) (ty := tyLeft.prod ty) (rest := Γ) (targets := L)) := by + simp only [rtimes, nil_vwk1, nil_seq, repack] + +theorem Eqv.rtimes_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} + (tyLeft : Ty α) (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) + : tyLeft ⋊ (r ;; s) = (tyLeft ⋊ r) ;; (tyLeft ⋊ s) := by + apply Eq.symm + rw [rtimes, rtimes, let2_seq, seq_assoc, ret_seq] + simp only [ + vwk1, vwk_let2, wk_var, Nat.liftWk, vsubst_let2, vwk_vwk, Ctx.InS.liftn₂_comp_liftn₂, + subst_pair, subst_var, Term.Subst.InS.get_0_subst0, let2_pair, let1_beta, + vsubst_vsubst + ] + apply congrArg + rw [vwk1_seq, vwk1_seq, seq_assoc] + congr 1 + . simp [vwk1, vwk_vwk] + . sorry + def Eqv.ltimes {tyIn tyOut : Ty α} {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (⟨tyIn, ⊥⟩::Γ) (tyOut::L)) (tyRight : Ty α) : Eqv φ (⟨tyIn.prod tyRight, ⊥⟩::Γ) ((tyOut.prod tyRight)::L) @@ -203,3 +379,17 @@ theorem Eqv.swap_ltimes_swap {Γ : Ctx α ε} {L : LCtx α} : Eqv.swap ;; r ⋉ C ;; Eqv.swap = C ⋊ r := by rw [ ltimes, seq_assoc, seq_assoc, swap_swap, seq_assoc, seq_nil, <-seq_assoc, swap_swap, nil_seq] + +theorem Eqv.ltimes_nil {ty : Ty α} {Γ : Ctx α ε} {L : LCtx α} + : Eqv.nil ⋉ tyRight = (Eqv.nil (φ := φ) (ty := ty.prod tyRight) (rest := Γ) (targets := L)) + := by rw [<-swap_rtimes_swap, rtimes_nil, seq_nil, swap_swap] + +theorem Eqv.ltimes_seq {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α} + (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)) + : (r ;; s) ⋉ tyRight = (r ⋉ tyRight) ;; (s ⋉ tyRight) := by + simp only [<-swap_rtimes_swap, rtimes_seq, seq_assoc] + rw [<-seq_assoc swap swap, swap_swap, nil_seq] + +end Region + +end BinSyntax diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean b/DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean index 21e9c18..12bc4a9 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Definitions.lean @@ -908,6 +908,33 @@ theorem InS.vsubst_q {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.InS φ theorem Eqv.vsubst_quot {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.InS φ Γ Δ} {r : InS φ Δ L} : Eqv.vsubst σ ⟦r⟧ = ⟦r.vsubst σ⟧ := rfl +theorem Eqv.vsubst_vsubst {Γ Δ Ξ : Ctx α ε} {L : LCtx α} {r : Eqv φ Ξ L} + {σ : Term.Subst.InS φ Γ Δ} {τ : Term.Subst.InS φ Δ Ξ} + : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) := by + induction r using Quotient.inductionOn; + simp [InS.vsubst_vsubst] + +@[simp] +theorem Eqv.vsubst_let1 {Γ : Ctx α ε} {L : LCtx α} + {σ : Term.Subst.InS φ Γ Δ} {a : Term.InS φ Δ ⟨A, e⟩} {r : Eqv φ (⟨A, ⊥⟩::Δ) L} + : Eqv.vsubst σ (Eqv.let1 a r) = Eqv.let1 (a.subst σ) (Eqv.vsubst (σ.lift (le_refl _)) r) := by + induction r using Quotient.inductionOn; rfl + +@[simp] +theorem Eqv.vsubst_let2 {Γ : Ctx α ε} {L : LCtx α} + {σ : Term.Subst.InS φ Γ Δ} {a : Term.InS φ Δ ⟨Ty.prod A B, e⟩} {r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Δ) L} + : Eqv.vsubst σ (Eqv.let2 a r) + = Eqv.let2 (a.subst σ) (Eqv.vsubst (σ.liftn₂ (le_refl _) (le_refl _)) r) := by + induction r using Quotient.inductionOn; rfl + +@[simp] +theorem Eqv.vsubst_case {Γ : Ctx α ε} {L : LCtx α} + {σ : Term.Subst.InS φ Γ Δ} {e : Term.InS φ Δ ⟨Ty.coprod A B, e⟩} + {r : Eqv φ (⟨A, ⊥⟩::Δ) L} {s : Eqv φ (⟨B, ⊥⟩::Δ) L} + : Eqv.vsubst σ (Eqv.case e r s) + = Eqv.case (e.subst σ) (Eqv.vsubst (σ.lift (le_refl _)) r) (Eqv.vsubst (σ.lift (le_refl _)) s) + := by induction r using Quotient.inductionOn; induction s using Quotient.inductionOn; rfl + @[simp] theorem InS.lwk_id_q {Γ : Ctx α ε} {L K : LCtx α} {r : InS φ Γ L} (hρ : L.Wkn K id) : (r.q).lwk_id hρ = (r.lwk_id hρ).q := rfl @@ -1451,7 +1478,22 @@ theorem Eqv.cfg_zero {Γ : Ctx α ε} {L : LCtx α} : β.cfg [] (λi => i.elim0) = β := by induction β using Quotient.inductionOn with | h β => exact Eqv.sound $ β.cfg_zero --- TODO: let2_eta +theorem InS.let2_eta {Γ : Ctx α ε} {L : LCtx α} + (a : Term.InS φ Γ ⟨Ty.prod A B, ea⟩) + (r : InS φ (⟨A.prod B, ⊥⟩::Γ) L) + : (let2 a $ + let1 ((Term.InS.var 1 ⟨by simp, le_refl _⟩).pair (Term.InS.var 0 (by simp))) r.vwk1.vwk1) + ≈ let1 a r + := EqvGen.rel _ _ $ Wf.Cong.rel $ + TStep.step InS.coe_wf InS.coe_wf (FStep.rw (by constructor)) + +theorem Eqv.let2_eta {Γ : Ctx α ε} {L : LCtx α} + (a : Term.InS φ Γ ⟨Ty.prod A B, ea⟩) + (r : Eqv φ (⟨A.prod B, ⊥⟩::Γ) L) + : (let2 a $ + let1 ((Term.InS.var 1 ⟨by simp, le_refl _⟩).pair (Term.InS.var 0 (by simp))) r.vwk1.vwk1) + = let1 a r + := by induction r using Quotient.inductionOn with | h r => exact Eqv.sound $ InS.let2_eta a r theorem InS.wk_cfg {Γ : Ctx α ε} {L : LCtx α} (R S : LCtx α) (β : InS φ Γ (R ++ L)) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Subst.lean b/DeBruijnSSA/BinSyntax/Rewrite/Subst.lean index fd0ba1b..284c831 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Subst.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Subst.lean @@ -30,6 +30,31 @@ def Eqv.lsubst {Γ : Ctx α ε} {L K : LCtx α} (σ : Subst.Eqv φ Γ L K) (r : (λσ r => (r.lsubst σ).q) sorry +def Subst.Eqv.vlift {Γ : Ctx α ε} {L K : LCtx α} (σ : Subst.Eqv φ Γ L K) + : Subst.Eqv φ (head::Γ) L K + := Quotient.liftOn σ + (λσ => ⟦σ.vlift⟧) + sorry + +@[simp] +theorem Subst.Eqv.vlift_quot {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K} + : vlift (head := head) ⟦σ⟧ = ⟦σ.vlift⟧ := rfl + +def Subst.Eqv.vliftn₂ {Γ : Ctx α ε} {L K : LCtx α} (σ : Subst.Eqv φ Γ L K) + : Subst.Eqv φ (left::right::Γ) L K + := Quotient.liftOn σ + (λσ => ⟦σ.vliftn₂⟧) + sorry + +@[simp] +theorem Subst.Eqv.vliftn₂_quot {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K} + : vliftn₂ (left := left) (right := right) ⟦σ⟧ = ⟦σ.vliftn₂⟧ := rfl + +theorem Subst.Eqv.vliftn₂_eq_vlift_vlift {Γ : Ctx α ε} {L K : LCtx α} (σ : Subst.Eqv φ Γ L K) + : σ.vliftn₂ (left := left) (right := right) = σ.vlift.vlift := by + induction σ using Quotient.inductionOn; + simp [Subst.InS.vliftn₂_eq_vlift_vlift] + @[simp] theorem InS.lsubst_q {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K} {r : InS φ Γ L} : (r.q).lsubst ⟦σ⟧ = (r.lsubst σ).q := rfl @@ -38,4 +63,25 @@ theorem InS.lsubst_q {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K} theorem Eqv.lsubst_quot {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K} {r : InS φ Γ L} : lsubst ⟦σ⟧ ⟦r⟧ = ⟦r.lsubst σ⟧ := rfl +@[simp] +theorem Eqv.lsubst_let1 {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L K} + {a : Term.InS φ Γ ⟨A, e⟩} {r : Eqv φ (⟨A, ⊥⟩::Γ) L} + : (let1 a r).lsubst σ = let1 a (r.lsubst σ.vlift) := by + induction r using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl + +@[simp] +theorem Eqv.lsubst_let2 {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L K} + {a : Term.InS φ Γ ⟨A.prod B, e⟩} {r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L} + : (let2 a r).lsubst σ = let2 a (r.lsubst σ.vliftn₂) := by + induction r using Quotient.inductionOn; induction σ using Quotient.inductionOn; rfl + +@[simp] +theorem Eqv.lsubst_case {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.Eqv φ Γ L K} + {a : Term.InS φ Γ ⟨A.coprod B, e⟩} {r : Eqv φ (⟨A, ⊥⟩::Γ) L} {s : Eqv φ (⟨B, ⊥⟩::Γ) L} + : (case a r s).lsubst σ = case a (r.lsubst σ.vlift) (s.lsubst σ.vlift) := by + induction r using Quotient.inductionOn; induction s using Quotient.inductionOn; + induction σ using Quotient.inductionOn; rfl + +-- TODO: lsubst_cfg + end Region diff --git a/DeBruijnSSA/BinSyntax/Subst.lean b/DeBruijnSSA/BinSyntax/Subst.lean index ced495e..09d9f12 100644 --- a/DeBruijnSSA/BinSyntax/Subst.lean +++ b/DeBruijnSSA/BinSyntax/Subst.lean @@ -120,6 +120,14 @@ theorem Term.Subst.Wf.liftn₂ (h₁ : V₁ ≤ V₁') (h₂ : V₂ ≤ V₂') ( : (σ.liftn 2).Wf (V₁::V₂::Γ) (V₁'::V₂'::Δ) := Subst.liftn_eq_iterate_lift 2 ▸ hσ.lift₂ h₁ h₂ +def Term.Subst.InS.liftn₂ (h₁ : V₁ ≤ V₁') (h₂ : V₂ ≤ V₂') (σ : Subst.InS φ Γ Δ) + : Subst.InS φ (V₁::V₂::Γ) (V₁'::V₂'::Δ) + := ⟨Subst.liftn 2 σ, σ.prop.liftn₂ h₁ h₂⟩ + +theorem Term.Subst.InS.lift_lift (h₁ : V₁ ≤ V₁') (h₂ : V₂ ≤ V₂') (σ : Subst.InS φ Γ Δ) + : (σ.lift h₂).lift h₁ = (σ.liftn₂ h₁ h₂) + := by simp [lift, liftn₂, Subst.liftn_succ] + def Term.Subst.WfD.sliftn₂ {left right} (hσ : σ.WfD Γ Δ) : (σ.liftn 2).WfD (left::right::Γ) (left::right::Δ) := hσ.liftn₂ (le_refl _) (le_refl _) @@ -146,6 +154,7 @@ def Term.WfD.subst {a : Term φ} (hσ : σ.WfD Γ Δ) : a.WfD Δ V → (a.subst theorem Term.Wf.subst {a : Term φ} (hσ : σ.Wf Γ Δ) (h : a.Wf Δ V) : (a.subst σ).Wf Γ V := let ⟨d⟩ := h.nonempty; let ⟨hσ⟩ := hσ.nonempty; (d.subst hσ).toWf + def Term.InS.subst (σ : Subst.InS φ Γ Δ) (a : InS φ Δ V) : InS φ Γ V := ⟨(a : Term φ).subst σ, a.prop.subst σ.prop⟩ @@ -154,6 +163,44 @@ theorem Term.InS.coe_subst {σ : Subst.InS φ Γ Δ} {a : InS φ Δ V} : (a.subst σ : Term φ) = (a : Term φ).subst σ := rfl +def Term.Subst.InS.get (n) (h : Δ.Var n V) (σ : Subst.InS φ Γ Δ) : Term.InS φ Γ V + := ⟨σ.val n, h.subst' σ.prop⟩ + +@[simp] +theorem Term.InS.subst_var (σ : Subst.InS φ Γ Δ) (h : Δ.Var n V) : + (var n h).subst σ = σ.get n h + := rfl + +@[simp] +theorem Term.InS.subst_op (σ : Subst.InS φ Γ Δ) (df : Φ.EFn f A B e) (de : InS φ Δ ⟨A, e⟩) : + (op f df de).subst σ = op f df (de.subst σ) + := rfl + +@[simp] +theorem Term.InS.subst_pair (σ : Subst.InS φ Γ Δ) (dl : InS φ Δ ⟨A, e⟩) (dr : InS φ Δ ⟨B, e⟩) : + (pair dl dr).subst σ = pair (dl.subst σ) (dr.subst σ) + := rfl + +@[simp] +theorem Term.InS.subst_inl (σ : Subst.InS φ Γ Δ) (d : InS φ Δ ⟨A, e⟩) : + (inl (right := right) d).subst σ = inl (d.subst σ) + := rfl + +@[simp] +theorem Term.InS.subst_inr (σ : Subst.InS φ Γ Δ) (d : InS φ Δ ⟨B, e⟩) : + (inr (left := left) d).subst σ = inr (d.subst σ) + := rfl + +@[simp] +theorem Term.InS.subst_abort (σ : Subst.InS φ Γ Δ) (d : InS φ Δ ⟨Ty.empty, e⟩) : + (abort (tyOut := tyOut) d).subst σ = abort (tyOut := tyOut) (d.subst σ) + := rfl + +@[simp] +theorem Term.InS.subst_unit (σ : Subst.InS φ Γ Δ) (e : ε) : + (unit e).subst σ = unit e + := rfl + theorem Term.InS.subst_equiv {σ τ : Subst.InS φ Γ Δ} (a : InS φ Δ V) (h : σ ≈ τ) : a.subst σ = a.subst τ := sorry @@ -172,6 +219,18 @@ theorem Term.InS.coe_subst0 {a : InS φ Γ V} : (a.subst0 : Subst φ) = (a : Term φ).subst0 := rfl +@[simp] +theorem Term.Subst.InS.get_0_subst0 (a : Term.InS φ Δ ty) + : a.subst0.get 0 (by simp) = a + := rfl + +@[simp] +theorem Term.Subst.InS.get_succ_lift (n) + (h : Ctx.Var _ (n + 1) ty) (σ : Subst.InS φ Γ Δ) + (hv : lo ≤ hi) + : (σ.lift hv).get (n + 1) h = (σ.get n h.tail).wk ⟨Nat.succ, by simp⟩ + := rfl + def Term.Subst.WfD.comp {Γ Δ Ξ : Ctx α ε} {σ : Term.Subst φ} {τ : Term.Subst φ} (hσ : σ.WfD Γ Δ) (hτ : τ.WfD Δ Ξ) : (σ.comp τ).WfD Γ Ξ := λi => (hτ i).subst hσ @@ -249,6 +308,11 @@ theorem Region.InS.coe_vsubst {Γ Δ : Ctx α ε} {σ : Term.Subst.InS φ Γ Δ} : (r.vsubst σ : Region φ) = (r : Region φ).vsubst σ := rfl +theorem Region.InS.vsubst_vsubst {Γ Δ Ξ : Ctx α ε} + {σ : Term.Subst.InS φ Γ Δ} {τ : Term.Subst.InS φ Δ Ξ} + (r : InS φ Ξ L) : (r.vsubst τ).vsubst σ = r.vsubst (σ.comp τ) + := by ext; simp [Region.vsubst_vsubst] + theorem Region.InS.vsubst_equiv {Γ Δ : Ctx α ε} {σ τ : Term.Subst.InS φ Γ Δ} (r : InS φ Δ L) (h : σ ≈ τ) : r.vsubst σ = r.vsubst τ := sorry @@ -427,17 +491,30 @@ def Region.Subst.WfD.liftn_append_cons' (V : Ty α) {J : LCtx α} (hn : n = J.le : (σ.liftn n).WfD Γ (V::(J ++ L)) (V::(J ++ K)) := hn ▸ hσ.liftn_append_cons V J -def Region.Subst.WfD.vlift (V) (hσ : σ.WfD Γ L K) : σ.vlift.WfD (V::Γ) L K +def Region.Subst.WfD.vlift (hσ : σ.WfD Γ L K) : σ.vlift.WfD (head::Γ) L K := λi => (hσ i).vwk (Ctx.Wkn.id.step.slift) -theorem Region.Subst.Wf.vlift (V) (hσ : σ.Wf Γ L K) : σ.vlift.Wf (V::Γ) L K +theorem Region.Subst.Wf.vlift (hσ : σ.Wf Γ L K) : σ.vlift.Wf (head::Γ) L K := λi => (hσ i).vwk (Ctx.Wkn.id.step.slift) -def Region.Subst.WfD.vlift₂ (V₁ V₂) (hσ : σ.WfD Γ L K) : σ.vlift.vlift.WfD (V₁::V₂::Γ) L K - := (hσ.vlift _).vlift _ +def Region.Subst.InS.vlift (σ : Region.Subst.InS φ Γ L K) : InS φ (head::Γ) L K + := ⟨Subst.vlift σ, σ.prop.vlift⟩ -def Region.Subst.WfD.vliftn₂ (V₁ V₂) (hσ : σ.WfD Γ L K) : (σ.vliftn 2).WfD (V₁::V₂::Γ) L K - := Region.Subst.vliftn_eq_iterate_vlift 2 ▸ hσ.vlift₂ _ _ +def Region.Subst.WfD.vlift₂ (hσ : σ.WfD Γ L K) : σ.vlift.vlift.WfD (left::right::Γ) L K + := hσ.vlift.vlift + +def Region.Subst.WfD.vliftn₂ (hσ : σ.WfD Γ L K) : (σ.vliftn 2).WfD (left::right::Γ) L K + := Region.Subst.vliftn_eq_iterate_vlift 2 ▸ hσ.vlift₂ + +theorem Region.Subst.Wf.vliftn₂ (hσ : σ.Wf Γ L K) : (σ.vliftn 2).Wf (left::right::Γ) L K + := let ⟨d⟩ := hσ.nonempty; (d.vliftn₂).toWf + +def Region.Subst.InS.vliftn₂ (σ : Region.Subst.InS φ Γ L K) : InS φ (left::right::Γ) L K + := ⟨Subst.vliftn 2 σ, σ.prop.vliftn₂⟩ + +theorem Region.Subst.InS.vliftn₂_eq_vlift_vlift (σ : Region.Subst.InS φ Γ L K) + : σ.vliftn₂ (left := left) (right := right) = σ.vlift.vlift + := by simp [vliftn₂, vlift, vliftn_succ] def Region.Subst.WfD.vliftn_append (Ξ : Ctx α ε) (hσ : σ.WfD Γ L K) : (σ.vliftn Ξ.length).WfD (Ξ ++ Γ) L K @@ -469,12 +546,12 @@ def LCtx.Trg.rsubst0 def Region.WfD.lsubst {Γ : Ctx α ε} {L} {σ} {r : Region φ} (hσ : σ.WfD Γ L K) : r.WfD Γ L → (r.lsubst σ).WfD Γ K | br hL ha => hL.rsubst0 hσ ha - | case he hs ht => case he (hs.lsubst (hσ.vlift _)) (ht.lsubst (hσ.vlift _)) - | let1 da dt => let1 da (dt.lsubst (hσ.vlift _)) - | let2 da dt => let2 da (dt.lsubst (hσ.vliftn₂ _ _)) + | case he hs ht => case he (hs.lsubst hσ.vlift) (ht.lsubst hσ.vlift) + | let1 da dt => let1 da (dt.lsubst hσ.vlift) + | let2 da dt => let2 da (dt.lsubst hσ.vliftn₂) | cfg n R hR hr hG => cfg n R hR (hr.lsubst (hσ.liftn_append' hR.symm)) - (λi => (hG i).lsubst ((hσ.liftn_append' hR.symm).vlift _)) + (λi => (hG i).lsubst (hσ.liftn_append' hR.symm).vlift) theorem Region.Wf.lsubst {Γ : Ctx α ε} {L} {σ} {r : Region φ} (hσ : σ.Wf Γ L K) (h : r.Wf Γ L) : (r.lsubst σ).Wf Γ K @@ -485,11 +562,11 @@ def Region.InS.lsubst {Γ : Ctx α ε} (σ : Region.Subst.InS φ Γ L K) (r : In def Region.Subst.WfD.comp {Γ : Ctx α ε} {σ : Region.Subst φ} {τ : Region.Subst φ} (hσ : σ.WfD Γ K J) (hτ : τ.WfD Γ L K) : (σ.comp τ).WfD Γ L J - := λi => (hτ i).lsubst (hσ.vlift _) + := λi => (hτ i).lsubst hσ.vlift theorem Region.Subst.Wf.comp {Γ : Ctx α ε} {σ : Region.Subst φ} {τ : Region.Subst φ} (hσ : σ.Wf Γ K J) (hτ : τ.Wf Γ L K) : (σ.comp τ).Wf Γ L J - := λi => (hτ i).lsubst (hσ.vlift _) + := λi => (hτ i).lsubst hσ.vlift end RegionSubst diff --git a/DeBruijnSSA/BinSyntax/Typing.lean b/DeBruijnSSA/BinSyntax/Typing.lean index efb5ef3..958228a 100644 --- a/DeBruijnSSA/BinSyntax/Typing.lean +++ b/DeBruijnSSA/BinSyntax/Typing.lean @@ -1149,6 +1149,18 @@ theorem Ctx.Wkn.comp {Γ Δ Ξ : Ctx α ε} {ρ σ} def Ctx.InS.comp {Γ Δ Ξ : Ctx α ε} (ρ : Ctx.InS Γ Δ) (σ : Ctx.InS Δ Ξ) : Ctx.InS Γ Ξ := ⟨(ρ : ℕ → ℕ) ∘ (σ : ℕ → ℕ), ρ.2.comp σ.2⟩ +theorem Ctx.InS.lift_comp_lift {Γ Δ Ξ : Ctx α ε} (ρ : Ctx.InS Γ Δ) (σ : Ctx.InS Δ Ξ) + {lo hi : Ty α × ε} (hρ : lo ≤ mid) (hσ : mid ≤ hi) + : (ρ.lift hρ).comp (σ.lift hσ) = (ρ.comp σ).lift (le_trans hρ hσ) + := by + cases ρ; cases σ + simp only [comp, lift, Nat.liftWk_comp] + +theorem Ctx.InS.liftn₂_comp_liftn₂ {Γ Δ Ξ : Ctx α ε} (ρ : Ctx.InS Γ Δ) (σ : Ctx.InS Δ Ξ) + (hρ : lo ≤ mid) (hσ : mid ≤ hi) (hρ' : lo' ≤ mid') (hσ' : mid' ≤ hi') + : (ρ.liftn₂ hρ hρ').comp (σ.liftn₂ hσ hσ') = (ρ.comp σ).liftn₂ (le_trans hρ hσ) (le_trans hρ' hσ') + := by simp [<-lift_lift, lift_comp_lift] + @[simp] theorem Ctx.InS.coe_comp {Γ Δ Ξ : Ctx α ε} (ρ : Ctx.InS Γ Δ) (σ : Ctx.InS Δ Ξ) : (ρ.comp σ : ℕ → ℕ) = (ρ : ℕ → ℕ) ∘ (σ : ℕ → ℕ) @@ -1411,6 +1423,43 @@ theorem Term.InS.wk_equiv {Γ Δ : Ctx α ε} {ρ ρ' : Γ.InS Δ} (d : InS φ : d.wk ρ = d.wk ρ' := sorry +@[simp] +theorem Term.InS.wk_var {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {n} (h : Δ.Var n A) + : (var (φ := φ) n h).wk ρ = var (ρ.val n) (h.wk ρ.prop) + := rfl + +@[simp] +theorem Term.InS.wk_op {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} + {df : Φ.EFn f A B e} {de : Term.InS φ Δ ⟨A, e⟩} + : (op f df de).wk ρ = op f df (de.wk ρ) + := rfl + +@[simp] +theorem Term.InS.wk_pair {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} + {dl : Term.InS φ Δ ⟨A, e⟩} {dr : Term.InS φ Δ ⟨B, e⟩} + : (pair dl dr).wk ρ = pair (dl.wk ρ) (dr.wk ρ) + := rfl + +@[simp] +theorem Term.InS.wk_inl {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {dl : Term.InS φ Δ ⟨A, e⟩} + : (inl (right := right) dl).wk ρ = inl (dl.wk ρ) + := rfl + +@[simp] +theorem Term.InS.wk_inr {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {dr : Term.InS φ Δ ⟨B, e⟩} + : (inr (left := left) dr).wk ρ = inr (dr.wk ρ) + := rfl + +@[simp] +theorem Term.InS.wk_abort {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {da : Term.InS φ Δ ⟨Ty.empty, e⟩} + : (abort (tyOut := tyOut) da).wk ρ = abort (tyOut := tyOut) (da.wk ρ) + := rfl + +@[simp] +theorem Term.InS.wk_unit {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ} {e} + : (unit (φ := φ) e).wk ρ = unit e + := rfl + /-- Reverse-weaken a term derivation, given that it is inbounds -/ def Term.WfD.wk_inv {a : Term φ} (h : Γ.EWkn Δ ρ) (d : WfD Γ (a.wk ρ) ⟨A, e⟩) (ha : a.fvi ≤ Δ.length) : WfD Δ a ⟨A, e⟩