From 8d645dd45842526d402300ddf3aff94db4c49405 Mon Sep 17 00:00:00 2001 From: Andrew Marmaduke Date: Sun, 31 May 2026 20:15:40 -0500 Subject: [PATCH 1/4] wip --- LeanSubst/Ren.lean | 149 +++++++++++++++++-------- LeanSubst/Subst.lean | 227 ++++++++++++++++++++++++++++----------- LeanSubst/Subst_Old.lean | 137 +++++++++++++++++++++++ LeanSubst/Types.lean | 24 +++++ 4 files changed, 429 insertions(+), 108 deletions(-) create mode 100644 LeanSubst/Subst_Old.lean create mode 100644 LeanSubst/Types.lean diff --git a/LeanSubst/Ren.lean b/LeanSubst/Ren.lean index 2dd13b0..04f03d0 100644 --- a/LeanSubst/Ren.lean +++ b/LeanSubst/Ren.lean @@ -8,67 +8,94 @@ namespace LeanSubst def Ren.id : Ren := ⟨λ x => x⟩ + @[simp] + theorem Ren.id_action {x} : id.act x = x := by simp [Ren.id] + + def Ren.succ : Ren := ⟨(· + 1)⟩ + + @[simp] + theorem Ren.succ_action {x} : succ.act x = x + 1 := by simp [Ren.succ] + + def Ren.pred : Ren := ⟨(· - 1)⟩ + + @[simp] + theorem Ren.pred_action {x} : pred.act x = x - 1 := by simp [Ren.pred] + def Ren.add (k : Nat) : Ren := ⟨(· + k)⟩ + @[simp] + theorem Ren.add_action {k x} : (add k).act x = x + k := by simp [Ren.add] + + @[simp] + theorem Ren.add_zero : add 0 = id := by simp [Ren.add, Ren.id] + + @[simp] + theorem Ren.add_one : add 1 = succ := by simp [Ren.add, Ren.succ] + def Ren.sub (k : Nat) : Ren := ⟨(· - k)⟩ - def Ren.lift (r : Ren) (k : Nat := 1) : Ren := .mk λ n => - if n < k then n else r.act (n - k) + k + @[simp] + theorem Ren.sub_action {k x} : (sub k).act x = x - k := by simp [Ren.sub] + + @[simp] + theorem Ren.sub_zero : sub 0 = id := by simp [Ren.sub, Ren.id] + + @[simp] + theorem Ren.sub_one : sub 1 = pred := by simp [Ren.sub, Ren.pred] def Ren.cons (a : Nat) (r : Ren) : Ren := .mk λ n => match n with | 0 => a | n + 1 => r.act n + infixr:67 (name := Ren.cons_notation) " :: " => Ren.cons + + @[simp] + theorem Ren.cons_action0 {a} {r : Ren} : (a::r).act 0 = a := by simp [Ren.cons] + + @[simp] + theorem Ren.cons_action {a i} {r : Ren} : (a::r).act (i + 1) = r.act i := by simp [Ren.cons] + def Ren.append : List Nat -> Ren -> Ren | .nil, r => r - | .cons hd tl, r => append tl (r.cons hd) + | .cons hd tl, r => hd::append tl r instance : HAppend (List Nat) Ren Ren where hAppend := Ren.append - def Ren.compose : Ren -> Ren -> Ren - | r1, r2 => .mk λ n => r2.act (r1.act n) - - class RenMap (T : Type) where - rmap : Ren -> T -> T - - export RenMap (rmap) + @[simp] + theorem Ren.append_nil {r : Ren} : ([] : List Nat) ++ r = r := by + simp [HAppend.hAppend, Ren.append] - macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t) - infixr:67 (name := Ren.cons_notation) " :: " => Ren.cons - infixr:85 (name := Ren.compose_notation) " ∘ " => Ren.compose + @[simp] + theorem Ren.append_cons {a} {ℓ : List Nat} {r : Ren} : (a::ℓ) ++ r = a::(ℓ ++ r) := by + simp [HAppend.hAppend, Ren.append] - @[app_unexpander rmap] - def unexpandRenApply : Lean.PrettyPrinter.Unexpander - | `($_ $r $t) => `($t⟨$r⟩) - | _ => throw () + @[simp, grind <-] + theorem Ren.append_action_lt {r : Ren} {i} + : {ℓ : List Nat} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] + | .cons hd tl, h => + match i with + | 0 => rfl + | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) @[simp, grind =] - theorem Ren.lift_zero {r : Ren} : r.lift 0 = r := by - unfold Ren.lift; congr + theorem Ren.append_action_ge {r : Ren} {i} + : {ℓ : List Nat} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) + | .nil, h => by simp + | .cons hd tl, h => + match i with + | 0 => by simp at h + | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) - @[grind =] - theorem Ren.lift_succ {r : Ren} {k} : r.lift (k + 1) = (r.lift k).lift := by - induction k; simp - case _ n ih => - unfold Ren.lift; congr; funext; case _ i => - simp; unfold Ren.lift at ih; simp at ih - grind - - @[simp] - theorem Ren.id_action {x} : Ren.id.act x = x := by simp [Ren.id] - - @[simp] - theorem Ren.lift_id {k} : Ren.lift Ren.id k = Ren.id := by - simp [Ren.id, Ren.lift]; congr; funext; case _ x => - cases x <;> simp; omega + def Ren.compose : Ren -> Ren -> Ren + | r1, r2 => .mk λ n => r2.act (r1.act n) - @[simp] - theorem Ren.cons_head_action {n} {r : Ren} : (n::r).act 0 = n := by simp [Ren.cons] + infixr:85 (name := Ren.compose_notation) " ∘ " => Ren.compose @[simp] - theorem Ren.cons_tail_action {n i} {r : Ren} : (n::r).act (i + 1) = r.act i := by simp [Ren.cons] + theorem Ren.compose_action {r1 r2 : Ren} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by + simp [Ren.compose] @[simp] theorem Ren.compose_id_left {r : Ren} : id ∘ r = r := by @@ -82,9 +109,33 @@ namespace LeanSubst theorem Ren.compose_assoc {r1 r2 r3 : Ren} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by simp [Ren.compose] + def Ren.lift (r : Ren) (k : Nat := 1) : Ren := .mk λ n => + if n < k then n else r.act (n - k) + k + + @[simp, grind <-] + theorem Ren.lift_action_lt {r k i} (h : i < k) : (lift r k).act i = i := by + simp [Ren.lift]; grind + + @[simp, grind <-] + theorem Ren.lift_action_ge {r k i} (h : i ≥ k) : (lift r k).act i = r.act (i - k) + k := by + simp [Ren.lift]; grind + @[simp] - theorem Ren.compose_action {r1 r2 : Ren} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by - simp [Ren.compose] + theorem Ren.lift_of_zero {r : Ren} : r.lift 0 = r := by + unfold Ren.lift; congr + + @[grind =] + theorem Ren.lift_of_succ {r : Ren} {k} : r.lift (k + 1) = (r.lift k).lift := by + induction k; simp + case _ n ih => + unfold Ren.lift; congr; funext; case _ i => + simp; unfold Ren.lift at ih; simp at ih + grind + + @[simp] + theorem Ren.lift_id {k} : Ren.lift Ren.id k = Ren.id := by + simp [Ren.id, Ren.lift]; congr; funext; case _ x => + cases x <;> simp; omega theorem Ren.compose_lift_k1 {r1 r2 : Ren} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by simp [Ren.compose, Ren.lift] @@ -95,18 +146,30 @@ namespace LeanSubst theorem Ren.compose_lift {k} {r1 r2 : Ren} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by induction k generalizing r1 r2; simp case _ k ih => - rw [lift_succ, ih] - rw [lift_succ (r := r1)] - rw [lift_succ (r := r2)] + rw [lift_of_succ, ih] + rw [lift_of_succ (r := r1)] + rw [lift_of_succ (r := r2)] rw [compose_lift_k1] + class RenMap (T : Type) where + rmap : Ren -> T -> T + + export RenMap (rmap) + + macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t) + + @[app_unexpander rmap] + def unexpandRenApply : Lean.PrettyPrinter.Unexpander + | `($_ $r $t) => `($t⟨$r⟩) + | _ => throw () + class RenMapId (S : Type) [RenMap S] where apply_id {t : S} : t⟨Ren.id⟩ = t class RenMapCompose (S : Type) [RenMap S] where apply_compose {s : S} {r1 r2 : Ren} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩ - @[simp, grind =] + @[simp] theorem Ren.apply_id [RenMap T] [RenMapId T] {t : T} : t⟨id⟩ = t := RenMapId.apply_id @[simp, grind =] diff --git a/LeanSubst/Subst.lean b/LeanSubst/Subst.lean index a17602e..7b8a3ca 100644 --- a/LeanSubst/Subst.lean +++ b/LeanSubst/Subst.lean @@ -11,92 +11,200 @@ namespace LeanSubst export Subst.Action (re su) + @[simp] + def Subst.Action.rmap {T} [RenMap T] (r : Ren) : Subst.Action T -> Subst.Action T + | re x => re $ r.act x + | su t => su t⟨r⟩ + + instance [RenMap T] : RenMap (Subst.Action T) where + rmap := Subst.Action.rmap + + @[simp] + theorem Subst.Action.rmap_re [RenMap T] {r} {x : Nat} + : (@re T x)⟨r⟩ = re (r.act x) + := by simp [RenMap.rmap] + + @[simp] + theorem Subst.Action.rmap_su [RenMap T] {r} {t : T} : (su t)⟨r⟩ = su t⟨r⟩ := by + simp [RenMap.rmap] + + instance [RenMap T] [RenMapId T] : RenMapId (Subst.Action T) where + apply_id := by + intro t; simp [RenMap.rmap] + cases t <;> simp + + instance [RenMap T] [RenMapCompose T] : RenMapCompose (Subst.Action T) where + apply_compose := by + intro s r1 r2; simp [RenMap.rmap, Ren.compose] + cases s <;> simp [Ren.compose] + structure Subst (T : Type) where act : Nat -> Subst.Action T - @[coe] - def Ren.to : Ren -> Subst T - | r => .mk λ n => re (r.act n) + def Subst.id : Subst T := ⟨λ x => re x⟩ + notation "+0" => Subst.id - instance : Coe Ren (Subst T) where - coe := Ren.to + @[simp] + theorem Subst.id_action {x} : (@Subst.id T).act x = re x := by simp [Subst.id] - class SubstMap (S T : Type) where - smap : Subst T -> S -> S + def Subst.succ : Subst T := ⟨λ x => re $ x + 1⟩ + notation "+1" => Subst.succ - export SubstMap (smap) + @[simp] + theorem Subst.succ_action {x} : (@Subst.succ T).act x = re (x + 1) := by simp [Subst.succ] - def Subst.lift [RenMap T] (σ : Subst T) (k : Nat := 1) : Subst T := .mk λ n => - if n < k then re n else - match σ.act (n - k) with - | su t => su (rmap (Ren.add k) t) - | re i => re (i + k) + def Subst.pred : Subst T := ⟨λ x => re $ x - 1⟩ + notation "-1" => Subst.pred + + @[simp] + theorem Subst.pred_action {x} : (@Subst.pred T).act x = re (x - 1) := by simp [Subst.pred] + + def Subst.add (k : Nat) : Subst T := ⟨λ x => re $ x + k⟩ + + @[simp] + theorem Subst.add_action {k x} : (@Subst.add T k).act x = re (x + k) := by simp [Subst.add] + + @[simp] + theorem Subst.add_zero : add 0 = @id T := by simp [Subst.add, Subst.id] + + @[simp] + theorem Subst.add_one : add 1 = @succ T := by simp [Subst.add, Subst.succ] + + def Subst.sub (k : Nat) : Subst T := ⟨λ x => re $ x - k⟩ + + @[simp] + theorem Subst.sub_action {k x} : (@Subst.sub T k).act x = re (x - k) := by simp [Subst.sub] + + @[simp] + theorem Subst.sub_zero : sub 0 = @id T := by simp [Subst.sub, Subst.id] + + @[simp] + theorem Subst.sub_one : sub 1 = @pred T := by simp [Subst.sub, Subst.pred] def Subst.cons (a : Subst.Action T) (σ : Subst T) : Subst T := .mk λ n => match n with | 0 => a | n + 1 => σ.act n + infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons + + @[simp] + theorem Subst.cons_action0 {a} {σ : Subst T} : (a::σ).act 0 = a := by simp [Subst.cons] + + @[simp] + theorem Subst.cons_action {a i} {σ : Subst T} : (a::σ).act (i + 1) = σ.act i := by + simp [Subst.cons] + def Subst.append : List (Subst.Action T) -> Subst T -> Subst T | .nil, σ => σ - | .cons hd tl, σ => append tl (σ.cons hd) + | .cons hd tl, σ => hd::append tl σ instance : HAppend (List $ Subst.Action T) (Subst T) (Subst T) where hAppend := Subst.append @[simp] - abbrev smap1 [SubstMap S S] := smap (S := S) (T := S) + theorem Subst.append_nil {σ : Subst T} : ([] : List $ Action T) ++ σ = σ := by + simp [HAppend.hAppend, Subst.append] + + @[simp] + theorem Subst.append_cons {a} {ℓ : List (Action T)} {σ : Subst T} + : (a::ℓ) ++ σ = a::(ℓ ++ σ) + := by simp [HAppend.hAppend, Subst.append] + + @[simp, grind <-] + theorem Subst.append_action_lt {σ : Subst T} {i} + : {ℓ : List $ Action T} -> (h : i < ℓ.length) -> (ℓ ++ σ).act i = ℓ[i] + | .cons hd tl, h => + match i with + | 0 => rfl + | i + 1 => append_action_lt (σ := σ) (ℓ := tl) (by grind) + + @[simp, grind =] + theorem Subst.append_action_ge {σ : Subst T} {i} + : {ℓ : List $ Action T} -> (h : i ≥ ℓ.length) -> (ℓ ++ σ).act i = σ.act (i - ℓ.length) + | .nil, h => by simp + | .cons hd tl, h => + match i with + | 0 => by simp at h + | i + 1 => @append_action_ge σ i tl (by grind) |> cast (by simp) + + class SubstMap (S T : Type) where + smap : Subst T -> S -> S + + export SubstMap (smap) + + macro:max t:term noWs "[" σ:term "]" : term => `(smap $σ $t) + + @[app_unexpander smap] + def unexpandSubstApply : Lean.PrettyPrinter.Unexpander + | `($_ $σ $t) => `($t[$σ]) + | _ => throw () def Subst.compose [RenMap T] [SubstMap T T] : Subst T -> Subst T -> Subst T | σ, τ => .mk λ n => match σ.act n with - | su t => su (smap τ t) + | su t => su t[τ] | re k => τ.act k - def Subst.hcompose [RenMap T] [SubstMap S T] : Subst S -> Subst T -> Subst S - | σ, τ => .mk λ n => - match σ.act n with - | su t => su (smap τ t) - | re k => re k + infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose - def Subst.id : Subst T := ⟨λ n => re n⟩ - def Subst.succ : Subst T := ⟨λ n => re (n + 1)⟩ - def Subst.pred : Subst T := ⟨λ n => re (n - 1)⟩ + def Subst.lift [RenMap T] (σ : Subst T) (k : Nat := 1) : Subst T := .mk λ n => + if n < k then re n else (σ.act (n - k))⟨.add k⟩ + + @[simp, grind <-] + theorem Subst.lift_action_lt [RenMap T] {σ : Subst T} {k i} (h : i < k) + : (lift σ k).act i = re i + := by simp [Subst.lift]; grind + + @[simp, grind <-] + theorem Subst.lift_action_ge [RenMap T] {σ : Subst T} {k i} (h : i ≥ k) + : (lift σ k).act i = (σ.act (i - k))⟨.add k⟩ + := by simp [Subst.lift]; grind + + -- @[simp] + -- theorem Subst.lift_of_zero [RenMap T] [RenMapId T] {σ : Subst T} : σ.lift 0 = σ := by + -- unfold Subst.lift; congr; simp + + -- @[grind =] + -- theorem Subst.lift_of_succ [RenMap T] [RenMapId T] {σ : Subst T} {k} : σ.lift (k + 1) = (σ.lift k).lift := by + -- induction k; simp + -- case _ n ih => + -- unfold Subst.lift; congr; funext; case _ i => + -- simp; unfold Subst.lift at ih; simp at ih + -- grind + + -- @[simp] + -- theorem Subst.lift_id {k} : Subst.lift Subst.id k = Subst.id := by + -- simp [Subst.id, Subst.lift]; congr; funext; case _ x => + -- cases x <;> simp; omega - notation "+0" => Subst.id - macro "+0@" noWs T:term : term =>`(@Subst.id $T) - notation "+1" => Subst.succ - macro "+1@" noWs T:term : term =>`(@Subst.succ $T) - notation "-1" => Subst.pred - macro "-1@" noWs T:term : term =>`(@Subst.pred $T) + @[coe] + def Ren.to : Ren -> Subst T + | r => .mk λ n => re (r.act n) - @[simp, grind =] - theorem Subst.id_action {n} : (+0@T).act n = re n := by simp [Subst.id] + instance : Coe Ren (Subst T) where + coe := Ren.to @[simp, grind =] - theorem Subst.succ_action {n} : (+1@T).act n = re (n + 1) := by simp [Subst.succ] + theorem Ren.to_id : Ren.to (T := T) id = +0 := by simp [Ren.to, Subst.id, id] @[simp, grind =] - theorem Subst.pred_action {n} : (-1@T).act n = re (n - 1) := by simp [Subst.pred] + theorem Ren.to_succ : Ren.to (T := T) succ = +1 := by simp [Ren.to, Subst.succ] @[simp, grind =] - theorem Ren.to_id : Ren.to (T := T) id = +0 := by - unfold Ren.to; unfold Subst.id; simp [id] + theorem Ren.to_pred : Ren.to (T := T) pred = -1 := by simp [Ren.to, Subst.pred] @[simp, grind =] - theorem Ren.to_succ : Ren.to (T := T) (Ren.add 1) = +1 := by - unfold Ren.to; simp; unfold Subst.succ; simp [Ren.add] + theorem Ren.to_add {k} : Ren.to (T := T) (add k) = Subst.add k := by simp [Ren.to, Subst.add] @[simp, grind =] - theorem Ren.to_pred : Ren.to (T := T) (Ren.sub 1) = -1 := by - unfold Ren.to; simp; unfold Subst.pred; simp [Ren.sub] + theorem Ren.to_sub {k} : Ren.to (T := T) (sub k) = Subst.sub k := by simp [Ren.to, Subst.sub] @[simp, grind =] theorem Ren.pred_succ [RenMap T] [SubstMap T T] : Subst.compose (T := T) +1 -1 = +0 := by - unfold Subst.compose; simp - unfold Subst.id; rfl + simp [Subst.compose, Subst.id] - @[grind =] + @[simp, grind =] theorem Ren.to_lift [RenMap T] {r : Ren} {k} : (r.lift k).to = (@Ren.to T r).lift k := by cases r; simp [Ren.lift, Ren.to, Subst.lift]; case _ act => funext; case _ x => @@ -104,34 +212,23 @@ namespace LeanSubst case zero => grind case _ n => cases Nat.decLt (n + 1) k <;> simp [ite] - macro:max t:term noWs "[" σ:term "]" : term => `(smap1 $σ $t) - macro:max t:term noWs "[" σ:term ":" T:term "]" : term => `(smap (T := $T) $σ $t) - infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons - infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose - infixr:85 " ◾ " => Subst.hcompose - - @[app_unexpander smap1] - def unexpandSubstApply1 : Lean.PrettyPrinter.Unexpander - | `($_ $σ $t) => `($t[$σ]) - | _ => throw () - - @[app_unexpander smap] - def unexpandSubstApply : Lean.PrettyPrinter.Unexpander - | `($_ $σ $t) => `($t[$σ : _]) - | `($_ (T := $T) $σ $t) => `($t[$σ : $T]) - | _ => throw () - @[simp, grind =] theorem Ren.to_compose {r1 r2 : Ren} [RenMap T] [SubstMap T T] - : Ren.to (T := T) (r1 ∘ r2) = Subst.compose r1 r2 + : Ren.to (T := T) (r1 ∘ r2) = r1.to ∘ r2.to := by funext; case _ x => cases x <;> simp [Ren.to, Subst.compose, Ren.compose] - @[simp] - theorem Subst.cons_head_action {t} {σ : Subst T} : (t::σ).act 0 = t := by simp [Subst.cons] + -- def Subst.hcompose [RenMap T] [SubstMap S T] : Subst S -> Subst T -> Subst S + -- | σ, τ => .mk λ n => + -- match σ.act n with + -- | su t => su (smap τ t) + -- | re k => re k - @[simp] - theorem Subst.cons_tail_action {t i} {σ : Subst T} : (t::σ).act (i + 1) = σ.act i := by simp [Subst.cons] + -- infixr:85 " ◾ " => Subst.hcompose + + -- macro "+0@" noWs T:term : term =>`(@Subst.id $T) + -- macro "+1@" noWs T:term : term =>`(@Subst.succ $T) + -- macro "-1@" noWs T:term : term =>`(@Subst.pred $T) end LeanSubst diff --git a/LeanSubst/Subst_Old.lean b/LeanSubst/Subst_Old.lean new file mode 100644 index 0000000..a17602e --- /dev/null +++ b/LeanSubst/Subst_Old.lean @@ -0,0 +1,137 @@ +import LeanSubst.Ren + +namespace LeanSubst + universe u + variable {S T : Type} + + inductive Subst.Action (T : Type) where + | re : Nat -> Subst.Action T + | su : T -> Subst.Action T + deriving Repr + + export Subst.Action (re su) + + structure Subst (T : Type) where + act : Nat -> Subst.Action T + + @[coe] + def Ren.to : Ren -> Subst T + | r => .mk λ n => re (r.act n) + + instance : Coe Ren (Subst T) where + coe := Ren.to + + class SubstMap (S T : Type) where + smap : Subst T -> S -> S + + export SubstMap (smap) + + def Subst.lift [RenMap T] (σ : Subst T) (k : Nat := 1) : Subst T := .mk λ n => + if n < k then re n else + match σ.act (n - k) with + | su t => su (rmap (Ren.add k) t) + | re i => re (i + k) + + def Subst.cons (a : Subst.Action T) (σ : Subst T) : Subst T := .mk λ n => + match n with + | 0 => a + | n + 1 => σ.act n + + def Subst.append : List (Subst.Action T) -> Subst T -> Subst T + | .nil, σ => σ + | .cons hd tl, σ => append tl (σ.cons hd) + + instance : HAppend (List $ Subst.Action T) (Subst T) (Subst T) where + hAppend := Subst.append + + @[simp] + abbrev smap1 [SubstMap S S] := smap (S := S) (T := S) + + def Subst.compose [RenMap T] [SubstMap T T] : Subst T -> Subst T -> Subst T + | σ, τ => .mk λ n => + match σ.act n with + | su t => su (smap τ t) + | re k => τ.act k + + def Subst.hcompose [RenMap T] [SubstMap S T] : Subst S -> Subst T -> Subst S + | σ, τ => .mk λ n => + match σ.act n with + | su t => su (smap τ t) + | re k => re k + + def Subst.id : Subst T := ⟨λ n => re n⟩ + def Subst.succ : Subst T := ⟨λ n => re (n + 1)⟩ + def Subst.pred : Subst T := ⟨λ n => re (n - 1)⟩ + + notation "+0" => Subst.id + macro "+0@" noWs T:term : term =>`(@Subst.id $T) + notation "+1" => Subst.succ + macro "+1@" noWs T:term : term =>`(@Subst.succ $T) + notation "-1" => Subst.pred + macro "-1@" noWs T:term : term =>`(@Subst.pred $T) + + @[simp, grind =] + theorem Subst.id_action {n} : (+0@T).act n = re n := by simp [Subst.id] + + @[simp, grind =] + theorem Subst.succ_action {n} : (+1@T).act n = re (n + 1) := by simp [Subst.succ] + + @[simp, grind =] + theorem Subst.pred_action {n} : (-1@T).act n = re (n - 1) := by simp [Subst.pred] + + @[simp, grind =] + theorem Ren.to_id : Ren.to (T := T) id = +0 := by + unfold Ren.to; unfold Subst.id; simp [id] + + @[simp, grind =] + theorem Ren.to_succ : Ren.to (T := T) (Ren.add 1) = +1 := by + unfold Ren.to; simp; unfold Subst.succ; simp [Ren.add] + + @[simp, grind =] + theorem Ren.to_pred : Ren.to (T := T) (Ren.sub 1) = -1 := by + unfold Ren.to; simp; unfold Subst.pred; simp [Ren.sub] + + @[simp, grind =] + theorem Ren.pred_succ [RenMap T] [SubstMap T T] : Subst.compose (T := T) +1 -1 = +0 := by + unfold Subst.compose; simp + unfold Subst.id; rfl + + @[grind =] + theorem Ren.to_lift [RenMap T] {r : Ren} {k} : (r.lift k).to = (@Ren.to T r).lift k := by + cases r; simp [Ren.lift, Ren.to, Subst.lift]; case _ act => + funext; case _ x => + cases x + case zero => grind + case _ n => cases Nat.decLt (n + 1) k <;> simp [ite] + + macro:max t:term noWs "[" σ:term "]" : term => `(smap1 $σ $t) + macro:max t:term noWs "[" σ:term ":" T:term "]" : term => `(smap (T := $T) $σ $t) + infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons + infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose + infixr:85 " ◾ " => Subst.hcompose + + @[app_unexpander smap1] + def unexpandSubstApply1 : Lean.PrettyPrinter.Unexpander + | `($_ $σ $t) => `($t[$σ]) + | _ => throw () + + @[app_unexpander smap] + def unexpandSubstApply : Lean.PrettyPrinter.Unexpander + | `($_ $σ $t) => `($t[$σ : _]) + | `($_ (T := $T) $σ $t) => `($t[$σ : $T]) + | _ => throw () + + @[simp, grind =] + theorem Ren.to_compose {r1 r2 : Ren} [RenMap T] [SubstMap T T] + : Ren.to (T := T) (r1 ∘ r2) = Subst.compose r1 r2 + := by + funext; case _ x => + cases x <;> simp [Ren.to, Subst.compose, Ren.compose] + + @[simp] + theorem Subst.cons_head_action {t} {σ : Subst T} : (t::σ).act 0 = t := by simp [Subst.cons] + + @[simp] + theorem Subst.cons_tail_action {t i} {σ : Subst T} : (t::σ).act (i + 1) = σ.act i := by simp [Subst.cons] + +end LeanSubst diff --git a/LeanSubst/Types.lean b/LeanSubst/Types.lean new file mode 100644 index 0000000..c770dc2 --- /dev/null +++ b/LeanSubst/Types.lean @@ -0,0 +1,24 @@ + +namespace LeanSubst + universe u1 u2 + variable {S : Type u1} {T : Type u2} + + structure Ren where + act : Nat -> Nat + + structure HetRen (T : Type u1) where + act : Nat -> Nat + + inductive Subst.Action (T : Type u1) where + | re : Nat -> Subst.Action T + | su : T -> Subst.Action T + deriving Repr + + export Subst.Action (re su) + + structure Subst (T : Type u1) where + act : Nat -> Subst.Action T + + + +end LeanSubst From 59e78c09e75239e69951288955a57dc25224a02d Mon Sep 17 00:00:00 2001 From: Andrew Marmaduke Date: Sun, 31 May 2026 22:15:04 -0500 Subject: [PATCH 2/4] wip --- LeanSubst/{ => Old}/HetRen.lean | 0 LeanSubst/{ => Old}/Laws.lean | 0 LeanSubst/{ => Old}/List.lean | 0 LeanSubst/{ => Old}/Option.lean | 0 LeanSubst/{ => Old}/Ren.lean | 0 LeanSubst/{ => Old}/Subst.lean | 0 LeanSubst/{ => Old}/Subst_Old.lean | 0 LeanSubst/Ops.lean | 157 +++++++++++++++++++++++++++++ LeanSubst/Types.lean | 50 ++++++--- 9 files changed, 194 insertions(+), 13 deletions(-) rename LeanSubst/{ => Old}/HetRen.lean (100%) rename LeanSubst/{ => Old}/Laws.lean (100%) rename LeanSubst/{ => Old}/List.lean (100%) rename LeanSubst/{ => Old}/Option.lean (100%) rename LeanSubst/{ => Old}/Ren.lean (100%) rename LeanSubst/{ => Old}/Subst.lean (100%) rename LeanSubst/{ => Old}/Subst_Old.lean (100%) create mode 100644 LeanSubst/Ops.lean diff --git a/LeanSubst/HetRen.lean b/LeanSubst/Old/HetRen.lean similarity index 100% rename from LeanSubst/HetRen.lean rename to LeanSubst/Old/HetRen.lean diff --git a/LeanSubst/Laws.lean b/LeanSubst/Old/Laws.lean similarity index 100% rename from LeanSubst/Laws.lean rename to LeanSubst/Old/Laws.lean diff --git a/LeanSubst/List.lean b/LeanSubst/Old/List.lean similarity index 100% rename from LeanSubst/List.lean rename to LeanSubst/Old/List.lean diff --git a/LeanSubst/Option.lean b/LeanSubst/Old/Option.lean similarity index 100% rename from LeanSubst/Option.lean rename to LeanSubst/Old/Option.lean diff --git a/LeanSubst/Ren.lean b/LeanSubst/Old/Ren.lean similarity index 100% rename from LeanSubst/Ren.lean rename to LeanSubst/Old/Ren.lean diff --git a/LeanSubst/Subst.lean b/LeanSubst/Old/Subst.lean similarity index 100% rename from LeanSubst/Subst.lean rename to LeanSubst/Old/Subst.lean diff --git a/LeanSubst/Subst_Old.lean b/LeanSubst/Old/Subst_Old.lean similarity index 100% rename from LeanSubst/Subst_Old.lean rename to LeanSubst/Old/Subst_Old.lean diff --git a/LeanSubst/Ops.lean b/LeanSubst/Ops.lean new file mode 100644 index 0000000..6d83a7a --- /dev/null +++ b/LeanSubst/Ops.lean @@ -0,0 +1,157 @@ + +import LeanSubst.Types + +namespace LeanSubst + +universe u1 u2 u3 +variable {S : Type u1} {T : Type u2} + +def Ren.id : Ren := ⟨λ x => x⟩ + +@[simp] +theorem Ren.id_action {x} : id.act x = x := by simp [Ren.id] + +def Ren.succ : Ren := ⟨(· + 1)⟩ + +@[simp] +theorem Ren.succ_action {x} : succ.act x = x + 1 := by simp [Ren.succ] + +def Ren.pred : Ren := ⟨(· - 1)⟩ + +@[simp] +theorem Ren.pred_action {x} : pred.act x = x - 1 := by simp [Ren.pred] + +def Ren.add (k : Nat) : Ren := ⟨(· + k)⟩ + +@[simp] +theorem Ren.add_action {k x} : (add k).act x = x + k := by simp [Ren.add] + +@[simp] +theorem Ren.add_zero : add 0 = id := by simp [Ren.add, Ren.id] + +@[simp] +theorem Ren.add_one : add 1 = succ := by simp [Ren.add, Ren.succ] + +def Ren.sub (k : Nat) : Ren := ⟨(· - k)⟩ + +@[simp] +theorem Ren.sub_action {k x} : (sub k).act x = x - k := by simp [Ren.sub] + +@[simp] +theorem Ren.sub_zero : sub 0 = id := by simp [Ren.sub, Ren.id] + +@[simp] +theorem Ren.sub_one : sub 1 = pred := by simp [Ren.sub, Ren.pred] + +def Ren.cons (a : Nat) (r : Ren) : Ren := .mk λ n => + match n with + | 0 => a + | n + 1 => r.act n + +infixr:67 (name := Ren.cons_notation) " :: " => Ren.cons + +@[simp] +theorem Ren.cons_action0 {a} {r : Ren} : (a::r).act 0 = a := by simp [Ren.cons] + +@[simp] +theorem Ren.cons_action {a i} {r : Ren} : (a::r).act (i + 1) = r.act i := by simp [Ren.cons] + +def Ren.append : List Nat -> Ren -> Ren +| .nil, r => r +| .cons hd tl, r => hd::append tl r + +instance : HAppend (List Nat) Ren Ren where + hAppend := Ren.append + +@[simp] +theorem Ren.append_nil {r : Ren} : ([] : List Nat) ++ r = r := by + simp [HAppend.hAppend, Ren.append] + +@[simp] +theorem Ren.append_cons {a} {ℓ : List Nat} {r : Ren} : (a::ℓ) ++ r = a::(ℓ ++ r) := by + simp [HAppend.hAppend, Ren.append] + +@[simp, grind <-] +theorem Ren.append_action_lt {r : Ren} {i} + : {ℓ : List Nat} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] +| .cons hd tl, h => + match i with + | 0 => rfl + | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) + +@[simp, grind =] +theorem Ren.append_action_ge {r : Ren} {i} + : {ℓ : List Nat} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) +| .nil, h => by simp +| .cons hd tl, h => + match i with + | 0 => by simp at h + | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) + +def Ren.compose : Ren -> Ren -> Ren +| r1, r2 => .mk λ n => r2.act (r1.act n) + +infixr:85 (name := Ren.compose_notation) " ∘ " => Ren.compose + +@[simp] +theorem Ren.compose_action {r1 r2 : Ren} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by + simp [Ren.compose] + +@[simp] +theorem Ren.compose_id_left {r : Ren} : id ∘ r = r := by + simp [Ren.compose, Ren.id] + +@[simp] +theorem Ren.compose_id_right {r : Ren} : r ∘ id = r := by + simp [Ren.compose, Ren.id] + +@[simp] +theorem Ren.compose_assoc {r1 r2 r3 : Ren} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by + simp [Ren.compose] + +def Ren.lift (r : Ren) (k : Nat := 1) : Ren := .mk λ n => + if n < k then n else r.act (n - k) + k + +@[simp, grind <-] +theorem Ren.lift_action_lt {r k i} (h : i < k) : (lift r k).act i = i := by + simp [Ren.lift]; grind + +@[simp, grind <-] +theorem Ren.lift_action_ge {r k i} (h : i ≥ k) : (lift r k).act i = r.act (i - k) + k := by + simp [Ren.lift]; grind + +@[simp] +theorem Ren.lift_of_zero {r : Ren} : r.lift 0 = r := by + unfold Ren.lift; congr + +@[grind =] +theorem Ren.lift_of_succ {r : Ren} {k} : r.lift (k + 1) = (r.lift k).lift := by + induction k; simp + case _ n ih => + unfold Ren.lift; congr; funext; case _ i => + simp; unfold Ren.lift at ih; simp at ih + grind + +@[simp] +theorem Ren.lift_id {k} : Ren.lift Ren.id k = Ren.id := by + simp [Ren.id, Ren.lift]; congr; funext; case _ x => + cases x <;> simp; omega + +theorem Ren.compose_lift_k1 {r1 r2 : Ren} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by + simp [Ren.compose, Ren.lift] + funext; case _ x => + cases x <;> simp + +@[simp] +theorem Ren.compose_lift {k} {r1 r2 : Ren} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by + induction k generalizing r1 r2; simp + case _ k ih => + rw [lift_of_succ, ih] + rw [lift_of_succ (r := r1)] + rw [lift_of_succ (r := r2)] + rw [compose_lift_k1] + + + + +end LeanSubst diff --git a/LeanSubst/Types.lean b/LeanSubst/Types.lean index c770dc2..911ad8a 100644 --- a/LeanSubst/Types.lean +++ b/LeanSubst/Types.lean @@ -1,24 +1,48 @@ namespace LeanSubst - universe u1 u2 - variable {S : Type u1} {T : Type u2} - structure Ren where - act : Nat -> Nat +universe u1 u2 u3 +variable {S : Type u1} {T : Type u2} - structure HetRen (T : Type u1) where - act : Nat -> Nat +structure Ren where + act : Nat -> Nat - inductive Subst.Action (T : Type u1) where - | re : Nat -> Subst.Action T - | su : T -> Subst.Action T - deriving Repr +class RenMap (S : Type u1) where + rmap : Ren -> S -> S - export Subst.Action (re su) +export RenMap (rmap) - structure Subst (T : Type u1) where - act : Nat -> Subst.Action T +macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t) +structure HetRen (T : Type u2) where + act : Nat -> Nat +class HetRenMap (S : Type u1) (T : Type u2) where + hrmap : HetRen T -> S -> S + +export HetRenMap (hrmap) + +inductive Subst.Action (S : Type u1) where +| re : Nat -> Subst.Action S +| su : S -> Subst.Action S +deriving Repr + +export Subst.Action (re su) + +structure Subst (S : Type u1) where + act : Nat -> Subst.Action S + +class SubstMap (S : Type u1) where + smap : Subst S -> S -> S + +export SubstMap (smap) + +structure HetSubst (S : Type u1) (T : Type u2) where + act : Nat -> Subst.Action S + +class HetSubstMap (S : Type u1) (T : Type u2) where + hsmap : HetSubst S T -> S -> S + +export HetSubstMap (hsmap) end LeanSubst From bbba96da58d75fe9b56af58da6aaa1d26e9c9cf0 Mon Sep 17 00:00:00 2001 From: Andrew Marmaduke Date: Mon, 1 Jun 2026 01:42:34 -0500 Subject: [PATCH 3/4] wip --- LeanSubst/Lemma/Ren.lean | 24 ++ LeanSubst/Ops.lean | 381 ++++++++++++++++++++++- LeanSubst/{ => Rewriting}/Normal.lean | 0 LeanSubst/{ => Rewriting}/Reduction.lean | 0 LeanSubst/Types.lean | 38 ++- 5 files changed, 431 insertions(+), 12 deletions(-) create mode 100644 LeanSubst/Lemma/Ren.lean rename LeanSubst/{ => Rewriting}/Normal.lean (100%) rename LeanSubst/{ => Rewriting}/Reduction.lean (100%) diff --git a/LeanSubst/Lemma/Ren.lean b/LeanSubst/Lemma/Ren.lean new file mode 100644 index 0000000..8a39fb1 --- /dev/null +++ b/LeanSubst/Lemma/Ren.lean @@ -0,0 +1,24 @@ + +import LeanSubst.Ops + +namespace LeanSubst + +universe u1 u2 u3 +variable {S : Type u1} {T : Type u2} + +class RenMapId (S : Type u1) [RenMap S] where + apply_id {t : S} : t⟨Ren.id⟩ = t + +class RenMapCompose (S : Type u1) [RenMap S] where + apply_compose {s : S} {r1 r2 : Ren} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩ + +@[simp] +theorem Ren.apply_id [RenMap T] [RenMapId T] {t : T} : t⟨id⟩ = t := RenMapId.apply_id + +@[simp, grind =] +theorem Ren.apply_compose [RenMap T] [RenMapCompose T] {t : T} {r1 r2 : Ren} + : t⟨r1⟩⟨r2⟩ = t⟨r1 ∘ r2⟩ +:= RenMapCompose.apply_compose + + +end LeanSubst diff --git a/LeanSubst/Ops.lean b/LeanSubst/Ops.lean index 6d83a7a..612eab9 100644 --- a/LeanSubst/Ops.lean +++ b/LeanSubst/Ops.lean @@ -6,21 +6,165 @@ namespace LeanSubst universe u1 u2 u3 variable {S : Type u1} {T : Type u2} +---------------------------------------------------------------------------------------------------- +---- Translation +---------------------------------------------------------------------------------------------------- +def Ren.het T (r : Ren) : HetRen T := ⟨r.act⟩ + +@[simp] +theorem Ren.het_act {r : Ren} {x} : (r.het T).act x = r.act x := by simp [Ren.het] + +def HetRen.forget (r : HetRen T) : Ren := ⟨r.act⟩ + +@[simp] +theorem HetRen.forget_act {r : HetRen T} {x} : r.forget.act x = r.act x := by simp [HetRen.forget] + +@[simp] +theorem Ren.het_forget (r : Ren) : (r.het T).forget = r := by simp [Ren.het, HetRen.forget] + +@[simp] +theorem HetRen.forget_het (r : HetRen T) : r.forget.het T = r := by simp [Ren.het, HetRen.forget] + +def Subst.het S (σ : Subst T) : HetSubst S T := ⟨σ.act⟩ + +@[simp] +theorem Subst.het_act {r : Subst T} {x} : (r.het S).act x = r.act x := by simp [Subst.het] + +def HetSubst.forget (σ : HetSubst S T) : Subst T := ⟨σ.act⟩ + +@[simp] +theorem HetSubst.forget_act {r : HetSubst S T} {x} : r.forget.act x = r.act x := by + simp [HetSubst.forget] + +@[simp] +theorem Subst.het_forget (σ : Subst T) : (σ.het S).forget = σ := by + simp [Subst.het, HetSubst.forget] + +@[simp] +theorem HetSubst.forget_het (σ : HetSubst S T) : σ.forget.het S = σ := by + simp [Subst.het, HetSubst.forget] + +def Ren.to (r : Ren) : Subst S := ⟨λ x => re (r.act x)⟩ + +@[simp] +theorem Ren.to_act {r : Ren} {x} : (@Ren.to S r).act x = re (r.act x) := by simp [Ren.to] + +def HetRen.to (r : HetRen T) : HetSubst S T := ⟨λ x => re (r.act x)⟩ + +@[simp] +theorem HetRen.to_act {r : HetRen T} {x} : (@HetRen.to S T r).act x = re (r.act x) := by + simp [HetRen.to] +---------------------------------------------------------------------------------------------------- +---- Action +---------------------------------------------------------------------------------------------------- +@[simp] +def Action.rmap [RenMap S] (r : Ren) : Action S -> Action S +| re x => re $ r.act x +| su t => su t⟨r⟩ + +instance [RenMap S] : RenMap (Action S) where + rmap := Action.rmap + +@[simp] +theorem Action.rmap_re [RenMap S] {r : Ren} {x : Nat} + : (@re S x)⟨r⟩ = re (r.act x) +:= by simp [RenMap.rmap] + +@[simp] +theorem Action.rmap_su [RenMap S] {r : Ren} {t : S} : (su t)⟨r⟩ = su t⟨r⟩ := by simp [RenMap.rmap] + +@[simp] +def Action.hsmap [SubstMap S] (σ : HetSubst (Action S) S) : Action S -> Action S +| re x => σ.act x +| su t => su t[σ.forget] + +instance [SubstMap S] : HetSubstMap (Action S) S where + hsmap := Action.hsmap + +@[simp] +theorem Action.hsmap_re [SubstMap S] {σ : HetSubst (Action S) S} {x : Nat} + : (@re S x)[σ] = σ.act x +:= by simp [HetSubstMap.hsmap] + +@[simp] +theorem Action.hsmap_su [SubstMap S] {σ : HetSubst (Action S) S} {t : S} + : (su t)[σ] = su t[σ.forget] +:= by simp [HetSubstMap.hsmap] +---------------------------------------------------------------------------------------------------- +---- Identity +---------------------------------------------------------------------------------------------------- def Ren.id : Ren := ⟨λ x => x⟩ @[simp] theorem Ren.id_action {x} : id.act x = x := by simp [Ren.id] +def HetRen.id T : HetRen T := ⟨λ x => x⟩ + +@[simp] +theorem HetRen.id_action {x} : (id T).act x = x := by simp [HetRen.id] + +def Subst.id : Subst S := ⟨λ x => re x⟩ +notation "+0" => Subst.id + +@[simp] +theorem Subst.id_action {x} : (@id S).act x = re x := by simp [Subst.id] + +def HetSubst.id T : HetSubst S T := ⟨λ x => re x⟩ +macro "+0@" noWs T:term : term =>`(HetSubst.id $T) + +@[simp] +theorem HetSubst.id_action {x} : (@id S T).act x = re x := by simp [HetSubst.id] +---------------------------------------------------------------------------------------------------- +---- Successor +---------------------------------------------------------------------------------------------------- def Ren.succ : Ren := ⟨(· + 1)⟩ @[simp] theorem Ren.succ_action {x} : succ.act x = x + 1 := by simp [Ren.succ] +def HetRen.succ T : HetRen T := ⟨(· + 1)⟩ + +@[simp] +theorem HetRen.succ_action {x} : (succ T).act x = x + 1 := by simp [HetRen.succ] + +def Subst.succ : Subst S := ⟨λ x => re $ x + 1⟩ +notation "+1" => Subst.succ + +@[simp] +theorem Subst.succ_action {x} : (@succ S).act x = re (x + 1) := by simp [Subst.succ] + +def HetSubst.succ T : HetSubst S T := ⟨λ x => re $ x + 1⟩ +macro "+1@" noWs T:term : term =>`(HetSubst.succ $T) + +@[simp] +theorem HetSubst.succ_action {x} : (@succ S T).act x = re (x + 1) := by simp [HetSubst.succ] +---------------------------------------------------------------------------------------------------- +---- Predecessor +---------------------------------------------------------------------------------------------------- def Ren.pred : Ren := ⟨(· - 1)⟩ @[simp] theorem Ren.pred_action {x} : pred.act x = x - 1 := by simp [Ren.pred] +def HetRen.pred T : HetRen T := ⟨(· - 1)⟩ + +@[simp] +theorem HetRen.pred_action {x} : (pred T).act x = x - 1 := by simp [HetRen.pred] + +def Subst.pred : Subst S := ⟨λ x => re $ x - 1⟩ +notation "-1" => Subst.pred + +@[simp] +theorem Subst.pred_action {x} : (@pred S).act x = re (x - 1) := by simp [Subst.pred] + +def HetSubst.pred : HetSubst S T := ⟨λ x => re $ x - 1⟩ +macro "-1@" noWs T:term : term =>`(HetSubst.pred $T) + +@[simp] +theorem HetSubst.pred_action {x} : (@pred S T).act x = re (x - 1) := by simp [HetSubst.pred] +---------------------------------------------------------------------------------------------------- +---- Addition +---------------------------------------------------------------------------------------------------- def Ren.add (k : Nat) : Ren := ⟨(· + k)⟩ @[simp] @@ -32,6 +176,41 @@ theorem Ren.add_zero : add 0 = id := by simp [Ren.add, Ren.id] @[simp] theorem Ren.add_one : add 1 = succ := by simp [Ren.add, Ren.succ] +def HetRen.add T (k : Nat) : HetRen T := ⟨(· + k)⟩ + +@[simp] +theorem HetRen.add_action {k x} : (add T k).act x = x + k := by simp [HetRen.add] + +@[simp] +theorem HetRen.add_zero : add T 0 = id T := by simp [HetRen.add, HetRen.id] + +@[simp] +theorem HetRen.add_one : add T 1 = succ T := by simp [HetRen.add, HetRen.succ] + +def Subst.add (k : Nat) : Subst S := ⟨λ x => re $ x + k⟩ + +@[simp] +theorem Subst.add_action {k x} : (@add S k).act x = re (x + k) := by simp [Subst.add] + +@[simp] +theorem Subst.add_zero : @add S 0 = id := by simp [Subst.add, Subst.id] + +@[simp] +theorem Subst.add_one : @add S 1 = succ := by simp [Subst.add, Subst.succ] + +def HetSubst.add (k : Nat) : HetSubst S T := ⟨λ x => re $ x + k⟩ + +@[simp] +theorem HetSubst.add_action {k x} : (@add S T k).act x = re (x + k) := by simp [HetSubst.add] + +@[simp] +theorem HetSubst.add_zero : @add S T 0 = id T := by simp [HetSubst.add, HetSubst.id] + +@[simp] +theorem HetSubst.add_one : @add S T 1 = succ T := by simp [HetSubst.add, HetSubst.succ] +---------------------------------------------------------------------------------------------------- +---- Subtraction +---------------------------------------------------------------------------------------------------- def Ren.sub (k : Nat) : Ren := ⟨(· - k)⟩ @[simp] @@ -43,11 +222,23 @@ theorem Ren.sub_zero : sub 0 = id := by simp [Ren.sub, Ren.id] @[simp] theorem Ren.sub_one : sub 1 = pred := by simp [Ren.sub, Ren.pred] +def HetRen.sub T (k : Nat) : HetRen T := ⟨(· - k)⟩ + +@[simp] +theorem HetRen.sub_action {k x} : (sub T k).act x = x - k := by simp [HetRen.sub] + +@[simp] +theorem HetRen.sub_zero : sub T 0 = id T := by simp [HetRen.sub, HetRen.id] + +@[simp] +theorem HetRen.sub_one : sub T 1 = pred T := by simp [HetRen.sub, HetRen.pred] +---------------------------------------------------------------------------------------------------- +---- Cons +---------------------------------------------------------------------------------------------------- def Ren.cons (a : Nat) (r : Ren) : Ren := .mk λ n => match n with | 0 => a | n + 1 => r.act n - infixr:67 (name := Ren.cons_notation) " :: " => Ren.cons @[simp] @@ -56,6 +247,46 @@ theorem Ren.cons_action0 {a} {r : Ren} : (a::r).act 0 = a := by simp [Ren.cons] @[simp] theorem Ren.cons_action {a i} {r : Ren} : (a::r).act (i + 1) = r.act i := by simp [Ren.cons] +def HetRen.cons (a : Nat) (r : HetRen T) : HetRen T := .mk λ n => + match n with + | 0 => a + | n + 1 => r.act n +infixr:67 (name := HetRen.cons_notation) " :: " => HetRen.cons + +@[simp] +theorem HetRen.cons_action0 {a} {r : HetRen T} : (a::r).act 0 = a := by simp [HetRen.cons] + +@[simp] +theorem HetRen.cons_action {a i} {r : HetRen T} : (a::r).act (i + 1) = r.act i := by + simp [HetRen.cons] + +def Subst.cons (a : Action S) (r : Subst S) : Subst S := .mk λ n => + match n with + | 0 => a + | n + 1 => r.act n +infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons + +@[simp] +theorem Subst.cons_action0 {a} {r : Subst S} : (a::r).act 0 = a := by simp [Subst.cons] + +@[simp] +theorem Subst.cons_action {a i} {r : Subst S} : (a::r).act (i + 1) = r.act i := by simp [Subst.cons] + +def HetSubst.cons (a : Action T) (r : HetSubst S T) : HetSubst S T := .mk λ n => + match n with + | 0 => a + | n + 1 => r.act n +infixr:67 (name := HetSubst.cons_notation) " :: " => HetSubst.cons + +@[simp] +theorem HetSubst.cons_action0 {a} {r : HetSubst S T} : (a::r).act 0 = a := by simp [HetSubst.cons] + +@[simp] +theorem HetSubst.cons_action {a i} {r : HetSubst S T} : (a::r).act (i + 1) = r.act i := by + simp [HetSubst.cons] +---------------------------------------------------------------------------------------------------- +---- Append +---------------------------------------------------------------------------------------------------- def Ren.append : List Nat -> Ren -> Ren | .nil, r => r | .cons hd tl, r => hd::append tl r @@ -79,7 +310,7 @@ theorem Ren.append_action_lt {r : Ren} {i} | 0 => rfl | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) -@[simp, grind =] +@[simp, grind <-] theorem Ren.append_action_ge {r : Ren} {i} : {ℓ : List Nat} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) | .nil, h => by simp @@ -88,9 +319,107 @@ theorem Ren.append_action_ge {r : Ren} {i} | 0 => by simp at h | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) +def HetRen.append : List Nat -> HetRen T -> HetRen T +| .nil, r => r +| .cons hd tl, r => hd::append tl r + +instance : HAppend (List Nat) (HetRen T) (HetRen T) where + hAppend := HetRen.append + +@[simp] +theorem HetRen.append_nil {r : HetRen T} : ([] : List Nat) ++ r = r := by + simp [HAppend.hAppend, HetRen.append] + +@[simp] +theorem HetRen.append_cons {a} {ℓ : List Nat} {r : HetRen T} : (a::ℓ) ++ r = a::(ℓ ++ r) := by + simp [HAppend.hAppend, HetRen.append] + +@[simp, grind <-] +theorem HetRen.append_action_lt {r : HetRen T} {i} + : {ℓ : List Nat} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] +| .cons hd tl, h => + match i with + | 0 => rfl + | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) + +@[simp, grind <-] +theorem HetRen.append_action_ge {r : HetRen T} {i} + : {ℓ : List Nat} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) +| .nil, h => by simp +| .cons hd tl, h => + match i with + | 0 => by simp at h + | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) + +def Subst.append : List (Action S) -> Subst S -> Subst S +| .nil, r => r +| .cons hd tl, r => hd::append tl r + +instance : HAppend (List $ Action S) (Subst S) (Subst S) where + hAppend := Subst.append + +@[simp] +theorem Subst.append_nil {r : Subst S} : ([] : List $ Action S) ++ r = r := by + simp [HAppend.hAppend, Subst.append] + +@[simp] +theorem Subst.append_cons {a} {ℓ : List $ Action S} {r : Subst S} : (a::ℓ) ++ r = a::(ℓ ++ r) := by + simp [HAppend.hAppend, Subst.append] + +@[simp, grind <-] +theorem Subst.append_action_lt {r : Subst S} {i} + : {ℓ : List $ Action S} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] +| .cons hd tl, h => + match i with + | 0 => rfl + | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) + +@[simp, grind <-] +theorem Subst.append_action_ge {r : Subst S} {i} + : {ℓ : List $ Action S} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) +| .nil, h => by simp +| .cons hd tl, h => + match i with + | 0 => by simp at h + | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) + +def HetSubst.append : List (Action T) -> HetSubst S T -> HetSubst S T +| .nil, r => r +| .cons hd tl, r => hd::append tl r + +instance : HAppend (List $ Action T) (HetSubst S T) (HetSubst S T) where + hAppend := HetSubst.append + +@[simp] +theorem HetSubst.append_nil {r : HetSubst S T} : ([] : List $ Action T) ++ r = r := by + simp [HAppend.hAppend, HetSubst.append] + +@[simp] +theorem HetSubst.append_cons {a} {ℓ : List $ Action T} {r : HetSubst S T} + : (a::ℓ) ++ r = a::(ℓ ++ r) +:= by simp [HAppend.hAppend, HetSubst.append] + +@[simp, grind <-] +theorem HetSubst.append_action_lt {r : HetSubst S T} {i} + : {ℓ : List $ Action T} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] +| .cons hd tl, h => + match i with + | 0 => rfl + | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) + +@[simp, grind <-] +theorem HetSubst.append_action_ge {r : HetSubst S T} {i} + : {ℓ : List $ Action T} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) +| .nil, h => by simp +| .cons hd tl, h => + match i with + | 0 => by simp at h + | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) +---------------------------------------------------------------------------------------------------- +---- Composition +---------------------------------------------------------------------------------------------------- def Ren.compose : Ren -> Ren -> Ren | r1, r2 => .mk λ n => r2.act (r1.act n) - infixr:85 (name := Ren.compose_notation) " ∘ " => Ren.compose @[simp] @@ -109,6 +438,46 @@ theorem Ren.compose_id_right {r : Ren} : r ∘ id = r := by theorem Ren.compose_assoc {r1 r2 r3 : Ren} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by simp [Ren.compose] +def HetRen.compose : HetRen T -> HetRen T -> HetRen T +| r1, r2 => .mk λ n => r2.act (r1.act n) +infixr:85 (name := HetRen.compose_notation) " ∘ " => HetRen.compose + +@[simp] +theorem HetRen.compose_action {r1 r2 : HetRen T} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by + simp [HetRen.compose] + +@[simp] +theorem HetRen.compose_id_left {r : HetRen T} : id T ∘ r = r := by + simp [HetRen.compose, HetRen.id] + +@[simp] +theorem HetRen.compose_id_right {r : HetRen T} : r ∘ id T = r := by + simp [HetRen.compose, HetRen.id] + +@[simp] +theorem HetRen.compose_assoc {r1 r2 r3 : HetRen T} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by + simp [HetRen.compose] + +def Subst.compose [RenMap S] [SubstMap S] : Subst S -> Subst S -> Subst S +| σ, τ => .mk λ n => (σ.act n)[τ.het _] +infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose + +@[simp] +theorem Subst.compose_action [RenMap S] [SubstMap S] {σ τ : Subst S} {x} + : (σ ∘ τ).act x = (σ.act x)[τ.het _] +:= by simp [Subst.compose] + +def HetSubst.compose [HetRenMap S T] [HetSubstMap S T] : HetSubst S T -> HetSubst S T -> HetSubst S T +| σ, τ => .mk λ n => (σ.act n)[τ] +infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose + +@[simp] +theorem Subst.compose_action [RenMap S] [SubstMap S] {σ τ : Subst S} {x} + : (σ ∘ τ).act x = (σ.act x)[τ.het _] +:= by simp [Subst.compose] +---------------------------------------------------------------------------------------------------- +---- Lift +---------------------------------------------------------------------------------------------------- def Ren.lift (r : Ren) (k : Nat := 1) : Ren := .mk λ n => if n < k then n else r.act (n - k) + k @@ -137,19 +506,19 @@ theorem Ren.lift_id {k} : Ren.lift Ren.id k = Ren.id := by simp [Ren.id, Ren.lift]; congr; funext; case _ x => cases x <;> simp; omega -theorem Ren.compose_lift_k1 {r1 r2 : Ren} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by +theorem Ren.lift_compose_k1 {r1 r2 : Ren} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by simp [Ren.compose, Ren.lift] funext; case _ x => cases x <;> simp @[simp] -theorem Ren.compose_lift {k} {r1 r2 : Ren} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by +theorem Ren.lift_compose {k} {r1 r2 : Ren} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by induction k generalizing r1 r2; simp case _ k ih => rw [lift_of_succ, ih] rw [lift_of_succ (r := r1)] rw [lift_of_succ (r := r2)] - rw [compose_lift_k1] + rw [lift_compose_k1] diff --git a/LeanSubst/Normal.lean b/LeanSubst/Rewriting/Normal.lean similarity index 100% rename from LeanSubst/Normal.lean rename to LeanSubst/Rewriting/Normal.lean diff --git a/LeanSubst/Reduction.lean b/LeanSubst/Rewriting/Reduction.lean similarity index 100% rename from LeanSubst/Reduction.lean rename to LeanSubst/Rewriting/Reduction.lean diff --git a/LeanSubst/Types.lean b/LeanSubst/Types.lean index 911ad8a..74560df 100644 --- a/LeanSubst/Types.lean +++ b/LeanSubst/Types.lean @@ -14,6 +14,11 @@ export RenMap (rmap) macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t) +@[app_unexpander rmap] +def unexpand_rmap : Lean.PrettyPrinter.Unexpander +| `($_ $r $t) => `($t⟨$r⟩) +| _ => throw () + structure HetRen (T : Type u2) where act : Nat -> Nat @@ -22,27 +27,48 @@ class HetRenMap (S : Type u1) (T : Type u2) where export HetRenMap (hrmap) -inductive Subst.Action (S : Type u1) where -| re : Nat -> Subst.Action S -| su : S -> Subst.Action S +macro:max t:term noWs "⟨" r:term "⟩" : term => `(hrmap $r $t) + +@[app_unexpander rmap] +def unexpand_hrmap : Lean.PrettyPrinter.Unexpander +| `($_ $r $t) => `($t⟨$r⟩) +| _ => throw () + +inductive Action (S : Type u1) where +| re : Nat -> Action S +| su : S -> Action S deriving Repr -export Subst.Action (re su) +export Action (re su) structure Subst (S : Type u1) where - act : Nat -> Subst.Action S + act : Nat -> Action S class SubstMap (S : Type u1) where smap : Subst S -> S -> S export SubstMap (smap) +macro:max t:term noWs "[" σ:term "]" : term => `(smap $σ $t) + +@[app_unexpander smap] +def unexpand_smap : Lean.PrettyPrinter.Unexpander +| `($_ $σ $t) => `($t[$σ]) +| _ => throw () + structure HetSubst (S : Type u1) (T : Type u2) where - act : Nat -> Subst.Action S + act : Nat -> Action T class HetSubstMap (S : Type u1) (T : Type u2) where hsmap : HetSubst S T -> S -> S export HetSubstMap (hsmap) +macro:max t:term noWs "[" σ:term "]" : term => `(hsmap $σ $t) + +@[app_unexpander smap] +def unexpand_hsmap : Lean.PrettyPrinter.Unexpander +| `($_ $σ $t) => `($t[$σ]) +| _ => throw () + end LeanSubst From 7982bbbed671ab37cdbd3943b55decc46c37c39b Mon Sep 17 00:00:00 2001 From: Andrew Marmaduke Date: Wed, 10 Jun 2026 20:11:30 -0500 Subject: [PATCH 4/4] rework laws --- {LeanSubst/Old => Archive}/List.lean | 0 Examples/LambdaCalc.lean | 30 +- Examples/LambdaCalcKit.lean | 36 +- LeanSubst.lean | 13 +- LeanSubst/Basic.lean | 44 +++ LeanSubst/Laws.lean | 409 +++++++++++++++++++ LeanSubst/Lemma/Ren.lean | 24 -- LeanSubst/Old/HetRen.lean | 123 ------ LeanSubst/Old/Laws.lean | 566 --------------------------- LeanSubst/Old/Option.lean | 45 --- LeanSubst/Old/Ren.lean | 180 --------- LeanSubst/Old/Subst.lean | 234 ----------- LeanSubst/Old/Subst_Old.lean | 137 ------- LeanSubst/Ops.lean | 509 ++++++++++-------------- LeanSubst/Rewriting/Normal.lean | 7 +- LeanSubst/Rewriting/Reduction.lean | 9 +- LeanSubst/Types.lean | 74 ---- LeanSubst/Types/List.lean | 51 +++ LeanSubst/Types/Option.lean | 51 +++ 19 files changed, 822 insertions(+), 1720 deletions(-) rename {LeanSubst/Old => Archive}/List.lean (100%) create mode 100644 LeanSubst/Basic.lean create mode 100644 LeanSubst/Laws.lean delete mode 100644 LeanSubst/Lemma/Ren.lean delete mode 100644 LeanSubst/Old/HetRen.lean delete mode 100644 LeanSubst/Old/Laws.lean delete mode 100644 LeanSubst/Old/Option.lean delete mode 100644 LeanSubst/Old/Ren.lean delete mode 100644 LeanSubst/Old/Subst.lean delete mode 100644 LeanSubst/Old/Subst_Old.lean delete mode 100644 LeanSubst/Types.lean create mode 100644 LeanSubst/Types/List.lean create mode 100644 LeanSubst/Types/Option.lean diff --git a/LeanSubst/Old/List.lean b/Archive/List.lean similarity index 100% rename from LeanSubst/Old/List.lean rename to Archive/List.lean diff --git a/Examples/LambdaCalc.lean b/Examples/LambdaCalc.lean index 0209aba..ba7de64 100644 --- a/Examples/LambdaCalc.lean +++ b/Examples/LambdaCalc.lean @@ -11,7 +11,7 @@ namespace LeanSubst.Examples.LambdaCalc infixl:65 " :@ " => Term.app @[coe] - def Term.from_action : Subst.Action Term -> Term + def Term.from_action : Action Term -> Term | re y => var y | su t => t @@ -29,34 +29,34 @@ namespace LeanSubst.Examples.LambdaCalc @[simp, grind =] theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] - instance instCoe_SubstActionTerm_Term : Coe (Subst.Action Term) Term where + instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where coe := Term.from_action @[simp] - def rmap (r : Ren) : Term -> Term + def rmap (r : Ren Term) : Term -> Term | .var x => .var (r.act x) | t1 :@ t2 => rmap r t1 :@ rmap r t2 | :λ t => :λ rmap r.lift t - instance : RenMap Term where + instance : RenMap Term Term where rmap := rmap @[simp, grind =] - theorem ren_var {x} {r : Ren} : (Term.var x)⟨r⟩ = .var (r.act x) := by + theorem ren_var {x} {r : Ren Term} : (Term.var x)⟨r⟩ = .var (r.act x) := by simp [RenMap.rmap] @[simp, grind =] - theorem ren_app {t1 t2} {r : Ren} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by + theorem ren_app {t1 t2} {r : Ren Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by simp [RenMap.rmap] @[simp, grind =] - theorem ren_lam {t} {r : Ren} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by + theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by simp [RenMap.rmap] - instance : RenMapId Term where + instance : RenMapId Term Term where apply_id := by subst_solve_id - instance : RenMapCompose Term where + instance : RenMapCompose Term Term where apply_compose := by subst_solve_compose @[simp] @@ -88,16 +88,24 @@ namespace LeanSubst.Examples.LambdaCalc generalize zdef : σ.act x = z cases z <;> simp [Term.from_action] + @[simp] + theorem Term.from_action_compose_ren {x} {σ : Subst Term} {r : Ren Term} + : (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x) + := by + simp [Term.from_action] + generalize zdef : σ.act x = z + cases z <;> simp + instance : SubstMapId Term Term where apply_id := by subst_solve_id - instance : SubstMapStable Term where + instance : SubstMapStable Term Term where apply_stable := by subst_solve_stable instance : SubstMapRenComposeLeft Term Term where apply_ren_compose_left := by subst_solve_compose - instance : SubstMapRenComposeRight Term Term where + instance : SubstMapRenComposeRight Term where apply_ren_compose_right := by subst_solve_compose instance : SubstMapCompose Term Term where diff --git a/Examples/LambdaCalcKit.lean b/Examples/LambdaCalcKit.lean index 3f75821..8b89f00 100644 --- a/Examples/LambdaCalcKit.lean +++ b/Examples/LambdaCalcKit.lean @@ -11,7 +11,7 @@ namespace LeanSubst.Examples.LambdaCalc infixl:65 " :@ " => Term.app @[coe] - def Term.from_action : Subst.Action Term -> Term + def Term.from_action : Action Term -> Term | re y => var y | su t => t @@ -29,11 +29,11 @@ namespace LeanSubst.Examples.LambdaCalc @[simp, grind =] theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] - instance instCoe_SubstActionTerm_Term : Coe (Subst.Action Term) Term where + instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where coe := Term.from_action @[simp] - def Term.ren_act (r : Ren) : Term -> Term + def Term.ren_act (r : Ren Term) : Term -> Term | .var x => .var (r.act x) | t => t @@ -47,12 +47,12 @@ namespace LeanSubst.Examples.LambdaCalc lift (f : A) (k : Nat := 1) : A @[simp] - instance : Kit Term Ren where + instance : Kit Term (Ren Term) where act := Term.ren_act lift f n := Ren.lift f n @[simp] - instance [RenMap Term] : Kit Term (Subst Term) where + instance [RenMap Term Term] : Kit Term (Subst Term) where act := Term.subst_act lift f n := Subst.lift f n @@ -63,27 +63,27 @@ namespace LeanSubst.Examples.LambdaCalc | :λ t => :λ kitmap (kit.lift σ) t @[simp] - def rmap (r : Ren) : Term -> Term := kitmap r + def rmap (r : Ren Term) : Term -> Term := kitmap r - instance : RenMap Term where + instance : RenMap Term Term where rmap := rmap @[simp, grind =] - theorem ren_var {x} {r : Ren} : (Term.var x)⟨r⟩ = .var (r.act x) := by + theorem ren_var {x} {r : Ren Term} : (Term.var x)⟨r⟩ = .var (r.act x) := by simp +instances [RenMap.rmap] @[simp, grind =] - theorem ren_app {t1 t2} {r : Ren} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by + theorem ren_app {t1 t2} {r : Ren Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by simp [RenMap.rmap] @[simp, grind =] - theorem ren_lam {t} {r : Ren} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by + theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by simp +instances [RenMap.rmap] - instance : RenMapId Term where + instance : RenMapId Term Term where apply_id := by intro t; induction t <;> simp [*] - instance : RenMapCompose Term where + instance : RenMapCompose Term Term where apply_compose := by subst_solve_compose @[simp] @@ -112,16 +112,24 @@ namespace LeanSubst.Examples.LambdaCalc generalize zdef : σ.act x = z cases z <;> simp [Term.from_action] + @[simp] + theorem Term.from_action_compose_ren {x} {σ : Subst Term} {r : Ren Term} + : (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x) + := by + simp [Term.from_action] + generalize zdef : σ.act x = z + cases z <;> simp + instance : SubstMapId Term Term where apply_id := by subst_solve_id - instance : SubstMapStable Term where + instance : SubstMapStable Term Term where apply_stable := by subst_solve_stable instance : SubstMapRenComposeLeft Term Term where apply_ren_compose_left := by subst_solve_compose - instance : SubstMapRenComposeRight Term Term where + instance : SubstMapRenComposeRight Term where apply_ren_compose_right := by subst_solve_compose instance : SubstMapCompose Term Term where diff --git a/LeanSubst.lean b/LeanSubst.lean index 0d966e3..e5654ba 100644 --- a/LeanSubst.lean +++ b/LeanSubst.lean @@ -1,9 +1,8 @@ -import LeanSubst.Ren -import LeanSubst.HetRen -import LeanSubst.Subst +import LeanSubst.Basic +import LeanSubst.Ops import LeanSubst.Laws -import LeanSubst.Option -import LeanSubst.List -import LeanSubst.Reduction -import LeanSubst.Normal +import LeanSubst.Types.Option +import LeanSubst.Types.List +import LeanSubst.Rewriting.Reduction +import LeanSubst.Rewriting.Normal diff --git a/LeanSubst/Basic.lean b/LeanSubst/Basic.lean new file mode 100644 index 0000000..e058419 --- /dev/null +++ b/LeanSubst/Basic.lean @@ -0,0 +1,44 @@ + +namespace LeanSubst + +universe u1 u2 +variable {S : Type u1} {T : Type u2} + +structure Ren (T : Type u2) where + act : Nat -> Nat + +class RenMap (S : Type u1) (T : Type u2) where + rmap : Ren T -> S -> S + +export RenMap (rmap) + +macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t) + +@[app_unexpander rmap] +def unexpand_rmap : Lean.PrettyPrinter.Unexpander +| `($_ $r $t) => `($t⟨$r⟩) +| _ => throw () + +inductive Action (T : Type u2) where +| re : Nat -> Action T +| su : T -> Action T +deriving Repr + +export Action (re su) + +structure Subst (T : Type u2) where + act : Nat -> Action T + +class SubstMap (S : Type u1) (T : Type u2) where + smap : Subst T -> S -> S + +export SubstMap (smap) + +macro:max t:term noWs "[" σ:term "]" : term => `(smap $σ $t) + +@[app_unexpander smap] +def unexpand_smap : Lean.PrettyPrinter.Unexpander +| `($_ $σ $t) => `($t[$σ]) +| _ => throw () + +end LeanSubst diff --git a/LeanSubst/Laws.lean b/LeanSubst/Laws.lean new file mode 100644 index 0000000..7d51b02 --- /dev/null +++ b/LeanSubst/Laws.lean @@ -0,0 +1,409 @@ + +import LeanSubst.Basic +import LeanSubst.Ops + +namespace LeanSubst + +universe u1 u2 u3 +variable {S : Type u1} {T : Type u2} {U : Type u3} + +class RenMapId (S : Type u1) (T : Type u2) [RenMap S T] where + apply_id {s : S} : s⟨.id T⟩ = s + +class RenMapCompose (S : Type u1) (T : Type u2) [RenMap S T] where + apply_compose {s : S} {r1 r2 : Ren T} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩ + +@[simp] +theorem Ren.apply_id [RenMap S T] [RenMapId S T] {s : S} : s⟨id T⟩ = s := RenMapId.apply_id + +@[simp, grind =] +theorem Ren.apply_compose [RenMap S T] [RenMapCompose S T] {s : S} {r1 r2 : Ren T} + : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩ +:= RenMapCompose.apply_compose + +instance (priority := high) [RenMap T T] [RenMapId T T] : RenMapId (Action T) T where + apply_id := by intro s; cases s <;> simp + +instance [RenMap S T] [RenMapId S T] : RenMapId (Action S) T where + apply_id := by intro s; cases s <;> simp + +instance (priority := high) [RenMap T T] [RenMapCompose T T] : RenMapCompose (Action T) T where + apply_compose := by intro s; cases s <;> simp + +instance [RenMap S T] [RenMapCompose S T] : RenMapCompose (Action S) T where + apply_compose := by intro s; cases s <;> simp + +class SubstMapId (S : Type u1) (T : Type u2) [SubstMap S T] where + apply_id {s : S} : s[.id T] = s + +class SubstMapStable (S : Type u1) (T : Type u2) [RenMap S T] [SubstMap S T] where + apply_stable (r : Ren T) (σ : Subst T) : r.to = σ -> rmap (S := S) r = smap σ + +class SubstMapRenComposeLeft (S : Type u1) (T : Type u2) [RenMap S T] [SubstMap S T] where + apply_ren_compose_left {s : S} {r : Ren T} {τ : Subst T} : s⟨r⟩[τ] = s[r ∘ τ] + +class SubstMapRenComposeRight (T : Type u2) [RenMap T T] [SubstMap T T] where + apply_ren_compose_right {t : T} {r : Ren T} {σ : Subst T} : t[σ]⟨r⟩ = t[σ ∘ r] + +class SubstMapCompose (S : Type u1) (T : Type u2) [SubstMap S T] [SubstMap T T] where + apply_compose {s : S} {σ τ : Subst T} : s[σ][τ] = s[σ ∘ τ] + +class SubstMapRenCommute (S : Type u1) (T : Type u2) [RenMap S S] [SubstMap S T] where + apply_ren_commute {s : S} (r : Ren S) (τ : Subst T) : s⟨r⟩[τ] = s[τ]⟨r⟩ + +class SubstMapHetCompose (S : Type u1) (T : Type u2) [SubstMap S S] [SubstMap S T] where + apply_hcompose {s : S} {σ : Subst S} {τ : Subst T} : s[σ][τ] = s[τ][σ ◾ τ] + +namespace Subst + export SubstMapStable (apply_stable) + export SubstMapRenComposeLeft (apply_ren_compose_left) + export SubstMapRenComposeRight (apply_ren_compose_right) + export SubstMapRenCommute (apply_ren_commute) +end Subst + +@[grind <-] +theorem Ren.lift_eq_from_eq [RenMap T T] {r : Ren T} {σ : Subst T} + : r.to = σ -> r.to.lift = σ.lift +:= by intro h; rw [<-h] + +namespace Subst + section + @[simp, grind =] + theorem rewrite1 : re 0 :: +1 = id T := by + simp [Subst.cons, Subst.id] + funext; case _ x => + cases x; all_goals simp + + open SubstMap + + @[simp, grind =] + theorem I_lift [RenMap T T] {k} : +0.lift k = id T := by + funext; case _ x => + cases x; all_goals (simp [Subst.lift, Subst.id]) + grind + + @[simp, grind =] + theorem rewrite2 [SubstMap T T] {σ : Subst T} : +0 ∘ σ = σ := by + funext; case _ x => + unfold Subst.compose; simp [Subst.id] + + @[simp, grind =] + theorem rewrite3_replace [SubstMap T T] {σ τ : Subst T} {s : T} + : (su s :: σ) ∘ τ = su s[τ] :: (σ ∘ τ) + := by + simp [Subst.cons, Subst.compose] + funext; case _ x => + cases x; all_goals simp + + @[simp, grind =] + theorem rewrite3_rename [SubstMap T T] {s} {σ τ : Subst T} + : (re s :: σ) ∘ τ = (τ.act s) :: (σ ∘ τ) + := by + simp [Subst.cons, Subst.compose] + funext; case _ x => + cases x; all_goals simp + + @[simp, grind =] + theorem rewrite4 [SubstMap T T] {s} {σ : Subst T} : +1 ∘ (s :: σ) = σ := by + simp [Subst.cons] + funext; case _ x => + cases x; all_goals (simp [Subst.compose, Subst.succ]) + + @[simp, grind =] + theorem rewrite5 [SubstMap T T] {σ : Subst T} : σ.act 0 :: (+1 ∘ σ) = σ := by + simp [Subst.cons, Subst.compose]; congr + funext; case _ x => + cases x <;> simp + end + + @[simp, grind =] + theorem apply_I_is_id [SubstMap S T] [SubstMapId S T] {s : S} + : s[id T] = s + := SubstMapId.apply_id + + @[simp, grind =] + theorem rewrite_lift [RenMap T T] [SubstMap T T] [SubstMapStable T T] {σ : Subst T} + : σ.lift = re 0 :: (σ ∘ +1) + := by + simp [Subst.cons, Subst.lift, Subst.compose] + funext; case _ x => + cases x; simp + case _ n => + simp [Subst.succ] + generalize tdef : σ.act n = t + cases t <;> simp at * + case _ y => + rw [apply_stable (σ := +1)] + simp [Subst.succ] + rw [Ren.to_succ] + + @[simp, grind =] + theorem rewrite_lift_zero [RenMap T T] [RenMapId T T] {σ : Subst T} + : σ.lift 0 = σ + := by simp [Subst.lift] + + @[grind =] + theorem rewrite_lift_succ + [RenMap T T] [RenMapId T T] [RenMapCompose T T] + {k} {σ : Subst T} + : σ.lift (k + 1) = (σ.lift k).lift + := by + induction k; simp + case _ n ih => + replace ih i : (σ.lift (n + 1)).act i = ((σ.lift n).lift 1).act i := by rw [ih] + simp [Subst.lift] + funext; case _ i => + have lem := ih i + cases i <;> simp + case _ i => + simp [Subst.lift] at lem + split; simp; case _ h1 => + simp at h1 + have lem2 : n ≤ i := by omega + generalize zdef : σ.act (i - (n + 1)) = z + cases z <;> simp; omega + congr + + @[simp, grind =] + theorem rewrite6 [RenMap T T] [SubstMap T T] [SubstMapId T T] {σ : Subst T} + : σ ∘ +0 = σ + := by + simp [Subst.compose, Subst.id]; congr + funext; case _ x => + generalize zdef : σ.act x = z + cases z <;> simp at *; case _ s => + have lem := SubstMapId.apply_id (T := T) (s := s) + simp [Subst.id] at lem; exact lem + + @[simp, grind =] + theorem apply_compose [SubstMap S T] [SubstMap T T] [SubstMapCompose S T] {s : S} {σ τ : Subst T} + : s[σ][τ] = s[σ ∘ τ] + := SubstMapCompose.apply_compose + + @[simp, grind =] + theorem rewrite7 + [SubstMap T T] [SubstMapCompose T T] + {σ τ μ : Subst T} + : (σ ∘ τ) ∘ μ = σ ∘ τ ∘ μ + := by + simp [Subst.compose] + funext; case _ x => + cases σ.act x <;> simp [Subst.compose] + + @[simp, grind =] + theorem hrewrite1 [SubstMap S T] [SubstMapId S T] {σ : Subst S} : σ ◾ (id T) = σ := by + simp [Subst.hcompose]; congr + funext; case _ x => + generalize zdef : σ.act x = z + cases z <;> simp + + -- @[simp, grind =] + -- theorem hcomp_ren_left + -- [RenMap S] [RenMap T] [SubstMap S T] + -- (r : Ren) (σ : Subst T) + -- : (@Ren.to S r) ◾ σ = r.to + -- := by + -- funext; case _ x => + -- induction x <;> simp [Subst.hcompose, Ren.to] + + @[simp, grind =] + theorem hrewrite2 [SubstMap S T] {σ : Subst T} : (id S) ◾ σ = +0 := by simp [hcompose, id] + + @[simp, grind =] + theorem hrewrite3 [SubstMap S T] {σ : Subst T} : (succ S) ◾ σ = +1 := by simp [hcompose, succ] + + @[simp, grind =] + theorem hrewrite4 + [SubstMap S T] + {x} {σ : Subst S} {τ : Subst T} + : (re x :: σ) ◾ τ = re x :: (σ ◾ τ) + := by + simp [Subst.hcompose]; congr + funext; case _ i => + cases i <;> simp [Subst.cons] + + @[grind =] + theorem hcomp_dist_ren_left + [SubstMap S T] + (r : Ren S) {σ : Subst S} {τ : Subst T} + : (r ∘ σ) ◾ τ = r ∘ σ ◾ τ + := by + funext; case _ x => + simp [hcompose, compose_ren_left] + + @[simp, grind =] + theorem hrewrite5 + [SubstMap S T] [SubstMap T T] [SubstMapCompose S T] + {σ : Subst S} {τ μ : Subst T} + : (σ ◾ τ) ◾ μ = σ ◾ (τ ∘ μ) + := by + simp [Subst.hcompose] + funext; case _ x => + generalize zdef : σ.act x = z + cases z <;> simp + + @[grind =] + theorem hcomp_distr_ren_right + [RenMap S S] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] + (r : Ren S) (σ : Subst S) (μ : Subst T) + : (σ ∘ r) ◾ μ = (σ ◾ μ) ∘ r + := by + simp [hcompose, compose_ren_right]; funext; case _ x => + generalize zdef : σ.act x = z + cases z <;> simp + rw [apply_ren_commute] + + @[simp, grind =] + theorem apply_hcompose + [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] + {s : S} {σ : Subst S} {τ : Subst T} + : s[σ][τ] = s[τ][σ ◾ τ] + := by exact SubstMapHetCompose.apply_hcompose + + @[simp, grind =] + theorem hrewrite7 + [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] + {σ τ : Subst S} (μ : Subst T) + : (σ ∘ τ) ◾ μ = (σ ◾ μ) ∘ τ ◾ μ + := by + simp [Subst.hcompose, Subst.compose] + funext; case _ x => + generalize zdef : σ.act x = z + cases z <;> simp [Subst.hcompose] + + theorem hrewrite_lift1 + [RenMap S S] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] [SubstMapRenCommute S T] + {σ : Subst S} {τ : Subst T} + : (σ ◾ τ).lift = σ.lift ◾ τ + := by + simp [Subst.lift]; congr; funext; case _ i => + cases i <;> simp + case _ n => + generalize zdef : σ.act n = z + cases z <;> simp; case _ t => + rw [SubstMapRenCommute.apply_ren_commute] + + @[simp, grind =] + theorem hrewrite_lift + [RenMap S S] [SubstMap S S] [SubstMap S T] [RenMapId S S] [RenMapCompose S S] + [SubstMapHetCompose S T] [SubstMapRenCommute S T] + {k} {σ : Subst S} {τ : Subst T} + : (σ ◾ τ).lift k = σ.lift k ◾ τ + := by + induction k generalizing σ τ + case _ => simp + case _ i ih => + rw [rewrite_lift_succ] + rw [rewrite_lift_succ] + simp; rw [ih, hrewrite_lift1] + grind +end Subst + +@[grind =] +theorem Subst.compose_commute_succ [RenMap T T] {τ : Subst T} + : τ ∘ Ren.succ T = Ren.succ T ∘ τ.lift +:= by congr + +@[grind =] +theorem Ren.compose_commute_succ {r : Ren T} : r ∘ succ T = succ T ∘ r.lift := by simp [compose] + +theorem Subst.rewrite_lift_compose_ren_left_k1 [RenMap T T] {r : Ren T} {τ : Subst T} + : (r ∘ τ).lift = r.lift ∘ τ.lift +:= by + simp [compose_ren_left, lift, Ren.lift] + funext; case _ x => + cases x <;> simp + +@[simp, grind =] +theorem Subst.rewrite_lift_compose_ren_left + [RenMap T T] [RenMapId T T] [RenMapCompose T T] + {k} {r : Ren T} {τ : Subst T} + : (r ∘ τ).lift k = r.lift k ∘ τ.lift k +:= by + induction k generalizing r τ; congr + case _ k ih => + rw [rewrite_lift_succ, ih] + rw [rewrite_lift_compose_ren_left_k1] + rw [<-rewrite_lift_succ] + rw [<-Ren.lift_of_succ] + +theorem Subst.lift_compose_ren_right_k1 + [RenMap T T] [RenMapId T T] [RenMapCompose T T] + {σ : Subst T} {r : Ren T} + : (σ ∘ r).lift = σ.lift ∘ r.lift +:= by + simp [lift]; congr; funext; case _ x => + cases x <;> simp; case _ x => + grind + +@[simp, grind =] +theorem Subst.lift_compose_ren_right + [RenMap T T] [RenMapId T T] [RenMapCompose T T] + {k} {σ : Subst T} {r : Ren T} + : (σ ∘ r).lift k = σ.lift k ∘ r.lift k +:= by + induction k generalizing σ r; simp + case _ k ih => + rw [rewrite_lift_succ, ih] + rw [lift_compose_ren_right_k1] + rw [<-rewrite_lift_succ] + rw [<-Ren.lift_of_succ] + +theorem Subst.rewrite_lift_compose_k1 + [RenMap T T] [SubstMap T T] [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T] + {σ τ : Subst T} + : (σ ∘ τ).lift = σ.lift ∘ τ.lift +:= by + simp [compose, lift] + funext; case _ x => + cases x <;> simp + case _ x => + cases σ.act x <;> simp; case _ t => + rw [SubstMapRenComposeLeft.apply_ren_compose_left] + rw [SubstMapRenComposeRight.apply_ren_compose_right] + have lem := Subst.compose_commute_succ (τ := τ) + simp [lift] at lem + rw [lem] + +@[simp, grind =] +theorem Subst.rewrite_lift_compose + [RenMap T T] [RenMapId T T] [RenMapCompose T T] [SubstMap T T] + [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T] + {k} {σ τ : Subst T} + : (σ ∘ τ).lift k = σ.lift k ∘ τ.lift k +:= by + induction k generalizing σ τ; simp + case _ k ih => + rw [rewrite_lift_succ, ih] + rw [rewrite_lift_succ (σ := σ)] + rw [rewrite_lift_succ (σ := τ)] + rw [rewrite_lift_compose_k1] + +macro "subst_solve_id" : tactic => `(tactic| { + intro t; induction t + any_goals solve | simp +instances [*] + all_goals try simp at *; simp +instances [*]; grind +}) + +macro "subst_solve_stable" : tactic => `(tactic| { + intro r σ h + funext; case _ t => + induction t generalizing r σ + all_goals simp [rmap, smap, *] at *; try simp +instances [*] + any_goals solve | (rw [<-h]; simp +instances [Ren.to]) + all_goals try repeat funext; grind +}) + +macro "subst_solve_compose" : tactic => `(tactic| { + intro s σ τ + induction s generalizing σ τ + any_goals solve | simp +instances [*] + try any_goals solve | ( + try simp [-Subst.rewrite_lift, *] + try funext; case _ x => + try rw [<-Ren.to_lift] + try simp [-Subst.rewrite_lift, *] + try grind) +}) + +end LeanSubst diff --git a/LeanSubst/Lemma/Ren.lean b/LeanSubst/Lemma/Ren.lean deleted file mode 100644 index 8a39fb1..0000000 --- a/LeanSubst/Lemma/Ren.lean +++ /dev/null @@ -1,24 +0,0 @@ - -import LeanSubst.Ops - -namespace LeanSubst - -universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} - -class RenMapId (S : Type u1) [RenMap S] where - apply_id {t : S} : t⟨Ren.id⟩ = t - -class RenMapCompose (S : Type u1) [RenMap S] where - apply_compose {s : S} {r1 r2 : Ren} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩ - -@[simp] -theorem Ren.apply_id [RenMap T] [RenMapId T] {t : T} : t⟨id⟩ = t := RenMapId.apply_id - -@[simp, grind =] -theorem Ren.apply_compose [RenMap T] [RenMapCompose T] {t : T} {r1 r2 : Ren} - : t⟨r1⟩⟨r2⟩ = t⟨r1 ∘ r2⟩ -:= RenMapCompose.apply_compose - - -end LeanSubst diff --git a/LeanSubst/Old/HetRen.lean b/LeanSubst/Old/HetRen.lean deleted file mode 100644 index 40fa887..0000000 --- a/LeanSubst/Old/HetRen.lean +++ /dev/null @@ -1,123 +0,0 @@ -import LeanSubst.Ren - -namespace LeanSubst - universe u - variable {S T : Type} - - structure HetRen (T : Type) where - act : Nat -> Nat - - def HetRen.id T : HetRen T := ⟨λ x => x⟩ - - def HetRen.add T (k : Nat) : HetRen T := ⟨(· + k)⟩ - - def HetRen.sub T (k : Nat) : HetRen T := ⟨(· - k)⟩ - - def HetRen.lift (r : HetRen T) (k : Nat := 1) : HetRen T := .mk λ n => - if n < k then n else r.act (n - k) + k - - def HetRen.cons (a : Nat) (r : HetRen T) : HetRen T := .mk λ n => - match n with - | 0 => a - | n + 1 => r.act n - - def HetRen.append : List Nat -> HetRen T -> HetRen T - | .nil, r => r - | .cons hd tl, r => append tl (r.cons hd) - - instance : HAppend (List Nat) (HetRen T) (HetRen T) where - hAppend := HetRen.append - - def HetRen.compose : HetRen T -> HetRen T -> HetRen T - | r1, r2 => .mk λ n => r2.act (r1.act n) - - def Ren.het T (r : Ren) : HetRen T := ⟨r.act⟩ - - @[simp] - theorem Ren.het_action {T i} {r : Ren} : (r.het T).act i = r.act i := by simp [Ren.het] - - class HetRenMap (S T : Type) where - hrmap : HetRen T -> S -> S - - export HetRenMap (hrmap) - - macro:max t:term noWs "⟨" r:term "⟩" : term => `(hrmap $r $t) - infixr:67 (name := HetRen.cons_notation) " :: " => HetRen.cons - infixr:85 (name := HetRen.compose_notation) " ∘ " => HetRen.compose - - @[app_unexpander hrmap] - def unexpandHetRenApply : Lean.PrettyPrinter.Unexpander - | `($_ $r $t) => `($t⟨$r⟩) - | _ => throw () - - @[simp, grind =] - theorem HetRen.lift_zero {r : HetRen T} : r.lift 0 = r := by - unfold HetRen.lift; congr - - @[grind =] - theorem HetRen.lift_succ {r : HetRen T} {k} : r.lift (k + 1) = (r.lift k).lift := by - induction k; simp - case _ n ih => - unfold HetRen.lift; congr; funext; case _ i => - simp; unfold HetRen.lift at ih; simp at ih - grind - - @[simp] - theorem HetRen.id_action {x} : (HetRen.id T).act x = x := by simp [HetRen.id] - - @[simp] - theorem HetRen.lift_id {k} : HetRen.lift (HetRen.id T) k = HetRen.id T := by - simp [HetRen.id, HetRen.lift]; congr; funext; case _ x => - cases x <;> simp; omega - - @[simp] - theorem HetRen.cons_head_action {n} {r : HetRen T} : (n::r).act 0 = n := by simp [HetRen.cons] - - @[simp] - theorem HetRen.cons_tail_action {n i} {r : HetRen T} : (n::r).act (i + 1) = r.act i := by simp [HetRen.cons] - - @[simp] - theorem HetRen.compose_id_left {r : HetRen T} : (id T) ∘ r = r := by - simp [HetRen.compose, HetRen.id] - - @[simp] - theorem HetRen.compose_id_right {r : HetRen T} : r ∘ (id T) = r := by - simp [HetRen.compose, HetRen.id] - - @[simp] - theorem HetRen.compose_assoc {r1 r2 r3 : HetRen T} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by - simp [HetRen.compose] - - @[simp] - theorem HetRen.compose_action {r1 r2 : HetRen T} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by - simp [HetRen.compose] - - theorem HetRen.compose_lift_k1 {r1 r2 : HetRen T} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by - simp [HetRen.compose, HetRen.lift] - funext; case _ x => - cases x <;> simp - - @[simp] - theorem HetRen.compose_lift {k} {r1 r2 : HetRen T} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by - induction k generalizing r1 r2; simp - case _ k ih => - rw [lift_succ, ih] - rw [lift_succ (r := r1)] - rw [lift_succ (r := r2)] - rw [compose_lift_k1] - - class HetRenMapId (S T : Type) [HetRenMap S T] where - apply_id {t : S} : t⟨HetRen.id T⟩ = t - - class HetRenMapCompose (S T : Type) [HetRenMap S T] where - apply_compose {s : S} {r1 r2 : HetRen T} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩ - - @[simp, grind =] - theorem HetRen.apply_id [HetRenMap S T] [HetRenMapId S T] {t : S} : t⟨id T⟩ = t := HetRenMapId.apply_id - - @[simp, grind =] - theorem HetRen.apply_compose [HetRenMap S T] [HetRenMapCompose S T] {t : S} {r1 r2 : HetRen T} - : t⟨r1⟩⟨r2⟩ = t⟨r1 ∘ r2⟩ - := HetRenMapCompose.apply_compose - -end LeanSubst diff --git a/LeanSubst/Old/Laws.lean b/LeanSubst/Old/Laws.lean deleted file mode 100644 index 2c87803..0000000 --- a/LeanSubst/Old/Laws.lean +++ /dev/null @@ -1,566 +0,0 @@ -import LeanSubst.Ren -import LeanSubst.Subst - -namespace LeanSubst - universe u - variable {S T : Type} - - class SubstMapId (S T : Type) [RenMap T] [SubstMap S T] where - apply_id {t : S} : t[+0:T] = t - - class SubstMapStable (S : Type) [RenMap S] [SubstMap S S] where - apply_stable (r : Ren) (σ : Subst S) : r = σ -> rmap (T := S) r = smap σ - - class SubstMapRenCommute (S T : Type) [RenMap S] [RenMap T] [SubstMap S T] where - apply_ren_commute {s : S} (r : Ren) (τ : Subst T) : s⟨r⟩[τ:T] = s[τ:T]⟨r⟩ - - class SubstMapRenComposeLeft (S T : Type) [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] where - apply_ren_compose_left {s : S} {r : Ren} {τ : Subst T} : s[r.to:T][τ:_] = s[r.to ∘ τ:T] - - class SubstMapRenComposeRight (S T : Type) [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] where - apply_ren_compose_right {s : S} {r : Ren} {σ : Subst T} : s[σ:_][r.to:T] = s[σ ∘ r.to:T] - - class SubstMapCompose (S T : Type) [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] where - apply_compose {s : S} {σ τ : Subst T} : s[σ:T][τ:_] = s[σ ∘ τ:T] - - class SubstMapHetCompose (S T : Type) [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] where - apply_hcompose {s : S} {σ : Subst S} {τ : Subst T} : s[σ][τ:T] = s[τ:T][σ ◾ τ] - - namespace Subst - export SubstMapStable (apply_stable) - export SubstMapRenCommute (apply_ren_commute) - export SubstMapRenComposeLeft (apply_ren_compose_left) - export SubstMapRenComposeRight (apply_ren_compose_right) - end Subst - - theorem Ren.lift_eq_from_eq [RenMap T] [SubstMap S T] {r : Ren} {σ : Subst T} - : r = σ -> r.lift = σ.lift - := by intro h; rw [<-h, to_lift] - - namespace Subst - section - @[simp, grind =] - theorem rewrite1 : re 0 :: +1 = +0@T := by - simp [Subst.cons, Subst.id] - funext; case _ x => - cases x; all_goals simp - - open SubstMap - variable [RenMap T] - - @[simp, grind =] - theorem I_lift {k} : +0.lift k = +0@T := by - funext; case _ x => - cases x; all_goals (simp [Subst.lift, Subst.id]) - grind - - @[simp, grind =] - theorem rewrite2 [SubstMap T T] {σ : Subst T} : +0 ∘ σ = σ := by - funext; case _ x => - unfold Subst.compose; simp [Subst.id] - - @[simp, grind =] - theorem rewrite3_replace [SubstMap T T] {σ τ : Subst T} {s : T} - : (su s :: σ) ∘ τ = su s[τ] :: (σ ∘ τ) - := by - simp [Subst.cons, Subst.compose] - funext; case _ x => - cases x; all_goals simp - - @[simp, grind =] - theorem rewrite3_rename [SubstMap T T] {s} {σ τ : Subst T} - : (re s :: σ) ∘ τ = (τ.act s) :: (σ ∘ τ) - := by - simp [Subst.cons, Subst.compose] - funext; case _ x => - cases x; all_goals simp - - @[simp, grind =] - theorem rewrite4 [SubstMap T T] {s} {σ : Subst T} : +1 ∘ (s :: σ) = σ := by - simp [Subst.cons] - funext; case _ x => - cases x; all_goals (simp [Subst.compose, Subst.succ]) - - @[simp, grind =] - theorem rewrite5 [SubstMap T T] {σ : Subst T} : σ.act 0 :: (+1 ∘ σ) = σ := by - simp [Subst.cons, Subst.compose]; congr - funext; case _ x => - cases x <;> simp - end - - @[simp, grind =] - theorem apply_I_is_id [RenMap T] [SubstMap S T] [SubstMapId S T] {s : S} - : s[+0:T] = s - := SubstMapId.apply_id - - @[simp, grind =] - theorem rewrite_lift [RenMap T] [SubstMap T T] [SubstMapStable T] {σ : Subst T} - : σ.lift = re 0 :: (σ ∘ +1) - := by - simp [Subst.cons, Subst.lift, Subst.compose] - funext; case _ x => - cases x; simp - case _ n => - simp [Subst.succ] - generalize tdef : σ.act n = t - cases t <;> simp at * - case _ y => - rw [apply_stable (σ := +1)] - simp [Subst.succ] - rw [Ren.to_succ] - - @[simp, grind =] - theorem rewrite_lift_zero [RenMap S] [RenMapId S] {σ : Subst S} - : σ.lift 0 = σ - := by - simp [Subst.lift]; congr; funext; case _ i => - generalize zdef : σ.act i = z - cases z <;> simp [Ren.add]; case _ s => - have lem := RenMapId.apply_id (t := s) - simp [Ren.id] at lem; exact lem - - @[grind =] - theorem rewrite_lift_succ - [RenMap S] [RenMapId S] [RenMapCompose S] - {k} {σ : Subst S} - : σ.lift (k + 1) = (σ.lift k).lift - := by - induction k; simp - case _ n ih => - replace ih i : (σ.lift (n + 1)).act i = ((σ.lift n).lift 1).act i := by rw [ih] - simp [Subst.lift] - funext; case _ i => - have lem := ih i - cases i <;> simp - case _ i => - simp [Subst.lift] at lem - split; simp; case _ h1 => - simp at h1 - have lem2 : n ≤ i := by omega - generalize zdef : σ.act (i - (n + 1)) = z - cases z <;> simp; omega - congr - - @[simp, grind =] - theorem rewrite6 [RenMap T] [SubstMap T T] [SubstMapId T T] {σ : Subst T} - : σ ∘ +0 = σ - := by - simp [Subst.compose, Subst.id]; congr - funext; case _ x => - generalize zdef : σ.act x = z - cases z <;> simp at *; case _ s => - have lem := SubstMapId.apply_id (T := T) (t := s) - simp [Subst.id] at lem; exact lem - - @[simp, grind =] - theorem apply_compose - [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] - {s : S} {σ τ : Subst T} - : s[σ:T][τ:_] = s[σ ∘ τ:T] - := SubstMapCompose.apply_compose - - @[simp, grind =] - theorem rewrite7 - [RenMap T] [SubstMap T T] [SubstMapCompose T T] - {σ τ μ : Subst T} - : (σ ∘ τ) ∘ μ = σ ∘ τ ∘ μ - := by - simp [Subst.compose] - funext; case _ x => - cases σ.act x <;> simp [Subst.compose] - - @[simp, grind =] - theorem hrewrite1 - [RenMap T] [SubstMap S T] [SubstMapId S T] - {σ : Subst S} - : σ ◾ (+0@T) = σ - := by - simp [Subst.hcompose]; congr - funext; case _ x => - generalize zdef : σ.act x = z - cases z <;> simp - - @[simp, grind =] - theorem hcomp_ren_left - [RenMap S] [RenMap T] [SubstMap S T] - (r : Ren) (σ : Subst T) - : (@Ren.to S r) ◾ σ = r.to - := by - funext; case _ x => - induction x <;> simp [Subst.hcompose, Ren.to] - - @[simp, grind =] - theorem hrewrite2 - [RenMap S] [RenMap T] [SubstMap S T] - {σ : Subst T} - : (+0@S) ◾ σ = +0 - := by - apply hcomp_ren_left (S := S) (T := T) Ren.id σ - - @[simp, grind =] - theorem hrewrite3 - [RenMap S] [RenMap T] [SubstMap S T] - {σ : Subst T} - : (+1@S) ◾ σ = +1 - := by - have lem := hcomp_ren_left (S := S) (T := T) (Ren.add 1) σ - simp at lem; exact lem - - @[simp, grind =] - theorem hrewrite4 - [RenMap T] [SubstMap S T] - {x} {σ : Subst S} {τ : Subst T} - : (re x :: σ) ◾ τ = re x :: (σ ◾ τ) - := by - simp [Subst.hcompose]; congr - funext; case _ i => - cases i <;> simp [Subst.cons] - - @[grind =] - theorem hcomp_dist_ren_left - [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] - (r : Ren) {σ : Subst S} {τ : Subst T} - : (r.to ∘ σ) ◾ τ = r.to ∘ σ ◾ τ - := by - funext; case _ x => - simp [Subst.hcompose, Subst.compose, Ren.to] - - @[simp, grind =] - theorem hrewrite5 - [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] - {σ : Subst S} {τ μ : Subst T} - : (σ ◾ τ) ◾ μ = σ ◾ (τ ∘ μ) - := by - simp [Subst.hcompose] - funext; case _ x => - generalize zdef : σ.act x = z - cases z <;> simp - - @[grind =] - theorem hcomp_distr_ren_right - [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] - [SubstMapStable S] [SubstMapRenCommute S T] - (r : Ren) (σ : Subst S) (μ : Subst T) - : (σ ∘ r.to) ◾ μ = (σ ◾ μ) ∘ r.to - := by - simp [Subst.hcompose, Subst.compose, Ren.to] - funext; case _ x => - generalize zdef : σ.act x = z - cases z <;> simp - rw [<-apply_stable r ⟨λ n => re (r.act n)⟩ rfl] - rw [SubstMapRenCommute.apply_ren_commute r μ] - - @[grind =] - theorem hcomp_distr_ren_right_p1 - [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] - [SubstMapStable S] [SubstMapRenCommute S T] - (σ : Subst S) (μ : Subst T) - : (σ ∘ +1) ◾ μ = (σ ◾ μ) ∘ +1 - := by - have lem : @Subst.succ S = Ren.to (Ren.add 1) := by simp - rw [lem, hcomp_distr_ren_right] - - @[simp, grind =] - theorem hrewrite6 - [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] - [SubstMapStable S] [SubstMapRenCommute S T] - (r : Ren) (σ : Subst S) - : (σ ∘ r.to) ◾ (+1@T) = (σ ◾ +1@T) ∘ r.to - := by - have lem := hcomp_distr_ren_right (T := T) r σ +1 - simp at lem; exact lem - - @[simp, grind =] - theorem apply_hcompose - [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] - {s : S} {σ : Subst S} {τ : Subst T} - : s[σ][τ:T] = s[τ:T][σ ◾ τ] - := by exact SubstMapHetCompose.apply_hcompose - - @[simp, grind =] - theorem hrewrite7 - [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] - {σ τ : Subst S} (μ : Subst T) - : (σ ∘ τ) ◾ μ = (σ ◾ μ) ∘ τ ◾ μ - := by - simp [Subst.hcompose, Subst.compose] - funext; case _ x => - generalize zdef : σ.act x = z - cases z <;> simp [Subst.hcompose] - - theorem hrewrite_lift1 - [RenMap S] [RenMap T] [SubstMap S T] [SubstMapRenCommute S T] - {σ : Subst S} {τ : Subst T} - : (σ ◾ τ).lift = σ.lift ◾ τ - := by - simp [Subst.lift]; congr; funext; case _ i => - cases i <;> simp [hcompose] - case _ n => - generalize zdef : σ.act n = z - cases z <;> simp; case _ t => - rw [SubstMapRenCommute.apply_ren_commute] - - @[simp, grind =] - theorem hrewrite_lift - [RenMap S] [RenMap T] [SubstMap S T] [RenMapId S] [RenMapCompose S] [SubstMapRenCommute S T] - {k} {σ : Subst S} {τ : Subst T} - : (σ ◾ τ).lift k = σ.lift k ◾ τ - := by - induction k generalizing σ τ - case _ => simp - case _ i ih => - rw [rewrite_lift_succ] - rw [rewrite_lift_succ] - simp; rw [ih, hrewrite_lift1] - grind - end Subst - - @[grind =] - theorem Subst.Compose.lemma1 - [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] [SubstMapStable S] - {k} {τ : Subst S} - : (Ren.to (Ren.add 1)) ∘ τ.lift (k + 1) = τ.lift k ∘ (Ren.to (Ren.add 1)) - := by - simp [Subst.compose] - funext; case _ x => - cases x - all_goals - unfold Subst.lift; simp - split; simp; split - any_goals solve | congr 1 - all_goals - rw [<-apply_stable _ +1 rfl] - simp; congr - - @[grind =] - theorem Subst.Compose.lemma1s - [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] [SubstMapStable S] - {k} {τ : Subst S} - : +1 ∘ τ.lift (k + 1) = τ.lift k ∘ +1 - := by - have lem : @Subst.succ S = Ren.to (Ren.add 1) := by simp - rw [lem]; grind - - @[grind =] - theorem Subst.Compose.lemma2_k1 - [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] - {σ : Subst S} {r : Ren} - : (r ∘ σ).lift = (Ren.to r).lift ∘ σ.lift - := by - simp [Subst.lift, Subst.compose, Ren.to] - funext; case _ x => - cases x <;> simp - - @[grind =] - theorem Subst.Compose.lemma2 - [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] - {k} {σ : Subst S} {r : Ren} - : (r ∘ σ).lift k = (Ren.to r).lift k ∘ σ.lift k - := by - induction k generalizing r σ; simp - case _ k ih => - rw [Subst.rewrite_lift_succ, ih] - rw [<-Ren.to_lift, Subst.Compose.lemma2_k1] - rw [Subst.rewrite_lift_succ (σ := r.to)] - rw [Subst.rewrite_lift_succ (σ := σ)] - grind - - @[grind =] - theorem Subst.Compose.lemma2s - [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] - {k} {σ : Subst S} - : (+1 ∘ σ).lift k = +1.lift k ∘ σ.lift k - := by - have lem : @Subst.succ S = Ren.to (Ren.add 1) := by simp - rw [lem]; grind - - @[grind =] - theorem Subst.Compose.lemma3 - [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapRenComposeLeft S T] - {s : S} {σ : Subst T} - : s[+1:T][σ:_] = s[+1 ∘ σ:_] - := by - have lem : @Subst.succ T = Ren.to (Ren.add 1) := by simp - rw [lem, apply_ren_compose_left] - - @[grind =] - theorem Subst.Compose.lemma4 - [RenMap T] [SubstMap T T] - {σ τ : Subst T} - : +1 ∘ τ ∘ σ = (+1 ∘ τ) ∘ σ - := by - funext; case _ x => - cases x <;> simp [Subst.compose, Subst.succ] - - @[grind =] - theorem Subst.compose.lemma5 - [RenMap T] [SubstMap T T] [RenMapCompose T] [SubstMapStable T] - {r1 r2 : Ren} {τ : Subst T} - : (τ ∘ r2.to) ∘ r1.to = τ ∘ r2.to ∘ r1.to - := by - simp [Subst.compose] - funext; case _ x => - cases τ.act x <;> simp [*] - simp [Ren.to] - rw [<-apply_stable r2 ⟨λ n => re (r2.act n)⟩ rfl] - rw [<-apply_stable r1 ⟨λ n => re (r1.act n)⟩ rfl] - simp - rw [apply_stable _ _ rfl] - rw [Ren.to_compose] - unfold Subst.compose; simp [Ren.to] - - @[grind =] - theorem Subst.Compose.lemma6_k1 - [RenMap S] [SubstMap S S] [SubstMapStable S] [SubstMapRenComposeLeft S S] - {σ : Subst S} {r : Ren} - : (σ ∘ r.to).lift = σ.lift ∘ (Ren.to r).lift - := by - simp [Subst.lift, Subst.compose] - funext; case _ x => - cases x <;> simp - case _ x => - cases σ.act x <;> simp - rw [apply_stable (Ren.add 1) _ rfl] - rw [apply_ren_compose_left] - rw [apply_ren_compose_left] - simp [Ren.to, Subst.compose, Ren.add] - - @[grind =] - theorem Subst.Compose.lemma6 - [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] - [SubstMapStable S] [SubstMapRenComposeLeft S S] - {k} {σ : Subst S} {r : Ren} - : (σ ∘ r.to).lift k = σ.lift k ∘ (Ren.to r).lift k - := by - induction k generalizing r σ; simp - case _ k ih => - rw [Subst.rewrite_lift_succ, ih] - rw [<-Ren.to_lift, Subst.Compose.lemma6_k1] - rw [Subst.rewrite_lift_succ (σ := r.to)] - rw [Subst.rewrite_lift_succ (σ := σ)] - grind - - @[grind =] - theorem Subst.Compose.lemma6s - [RenMap S] [SubstMap S S] [RenMapId S] [RenMapCompose S] - [SubstMapStable S] [SubstMapRenComposeLeft S S] - {k} {σ : Subst S} - : (σ ∘ +1).lift k = σ.lift k ∘ +1.lift k - := by - have lem : @Subst.succ S = Ren.to (Ren.add 1) := by simp - rw [lem]; grind - - @[grind =] - theorem Subst.Compose.lemma7 - [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapRenComposeRight S T] - {s : S} {τ : Subst T} - : s[τ:_][+1:T] = s[τ ∘ +1:_] - := by - have lem : @Subst.succ T = Ren.to (Ren.add 1) := by simp - rw [lem, apply_ren_compose_right] - - @[grind =] - theorem Subst.Compose.lemma8 - [RenMap T] [SubstMap T T] [SubstMapRenComposeLeft T T] - {σ τ : Subst T} - : (σ ∘ +1) ∘ τ = σ ∘ +1 ∘ τ - := by - simp [Subst.compose] - funext; case _ x => - cases σ.act x <;> simp at * - rw [lemma3] - unfold Subst.compose; simp - - @[grind =] - theorem Subst.Compose.lemma9 - [RenMap T] [SubstMap T T] [SubstMapRenComposeRight T T] - {σ τ : Subst T} - : ((σ ∘ τ) ∘ +1) = σ ∘ τ ∘ +1 - := by - simp [Subst.compose] - funext; case _ x => - cases σ.act x <;> simp at * - rw [lemma7] - unfold Subst.compose; simp - - @[grind =] - theorem Subst.Compose.lemma10 - [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] - [SubstMapStable S] [SubstMapRenCommute S T] - {σ : Subst S} {μ : Subst T} {r : Ren} - : (σ ∘ r.to) ◾ μ = (σ ◾ μ) ∘ r.to - := by - simp [Subst.hcompose, Subst.compose] - funext; case _ x => - generalize zdef : σ.act x = z - cases z <;> simp [Ren.to] - rw [<-apply_stable r ⟨λ n => re (r.act n)⟩ rfl] - rw [Subst.apply_ren_commute] - - @[grind =] - theorem Subst.Compose.lemma10s - [RenMap S] [RenMap T] [SubstMap S S] [SubstMap S T] - [SubstMapStable S] [SubstMapRenCommute S T] - {σ : Subst S} {μ : Subst T} - : (σ ∘ +1) ◾ μ = (σ ◾ μ) ∘ +1 - := by - have lem := lemma10 (σ := σ) (μ := μ) (r := (Ren.add 1)) - simp at lem; exact lem - - theorem Subst.rewrite_lift_compose_k1 - [RenMap T] [SubstMap T T] [SubstMapStable T] - [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T T] - {σ τ : Subst T} - : (σ ∘ τ).lift = σ.lift ∘ τ.lift - := by - simp [Subst.lift, Subst.compose] - funext; case _ x => - cases x <;> simp - case _ x => - cases σ.act x <;> simp - rw [apply_stable _ (Ren.add 1) rfl]; simp - rw [Compose.lemma7, Compose.lemma3] - simp [Subst.compose] - - @[simp, grind =] - theorem Subst.rewrite_lift_compose - [RenMap T] [SubstMap T T] [RenMapId T] [RenMapCompose T] [SubstMapStable T] - [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T T] - {k} {σ τ : Subst T} - : (σ ∘ τ).lift k = σ.lift k ∘ τ.lift k - := by - induction k generalizing σ τ; simp - case _ k ih => - rw [rewrite_lift_succ, ih] - rw [rewrite_lift_succ (σ := σ)] - rw [rewrite_lift_succ (σ := τ)] - rw [rewrite_lift_compose_k1] - - macro "subst_solve_id" : tactic => `(tactic| { - intro t; induction t - any_goals solve | simp +instances [*] - all_goals try simp at *; simp +instances [*]; grind - }) - - macro "subst_solve_stable" : tactic => `(tactic| { - intro r σ h - funext; case _ t => - induction t generalizing r σ - all_goals simp [rmap, smap, *] at *; try simp +instances [*] - any_goals solve | (rw [<-h]; simp +instances [Ren.to]) - all_goals try repeat funext; grind - }) - - macro "subst_solve_compose" : tactic => `(tactic| { - intro s σ τ - induction s generalizing σ τ - any_goals solve | simp +instances [*] - try any_goals solve | ( - try simp [-Subst.rewrite_lift, *] - try funext; case _ x => - try rw [<-Ren.to_lift] - try simp [-Subst.rewrite_lift, *] - try grind) - }) - -end LeanSubst diff --git a/LeanSubst/Old/Option.lean b/LeanSubst/Old/Option.lean deleted file mode 100644 index bf19a5e..0000000 --- a/LeanSubst/Old/Option.lean +++ /dev/null @@ -1,45 +0,0 @@ -import LeanSubst.Ren -import LeanSubst.Subst -import LeanSubst.Laws - -namespace LeanSubst - -variable {S T : Type} - -def Option.rmap [i : RenMap S] (r : Ren) : Option S -> Option S -| none => none -| some t => some (i.rmap r t) - -instance [RenMap S] : RenMap (Option S) where - rmap := Option.rmap - -def Option.smap [SubstMap S T] (σ : Subst T) : Option S -> Option S -| none => none -| some t => some t[σ:_] - -instance [SubstMap S T] : SubstMap (Option S) T where - smap := Option.smap - -@[simp, grind =] -theorem Option.smap_none [SubstMap S T] {σ : Subst T} - : (@Option.none S)[σ:_] = none -:= by - simp [SubstMap.smap, Option.smap] - -@[simp, grind =] -theorem Option.smap_some [SubstMap S T] {x : S} {σ : Subst T} - : (some x)[σ:_] = some x[σ:_] -:= by - simp [SubstMap.smap, Option.smap] - -instance [RenMap T] [SubstMap S T] [SubstMapId S T] - : SubstMapId (Option S) T -where - apply_id := by intro t; cases t <;> simp - -instance [RenMap S] [RenMap T] [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] - : SubstMapCompose (Option S) T -where - apply_compose := by intro s σ τ; cases s <;> simp - -end LeanSubst diff --git a/LeanSubst/Old/Ren.lean b/LeanSubst/Old/Ren.lean deleted file mode 100644 index 04f03d0..0000000 --- a/LeanSubst/Old/Ren.lean +++ /dev/null @@ -1,180 +0,0 @@ - -namespace LeanSubst - universe u - variable {S T : Type} - - structure Ren where - act : Nat -> Nat - - def Ren.id : Ren := ⟨λ x => x⟩ - - @[simp] - theorem Ren.id_action {x} : id.act x = x := by simp [Ren.id] - - def Ren.succ : Ren := ⟨(· + 1)⟩ - - @[simp] - theorem Ren.succ_action {x} : succ.act x = x + 1 := by simp [Ren.succ] - - def Ren.pred : Ren := ⟨(· - 1)⟩ - - @[simp] - theorem Ren.pred_action {x} : pred.act x = x - 1 := by simp [Ren.pred] - - def Ren.add (k : Nat) : Ren := ⟨(· + k)⟩ - - @[simp] - theorem Ren.add_action {k x} : (add k).act x = x + k := by simp [Ren.add] - - @[simp] - theorem Ren.add_zero : add 0 = id := by simp [Ren.add, Ren.id] - - @[simp] - theorem Ren.add_one : add 1 = succ := by simp [Ren.add, Ren.succ] - - def Ren.sub (k : Nat) : Ren := ⟨(· - k)⟩ - - @[simp] - theorem Ren.sub_action {k x} : (sub k).act x = x - k := by simp [Ren.sub] - - @[simp] - theorem Ren.sub_zero : sub 0 = id := by simp [Ren.sub, Ren.id] - - @[simp] - theorem Ren.sub_one : sub 1 = pred := by simp [Ren.sub, Ren.pred] - - def Ren.cons (a : Nat) (r : Ren) : Ren := .mk λ n => - match n with - | 0 => a - | n + 1 => r.act n - - infixr:67 (name := Ren.cons_notation) " :: " => Ren.cons - - @[simp] - theorem Ren.cons_action0 {a} {r : Ren} : (a::r).act 0 = a := by simp [Ren.cons] - - @[simp] - theorem Ren.cons_action {a i} {r : Ren} : (a::r).act (i + 1) = r.act i := by simp [Ren.cons] - - def Ren.append : List Nat -> Ren -> Ren - | .nil, r => r - | .cons hd tl, r => hd::append tl r - - instance : HAppend (List Nat) Ren Ren where - hAppend := Ren.append - - @[simp] - theorem Ren.append_nil {r : Ren} : ([] : List Nat) ++ r = r := by - simp [HAppend.hAppend, Ren.append] - - @[simp] - theorem Ren.append_cons {a} {ℓ : List Nat} {r : Ren} : (a::ℓ) ++ r = a::(ℓ ++ r) := by - simp [HAppend.hAppend, Ren.append] - - @[simp, grind <-] - theorem Ren.append_action_lt {r : Ren} {i} - : {ℓ : List Nat} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] - | .cons hd tl, h => - match i with - | 0 => rfl - | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) - - @[simp, grind =] - theorem Ren.append_action_ge {r : Ren} {i} - : {ℓ : List Nat} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) - | .nil, h => by simp - | .cons hd tl, h => - match i with - | 0 => by simp at h - | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) - - def Ren.compose : Ren -> Ren -> Ren - | r1, r2 => .mk λ n => r2.act (r1.act n) - - infixr:85 (name := Ren.compose_notation) " ∘ " => Ren.compose - - @[simp] - theorem Ren.compose_action {r1 r2 : Ren} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by - simp [Ren.compose] - - @[simp] - theorem Ren.compose_id_left {r : Ren} : id ∘ r = r := by - simp [Ren.compose, Ren.id] - - @[simp] - theorem Ren.compose_id_right {r : Ren} : r ∘ id = r := by - simp [Ren.compose, Ren.id] - - @[simp] - theorem Ren.compose_assoc {r1 r2 r3 : Ren} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by - simp [Ren.compose] - - def Ren.lift (r : Ren) (k : Nat := 1) : Ren := .mk λ n => - if n < k then n else r.act (n - k) + k - - @[simp, grind <-] - theorem Ren.lift_action_lt {r k i} (h : i < k) : (lift r k).act i = i := by - simp [Ren.lift]; grind - - @[simp, grind <-] - theorem Ren.lift_action_ge {r k i} (h : i ≥ k) : (lift r k).act i = r.act (i - k) + k := by - simp [Ren.lift]; grind - - @[simp] - theorem Ren.lift_of_zero {r : Ren} : r.lift 0 = r := by - unfold Ren.lift; congr - - @[grind =] - theorem Ren.lift_of_succ {r : Ren} {k} : r.lift (k + 1) = (r.lift k).lift := by - induction k; simp - case _ n ih => - unfold Ren.lift; congr; funext; case _ i => - simp; unfold Ren.lift at ih; simp at ih - grind - - @[simp] - theorem Ren.lift_id {k} : Ren.lift Ren.id k = Ren.id := by - simp [Ren.id, Ren.lift]; congr; funext; case _ x => - cases x <;> simp; omega - - theorem Ren.compose_lift_k1 {r1 r2 : Ren} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by - simp [Ren.compose, Ren.lift] - funext; case _ x => - cases x <;> simp - - @[simp] - theorem Ren.compose_lift {k} {r1 r2 : Ren} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by - induction k generalizing r1 r2; simp - case _ k ih => - rw [lift_of_succ, ih] - rw [lift_of_succ (r := r1)] - rw [lift_of_succ (r := r2)] - rw [compose_lift_k1] - - class RenMap (T : Type) where - rmap : Ren -> T -> T - - export RenMap (rmap) - - macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t) - - @[app_unexpander rmap] - def unexpandRenApply : Lean.PrettyPrinter.Unexpander - | `($_ $r $t) => `($t⟨$r⟩) - | _ => throw () - - class RenMapId (S : Type) [RenMap S] where - apply_id {t : S} : t⟨Ren.id⟩ = t - - class RenMapCompose (S : Type) [RenMap S] where - apply_compose {s : S} {r1 r2 : Ren} : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩ - - @[simp] - theorem Ren.apply_id [RenMap T] [RenMapId T] {t : T} : t⟨id⟩ = t := RenMapId.apply_id - - @[simp, grind =] - theorem Ren.apply_compose [RenMap T] [RenMapCompose T] {t : T} {r1 r2 : Ren} - : t⟨r1⟩⟨r2⟩ = t⟨r1 ∘ r2⟩ - := RenMapCompose.apply_compose - -end LeanSubst diff --git a/LeanSubst/Old/Subst.lean b/LeanSubst/Old/Subst.lean deleted file mode 100644 index 7b8a3ca..0000000 --- a/LeanSubst/Old/Subst.lean +++ /dev/null @@ -1,234 +0,0 @@ -import LeanSubst.Ren - -namespace LeanSubst - universe u - variable {S T : Type} - - inductive Subst.Action (T : Type) where - | re : Nat -> Subst.Action T - | su : T -> Subst.Action T - deriving Repr - - export Subst.Action (re su) - - @[simp] - def Subst.Action.rmap {T} [RenMap T] (r : Ren) : Subst.Action T -> Subst.Action T - | re x => re $ r.act x - | su t => su t⟨r⟩ - - instance [RenMap T] : RenMap (Subst.Action T) where - rmap := Subst.Action.rmap - - @[simp] - theorem Subst.Action.rmap_re [RenMap T] {r} {x : Nat} - : (@re T x)⟨r⟩ = re (r.act x) - := by simp [RenMap.rmap] - - @[simp] - theorem Subst.Action.rmap_su [RenMap T] {r} {t : T} : (su t)⟨r⟩ = su t⟨r⟩ := by - simp [RenMap.rmap] - - instance [RenMap T] [RenMapId T] : RenMapId (Subst.Action T) where - apply_id := by - intro t; simp [RenMap.rmap] - cases t <;> simp - - instance [RenMap T] [RenMapCompose T] : RenMapCompose (Subst.Action T) where - apply_compose := by - intro s r1 r2; simp [RenMap.rmap, Ren.compose] - cases s <;> simp [Ren.compose] - - structure Subst (T : Type) where - act : Nat -> Subst.Action T - - def Subst.id : Subst T := ⟨λ x => re x⟩ - notation "+0" => Subst.id - - @[simp] - theorem Subst.id_action {x} : (@Subst.id T).act x = re x := by simp [Subst.id] - - def Subst.succ : Subst T := ⟨λ x => re $ x + 1⟩ - notation "+1" => Subst.succ - - @[simp] - theorem Subst.succ_action {x} : (@Subst.succ T).act x = re (x + 1) := by simp [Subst.succ] - - def Subst.pred : Subst T := ⟨λ x => re $ x - 1⟩ - notation "-1" => Subst.pred - - @[simp] - theorem Subst.pred_action {x} : (@Subst.pred T).act x = re (x - 1) := by simp [Subst.pred] - - def Subst.add (k : Nat) : Subst T := ⟨λ x => re $ x + k⟩ - - @[simp] - theorem Subst.add_action {k x} : (@Subst.add T k).act x = re (x + k) := by simp [Subst.add] - - @[simp] - theorem Subst.add_zero : add 0 = @id T := by simp [Subst.add, Subst.id] - - @[simp] - theorem Subst.add_one : add 1 = @succ T := by simp [Subst.add, Subst.succ] - - def Subst.sub (k : Nat) : Subst T := ⟨λ x => re $ x - k⟩ - - @[simp] - theorem Subst.sub_action {k x} : (@Subst.sub T k).act x = re (x - k) := by simp [Subst.sub] - - @[simp] - theorem Subst.sub_zero : sub 0 = @id T := by simp [Subst.sub, Subst.id] - - @[simp] - theorem Subst.sub_one : sub 1 = @pred T := by simp [Subst.sub, Subst.pred] - - def Subst.cons (a : Subst.Action T) (σ : Subst T) : Subst T := .mk λ n => - match n with - | 0 => a - | n + 1 => σ.act n - - infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons - - @[simp] - theorem Subst.cons_action0 {a} {σ : Subst T} : (a::σ).act 0 = a := by simp [Subst.cons] - - @[simp] - theorem Subst.cons_action {a i} {σ : Subst T} : (a::σ).act (i + 1) = σ.act i := by - simp [Subst.cons] - - def Subst.append : List (Subst.Action T) -> Subst T -> Subst T - | .nil, σ => σ - | .cons hd tl, σ => hd::append tl σ - - instance : HAppend (List $ Subst.Action T) (Subst T) (Subst T) where - hAppend := Subst.append - - @[simp] - theorem Subst.append_nil {σ : Subst T} : ([] : List $ Action T) ++ σ = σ := by - simp [HAppend.hAppend, Subst.append] - - @[simp] - theorem Subst.append_cons {a} {ℓ : List (Action T)} {σ : Subst T} - : (a::ℓ) ++ σ = a::(ℓ ++ σ) - := by simp [HAppend.hAppend, Subst.append] - - @[simp, grind <-] - theorem Subst.append_action_lt {σ : Subst T} {i} - : {ℓ : List $ Action T} -> (h : i < ℓ.length) -> (ℓ ++ σ).act i = ℓ[i] - | .cons hd tl, h => - match i with - | 0 => rfl - | i + 1 => append_action_lt (σ := σ) (ℓ := tl) (by grind) - - @[simp, grind =] - theorem Subst.append_action_ge {σ : Subst T} {i} - : {ℓ : List $ Action T} -> (h : i ≥ ℓ.length) -> (ℓ ++ σ).act i = σ.act (i - ℓ.length) - | .nil, h => by simp - | .cons hd tl, h => - match i with - | 0 => by simp at h - | i + 1 => @append_action_ge σ i tl (by grind) |> cast (by simp) - - class SubstMap (S T : Type) where - smap : Subst T -> S -> S - - export SubstMap (smap) - - macro:max t:term noWs "[" σ:term "]" : term => `(smap $σ $t) - - @[app_unexpander smap] - def unexpandSubstApply : Lean.PrettyPrinter.Unexpander - | `($_ $σ $t) => `($t[$σ]) - | _ => throw () - - def Subst.compose [RenMap T] [SubstMap T T] : Subst T -> Subst T -> Subst T - | σ, τ => .mk λ n => - match σ.act n with - | su t => su t[τ] - | re k => τ.act k - - infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose - - def Subst.lift [RenMap T] (σ : Subst T) (k : Nat := 1) : Subst T := .mk λ n => - if n < k then re n else (σ.act (n - k))⟨.add k⟩ - - @[simp, grind <-] - theorem Subst.lift_action_lt [RenMap T] {σ : Subst T} {k i} (h : i < k) - : (lift σ k).act i = re i - := by simp [Subst.lift]; grind - - @[simp, grind <-] - theorem Subst.lift_action_ge [RenMap T] {σ : Subst T} {k i} (h : i ≥ k) - : (lift σ k).act i = (σ.act (i - k))⟨.add k⟩ - := by simp [Subst.lift]; grind - - -- @[simp] - -- theorem Subst.lift_of_zero [RenMap T] [RenMapId T] {σ : Subst T} : σ.lift 0 = σ := by - -- unfold Subst.lift; congr; simp - - -- @[grind =] - -- theorem Subst.lift_of_succ [RenMap T] [RenMapId T] {σ : Subst T} {k} : σ.lift (k + 1) = (σ.lift k).lift := by - -- induction k; simp - -- case _ n ih => - -- unfold Subst.lift; congr; funext; case _ i => - -- simp; unfold Subst.lift at ih; simp at ih - -- grind - - -- @[simp] - -- theorem Subst.lift_id {k} : Subst.lift Subst.id k = Subst.id := by - -- simp [Subst.id, Subst.lift]; congr; funext; case _ x => - -- cases x <;> simp; omega - - @[coe] - def Ren.to : Ren -> Subst T - | r => .mk λ n => re (r.act n) - - instance : Coe Ren (Subst T) where - coe := Ren.to - - @[simp, grind =] - theorem Ren.to_id : Ren.to (T := T) id = +0 := by simp [Ren.to, Subst.id, id] - - @[simp, grind =] - theorem Ren.to_succ : Ren.to (T := T) succ = +1 := by simp [Ren.to, Subst.succ] - - @[simp, grind =] - theorem Ren.to_pred : Ren.to (T := T) pred = -1 := by simp [Ren.to, Subst.pred] - - @[simp, grind =] - theorem Ren.to_add {k} : Ren.to (T := T) (add k) = Subst.add k := by simp [Ren.to, Subst.add] - - @[simp, grind =] - theorem Ren.to_sub {k} : Ren.to (T := T) (sub k) = Subst.sub k := by simp [Ren.to, Subst.sub] - - @[simp, grind =] - theorem Ren.pred_succ [RenMap T] [SubstMap T T] : Subst.compose (T := T) +1 -1 = +0 := by - simp [Subst.compose, Subst.id] - - @[simp, grind =] - theorem Ren.to_lift [RenMap T] {r : Ren} {k} : (r.lift k).to = (@Ren.to T r).lift k := by - cases r; simp [Ren.lift, Ren.to, Subst.lift]; case _ act => - funext; case _ x => - cases x - case zero => grind - case _ n => cases Nat.decLt (n + 1) k <;> simp [ite] - - @[simp, grind =] - theorem Ren.to_compose {r1 r2 : Ren} [RenMap T] [SubstMap T T] - : Ren.to (T := T) (r1 ∘ r2) = r1.to ∘ r2.to - := by - funext; case _ x => - cases x <;> simp [Ren.to, Subst.compose, Ren.compose] - - -- def Subst.hcompose [RenMap T] [SubstMap S T] : Subst S -> Subst T -> Subst S - -- | σ, τ => .mk λ n => - -- match σ.act n with - -- | su t => su (smap τ t) - -- | re k => re k - - -- infixr:85 " ◾ " => Subst.hcompose - - -- macro "+0@" noWs T:term : term =>`(@Subst.id $T) - -- macro "+1@" noWs T:term : term =>`(@Subst.succ $T) - -- macro "-1@" noWs T:term : term =>`(@Subst.pred $T) - -end LeanSubst diff --git a/LeanSubst/Old/Subst_Old.lean b/LeanSubst/Old/Subst_Old.lean deleted file mode 100644 index a17602e..0000000 --- a/LeanSubst/Old/Subst_Old.lean +++ /dev/null @@ -1,137 +0,0 @@ -import LeanSubst.Ren - -namespace LeanSubst - universe u - variable {S T : Type} - - inductive Subst.Action (T : Type) where - | re : Nat -> Subst.Action T - | su : T -> Subst.Action T - deriving Repr - - export Subst.Action (re su) - - structure Subst (T : Type) where - act : Nat -> Subst.Action T - - @[coe] - def Ren.to : Ren -> Subst T - | r => .mk λ n => re (r.act n) - - instance : Coe Ren (Subst T) where - coe := Ren.to - - class SubstMap (S T : Type) where - smap : Subst T -> S -> S - - export SubstMap (smap) - - def Subst.lift [RenMap T] (σ : Subst T) (k : Nat := 1) : Subst T := .mk λ n => - if n < k then re n else - match σ.act (n - k) with - | su t => su (rmap (Ren.add k) t) - | re i => re (i + k) - - def Subst.cons (a : Subst.Action T) (σ : Subst T) : Subst T := .mk λ n => - match n with - | 0 => a - | n + 1 => σ.act n - - def Subst.append : List (Subst.Action T) -> Subst T -> Subst T - | .nil, σ => σ - | .cons hd tl, σ => append tl (σ.cons hd) - - instance : HAppend (List $ Subst.Action T) (Subst T) (Subst T) where - hAppend := Subst.append - - @[simp] - abbrev smap1 [SubstMap S S] := smap (S := S) (T := S) - - def Subst.compose [RenMap T] [SubstMap T T] : Subst T -> Subst T -> Subst T - | σ, τ => .mk λ n => - match σ.act n with - | su t => su (smap τ t) - | re k => τ.act k - - def Subst.hcompose [RenMap T] [SubstMap S T] : Subst S -> Subst T -> Subst S - | σ, τ => .mk λ n => - match σ.act n with - | su t => su (smap τ t) - | re k => re k - - def Subst.id : Subst T := ⟨λ n => re n⟩ - def Subst.succ : Subst T := ⟨λ n => re (n + 1)⟩ - def Subst.pred : Subst T := ⟨λ n => re (n - 1)⟩ - - notation "+0" => Subst.id - macro "+0@" noWs T:term : term =>`(@Subst.id $T) - notation "+1" => Subst.succ - macro "+1@" noWs T:term : term =>`(@Subst.succ $T) - notation "-1" => Subst.pred - macro "-1@" noWs T:term : term =>`(@Subst.pred $T) - - @[simp, grind =] - theorem Subst.id_action {n} : (+0@T).act n = re n := by simp [Subst.id] - - @[simp, grind =] - theorem Subst.succ_action {n} : (+1@T).act n = re (n + 1) := by simp [Subst.succ] - - @[simp, grind =] - theorem Subst.pred_action {n} : (-1@T).act n = re (n - 1) := by simp [Subst.pred] - - @[simp, grind =] - theorem Ren.to_id : Ren.to (T := T) id = +0 := by - unfold Ren.to; unfold Subst.id; simp [id] - - @[simp, grind =] - theorem Ren.to_succ : Ren.to (T := T) (Ren.add 1) = +1 := by - unfold Ren.to; simp; unfold Subst.succ; simp [Ren.add] - - @[simp, grind =] - theorem Ren.to_pred : Ren.to (T := T) (Ren.sub 1) = -1 := by - unfold Ren.to; simp; unfold Subst.pred; simp [Ren.sub] - - @[simp, grind =] - theorem Ren.pred_succ [RenMap T] [SubstMap T T] : Subst.compose (T := T) +1 -1 = +0 := by - unfold Subst.compose; simp - unfold Subst.id; rfl - - @[grind =] - theorem Ren.to_lift [RenMap T] {r : Ren} {k} : (r.lift k).to = (@Ren.to T r).lift k := by - cases r; simp [Ren.lift, Ren.to, Subst.lift]; case _ act => - funext; case _ x => - cases x - case zero => grind - case _ n => cases Nat.decLt (n + 1) k <;> simp [ite] - - macro:max t:term noWs "[" σ:term "]" : term => `(smap1 $σ $t) - macro:max t:term noWs "[" σ:term ":" T:term "]" : term => `(smap (T := $T) $σ $t) - infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons - infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose - infixr:85 " ◾ " => Subst.hcompose - - @[app_unexpander smap1] - def unexpandSubstApply1 : Lean.PrettyPrinter.Unexpander - | `($_ $σ $t) => `($t[$σ]) - | _ => throw () - - @[app_unexpander smap] - def unexpandSubstApply : Lean.PrettyPrinter.Unexpander - | `($_ $σ $t) => `($t[$σ : _]) - | `($_ (T := $T) $σ $t) => `($t[$σ : $T]) - | _ => throw () - - @[simp, grind =] - theorem Ren.to_compose {r1 r2 : Ren} [RenMap T] [SubstMap T T] - : Ren.to (T := T) (r1 ∘ r2) = Subst.compose r1 r2 - := by - funext; case _ x => - cases x <;> simp [Ren.to, Subst.compose, Ren.compose] - - @[simp] - theorem Subst.cons_head_action {t} {σ : Subst T} : (t::σ).act 0 = t := by simp [Subst.cons] - - @[simp] - theorem Subst.cons_tail_action {t i} {σ : Subst T} : (t::σ).act (i + 1) = σ.act i := by simp [Subst.cons] - -end LeanSubst diff --git a/LeanSubst/Ops.lean b/LeanSubst/Ops.lean index 612eab9..7f0136b 100644 --- a/LeanSubst/Ops.lean +++ b/LeanSubst/Ops.lean @@ -1,309 +1,211 @@ -import LeanSubst.Types +import LeanSubst.Basic namespace LeanSubst universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} +variable {S : Type u1} {T : Type u2} {U : Type u3} ---------------------------------------------------------------------------------------------------- ----- Translation +---- Action ---------------------------------------------------------------------------------------------------- -def Ren.het T (r : Ren) : HetRen T := ⟨r.act⟩ - -@[simp] -theorem Ren.het_act {r : Ren} {x} : (r.het T).act x = r.act x := by simp [Ren.het] - -def HetRen.forget (r : HetRen T) : Ren := ⟨r.act⟩ - @[simp] -theorem HetRen.forget_act {r : HetRen T} {x} : r.forget.act x = r.act x := by simp [HetRen.forget] +def Action.rmap [RenMap S T] (r : Ren T) : Action S -> Action S +| re x => re $ r.act x +| su t => su t⟨r⟩ -@[simp] -theorem Ren.het_forget (r : Ren) : (r.het T).forget = r := by simp [Ren.het, HetRen.forget] +instance (priority := high) [RenMap T T] : RenMap (Action T) T where + rmap := Action.rmap @[simp] -theorem HetRen.forget_het (r : HetRen T) : r.forget.het T = r := by simp [Ren.het, HetRen.forget] - -def Subst.het S (σ : Subst T) : HetSubst S T := ⟨σ.act⟩ +theorem Action.rmap_re [RenMap T T] {r : Ren T} {x : Nat} : (@re T x)⟨r⟩ = re (r.act x) := by + simp [RenMap.rmap] @[simp] -theorem Subst.het_act {r : Subst T} {x} : (r.het S).act x = r.act x := by simp [Subst.het] - -def HetSubst.forget (σ : HetSubst S T) : Subst T := ⟨σ.act⟩ +theorem Action.rmap_su [RenMap T T] {r : Ren T} {t : T} : (su t)⟨r⟩ = su t⟨r⟩ := by + simp [RenMap.rmap] @[simp] -theorem HetSubst.forget_act {r : HetSubst S T} {x} : r.forget.act x = r.act x := by - simp [HetSubst.forget] +def Action.hrmap [RenMap S T] (r : Ren T) : Action S -> Action S +| re x => re x +| su t => su t⟨r⟩ -@[simp] -theorem Subst.het_forget (σ : Subst T) : (σ.het S).forget = σ := by - simp [Subst.het, HetSubst.forget] +instance [RenMap S T] : RenMap (Action S) T where + rmap := Action.hrmap @[simp] -theorem HetSubst.forget_het (σ : HetSubst S T) : σ.forget.het S = σ := by - simp [Subst.het, HetSubst.forget] - -def Ren.to (r : Ren) : Subst S := ⟨λ x => re (r.act x)⟩ +theorem Action.hrmap_re [RenMap S T] {r : Ren T} {x : Nat} : (@re S x)⟨r⟩ = re x := by + simp [RenMap.rmap] @[simp] -theorem Ren.to_act {r : Ren} {x} : (@Ren.to S r).act x = re (r.act x) := by simp [Ren.to] +theorem Actionh.rmap_su [RenMap S T] {r : Ren T} {t : S} : (su t)⟨r⟩ = su t⟨r⟩ := by + simp [RenMap.rmap] -def HetRen.to (r : HetRen T) : HetSubst S T := ⟨λ x => re (r.act x)⟩ - -@[simp] -theorem HetRen.to_act {r : HetRen T} {x} : (@HetRen.to S T r).act x = re (r.act x) := by - simp [HetRen.to] ----------------------------------------------------------------------------------------------------- ----- Action ----------------------------------------------------------------------------------------------------- @[simp] -def Action.rmap [RenMap S] (r : Ren) : Action S -> Action S -| re x => re $ r.act x -| su t => su t⟨r⟩ +def Action.smap [SubstMap T T] (σ : Subst T) : Action T -> Action T +| re x => σ.act x +| su t => su t[σ] -instance [RenMap S] : RenMap (Action S) where - rmap := Action.rmap +instance (priority := high) [SubstMap T T] : SubstMap (Action T) T where + smap := Action.smap @[simp] -theorem Action.rmap_re [RenMap S] {r : Ren} {x : Nat} - : (@re S x)⟨r⟩ = re (r.act x) -:= by simp [RenMap.rmap] +theorem Action.smap_re [SubstMap T T] {σ : Subst T} {x : Nat} : (@re T x)[σ] = σ.act x := by + simp [SubstMap.smap] @[simp] -theorem Action.rmap_su [RenMap S] {r : Ren} {t : S} : (su t)⟨r⟩ = su t⟨r⟩ := by simp [RenMap.rmap] +theorem Action.smap_su [SubstMap T T] {σ : Subst T} {t : T} : (su t)[σ] = su t[σ] := by + simp [SubstMap.smap] @[simp] -def Action.hsmap [SubstMap S] (σ : HetSubst (Action S) S) : Action S -> Action S -| re x => σ.act x -| su t => su t[σ.forget] +def Action.hsmap [SubstMap S T] (σ : Subst T) : Action S -> Action S +| re x => re x +| su t => su t[σ] -instance [SubstMap S] : HetSubstMap (Action S) S where - hsmap := Action.hsmap +instance [SubstMap S T] : SubstMap (Action S) T where + smap := Action.hsmap @[simp] -theorem Action.hsmap_re [SubstMap S] {σ : HetSubst (Action S) S} {x : Nat} - : (@re S x)[σ] = σ.act x -:= by simp [HetSubstMap.hsmap] +theorem Action.hsmap_re [SubstMap S T] {σ : Subst T} {x : Nat} : (@re S x)[σ] = re x := by + simp [SubstMap.smap] @[simp] -theorem Action.hsmap_su [SubstMap S] {σ : HetSubst (Action S) S} {t : S} - : (su t)[σ] = su t[σ.forget] -:= by simp [HetSubstMap.hsmap] +theorem Actionh.smap_su [SubstMap S T] {σ : Subst T} {t : S} : (su t)[σ] = su t[σ] := by + simp [SubstMap.smap] ---------------------------------------------------------------------------------------------------- ---- Identity ---------------------------------------------------------------------------------------------------- -def Ren.id : Ren := ⟨λ x => x⟩ - -@[simp] -theorem Ren.id_action {x} : id.act x = x := by simp [Ren.id] - -def HetRen.id T : HetRen T := ⟨λ x => x⟩ +def Ren.id T : Ren T := ⟨λ x => x⟩ @[simp] -theorem HetRen.id_action {x} : (id T).act x = x := by simp [HetRen.id] +theorem Ren.id_action {x} : (id T).act x = x := by simp [Ren.id] -def Subst.id : Subst S := ⟨λ x => re x⟩ -notation "+0" => Subst.id +def Subst.id T : Subst T := ⟨λ x => re x⟩ +notation "+0" => Subst.id _ @[simp] -theorem Subst.id_action {x} : (@id S).act x = re x := by simp [Subst.id] - -def HetSubst.id T : HetSubst S T := ⟨λ x => re x⟩ -macro "+0@" noWs T:term : term =>`(HetSubst.id $T) - -@[simp] -theorem HetSubst.id_action {x} : (@id S T).act x = re x := by simp [HetSubst.id] +theorem Subst.id_action {x} : (id T).act x = re x := by simp [Subst.id] ---------------------------------------------------------------------------------------------------- ---- Successor ---------------------------------------------------------------------------------------------------- -def Ren.succ : Ren := ⟨(· + 1)⟩ - -@[simp] -theorem Ren.succ_action {x} : succ.act x = x + 1 := by simp [Ren.succ] - -def HetRen.succ T : HetRen T := ⟨(· + 1)⟩ - -@[simp] -theorem HetRen.succ_action {x} : (succ T).act x = x + 1 := by simp [HetRen.succ] - -def Subst.succ : Subst S := ⟨λ x => re $ x + 1⟩ -notation "+1" => Subst.succ +def Ren.succ T : Ren T := ⟨(· + 1)⟩ @[simp] -theorem Subst.succ_action {x} : (@succ S).act x = re (x + 1) := by simp [Subst.succ] +theorem Ren.succ_action {x} : (succ T).act x = x + 1 := by simp [Ren.succ] -def HetSubst.succ T : HetSubst S T := ⟨λ x => re $ x + 1⟩ -macro "+1@" noWs T:term : term =>`(HetSubst.succ $T) +def Subst.succ T : Subst T := ⟨λ x => re $ x + 1⟩ +notation "+1" => Subst.succ _ @[simp] -theorem HetSubst.succ_action {x} : (@succ S T).act x = re (x + 1) := by simp [HetSubst.succ] +theorem Subst.succ_action {x} : (succ T).act x = re (x + 1) := by simp [Subst.succ] ---------------------------------------------------------------------------------------------------- ---- Predecessor ---------------------------------------------------------------------------------------------------- -def Ren.pred : Ren := ⟨(· - 1)⟩ +def Ren.pred T : Ren T := ⟨(· - 1)⟩ @[simp] -theorem Ren.pred_action {x} : pred.act x = x - 1 := by simp [Ren.pred] +theorem Ren.pred_action {x} : (pred T).act x = x - 1 := by simp [Ren.pred] -def HetRen.pred T : HetRen T := ⟨(· - 1)⟩ +def Subst.pred T : Subst T := ⟨λ x => re $ x - 1⟩ +notation "-1" => Subst.pred _ @[simp] -theorem HetRen.pred_action {x} : (pred T).act x = x - 1 := by simp [HetRen.pred] - -def Subst.pred : Subst S := ⟨λ x => re $ x - 1⟩ -notation "-1" => Subst.pred - -@[simp] -theorem Subst.pred_action {x} : (@pred S).act x = re (x - 1) := by simp [Subst.pred] - -def HetSubst.pred : HetSubst S T := ⟨λ x => re $ x - 1⟩ -macro "-1@" noWs T:term : term =>`(HetSubst.pred $T) - -@[simp] -theorem HetSubst.pred_action {x} : (@pred S T).act x = re (x - 1) := by simp [HetSubst.pred] +theorem Subst.pred_action {x} : (pred T).act x = re (x - 1) := by simp [Subst.pred] ---------------------------------------------------------------------------------------------------- ---- Addition ---------------------------------------------------------------------------------------------------- -def Ren.add (k : Nat) : Ren := ⟨(· + k)⟩ - -@[simp] -theorem Ren.add_action {k x} : (add k).act x = x + k := by simp [Ren.add] - -@[simp] -theorem Ren.add_zero : add 0 = id := by simp [Ren.add, Ren.id] - -@[simp] -theorem Ren.add_one : add 1 = succ := by simp [Ren.add, Ren.succ] - -def HetRen.add T (k : Nat) : HetRen T := ⟨(· + k)⟩ - -@[simp] -theorem HetRen.add_action {k x} : (add T k).act x = x + k := by simp [HetRen.add] +def Ren.add T (k : Nat) : Ren T := ⟨(· + k)⟩ @[simp] -theorem HetRen.add_zero : add T 0 = id T := by simp [HetRen.add, HetRen.id] +theorem Ren.add_action {k x} : (add T k).act x = x + k := by simp [Ren.add] @[simp] -theorem HetRen.add_one : add T 1 = succ T := by simp [HetRen.add, HetRen.succ] - -def Subst.add (k : Nat) : Subst S := ⟨λ x => re $ x + k⟩ - -@[simp] -theorem Subst.add_action {k x} : (@add S k).act x = re (x + k) := by simp [Subst.add] - -@[simp] -theorem Subst.add_zero : @add S 0 = id := by simp [Subst.add, Subst.id] +theorem Ren.add_zero : add T 0 = id T := by simp [Ren.add, Ren.id] @[simp] -theorem Subst.add_one : @add S 1 = succ := by simp [Subst.add, Subst.succ] +theorem Ren.add_one : add T 1 = succ T := by simp [Ren.add, Ren.succ] -def HetSubst.add (k : Nat) : HetSubst S T := ⟨λ x => re $ x + k⟩ +def Subst.add T (k : Nat) : Subst T := ⟨λ x => re $ x + k⟩ @[simp] -theorem HetSubst.add_action {k x} : (@add S T k).act x = re (x + k) := by simp [HetSubst.add] +theorem Subst.add_action {k x} : (add T k).act x = re (x + k) := by simp [Subst.add] @[simp] -theorem HetSubst.add_zero : @add S T 0 = id T := by simp [HetSubst.add, HetSubst.id] +theorem Subst.add_zero : add T 0 = +0 := by simp [Subst.add, Subst.id] @[simp] -theorem HetSubst.add_one : @add S T 1 = succ T := by simp [HetSubst.add, HetSubst.succ] +theorem Subst.add_one : add T 1 = +1 := by simp [Subst.add, Subst.succ] ---------------------------------------------------------------------------------------------------- ---- Subtraction ---------------------------------------------------------------------------------------------------- -def Ren.sub (k : Nat) : Ren := ⟨(· - k)⟩ +def Ren.sub T (k : Nat) : Ren T := ⟨(· - k)⟩ @[simp] -theorem Ren.sub_action {k x} : (sub k).act x = x - k := by simp [Ren.sub] +theorem Ren.sub_action {k x} : (sub T k).act x = x - k := by simp [Ren.sub] @[simp] -theorem Ren.sub_zero : sub 0 = id := by simp [Ren.sub, Ren.id] +theorem Ren.sub_zero : sub T 0 = id T := by simp [Ren.sub, Ren.id] @[simp] -theorem Ren.sub_one : sub 1 = pred := by simp [Ren.sub, Ren.pred] +theorem Ren.sub_one : sub T 1 = pred T := by simp [Ren.sub, Ren.pred] -def HetRen.sub T (k : Nat) : HetRen T := ⟨(· - k)⟩ +def Subst.sub T (k : Nat) : Subst T := ⟨λ x => re $ x - k⟩ @[simp] -theorem HetRen.sub_action {k x} : (sub T k).act x = x - k := by simp [HetRen.sub] +theorem Subst.sub_action {k x} : (@sub T k).act x = re (x - k) := by simp [Subst.sub] @[simp] -theorem HetRen.sub_zero : sub T 0 = id T := by simp [HetRen.sub, HetRen.id] +theorem Subst.sub_zero : sub T 0 = +0 := by simp [Subst.sub, Subst.id] @[simp] -theorem HetRen.sub_one : sub T 1 = pred T := by simp [HetRen.sub, HetRen.pred] +theorem Subst.sub_one : sub T 1 = -1 := by simp [Subst.sub, Subst.pred] + ---------------------------------------------------------------------------------------------------- ---- Cons ---------------------------------------------------------------------------------------------------- -def Ren.cons (a : Nat) (r : Ren) : Ren := .mk λ n => +def Ren.cons (a : Nat) (r : Ren T) : Ren T := .mk λ n => match n with | 0 => a | n + 1 => r.act n infixr:67 (name := Ren.cons_notation) " :: " => Ren.cons @[simp] -theorem Ren.cons_action0 {a} {r : Ren} : (a::r).act 0 = a := by simp [Ren.cons] - -@[simp] -theorem Ren.cons_action {a i} {r : Ren} : (a::r).act (i + 1) = r.act i := by simp [Ren.cons] - -def HetRen.cons (a : Nat) (r : HetRen T) : HetRen T := .mk λ n => - match n with - | 0 => a - | n + 1 => r.act n -infixr:67 (name := HetRen.cons_notation) " :: " => HetRen.cons - -@[simp] -theorem HetRen.cons_action0 {a} {r : HetRen T} : (a::r).act 0 = a := by simp [HetRen.cons] +theorem Ren.cons_action0 {a} {r : Ren T} : (a::r).act 0 = a := by simp [Ren.cons] @[simp] -theorem HetRen.cons_action {a i} {r : HetRen T} : (a::r).act (i + 1) = r.act i := by - simp [HetRen.cons] +theorem Ren.cons_action {a i} {r : Ren T} : (a::r).act (i + 1) = r.act i := by simp [Ren.cons] -def Subst.cons (a : Action S) (r : Subst S) : Subst S := .mk λ n => +def Subst.cons (a : Action T) (σ : Subst T) : Subst T := .mk λ n => match n with | 0 => a - | n + 1 => r.act n + | n + 1 => σ.act n infixr:67 (name := Subst.cons_notation) " :: " => Subst.cons @[simp] -theorem Subst.cons_action0 {a} {r : Subst S} : (a::r).act 0 = a := by simp [Subst.cons] - -@[simp] -theorem Subst.cons_action {a i} {r : Subst S} : (a::r).act (i + 1) = r.act i := by simp [Subst.cons] - -def HetSubst.cons (a : Action T) (r : HetSubst S T) : HetSubst S T := .mk λ n => - match n with - | 0 => a - | n + 1 => r.act n -infixr:67 (name := HetSubst.cons_notation) " :: " => HetSubst.cons - -@[simp] -theorem HetSubst.cons_action0 {a} {r : HetSubst S T} : (a::r).act 0 = a := by simp [HetSubst.cons] +theorem Subst.cons_action0 {a} {σ : Subst T} : (a::σ).act 0 = a := by simp [Subst.cons] @[simp] -theorem HetSubst.cons_action {a i} {r : HetSubst S T} : (a::r).act (i + 1) = r.act i := by - simp [HetSubst.cons] +theorem Subst.cons_action {a i} {σ : Subst T} : (a::σ).act (i + 1) = σ.act i := by simp [Subst.cons] ---------------------------------------------------------------------------------------------------- ---- Append ---------------------------------------------------------------------------------------------------- -def Ren.append : List Nat -> Ren -> Ren +def Ren.append : List Nat -> Ren T -> Ren T | .nil, r => r | .cons hd tl, r => hd::append tl r -instance : HAppend (List Nat) Ren Ren where +instance : HAppend (List Nat) (Ren T) (Ren T) where hAppend := Ren.append @[simp] -theorem Ren.append_nil {r : Ren} : ([] : List Nat) ++ r = r := by +theorem Ren.append_nil {r : Ren T} : ([] : List Nat) ++ r = r := by simp [HAppend.hAppend, Ren.append] @[simp] -theorem Ren.append_cons {a} {ℓ : List Nat} {r : Ren} : (a::ℓ) ++ r = a::(ℓ ++ r) := by +theorem Ren.append_cons {a} {ℓ : List Nat} {r : Ren T} : (a::ℓ) ++ r = a::(ℓ ++ r) := by simp [HAppend.hAppend, Ren.append] @[simp, grind <-] -theorem Ren.append_action_lt {r : Ren} {i} +theorem Ren.append_action_lt {r : Ren T} {i} : {ℓ : List Nat} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] | .cons hd tl, h => match i with @@ -311,7 +213,7 @@ theorem Ren.append_action_lt {r : Ren} {i} | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) @[simp, grind <-] -theorem Ren.append_action_ge {r : Ren} {i} +theorem Ren.append_action_ge {r : Ren T} {i} : {ℓ : List Nat} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) | .nil, h => by simp | .cons hd tl, h => @@ -319,182 +221,151 @@ theorem Ren.append_action_ge {r : Ren} {i} | 0 => by simp at h | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) -def HetRen.append : List Nat -> HetRen T -> HetRen T +def Subst.append : List (Action T) -> Subst T -> Subst T | .nil, r => r | .cons hd tl, r => hd::append tl r -instance : HAppend (List Nat) (HetRen T) (HetRen T) where - hAppend := HetRen.append - -@[simp] -theorem HetRen.append_nil {r : HetRen T} : ([] : List Nat) ++ r = r := by - simp [HAppend.hAppend, HetRen.append] - -@[simp] -theorem HetRen.append_cons {a} {ℓ : List Nat} {r : HetRen T} : (a::ℓ) ++ r = a::(ℓ ++ r) := by - simp [HAppend.hAppend, HetRen.append] - -@[simp, grind <-] -theorem HetRen.append_action_lt {r : HetRen T} {i} - : {ℓ : List Nat} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] -| .cons hd tl, h => - match i with - | 0 => rfl - | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) - -@[simp, grind <-] -theorem HetRen.append_action_ge {r : HetRen T} {i} - : {ℓ : List Nat} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) -| .nil, h => by simp -| .cons hd tl, h => - match i with - | 0 => by simp at h - | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) - -def Subst.append : List (Action S) -> Subst S -> Subst S -| .nil, r => r -| .cons hd tl, r => hd::append tl r - -instance : HAppend (List $ Action S) (Subst S) (Subst S) where +instance : HAppend (List $ Action T) (Subst T) (Subst T) where hAppend := Subst.append @[simp] -theorem Subst.append_nil {r : Subst S} : ([] : List $ Action S) ++ r = r := by +theorem Subst.append_nil {σ : Subst T} : ([] : List $ Action T) ++ σ = σ := by simp [HAppend.hAppend, Subst.append] @[simp] -theorem Subst.append_cons {a} {ℓ : List $ Action S} {r : Subst S} : (a::ℓ) ++ r = a::(ℓ ++ r) := by +theorem Subst.append_cons {a} {ℓ : List $ Action T} {σ : Subst T} : (a::ℓ) ++ σ = a::(ℓ ++ σ) := by simp [HAppend.hAppend, Subst.append] @[simp, grind <-] -theorem Subst.append_action_lt {r : Subst S} {i} - : {ℓ : List $ Action S} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] -| .cons hd tl, h => - match i with - | 0 => rfl - | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) - -@[simp, grind <-] -theorem Subst.append_action_ge {r : Subst S} {i} - : {ℓ : List $ Action S} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) -| .nil, h => by simp -| .cons hd tl, h => - match i with - | 0 => by simp at h - | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) - -def HetSubst.append : List (Action T) -> HetSubst S T -> HetSubst S T -| .nil, r => r -| .cons hd tl, r => hd::append tl r - -instance : HAppend (List $ Action T) (HetSubst S T) (HetSubst S T) where - hAppend := HetSubst.append - -@[simp] -theorem HetSubst.append_nil {r : HetSubst S T} : ([] : List $ Action T) ++ r = r := by - simp [HAppend.hAppend, HetSubst.append] - -@[simp] -theorem HetSubst.append_cons {a} {ℓ : List $ Action T} {r : HetSubst S T} - : (a::ℓ) ++ r = a::(ℓ ++ r) -:= by simp [HAppend.hAppend, HetSubst.append] - -@[simp, grind <-] -theorem HetSubst.append_action_lt {r : HetSubst S T} {i} - : {ℓ : List $ Action T} -> (h : i < ℓ.length) -> (ℓ ++ r).act i = ℓ[i] +theorem Subst.append_action_lt {σ : Subst T} {i} + : {ℓ : List $ Action T} -> (h : i < ℓ.length) -> (ℓ ++ σ).act i = ℓ[i] | .cons hd tl, h => match i with | 0 => rfl - | i + 1 => append_action_lt (r := r) (ℓ := tl) (by grind) + | i + 1 => append_action_lt (σ := σ) (ℓ := tl) (by grind) @[simp, grind <-] -theorem HetSubst.append_action_ge {r : HetSubst S T} {i} - : {ℓ : List $ Action T} -> (h : i ≥ ℓ.length) -> (ℓ ++ r).act i = r.act (i - ℓ.length) +theorem Subst.append_action_ge {σ : Subst T} {i} + : {ℓ : List $ Action T} -> (h : i ≥ ℓ.length) -> (ℓ ++ σ).act i = σ.act (i - ℓ.length) | .nil, h => by simp | .cons hd tl, h => match i with | 0 => by simp at h - | i + 1 => @append_action_ge r i tl (by grind) |> cast (by simp) + | i + 1 => @append_action_ge σ i tl (by grind) |> cast (by simp) ---------------------------------------------------------------------------------------------------- ---- Composition ---------------------------------------------------------------------------------------------------- -def Ren.compose : Ren -> Ren -> Ren +def Ren.compose : Ren T -> Ren T -> Ren T | r1, r2 => .mk λ n => r2.act (r1.act n) -infixr:85 (name := Ren.compose_notation) " ∘ " => Ren.compose +infixr:85 " ∘ " => Ren.compose @[simp] -theorem Ren.compose_action {r1 r2 : Ren} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by - simp [Ren.compose] +theorem Ren.compose_action {r1 r2 : Ren T} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := + by simp [Ren.compose] @[simp] -theorem Ren.compose_id_left {r : Ren} : id ∘ r = r := by +theorem Ren.compose_id_left {r : Ren T} : id T ∘ r = r := by simp [Ren.compose, Ren.id] @[simp] -theorem Ren.compose_id_right {r : Ren} : r ∘ id = r := by +theorem Ren.compose_id_right {r : Ren T} : r ∘ id T = r := by simp [Ren.compose, Ren.id] @[simp] -theorem Ren.compose_assoc {r1 r2 r3 : Ren} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by +theorem Ren.compose_assoc {r1 r2 r3 : Ren T} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by simp [Ren.compose] -def HetRen.compose : HetRen T -> HetRen T -> HetRen T -| r1, r2 => .mk λ n => r2.act (r1.act n) -infixr:85 (name := HetRen.compose_notation) " ∘ " => HetRen.compose +@[simp] +theorem Ren.compose_pred_succ : succ T ∘ pred T = id T := by simp [succ, pred, id, compose] @[simp] -theorem HetRen.compose_action {r1 r2 : HetRen T} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by - simp [HetRen.compose] +theorem Ren.compose_sub_add {k} : add T k ∘ sub T k = id T := by simp [sub, add, id, compose] + +-- -- r1 contains only S-vars, hence a renaming of T-vars is a no-op +-- def Ren.hcompose : Ren S -> Ren T -> Ren S +-- | r, _ => .mk λ n => r.act n +-- infixr:85 " ◾ " => Ren.hcompose + +-- @[simp] +-- theorem Ren.hcompose_ext {r1 : Ren S} {r2 : Ren T} : r1 ◾ r2 = r1 := sorry + +-- -- same deal as `Ren.hcompose` +-- def Ren.hcompose_subst : Ren S -> Subst T -> Ren S +-- | r, _ => .mk λ n => r.act n +-- infixr:85 " ◾ " => Ren.hcompose + +def Subst.compose [SubstMap T T] : Subst T -> Subst T -> Subst T +| σ, τ => .mk λ n => (σ.act n)[τ] +infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose @[simp] -theorem HetRen.compose_id_left {r : HetRen T} : id T ∘ r = r := by - simp [HetRen.compose, HetRen.id] +theorem Subst.compose_action [SubstMap T T] {σ τ : Subst T} {x} : (σ ∘ τ).act x = (σ.act x)[τ] := by + simp [Subst.compose] @[simp] -theorem HetRen.compose_id_right {r : HetRen T} : r ∘ id T = r := by - simp [HetRen.compose, HetRen.id] +theorem Subst.compose_pred_succ [SubstMap T T] : succ T ∘ pred T = id T := by + simp [succ, pred, id, compose] @[simp] -theorem HetRen.compose_assoc {r1 r2 r3 : HetRen T} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by - simp [HetRen.compose] +theorem Subst.compose_sub_add [SubstMap T T] {k} : add T k ∘ sub T k = id T := by + simp [sub, add, id, compose] -def Subst.compose [RenMap S] [SubstMap S] : Subst S -> Subst S -> Subst S -| σ, τ => .mk λ n => (σ.act n)[τ.het _] -infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose +def Subst.compose_ren_left : Ren T -> Subst T -> Subst T +| r, τ => .mk λ n => τ.act (r.act n) +infixr:85 (name := Subst.compose_ren_left_notation) " ∘ " => Subst.compose_ren_left + +@[simp] +theorem Subst.compose_ren_left_action {r : Ren T} {τ : Subst T} {x} + : (r ∘ τ).act x = τ.act (r.act x) +:= by simp [Subst.compose_ren_left] + +def Subst.compose_ren_right [RenMap T T] : Subst T -> Ren T -> Subst T +| σ, r => .mk λ n => (σ.act n)⟨r⟩ +infixr:85 (name := Subst.compose_ren_right_notation) " ∘ " => Subst.compose_ren_right @[simp] -theorem Subst.compose_action [RenMap S] [SubstMap S] {σ τ : Subst S} {x} - : (σ ∘ τ).act x = (σ.act x)[τ.het _] -:= by simp [Subst.compose] +theorem Subst.compose_ren_right_action [RenMap T T] {σ : Subst T} {r : Ren T} {x} + : (σ ∘ r).act x = (σ.act x)⟨r⟩ +:= by simp [Subst.compose_ren_right] -def HetSubst.compose [HetRenMap S T] [HetSubstMap S T] : HetSubst S T -> HetSubst S T -> HetSubst S T +def Subst.hcompose [SubstMap S T] : Subst S -> Subst T -> Subst S | σ, τ => .mk λ n => (σ.act n)[τ] -infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose +infixr:85 " ◾ " => Subst.hcompose + +@[simp] +theorem Subst.hcompose_action [SubstMap S T] {σ : Subst S} {τ : Subst T} {x} + : (σ ◾ τ).act x = (σ.act x)[τ] +:= by simp [Subst.hcompose] + +def Subst.hcompose_ren [RenMap S T] : Subst S -> Ren T -> Subst S +| σ, r => .mk λ n => (σ.act n)⟨r⟩ +infixr:85 " ◾ " => Subst.hcompose_ren @[simp] -theorem Subst.compose_action [RenMap S] [SubstMap S] {σ τ : Subst S} {x} - : (σ ∘ τ).act x = (σ.act x)[τ.het _] -:= by simp [Subst.compose] +theorem Subst.hcompose_ren_action [RenMap S T] {σ : Subst S} {r : Ren T} {x} + : (σ ◾ r).act x = (σ.act x)⟨r⟩ +:= by simp [Subst.hcompose_ren] + ---------------------------------------------------------------------------------------------------- ---- Lift ---------------------------------------------------------------------------------------------------- -def Ren.lift (r : Ren) (k : Nat := 1) : Ren := .mk λ n => +def Ren.lift (r : Ren T) (k : Nat := 1) : Ren T := .mk λ n => if n < k then n else r.act (n - k) + k @[simp, grind <-] -theorem Ren.lift_action_lt {r k i} (h : i < k) : (lift r k).act i = i := by +theorem Ren.lift_action_lt {r : Ren T} {k i} (h : i < k) : (lift r k).act i = i := by simp [Ren.lift]; grind @[simp, grind <-] -theorem Ren.lift_action_ge {r k i} (h : i ≥ k) : (lift r k).act i = r.act (i - k) + k := by - simp [Ren.lift]; grind +theorem Ren.lift_action_ge {r : Ren T} {k i} (h : i ≥ k) : (lift r k).act i = r.act (i - k) + k := + by simp [Ren.lift]; grind @[simp] -theorem Ren.lift_of_zero {r : Ren} : r.lift 0 = r := by +theorem Ren.lift_of_zero {r : Ren T} : r.lift 0 = r := by unfold Ren.lift; congr @[grind =] -theorem Ren.lift_of_succ {r : Ren} {k} : r.lift (k + 1) = (r.lift k).lift := by +theorem Ren.lift_of_succ {r : Ren T} {k} : r.lift (k + 1) = (r.lift k).lift := by induction k; simp case _ n ih => unfold Ren.lift; congr; funext; case _ i => @@ -502,25 +373,71 @@ theorem Ren.lift_of_succ {r : Ren} {k} : r.lift (k + 1) = (r.lift k).lift := by grind @[simp] -theorem Ren.lift_id {k} : Ren.lift Ren.id k = Ren.id := by +theorem Ren.lift_id {k} : lift (id T) k = id T := by simp [Ren.id, Ren.lift]; congr; funext; case _ x => cases x <;> simp; omega -theorem Ren.lift_compose_k1 {r1 r2 : Ren} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by +theorem Ren.lift_compose1 {r1 r2 : Ren T} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by simp [Ren.compose, Ren.lift] funext; case _ x => cases x <;> simp @[simp] -theorem Ren.lift_compose {k} {r1 r2 : Ren} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by +theorem Ren.lift_compose {k} {r1 r2 : Ren T} : (r1 ∘ r2).lift k = r1.lift k ∘ r2.lift k := by induction k generalizing r1 r2; simp case _ k ih => rw [lift_of_succ, ih] rw [lift_of_succ (r := r1)] rw [lift_of_succ (r := r2)] - rw [lift_compose_k1] + rw [lift_compose1] + +def Subst.lift [RenMap T T] (σ : Subst T) (k : Nat := 1) : Subst T := .mk λ n => + if n < k then re n else (σ.act (n - k))⟨.add T k⟩ + +@[simp, grind <-] +theorem Subst.lift_action_lt [RenMap T T] {σ : Subst T} {k i} (h : i < k) + : (lift σ k).act i = re i +:= by simp [Subst.lift]; grind + +@[simp, grind <-] +theorem Subst.lift_action_ge [RenMap T T] {σ : Subst T} {k i} (h : i ≥ k) + : (lift σ k).act i = (σ.act (i - k))⟨.add T k⟩ +:= by simp [Subst.lift]; grind +---------------------------------------------------------------------------------------------------- +---- Promotion +---------------------------------------------------------------------------------------------------- +def Ren.to (r : Ren T) : Subst T := ⟨λ x => re (r.act x)⟩ + +@[simp] +theorem Ren.to_act {r : Ren T} {x} : (@to T r).act x = re (r.act x) := by simp [Ren.to] + +@[simp] +theorem Ren.to_id : (id T).to = .id T := by simp [to, id, Subst.id] + +@[simp] +theorem Ren.to_succ : (succ T).to = .succ T := by simp [to, succ, Subst.succ] + +@[simp] +theorem Ren.to_pred : (pred T).to = .pred T := by simp [to, pred, Subst.pred] + +@[simp] +theorem Ren.to_add {k} : (add T k).to = .add T k := by simp [to, add, Subst.add] +@[simp] +theorem Ren.to_sub {k} : (sub T k).to = .sub T k := by simp [to, sub, Subst.sub] +@[simp] +theorem Ren.to_lift [RenMap T T] {r : Ren T} {k} : (r.lift k).to = (@to T r).lift k := by + cases r; simp [to, lift, Subst.lift]; case _ act => + funext; case _ x => + cases x; grind + case _ n => cases Nat.decLt (n + 1) k <;> simp [ite] +@[simp] +theorem Ren.to_compose [RenMap T T] [SubstMap T T] {r1 r2 : Ren T} + : @to T (r1 ∘ r2) = r1.to ∘ r2.to +:= by + funext; case _ x => + cases x <;> simp [to, compose, Subst.compose] end LeanSubst diff --git a/LeanSubst/Rewriting/Normal.lean b/LeanSubst/Rewriting/Normal.lean index cb7c8a9..596a13b 100644 --- a/LeanSubst/Rewriting/Normal.lean +++ b/LeanSubst/Rewriting/Normal.lean @@ -1,8 +1,7 @@ import Init.WF -import LeanSubst.Ren -import LeanSubst.Subst -import LeanSubst.Reduction +import LeanSubst.Laws +import LeanSubst.Rewriting.Reduction namespace LeanSubst universe u @@ -113,7 +112,7 @@ namespace LeanSubst intro a; replace h := h a apply equiv_acc.1 h - variable [RenMap T] [SubstMap T T] [Substitutive R] + variable [RenMap T T] [SubstMap T T] [Substitutive R] theorem subst_preimage {σ : Subst T} {t} : SN R t[σ] -> SN R t := by intro r; apply preimage (smap σ) t _ r diff --git a/LeanSubst/Rewriting/Reduction.lean b/LeanSubst/Rewriting/Reduction.lean index db77ef0..927c24a 100644 --- a/LeanSubst/Rewriting/Reduction.lean +++ b/LeanSubst/Rewriting/Reduction.lean @@ -1,11 +1,10 @@ -import LeanSubst.Ren -import LeanSubst.Subst +import LeanSubst.Laws namespace LeanSubst universe u - class Substitutive {T : Type} [RenMap T] [SubstMap T T] (R : T -> T -> Prop) where + class Substitutive {T : Type} [RenMap T T] [SubstMap T T] (R : T -> T -> Prop) where subst {t s} (σ : Subst T) : R t s -> R (t[σ]) (s[σ]) class HasTriangle {T : Type u} (R : T -> T -> Prop) where @@ -15,7 +14,7 @@ namespace LeanSubst section variable {T : Type} - inductive ActionRed (R : T -> T -> Prop) : Subst.Action T -> Subst.Action T -> Prop where + inductive ActionRed (R : T -> T -> Prop) : Action T -> Action T -> Prop where | su {x y} : R x y -> ActionRed R (.su x) (.su y) | re {x} : ActionRed R (.re x) (.re x) @@ -190,7 +189,7 @@ namespace LeanSubst exists q; apply And.intro apply lem.1; apply Star.step ih.2 lem.2 - variable [RenMap T] [SubstMap T T] [Substitutive R] + variable [RenMap T T] [SubstMap T T] [Substitutive R] omit [HasTriangle R] in theorem subst {x y} (σ : Subst T) : Star R x y -> Star R x[σ] y[σ] := by diff --git a/LeanSubst/Types.lean b/LeanSubst/Types.lean deleted file mode 100644 index 74560df..0000000 --- a/LeanSubst/Types.lean +++ /dev/null @@ -1,74 +0,0 @@ - -namespace LeanSubst - -universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} - -structure Ren where - act : Nat -> Nat - -class RenMap (S : Type u1) where - rmap : Ren -> S -> S - -export RenMap (rmap) - -macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t) - -@[app_unexpander rmap] -def unexpand_rmap : Lean.PrettyPrinter.Unexpander -| `($_ $r $t) => `($t⟨$r⟩) -| _ => throw () - -structure HetRen (T : Type u2) where - act : Nat -> Nat - -class HetRenMap (S : Type u1) (T : Type u2) where - hrmap : HetRen T -> S -> S - -export HetRenMap (hrmap) - -macro:max t:term noWs "⟨" r:term "⟩" : term => `(hrmap $r $t) - -@[app_unexpander rmap] -def unexpand_hrmap : Lean.PrettyPrinter.Unexpander -| `($_ $r $t) => `($t⟨$r⟩) -| _ => throw () - -inductive Action (S : Type u1) where -| re : Nat -> Action S -| su : S -> Action S -deriving Repr - -export Action (re su) - -structure Subst (S : Type u1) where - act : Nat -> Action S - -class SubstMap (S : Type u1) where - smap : Subst S -> S -> S - -export SubstMap (smap) - -macro:max t:term noWs "[" σ:term "]" : term => `(smap $σ $t) - -@[app_unexpander smap] -def unexpand_smap : Lean.PrettyPrinter.Unexpander -| `($_ $σ $t) => `($t[$σ]) -| _ => throw () - -structure HetSubst (S : Type u1) (T : Type u2) where - act : Nat -> Action T - -class HetSubstMap (S : Type u1) (T : Type u2) where - hsmap : HetSubst S T -> S -> S - -export HetSubstMap (hsmap) - -macro:max t:term noWs "[" σ:term "]" : term => `(hsmap $σ $t) - -@[app_unexpander smap] -def unexpand_hsmap : Lean.PrettyPrinter.Unexpander -| `($_ $σ $t) => `($t[$σ]) -| _ => throw () - -end LeanSubst diff --git a/LeanSubst/Types/List.lean b/LeanSubst/Types/List.lean new file mode 100644 index 0000000..17ea6d8 --- /dev/null +++ b/LeanSubst/Types/List.lean @@ -0,0 +1,51 @@ + +import LeanSubst.Laws + +namespace LeanSubst + +universe u1 u2 u3 +variable {S : Type u1} {T : Type u2} {U : Type u3} + +def List.rmap [RenMap S T] (r : Ren T) : List S -> List S +| [] => [] +| .cons x xs => x⟨r⟩ :: rmap r xs + +instance [RenMap S T] : RenMap (List S) T where + rmap := List.rmap + +@[simp, grind =] +theorem List.rmap_nil [RenMap S T] {r : Ren T} : (@List.nil S)⟨r⟩ = [] := by + simp [RenMap.rmap, List.rmap] + +@[simp, grind =] +theorem List.rmap_cons [RenMap S T] {x} {xs : List S} {r : Ren T} : (x::xs)⟨r⟩ = x⟨r⟩::xs⟨r⟩ := by + simp [RenMap.rmap, List.rmap] + +instance [RenMap S T] [RenMapId S T] : RenMapId (List S) T where + apply_id := by intro t; induction t <;> simp [*] + +instance [RenMap S T] [RenMapCompose S T] : RenMapCompose (List S) T where + apply_compose := by intro s σ τ; induction s <;> simp [*] + +def List.smap [SubstMap S T] (σ : Subst T) : List S -> List S +| [] => [] +| .cons x xs => x[σ] :: smap σ xs + +instance [SubstMap S T] : SubstMap (List S) T where + smap := List.smap + +@[simp, grind =] +theorem List.smap_none [SubstMap S T] {σ : Subst T} : (@List.nil S)[σ] = [] := by + simp [SubstMap.smap, List.smap] + +@[simp, grind =] +theorem List.smap_some [SubstMap S T] {x} {xs : List S} {σ : Subst T} : (x::xs)[σ] = x[σ]::xs[σ] +:= by simp [SubstMap.smap, List.smap] + +instance [RenMap S T] [SubstMap S T] [SubstMapId S T] : SubstMapId (List S) T where + apply_id := by intro t; induction t <;> simp [*] + +instance [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] : SubstMapCompose (List S) T where + apply_compose := by intro s σ τ; induction s <;> simp [*] + +end LeanSubst diff --git a/LeanSubst/Types/Option.lean b/LeanSubst/Types/Option.lean new file mode 100644 index 0000000..ac46d4f --- /dev/null +++ b/LeanSubst/Types/Option.lean @@ -0,0 +1,51 @@ + +import LeanSubst.Laws + +namespace LeanSubst + +universe u1 u2 u3 +variable {S : Type u1} {T : Type u2} {U : Type u3} + +def Option.rmap [i : RenMap S T] (r : Ren T) : Option S -> Option S +| none => none +| some t => some t⟨r⟩ + +instance [RenMap S T] : RenMap (Option S) T where + rmap := Option.rmap + +@[simp, grind =] +theorem Option.rmap_none [RenMap S T] {r : Ren T} : (@Option.none S)⟨r⟩ = none := by + simp [RenMap.rmap, Option.rmap] + +@[simp, grind =] +theorem Option.rmap_some [RenMap S T] {x : S} {r : Ren T} : (some x)⟨r⟩ = some x⟨r⟩ := by + simp [RenMap.rmap, Option.rmap] + +instance [RenMap S T] [RenMapId S T] : RenMapId (Option S) T where + apply_id := by intro t; cases t <;> simp + +instance [RenMap S T] [RenMapCompose S T] : RenMapCompose (Option S) T where + apply_compose := by intro s σ τ; cases s <;> simp + +def Option.smap [SubstMap S T] (σ : Subst T) : Option S -> Option S +| none => none +| some t => some t[σ] + +instance [SubstMap S T] : SubstMap (Option S) T where + smap := Option.smap + +@[simp, grind =] +theorem Option.smap_none [SubstMap S T] {σ : Subst T} : (@Option.none S)[σ] = none := by + simp [SubstMap.smap, Option.smap] + +@[simp, grind =] +theorem Option.smap_some [SubstMap S T] {x : S} {σ : Subst T} : (some x)[σ] = some x[σ] := by + simp [SubstMap.smap, Option.smap] + +instance [RenMap S T] [SubstMap S T] [SubstMapId S T] : SubstMapId (Option S) T where + apply_id := by intro t; cases t <;> simp + +instance [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] : SubstMapCompose (Option S) T where + apply_compose := by intro s σ τ; cases s <;> simp + +end LeanSubst