diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean index a1f8ad5..ec62e98 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean @@ -598,11 +598,23 @@ theorem Eqv.assoc_right_nat {A B C C' : Ty α} {Γ : Ctx α ε} {L : LCtx α} le_refl, subst_liftn₂_var_zero, let2_pair, let1_beta] rw [br_zero_eq_ret, wk_res_self] apply congrArg - rw [<-let2_ret] - sorry - -- calc - -- _ = let1 (var 1 Ctx.Var.shead.step) (r.vwk0.vwk1 ;; sorry) := sorry - -- _ = _ := sorry + rw [<-let2_ret, seq_let2_wk0_pure' (a' := var 0 Ctx.Var.shead) (ha := by rfl)] + apply congrArg + induction r using Quotient.inductionOn + apply Eqv.eq_of_reg_eq + simp only [Set.mem_setOf_eq, InS.vwk_br, Term.InS.wk_pair, Term.InS.wk_var, Ctx.InS.coe_swap02, + Nat.ofNat_pos, Nat.swap0_lt, Nat.swap0_0, Nat.one_lt_ofNat, Ctx.InS.coe_wk1, Nat.liftWk_succ, + Nat.succ_eq_add_one, Nat.reduceAdd, zero_add, Nat.liftWk_zero, InS.coe_vwk, InS.coe_lsubst, + InS.coe_alpha0, InS.coe_br, Term.InS.coe_pair, Term.InS.coe_var, vwk_lsubst, InS.coe_vsubst, + Term.InS.coe_subst0, Term.Subst.InS.coe_liftn₂, Region.vsubst_lsubst] + congr + · funext k; cases k with + | zero => simp + | succ => rfl + · simp only [Region.vwk_vwk] + simp only [Region.vsubst_vsubst, <-Region.vsubst_fromWk] + congr + funext k; cases k <;> rfl theorem Eqv.triangle {X Y : Ty α} {Γ : Ctx α ε} {L : LCtx α} : assoc (φ := φ) (Γ := Γ) (L := L) (A := X) (B := Ty.unit) (C := Y) ;; X ⋊ pi_r = pi_l ⋉ Y diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean index cf0b148..37b300d 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean @@ -197,13 +197,94 @@ theorem Eqv.let2_seq {Γ : Ctx α ε} {L : LCtx α} : (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.seq_let2_wk0_vwk2 {Γ : Ctx α ε} {L : LCtx α} --- (r : Eqv φ (⟨X, ⊥⟩::Γ) (Y::L)) --- (a : Term.Eqv φ Γ ⟨A.prod B, ⊥⟩) --- (s : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (D::L)) --- : (r ;; let2 a.wk0 s.vwk2) = let2 a.wk0 --- (let1 (Term.Eqv.var 2 Ctx.Var.shead.step.step) (r.vwk1.vwk1.vwk1 ;; s.vwk2.vwk0)) := by --- sorry +theorem Eqv.seq_let1_wk0_pure {Γ : Ctx α ε} {L : LCtx α} + (a : Term.Eqv φ Γ ⟨X, ⊥⟩) + (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)) + : r ;; (let1 a.wk0 s) = let1 a.wk0 (r.vwk1 ;; s.vswap01).vswap01 := by + simp only [seq_def, let1_beta] + induction a using Quotient.inductionOn + induction r using Quotient.inductionOn + induction s using Quotient.inductionOn + apply Eqv.eq_of_reg_eq + simp only [Set.mem_setOf_eq, InS.coe_lsubst, InS.coe_alpha0, InS.coe_vwk, Ctx.InS.coe_wk1, + InS.coe_vsubst, Term.InS.coe_subst0, Term.InS.coe_wk, Ctx.InS.coe_wk0, Ctx.InS.coe_swap01, + vwk_lsubst, Region.vsubst_lsubst] + congr + · funext k; cases k with + | zero => + simp only [alpha, Function.update_same, Region.vwk_vwk, Function.comp_apply] + simp only [<-Region.vsubst_fromWk, Region.vsubst_vsubst] + congr + funext k; cases k using Nat.cases2 with + | zero => simp only [Term.Subst.comp, Term.subst0_zero, Term.subst_fromWk, Term.wk_wk, + Nat.liftWk_succ_comp_succ, Term.subst, Function.comp_apply, Nat.swap0_0, Nat.liftWk_succ, + Nat.succ_eq_add_one, zero_add, Nat.reduceAdd, zero_lt_one, Nat.swap0_lt, + Term.Subst.lift_succ]; rfl + | _ => rfl + | succ => rfl + · rw [Region.vwk_vwk, <-Region.vsubst_fromWk, Region.vsubst_vsubst, Region.vsubst_id'] + funext k; cases k <;> rfl + +-- theorem Eqv.lsubst_let2_alpha0 {Γ : Ctx α ε} {L : LCtx α} +-- (p : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩) +-- (r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (C::L)) +-- : lsubst (let2 p.wk0.wk0 s).alpha0 r +-- = let2 p.wk0 (lsubst (alpha0 s.vswap02.vswap02) r.vwk0.vwk0) +-- := by induction r using Eqv.arrow_induction with +-- | br ℓ a hℓ => +-- cases ℓ with +-- | zero => +-- induction p using Quotient.inductionOn +-- induction s using Quotient.inductionOn +-- induction a using Quotient.inductionOn +-- apply Eqv.eq_of_reg_eq +-- simp only [Set.mem_setOf_eq, InS.lsubst_br, List.length_cons, List.get_eq_getElem, +-- InS.coe_vsubst, Term.InS.coe_subst0, InS.coe_vwk_id, Subst.InS.coe_get, InS.coe_alpha0, +-- InS.coe_let2, Term.InS.coe_wk, Ctx.InS.coe_wk0, InS.vwk_br, InS.coe_vwk, Ctx.InS.coe_swap02] +-- simp only [Region.vsubst, Term.wk_succ_subst_subst0, alpha, ← vsubst_fromWk, +-- Region.vsubst_vsubst, Function.update_same, let2.injEq, true_and] +-- congr +-- funext k; cases k using Nat.cases3 with +-- | two => simp only [Term.Subst.liftn, lt_self_iff_false, ↓reduceIte, le_refl, +-- tsub_eq_zero_of_le, Term.subst0_zero, Term.Subst.comp, Term.subst, Term.wk_wk, +-- Nat.one_lt_ofNat, Nat.swap0_lt, Nat.ofNat_pos]; rfl +-- | _ => rfl +-- | succ ℓ => simp [get_alpha0, let2_br, Term.Eqv.nil, Term.Eqv.let2_wk0_wk0_pure] +-- | let1 a r => sorry +-- | let2 a r => sorry +-- | case a l r => sorry +-- | cfg R β G => sorry + +theorem Eqv.seq_let2_wk0_pure {Γ : Ctx α ε} {L : LCtx α} + {a : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩} + {r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)} {s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)} + : r ;; (let2 a.wk0 s) = let2 a.wk0 (r.vwk1.vwk1 ;; s.vswap02.vswap02).vswap02 := by + sorry + -- rw [seq, vwk1_let2, Term.Eqv.wk0_wk1, lsubst_let2_alpha0] + -- congr + -- rw [seq] + -- induction r using Quotient.inductionOn + -- induction s using Quotient.inductionOn + -- induction a using Quotient.inductionOn + -- apply Eqv.eq_of_reg_eq + -- simp only [Set.mem_setOf_eq, InS.coe_lsubst, InS.coe_alpha0, InS.coe_vwk, Ctx.InS.coe_swap02, + -- Ctx.InS.coe_wk3, Ctx.InS.coe_wk0, Ctx.InS.coe_wk1, vwk_lsubst] + -- congr 1 + -- · funext k; cases k with + -- | zero => + -- simp only [alpha, Region.vwk_vwk, Function.update_same, Function.comp_apply] + -- congr + -- funext k; cases k using Nat.cases3 <;> rfl + -- | succ => rfl + -- · simp only [Region.vwk_vwk]; congr; funext k; cases k <;> rfl + +theorem Eqv.seq_let2_wk0_pure' {Γ : Ctx α ε} {L : LCtx α} + {a : Term.Eqv φ (_::Γ) ⟨X.prod Y, ⊥⟩} {a' : Term.Eqv φ Γ ⟨X.prod Y, ⊥⟩} + {r : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)} {s : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::⟨B, ⊥⟩::Γ) (C::L)} + (ha : a = a'.wk0) + : r ;; (let2 a s) = let2 a'.wk0 (r.vwk1.vwk1 ;; s.vswap02.vswap02).vswap02 := by + cases ha; rw [seq_let2_wk0_pure] + theorem Eqv.case_seq {Γ : Ctx α ε} {L : LCtx α} (a : Term.Eqv φ (⟨A, ⊥⟩::Γ) ⟨X.coprod Y, e⟩) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean index 5570317..dc734be 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean @@ -721,6 +721,18 @@ theorem Eqv.vwk1_shf {Γ : Ctx α ε} {L : LCtx α} {R : LCtx α} {Y : Ty α} : d.shf.vwk1 (inserted := inserted) = (d.vwk1).shf := by induction d using Quotient.inductionOn; rfl +@[simp] +theorem Eqv.vwk_br {Γ Δ : Ctx α ε} {L : LCtx α} {ρ : Γ.InS Δ} + {ℓ} {a : Term.Eqv φ Δ ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A} + : Eqv.vwk ρ (Eqv.br ℓ a hℓ) = Eqv.br ℓ (a.wk ρ) hℓ := by + induction a using Quotient.inductionOn; rfl + +@[simp] +theorem Eqv.vwk0_br {Γ : Ctx α ε} {L : LCtx α} + {ℓ} {a : Term.Eqv φ Γ ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A} + : Eqv.vwk0 (Eqv.br ℓ a hℓ) = Eqv.br ℓ (a.wk0 (head := head)) hℓ := by + induction a using Quotient.inductionOn; rfl + @[simp] theorem Eqv.vwk1_br {Γ : Ctx α ε} {L : LCtx α} {ℓ} {a : Term.Eqv φ (head::Γ) ⟨A, ⊥⟩} {hℓ : L.Trg ℓ A} @@ -775,6 +787,21 @@ theorem Eqv.vwk1_vwk2 {Γ : Ctx α ε} {L : LCtx α} congr 1 ext k; cases k <;> rfl +def Eqv.vwk3 {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (left::middle::right::Γ) L) + : Eqv φ (left::middle::right::inserted::Γ) L := Eqv.vwk Ctx.InS.wk3 r + +@[simp] +theorem Eqv.vwk3_quot {Γ : Ctx α ε} {L : LCtx α} {r : InS φ (left::middle::right::Γ) L} + : Eqv.vwk3 (inserted := inserted) ⟦r⟧ = ⟦r.vwk3⟧ := rfl + +theorem Eqv.vwk1_let2 {L : LCtx α} + {a : Term.Eqv φ (⟨X, ⊥⟩::Γ) ⟨Ty.prod A B, e⟩} {r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::⟨X, ⊥⟩::Γ) L} + : vwk1 (inserted := inserted) (let2 a r) + = let2 a.wk1 r.vwk3 := by + induction a using Quotient.inductionOn; induction r using Quotient.inductionOn; + apply Eqv.eq_of_reg_eq + simp [Nat.liftnWk_succ] + def Eqv.vswap01 {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (left::right::Γ) L) : Eqv φ (right::left::Γ) L := Eqv.vwk Ctx.InS.swap01 r @@ -793,6 +820,15 @@ theorem Eqv.vswap02_quot {Γ : Ctx α ε} {L : LCtx α} {r : InS φ (left::mid::right::Γ) L} : Eqv.vswap02 ⟦r⟧ = ⟦r.vswap02⟧ := rfl +def Eqv.vswap03 + {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ (first::second::third::fourth::Γ) L) + : Eqv φ (second::third::fourth::first::Γ) L := Eqv.vwk Ctx.InS.swap03 r + +@[simp] +theorem Eqv.vswap03_quot + {Γ : Ctx α ε} {L : LCtx α} {r : InS φ (first::second::third::fourth::Γ) L} + : Eqv.vswap03 ⟦r⟧ = ⟦r.vswap03⟧ := rfl + def Eqv.lwk0 {Γ : Ctx α ε} {L : LCtx α} (r : Eqv φ Γ L) : Eqv φ Γ (head::L) := Eqv.lwk LCtx.InS.wk0 r diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Seq.lean index 7f947e5..b3471d4 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Seq.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Seq.lean @@ -17,6 +17,10 @@ def Eqv.nil {A : Ty α} {Γ : Ctx α ε} : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A, e⟩ theorem Eqv.wk0_nil {A : Ty α} {Γ : Ctx α ε} : (nil : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A, e⟩).wk0 (head := ⟨head, ⊥⟩) = (var 1 (by simp)) := rfl +@[simp] +theorem Eqv.wk_id_nil {A : Ty α} {Γ Δ : Ctx α ε} {hΓ : Ctx.Wkn (⟨A, ⊥⟩::Γ) ((A, ⊥)::Δ) id} + : (nil : Eqv φ (⟨A, ⊥⟩::Δ) ⟨A, e⟩).wk_id hΓ = nil := rfl + @[simp] theorem Eqv.wk1_nil {A : Ty α} {Γ : Ctx α ε} : (nil (φ := φ) (A := A) (Γ := Γ) (e := e)).wk1 (inserted := inserted) = nil diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean index a9e96e6..7033260 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean @@ -1643,6 +1643,9 @@ theorem Eqv.Pure.let2_wk0_wk0 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A.prod B, e⟩} apply Pure.wk0 exact ⟨a.let2 (var 0 (by simp)), by simp⟩ +theorem Eqv.let2_wk0_wk0_pure {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A.prod B, ⊥⟩} {b : Eqv φ Γ ⟨C, ⊥⟩} + : let2 a b.wk0.wk0 = b := Eqv.Pure.let2_wk0_wk0 (by simp) + theorem Eqv.Pure.let1_let2_of_right {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B.prod C, e⟩} {c : Eqv φ (⟨C, ⊥⟩::⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨D, e⟩} (hb : b.Pure) : let1 a (let2 b.wk0 c) = let2 b (let1 a.wk0.wk0 c.swap02.swap02) := by diff --git a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean index 007d805..a796afa 100644 --- a/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean +++ b/DeBruijnSSA/BinSyntax/Syntax/Definitions.lean @@ -851,6 +851,8 @@ def Region.vswap01 : Region φ → Region φ := vwk (Nat.swap0 1) def Region.vswap02 : Region φ → Region φ := vwk (Nat.swap0 2) +def Region.vswap03 : Region φ → Region φ := vwk (Nat.swap0 3) + theorem Region.vwk_vwk1 (r : Region φ) : r.vwk1.vwk ρ = r.vwk (ρ ∘ Nat.liftWk Nat.succ) := by simp only [vwk1, vwk_vwk, <-Nat.liftWk_comp] diff --git a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean index c9998af..12650fd 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean @@ -259,9 +259,17 @@ theorem InS.coe_swap02 {first second third : Ty α × ε} {Γ : Ctx α ε} : (InS.swap02 (Γ := Γ) (first := first) (second := second) (third := third) : ℕ → ℕ) = Nat.swap0 2 := rfl --- def InS.swap03 {first second third fourth : Ty α × ε} {Γ : Ctx α ε} --- : InS (first::second::third::fourth::Γ) (fourth::first::second::third::Γ) --- := ⟨Nat.swap0 3, λi hi => sorry⟩ +theorem Wkn.swap03 {first second third fourth : Ty α × ε} {Γ : Ctx α ε} + : Wkn (first::second::third::fourth::Γ) (fourth::first::second::third::Γ) (Nat.swap0 3) + | 0, _ => by simp + | 1, _ => by simp + | 2, _ => by simp + | 3, _ => by simp + | n + 4, hn => ⟨hn, by simp⟩ + +def InS.swap03 {first second third fourth : Ty α × ε} {Γ : Ctx α ε} + : InS (first::second::third::fourth::Γ) (fourth::first::second::third::Γ) + := ⟨Nat.swap0 3, Wkn.swap03⟩ def Nat.swap20 : ℕ → ℕ | 0 => 2 @@ -339,6 +347,27 @@ theorem InS.coe_wk2 {left right inserted} {Γ : Ctx α ε} = Nat.liftnWk 2 Nat.succ := rfl +theorem Wkn.wk3 {left middle right inserted} {Γ : Ctx α ε} + : Wkn (left::middle::right::inserted::Γ) (left::middle::right::Γ) (Nat.liftnWk 3 Nat.succ) + := by intro i hi; cases i using Nat.cases3 with + | rest => + simp only [Nat.liftnWk, add_lt_iff_neg_right, not_lt_zero', ↓reduceIte, + add_tsub_cancel_right, Nat.succ_eq_add_one, List.length_cons, List.get_eq_getElem, + List.getElem_cons_succ, Var.step_iff]; + simp only [List.length_cons, add_lt_add_iff_right] at hi + exact ⟨hi, by simp⟩ + | _ => simp [Nat.liftnWk] + +def InS.wk3 {left middle right inserted} {Γ : Ctx α ε} + : InS (left::middle::right::inserted::Γ) (left::middle::right::Γ) + := ⟨Nat.liftnWk 3 Nat.succ, Wkn.wk3⟩ + +@[simp] +theorem InS.coe_wk3 {left middle right inserted} {Γ : Ctx α ε} + : (InS.wk3 (Γ := Γ) (left := left) (middle := middle) (right := right) (inserted := inserted) : ℕ → ℕ) + = Nat.liftnWk 3 Nat.succ + := rfl + @[simp] theorem InS.coe_liftn₂ {V₁ V₁' V₂ V₂' : Ty α × ε} (hV₁ : V₁ ≤ V₁') (hV₂ : V₂ ≤ V₂') (ρ : InS Γ Δ) : (InS.liftn₂ hV₁ hV₂ ρ : ℕ → ℕ) = Nat.liftnWk 2 ρ diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean b/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean index 1e5a2d0..70be2a7 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean @@ -625,6 +625,14 @@ theorem InS.vwk1_let1 {Γ : Ctx α ε} {L : LCtx α} {A e} : (t.let1 a).vwk1 (inserted := inserted) = let1 a.wk1 t.vwk2 := by ext; simp [Region.vwk1, Nat.liftnWk_two, Region.vwk2, Term.wk1] +def InS.vwk3 {Γ : Ctx α ε} {L} (r : InS φ (left::middle::right::Γ) L) + : InS φ (left::middle::right::inserted::Γ) L + := r.vwk Ctx.InS.wk3 + +@[simp] +theorem InS.coe_vwk3 {Γ : Ctx α ε} {L} {r : InS φ (left::middle::right::Γ) L} + : (r.vwk3 (inserted := inserted) : Region φ) = (r : Region φ).vwk3 := rfl + def InS.vswap01 {Γ : Ctx α ε} {L} (r : InS φ (left::right::Γ) L) : InS φ (right::left::Γ) L := r.vwk Ctx.InS.swap01 @@ -640,6 +648,14 @@ def InS.vswap02 {Γ : Ctx α ε} {L} (r : InS φ (left::mid::right::Γ) L) theorem InS.coe_vswap02 {Γ : Ctx α ε} {L} {r : InS φ (left::mid::right::Γ) L} : (r.vswap02 : Region φ) = r.vswap02 := rfl +def InS.vswap03 {Γ : Ctx α ε} {L} (r : InS φ (first::second::third::fourth::Γ) L) + : InS φ (second::third::fourth::first::Γ) L + := r.vwk Ctx.InS.swap03 + +@[simp] +theorem InS.coe_vswap03 {Γ : Ctx α ε} {L} {r : InS φ (first::second::third::fourth::Γ) L} + : (r.vswap03 : Region φ) = r.vswap03 := rfl + def InS.lwk {Γ : Ctx α ε} (ρ : L.InS K) (r : InS φ Γ L) : InS φ Γ K := ⟨(r : Region φ).lwk ρ, r.2.lwk ρ.prop⟩