Skip to content

Commit

Permalink
Substitution for term rewriting
Browse files Browse the repository at this point in the history
  • Loading branch information
@imbrem
imbrem committed Aug 29, 2024
1 parent 59a9075 commit c5fcac2
Show file tree
Hide file tree
Showing 4 changed files with 168 additions and 22 deletions.
14 changes: 7 additions & 7 deletions DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ theorem Eqv.reassoc_beta {A B C : Ty α} {Γ : Ctx α ε}
rw [reassoc, let2_pair, let1_pair, let1_beta_let2_eta]
simp only [wk1_let1, wk2_let2, wk2_var1, List.length_cons, Fin.mk_one, List.get_eq_getElem,
Fin.val_one, List.getElem_cons_succ, List.getElem_cons_zero, wk_pair, wk_var, Set.mem_setOf_eq,
Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte, Nat.ofNat_pos, lt_self_iff_false,
Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte, lt_self_iff_false,
le_refl, tsub_eq_zero_of_le, Ctx.InS.coe_wk2, zero_add, subst_let1, subst_let2,
subst_lift_var_succ, var0_subst0, Fin.zero_eta, Fin.val_zero, wk_res_eff, wk_eff_pair,
wk_eff_var, wk0_pair, wk0_var, Nat.reduceAdd, ← Subst.Eqv.lift_lift, subst_pair,
Expand All @@ -89,7 +89,7 @@ theorem Eqv.reassoc_inv_beta {A B C : Ty α} {Γ : Ctx α ε}
simp only [wk1_let2, wk1_var0, List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
List.getElem_cons_zero, wk_pair, wk_var, Set.mem_setOf_eq, Ctx.InS.coe_liftn₂, Nat.liftnWk,
Nat.reduceLT, ↓reduceIte, Nat.reduceSub, Ctx.InS.coe_wk1, Nat.liftWk_succ, Nat.succ_eq_add_one,
zero_add, Nat.reduceAdd, Nat.one_lt_ofNat, Nat.ofNat_pos, subst_let2, var0_subst0, wk_res_eff,
zero_add, Nat.reduceAdd, Nat.one_lt_ofNat, subst_let2, var0_subst0, wk_res_eff,
wk_eff_pair, wk_eff_var, subst_pair, subst_liftn₂_var_add_2, var_succ_subst0, wk0_var,
subst_liftn₂_var_one, ge_iff_le, Prod.mk_le_mk, le_refl, bot_le, and_self,
subst_liftn₂_var_zero, let2_pair, let1_beta_var1, ↓dreduceIte, Nat.liftWk_zero]
Expand Down Expand Up @@ -897,7 +897,7 @@ theorem Eqv.reassoc_tensor {A B C A' B' C' : Ty α} {Γ : Ctx α ε}
wk2_pair, wk2_nil, let2_let2, wk2_let2, wk2_var1, List.length_cons, Fin.mk_one,
List.get_eq_getElem, Fin.val_one, List.getElem_cons_succ, List.getElem_cons_zero, wk_var,
Set.mem_setOf_eq, Ctx.InS.coe_liftn₂, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte, le_refl,
Nat.ofNat_pos, lt_self_iff_false, tsub_eq_zero_of_le, Ctx.InS.coe_wk2, zero_add, let2_pair,
lt_self_iff_false, tsub_eq_zero_of_le, Ctx.InS.coe_wk2, zero_add, let2_pair,
let1_beta_var1, subst_let2, var_succ_subst0, subst_pair, subst_liftn₂_var_one, ge_iff_le,
Prod.mk_le_mk, bot_le, and_self, subst_liftn₂_var_zero, subst_liftn₂_var_add_2, var0_subst0,
Nat.reduceAdd, ↓dreduceIte, Nat.reduceSub, Nat.succ_eq_add_one, Fin.zero_eta, Fin.val_zero,
Expand Down Expand Up @@ -1001,7 +1001,7 @@ theorem Eqv.pentagon {W X Y Z : Ty α} {Γ : Ctx α ε}
rw [let1_let2]
simp only [wk0_pair, wk0_var, zero_add, Nat.reduceAdd, wk2, wk_let2, wk_var, Set.mem_setOf_eq,
Ctx.InS.coe_wk2, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte, wk_pair, Ctx.InS.coe_liftn₂,
Nat.ofNat_pos, lt_self_iff_false, le_refl, tsub_eq_zero_of_le, let1_beta_var1, subst_let1,
lt_self_iff_false, le_refl, tsub_eq_zero_of_le, let1_beta_var1, subst_let1,
subst_pair, var_succ_subst0, subst_let2, subst_lift_var_succ, var0_subst0, List.length_cons,
↓dreduceIte, Nat.reduceSub, Nat.succ_eq_add_one, Fin.zero_eta, List.get_eq_getElem,
Fin.val_zero, List.getElem_cons_zero, wk_res_eff, wk_eff_var, subst_liftn₂_var_one, ge_iff_le,
Expand All @@ -1019,7 +1019,7 @@ theorem Eqv.pentagon {W X Y Z : Ty α} {Γ : Ctx α ε}
simp only [subst_pair, subst_liftn₂_var_one, ge_iff_le, Prod.mk_le_mk, le_refl, bot_le, and_self,
subst_liftn₂_var_zero, subst_liftn₂_var_add_2, var0_subst0, List.length_cons, Nat.reduceAdd,
Nat.add_zero, Nat.zero_eq, Set.mem_setOf_eq, Ctx.InS.coe_liftn₂, Ctx.InS.coe_wk2, Nat.liftnWk,
lt_self_iff_false, ↓dreduceIte, Nat.reduceSub, Nat.ofNat_pos, Nat.succ_eq_add_one, Fin.zero_eta,
lt_self_iff_false, ↓dreduceIte, Nat.reduceSub, Nat.succ_eq_add_one, Fin.zero_eta,
List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, wk_res_eff, wk_eff_pair, wk_eff_var,
wk0_pair, wk0_var, zero_add, wk1, wk_let2, wk_var, Ctx.InS.coe_wk1, Nat.liftWk_zero, wk_pair,
Nat.one_lt_ofNat, ↓reduceIte, Nat.reduceLT, Nat.liftWk_succ, subst_let2, id_eq, var_succ_subst0,
Expand All @@ -1044,11 +1044,11 @@ theorem Eqv.hexagon {X Y Z : Ty α} {Γ : Ctx α ε}
List.getElem_cons_zero, wk_res_eff, wk_eff_var, subst_lift_braid, let2_let2, wk2, wk_let2,
wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk2, Nat.liftnWk, Nat.one_lt_ofNat, ↓reduceIte, ←
Ctx.InS.lift_lift, wk_let1, wk_pair, Ctx.InS.coe_lift, Nat.liftWk_zero, Nat.liftWk_succ,
Nat.ofNat_pos, wk_lift_braid, wk0_nil, subst_let2, ← Subst.Eqv.lift_lift, subst_lift_var_zero,
wk_lift_braid, wk0_nil, subst_let2, ← Subst.Eqv.lift_lift, subst_lift_var_zero,
↓dreduceIte, Nat.reduceSub, Nat.succ_eq_add_one]
congr
simp only [seq_braid, let2_let2, wk2, wk_pair, wk_var, Set.mem_setOf_eq, Ctx.InS.coe_wk2,
Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte, Nat.one_lt_ofNat, let2_pair, wk0_pair, wk0_var,
Nat.liftnWk, ↓reduceIte, Nat.one_lt_ofNat, let2_pair, wk0_pair, wk0_var,
zero_add, Nat.reduceAdd, let1_beta_var1, subst_let1, subst_pair, var_succ_subst0,
subst_lift_var_zero, subst_lift_var_succ, var0_subst0, List.length_cons, ↓dreduceIte,
Nat.reduceSub, Nat.succ_eq_add_one, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
Expand Down
2 changes: 1 addition & 1 deletion DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1471,7 +1471,7 @@ theorem Eqv.Pure.let1_let2_of_left {Γ : Ctx α ε}
Set.mem_setOf_eq, Subst.InS.get, Subst.InS.liftn₂, InS.coe_subst0, Subst.liftn,
lt_self_iff_false, ↓reduceIte, le_refl, tsub_eq_zero_of_le, subst0_zero,
Subst.InS.coe_comp, Subst.comp, Term.subst, Ctx.InS.coe_comp, Ctx.InS.coe_swap02,
Function.comp_apply, Nat.one_lt_ofNat, Nat.swap0_lt, Nat.ofNat_pos, InS.coe_wk,
Function.comp_apply, Nat.one_lt_ofNat, Nat.swap0_lt, InS.coe_wk,
Ctx.InS.coe_wk0, Term.wk_wk]
rfl
| succ i => rfl
Expand Down
103 changes: 89 additions & 14 deletions DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Step.lean
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,3 @@
import Mathlib.Combinatorics.Quiver.Path
import Mathlib.Combinatorics.Quiver.Symmetric
import Mathlib.CategoryTheory.PathCategory
import Mathlib.Algebra.Order.BigOperators.Group.Finset

import Discretion.Correspondence.Definitions

import DeBruijnSSA.BinSyntax.Syntax.Subst
Expand Down Expand Up @@ -43,7 +38,7 @@ inductive Rewrite : Term φ → Term φ → Prop
| let2_pair (a b r) : Rewrite (let2 (pair a b) r) (let1 a $ let1 b.wk0 $ r)
| let1_eta (a) : Rewrite (let1 a (var 0)) a
| let2_bind (e r) :
Rewrite (let2 e r) (let1 e $ (let2 (var 0) (r.wk (Nat.liftnWk 2 Nat.succ))))
Rewrite (let2 e r) (let1 e $ (let2 (var 0) (r.wk2)))
| case_bind (e r s) :
Rewrite (case e r s) (let1 e $ case (var 0) (r.wk1) (s.wk1))
| case_eta (a) : Rewrite (case a (inl (var 0)) (inr (var 0))) a
Expand Down Expand Up @@ -71,22 +66,102 @@ inductive Rewrite : Term φ → Term φ → Prop
(let1 e $ pair (case (var 0) al.wk1 ar.wk1) (case (var 0) bl.wk1 br.wk1))
| case_wk0_wk0 (e r) : Rewrite (case e (wk0 r) (wk0 r)) (let1 e r.wk0)

theorem Rewrite.wk {e e' : Term φ} (h : e.Rewrite e') (ρ) : (e.wk ρ).Rewrite (e'.wk ρ)
:= sorry

theorem Rewrite.subst {e e' : Term φ} (h : e.Rewrite e') (σ) : (e.subst σ).Rewrite (e'.subst σ)
:= sorry
:= by induction h with
| let1_op f e r =>
simp only [Term.subst, Subst.lift_zero, <-wk1_subst_lift]
exact let1_op f (e.subst σ) (r.subst (σ.lift))
| let1_let1 a b r =>
simp only [Term.subst, <-wk1_subst_lift]
exact let1_let1 (a.subst σ) (b.subst (σ.lift)) (r.subst (σ.lift))
| let1_pair a b r =>
simp only [Term.subst, Subst.lift_succ, wk, Nat.succ_eq_add_one, zero_add,
Subst.lift_zero, <-Term.wk1_subst_lift, Term.subst_lift]
exact let1_pair (a.subst σ) (b.subst σ) (r.subst (σ.lift))
| let1_let2 a b r =>
simp only [Term.subst, <-wk1_subst_lift, Subst.liftn_two]
exact let1_let2 (a.subst σ) (b.subst σ.lift.lift) (r.subst σ.lift)
| let1_inl e r =>
simp only [Term.subst, <-wk1_subst_lift]
exact let1_inl (e.subst σ) (r.subst (σ.lift))
| let1_inr e r =>
simp only [Term.subst, <-wk1_subst_lift]
exact let1_inr (e.subst σ) (r.subst (σ.lift))
| let1_case a l r s =>
simp only [Term.subst, <-wk1_subst_lift]
exact let1_case (a.subst σ) (l.subst σ.lift) (r.subst σ.lift) (s.subst σ.lift)
| let1_abort e r =>
simp only [Term.subst, <-wk1_subst_lift]
exact let1_abort (e.subst σ) (r.subst σ.lift)
| let2_eta a => exact let2_eta (a.subst σ)
| let2_pair a b r =>
simp only [Term.subst, <-wk1_subst_lift, Subst.liftn_two, <-wk0_subst]
exact let2_pair (a.subst σ) (b.subst σ) (r.subst σ.lift.lift)
| let1_eta a => exact let1_eta (a.subst σ)
| let2_bind e r =>
simp only [Term.subst, <-wk1_subst_lift, Subst.liftn_two, <-wk2_subst_lift_lift]
exact let2_bind (e.subst σ) (r.subst (σ.lift.lift))
| case_bind e r s =>
simp only [Term.subst, <-wk1_subst_lift]
exact case_bind (e.subst σ) (r.subst σ.lift) (s.subst σ.lift)
| case_eta a => exact case_eta (a.subst σ)
| let1_let1_case a b r s =>
simp only [Term.subst, <-wk1_subst_lift, <-wk0_subst, <-swap01_subst_lift_lift]
exact let1_let1_case (a.subst σ) (b.subst σ.lift)
(r.subst σ.lift.lift.lift) (s.subst σ.lift.lift.lift)
| let1_let2_case a b r s =>
simp only [
Term.subst, <-wk1_subst_lift, <-wk0_subst, <-swap02_subst_lift_lift_lift, Subst.liftn_two]
exact let1_let2_case (a.subst σ) (b.subst σ.lift)
(r.subst σ.lift.lift.lift.lift) (s.subst σ.lift.lift.lift.lift)
| let1_case_case a d ll lr rl rr =>
simp only [
Term.subst, <-wk1_subst_lift, <-swap01_subst_lift_lift, <-swap01_subst_lift_lift,
<-wk0_subst
]
exact let1_case_case (a.subst σ) (d.subst σ.lift)
(ll.subst σ.lift.lift.lift) (lr.subst σ.lift.lift.lift)
(rl.subst σ.lift.lift.lift) (rr.subst σ.lift.lift.lift)
| case_op_op e f r s =>
simp only [Term.subst, <-wk1_subst_lift]
exact case_op_op (e.subst σ) f (r.subst σ.lift) (s.subst σ.lift)
| case_inl_inl e r s =>
simp only [Term.subst, <-wk1_subst_lift]
exact case_inl_inl (e.subst σ) (r.subst σ.lift) (s.subst σ.lift)
| case_inr_inr e r s =>
simp only [Term.subst, <-wk1_subst_lift]
exact case_inr_inr (e.subst σ) (r.subst σ.lift) (s.subst σ.lift)
| case_abort_abort e r s =>
simp only [Term.subst, <-wk1_subst_lift]
exact case_abort_abort (e.subst σ) (r.subst σ.lift) (s.subst σ.lift)
| case_pair_pair e al bl ar br =>
simp only [Term.subst, <-wk1_subst_lift]
exact case_pair_pair (e.subst σ)
(al.subst σ.lift) (bl.subst σ.lift)
(ar.subst σ.lift) (br.subst σ.lift)
| case_wk0_wk0 e r =>
simp only [Term.subst, <-wk1_subst_lift, <-wk0_subst]
exact case_wk0_wk0 (e.subst σ) (r.subst σ)

theorem Rewrite.wk {e e' : Term φ} (h : e.Rewrite e') (ρ) : (e.wk ρ).Rewrite (e'.wk ρ)
:= by simp only [<-Term.subst_fromWk]; exact h.subst _

-- TODO: Cong.Rewrite induces a Setoid on Term... but we should maybe add more stuff?

inductive Reduce : Term φ → Term φ → Prop
| case_inl (e r s) : Reduce (case (inl e) r s) (let1 e r)
| case_inr (e r s) : Reduce (case (inr e) r s) (let1 e s)

theorem Reduce.wk {e e' : Term φ} (h : e.Reduce e') (ρ) : (e.wk ρ).Reduce (e'.wk ρ)
:= sorry

theorem Reduce.subst {e e' : Term φ} (h : e.Reduce e') (σ) : (e.subst σ).Reduce (e'.subst σ)
:= sorry
:= by induction h with
| case_inl e r s =>
simp only [Term.subst, <-wk1_subst_lift]
exact case_inl (e.subst σ) (r.subst σ.lift) (s.subst σ.lift)
| case_inr e r s =>
simp only [Term.subst, <-wk1_subst_lift]
exact case_inr (e.subst σ) (r.subst σ.lift) (s.subst σ.lift)

theorem Reduce.wk {e e' : Term φ} (h : e.Reduce e') (ρ) : (e.wk ρ).Reduce (e'.wk ρ)
:= by simp only [<-Term.subst_fromWk]; exact h.subst _

-- TODO: Step, FStep, friends...
71 changes: 71 additions & 0 deletions DeBruijnSSA/BinSyntax/Syntax/Subst.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -391,6 +391,77 @@ theorem wkn_comp_substn_succ (n : ℕ) (e : Term φ)
@[simp]
theorem alpha_var : (var n).alpha n = @Subst.id φ := by funext n; simp [alpha, Subst.id]

theorem wk0_subst {σ : Subst φ} {e : Term φ}
: (e.subst σ).wk0 = e.wk0.subst σ.lift := (subst_lift e σ).symm

theorem wk1_subst_lift {σ : Subst φ} {e : Term φ}
: (e.subst σ.lift).wk1 = e.wk1.subst σ.lift.lift := by
simp only [wk1, <-subst_fromWk, subst_subst]
congr
funext k
cases k with
| zero => rfl
| succ k =>
simp only [
Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ
]
rfl

theorem wk2_subst_lift_lift {σ : Subst φ} {e : Term φ}
: (e.subst σ.lift.lift).wk2 = e.wk2.subst σ.lift.lift.lift := by
simp only [wk2, <-subst_fromWk, subst_subst]
congr
funext k
cases k with
| zero => rfl
| succ k =>
cases k with
| zero => rfl
| succ k =>
simp_arith only [
Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte
]
rfl

theorem swap01_subst_lift_lift {σ : Subst φ} {e : Term φ}
: (e.subst σ.lift.lift).swap01 = e.swap01.subst σ.lift.lift := by
simp only [swap01, <-subst_fromWk, subst_subst]
congr
funext k
cases k with
| zero => rfl
| succ k =>
cases k with
| zero => rfl
| succ k =>
simp_arith only [
Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte, Nat.swap0
]
rfl

theorem swap02_subst_lift_lift_lift {σ : Subst φ} {e : Term φ}
: (e.subst σ.lift.lift.lift).swap02 = e.swap02.subst σ.lift.lift.lift := by
simp only [swap02, <-subst_fromWk, subst_subst]
congr
funext k
cases k with
| zero => rfl
| succ k =>
cases k with
| zero => rfl
| succ k =>
cases k with
| zero => rfl
| succ k =>
simp_arith only [
Subst.comp, BinSyntax.Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one, Subst.lift_succ,
wk_wk, subst_fromWk, Nat.liftWk_succ_comp_succ, Nat.liftnWk, ↓reduceIte, Nat.swap0
]
rfl

end Term

/-- Substitute the free variables in a body -/
Expand Down

0 comments on commit c5fcac2

Please sign in to comment.