From 684c02f95be1419f1aeb7dbd7e1b357f18a8f66d Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Wed, 10 Jul 2024 19:40:04 +0100 Subject: [PATCH] Work on associator lore --- .../Rewrite/Region/Compose/Product.lean | 0 .../BinSyntax/Rewrite/Region/Compose/Seq.lean | 0 .../BinSyntax/Rewrite/Region/Compose/Sum.lean | 0 .../BinSyntax/Rewrite/Term/Compose.lean | 100 +++++++++++++-- .../Rewrite/Term/Compose/Product.lean | 0 .../BinSyntax/Rewrite/Term/Compose/Seq.lean | 0 .../BinSyntax/Rewrite/Term/Compose/Sum.lean | 0 DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean | 118 ++++++++++++++++++ .../BinSyntax/Rewrite/Term/Induction.lean | 12 ++ DeBruijnSSA/BinSyntax/Typing/Ctx.lean | 18 +++ DeBruijnSSA/BinSyntax/Typing/Term/Subst.lean | 8 ++ 11 files changed, 248 insertions(+), 8 deletions(-) create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Seq.lean create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Sum.lean create mode 100644 DeBruijnSSA/BinSyntax/Rewrite/Term/Induction.lean diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Product.lean new file mode 100644 index 0000000..e69de29 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Seq.lean new file mode 100644 index 0000000..e69de29 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Sum.lean new file mode 100644 index 0000000..e69de29 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose.lean index b180a2b..4eb0bd1 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose.lean @@ -25,11 +25,20 @@ theorem Eqv.wk2_nil {A : Ty α} {Γ : Ctx α ε} : (nil (φ := φ) (A := A) (Γ := head::Γ) (e := e)).wk2 (inserted := inserted) = nil := rfl +@[simp] +theorem Eqv.subst_lift_nil {A : Ty α} {Γ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ} {h} + : (nil : Eqv φ (⟨A, ⊥⟩::Δ) ⟨A, e⟩).subst (σ.lift h) = nil := by + induction σ using Quotient.inductionOn; rfl + @[simp] theorem Eqv.wk_eff_nil {A : Ty α} {Γ : Ctx α ε} (h : lo ≤ hi) : (nil (φ := φ) (A := A) (Γ := Γ)).wk_eff h = nil := rfl +theorem Eqv.nil_pure {A : Ty α} {Γ : Ctx α ε} + : (nil : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A, e⟩) = nil.wk_eff bot_le + := rfl + @[simp] theorem Eqv.subst0_nil_wk1 {Γ : Ctx α ε} (a : Eqv φ (⟨A, ⊥⟩::Γ) V) : a.wk1.subst nil.subst0 = a @@ -41,8 +50,8 @@ theorem Eqv.nil_subst0 {Γ : Ctx α ε} (a : Eqv φ Γ ⟨A, ⊥⟩) := by induction a using Quotient.inductionOn; rfl @[simp] -theorem Eqv.nil_pure {A : Ty α} {Γ : Ctx α ε} : (nil (φ := φ) (A := A) (Γ := Γ) (e := e)).Pure - := ⟨nil, rfl⟩ +theorem Eqv.Pure.nil {A : Ty α} {Γ : Ctx α ε} : (nil (φ := φ) (A := A) (Γ := Γ) (e := e)).Pure + := ⟨Eqv.nil, rfl⟩ def Eqv.seq {A B C : Ty α} {Γ : Ctx α ε} (a : Eqv φ ((A, ⊥)::Γ) (B, e)) (b : Eqv φ ((B, ⊥)::Γ) (C, e)) @@ -422,6 +431,12 @@ theorem Eqv.swap_ltimes {A B B' : Ty α} {Γ : Ctx α ε} (l : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩) : swap ;;' ltimes l A = rtimes A l ;;' swap := by rw [<-seq_swap_inj, swap_ltimes_swap, <-seq_assoc, swap_swap, seq_nil] +theorem Eqv.rtimes_swap {A B B' : Ty α} {Γ : Ctx α ε} + (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩) : rtimes A r ;;' swap = swap ;;' ltimes r A := by rw [swap_ltimes] + +theorem Eqv.ltimes_swap {A B B' : Ty α} {Γ : Ctx α ε} + (l : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩) : ltimes l A ;;' swap = swap ;;' rtimes A l := by rw [swap_rtimes] + theorem Eqv.rtimes_nil {A B : Ty α} {Γ : Ctx α ε} : rtimes (φ := φ) (Γ := Γ) (A := A) (B := B) (B' := B) (e := e) nil = nil := tensor_nil_nil @@ -454,13 +469,36 @@ theorem Eqv.ltimes_rtimes {A A' B B' : Ty α} {Γ : Ctx α ε} theorem Eqv.Pure.left_central {A A' B B' : Ty α} {Γ : Ctx α ε} {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A', e⟩} (hl : l.Pure) (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩) : ltimes l B ;;' rtimes A' r = rtimes A r ;;' ltimes l B':= by - rw [<-swap_rtimes_swap (r := l) (A := B'), seq_assoc] - sorry + rw [ltimes_rtimes, seq_ltimes, tensor, rtimes, tensor, let2_let2] + apply congrArg + rw [let2_pair] + simp only [wk1_nil, wk0_nil, wk2_pair, wk2_nil, let1_beta_var1, subst_let1, subst0_wk0, + subst_pair, subst_lift_nil] + apply Eq.symm + rw [pair_bind_left] + apply Eq.symm + rw [pair_bind_swap_left] + -- TODO: this REALLY needs to be factored out... + congr + induction l using Quotient.inductionOn + apply eq_of_term_eq + simp only [Set.mem_setOf_eq, InS.coe_wk, Ctx.InS.coe_wk0, Ctx.InS.coe_wk1, ← subst_fromWk, + Term.subst_subst, InS.coe_subst, Subst.coe_lift, InS.coe_subst0, InS.coe_var, Ctx.InS.coe_wk2] + congr + funext k + cases k <;> rfl + sorry -- TODO: obviously, if something is pure so are its weakenings theorem Eqv.Pure.right_central {A A' B B' : Ty α} {Γ : Ctx α ε} (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A', e⟩) {r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩} (hr : r.Pure) : ltimes l B ;;' rtimes A' r = rtimes A r ;;' ltimes l B' - := by sorry + := by + apply Eq.symm + rw [ + <-swap_ltimes_swap, <-seq_assoc, swap_ltimes (l := l), seq_assoc, <-seq_assoc (a := swap), + hr.left_central, seq_assoc, swap_rtimes, <-seq_assoc, ltimes_swap (l := r), seq_assoc, + <-seq_assoc (c := swap), swap_swap, seq_nil + ] theorem Eqv.tensor_seq_of_comm {A₀ A₁ A₂ B₀ B₁ B₂ : Ty α} {Γ : Ctx α ε} {l : Eqv φ (⟨A₀, ⊥⟩::Γ) ⟨A₁, e⟩} {r : Eqv φ (⟨B₀, ⊥⟩::Γ) ⟨B₁, e⟩} @@ -473,8 +511,6 @@ theorem Eqv.tensor_seq_of_comm {A₀ A₁ A₂ B₀ B₁ B₂ : Ty α} {Γ : Ctx -- TODO: tensor_seq (pure only) --- TODO: swap - def Eqv.split {A : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨A, ⊥⟩::Γ) ⟨A.prod A, e⟩ := let1 nil (pair nil nil) @@ -492,7 +528,55 @@ def Eqv.assoc_inv {A B C : Ty α} {Γ : Ctx α ε} let2 (var (V := (B.prod C, e)) 0 (by simp)) $ pair (pair (var 3 (by simp)) (var 1 (by simp))) (var 0 (by simp)) --- TODO: assoc_assoc_inv, assoc_inv_assoc +theorem Eqv.seq_prod_assoc {A B C : Ty α} {Γ : Ctx α ε} + (r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨(A.prod B).prod C, e⟩) + : r ;;' assoc = (let2 r $ let2 (var (V := (A.prod B, e)) 1 (by simp)) + $ pair (var 1 (by simp)) (pair (var 0 (by simp)) (var 2 (by simp)))) + := sorry + +theorem Eqv.seq_assoc_inv {A B C : Ty α} {Γ : Ctx α ε} + (r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A.prod (B.prod C), e⟩) + : r ;;' assoc_inv = (let2 r $ let2 (var (V := (B.prod C, e)) 0 (by simp)) + $ pair (pair (var 3 (by simp)) (var 1 (by simp))) (var 0 (by simp))) + := sorry + +@[simp] +theorem Eqv.wk_eff_assoc {A B C : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi} + : (assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := lo)).wk_eff h = assoc := rfl + +@[simp] +theorem Eqv.wk_eff_assoc_inv {A B C : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi} + : (assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := lo)).wk_eff h = assoc_inv := rfl + +theorem Eqv.assoc_pure {A B C : Ty α} {Γ : Ctx α ε} + : assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) = assoc.wk_eff bot_le + := rfl + +theorem Eqv.assoc_inv_pure {A B C : Ty α} {Γ : Ctx α ε} + : assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) = assoc_inv.wk_eff bot_le + := rfl + +@[simp] +theorem Eqv.Pure.assoc {A B C : Ty α} {Γ : Ctx α ε} + : (assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)).Pure := ⟨Eqv.assoc, rfl⟩ + +@[simp] +theorem Eqv.Pure.assoc_inv {A B C : Ty α} {Γ : Ctx α ε} + : (assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)).Pure := ⟨Eqv.assoc_inv, rfl⟩ + +theorem Eqv.assoc_assoc_inv_pure {A B C : Ty α} {Γ : Ctx α ε} + : assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := ⊥) ;;' assoc_inv = nil := sorry + +theorem Eqv.assoc_inv_assoc_pure {A B C : Ty α} {Γ : Ctx α ε} + : assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := ⊥) ;;' assoc = nil := sorry + +theorem Eqv.assoc_assoc_inv {A B C : Ty α} {Γ : Ctx α ε} + : assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) ;;' assoc_inv = nil := by + rw [assoc_pure, assoc_inv_pure, <-wk_eff_seq, assoc_assoc_inv_pure]; rfl + +theorem Eqv.assoc_inv_assoc {A B C : Ty α} {Γ : Ctx α ε} + : assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) ;;' assoc = nil := by + rw [assoc_pure, assoc_inv_pure, <-wk_eff_seq, assoc_inv_assoc_pure]; rfl def Eqv.coprod {A B C : Ty α} {Γ : Ctx α ε} (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩) (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩) diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean new file mode 100644 index 0000000..e69de29 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Seq.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Seq.lean new file mode 100644 index 0000000..e69de29 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Sum.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Sum.lean new file mode 100644 index 0000000..e69de29 diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean index 0aa9649..91a6a38 100644 --- a/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean @@ -24,6 +24,9 @@ theorem Eqv.sound {a a' : InS φ Γ V} (h : a ≈ a') : InS.q a = InS.q a' := Qu theorem Eqv.eq {a a' : InS φ Γ V} : a.q = a'.q ↔ a ≈ a' := Quotient.eq +theorem Eqv.eq_of_term_eq {a a' : InS φ Γ V} (h : (a : Term φ) = (a' : Term φ)) + : a.q = a'.q := sorry + def Eqv.var (n : ℕ) (hn : Γ.Var n V) : Eqv φ Γ V := ⟦InS.var n hn⟧ def Eqv.op (f : φ) (hf : Φ.EFn f A B e) (a : Eqv φ Γ ⟨A, e⟩) : Eqv φ Γ ⟨B, e⟩ @@ -474,6 +477,8 @@ theorem Eqv.subst_var_wk0 {σ : Subst.Eqv φ Γ Δ} {n : ℕ} induction σ using Quotient.inductionOn rfl +def Subst.Eqv.fromWk (ρ : Γ.InS Δ) : Eqv φ Γ Δ := ⟦Subst.InS.fromWk ρ⟧ + -- TODO: subst_var lore @[simp] @@ -897,6 +902,119 @@ theorem Eqv.initial (hΓ : Γ.IsInitial) {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ induction a using Quotient.inductionOn; induction b using Quotient.inductionOn; apply sound; apply InS.initial hΓ +-- TODO: eqv induction... + +theorem Eqv.let1_wk_eff_let1 {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ Γ ⟨B, e⟩} {c : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩} + : let1 (a.wk_eff bot_le) (let1 b.wk0 c) + = let1 b (let1 (a.wk_eff bot_le).wk0 (c.wk Ctx.InS.swap01)) := by + rw [let1_beta, wk0_wk_eff, let1_beta, subst_let1, subst0_wk0] + apply congrArg + induction c using Quotient.inductionOn + induction a using Quotient.inductionOn + apply Eqv.eq_of_term_eq + simp only [Set.mem_setOf_eq, InS.coe_subst, Subst.coe_lift, InS.coe_subst0, InS.coe_wk0, + InS.coe_wk, Ctx.InS.coe_swap01, ← subst_fromWk, Term.subst_subst] + congr + funext k + cases k with + | zero => rfl + | succ k => cases k with + | zero => simp [Term.Subst.comp, Term.subst_fromWk] + | succ k => rfl + +theorem Eqv.Pure.let1_let1 {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} {c : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩} + : a.Pure → let1 a (let1 b.wk0 c) = let1 b (let1 a.wk0 (c.wk Ctx.InS.swap01)) + | ⟨a, ha⟩ => by cases ha; rw [let1_wk_eff_let1] + +theorem Eqv.let1_let1_comm {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ Γ ⟨B, ⊥⟩} {c : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, ⊥⟩} + : let1 a (let1 b.wk0 c) = let1 b (let1 a.wk0 (c.wk Ctx.InS.swap01)) + := Eqv.Pure.let1_let1 ⟨a, by simp⟩ + +theorem Eqv.swap01_let2_eta {Γ : Ctx α ε} {A B : Ty α} {e} + : (pair (var 1 (by simp)) (var 0 (by simp)) : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) (A.prod B, e) + ).wk Ctx.InS.swap01 = pair (var 0 (by simp)) (var 1 (by simp)) := rfl + +theorem Eqv.pair_bind_swap_left + {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} + (ha : a.Pure) + : pair a b = (let1 b $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp))) := by + rw [pair_bind, ha.let1_let1, swap01_let2_eta] + +theorem Eqv.pair_bind_swap_right + {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} + (hb : b.Pure) + : pair a b = (let1 b $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp))) := by + rw [pair_bind, hb.let1_let1]; rfl + +theorem Eqv.pair_bind_swap_wk_eff_left {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ Γ ⟨B, e⟩} + : pair (a.wk_eff bot_le) b + = (let1 b $ let1 (a.wk_eff bot_le).wk0 $ pair (var 0 (by simp)) (var 1 (by simp))) + := pair_bind_swap_left ⟨a, rfl⟩ + +theorem Eqv.pair_bind_swap_wk_eff_right {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, ⊥⟩} + : pair a (b.wk_eff bot_le) + = (let1 (b.wk_eff bot_le) $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp))) + := pair_bind_swap_right ⟨b, rfl⟩ + +theorem Eqv.pair_bind_swap + {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, ⊥⟩} {b : Eqv φ Γ ⟨B, ⊥⟩} + : pair a b = (let1 b $ let1 a.wk0 $ pair (var 0 (by simp)) (var 1 (by simp))) + := pair_bind_swap_left ⟨a, by simp⟩ + +def Eqv.reassoc {A B C : Ty α} {Γ : Ctx α ε} + (r : Eqv φ Γ ⟨(A.prod B).prod C, e⟩) + : Eqv φ Γ ⟨A.prod (B.prod C), e⟩ + := let2 r + $ let2 (var (V := (A.prod B, e)) 1 (by simp)) + $ pair (var 1 (by simp)) (pair (var 0 (by simp)) (var 2 (by simp))) + +def Eqv.reassoc_inv {A B C : Ty α} {Γ : Ctx α ε} + (r : Eqv φ Γ ⟨A.prod (B.prod C), e⟩) + : Eqv φ Γ ⟨(A.prod B).prod C, e⟩ + := let2 r + $ let2 (var (V := (B.prod C, e)) 0 (by simp)) + $ pair (pair (var 3 (by simp)) (var 1 (by simp))) (var 0 (by simp)) + +theorem Eqv.reassoc_beta {A B C : Ty α} {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} {c : Eqv φ Γ ⟨C, e⟩} + : reassoc (pair (pair a b) c) = pair a (pair b c) := by sorry + +theorem Eqv.reassoc_inv_beta {A B C : Ty α} {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ ⟨B, e⟩} {c : Eqv φ Γ ⟨C, e⟩} + : reassoc_inv (pair a (pair b c)) = pair (pair a b) c := by sorry + +theorem Eqv.let1_reassoc {A B C : Ty α} {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨X, e⟩} + {r : Eqv φ ((X, ⊥)::Γ) ⟨(A.prod B).prod C, e⟩} + : let1 a (reassoc r) = reassoc (let1 a r) := sorry + +theorem Eqv.let2_reassoc {A B C : Ty α} {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨X.prod Y, e⟩} + {r : Eqv φ ((Y, ⊥)::(X, ⊥)::Γ) ⟨(A.prod B).prod C, e⟩} + : let2 a (reassoc r) = reassoc (let2 a r) := sorry + +theorem Eqv.case_reassoc {A B C : Ty α} {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨Ty.coprod X Y, e⟩} + {l : Eqv φ (⟨X, ⊥⟩::Γ) ⟨(A.prod B).prod C, e⟩} + {r : Eqv φ (⟨Y, ⊥⟩::Γ) ⟨(A.prod B).prod C, e⟩} + : case a (reassoc l) (reassoc r) = reassoc (case a l r) := by + sorry + +theorem Eqv.let1_reassoc_inv {A B C : Ty α} {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨X, e⟩} + {r : Eqv φ ((X, ⊥)::Γ) ⟨A.prod (B.prod C), e⟩} + : let1 a (reassoc_inv r) = reassoc_inv (let1 a r) := sorry + +theorem Eqv.let2_reassoc_inv {A B C : Ty α} {Γ : Ctx α ε} + {a : Eqv φ Γ ⟨X.prod Y, e⟩} + {r : Eqv φ ((Y, ⊥)::(X, ⊥)::Γ) ⟨A.prod (B.prod C), e⟩} + : let2 a (reassoc_inv r) = reassoc_inv (let2 a r) := sorry + end Basic end Term diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Term/Induction.lean b/DeBruijnSSA/BinSyntax/Rewrite/Term/Induction.lean new file mode 100644 index 0000000..d159590 --- /dev/null +++ b/DeBruijnSSA/BinSyntax/Rewrite/Term/Induction.lean @@ -0,0 +1,12 @@ +import DeBruijnSSA.BinSyntax.Rewrite.Term.Setoid + +import Discretion.Utils.Quotient + +namespace BinSyntax + +variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε] + +namespace Term + + +-- ... diff --git a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean index 9b87d17..d685e78 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Ctx.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Ctx.lean @@ -269,6 +269,15 @@ theorem Wkn.swap01 {left right : Ty α × ε} {Γ : Ctx α ε} | 1, _ => by simp | n + 2, hn => ⟨hn, by simp⟩ +def InS.swap01 {left right : Ty α × ε} {Γ : Ctx α ε} + : InS (left::right::Γ) (right::left::Γ) + := ⟨Nat.swap0 1, Wkn.swap01⟩ + +@[simp] +theorem InS.coe_swap01 {left right : Ty α × ε} {Γ : Ctx α ε} + : (InS.swap01 (Γ := Γ) (left := left) (right := right) : ℕ → ℕ) = Nat.swap0 1 + := rfl + theorem Wkn.swap02 {first second third : Ty α × ε} {Γ : Ctx α ε} : Wkn (first::second::third::Γ) (third::first::second::Γ) (Nat.swap0 2) | 0, _ => by simp @@ -276,6 +285,15 @@ theorem Wkn.swap02 {first second third : Ty α × ε} {Γ : Ctx α ε} | 2, _ => by simp | n + 3, hn => ⟨hn, by simp⟩ +def InS.swap02 {first second third : Ty α × ε} {Γ : Ctx α ε} + : InS (first::second::third::Γ) (third::first::second::Γ) + := ⟨Nat.swap0 2, Wkn.swap02⟩ + +@[simp] +theorem InS.coe_swap02 {first second third : Ty α × ε} {Γ : Ctx α ε} + : (InS.swap02 (Γ := Γ) (first := first) (second := second) (third := third) : ℕ → ℕ) = Nat.swap0 2 + := rfl + @[simp] theorem Wkn.add2 {first second} {Γ : Ctx α ε} : Wkn (first::second::Γ) Γ (· + 2) diff --git a/DeBruijnSSA/BinSyntax/Typing/Term/Subst.lean b/DeBruijnSSA/BinSyntax/Typing/Term/Subst.lean index 270a973..d919cdf 100644 --- a/DeBruijnSSA/BinSyntax/Typing/Term/Subst.lean +++ b/DeBruijnSSA/BinSyntax/Typing/Term/Subst.lean @@ -276,3 +276,11 @@ theorem InS.subst0_var0_wk1 {Γ : Ctx α ε} theorem InS.subst0_wk0 {Γ : Ctx α ε} (a : InS φ Γ V) (b : InS φ Γ V') : a.wk0.subst b.subst0 = a := by ext; simp + +def Subst.InS.fromWk {Γ Δ : Ctx α ε} (h : Γ.InS Δ) : Subst.InS φ Γ Δ + := ⟨Subst.fromWk h, λi => by simp only [Set.mem_setOf_eq, fromWk_apply, Wf.var_iff, h.prop i]⟩ + +@[simp] +theorem Subst.InS.coe_fromWk {Γ Δ : Ctx α ε} (h : Γ.InS Δ) + : ((fromWk h : Subst.InS φ Γ Δ) : Subst φ) = Subst.fromWk h + := rfl