diff --git a/Examples/CCOmegaVarSorted/Term.lean b/Examples/CCOmegaVarSorted/Term.lean new file mode 100644 index 0000000..94c0c1c --- /dev/null +++ b/Examples/CCOmegaVarSorted/Term.lean @@ -0,0 +1,150 @@ + +import LeanSubst +open LeanSubst + +namespace CCOmegaVarSorted + +inductive Univ where +| prop +| pred (n : Nat) + +inductive Term where +| var : Univ -> Nat -> Term +| univ : Univ -> Term +| app : Term -> Term -> Term +| lam : Term -> Term -> Term +| pi : Term -> Term -> Term + +---------------------------------------------------------------------------------------------------- +-- Why do we care about annotating variables, or this example in particular? +-- Because it lets us trivially compute the universe of a term: + +def Term.universe : Term -> Univ +| var u _ => u +| univ (.prop) => .pred 0 +| univ (.pred x) => .pred (x + 1) +| app f _ => f.universe +| lam _ t => t.universe +| pi A B => + match A.universe, B.universe with + | .prop, .prop => .prop + | .pred u, .prop => .pred (u + 1) + | .prop, .pred u => .pred (u + 1) + | .pred u1, .pred u2 => .pred ((max u1 u2) + 1) + +-- Without `Univ` annotations on `var` we would need an ambient context +-- (which also means renaming and substitution lemmas..) +-- NOTE: calculation of universes might be off in the `pi` case +---------------------------------------------------------------------------------------------------- + +-- When we promote `Action Term` to `Term` we need to be given whatever annotation data +@[coe] +def Term.from_action (u : Univ) : Action Term -> Term +| re y => var u y +| su t => t + +@[simp, grind =] +theorem Term.from_action_id {n u} : from_action u (𝐬0.act n) = var u n := by + simp [from_action] + +@[simp, grind =] +theorem Term.from_action_succ {n u} : from_action u (𝐬1.act n) = var u (n + 1) := by + simp [from_action] + +@[simp, grind =] +theorem Term.from_acton_re {n u} : from_action u (re n) = var u n := by simp [from_action] + +@[simp, grind =] +theorem Term.from_action_su {t u} : from_action u (su t) = t := by simp [from_action] + +-- The `coe` stuff doesn't make sense anymore, put we can provide reasonable custom notation +-- Perhaps this should be its own typeclass, dunno +notation:max "↑[" u "]" t => Term.from_action u t + +-- instance : Coe (Action Term) Term where +-- coe := Term.from_action + +@[simp] +def Term.rmap (r : Ren Term) : Term -> Term +| var u x => var u (r.act x) +| univ u => univ u +| app t1 t2 => app (t1.rmap r) (t2.rmap r) +| lam t1 t2 => lam (t1.rmap r) (t2.rmap $ r.lift) +| pi t1 t2 => pi (t1.rmap r) (t2.rmap $ r.lift) + +instance : RenMap Term [Term] where + rmap r := Term.rmap r.1 + +@[simp, grind =] +theorem Term.rmap_var {u x} {r : Ren Term} : (var u x)⟨r⟩ = var u (r.act x) := by + simp [RenMap.rmap] + +@[simp, grind =] +theorem Term.rmap_univ {u} {r : Ren Term} : (univ u)⟨r⟩ = univ u := by + simp [RenMap.rmap] + +@[simp, grind =] +theorem Term.rmap_app {t1 t2} {r : Ren Term} : (app t1 t2)⟨r⟩ = app t1⟨r⟩ t2⟨r⟩ := by + simp [RenMap.rmap] + +@[simp, grind =] +theorem Term.rmap_lam {t1 t2} {r : Ren Term} : (lam t1 t2)⟨r⟩ = lam t1⟨r⟩ t2⟨r.lift⟩ := by + simp [RenMap.rmap] + +@[simp, grind =] +theorem Term.rmap_pi {t1 t2} {r : Ren Term} : (pi t1 t2)⟨r⟩ = pi t1⟨r⟩ t2⟨r.lift⟩ := by + simp [RenMap.rmap] + +instance : RenMapId Term [Term] where + apply_id := by subst_solve_id + +instance : RenMapCompose Term [Term] where + apply_compose := by sorry + +@[simp] +def Term.smap (σ : Subst Term) : Term -> Term +| var u x => ↑[u] σ.act x +| univ u => univ u +| app t1 t2 => app (t1.smap σ) (t2.smap σ) +| lam t1 t2 => lam (t1.smap σ) (t2.smap $ σ.lift) +| pi t1 t2 => pi (t1.smap σ) (t2.smap $ σ.lift) + +instance : SubstMap Term [Term] where + smap σ := Term.smap σ.1 + +@[simp, grind =] +theorem Term.smap_var {u x} {σ : Subst Term} : (var u x)[σ] = ↑[u] σ.act x := by + simp [SubstMap.smap] + +@[simp, grind =] +theorem Term.smap_univ {u} {σ : Subst Term} : (univ u)[σ] = univ u := by + simp [SubstMap.smap] + +@[simp, grind =] +theorem Term.smap_app {t1 t2 : Term} {σ : Subst Term} : (app t1 t2)[σ] = app t1[σ] t2[σ] := by + simp [SubstMap.smap] + +@[simp, grind =] +theorem Term.smap_lam {t1 t2 : Term} {σ : Subst Term} : (lam t1 t2)[σ] = lam t1[σ] t2[σ.lift] := by + simp [SubstMap.smap] + +@[simp, grind =] +theorem Term.smap_pi {t1 t2 : Term} {σ : Subst Term} : (pi t1 t2)[σ] = pi t1[σ] t2[σ.lift] := by + simp [SubstMap.smap] + +instance : SubstMapId Term [Term] where + apply_id := by sorry + +instance : SubstMapStable Term [Term] where + apply_stable := by sorry + +instance : SubstMapRenComposeLeft Term [Term] where + apply_ren_compose_left := by sorry + +instance : SubstMapRenComposeRight Term [Term] where + apply_ren_compose_right := by sorry + +instance : SubstMapCompose Term [Term] where + apply_compose := by sorry + +end CCOmegaVarSorted diff --git a/Examples/LambdaCalc.lean b/Examples/LambdaCalc.lean index 4ae9aa6..72b6065 100644 --- a/Examples/LambdaCalc.lean +++ b/Examples/LambdaCalc.lean @@ -3,113 +3,113 @@ open LeanSubst namespace Examples.LambdaCalc - inductive Term where - | var : Nat -> Term - | app : Term -> Term -> Term - | lam : Term -> Term - - prefix:100 ":λ " => Term.lam - infixl:65 " :@ " => Term.app - - @[coe] - def Term.from_action : Action Term -> Term - | re y => var y - | su t => t - - @[simp, grind =] - theorem Term.from_action_id {n} : from_action (+0σ.act n) = var n := by - simp [from_action] - - @[simp, grind =] - theorem Term.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by - simp [from_action] - - @[simp, grind =] - theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] - - @[simp, grind =] - theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] - - instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where - coe := Term.from_action - - @[simp] - 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 Term where - rmap := rmap - - @[simp, grind =] - 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 Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by - simp [RenMap.rmap] - - instance : RenMapId Term Term where - apply_id := by subst_solve_id - - instance : RenMapCompose Term Term where - apply_compose := by subst_solve_compose - - @[simp] - def smap (σ : Subst Term) : Term -> Term - | .var x => σ.act x - | t1 :@ t2 => smap σ t1 :@ smap σ t2 - | :λ t => :λ smap σ.lift t - - instance SubstMap_Term : SubstMap Term Term where - smap := smap - - @[simp, grind =] - theorem subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ.act x := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem subst_app {t1 t2} {σ : Subst Term} : (t1 :@ t2)[σ] = t1[σ] :@ t2[σ] := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem subst_lam {t} {σ : Subst Term} : (:λ t)[σ] = :λ t[σ.lift] := by - simp [SubstMap.smap] - - @[simp] - theorem Term.from_action_compose {x : Nat} {σ τ : Subst Term} - : (from_action (Subst.act σ x))[τ] = from_action ((σ ∘ τ).act x) - := by - simp [from_action, Subst.compose] - generalize zdef : σ.act x = z - cases z <;> simp [from_action] - - @[simp] - theorem Term.from_action_compose_ren {x : Nat} {σ : 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 Term where - apply_stable := by subst_solve_stable - - instance : SubstMapRenComposeLeft Term Term where - apply_ren_compose_left := by subst_solve_compose + -- inductive Term where + -- | var : Nat -> Term + -- | app : Term -> Term -> Term + -- | lam : Term -> Term + + -- prefix:100 ":λ " => Term.lam + -- infixl:65 " :@ " => Term.app + + -- @[coe] + -- def Term.from_action : Action Term -> Term + -- | re y => var y + -- | su t => t + + -- @[simp, grind =] + -- theorem Term.from_action_id {n} : from_action (+0σ.act n) = var n := by + -- simp [from_action] + + -- @[simp, grind =] + -- theorem Term.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by + -- simp [from_action] + + -- @[simp, grind =] + -- theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + + -- @[simp, grind =] + -- theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] + + -- instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where + -- coe := Term.from_action + + -- @[simp] + -- 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 Term where + -- rmap := rmap + + -- @[simp, grind =] + -- 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 Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by + -- simp [RenMap.rmap] + + -- @[simp, grind =] + -- theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by + -- simp [RenMap.rmap] + + -- instance : RenMapId Term Term where + -- apply_id := by subst_solve_id + + -- instance : RenMapCompose Term Term where + -- apply_compose := by subst_solve_compose + + -- @[simp] + -- def smap (σ : Subst Term) : Term -> Term + -- | .var x => σ.act x + -- | t1 :@ t2 => smap σ t1 :@ smap σ t2 + -- | :λ t => :λ smap σ.lift t + + -- instance SubstMap_Term : SubstMap Term Term where + -- smap := smap + + -- @[simp, grind =] + -- theorem subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ.act x := by + -- simp [SubstMap.smap] + + -- @[simp, grind =] + -- theorem subst_app {t1 t2} {σ : Subst Term} : (t1 :@ t2)[σ] = t1[σ] :@ t2[σ] := by + -- simp [SubstMap.smap] + + -- @[simp, grind =] + -- theorem subst_lam {t} {σ : Subst Term} : (:λ t)[σ] = :λ t[σ.lift] := by + -- simp [SubstMap.smap] + + -- @[simp] + -- theorem Term.from_action_compose {x : Nat} {σ τ : Subst Term} + -- : (from_action (Subst.act σ x))[τ] = from_action ((σ ∘ τ).act x) + -- := by + -- simp [from_action, Subst.compose] + -- generalize zdef : σ.act x = z + -- cases z <;> simp [from_action] + + -- @[simp] + -- theorem Term.from_action_compose_ren {x : Nat} {σ : 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 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 - apply_ren_compose_right := by subst_solve_compose + -- instance : SubstMapRenComposeRight Term Term where + -- apply_ren_compose_right := by subst_solve_compose - instance : SubstMapCompose Term Term where - apply_compose := by subst_solve_compose + -- instance : SubstMapCompose Term Term where + -- apply_compose := by subst_solve_compose end Examples.LambdaCalc diff --git a/Examples/LambdaCalcKit.lean b/Examples/LambdaCalcKit.lean index c342e66..cbc012f 100644 --- a/Examples/LambdaCalcKit.lean +++ b/Examples/LambdaCalcKit.lean @@ -2,137 +2,137 @@ import LeanSubst namespace LeanSubst.Examples.LambdaCalc - inductive Term where - | var : Nat -> Term - | app : Term -> Term -> Term - | lam : Term -> Term + -- inductive Term where + -- | var : Nat -> Term + -- | app : Term -> Term -> Term + -- | lam : Term -> Term - prefix:100 ":λ " => Term.lam - infixl:65 " :@ " => Term.app - - @[coe] - def Term.from_action : Action Term -> Term - | re y => var y - | su t => t - - @[simp, grind =] - theorem Term.from_action_id {n} : from_action (+0σ.act n) = var n := by - simp [from_action, Subst.id] - - @[simp, grind =] - theorem Term.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by - simp [from_action, Subst.succ] - - @[simp, grind =] - theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] - - @[simp, grind =] - theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] + -- prefix:100 ":λ " => Term.lam + -- infixl:65 " :@ " => Term.app + + -- @[coe] + -- def Term.from_action : Action Term -> Term + -- | re y => var y + -- | su t => t + + -- @[simp, grind =] + -- theorem Term.from_action_id {n} : from_action (+0σ.act n) = var n := by + -- simp [from_action, Subst.id] + + -- @[simp, grind =] + -- theorem Term.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by + -- simp [from_action, Subst.succ] + + -- @[simp, grind =] + -- theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + + -- @[simp, grind =] + -- theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] - instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where - coe := Term.from_action + -- instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where + -- coe := Term.from_action - @[simp] - def Term.ren_act (r : Ren Term) : Term -> Term - | .var x => .var (r.act x) - | t => t - - @[simp] - def Term.subst_act (σ : Subst Term) : Term -> Term - | .var x => σ.act x - | t => t - - class Kit (T : Type) (A : Type) where - act (f : A) : T -> T - lift (f : A) (k : Nat := 1) : A - - @[simp] - instance : Kit Term (Ren Term) where - act := Term.ren_act - lift f n := Ren.lift f n - - @[simp] - instance [RenMap Term Term] : Kit Term (Subst Term) where - act := Term.subst_act - lift f n := Subst.lift f n - - @[simp] - def kitmap {A} (σ : A) [kit : Kit Term A] : Term -> Term - | .var x => kit.act σ (.var x) - | t1 :@ t2 => kitmap σ t1 :@ kitmap σ t2 - | :λ t => :λ kitmap (kit.lift σ) t - - @[simp] - def rmap (r : Ren Term) : Term -> Term := kitmap r - - instance : RenMap Term Term where - rmap := rmap - - @[simp, grind =] - 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 Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by - simp +instances [RenMap.rmap] - - instance : RenMapId Term Term where - apply_id := by intro t; induction t <;> simp [*] - - instance : RenMapCompose Term Term where - apply_compose := by subst_solve_compose - - @[simp] - def smap (σ : Subst Term) : Term -> Term := kitmap σ - - instance SubstMap_Term : SubstMap Term Term where - smap := smap - - @[simp, grind =] - theorem subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ.act x := by - simp +instances [SubstMap.smap] - - @[simp, grind =] - theorem subst_app {t1 t2} {σ : Subst Term} : (t1 :@ t2)[σ] = t1[σ] :@ t2[σ] := by - simp +instances [SubstMap.smap] - - @[simp, grind =] - theorem subst_lam {t} {σ : Subst Term} : (:λ t)[σ] = :λ t[σ.lift] := by - simp +instances [SubstMap.smap] + -- @[simp] + -- def Term.ren_act (r : Ren Term) : Term -> Term + -- | .var x => .var (r.act x) + -- | t => t + + -- @[simp] + -- def Term.subst_act (σ : Subst Term) : Term -> Term + -- | .var x => σ.act x + -- | t => t + + -- class Kit (T : Type) (A : Type) where + -- act (f : A) : T -> T + -- lift (f : A) (k : Nat := 1) : A + + -- @[simp] + -- instance : Kit Term (Ren Term) where + -- act := Term.ren_act + -- lift f n := Ren.lift f n + + -- @[simp] + -- instance [RenMap Term Term] : Kit Term (Subst Term) where + -- act := Term.subst_act + -- lift f n := Subst.lift f n + + -- @[simp] + -- def kitmap {A} (σ : A) [kit : Kit Term A] : Term -> Term + -- | .var x => kit.act σ (.var x) + -- | t1 :@ t2 => kitmap σ t1 :@ kitmap σ t2 + -- | :λ t => :λ kitmap (kit.lift σ) t + + -- @[simp] + -- def rmap (r : Ren Term) : Term -> Term := kitmap r + + -- instance : RenMap Term Term where + -- rmap := rmap + + -- @[simp, grind =] + -- 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 Term} : (t1 :@ t2)⟨r⟩ = t1⟨r⟩ :@ t2⟨r⟩ := by + -- simp [RenMap.rmap] + + -- @[simp, grind =] + -- theorem ren_lam {t} {r : Ren Term} : (:λ t)⟨r⟩ = :λ t⟨r.lift⟩ := by + -- simp +instances [RenMap.rmap] + + -- instance : RenMapId Term Term where + -- apply_id := by intro t; induction t <;> simp [*] + + -- instance : RenMapCompose Term Term where + -- apply_compose := by subst_solve_compose + + -- @[simp] + -- def smap (σ : Subst Term) : Term -> Term := kitmap σ + + -- instance SubstMap_Term : SubstMap Term Term where + -- smap := smap + + -- @[simp, grind =] + -- theorem subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ.act x := by + -- simp +instances [SubstMap.smap] + + -- @[simp, grind =] + -- theorem subst_app {t1 t2} {σ : Subst Term} : (t1 :@ t2)[σ] = t1[σ] :@ t2[σ] := by + -- simp +instances [SubstMap.smap] + + -- @[simp, grind =] + -- theorem subst_lam {t} {σ : Subst Term} : (:λ t)[σ] = :λ t[σ.lift] := by + -- simp +instances [SubstMap.smap] - @[simp] - theorem Term.from_action_compose {x : Nat} {σ τ : Subst Term} - : (from_action (σ.act x))[τ] = from_action ((σ ∘ τ).act x) - := by - simp [Term.from_action, Subst.compose] - generalize zdef : σ.act x = z - cases z <;> simp [Term.from_action] + -- @[simp] + -- theorem Term.from_action_compose {x : Nat} {σ τ : Subst Term} + -- : (from_action (σ.act x))[τ] = from_action ((σ ∘ τ).act x) + -- := by + -- simp [Term.from_action, Subst.compose] + -- generalize zdef : σ.act x = z + -- cases z <;> simp [Term.from_action] - @[simp] - theorem Term.from_action_compose_ren {x : Nat} {σ : 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 + -- @[simp] + -- theorem Term.from_action_compose_ren {x : Nat} {σ : 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 : SubstMapId Term Term where + -- apply_id := by subst_solve_id - instance : SubstMapStable Term Term where - apply_stable := by subst_solve_stable + -- 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 : SubstMapRenComposeLeft Term Term where + -- apply_ren_compose_left := by subst_solve_compose - instance : SubstMapRenComposeRight Term Term where - apply_ren_compose_right := by subst_solve_compose + -- instance : SubstMapRenComposeRight Term Term where + -- apply_ren_compose_right := by subst_solve_compose - instance : SubstMapCompose Term Term where - apply_compose := by subst_solve_compose + -- instance : SubstMapCompose Term Term where + -- apply_compose := by subst_solve_compose end LeanSubst.Examples.LambdaCalc diff --git a/Examples/STLC/Term.lean b/Examples/STLC/Term.lean new file mode 100644 index 0000000..ee8049c --- /dev/null +++ b/Examples/STLC/Term.lean @@ -0,0 +1,128 @@ + +import LeanSubst +open LeanSubst + +namespace STLC + +inductive Ty where +| base : Ty +| arrow : Ty -> Ty + +notation "★" => Ty.base +infixr:64 " -:> " => Ty.arrow + +inductive Term where +| var : Nat -> Term +| app : Term -> Term -> Term +| lam : Ty -> Term -> Term + +prefix:max "#" => Term.var +notation "λ[" A "]" t => Term.lam A t + +@[simp] +instance : HSMul Term Term Term where + hSMul := Term.app + +@[coe] +def Term.from_action : Action Term -> Term +| re y => var y +| su t => t + +@[simp, grind =] +theorem Term.from_action_id {n} : from_action (𝐬0.act n) = var n := by + simp [from_action] + +@[simp, grind =] +theorem Term.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by + simp [from_action] + +@[simp, grind =] +theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + +@[simp, grind =] +theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] + +instance : Coe (Action Term) Term where + coe := Term.from_action + +@[simp] +def Term.rmap (r : Ren Term) : Term -> Term +| var x => var (r.act x) +| app t1 t2 => app (t1.rmap r) (t2.rmap r) +| λ[A] t => λ[A] t.rmap r.lift + +instance : RenMap Term [Term] where + rmap r := Term.rmap r.1 + +@[simp, grind =] +theorem Term.rmap_var {x} {r : Ren Term} : (#x)⟨r⟩ = .var (r.act x) := by + simp [RenMap.rmap] + +@[simp, grind =] +theorem Term.rmap_app {t1 t2 : Term} {r : Ren Term} : (app t1 t2)⟨r⟩ = app t1⟨r⟩ t2⟨r⟩ := by + simp +instances [RenMap.rmap] + +@[simp, grind =] +theorem Term.rmap_lam {A t} {r : Ren Term} : (λ[A] t)⟨r⟩ = λ[A] t⟨r.lift⟩ := by + simp [RenMap.rmap] + +instance : RenMapId Term [Term] where + apply_id := by subst_solve_id + +instance : RenMapCompose Term [Term] where + apply_compose := by sorry + +@[simp] +def Term.smap (σ : Subst Term) : Term -> Term +| var x => σ.act x +| app t1 t2 => app (t1.smap σ) (t2.smap σ) +| λ[A] t => λ[A] t.smap σ.lift + +instance : SubstMap Term [Term] where + smap σ := Term.smap σ.1 + +@[simp, grind =] +theorem Term.smap_var {x} {σ : SubstVec [Term]} : (#x)[σ,] = from_action (σ.1.act x) := by + simp [SubstMap.smap] + +@[simp, grind =] +theorem Term.smap_app {t1 t2 : Term} {σ : SubstVec [Term]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by + simp +instances [SubstMap.smap] + +@[simp, grind =] +theorem Term.smap_lam {A t} {σ : SubstVec [Term]} : (λ[A] t)[σ,] = λ[A] t[σ.lift,] := by + simp [-Subst.rewrite_lift, SubstMap.smap]; sorry + +instance : SubstMapId Term [Term] where + apply_id := by sorry + +instance : SubstMapStable Term [Term] where + apply_stable := by sorry + +instance : SubstMapRenComposeLeft Term [Term] where + apply_ren_compose_left := by sorry + +instance : SubstMapRenComposeRight Term [Term] where + apply_ren_compose_right := by sorry + +instance : SubstMapCompose Term [Term] where + apply_compose := by + intro s σ τ + induction s generalizing σ τ + case var => + simp + sorry + case app => simp [*] + case lam => + simp [*] + sorry + -- any_goals solve | simp_all +instances [List.Tuple] + -- try any_goals solve | ( + -- try simp_all +instances [List.Tuple] + -- try simp [-Subst.rewrite_lift, *] + -- try funext; case _ x => + -- try rw [<-Ren.to_lift] + -- try simp [-Subst.rewrite_lift, *] + -- try grind) + +end STLC diff --git a/Examples/SystemF.lean b/Examples/SystemF.lean index f4508f2..9f2f0eb 100644 --- a/Examples/SystemF.lean +++ b/Examples/SystemF.lean @@ -3,371 +3,386 @@ open LeanSubst namespace Examples.SystemF - inductive Ty where - | var : Nat -> Ty - | arr : Ty -> Ty -> Ty - | all : Ty -> Ty - - prefix:max "t#" => Ty.var - infixr:85 "-:>" => Ty.arr - notation ":∀" t => Ty.all t - - inductive Term where - | var : Nat -> Term - | app : Term -> Term -> Term - | lam : Ty -> Term -> Term - | tapp : Term -> Ty -> Term - | tlam : Term -> Term - - prefix:max "#" => Term.var - infixl:65 "•" => Term.app - notation:100 "λ[" A "]" t => Term.lam A t - notation:65 f "•[" a "]" => Term.tapp f a - notation:100 "Λ" t => Term.tlam t - ----------------------------------------------------------------------------------------------------- ----- Ty setup ----------------------------------------------------------------------------------------------------- - @[coe] - def Ty.from_action : Action Ty -> Ty - | re y => t#y - | su t => t - - @[simp, grind =] - theorem Ty.from_action_id {n} : from_action (+0σ.act n) = var n := by - simp [from_action] - - @[simp, grind =] - theorem Ty.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by - simp [from_action] - - @[simp, grind =] - theorem Ty.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] - - @[simp, grind =] - theorem Ty.from_action_su {t} : from_action (su t) = t := by simp [from_action] - - instance : Coe (Action Ty) Ty where - coe := Ty.from_action - - @[simp] - def Ty.rmap (r : Ren Ty) : Ty -> Ty - | t#x => t#(r.act x) - | t1 -:> t2 => rmap r t1 -:> rmap r t2 - | :∀ t => :∀ rmap r.lift t - - instance : RenMap Ty Ty where - rmap := Ty.rmap - - @[simp, grind =] - theorem Ty.ren_var {x} {r : Ren Ty} : (Ty.var x)⟨r⟩ = .var (r.act x) := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem Ty.ren_arr {t1 t2} {r : Ren Ty} : (t1 -:> t2)⟨r⟩ = t1⟨r⟩ -:> t2⟨r⟩ := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem Ty.ren_all {t} {r : Ren Ty} : (:∀ t)⟨r⟩ = :∀ t⟨r.lift⟩ := by - simp [RenMap.rmap] - - instance : RenMapId Ty Ty where - apply_id := by subst_solve_id - - instance : RenMapCompose Ty Ty where - apply_compose := by subst_solve_compose - - @[simp] - def Ty.smap (σ : Subst Ty) : Ty -> Ty - | t#x => σ.act x - | t1 -:> t2 => smap σ t1 -:> smap σ t2 - | :∀ t => :∀ smap σ.lift t - - instance : SubstMap Ty Ty where - smap := Ty.smap - - @[simp, grind =] - theorem Ty.subst_var {x} {σ : Subst Ty} : (Ty.var x)[σ] = σ.act x := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Ty.subst_arr {t1 t2} {σ : Subst Ty} : (t1 -:> t2)[σ] = t1[σ] -:> t2[σ] := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Ty.subst_all {t} {σ : Subst Ty} : (:∀ t)[σ] = :∀ t[σ.lift] := by - simp [SubstMap.smap] - - @[simp] - theorem Ty.from_action_compose {x : Nat} {σ τ : Subst Ty} - : (from_action (Subst.act σ x))[τ] = from_action ((σ ∘ τ).act x) - := by - simp [from_action, Subst.compose] - generalize zdef : σ.act x = z - cases z <;> simp [from_action] - - @[simp] - theorem Ty.from_action_compose_ren {x : Nat} {σ : Subst Ty} {r : Ren Ty} - : (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x) - := by - simp [Ty.from_action] - generalize zdef : σ.act x = z - cases z <;> simp - - instance : SubstMapId Ty Ty where - apply_id := by subst_solve_id - - instance : SubstMapStable Ty Ty where - apply_stable := by subst_solve_stable - - instance : SubstMapRenComposeLeft Ty Ty where - apply_ren_compose_left := by subst_solve_compose - - instance : SubstMapRenComposeRight Ty Ty where - apply_ren_compose_right := by subst_solve_compose - - instance : SubstMapCompose Ty Ty where - apply_compose := by subst_solve_compose - ----------------------------------------------------------------------------------------------------- ----- Term setup ----------------------------------------------------------------------------------------------------- - @[coe] - def Term.from_action : Action Term -> Term - | re y => var y - | su t => t - - @[simp, grind =] - theorem Term.from_action_id {n} : from_action (+0σ.act n) = var n := by - simp [from_action] - - @[simp, grind =] - theorem Term.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by - simp [from_action] - - @[simp, grind =] - theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] - - @[simp, grind =] - theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] - - instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where - coe := Term.from_action - - @[simp] - def Term.Ty.rmap (r : Ren Ty) : Term -> Term - | #x => #x - | app t1 t2 => (rmap r t1) • (rmap r t2) - | λ[A] t => λ[A⟨r⟩] rmap r t - | t1 •[t2] => rmap r t1 •[t2⟨r⟩] - | Λ t => Λ rmap r.lift t - - instance : RenMap Term Ty where - rmap := Term.Ty.rmap - - @[simp, grind =] - theorem Term.Ty.ren_var {x} {r : Ren Ty} : (#x)⟨r⟩ = #x := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem Term.Ty.ren_app {t1 t2} {r : Ren Ty} : (t1 • t2)⟨r⟩ = t1⟨r⟩ • t2⟨r⟩ := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem Term.Ty.ren_lam {A t} {r : Ren Ty} : (λ[A] t)⟨r⟩ = λ[A⟨r⟩] t⟨r⟩ := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem Term.Ty.ren_tapp {t1 t2} {r : Ren Ty} : (t1 •[t2])⟨r⟩ = t1⟨r⟩ •[t2⟨r⟩] := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem Term.Ty.ren_tlam {t} {r : Ren Ty} : (Λ t)⟨r⟩ = Λ t⟨r.lift⟩ := by - simp [RenMap.rmap] - - instance : RenMapId Term Ty where - apply_id := by subst_solve_id - - instance : RenMapCompose Term Ty where - apply_compose := by subst_solve_compose - - @[simp] - def Term.rmap (r : Ren Term) : Term -> Term - | #x => #(r.act x) - | app t1 t2 => rmap r t1 • rmap r t2 - | λ[A] t => λ[A] rmap r.lift t - | t1 •[t2] => rmap r t1 •[t2] - | Λ t => Λ rmap r t - - instance : RenMap Term Term where - rmap := Term.rmap - - @[simp, grind =] - theorem Term.ren_var {x} {r : Ren Term} : (Term.var x)⟨r⟩ = .var (r.act x) := by - simp [RenMap.rmap] +-- inductive Ty where +-- | var : Nat -> Ty +-- | arr : Ty -> Ty -> Ty +-- | all : Ty -> Ty + +-- prefix:max "t#" => Ty.var +-- infixr:85 "-:>" => Ty.arr +-- notation ":∀" t => Ty.all t + +-- inductive Term where +-- | var : Nat -> Term +-- | app : Term -> Term -> Term +-- | lam : Ty -> Term -> Term +-- | tapp : Term -> Ty -> Term +-- | tlam : Term -> Term + +-- prefix:max "#" => Term.var +-- infixl:65 "•" => Term.app +-- notation:100 "λ[" A "]" t => Term.lam A t +-- notation:65 f "•[" a "]" => Term.tapp f a +-- notation:100 "Λ" t => Term.tlam t + +-- ---------------------------------------------------------------------------------------------------- +-- ---- Ty setup +-- ---------------------------------------------------------------------------------------------------- +-- @[coe] +-- def Ty.from_action : Action Ty -> Ty +-- | re y => t#y +-- | su t => t + +-- @[simp, grind =] +-- theorem Ty.from_action_id {n} : from_action (+0σ.act n) = var n := by +-- simp [from_action] + +-- @[simp, grind =] +-- theorem Ty.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by +-- simp [from_action] + +-- @[simp, grind =] +-- theorem Ty.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + +-- @[simp, grind =] +-- theorem Ty.from_action_su {t} : from_action (su t) = t := by simp [from_action] + +-- instance : Coe (Action Ty) Ty where +-- coe := Ty.from_action + +-- @[simp] +-- def Ty.rmap (r : Ren Ty) : Ty -> Ty +-- | t#x => t#(r.act x) +-- | t1 -:> t2 => rmap r t1 -:> rmap r t2 +-- | :∀ t => :∀ rmap r.lift t + +-- instance : RenMap Ty Ty where +-- rmap := Ty.rmap + +-- @[simp, grind =] +-- theorem Ty.ren_var {x} {r : Ren Ty} : (Ty.var x)⟨r⟩ = .var (r.act x) := by +-- simp [RenMap.rmap] - @[simp, grind =] - theorem Term.ren_app {t1 t2} {r : Ren Term} : (t1 • t2)⟨r⟩ = t1⟨r⟩ • t2⟨r⟩ := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem Term.ren_lam {A t} {r : Ren Term} : (λ[A] t)⟨r⟩ = λ[A] t⟨r.lift⟩ := by - simp [RenMap.rmap] +-- @[simp, grind =] +-- theorem Ty.ren_arr {t1 t2} {r : Ren Ty} : (t1 -:> t2)⟨r⟩ = t1⟨r⟩ -:> t2⟨r⟩ := by +-- simp [RenMap.rmap] - @[simp, grind =] - theorem Term.ren_tapp {t1 t2} {r : Ren Term} : (t1 •[t2])⟨r⟩ = t1⟨r⟩ •[t2] := by - simp [RenMap.rmap] - - @[simp, grind =] - theorem Term.ren_tlam {t} {r : Ren Term} : (Λ t)⟨r⟩ = Λ t⟨r⟩ := by - simp [RenMap.rmap] - - instance : RenMapId Term Term where - apply_id := by subst_solve_id - - instance : RenMapCompose Term Term where - apply_compose := by subst_solve_compose - - @[simp] - def Term.Ty.smap (σ : Subst Ty) : Term -> Term - | #x => #x - | app t1 t2 => smap σ t1 • smap σ t2 - | λ[A] t => λ[A[σ]] smap σ t - | t1 •[t2] => smap σ t1 •[t2[σ]] - | Λ t => Λ smap σ.lift t - - instance : SubstMap Term Ty where - smap := Term.Ty.smap - - @[simp, grind =] - theorem Term.Ty.subst_var {x} {σ : Subst Ty} : (#x)[σ] = #x := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Term.Ty.subst_app {t1 t2} {σ : Subst Ty} : (t1 • t2)[σ] = t1[σ] • t2[σ] := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Term.Ty.subst_lam {A t} {σ : Subst Ty} : (λ[A] t)[σ] = λ[A[σ]] t[σ] := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Term.Ty.subst_tapp {t1 t2} {σ : Subst Ty} : (t1 •[t2])[σ] = t1[σ] •[t2[σ]] := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Term.Ty.subst_tlam {t} {σ : Subst Ty} : (Λ t)[σ] = Λ t[σ.lift] := by - simp [SubstMap.smap] - - instance : SubstMapId Term Ty where - apply_id := by subst_solve_id - - instance : SubstMapStable Term Ty where - apply_stable := by subst_solve_stable - - instance : SubstMapRenComposeLeft Term Ty where - apply_ren_compose_left := by subst_solve_compose - - instance : SubstMapRenComposeRight Term Ty where - apply_ren_compose_right := by subst_solve_compose - - instance : SubstMapCompose Term Ty where - apply_compose := by subst_solve_compose - - @[simp] - def Term.smap (σ : Subst Term) : Term -> Term - | #x => σ.act x - | app t1 t2 => smap σ t1 • smap σ t2 - | λ[A] t => λ[A] smap σ.lift t - | t1 •[t2] => smap σ t1 •[t2] - | Λ t => Λ smap (σ ◾ Ren.succ Ty) t - - instance : SubstMap Term Term where - smap := Term.smap - - @[simp, grind =] - theorem Term.subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ.act x := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Term.subst_app {t1 t2} {σ : Subst Term} : (t1 • t2)[σ] = t1[σ] • t2[σ] := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Term.subst_lam {A t} {σ : Subst Term} : (λ[A] t)[σ] = λ[A] t[σ.lift] := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Term.subst_tapp {t1 t2} {σ : Subst Term} : (t1 •[t2])[σ] = t1[σ] •[t2] := by - simp [SubstMap.smap] - - @[simp, grind =] - theorem Term.subst_tlam {t} {σ : Subst Term} : (Λ t)[σ] = Λ t[σ ◾ Ren.succ Ty] := by - simp [SubstMap.smap] - - @[simp] - theorem Term.from_action_compose {x : Nat} {σ τ : Subst Term} - : (from_action (σ.act x))[τ] = from_action ((σ ∘ τ).act x) - := by - simp [from_action, Subst.compose] - generalize zdef : σ.act x = z - cases z <;> simp [from_action] - - @[simp] - theorem Term.from_action_hcompose {x : Nat} {σ : Subst Term} {τ : Subst Ty} - : (from_action (σ.act x))[τ] = from_action ((σ ◾ τ).act x) - := by - simp [from_action] - generalize zdef : σ.act x = z - cases z <;> simp - - @[simp] - theorem Term.from_action_compose_ren {x : Nat} {σ : 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 - - @[simp] - theorem Term.from_action_hcompose_ren {x : Nat} {σ : Subst Term} {r : Ren Ty} - : (from_action (σ.act x))⟨r⟩ = from_action ((σ ◾ r).act x) - := by - simp [Term.from_action] - generalize zdef : σ.act x = z - cases z <;> simp - - instance : SubstMapRenCommute Term Ty where - apply_commute_ren_subst := by subst_solve_compose - apply_commute_ren_ren := by subst_solve_compose - - instance : SubstMapRenHetCompose Term Ty where - apply_hcompose_ren := by subst_solve_compose - - instance : SubstMapHetCompose Term Ty where - apply_hcompose := by subst_solve_compose - - instance : SubstMapId Term Term where - apply_id := by subst_solve_id - - -- instance : SubstMapStable Term Term where - -- apply_stable := by - -- intro r σ h - -- funext; case _ t => - -- induction t generalizing r σ - -- all_goals simp [*] at *; try simp +instances [*] - -- all_goals try solve | rw [Subst.apply_stable h] - -- all_goals try solve | (rw [<-h]; simp +instances [Ren.to]) - -- all_goals try repeat funext; grind - -- --subst_solve_stable - - instance : SubstMapRenComposeLeft Term Term where - apply_ren_compose_left := by subst_solve_compose - - instance : SubstMapRenComposeRight Term Term where - apply_ren_compose_right := by subst_solve_compose - - instance : SubstMapCompose Term Term where - apply_compose := by subst_solve_compose +-- @[simp, grind =] +-- theorem Ty.ren_all {t} {r : Ren Ty} : (:∀ t)⟨r⟩ = :∀ t⟨r.lift⟩ := by +-- simp [RenMap.rmap] + +-- instance : RenMapId Ty Ty where +-- apply_id := by subst_solve_id + +-- instance : RenMapCompose Ty Ty where +-- apply_compose := by subst_solve_compose + +-- @[simp] +-- def Ty.smap (σ : Subst Ty) : Ty -> Ty +-- | t#x => σ.act x +-- | t1 -:> t2 => smap σ t1 -:> smap σ t2 +-- | :∀ t => :∀ smap σ.lift t + +-- instance : SubstMap Ty Ty where +-- smap := Ty.smap + +-- @[simp, grind =] +-- theorem Ty.subst_var {x} {σ : Subst Ty} : (Ty.var x)[σ] = σ.act x := by +-- simp [SubstMap.smap] + +-- @[simp, grind =] +-- theorem Ty.subst_arr {t1 t2} {σ : Subst Ty} : (t1 -:> t2)[σ] = t1[σ] -:> t2[σ] := by +-- simp [SubstMap.smap] + +-- @[simp, grind =] +-- theorem Ty.subst_all {t} {σ : Subst Ty} : (:∀ t)[σ] = :∀ t[σ.lift] := by +-- simp [SubstMap.smap] + +-- @[simp] +-- theorem Ty.from_action_compose {x : Nat} {σ τ : Subst Ty} +-- : (from_action (Subst.act σ x))[τ] = from_action ((σ ∘ τ).act x) +-- := by +-- simp [from_action, Subst.compose] +-- generalize zdef : σ.act x = z +-- cases z <;> simp [from_action] + +-- @[simp] +-- theorem Ty.from_action_compose_ren {x : Nat} {σ : Subst Ty} {r : Ren Ty} +-- : (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x) +-- := by +-- simp [Ty.from_action] +-- generalize zdef : σ.act x = z +-- cases z <;> simp + +-- instance : SubstMapId Ty Ty where +-- apply_id := by subst_solve_id + +-- instance : SubstMapStable Ty Ty where +-- apply_stable := by subst_solve_stable + +-- instance : SubstMapRenComposeLeft Ty Ty where +-- apply_ren_compose_left := by subst_solve_compose + +-- instance : SubstMapRenComposeRight Ty Ty where +-- apply_ren_compose_right := by subst_solve_compose + +-- instance : SubstMapCompose Ty Ty where +-- apply_compose := by subst_solve_compose + +-- ---------------------------------------------------------------------------------------------------- +-- ---- Term setup +-- ---------------------------------------------------------------------------------------------------- +-- @[coe] +-- def Term.from_action : Action Term -> Term +-- | re y => var y +-- | su t => t + +-- @[simp, grind =] +-- theorem Term.from_action_id {n} : from_action (+0σ.act n) = var n := by +-- simp [from_action] + +-- @[simp, grind =] +-- theorem Term.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by +-- simp [from_action] + +-- @[simp, grind =] +-- theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + +-- @[simp, grind =] +-- theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] + +-- instance instCoe_SubstActionTerm_Term : Coe (Action Term) Term where +-- coe := Term.from_action + +-- universe u + + + +-- def test : Fin 2 -> Bool := #⟨true, false⟩ + +-- def ListRen (α : List (Type u)) := Vector + +-- structure ListRen (α : List (Type u)) where +-- act {i} {h : i < α.length} : Ren α[i] + +-- def ex1 : ListRen [Term, Term] := .mk #v[λ x => x, λ x => x] + +-- def Term.rmap (r : ListRen [Term, Ty]) + +-- -- @[simp] +-- -- def Term.Ty.rmap (r : Ren Ty) : Term -> Term +-- -- | #x => #x +-- -- | app t1 t2 => (rmap r t1) • (rmap r t2) +-- -- | λ[A] t => λ[A⟨r⟩] rmap r t +-- -- | t1 •[t2] => rmap r t1 •[t2⟨r⟩] +-- -- | Λ t => Λ rmap r.lift t + +-- -- instance : RenMap Term Ty where +-- -- rmap := Term.Ty.rmap + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.ren_var {x} {r : Ren Ty} : (#x)⟨r⟩ = #x := by +-- -- simp [RenMap.rmap] + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.ren_app {t1 t2} {r : Ren Ty} : (t1 • t2)⟨r⟩ = t1⟨r⟩ • t2⟨r⟩ := by +-- -- simp [RenMap.rmap] + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.ren_lam {A t} {r : Ren Ty} : (λ[A] t)⟨r⟩ = λ[A⟨r⟩] t⟨r⟩ := by +-- -- simp [RenMap.rmap] + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.ren_tapp {t1 t2} {r : Ren Ty} : (t1 •[t2])⟨r⟩ = t1⟨r⟩ •[t2⟨r⟩] := by +-- -- simp [RenMap.rmap] + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.ren_tlam {t} {r : Ren Ty} : (Λ t)⟨r⟩ = Λ t⟨r.lift⟩ := by +-- -- simp [RenMap.rmap] + +-- -- instance : RenMapId Term Ty where +-- -- apply_id := by subst_solve_id + +-- -- instance : RenMapCompose Term Ty where +-- -- apply_compose := by subst_solve_compose + +-- -- @[simp] +-- -- def Term.rmap (r : Ren Term) : Term -> Term +-- -- | #x => #(r.act x) +-- -- | app t1 t2 => rmap r t1 • rmap r t2 +-- -- | λ[A] t => λ[A] rmap r.lift t +-- -- | t1 •[t2] => rmap r t1 •[t2] +-- -- | Λ t => Λ rmap r t + +-- -- instance : RenMap Term Term where +-- -- rmap := Term.rmap + +-- -- @[simp, grind =] +-- -- theorem Term.ren_var {x} {r : Ren Term} : (Term.var x)⟨r⟩ = .var (r.act x) := by +-- -- simp [RenMap.rmap] + +-- -- @[simp, grind =] +-- -- theorem Term.ren_app {t1 t2} {r : Ren Term} : (t1 • t2)⟨r⟩ = t1⟨r⟩ • t2⟨r⟩ := by +-- -- simp [RenMap.rmap] + +-- -- @[simp, grind =] +-- -- theorem Term.ren_lam {A t} {r : Ren Term} : (λ[A] t)⟨r⟩ = λ[A] t⟨r.lift⟩ := by +-- -- simp [RenMap.rmap] + +-- -- @[simp, grind =] +-- -- theorem Term.ren_tapp {t1 t2} {r : Ren Term} : (t1 •[t2])⟨r⟩ = t1⟨r⟩ •[t2] := by +-- -- simp [RenMap.rmap] + +-- -- @[simp, grind =] +-- -- theorem Term.ren_tlam {t} {r : Ren Term} : (Λ t)⟨r⟩ = Λ t⟨r⟩ := by +-- -- simp [RenMap.rmap] + +-- -- instance : RenMapId Term Term where +-- -- apply_id := by subst_solve_id + +-- -- instance : RenMapCompose Term Term where +-- -- apply_compose := by subst_solve_compose + +-- -- @[simp] +-- -- def Term.Ty.smap (σ : Subst Ty) : Term -> Term +-- -- | #x => #x +-- -- | app t1 t2 => smap σ t1 • smap σ t2 +-- -- | λ[A] t => λ[A[σ]] smap σ t +-- -- | t1 •[t2] => smap σ t1 •[t2[σ]] +-- -- | Λ t => Λ smap σ.lift t + +-- -- instance : SubstMap Term Ty where +-- -- smap := Term.Ty.smap + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.subst_var {x} {σ : Subst Ty} : (#x)[σ] = #x := by +-- -- simp [SubstMap.smap] + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.subst_app {t1 t2} {σ : Subst Ty} : (t1 • t2)[σ] = t1[σ] • t2[σ] := by +-- -- simp [SubstMap.smap] + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.subst_lam {A t} {σ : Subst Ty} : (λ[A] t)[σ] = λ[A[σ]] t[σ] := by +-- -- simp [SubstMap.smap] + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.subst_tapp {t1 t2} {σ : Subst Ty} : (t1 •[t2])[σ] = t1[σ] •[t2[σ]] := by +-- -- simp [SubstMap.smap] + +-- -- @[simp, grind =] +-- -- theorem Term.Ty.subst_tlam {t} {σ : Subst Ty} : (Λ t)[σ] = Λ t[σ.lift] := by +-- -- simp [SubstMap.smap] + +-- -- instance : SubstMapId Term Ty where +-- -- apply_id := by subst_solve_id + +-- -- instance : SubstMapStable Term Ty where +-- -- apply_stable := by subst_solve_stable + +-- -- instance : SubstMapRenComposeLeft Term Ty where +-- -- apply_ren_compose_left := by subst_solve_compose + +-- -- instance : SubstMapRenComposeRight Term Ty where +-- -- apply_ren_compose_right := by subst_solve_compose + +-- -- instance : SubstMapCompose Term Ty where +-- -- apply_compose := by subst_solve_compose + +-- -- @[simp] +-- -- def Term.smap (σ : Subst Term) : Term -> Term +-- -- | #x => σ.act x +-- -- | app t1 t2 => smap σ t1 • smap σ t2 +-- -- | λ[A] t => λ[A] smap σ.lift t +-- -- | t1 •[t2] => smap σ t1 •[t2] +-- -- | Λ t => Λ smap (σ ◾ Ren.succ Ty) t + +-- -- instance : SubstMap Term Term where +-- -- smap := Term.smap + +-- -- @[simp, grind =] +-- -- theorem Term.subst_var {x} {σ : Subst Term} : (Term.var x)[σ] = σ.act x := by +-- -- simp [SubstMap.smap] + +-- -- @[simp, grind =] +-- -- theorem Term.subst_app {t1 t2} {σ : Subst Term} : (t1 • t2)[σ] = t1[σ] • t2[σ] := by +-- -- simp [SubstMap.smap] + +-- -- @[simp, grind =] +-- -- theorem Term.subst_lam {A t} {σ : Subst Term} : (λ[A] t)[σ] = λ[A] t[σ.lift] := by +-- -- simp [SubstMap.smap] + +-- -- @[simp, grind =] +-- -- theorem Term.subst_tapp {t1 t2} {σ : Subst Term} : (t1 •[t2])[σ] = t1[σ] •[t2] := by +-- -- simp [SubstMap.smap] + +-- -- @[simp, grind =] +-- -- theorem Term.subst_tlam {t} {σ : Subst Term} : (Λ t)[σ] = Λ t[σ ◾ Ren.succ Ty] := by +-- -- simp [SubstMap.smap] + +-- -- @[simp] +-- -- theorem Term.from_action_compose {x : Nat} {σ τ : Subst Term} +-- -- : (from_action (σ.act x))[τ] = from_action ((σ ∘ τ).act x) +-- -- := by +-- -- simp [from_action, Subst.compose] +-- -- generalize zdef : σ.act x = z +-- -- cases z <;> simp [from_action] + +-- -- @[simp] +-- -- theorem Term.from_action_hcompose {x : Nat} {σ : Subst Term} {τ : Subst Ty} +-- -- : (from_action (σ.act x))[τ] = from_action ((σ ◾ τ).act x) +-- -- := by +-- -- simp [from_action] +-- -- generalize zdef : σ.act x = z +-- -- cases z <;> simp + +-- -- @[simp] +-- -- theorem Term.from_action_compose_ren {x : Nat} {σ : 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 + +-- -- @[simp] +-- -- theorem Term.from_action_hcompose_ren {x : Nat} {σ : Subst Term} {r : Ren Ty} +-- -- : (from_action (σ.act x))⟨r⟩ = from_action ((σ ◾ r).act x) +-- -- := by +-- -- simp [Term.from_action] +-- -- generalize zdef : σ.act x = z +-- -- cases z <;> simp + +-- -- instance : SubstMapRenCommute Term Ty where +-- -- apply_commute_ren_subst := by subst_solve_compose +-- -- apply_commute_ren_ren := by subst_solve_compose + +-- -- instance : SubstMapRenHetCompose Term Ty where +-- -- apply_hcompose_ren := by subst_solve_compose + +-- -- instance : SubstMapHetCompose Term Ty where +-- -- apply_hcompose := by subst_solve_compose + +-- -- instance : SubstMapId Term Term where +-- -- apply_id := by subst_solve_id + +-- -- -- instance : SubstMapStable Term Term where +-- -- -- apply_stable := by +-- -- -- intro r σ h +-- -- -- funext; case _ t => +-- -- -- induction t generalizing r σ +-- -- -- all_goals simp [*] at *; try simp +instances [*] +-- -- -- all_goals try solve | rw [Subst.apply_stable h] +-- -- -- all_goals try solve | (rw [<-h]; simp +instances [Ren.to]) +-- -- -- all_goals try repeat funext; grind +-- -- -- --subst_solve_stable + +-- -- instance : SubstMapRenComposeLeft Term Term where +-- -- apply_ren_compose_left := by subst_solve_compose + +-- -- instance : SubstMapRenComposeRight Term Term where +-- -- apply_ren_compose_right := by subst_solve_compose + +-- -- instance : SubstMapCompose Term Term where +-- -- apply_compose := by subst_solve_compose end Examples.SystemF diff --git a/Examples/SystemF2.lean b/Examples/SystemF2.lean new file mode 100644 index 0000000..749fb1d --- /dev/null +++ b/Examples/SystemF2.lean @@ -0,0 +1,182 @@ +import LeanSubst +open LeanSubst + +namespace Examples.SystemF2 + +-- inductive Ty where +-- | var : Nat -> Ty +-- | arr : Ty -> Ty -> Ty +-- | all : Ty -> Ty + +-- prefix:max "t#" => Ty.var +-- infixr:85 "-:>" => Ty.arr +-- notation ":∀" t => Ty.all t + +-- inductive Term where +-- | var : Nat -> Term +-- | app : Term -> Term -> Term +-- | lam : Ty -> Term -> Term +-- | tapp : Term -> Ty -> Term +-- | tlam : Term -> Term + +-- prefix:max "#" => Term.var +-- infixl:65 "•" => Term.app +-- notation:100 "λ[" A "]" t => Term.lam A t +-- notation:65 f "•[" a "]" => Term.tapp f a +-- notation:100 "Λ" t => Term.tlam t + +-- ---------------------------------------------------------------------------------------------------- +-- ---- Ty setup +-- ---------------------------------------------------------------------------------------------------- +-- @[coe] +-- def Ty.from_action : Action Ty -> Ty +-- | re y => t#y +-- | su t => t + +-- @[simp, grind =] +-- theorem Ty.from_action_id {n} : from_action (+0σ.act n) = var n := by +-- simp [from_action] + +-- @[simp, grind =] +-- theorem Ty.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by +-- simp [from_action] + +-- @[simp, grind =] +-- theorem Ty.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + +-- @[simp, grind =] +-- theorem Ty.from_action_su {t} : from_action (su t) = t := by simp [from_action] + +-- instance : Coe (Action Ty) Ty where +-- coe := Ty.from_action + +-- @[simp] +-- def Ty.rmap (r : Ren Ty) : Ty -> Ty +-- | t#x => t#(r.act x) +-- | t1 -:> t2 => rmap r t1 -:> rmap r t2 +-- | :∀ t => :∀ rmap r.lift t + +-- instance : RenMap Ty Ty where +-- rmap := Ty.rmap + +-- @[simp, grind =] +-- theorem Ty.ren_var {x} {r : Ren Ty} : (Ty.var x)⟨r⟩ = .var (r.act x) := by +-- simp [RenMap.rmap] + +-- @[simp, grind =] +-- theorem Ty.ren_arr {t1 t2} {r : Ren Ty} : (t1 -:> t2)⟨r⟩ = t1⟨r⟩ -:> t2⟨r⟩ := by +-- simp [RenMap.rmap] + +-- @[simp, grind =] +-- theorem Ty.ren_all {t} {r : Ren Ty} : (:∀ t)⟨r⟩ = :∀ t⟨r.lift⟩ := by +-- simp [RenMap.rmap] + +-- instance : RenMapId Ty Ty where +-- apply_id := by subst_solve_id + +-- instance : RenMapCompose Ty Ty where +-- apply_compose := by subst_solve_compose + +-- @[simp] +-- def Ty.smap (σ : Subst Ty) : Ty -> Ty +-- | t#x => σ.act x +-- | t1 -:> t2 => smap σ t1 -:> smap σ t2 +-- | :∀ t => :∀ smap σ.lift t + +-- instance : SubstMap Ty Ty where +-- smap := Ty.smap + +-- @[simp, grind =] +-- theorem Ty.subst_var {x} {σ : Subst Ty} : (Ty.var x)[σ] = σ.act x := by +-- simp [SubstMap.smap] + +-- @[simp, grind =] +-- theorem Ty.subst_arr {t1 t2} {σ : Subst Ty} : (t1 -:> t2)[σ] = t1[σ] -:> t2[σ] := by +-- simp [SubstMap.smap] + +-- @[simp, grind =] +-- theorem Ty.subst_all {t} {σ : Subst Ty} : (:∀ t)[σ] = :∀ t[σ.lift] := by +-- simp [SubstMap.smap] + +-- @[simp] +-- theorem Ty.from_action_compose {x : Nat} {σ τ : Subst Ty} +-- : (from_action (Subst.act σ x))[τ] = from_action ((σ ∘ τ).act x) +-- := by +-- simp [from_action, Subst.compose] +-- generalize zdef : σ.act x = z +-- cases z <;> simp [from_action] + +-- @[simp] +-- theorem Ty.from_action_compose_ren {x : Nat} {σ : Subst Ty} {r : Ren Ty} +-- : (from_action (σ.act x))⟨r⟩ = from_action ((σ ∘ r).act x) +-- := by +-- simp [Ty.from_action] +-- generalize zdef : σ.act x = z +-- cases z <;> simp + +-- instance : SubstMapId Ty Ty where +-- apply_id := by subst_solve_id + +-- instance : SubstMapStable Ty Ty where +-- apply_stable := by subst_solve_stable + +-- instance : SubstMapRenComposeLeft Ty Ty where +-- apply_ren_compose_left := by subst_solve_compose + +-- instance : SubstMapRenComposeRight Ty Ty where +-- apply_ren_compose_right := by subst_solve_compose + +-- instance : SubstMapCompose Ty Ty where +-- apply_compose := by subst_solve_compose + +-- ---------------------------------------------------------------------------------------------------- +-- ---- Term setup +-- ---------------------------------------------------------------------------------------------------- +-- @[coe] +-- def Term.from_action : Action Term -> Term +-- | re y => #y +-- | su t => t + +-- @[simp, grind =] +-- theorem Term.from_action_id {n} : from_action (+0σ.act n) = var n := by +-- simp [from_action] + +-- @[simp, grind =] +-- theorem Term.from_action_succ {n} : from_action (+1σ.act n) = var (n + 1) := by +-- simp [from_action] + +-- @[simp, grind =] +-- theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + +-- @[simp, grind =] +-- theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] + +-- instance : Coe (Action Term) Term where +-- coe := Term.from_action + +-- @[simp] +-- def Term.rmap (r : Ren Term) (rt : Ren Ty) : Term -> Term +-- | #x => var (r.act x) +-- | app t1 t2 => (rmap r rt t1) • (rmap r rt t2) +-- | λ[A] t => λ[A⟨rt⟩] rmap r.lift rt t +-- | t1 •[A] => rmap r rt t1 •[A⟨rt⟩] +-- | Λ t => Λ rmap r rt.lift t + +-- instance : RenVecMap Term #(Ty) where +-- rvmap := Term.rmap + +-- instance : RenMap Term Ty where +-- rmap := Term.rmap (.id Term) + +-- @[simp] +-- def Term.smap (σ : Subst Term) (σt : Subst Ty) : Term -> Term +-- | #x => σ.act x +-- | app t1 t2 => (smap σ σt t1) • (smap σ σt t2) +-- | λ[A] t => λ[A[σt]] smap σ.lift σt t +-- | t1 •[A] => smap σ σt t1 •[A[σt]] +-- | Λ t => Λ smap (σ ◾ Ren.succ Ty) σt.lift t + +-- instance : SubstVecMap Term #(Ty) where +-- svmap := Term.smap + +end Examples.SystemF2 diff --git a/Examples/SystemFWithNat/Term.lean b/Examples/SystemFWithNat/Term.lean new file mode 100644 index 0000000..f4a3358 --- /dev/null +++ b/Examples/SystemFWithNat/Term.lean @@ -0,0 +1,96 @@ + +import LeanSubst +open LeanSubst + +namespace SystemFWithNat + +inductive Ty where +| var : Nat -> Ty +| arrow : Ty -> Ty -> Ty +| all : Ty -> Ty +| nat : Ty + +inductive Term where +| var : Nat -> Term +| app : Term -> Term -> Term +| lam (A : Ty) (t : Term) : Term -- binds Term in t +| tapp : Term -> Ty -> Term +| tlam (t : Term) : Term -- binds Ty in t (does it make sense to allow a user to give a name instead of a position?) +| zero : Term +| succ : Term -> Term +| nrec (motive : Ty) (z : Term) (s : Term) (n : Term) : Term -- binds 2 Term's in s + +---------------------------------------------------------------------------------------------------- +-- Ty Renaming & Substitution +---------------------------------------------------------------------------------------------------- + +-- This is just STLC with some constants + +instance : RenMap Ty [Ty] where + rmap := sorry + +instance : SubstMap Ty [Ty] where + smap := sorry + +---------------------------------------------------------------------------------------------------- +-- Term Renaming & Substitution +---------------------------------------------------------------------------------------------------- + +@[coe] +def Term.from_action : Action Term -> Term +| re y => var y +| su t => t + +@[simp, grind =] +theorem Term.from_action_id {n} : from_action (𝐬0.act n) = var n := by + simp [from_action] + +@[simp, grind =] +theorem Term.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by + simp [from_action] + +@[simp, grind =] +theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + +@[simp, grind =] +theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] + +instance : Coe (Action Term) Term where + coe := Term.from_action + +-- Defining the rmap/smap using the Tuple form might make more sense for a macro, dunno +@[simp] +def Term.rmap (r : RenVec [Term, Ty]) : Term -> Term +| var x => var (r.1.act x) +| app t1 t2 => app (t1.rmap r) (t2.rmap r) +| lam A t => lam A⟨r.2.1⟩ (t.rmap $ r.lift [1, 0]) +| tapp t A => tapp (t.rmap r) A⟨r.2.1⟩ +| tlam t => tlam (t.rmap $ r.lift [0, 1]) +| zero => zero +| succ t => succ (t.rmap r) +| nrec motive z s n => nrec motive⟨r.2.1⟩ (z.rmap r) (s.rmap $ r.lift [2, 0]) (n.rmap r) + +instance : RenMap Term [Term, Ty] where + rmap := Term.rmap + +instance : RenMap Term [Term] where + rmap r := Term.rmap (r.1, Ren.id Ty, .unit) + +instance : RenMap Term [Ty] where + rmap r := Term.rmap (Ren.id Term, r.1, .unit) + +@[simp] +def Term.smap (σ : Subst Term) (τ : Subst Ty) : Term -> Term +| var x => σ.act x +| app t1 t2 => app (t1.smap σ τ) (t2.smap σ τ) +| lam A t => lam A[τ] (t.smap σ.lift τ) +| tapp t A => tapp (t.smap σ τ) A[τ] +-- Because `Term` has `Ty` variables, we have to increment `Ty` variables in `σ` by 1 +-- v-------v +| tlam t => tlam (t.smap σ⟨𝐫1(Ty)⟩ τ.lift) +| zero => zero +| succ t => succ (t.smap σ τ) +| nrec motive z s n => nrec motive[τ] (z.smap σ τ) (s.smap (σ.lift 2) τ) (n.smap σ τ) + + +end SystemFWithNat diff --git a/Examples/VariadicSTLC/Term.lean b/Examples/VariadicSTLC/Term.lean new file mode 100644 index 0000000..05c2cc6 --- /dev/null +++ b/Examples/VariadicSTLC/Term.lean @@ -0,0 +1,104 @@ + +import LeanSubst +open LeanSubst + +namespace VariadicSTLC + +inductive Ty where +| base : Ty +| arrow : Ty -> Ty + +inductive Term where +| var : Nat -> Term +| app n : Term -> (Fin n -> Term) -> Term +| lam n : (Fin n -> Ty) -> Term -> Term + +@[coe] +def Term.from_action : Action Term -> Term +| re y => var y +| su t => t + +@[simp, grind =] +theorem Term.from_action_id {n} : from_action (𝐬0.act n) = var n := by + simp [from_action] + +@[simp, grind =] +theorem Term.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by + simp [from_action] + +@[simp, grind =] +theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + +@[simp, grind =] +theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] + +instance : Coe (Action Term) Term where + coe := Term.from_action + +@[simp] +def Term.rmap (r : Ren Term) : Term -> Term +| var x => var (r.act x) +| app n t ts => app n (t.rmap r) (λ i => (ts i).rmap r) +| lam n As t => lam n As (t.rmap $ r.lift n) + +instance : RenMap Term [Term] where + rmap r := Term.rmap r.1 + +@[simp, grind =] +theorem Term.rmap_var {x} {r : Ren Term} : (var x)⟨r⟩ = .var (r.act x) := by + simp [RenMap.rmap] + +@[simp, grind =] +theorem Term.rmap_app {n} {t : Term} {ts : Fin n -> Term} {r : Ren Term} + : (app n t ts)⟨r⟩ = app n t⟨r⟩ (λ i => (ts i)⟨r⟩) +:= by simp [RenMap.rmap] + +@[simp, grind =] +theorem Term.rmap_lam {n As t} {r : Ren Term} : (lam n As t)⟨r⟩ = lam n As t⟨r.lift n⟩ := by + simp [RenMap.rmap] + +instance : RenMapId Term [Term] where + apply_id := by subst_solve_id + +instance : RenMapCompose Term [Term] where + apply_compose := by sorry + +@[simp] +def Term.smap (σ : Subst Term) : Term -> Term +| var x => σ.act x +| app n t ts => app n (t.smap σ) (λ i => (ts i).smap σ) +| lam n As t => lam n As (t.smap $ σ.lift n) + +instance : SubstMap Term [Term] where + smap σ := Term.smap σ.1 + +-- `σ.1.act` might change to `σ[0].act` to prevent things like `σ.2.2.1.act` +@[simp, grind =] +theorem Term.smap_var {x} {σ : SubstVec [Term]} : (var x)[σ,] = from_action (σ.1.act x) := by + simp [SubstMap.smap] + +@[simp, grind =] +theorem Term.smap_app {n} {t : Term} {ts : Fin n -> Term} {σ : Subst Term} + : (app n t ts)[σ] = app n t[σ] (λ i => (ts i)[σ]) +:= by simp [SubstMap.smap] + +@[simp, grind =] +theorem Term.smap_lam {n As t} {σ : Subst Term} : (lam n As t)[σ] = lam n As t[σ.lift n] := by + simp [SubstMap.smap] + +instance : SubstMapId Term [Term] where + apply_id := by sorry + +instance : SubstMapStable Term [Term] where + apply_stable := by sorry + +instance : SubstMapRenComposeLeft Term [Term] where + apply_ren_compose_left := by sorry + +instance : SubstMapRenComposeRight Term [Term] where + apply_ren_compose_right := by sorry + +instance : SubstMapCompose Term [Term] where + apply_compose := by sorry + +end VariadicSTLC diff --git a/LeanSubst.lean b/LeanSubst.lean index 25a1642..55761f9 100644 --- a/LeanSubst.lean +++ b/LeanSubst.lean @@ -5,5 +5,6 @@ import LeanSubst.Laws import LeanSubst.Types.Option import LeanSubst.Types.List import LeanSubst.Misc +import LeanSubst.Expanded import LeanSubst.Rewriting.Reduction import LeanSubst.Rewriting.Normal diff --git a/LeanSubst/Basic.lean b/LeanSubst/Basic.lean index b31433a..d294f35 100644 --- a/LeanSubst/Basic.lean +++ b/LeanSubst/Basic.lean @@ -1,22 +1,78 @@ +import Lean.Elab.Term +import Lean.Elab.SyntheticMVars + namespace LeanSubst universe u1 u2 u3 variable {S : Type u1} {T : Type u2} {U : Type u3} +namespace Subst.Syntax + open Lean.Elab.Term + + open Lean in + def MetaM.promote {α} (x : Meta.MetaM α) : Elab.Term.TermElabM α := x + + def form_list : List Lean.Expr -> TermElabM (Lean.TSyntax `term) + | [] => `(List.nil) + | .cons x xs => do + let xs' <- form_list xs + `(List.cons $(<- exprToSyntax x) $xs') + + def form_prod : List Lean.Expr -> TermElabM (Lean.TSyntax `term) + | [] => `(PUnit.unit) + | .cons x xs => do + let xs' <- form_prod xs + `(Prod.mk $(<- exprToSyntax x) $xs') + + def get_ty_arg (e : TermElabM Lean.Expr) : TermElabM Lean.Expr := do + let e <- e + match e with + | .app _ ty => pure ty + | _ => Lean.Elab.throwUnsupportedSyntax +end Subst.Syntax + +set_option linter.unusedVariables false in +abbrev Var (T : Type u2) := Nat + structure Ren (T : Type u2) where act : Nat -> Nat -class RenMap (S : Type u1) (T : Type u2) where - rmap : Ren T -> S -> S +@[implicit_reducible] +def RenVec : List (Type u2) -> Type u2 +| [] => PUnit +| .cons x xs => Ren x × RenVec xs + +class RenMap (S : Type u1) (V : List (Type u2)) where + rmap : RenVec V -> S -> S + +class RenMapAll (V : List (Type u2)) where + rmap : ∀ (i : Fin V.length), RenMap V[i] [V[i]] export RenMap (rmap) -macro:max t:term noWs "⟨" r:term "⟩" : term => `(rmap $r $t) +macro:max (name := «term_⟨_,⟩») t:term noWs "⟨" r:term ",⟩" : term => `(rmap $r $t) +syntax:max (name := «term_⟨_,+⟩») term noWs "⟨" term ,+ "⟩" : term + +open Lean.Meta in +open Lean.Elab.Term in +open Subst.Syntax in +elab_rules <= expected +| `($t⟨ $elems,* ⟩) => do + let elems <- List.mapM id $ elems.getElems.foldl (λ acc t => elabTermAndSynthesize t none :: acc) [] + let elems_ty <- List.mapM id $ elems.map inferType |> List.map MetaM.promote |> List.map get_ty_arg + let list_ann <- form_list elems_ty.reverse + let elems_stx <- form_prod elems.reverse + let stx : TermElabM Lean.Syntax := `(@rmap _ $list_ann _ $elems_stx $t) + let stx <- stx + elabTermAndSynthesize stx expected @[app_unexpander rmap] def unexpand_rmap : Lean.PrettyPrinter.Unexpander -| `($_ $r $t) => `($t⟨$r⟩) +| `($_ ($r1, {down := ()}) $t) => `($t⟨$r1⟩) +| `($_ ($r1, $r2, {down := ()}) $t) => `($t⟨$r1, $r2⟩) +| `($_ ($r1, $r2, $r3, {down := ()}) $t) => `($t⟨$r1, $r2, $r3⟩) +| `($_ $r $t) => `($t⟨$r,⟩) | _ => throw () inductive Action (T : Type u2) where @@ -29,6 +85,11 @@ export Action (re su) structure Subst (T : Type u2) where inner : Nat -> Action T +@[implicit_reducible] +def SubstVec : List (Type u2) -> Type u2 +| [] => PUnit +| .cons x xs => Subst x × SubstVec xs + class SubstAction (T : Type u1) (A : Type u2) (U : outParam (Type u3)) where act (σ : Subst T) : A -> U @@ -37,16 +98,36 @@ def Subst.act [SubstAction S T U] (σ : Subst S) : T -> U := SubstAction.act σ instance : SubstAction T Nat (Action T) where act := Subst.inner -class SubstMap (S : Type u1) (T : Type u2) where - smap : Subst T -> S -> S +class SubstMap (S : Type u1) (V : List (Type u2)) where + smap : SubstVec V -> S -> S + +class SubstMapAll (V : List (Type u2)) where + smap : ∀ (i : Fin V.length), SubstMap V[i] [V[i]] export SubstMap (smap) -macro:max t:term noWs "[" σ:term "]" : term => `(smap $σ $t) +macro:max (name := «term_[_,]») t:term noWs "[" σ:term ",]" : term => `(smap $σ $t) +syntax:max (name := «term_[_,+]») term noWs "[" term ,+ "]" : term + +open Lean.Meta in +open Lean.Elab.Term in +open Subst.Syntax in +elab_rules <= expected +| `($t[ $elems,* ]) => do + let elems <- List.mapM id $ elems.getElems.foldl (λ acc t => elabTermAndSynthesize t none :: acc) [] + let elems_ty <- List.mapM id $ elems.map inferType |> List.map MetaM.promote |> List.map get_ty_arg + let list_ann <- form_list elems_ty.reverse + let elems_stx <- form_prod elems.reverse + let stx : TermElabM Lean.Syntax := `(@smap _ $list_ann _ $elems_stx $t) + let stx <- stx + elabTermAndSynthesize stx expected @[app_unexpander smap] def unexpand_smap : Lean.PrettyPrinter.Unexpander -| `($_ $σ $t) => `($t[$σ]) +| `($_ ($σ1, {down := ()}) $t) => `($t[$σ1]) +| `($_ ($σ1, $σ2, {down := ()}) $t) => `($t[$σ1, $σ2]) +| `($_ ($σ1, $σ2, $σ3, {down := ()}) $t) => `($t[$σ1, $σ2, $σ3]) +| `($_ $σ $t) => `($t[$σ,]) | _ => throw () end LeanSubst diff --git a/LeanSubst/Class.lean b/LeanSubst/Class.lean index 61638b7..6a5179f 100644 --- a/LeanSubst/Class.lean +++ b/LeanSubst/Class.lean @@ -4,111 +4,213 @@ import LeanSubst.Ops namespace LeanSubst universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} {U : Type u3} +variable {S : Type u1} {T T1 T2 : Type u2} {U : Type u3} +variable {V : List (Type u2)} -class RenMapId (S : Type u1) (T : Type u2) [RenMap S T] where - apply_id {s : S} : s⟨.id T⟩ = s +class RenMapId (S : Type u1) (V : List (Type u2)) [RenMap S V] where + apply_id {s : S} : s⟨Ren.ids V,⟩ = 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 V] [RenMapId S V] {s : S} : s⟨ids V,⟩ = s := RenMapId.apply_id + +@[simp] +theorem Ren.apply_id1 [RenMap S [T]] [RenMapId S [T]] {s : S} : s⟨id T⟩ = s := RenMapId.apply_id @[simp] -theorem Ren.apply_id [RenMap S T] [RenMapId S T] {s : S} : s⟨id T⟩ = s := RenMapId.apply_id +theorem Ren.apply_id2 [RenMap S [T1, T2]] [RenMapId S [T1, T2]] {s : S} : s⟨id T1, id T2⟩ = s := RenMapId.apply_id + +class RenMapCompose (S : Type u1) (V : List (Type u2)) [RenMap S V] where + apply_compose {s : S} {r1 r2 : RenVec V} : s⟨r1,⟩⟨r2,⟩ = s⟨r1 >> r2,⟩ @[simp, grind =] -theorem Ren.apply_compose [RenMap S T] [RenMapCompose S T] {s : S} {r1 r2 : Ren T} - : s⟨r1⟩⟨r2⟩ = s⟨r1 ∘ r2⟩ +theorem Ren.apply_compose [RenMap S V] [RenMapCompose S V] {s : S} {r1 r2 : RenVec V} + : 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 +@[simp, grind =] +theorem Ren.apply_compose1 [RenMap S [T]] [RenMapCompose S [T]] {s : S} {r1 r2 : Ren T} + : s⟨r1⟩⟨r2⟩ = s⟨r1 >> r2⟩ +:= Ren.apply_compose -instance [RenMap S T] [RenMapId S T] : RenMapId (Action S) T where - apply_id := by intro s; cases s <;> simp +@[simp, grind =] +theorem Ren.apply_compose2 [RenMap S [T1, T2]] [RenMapCompose S [T1, T2]] + {s : S} {r1 r2 : Ren T1} {k1 k2 : Ren T2} + : s⟨r1, k1⟩⟨r2, k2⟩ = s⟨r1 >> r2, k1 >> k2⟩ +:= Ren.apply_compose -instance (priority := high) [RenMap T T] [RenMapCompose T T] : RenMapCompose (Action T) T where - apply_compose := by intro s; cases s <;> simp +instance (priority := high) [RenMap T [T]] [RenMapId T [T]] : RenMapId (Action T) [T] where + apply_id := by intro s; cases s <;> simp [Ren.ids] -instance [RenMap S T] [RenMapCompose S T] : RenMapCompose (Action S) T where - apply_compose := by intro s; cases s <;> simp +instance (priority := low) [RenMap S V] [RenMapId S V] : RenMapId (Action S) V where + apply_id := by intro s; cases s <;> simp -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 σ +instance (priority := high) [RenMap T [T]] [RenMapCompose T [T]] : RenMapCompose (Action T) [T] where + apply_compose := by + intro s r1 r2; cases s + all_goals + simp [RenVec] at r1 r2 + simp [rmap, HAndThen.hAndThen, AndThen.andThen, RenVec.compose, Ren.compose] -class SubstMapId (S : Type u1) (T : Type u2) [SubstMap S T] where - apply_id {s : S} : s[.id T] = s +instance (priority := low) [RenMap S V] [RenMapCompose S V] : RenMapCompose (Action S) V where + apply_compose := by intro s; cases s <;> simp -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 SubstMapStable (S : Type u1) (V : List $ Type u2) [RenMap S V] [SubstMap S V] where + apply_stable (r : RenVec V) (σ : SubstVec V) : r.to = σ -> rmap (S := S) r = smap σ -class SubstMapRenComposeRight (S : Type u1) (T : Type u2) [RenMap S T] [RenMap T T] [SubstMap S T] where - apply_ren_compose_right {s : S} {r : Ren T} {σ : Subst T} : s[σ]⟨r⟩ = s[σ ∘ r] +class SubstMapId (S : Type u1) (V : List $ Type u2) [SubstMap S V] where + apply_id {s : S} : s[Subst.ids V,] = s -class SubstMapCompose (S : Type u1) (T : Type u2) [SubstMap S T] [SubstMap T T] where - apply_compose {s : S} {σ τ : Subst T} : s[σ][τ] = s[σ ∘ τ] +@[simp] +theorem Subst.apply_id [SubstMap S V] [SubstMapId S V] {s : S} : s[ids V,] = s := SubstMapId.apply_id -class SubstMapRenCommute (S : Type u1) (T : Type u2) [RenMap S S] [RenMap S T] [SubstMap S T] where - apply_commute_ren_subst {s : S} {r : Ren S} {τ : Subst T} : s⟨r⟩[τ] = s[τ]⟨r⟩ - apply_commute_ren_ren {s : S} {r1 : Ren S} {r2 : Ren T} : s⟨r1⟩⟨r2⟩ = s⟨r2⟩⟨r1⟩ +@[simp] +theorem Subst.apply_id1 [SubstMap S [T]] [SubstMapId S [T]] {s : S} : s[id T] = s := SubstMapId.apply_id -class SubstMapRenHetCompose (S : Type u1) (T : Type u2) [RenMap S T] [SubstMap S S] where - apply_hcompose_ren {s : S} {σ : Subst S} {r : Ren T} : s[σ]⟨r⟩ = s⟨r⟩[σ ◾ r] +@[simp] +theorem Subst.apply_id2 [SubstMap S [T1, T2]] [SubstMapId S [T1, T2]] {s : S} : s[id T1, id T2] = s := SubstMapId.apply_id -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[τ][σ ◾ τ] +class SubstMapRenComposeLeft (S : Type u1) (V : List $ Type u2) [RenMap S V] [SubstMap S V] where + apply_ren_compose_left {s : S} {r : RenVec V} {τ : SubstVec V} : s⟨r,⟩[τ,] = s[r >> τ,] -theorem Subst.apply_stable - [RenMap S T] [SubstMap S T] [SubstMapStable S T] - {r : Ren T} {σ : Subst T} - : r.to = σ -> rmap (S := S) r = smap σ -:= SubstMapStable.apply_stable _ _ +@[simp, grind =] +theorem Subst.apply_ren_compose_left + [RenMap S V] [SubstMap S V] [SubstMapRenComposeLeft S V] + {s : S} {r : RenVec V} {σ : SubstVec V} + : s⟨r,⟩[σ,] = s[r >> σ,] +:= SubstMapRenComposeLeft.apply_ren_compose_left @[simp, grind =] -theorem Subst.apply_id [SubstMap S T] [SubstMapId S T] {s : S} : s[.id T] = s := SubstMapId.apply_id +theorem Subst.apply_ren_compose_left1 + [RenMap S [T]] [SubstMap S [T]] [SubstMapRenComposeLeft S [T]] + {s : S} {r : Ren T} {σ : Subst T} + : s⟨r⟩[σ] = s[r >> σ] +:= Subst.apply_ren_compose_left @[simp, grind =] -theorem Subst.apply_ren_compose_left [RenMap S T] [SubstMap S T] [SubstMapRenComposeLeft S T] - {s : S} {r : Ren T} {τ : Subst T} - : s⟨r⟩[τ] = s[r ∘ τ] -:= SubstMapRenComposeLeft.apply_ren_compose_left +theorem Subst.apply_ren_compose_left2 + [RenMap S [T1, T2]] [SubstMap S [T1, T2]] [SubstMapRenComposeLeft S [T1, T2]] + {s : S} {r1 : Ren T1} {r2 : Ren T2} {σ1 : Subst T1} {σ2 : Subst T2} + : s⟨r1, r2⟩[σ1, σ2] = s[r1 >> σ1, r2 >> σ2] +:= Subst.apply_ren_compose_left + +class SubstMapRenComposeRight (S : Type u1) (V : List $ Type u2) [RenMap S V] [RenMapAll V] [SubstMap S V] where + apply_ren_compose_right {s : S} {r : RenVec V} {σ : SubstVec V} : s[σ,]⟨r,⟩ = s[σ >> r,] @[simp, grind =] theorem Subst.apply_ren_compose_right - [RenMap S T] [RenMap T T] [SubstMap S T] [SubstMapRenComposeRight S T] - {s : S} {σ : Subst T} {r : Ren T} - : s[σ]⟨r⟩ = s[σ ∘ r] + [RenMap S V] [RenMapAll V] [SubstMap S V] [SubstMapRenComposeRight S V] + {s : S} {r : RenVec V} {σ : SubstVec V} + : s[σ,]⟨r,⟩ = s[σ >> r,] := SubstMapRenComposeRight.apply_ren_compose_right -@[grind =] -theorem Subst.apply_commute_ren_subst - [RenMap S S] [RenMap S T] [SubstMap S T] [SubstMapRenCommute S T] - {s : S} {r : Ren S} {τ : Subst T} - : s⟨r⟩[τ] = s[τ]⟨r⟩ -:= SubstMapRenCommute.apply_commute_ren_subst +@[simp, grind =] +theorem Subst.apply_ren_compose_right1 + [RenMap S [T]] [RenMapAll [T]] [SubstMap S [T]] [SubstMapRenComposeRight S [T]] + {s : S} {r : Ren T} {σ : Subst T} + : s[σ]⟨r⟩ = s[σ >> r] +:= Subst.apply_ren_compose_right + +@[simp, grind =] +theorem Subst.apply_ren_compose_right2 + [RenMap S [T1, T2]] [RenMapAll [T1, T2]] [SubstMap S [T1, T2]] [SubstMapRenComposeRight S [T1, T2]] + {s : S} {r1 : Ren T1} {r2 : Ren T2} {σ1 : Subst T1} {σ2 : Subst T2} + : s[σ1, σ2]⟨r1, r2⟩ = s[σ1 >> r1, σ2 >> r2] +:= Subst.apply_ren_compose_right -@[grind =] -theorem Subst.apply_commute_ren_ren - [RenMap S S] [RenMap S T] [SubstMap S T] [SubstMapRenCommute S T] - {s : S} {r1 : Ren S} {r2 : Ren T} - : s⟨r1⟩⟨r2⟩ = s⟨r2⟩⟨r1⟩ -:= SubstMapRenCommute.apply_commute_ren_ren +class SubstMapCompose (S : Type u1) (V : List $ Type u2) [SubstMap S V] [SubstMapAll V] where + apply_compose {s : S} {σ τ : SubstVec V} : s[σ,][τ,] = s[σ >> τ,] @[simp, grind =] -theorem Subst.apply_compose [SubstMap S T] [SubstMap T T] [SubstMapCompose S T] - {s : S} {σ τ : Subst T} - : s[σ][τ] = s[σ ∘ τ] +theorem Subst.apply_compose + [SubstMap S V] [SubstMapAll V] [SubstMapCompose S V] + {s : S} {σ1 σ2 : SubstVec V} + : s[σ1,][σ2,] = s[σ1 >> σ2,] := SubstMapCompose.apply_compose @[simp, grind =] -theorem Subst.apply_hcompose_ren [SubstMap S S] [RenMap S T] [SubstMapRenHetCompose S T] - {s : S} {σ : Subst S} {r : Ren T} - : s[σ]⟨r⟩ = s⟨r⟩[σ ◾ r] -:= SubstMapRenHetCompose.apply_hcompose_ren +theorem Subst.apply_compose1 + [SubstMap S [T]] [SubstMap T [T]] [SubstMapCompose S [T]] + {s : S} {σ1 σ2 : Subst T} + : s[σ1][σ2] = s[σ1 >> σ2] +:= Subst.apply_compose @[simp, grind =] -theorem Subst.apply_hcompose [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] - {s : S} {σ : Subst S} {τ : Subst T} - : s[σ][τ] = s[τ][σ ◾ τ] -:= SubstMapHetCompose.apply_hcompose +theorem Subst.apply_compose2 + [SubstMap S [T1, T2]] [SubstMap T1 [T1]] [SubstMap T2 [T2]] [SubstMapCompose S [T1, T2]] + {s : S} {σ1 σ2 : Subst T1} {τ1 τ2 : Subst T2} + : s[σ1, τ1][σ2, τ2] = s[σ1 >> σ2, τ1 >> τ2] +:= Subst.apply_compose + +-- @[simp↓, grind =] +-- theorem Subst.apply_compose2 [SubstMap S [T1, T2]] [SubstMapCompose S [T1, T2]] +-- {s : S} {r1 r2 : Subst T1} {k1 k2 : Subst T2} +-- : s⟨r1, k1⟩⟨r2, k2⟩ = s⟨r1 >> r2, k1 >> k2⟩ +-- := by +-- have lem := @SubstMapCompose.apply_compose S [T1, T2] _ _ s (r1, k1, .up .unit) (r2, k2, .up .unit) +-- rw [lem]; simp [Subst.compose_tuple] + +-- class SubstMapRenCommute (S : Type u1) (T : Type u2) [RenMap S S] [RenMap S T] [SubstMap S T] where +-- apply_commute_ren_subst {s : S} {r : Ren S} {τ : Subst T} : s⟨r⟩[τ] = s[τ]⟨r⟩ +-- apply_commute_ren_ren {s : S} {r1 : Ren S} {r2 : Ren T} : s⟨r1⟩⟨r2⟩ = s⟨r2⟩⟨r1⟩ + +-- class SubstMapRenHetCompose (S : Type u1) (T : Type u2) [RenMap S T] [SubstMap S S] where +-- apply_hcompose_ren {s : S} {σ : Subst S} {r : Ren T} : s[σ]⟨r⟩ = s⟨r⟩[σ ◾ 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[τ][σ ◾ τ] + +-- theorem Subst.apply_stable +-- [RenMap S T] [SubstMap S T] [SubstMapStable S T] +-- {r : Ren T} {σ : Subst T} +-- : r.to = σ -> rmap (S := S) r = smap σ +-- := SubstMapStable.apply_stable _ _ + +-- @[simp, grind =] +-- theorem Subst.apply_id [SubstMap S T] [SubstMapId S T] {s : S} : s[.id T] = s := SubstMapId.apply_id + +-- @[simp, grind =] +-- theorem Subst.apply_ren_compose_left [RenMap S T] [SubstMap S T] [SubstMapRenComposeLeft S T] +-- {s : S} {r : Ren T} {τ : Subst T} +-- : s⟨r⟩[τ] = s[r >> τ] +-- := SubstMapRenComposeLeft.apply_ren_compose_left + +-- @[simp, grind =] +-- theorem Subst.apply_ren_compose_right +-- [RenMap S T] [RenMap T T] [SubstMap S T] [SubstMapRenComposeRight S T] +-- {s : S} {σ : Subst T} {r : Ren T} +-- : s[σ]⟨r⟩ = s[σ >> r] +-- := SubstMapRenComposeRight.apply_ren_compose_right + +-- @[grind =] +-- theorem Subst.apply_commute_ren_subst +-- [RenMap S S] [RenMap S T] [SubstMap S T] [SubstMapRenCommute S T] +-- {s : S} {r : Ren S} {τ : Subst T} +-- : s⟨r⟩[τ] = s[τ]⟨r⟩ +-- := SubstMapRenCommute.apply_commute_ren_subst + +-- @[grind =] +-- theorem Subst.apply_commute_ren_ren +-- [RenMap S S] [RenMap S T] [SubstMap S T] [SubstMapRenCommute S T] +-- {s : S} {r1 : Ren S} {r2 : Ren T} +-- : s⟨r1⟩⟨r2⟩ = s⟨r2⟩⟨r1⟩ +-- := SubstMapRenCommute.apply_commute_ren_ren + +-- @[simp, grind =] +-- theorem Subst.apply_compose [SubstMap S T] [SubstMap T T] [SubstMapCompose S T] +-- {s : S} {σ τ : Subst T} +-- : s[σ][τ] = s[σ >> τ] +-- := SubstMapCompose.apply_compose + +-- @[simp, grind =] +-- theorem Subst.apply_hcompose_ren [SubstMap S S] [RenMap S T] [SubstMapRenHetCompose S T] +-- {s : S} {σ : Subst S} {r : Ren T} +-- : s[σ]⟨r⟩ = s⟨r⟩[σ ◾ r] +-- := SubstMapRenHetCompose.apply_hcompose_ren + +-- @[simp, grind =] +-- theorem Subst.apply_hcompose [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] +-- {s : S} {σ : Subst S} {τ : Subst T} +-- : s[σ][τ] = s[τ][σ ◾ τ] +-- := SubstMapHetCompose.apply_hcompose end LeanSubst diff --git a/LeanSubst/Expanded.lean b/LeanSubst/Expanded.lean new file mode 100644 index 0000000..bbca0ea --- /dev/null +++ b/LeanSubst/Expanded.lean @@ -0,0 +1,22 @@ + +import LeanSubst.Basic +import LeanSubst.Ops +import LeanSubst.Class + +namespace LeanSubst + +universe u1 u2 u3 +variable {S : Type u1} {T T1 T2 : Type u2} {U : Type u3} +variable {V : List (Type u2)} + +-- @[simp] +-- theorem subst_tuple_eta1 [SubstMap S [T]] {s : S} {σ : List.Tuple Subst [T]} : s[σ,] = s[σ.1] := by +-- rcases σ with ⟨σ, u⟩; rcases u; simp + +-- @[simp] +-- theorem subst_tuple_eta2 [SubstMap S [T1, T2]] {s : S} {σ : List.Tuple Subst [T1, T2]} +-- : s[σ,] = s[σ.1, σ.2.1] +-- := by +-- rcases σ with ⟨σ1, σ2, u⟩; rcases u; simp + +end LeanSubst diff --git a/LeanSubst/Laws.lean b/LeanSubst/Laws.lean index a69d80e..3b1bfcd 100644 --- a/LeanSubst/Laws.lean +++ b/LeanSubst/Laws.lean @@ -8,27 +8,28 @@ import LeanSubst.Types.List namespace LeanSubst universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} {U : Type u3} +variable {S : Type u1} {T T1 T2 : Type u2} {U : Type u3} +variable {V : List (Type u2)} @[grind <-] -theorem Ren.lift_eq_from_eq [RenMap T T] {r : Ren T} {σ : Subst T} +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] - theorem rewrite0 [RenMap T T] : +0σ ∘ +1r = succ T := by + theorem rewrite0 [RenMap T [T]] : 𝐬0(T) >> 𝐫1(T) = 𝐬1 := by congr @[simp, grind =] - theorem rewrite1 : re 0 :: +1σ = id T := by + theorem rewrite1 : re 0 :: 𝐬1 = id T := by simp [Subst.cons, Subst.id] funext; case _ x => cases x; all_goals simp @[simp, grind =] - theorem rewrite1_ren : 0 :: +1r = Ren.id T := by + theorem rewrite1_ren : 0 :: 𝐫1 = Ren.id T := by simp [Ren.cons, Ren.id] funext; case _ x => cases x <;> simp @@ -36,99 +37,100 @@ namespace Subst open SubstMap @[simp, grind =] - theorem I_lift [RenMap T T] {k} : +0σ.lift k = id T := by + theorem I_lift [RenMap T [T]] {k} : 𝐬0.lift k = id T := by funext; case _ x => cases x; all_goals (simp [lift, id, act, SubstAction.act]) grind - @[simp, grind =] - theorem rewrite2 [SubstMap T T] {σ : Subst T} : +0σ ∘ σ = σ := by + @[simp] + theorem rewrite2 [SubstMap T [T]] {σ : Subst T} : 𝐬0 >> σ = σ := by funext; case _ x => - simp [compose, id, act, SubstAction.act] + simp [HAndThen.hAndThen, AndThen.andThen, compose, id, act, SubstAction.act] - @[simp, grind =] - theorem rewrite2_ren [SubstMap T T] {σ : Subst T} : +0r ∘ σ = σ := by + @[simp] + theorem rewrite2_ren [SubstMap T [T]] {σ : Subst T} : Ren.id T >> σ = σ := by funext; case _ x => - simp [compose_ren_left, act, SubstAction.act] + simp [HAndThen.hAndThen, compose_ren_left, act, SubstAction.act] - @[simp, grind =] - theorem rewrite3_cons [SubstMap T T] {σ τ : Subst T} {a : Action T} - : (a :: σ) ∘ τ = a[τ] :: (σ ∘ τ) + @[simp] + theorem rewrite3_cons [SubstMap T [T]] {σ τ : Subst T} {a : Action T} + : (a :: σ) >> τ = a[τ] :: (σ >> τ) := by - simp [cons, compose] + simp [cons, HAndThen.hAndThen, AndThen.andThen, compose] funext; case _ x => cases x; all_goals simp [act, SubstAction.act] - @[simp, grind =] - theorem rewrite3_cons_ren [RenMap T T] [SubstMap T T] {σ : Subst T} {r : Ren T} {x : Nat} - : (re x :: σ) ∘ r = re (r.act x) :: (σ ∘ r) + @[simp] + theorem rewrite3_cons_ren [RenMap T [T]] [SubstMap T [T]] {σ : Subst T} {r : Ren T} {x : Nat} + : (re x :: σ) >> r = re (r.act x) :: (σ >> r) := by - simp [cons, compose_ren_right] + simp [cons, HAndThen.hAndThen, compose_ren_right] funext; case _ x => cases x; all_goals simp [act, SubstAction.act] - @[simp, grind =] - theorem rewrite3_append [SubstMap T T] {σ τ : Subst T} {ℓ : List (Action T)} - : (ℓ ++ σ) ∘ τ = ℓ[τ] ++ (σ ∘ τ) + @[simp] + theorem rewrite3_append [SubstMap T [T]] {σ τ : Subst T} {ℓ : List (Action T)} + : (ℓ ++ σ) >> τ = ℓ[τ] ++ (σ >> τ) := by induction ℓ generalizing σ τ <;> simp case _ hd tl ih => cases hd <;> simp [*] - @[simp, grind =] - theorem rewrite3_append_act [SubstMap T T] {σ τ : Subst T} {ℓ : List Nat} - : (ℓ ++ σ) ∘ τ = τ.act ℓ ++ (σ ∘ τ) + @[simp] + theorem rewrite3_append_act [SubstMap T [T]] {σ τ : Subst T} {ℓ : List Nat} + : (ℓ ++ σ) >> τ = τ.act ℓ ++ (σ >> τ) := by induction ℓ generalizing σ τ <;> simp [*] - @[simp, grind =] - theorem rewrite3_append_ren [RenMap T T] [SubstMap T T] {σ : Subst T} {r : Ren T} {ℓ : List Nat} - : (ℓ ++ σ) ∘ r = ℓ⟨r⟩ ++ (σ ∘ r) + @[simp] + theorem rewrite3_append_ren [RenMap T [T]] [SubstMap T [T]] {σ : Subst T} {r : Ren T} {ℓ : List Nat} + : (ℓ ++ σ) >> r = ℓ⟨r⟩ ++ (σ >> r) := by induction ℓ generalizing σ r <;> simp case _ hd tl ih => cases hd <;> simp [*] - @[simp, grind =] - theorem rewrite4_cons [SubstMap T T] {s} {σ : Subst T} : +1σ ∘ (s :: σ) = σ := by + @[simp] + theorem rewrite4_cons [SubstMap T [T]] {s} {σ : Subst T} : 𝐬1 >> (s :: σ) = σ := by simp [Subst.cons] funext; case _ x => - cases x; all_goals (simp [compose, succ, act, SubstAction.act]) + cases x; all_goals (simp [HAndThen.hAndThen, AndThen.andThen, compose, succ, act, SubstAction.act]) - @[simp, grind =] - theorem rewrite4_cons_ren [SubstMap T T] {s} {σ : Subst T} : +1r ∘ (s :: σ) = σ := by + @[simp] + theorem rewrite4_cons_ren [SubstMap T [T]] {s} {σ : Subst T} : Ren.succ T >> (s :: σ) = σ := by simp [Subst.cons] funext; case _ x => - cases x; all_goals (simp [compose_ren_left, act, SubstAction.act]) + cases x; all_goals (simp [HAndThen.hAndThen, compose_ren_left, act, SubstAction.act]) @[simp, grind =] - theorem rewrite5 [SubstMap T T] {σ : Subst T} : σ.act 0 :: (+1σ ∘ σ) = σ := by - simp [Subst.cons, Subst.compose]; congr + theorem rewrite5 [SubstMap T [T]] {σ : Subst T} : σ.act 0 :: (𝐬1 >> σ) = σ := by + simp [cons, HAndThen.hAndThen, AndThen.andThen, compose]; congr funext; case _ x => cases x <;> simp [act, SubstAction.act] - @[simp, grind =] - theorem rewrite5_ren [SubstMap T T] {σ : Subst T} : σ.act 0 :: (+1r ∘ σ) = σ := by + @[simp] + theorem rewrite5_ren [SubstMap T [T]] {σ : Subst T} : σ.act 0 :: (Ren.succ T >> σ) = σ := by simp [Subst.cons]; congr funext; case _ x => cases x <;> simp [act, SubstAction.act] end @[simp, grind =] - theorem rewrite_lift [RenMap T T] {σ : Subst T} - : σ.lift = re 0 :: (σ ∘ +1r) + theorem rewrite_lift [RenMap T [T]] {σ : Subst T} + : σ.lift = re 0 :: (σ >> 𝐫1(T)) := by - simp [cons, lift, compose_ren_right] + simp [cons, lift] funext; case _ x => cases x <;> simp @[simp, grind =] - theorem rewrite_lift_zero [RenMap T T] [RenMapId T T] {σ : Subst T} + theorem rewrite_lift_zero [RenMap T [T]] [RenMapId T [T]] {σ : Subst T} : σ.lift 0 = σ - := by simp [lift, act, SubstAction.act] + := by + simp [lift, act, SubstAction.act] @[grind =] theorem rewrite_lift_succ - [RenMap T T] [RenMapId T T] [RenMapCompose T T] + [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] {k} {σ : Subst T} : σ.lift (k + 1) = (σ.lift k).lift := by @@ -142,12 +144,13 @@ namespace Subst case _ k => split <;> simp rw [Ren.compose_add_succ_right] + congr @[simp, grind =] - theorem rewrite6 [RenMap T T] [SubstMap T T] [SubstMapId T T] {σ : Subst T} - : σ ∘ +0σ = σ + theorem rewrite6 [RenMap T [T]] [SubstMap T [T]] [SubstMapId T [T]] {σ : Subst T} + : σ >> 𝐬0 = σ := by - simp [compose, id, act, SubstAction.act]; congr; funext; case _ x => + simp [HAndThen.hAndThen, AndThen.andThen, compose, id, act, SubstAction.act]; congr; funext; case _ x => generalize zdef : σ.inner x = z cases z <;> simp [act, SubstAction.act] case _ t => @@ -155,43 +158,37 @@ namespace Subst simp [id] at lem; exact lem @[simp, grind =] - theorem rewrite6_ren [RenMap T T] [RenMapId T T] {σ : Subst T} - : σ ∘ +0r = σ + theorem rewrite6_ren [RenMap T [T]] [RenMapId T [T]] {σ : Subst T} + : σ >> 𝐫0(T) = σ := by - simp [compose_ren_right]; congr + simp [HAndThen.hAndThen, compose_ren_right]; congr - @[simp, grind =] + @[simp] theorem rewrite7 - [SubstMap T T] [SubstMapCompose T T] + [SubstMap T [T]] [SubstMapCompose T [T]] {σ τ μ : Subst T} - : (σ ∘ τ) ∘ μ = σ ∘ τ ∘ μ + : (σ >> τ) >> μ = σ >> τ >> μ := by - simp [Subst.compose, act, SubstAction.act] + simp [HAndThen.hAndThen, AndThen.andThen, compose, act, SubstAction.act] funext; case _ x => cases σ.inner x <;> simp [act, SubstAction.act] - simp [compose, act, SubstAction.act] + simp [HAndThen.hAndThen, AndThen.andThen, SubstVec.compose, compose, act, SubstAction.act] + congr - @[simp, grind =] - theorem rewrite7_ren - [RenMap T T] [RenMapCompose T T] - {σ : Subst T} {r1 r2 : Ren T} - : (σ ∘ r1) ∘ r2 = σ ∘ r1 ∘ r2 - := by simp [compose_ren_right] - - @[simp, grind =] - theorem rewrite4_append_direct [SubstMap T T] [SubstMapCompose T T] + @[simp] + theorem rewrite4_append_direct [SubstMap T [T]] [SubstMapCompose T [T]] {ℓ : List $ Action T} {σ : Subst T} - : (add T ℓ.length) ∘ (ℓ ++ σ) = σ + : (add T ℓ.length) >> (ℓ ++ σ) = σ := by induction ℓ generalizing σ <;> simp case _ hd tl ih => rw [compose_add_succ_right] simp [*] - @[simp, grind <-] - theorem rewrite4_append_indirect [SubstMap T T] [SubstMapCompose T T] + @[simp] + theorem rewrite4_append_indirect [SubstMap T [T]] [SubstMapCompose T [T]] {k} {ℓ : List $ Action T} {σ : Subst T} (h : k = ℓ.length) - : (add T k) ∘ (ℓ ++ σ) = σ + : (add T k) >> (ℓ ++ σ) = σ := by subst h; simp @[grind =] @@ -229,7 +226,7 @@ namespace Subst @[simp] theorem range_act_succ_ren {s e : Nat} {σ : Subst T} - : (s..e)⟨.succ T⟩ ++ σ = s.succ..e.succ ++ σ + : (s..e)⟨Ren.succ T⟩ ++ σ = s.succ..e.succ ++ σ := by induction e generalizing s σ <;> simp case _ e ih => @@ -252,262 +249,266 @@ namespace Subst @[simp, grind =] theorem rewrite_lift_k - [RenMap T T] [RenMapId T T] [RenMapCompose T T] - [SubstMap T T] [SubstMapId T T] [SubstMapCompose T T] + [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] + [SubstMap T [T]] [SubstMapId T [T]] [SubstMapCompose T [T]] {k} {σ : Subst T} - : σ.lift k = 0..k ++ (σ ∘ +r k) + : σ.lift k = 0..k ++ (σ >> Ren.add T k) := by induction k generalizing σ <;> simp case _ k ih => rw [rewrite_lift_succ, ih] - simp; congr - - @[simp, grind =] - theorem hrewrite1 [SubstMap S T] [SubstMapId S T] {σ : Subst S} : σ ◾ (id T) = σ := by - simp [hcompose, act, SubstAction.act]; congr - funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp - - @[simp, grind =] - theorem hrewrite1_ren [RenMap S T] [RenMapId S T] {σ : Subst S} : σ ◾ (.id T) = σ := by - simp [hcompose_ren, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite2 [SubstMap S T] {σ : Subst T} : (id S) ◾ σ = +0σ := by - simp [hcompose, id, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite2_ren [RenMap S T] {r : Ren T} : (id S) ◾ r = +0σ := by - simp [hcompose_ren, id, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite3 [SubstMap S T] {σ : Subst T} : (succ S) ◾ σ = +1σ := by - simp [hcompose, succ, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite3_ren [RenMap S T] {r : Ren T} : (succ S) ◾ r = +1σ := by - simp [hcompose_ren, succ, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite4 - [SubstMap S T] - {x} {σ : Subst S} {τ : Subst T} - : (re x :: σ) ◾ τ = re x :: (σ ◾ τ) - := by - simp [Subst.hcompose, act]; congr - funext; case _ i => - cases i <;> simp [Subst.cons, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite4_ren - [RenMap S T] - {x} {σ : Subst S} {r : Ren T} - : (re x :: σ) ◾ r = re x :: (σ ◾ r) - := by - simp [hcompose_ren, act]; congr - funext; case _ i => - cases i <;> simp [Subst.cons, act, SubstAction.act] - - @[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, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite5_subst_subst - [SubstMap S T] [SubstMap T T] [SubstMapCompose S T] - {σ : Subst S} {τ μ : Subst T} - : (σ ◾ τ) ◾ μ = σ ◾ (τ ∘ μ) - := by - simp [Subst.hcompose, act, SubstAction.act] - funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp - - @[simp, grind =] - theorem hrewrite5_subst_ren - [RenMap S T] [RenMap T T] [SubstMap S T] [SubstMapRenComposeRight S T] - {σ : Subst S} {τ : Subst T} {r : Ren T} - : (σ ◾ τ) ◾ r = σ ◾ (τ ∘ r) - := by - simp [hcompose_ren, hcompose, act, SubstAction.act] - funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp - - @[simp, grind =] - theorem hrewrite5_ren_subst - [RenMap S T] [SubstMap S T] [SubstMapRenComposeLeft S T] - {σ : Subst S} {τ : Subst T} {r : Ren T} - : (σ ◾ r) ◾ τ = σ ◾ (r ∘ τ) - := by - simp [hcompose_ren, hcompose, act, SubstAction.act] - funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp - - @[simp, grind =] - theorem hrewrite5_ren_ren - [RenMap S T] [SubstMap S T] [RenMapCompose S T] - {σ : Subst S} {r1 r2 : Ren T} - : (σ ◾ r1) ◾ r2 = σ ◾ (r1 ∘ r2) - := by - simp [hcompose_ren, act, SubstAction.act] - - @[grind =] - theorem hcomp_distr_ren_right - [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] - (r : Ren S) (σ : Subst S) (μ : Subst T) - : (σ ∘ r) ◾ μ = (σ ◾ μ) ∘ r - := by - simp [hcompose, compose_ren_right, act, SubstAction.act]; funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp - rw [apply_commute_ren_subst] - - @[simp, grind =] - theorem hrewrite7 - [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] - {σ τ : Subst S} (μ : Subst T) - : (σ ∘ τ) ◾ μ = (σ ◾ μ) ∘ τ ◾ μ - := by - simp [hcompose, compose, act, SubstAction.act] - funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp [hcompose, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite7_ren - [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenHetCompose S T] - {σ τ : Subst S} {r : Ren T} - : (σ ∘ τ) ◾ r = (σ ◾ r) ∘ τ ◾ r - := by - simp [hcompose_ren, compose, act, SubstAction.act] - funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp [hcompose_ren, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite8 - [SubstMap S S] [SubstMap S T] - {r : Ren S} {τ : Subst S} (μ : Subst T) - : (r ∘ τ) ◾ μ = r ∘ τ ◾ μ - := by - simp [hcompose, compose_ren_left, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite8_ren - [RenMap S T] [SubstMap S S] [SubstMap S T] - {r : Ren S} {τ : Subst S} (μ : Ren T) - : (r ∘ τ) ◾ μ = r ∘ τ ◾ μ - := by - simp [hcompose_ren, compose_ren_left, act, SubstAction.act] - - @[simp, grind =] - theorem hrewrite9 - [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] - {σ : Subst S} {r : Ren S} (μ : Subst T) - : (σ ∘ r) ◾ μ = (σ ◾ μ) ∘ r - := by - simp [hcompose, compose_ren_right, act, SubstAction.act] - funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp - rw [apply_commute_ren_subst] - - @[simp, grind =] - theorem hrewrite9_ren - [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] - {σ : Subst S} {r : Ren S} (μ : Ren T) - : (σ ∘ r) ◾ μ = (σ ◾ μ) ∘ r - := by - simp [hcompose_ren, compose_ren_right, act, SubstAction.act] - funext; case _ x => - generalize zdef : σ.inner x = z - cases z <;> simp - rw [apply_commute_ren_ren] - - theorem hrewrite_lift1 - [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] - {σ : Subst S} {τ : Subst T} - : (σ ◾ τ).lift = σ.lift ◾ τ - := by - simp [lift, act, SubstAction.act]; congr; funext; case _ i => - cases i <;> simp [act, SubstAction.act] - case _ n => - simp [hcompose, act, SubstAction.act] - generalize zdef : σ.inner n = z - cases z <;> simp; case _ t => - rw [apply_commute_ren_subst] - - @[simp, grind =] - theorem hrewrite_lift - [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] - [RenMapId S S] [RenMapCompose S 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] - grind - - theorem hrewrite_lift1_ren - [RenMap S S] [SubstMap S S] [RenMap S T] [SubstMap S T] [SubstMapRenCommute S T] - {σ : Subst S} {τ : Ren T} - : (σ ◾ τ).lift = σ.lift ◾ τ - := by - simp [lift, act, SubstAction.act]; congr; funext; case _ i => - cases i <;> simp [act, SubstAction.act] - case _ n => - simp [hcompose_ren, act, SubstAction.act] - generalize zdef : σ.inner n = z - cases z <;> simp; case _ t => - rw [apply_commute_ren_ren] - - @[simp, grind =] - theorem hrewrite_lift_ren - [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] - [RenMapId S S] [RenMapCompose S S] [SubstMapRenCommute S T] - {k} {σ : Subst S} {τ : Ren T} - : (σ ◾ τ).lift k = σ.lift k ◾ τ - := by - induction k generalizing σ τ - case _ => simp - case _ i ih => - rw [rewrite_lift_succ] - rw [rewrite_lift_succ (k := i)] - simp; rw [ih] + simp + sorry + -- rw [rewrite_lift_succ, ih] + -- simp; congr + + -- @[simp, grind =] + -- theorem hrewrite1 [SubstMap S T] [SubstMapId S T] {σ : Subst S} : σ ◾ (id T) = σ := by + -- simp [hcompose, act, SubstAction.act]; congr + -- funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp + + -- @[simp, grind =] + -- theorem hrewrite1_ren [RenMap S T] [RenMapId S T] {σ : Subst S} : σ ◾ (.id T) = σ := by + -- simp [hcompose_ren, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite2 [SubstMap S T] {σ : Subst T} : (id S) ◾ σ = 𝐬0 := by + -- simp [hcompose, id, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite2_ren [RenMap S T] {r : Ren T} : (id S) ◾ r = 𝐬0 := by + -- simp [hcompose_ren, id, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite3 [SubstMap S T] {σ : Subst T} : (succ S) ◾ σ = 𝐬1 := by + -- simp [hcompose, succ, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite3_ren [RenMap S T] {r : Ren T} : (succ S) ◾ r = 𝐬1 := by + -- simp [hcompose_ren, succ, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite4 + -- [SubstMap S T] + -- {x} {σ : Subst S} {τ : Subst T} + -- : (re x :: σ) ◾ τ = re x :: (σ ◾ τ) + -- := by + -- simp [Subst.hcompose, act]; congr + -- funext; case _ i => + -- cases i <;> simp [Subst.cons, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite4_ren + -- [RenMap S T] + -- {x} {σ : Subst S} {r : Ren T} + -- : (re x :: σ) ◾ r = re x :: (σ ◾ r) + -- := by + -- simp [hcompose_ren, act]; congr + -- funext; case _ i => + -- cases i <;> simp [Subst.cons, act, SubstAction.act] + + -- @[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, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite5_subst_subst + -- [SubstMap S T] [SubstMap T [T]] [SubstMapCompose S T] + -- {σ : Subst S} {τ μ : Subst T} + -- : (σ ◾ τ) ◾ μ = σ ◾ (τ >> μ) + -- := by + -- simp [Subst.hcompose, act, SubstAction.act] + -- funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp + + -- @[simp, grind =] + -- theorem hrewrite5_subst_ren + -- [RenMap S T] [RenMap T [T]] [SubstMap S T] [SubstMapRenComposeRight S T] + -- {σ : Subst S} {τ : Subst T} {r : Ren T} + -- : (σ ◾ τ) ◾ r = σ ◾ (τ >> r) + -- := by + -- simp [hcompose_ren, hcompose, act, SubstAction.act] + -- funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp + + -- @[simp, grind =] + -- theorem hrewrite5_ren_subst + -- [RenMap S T] [SubstMap S T] [SubstMapRenComposeLeft S T] + -- {σ : Subst S} {τ : Subst T} {r : Ren T} + -- : (σ ◾ r) ◾ τ = σ ◾ (r >> τ) + -- := by + -- simp [hcompose_ren, hcompose, act, SubstAction.act] + -- funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp + + -- @[simp, grind =] + -- theorem hrewrite5_ren_ren + -- [RenMap S T] [SubstMap S T] [RenMapCompose S T] + -- {σ : Subst S} {r1 r2 : Ren T} + -- : (σ ◾ r1) ◾ r2 = σ ◾ (r1 >> r2) + -- := by + -- simp [hcompose_ren, act, SubstAction.act] + + -- @[grind =] + -- theorem hcomp_distr_ren_right + -- [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] + -- (r : Ren S) (σ : Subst S) (μ : Subst T) + -- : (σ >> r) ◾ μ = (σ ◾ μ) >> r + -- := by + -- simp [hcompose, compose_ren_right, act, SubstAction.act]; funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp + -- rw [apply_commute_ren_subst] + + -- @[simp, grind =] + -- theorem hrewrite7 + -- [SubstMap S S] [SubstMap S T] [SubstMapHetCompose S T] + -- {σ τ : Subst S} (μ : Subst T) + -- : (σ >> τ) ◾ μ = (σ ◾ μ) >> τ ◾ μ + -- := by + -- simp [hcompose, compose, act, SubstAction.act] + -- funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp [hcompose, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite7_ren + -- [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenHetCompose S T] + -- {σ τ : Subst S} {r : Ren T} + -- : (σ >> τ) ◾ r = (σ ◾ r) >> τ ◾ r + -- := by + -- simp [hcompose_ren, compose, act, SubstAction.act] + -- funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp [hcompose_ren, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite8 + -- [SubstMap S S] [SubstMap S T] + -- {r : Ren S} {τ : Subst S} (μ : Subst T) + -- : (r >> τ) ◾ μ = r >> τ ◾ μ + -- := by + -- simp [hcompose, compose_ren_left, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite8_ren + -- [RenMap S T] [SubstMap S S] [SubstMap S T] + -- {r : Ren S} {τ : Subst S} (μ : Ren T) + -- : (r >> τ) ◾ μ = r >> τ ◾ μ + -- := by + -- simp [hcompose_ren, compose_ren_left, act, SubstAction.act] + + -- @[simp, grind =] + -- theorem hrewrite9 + -- [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] + -- {σ : Subst S} {r : Ren S} (μ : Subst T) + -- : (σ >> r) ◾ μ = (σ ◾ μ) >> r + -- := by + -- simp [hcompose, compose_ren_right, act, SubstAction.act] + -- funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp + -- rw [apply_commute_ren_subst] + + -- @[simp, grind =] + -- theorem hrewrite9_ren + -- [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] + -- {σ : Subst S} {r : Ren S} (μ : Ren T) + -- : (σ >> r) ◾ μ = (σ ◾ μ) >> r + -- := by + -- simp [hcompose_ren, compose_ren_right, act, SubstAction.act] + -- funext; case _ x => + -- generalize zdef : σ.inner x = z + -- cases z <;> simp + -- rw [apply_commute_ren_ren] + + -- theorem hrewrite_lift1 + -- [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] [SubstMapRenCommute S T] + -- {σ : Subst S} {τ : Subst T} + -- : (σ ◾ τ).lift = σ.lift ◾ τ + -- := by + -- simp [lift, act, SubstAction.act]; congr; funext; case _ i => + -- cases i <;> simp [act, SubstAction.act] + -- case _ n => + -- simp [hcompose, act, SubstAction.act] + -- generalize zdef : σ.inner n = z + -- cases z <;> simp; case _ t => + -- rw [apply_commute_ren_subst] + + -- @[simp, grind =] + -- theorem hrewrite_lift + -- [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] + -- [RenMapId S S] [RenMapCompose S 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] + -- grind + + -- theorem hrewrite_lift1_ren + -- [RenMap S S] [SubstMap S S] [RenMap S T] [SubstMap S T] [SubstMapRenCommute S T] + -- {σ : Subst S} {τ : Ren T} + -- : (σ ◾ τ).lift = σ.lift ◾ τ + -- := by + -- simp [lift, act, SubstAction.act]; congr; funext; case _ i => + -- cases i <;> simp [act, SubstAction.act] + -- case _ n => + -- simp [hcompose_ren, act, SubstAction.act] + -- generalize zdef : σ.inner n = z + -- cases z <;> simp; case _ t => + -- rw [apply_commute_ren_ren] + + -- @[simp, grind =] + -- theorem hrewrite_lift_ren + -- [RenMap S S] [RenMap S T] [SubstMap S S] [SubstMap S T] + -- [RenMapId S S] [RenMapCompose S S] [SubstMapRenCommute S T] + -- {k} {σ : Subst S} {τ : Ren T} + -- : (σ ◾ τ).lift k = σ.lift k ◾ τ + -- := by + -- induction k generalizing σ τ + -- case _ => simp + -- case _ i ih => + -- rw [rewrite_lift_succ] + -- rw [rewrite_lift_succ (k := i)] + -- simp; rw [ih] end Subst @[grind =] -theorem Subst.compose_commute_succ [RenMap T T] {τ : Subst T} - : τ ∘ Ren.succ T = Ren.succ T ∘ τ.lift +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 Ren.compose_commute_succ {r : Ren T} : r >> succ T = succ T >> r.lift := by + simp [HAndThen.hAndThen, AndThen.andThen, compose] -theorem Subst.rewrite_lift_compose_ren_left_k1 [RenMap T T] {r : Ren T} {τ : Subst T} - : (r ∘ τ).lift = r.lift ∘ τ.lift +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, act, SubstAction.act] + simp [HAndThen.hAndThen, compose_ren_left, lift, Ren.lift, act, SubstAction.act] funext; case _ x => cases x <;> simp -@[simp, grind =] +@[simp] theorem Subst.rewrite_lift_compose_ren_left - [RenMap T T] [RenMapId T T] [RenMapCompose T T] + [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] {k} {r : Ren T} {τ : Subst T} - : (r ∘ τ).lift k = r.lift k ∘ τ.lift k + : (r >> τ).lift k = r.lift k >> τ.lift k := by induction k generalizing r τ; congr case _ k ih => @@ -517,19 +518,20 @@ theorem Subst.rewrite_lift_compose_ren_left rw [<-Ren.lift_of_succ] theorem Subst.lift_compose_ren_right_k1 - [RenMap T T] [RenMapId T T] [RenMapCompose T T] + [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] {σ : Subst T} {r : Ren T} - : (σ ∘ r).lift = σ.lift ∘ r.lift + : (σ >> r).lift = σ.lift >> r.lift := by simp [lift, act, SubstAction.act]; congr; funext; case _ x => cases x <;> simp [act, SubstAction.act]; case _ x => - simp [compose_ren_right, act, SubstAction.act]; grind + simp [HAndThen.hAndThen, AndThen.andThen, compose_ren_right, RenVec.compose, act, SubstAction.act] + congr 1 -@[simp, grind =] +@[simp] theorem Subst.lift_compose_ren_right - [RenMap T T] [RenMapId T T] [RenMapCompose T T] + [RenMap T [T]] [SubstMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] {k} {σ : Subst T} {r : Ren T} - : (σ ∘ r).lift k = σ.lift k ∘ r.lift k + : (σ >> r).lift k = σ.lift k >> r.lift k := by induction k generalizing σ r; simp case _ k ih => @@ -539,25 +541,23 @@ theorem Subst.lift_compose_ren_right rw [<-Ren.lift_of_succ] theorem Subst.rewrite_lift_compose_k1 - [RenMap T T] [SubstMap T T] [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T T] + [RenMap T [T]] [SubstMap T [T]] [SubstMapRenComposeLeft T [T]] [SubstMapRenComposeRight T [T]] {σ τ : Subst T} - : (σ ∘ τ).lift = σ.lift ∘ τ.lift + : (σ >> τ).lift = σ.lift >> τ.lift := by - simp [compose, lift, act, SubstAction.act] + simp [HAndThen.hAndThen, AndThen.andThen, compose, lift, act, SubstAction.act] funext; case _ x => cases x <;> simp [act, SubstAction.act] case _ x => cases σ.inner x <;> simp [act, SubstAction.act]; case _ t => - have lem := Subst.compose_commute_succ (τ := τ) - simp [lift, act, SubstAction.act] at lem - rw [lem] + simp [HAndThen.hAndThen, SubstVec.compose_ren_right, SubstVec.compose_ren_left]; congr -@[simp, grind =] +@[simp] theorem Subst.rewrite_lift_compose - [RenMap T T] [RenMapId T T] [RenMapCompose T T] [SubstMap T T] - [SubstMapRenComposeLeft T T] [SubstMapRenComposeRight T T] + [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] [SubstMap T [T]] + [SubstMapRenComposeLeft T [T]] [SubstMapRenComposeRight T [T]] {k} {σ τ : Subst T} - : (σ ∘ τ).lift k = σ.lift k ∘ τ.lift k + : (σ >> τ).lift k = σ.lift k >> τ.lift k := by induction k generalizing σ τ; simp case _ k ih => diff --git a/LeanSubst/Misc.lean b/LeanSubst/Misc.lean index d9ffd45..4eaceb1 100644 --- a/LeanSubst/Misc.lean +++ b/LeanSubst/Misc.lean @@ -10,34 +10,35 @@ import LeanSubst.Types.List namespace LeanSubst universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} {U : Type u3} +variable {S : Type u1} {T T1 T2 : Type u2} {U : Type u3} +variable {V : List (Type u2)} -instance [RenMap S T] [SubstMap S T] [SubstMapRenComposeLeft S T] : SubstMapRenComposeLeft (List S) T where +instance [RenMap S V] [SubstMap S V] [SubstMapRenComposeLeft S V] : SubstMapRenComposeLeft (List S) V where apply_ren_compose_left := by intro s r τ; induction s <;> simp [*] -instance [RenMap S T] [RenMap T T] [SubstMap S T] [SubstMapRenComposeRight S T] : SubstMapRenComposeRight (List S) T where +instance [RenMap S V] [RenMapAll V] [SubstMap S V] [SubstMapRenComposeRight S V] : SubstMapRenComposeRight (List S) V where apply_ren_compose_right := by intro s r τ; induction s <;> simp [*] -@[simp, grind =] -theorem Subst.rewrite3_cons_ren_fix [RenMap T T] [SubstMap T T] {a} {σ : Subst T} {r : Ren T} - : (a :: σ) ∘ r = a⟨r⟩:: (σ ∘ r) +@[simp] +theorem Subst.rewrite3_cons_ren_fix [RenMap T [T]] [SubstMap T [T]] {a} {σ : Subst T} {r : Ren T} + : (a :: σ) >> r = a⟨r⟩::(σ >> r) := by - simp [cons, compose_ren_right] + simp [cons, HAndThen.hAndThen, compose_ren_right] funext; case _ x => cases x; all_goals simp [act, SubstAction.act] -@[simp, grind =] -theorem Subst.rewrite3_cons_ren_subst [SubstMap T T] {x} {σ : Subst T} {r : Ren T} - : (x :: r) ∘ σ = σ.act x :: (r ∘ σ) +@[simp] +theorem Subst.rewrite3_cons_ren_subst [SubstMap T [T]] {x} {σ : Subst T} {r : Ren T} + : (x :: r) >> σ = σ.act x :: (r >> σ) := by - simp [cons, compose_ren_left] + simp [cons, HAndThen.hAndThen, compose_ren_left] funext; case _ x => cases x; all_goals simp [act, SubstAction.act] -@[simp, grind =] +@[simp] theorem Subst.ren_succ_beta_to {a} {r : Ren T} - : (r ∘ Ren.succ T) ∘ (a :: Subst.id T) = r.to -:= by simp [compose_ren_left, Ren.to] + : (r >> Ren.succ T) >> (a :: Subst.id T) = r.to +:= by simp [HAndThen.hAndThen, AndThen.andThen, compose_ren_left, Ren.compose, Ren.to] theorem Ren.lift_of_succ_rev {k} {r : Ren S} : r.lift (1 + k) = r.lift.lift k := by induction k; simp @@ -53,31 +54,27 @@ theorem Ren.lift_of_add {a b} {r : Ren S} : r.lift (a + b) = (r.lift a).lift b : rw [<-Ren.lift_of_succ_rev] rw [<-ih]; congr 1; omega -@[grind =] -theorem Subst.compose_commute_add [RenMap T T] [SubstMap T T] [SubstMapStable T T] {k} {τ : Subst T} - : τ ∘ add T k = add T k ∘ τ.lift k +theorem Subst.compose_commute_add [RenMap T [T]] [SubstMap T [T]] [SubstMapStable T [T]] {k} {τ : Subst T} + : τ >> add T k = add T k >> τ.lift k := by - simp [compose]; funext; case _ x => + simp [HAndThen.hAndThen, AndThen.andThen, compose]; funext; case _ x => generalize zdef : τ.act x = z cases z <;> simp - rw [apply_stable]; simp + rw [SubstMapStable.apply_stable]; simp [RenVec.to] -@[grind =] -theorem Subst.compose_commute_add_ren_subst [RenMap T T] [SubstMap T T] [SubstMapStable T T] {k} {τ : Subst T} - : τ ∘ Ren.add T k = Ren.add T k ∘ τ.lift k +theorem Subst.compose_commute_add_ren_subst [RenMap T [T]] [SubstMap T [T]] [SubstMapStable T [T]] {k} {τ : Subst T} + : τ >> Ren.add T k = Ren.add T k >> τ.lift k := by - simp [compose_ren_right, compose_ren_left] + simp [HAndThen.hAndThen, compose_ren_right, compose_ren_left] -@[grind =] -theorem Subst.compose_commute_add_ren [RenMap T T] {k} {r : Ren T} - : r ∘ add T k = add T k ∘ r.lift k +theorem Subst.compose_commute_add_ren [RenMap T [T]] {k} {r : Ren T} + : r >> add T k = add T k >> r.lift k := by - simp [compose_ren_left, compose_ren_right] + simp [HAndThen.hAndThen, compose_ren_left, compose_ren_right] -@[grind =] theorem Subst.compose_commute_add_ren_ren {k} {r : Ren T} - : r ∘ Ren.add T k = .add T k ∘ r.lift k -:= by simp [Ren.compose] + : r >> Ren.add T k = .add T k >> r.lift k +:= by simp [HAndThen.hAndThen, AndThen.andThen, Ren.compose] @[simp] theorem Ren.to_cons {x} {r : Ren T} : (x::r).to = re x :: r.to := by @@ -99,7 +96,7 @@ theorem Ren.assoc {T} {xs ys : List Nat} {r : Ren T} : xs ++ (ys ++ r) = xs ++ y theorem Ren.append_range_succ_succ {T s e} {r : Ren T} {h : s ≤ e + 1} : s..(e + 2) ++ r = s..(e + 1) ++ ((e + 1) :: r) := by simp_all [Ren.range, ← Ren.assoc] -theorem Subst.rewrite1_append_ren_le {T s e} : s..e ++ +r e = .add T (min s e) := by +theorem Subst.rewrite1_append_ren_le {T s e} : s..e ++ Ren.add T e = .add T (min s e) := by induction e generalizing s ; simp case succ e ih => cases Nat.decLt s (e + 1) @@ -129,7 +126,7 @@ theorem Subst.cons_add_succ {T n} : re n :: add T (n + 1) = add T n := by simp [cons, add] funext ; split <;> congr 1 <;> omega -theorem Subst.rewrite1_append_le {T s e} : s..e ++ +σ e = add T (min s e) := by +theorem Subst.rewrite1_append_le {T s e} : s..e ++ add T e = add T (min s e) := by induction e generalizing s ; simp case succ e ih => cases Nat.decLt s (e + 1) @@ -146,36 +143,36 @@ theorem Subst.rewrite1_append_le {T s e} : s..e ++ +σ e = add T (min s e) := by @[simp, grind =] -theorem Subst.rewrite1_append_ren {e} : 0..e ++ +r e = .id T := by +theorem Subst.rewrite1_append_ren {e} : 0..e ++ Ren.add T e = .id T := by have lem := @rewrite1_append_ren_le T 0 e simp at lem; exact lem @[simp, grind =] -theorem Subst.rewrite1_append {e} : 0..e ++ +σ e = id T := by +theorem Subst.rewrite1_append {e} : 0..e ++ add T e = id T := by have lem := @rewrite1_append_le T 0 e simp at lem; exact lem @[simp, grind =] -theorem Subst.rewrite_lift_ren {r : Ren T} : r.lift = 0::(r ∘ +1r) := by +theorem Subst.rewrite_lift_ren {r : Ren T} : r.lift = 0::(r >> 𝐫1) := by simp [Ren.lift, Ren.cons]; funext; case _ x => cases x <;> simp -@[simp, grind =] +@[simp] theorem Subst.rewrite3_append_ren_ren_cons {x} {r1 r2 : Ren T} - : (x::r1) ∘ r2 = r2.act x::(r1 ∘ r2) + : (x::r1) >> r2 = r2.act x::(r1 >> r2) := by - simp [Ren.cons, Ren.compose]; funext; case _ x => + simp [Ren.cons, HAndThen.hAndThen, AndThen.andThen, Ren.compose]; funext; case _ x => cases x <;> simp -@[simp, grind =] +@[simp] theorem Subst.rewrite3_append_ren_ren {ℓ : List Nat} {r1 r2 : Ren T} - : (ℓ ++ r1) ∘ r2 = ℓ⟨r2⟩ ++ (r1 ∘ r2) + : (ℓ ++ r1) >> r2 = ℓ⟨r2⟩ ++ (r1 >> r2) := by induction ℓ generalizing r1 r2 <;> simp [*] @[simp] theorem range_act_succ_ren_fixed {s e} - : (s..e)⟨.succ T⟩ = s.succ..e.succ + : (s..e)⟨Ren.succ T⟩ = s.succ..e.succ := by induction e generalizing s; simp case _ e ih => @@ -191,192 +188,195 @@ theorem range_act_succ_ren_fixed {s e} split <;> simp @[simp, grind =] -theorem Subst.rewrite_lift_k_ren {k} {r : Ren T} : r.lift k = 0..k ++ (r ∘ +r k) := by +theorem Subst.rewrite_lift_k_ren {k} {r : Ren T} : r.lift k = 0..k ++ (r >> Ren.add T k) := by induction k generalizing r <;> simp case _ k ih => rw [Ren.lift_of_succ, ih]; simp rw [<-Ren.compose_add_succ_right] -@[simp, grind =] +@[simp] theorem Subst.rewrite4_cons_ren_add_direct {r : Ren T} {ℓ : List Nat} - : Ren.add T ℓ.length ∘ (ℓ ++ r) = r -:= by simp [Ren.compose] + : Ren.add T ℓ.length >> (ℓ ++ r) = r +:= by simp [HAndThen.hAndThen, AndThen.andThen, Ren.compose] -@[simp, grind =] +@[simp] theorem Subst.rewrite4_cons_ren_add_indirect {k} {r : Ren T} {ℓ : List Nat} {h : k = ℓ.length} - : Ren.add T k ∘ (ℓ ++ r) = r -:= by simp [Ren.compose, h] + : Ren.add T k >> (ℓ ++ r) = r +:= by simp [HAndThen.hAndThen, AndThen.andThen, Ren.compose, h] -@[simp, grind =] +@[simp] theorem Subst.rewrite4_append_add_direct {σ : Subst T} {ℓ : List (Action T)} - : Ren.add T ℓ.length ∘ (ℓ ++ σ) = σ -:= by simp [compose_ren_left]; congr + : Ren.add T ℓ.length >> (ℓ ++ σ) = σ +:= by simp [HAndThen.hAndThen, compose_ren_left]; congr -@[simp, grind =] +@[simp] theorem Subst.rewrite4_append_add_indirect {k} {σ : Subst T} {ℓ : List (Action T)} {h : k = ℓ.length} - : Ren.add T k ∘ (ℓ ++ σ) = σ -:= by simp [compose_ren_left, h]; congr + : Ren.add T k >> (ℓ ++ σ) = σ +:= by simp [h] -theorem Subst.compose_ren_left_cons_lift_1 [RenMap T T] [SubstMap T T] {a : Action T} {r : Ren T} {σ : Subst T} - : r.lift ∘ (a :: σ) = a :: (r ∘ σ) +theorem Subst.compose_ren_left_cons_lift_1 [RenMap T [T]] [SubstMap T [T]] {a : Action T} {r : Ren T} {σ : Subst T} + : r.lift >> (a :: σ) = a :: (r >> σ) := by simp; congr 1 @[simp] -theorem Subst.compose_ren_left_cons_lift_k1 [RenMap T T] [SubstMap T T] {k} {a : Action T} {r : Ren T} {σ : Subst T} - : r.lift (k + 1) ∘ (a :: σ) = a :: (r.lift k ∘ σ) +theorem Subst.compose_ren_left_cons_lift_k1 [RenMap T [T]] [SubstMap T [T]] {k} {a : Action T} {r : Ren T} {σ : Subst T} + : r.lift (k + 1) >> (a :: σ) = a :: (r.lift k >> σ) := by rw [Ren.lift_of_succ, compose_ren_left_cons_lift_1] -@[simp, grind =] +@[simp] theorem Subst.compose_ren_left_cons_lift_direct - [RenMap T T] [SubstMap T T] {ℓ : List $ Action T} {r : Ren T} {σ : Subst T} - : r.lift ℓ.length ∘ (ℓ ++ σ) = ℓ ++ (r ∘ σ) + [RenMap T [T]] [SubstMap T [T]] {ℓ : List $ Action T} {r : Ren T} {σ : Subst T} + : r.lift ℓ.length >> (ℓ ++ σ) = ℓ ++ (r >> σ) := by induction ℓ generalizing r <;> simp [-Subst.rewrite_lift_k_ren, *] -@[simp, grind =] +@[simp] theorem Subst.compose_ren_left_cons_lift_indirect - [RenMap T T] [SubstMap T T] {k} {ℓ : List $ Action T} {r : Ren T} {σ : Subst T} {h : k = ℓ.length} - : r.lift k ∘ (ℓ ++ σ) = ℓ ++ (r ∘ σ) + [RenMap T [T]] [SubstMap T [T]] {k} {ℓ : List $ Action T} {r : Ren T} {σ : Subst T} {h : k = ℓ.length} + : r.lift k >> (ℓ ++ σ) = ℓ ++ (r >> σ) := by induction ℓ generalizing r <;> simp [-Subst.rewrite_lift_k_ren, *] -@[simp, grind =] -theorem Subst.compose_ren_right_append [RenMap T T] {ℓ : List $ Action T} {r : Ren T} {σ : Subst T} - : (ℓ ++ σ) ∘ r = ℓ⟨r⟩ ++ σ ∘ r +@[simp] +theorem Subst.compose_ren_right_append [RenMap T [T]] [SubstMap T [T]] {ℓ : List $ Action T} {r : Ren T} {σ : Subst T} + : (ℓ ++ σ) >> r = ℓ⟨r⟩ ++ (σ >> r) := by induction ℓ generalizing σ r <;> simp - case _ hd tl ih => - rw [<-ih]; simp [compose_ren_right, cons]; funext; case _ i => - cases i <;> simp + case _ hd tl ih => rw [<-ih] theorem Subst.compose_ren_right_assoc - [RenMap S S] [SubstMap S S] [SubstMapRenComposeLeft S S] + [RenMap S [S]] [SubstMap S [S]] [SubstMapRenComposeLeft S [S]] {σ τ : Subst S} {r : Ren S} - : (σ ∘ r) ∘ τ = σ ∘ (r ∘ τ) + : (σ >> r) >> τ = σ >> r >> τ := by - simp [compose, compose_ren_left, compose_ren_right]; funext; case _ i => + simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_left, compose_ren_right] + funext; case _ i => generalize zdef : σ.act i = z cases z <;> simp congr theorem Subst.compose_ren_right_assoc2 - [RenMap S S] [SubstMap S S] [SubstMapRenComposeRight S S] + [RenMap S [S]] [SubstMap S [S]] [SubstMapRenComposeRight S [S]] {σ τ : Subst S} {r : Ren S} - : (σ ∘ τ) ∘ r = σ ∘ (τ ∘ r) + : (σ >> τ) >> r = σ >> τ >> r := by - simp [compose, compose_ren_right]; funext; case _ i => + simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_right]; funext; case _ i => generalize zdef : σ.act i = z cases z <;> simp congr --- like rewrite_lift_succ but no [RenMapId S S] -theorem Subst.lift_of_succ [RenMap S S] [RenMapCompose S S] {k} {σ : Subst S} : σ.lift (k + 1) = (σ.lift k).lift := by +-- like rewrite_lift_succ but no [RenMapId S [S]] +theorem Subst.lift_of_succ [RenMap S [S]] [RenMapCompose S [S]] {k} {σ : Subst S} : σ.lift (k + 1) = (σ.lift k).lift := by simp [lift] funext n ; induction n case zero => simp case succ n' _ => - simp - split <;> simp [rmap] - split <;> grind [Ren.add, Ren.succ, Ren.compose] - -theorem Subst.lift_of_succ_rev [RenMap S S] [RenMapCompose S S] {k} {σ : Subst S} : σ.lift (1 + k) = σ.lift.lift k := by - rw [Nat.add_comm, lift_of_succ] - simp [lift] - funext n ; induction n - case zero => simp [eq_comm] - case succ n' _ => - repeat any_goals (simp ; split) - · simp ; omega - · grind [Ren.succ, Ren.add, Ren.compose] - · grind - · split <;> - · simp [Ren.succ, Ren.add, Ren.compose] ; grind + simp; sorry + +theorem Subst.lift_of_succ_rev [RenMap S [S]] [RenMapCompose S [S]] {k} {σ : Subst S} : σ.lift (1 + k) = σ.lift.lift k := by + sorry + -- rw [Nat.add_comm, lift_of_succ] + -- simp [lift] + -- funext n ; induction n + -- case zero => simp [eq_comm] + -- case succ n' _ => + -- repeat any_goals (simp ; split) + -- · simp ; omega + -- · grind [Ren.succ, Ren.add, Ren.compose] + -- · grind + -- · split <;> + -- · simp [Ren.succ, Ren.add, Ren.compose_tuple, Ren.compose] ; grind @[grind =] -theorem Subst.lift_of_add [RenMap S S] [RenMapId S S] [RenMapCompose S S] {a b} {σ : Subst S} : σ.lift (a + b) = (σ.lift a).lift b := by +theorem Subst.lift_of_add [RenMap S [S]] [SubstMap S [S]] [RenMapId S [S]] [RenMapCompose S [S]] {a b} {σ : Subst S} : σ.lift (a + b) = (σ.lift a).lift b := by induction a generalizing σ <;> grind [lift_of_succ_rev] -@[simp] -theorem Subst.ren_to_hcompose [SubstMap S T] {r : Ren S} {σ : Subst T} : r.to ◾ σ = r.to := by simp [hcompose, Ren.to] +-- @[simp] +-- theorem Subst.ren_to_hcompose [SubstMap S V] {r : Ren S} {σ : Subst T} : r.to ◾ σ = r.to := by simp [hcompose, Ren.to] -@[simp] -theorem Subst.ren_to_hcompose_ren [RenMap S T] {r : Ren S} {k : Ren T} : r.to ◾ k = r.to := by simp [hcompose_ren, Ren.to] +-- @[simp] +-- theorem Subst.ren_to_hcompose_ren [RenMap S T] {r : Ren S} {k : Ren T} : r.to ◾ k = r.to := by simp [hcompose_ren, Ren.to] @[simp] theorem Subst.to_append {ℓ : List Nat} {r : Ren T} : (ℓ ++ r).to = ℓ ++ r.to := by induction ℓ <;> simp_all [HAppend.hAppend, Ren.append, append_ren] -@[simp, grind =] -theorem Subst.ren_rewrite1 [RenMap T T] {r : Ren T} : id T ∘ r = r.to := by simp [Ren.to, compose_ren_right] +@[simp] +theorem Subst.ren_rewrite1 [RenMap T [T]] {r : Ren T} : id T >> r = r.to := by + simp [Ren.to, HAndThen.hAndThen, compose_ren_right] @[simp, grind =] -theorem Subst.ren_rewrite1_left {r : Ren T} : r ∘ id T = r.to := by simp [Ren.to, compose_ren_left] +theorem Subst.ren_rewrite1_left {r : Ren T} : r >> id T = r.to := by + simp [Ren.to, HAndThen.hAndThen, compose_ren_left] -- Not used but maybe useful -theorem Subst.rmap_of_succ_smap - [RenMap T T] [RenMapId T T] - [SubstMap T T] [SubstMapCompose T T] [SubstMapRenComposeLeft T T] - {x : Action T} {τ : Subst T} {t : T} - : t⟨Ren.succ T⟩[x :: τ] = t[τ] := by simp +-- theorem Subst.rmap_of_succ_smap +-- [RenMap T [T]] [RenMapId T [T]] +-- [SubstMap T [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] +-- {x : Action T} {τ : Subst T} {t : T} +-- : t⟨Ren.succ T⟩[x :: τ] = t[τ] := by simp [compose_ren_left_tuple] theorem Subst.compose_compose_left_succ - [RenMap T T] [RenMapId T T] - [SubstMap T T] [SubstMapCompose T T] [SubstMapRenComposeLeft T T] + [RenMap T [T]] [RenMapId T [T]] + [SubstMap T [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] {x : Action T} {σ τ : Subst T} - : (σ ∘ Ren.succ T) ∘ (x :: τ) = σ ∘ τ := by - simp [compose, smap] + : (σ >> Ren.succ T) >> (x :: τ) = σ >> τ := by + simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_right, smap] congr ; funext n generalize zdef : σ.act n = z - induction z <;> simp + induction z <;> simp [HAndThen.hAndThen, SubstVec.compose_ren_left, compose_ren_left]; congr theorem Subst.compose_left_cons_lift1_indirect - [RenMap T T] [RenMapId T T] - [SubstMap T T] [SubstMapCompose T T] [SubstMapRenComposeLeft T T] + [RenMap T [T]] [RenMapId T [T]] + [SubstMap T [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] {x : Action T} {σ τ : Subst T} - : σ.lift ∘ (x :: τ) = x :: (σ ∘ τ) := by - rw [rewrite_lift, rewrite3_cons, Action.smap_re, cons_action0] + : σ.lift >> (x :: τ) = x :: (σ >> τ) := by + rw [rewrite_lift, rewrite3_cons] congr 1 exact compose_compose_left_succ theorem Subst.compose_left_cons_lift_indirect {k} - [RenMap T T] [RenMapId T T] [RenMapCompose T T] - [SubstMap T T] [SubstMapCompose T T] [SubstMapRenComposeLeft T T] + [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] + [SubstMap T [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] {ℓ : List $ Action T} {σ τ : Subst T} {h : k = ℓ.length} - : σ.lift k ∘ (ℓ ++ τ) = ℓ ++ (σ ∘ τ) := by + : σ.lift k >> (ℓ ++ τ) = ℓ ++ (σ >> τ) := by induction ℓ generalizing k <;> simp [*] case cons x xs ih => rw [lift_of_succ, compose_left_cons_lift1_indirect, ← @ih xs.length rfl] theorem Subst.compose_lift_append_indirect {k} - [RenMap S S] [RenMapId S S] [RenMapCompose S S] - [SubstMap S S] [SubstMapId S S] [SubstMapRenComposeLeft S S] [SubstMapCompose S S] + [RenMap S [S]] [RenMapId S [S]] [RenMapCompose S [S]] + [SubstMap S [S]] [SubstMapId S [S]] [SubstMapRenComposeLeft S [S]] [SubstMapCompose S [S]] {ℓ1 ℓ2 : List (Action S)} (h : k = ℓ2.length) - : (ℓ1 ++ Subst.id S).lift k ∘ (ℓ2 ++ Subst.id S) = (ℓ2 ++ ℓ1) ++ Subst.id S := by grind [compose_left_cons_lift_indirect] + : (ℓ1 ++ Subst.id S).lift k >> (ℓ2 ++ Subst.id S) = (ℓ2 ++ ℓ1) ++ Subst.id S +:= by + sorry + -- grind [compose_left_cons_lift_indirect] @[simp] -theorem Subst.List.smap_append [SubstMap S T] {a b : List S} {σ : Subst T} - : (a ++ b)[σ] = a[σ] ++ b[σ] := by induction a <;> grind +theorem Subst.List.smap_append [SubstMap S V] {a b : List S} {σ : SubstVec V} + : (a ++ b)[σ,] = a[σ,] ++ b[σ,] := by induction a <;> grind @[simp] -theorem Subst.List.rmap_reverse [RenMap S T] {ℓ : List S} {r : Ren T} : ℓ.reverse⟨r⟩ = ℓ⟨r⟩.reverse := by +theorem Subst.List.rmap_reverse [RenMap S V] {ℓ : List S} {r : RenVec V} : ℓ.reverse⟨r,⟩ = ℓ⟨r,⟩.reverse := by induction ℓ <;> simp ; grind @[simp] -theorem Subst.List.smap_reverse [SubstMap S T] {ℓ : List S} {σ : Subst T} : ℓ.reverse[σ] = ℓ[σ].reverse := by +theorem Subst.List.smap_reverse [SubstMap S V] {ℓ : List S} {σ : SubstVec V} : ℓ.reverse[σ,] = ℓ[σ,].reverse := by induction ℓ <;> simp ; grind @[simp] -theorem Subst.List.rmap_map_su [RenMap T T] {ℓ : List T} {r : Ren T} : (List.map su ℓ)⟨r⟩ = List.map su ℓ⟨r⟩ := by +theorem Subst.List.rmap_map_su [RenMap T [T]] {ℓ : List T} {r : Ren T} : (List.map su ℓ)⟨r⟩ = List.map su ℓ⟨r⟩ := by induction ℓ <;> simp ; grind @[simp] -theorem Subst.List.smap_map_su [SubstMap T T] {ℓ : List T} {σ : Subst T} : (List.map su ℓ)[σ] = List.map su ℓ[σ] := by +theorem Subst.List.smap_map_su [SubstMap T [T]] {ℓ : List T} {σ : Subst T} : (List.map su ℓ)[σ] = List.map su ℓ[σ] := by induction ℓ <;> simp ; grind macro "subst_solve_id" : tactic => `(tactic| { intro t; induction t - any_goals solve | simp +instances [*] + any_goals solve | simp_all +instances all_goals try simp at *; simp +instances [*]; grind }) diff --git a/LeanSubst/Ops.lean b/LeanSubst/Ops.lean index 5fd689b..fedc9e2 100644 --- a/LeanSubst/Ops.lean +++ b/LeanSubst/Ops.lean @@ -4,117 +4,208 @@ import LeanSubst.Basic namespace LeanSubst universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} {U : Type u3} +variable {S : Type u1} {T T1 T2 : Type u2} {U : Type u3} +variable {V : List (Type u2)} +---------------------------------------------------------------------------------------------------- +---- RenMapAll & SubstMapAll +---------------------------------------------------------------------------------------------------- +set_option synthInstance.checkSynthOrder false in +instance [i : RenMapAll (T::V)] : RenMap T [T] where + rmap := (i.rmap 0).rmap + +set_option synthInstance.checkSynthOrder false in +instance [i : RenMapAll (T::V)] : RenMapAll V where + rmap := λ k => (i.rmap k.succ) + +instance [i : RenMap T [T]] : RenMapAll [T] where + rmap := λ 0 => i + +instance [i1 : RenMap T1 [T1]] [i2 : RenMap T2 [T2]] : RenMapAll [T1, T2] where + rmap := by + intro i; cases i using Fin.cases with + | zero => exact i1 + | succ i => + cases i using Fin.cases with + | zero => exact i2 + | succ i => apply Fin.elim0 i + +set_option synthInstance.checkSynthOrder false in +instance [i : SubstMapAll (T::V)] : SubstMap T [T] where + smap := (i.smap 0).smap + +set_option synthInstance.checkSynthOrder false in +instance [i : SubstMapAll (T::V)] : SubstMapAll V where + smap := λ k => (i.smap k.succ) + +instance [i : SubstMap T [T]] : SubstMapAll [T] where + smap := λ 0 => i + +instance [i1 : SubstMap T1 [T1]] [i2 : SubstMap T2 [T2]] : SubstMapAll [T1, T2] where + smap := by + intro i; cases i using Fin.cases with + | zero => exact i1 + | succ i => + cases i using Fin.cases with + | zero => exact i2 + | succ i => apply Fin.elim0 i + +---------------------------------------------------------------------------------------------------- +---- Var +---------------------------------------------------------------------------------------------------- +-- @[simp] +-- def Var.rmap1 [RenMap S [S]] (r : Ren S) (x : Var S) : Var S := r.act x + +-- instance (priority := high) [RenMap S [S]] : RenMap (Var S) [S] where +-- rmap := Var.rmap1 + +-- @[simp] +-- def Var.rmap0 [RenMap S V] (_ : V) (x : Var S) : Var S := x + +-- instance (priority := low) [RenMap S V] : RenMap (Var S) V where +-- rmap := Var.rmap0 + +-- @[simp] +-- def Var.smap [i : SubstMap S V] (σ : V) (x : Var S) : Action S := +-- match i.self with +-- | some ⟨k, e⟩ => (Tuple.get σ k |> cast e).act x +-- | none => re x + +-- @[simp] +-- def Var.smap1 [SubstMap S [S]] (σ : Subst S) (x : Var S) : Action S := smap (σ::#⟨⟩) x ---------------------------------------------------------------------------------------------------- ---- Action ---------------------------------------------------------------------------------------------------- @[simp] -def Action.rmap [RenMap S T] (r : Ren T) : Action S -> Action S +theorem Subst.act_inner {f : Nat -> Action T} {x} : Subst.act { inner := f } x = f x := by + simp [act, SubstAction.act] + +@[simp] +def Action.rmap1 [RenMap S [S]] (r : Ren S) : Action S -> Action S | re x => re $ r.act x | su t => su t⟨r⟩ -instance (priority := high) [RenMap T T] : RenMap (Action T) T where - rmap := Action.rmap +instance (priority := high) [RenMap S [S]] : RenMap (Action S) [S] where + rmap v := Action.rmap1 v.1 @[simp] -theorem Action.rmap_re [RenMap T T] {r : Ren T} {x : Nat} : (@re T x)⟨r⟩ = re (r.act x) := by +theorem Action.rmap1_re [RenMap S [S]] {r : Ren S} {x : Var S} : (@re S x)⟨r⟩ = re (r.act x) := by simp [RenMap.rmap] @[simp] -theorem Action.rmap_su [RenMap T T] {r : Ren T} {t : T} : (su t)⟨r⟩ = su t⟨r⟩ := by +theorem Action.rmap1_su [RenMap S [S]] {r : Ren S} {t : S} : (su t)⟨r⟩ = su t⟨r⟩ := by simp [RenMap.rmap] @[simp] -def Action.hrmap [RenMap S T] (r : Ren T) : Action S -> Action S +def Action.rmap0 [RenMap S V] (r : RenVec V) : Action S -> Action S | re x => re x -| su t => su t⟨r⟩ +| su t => su t⟨r,⟩ -instance [RenMap S T] : RenMap (Action S) T where - rmap := Action.hrmap +instance (priority := low) [RenMap S V] : RenMap (Action S) V where + rmap := Action.rmap0 @[simp] -theorem Action.hrmap_re [RenMap S T] {r : Ren T} {x : Nat} : (@re S x)⟨r⟩ = re x := by +theorem Action.rmap0_re [RenMap S V] {r : RenVec V} {x : Var S} : (@re S x)⟨r,⟩ = re x := by simp [RenMap.rmap] @[simp] -theorem Action.hrmap_su [RenMap S T] {r : Ren T} {t : S} : (su t)⟨r⟩ = su t⟨r⟩ := by +theorem Action.rmap0_su [RenMap S V] {r : RenVec V} {t : S} : (su t)⟨r,⟩ = su t⟨r,⟩ := by simp [RenMap.rmap] @[simp] -def Action.smap [SubstMap T T] (σ : Subst T) : Action T -> Action T +def Action.smap1 [SubstMap T [T]] (σ : Subst T) : Action T -> Action T | re x => σ.act x | su t => su t[σ] -instance (priority := high) [SubstMap T T] : SubstMap (Action T) T where - smap := Action.smap +instance (priority := high) [SubstMap T [T]] : SubstMap (Action T) [T] where + smap v := Action.smap1 v.1 @[simp] -theorem Action.smap_re [SubstMap T T] {σ : Subst T} {x : Nat} : (@re T x)[σ] = σ.act x := by - simp [SubstMap.smap] +theorem Action.smap1_re [SubstMap T [T]] {σ : Subst T} {x : Nat} : (@re T x)[σ] = σ.act x := by + simp [SubstMap.smap, Subst.act, SubstAction.act] @[simp] -theorem Action.smap_su [SubstMap T T] {σ : Subst T} {t : T} : (su t)[σ] = su t[σ] := by +theorem Action.smap1_su [SubstMap T [T]] {σ : Subst T} {t : T} : (su t)[σ] = su t[σ] := by simp [SubstMap.smap] @[simp] -def Action.hsmap [SubstMap S T] (σ : Subst T) : Action S -> Action S +def Action.smap0 [SubstMap S V] (σ : SubstVec V) : Action S -> Action S | re x => re x -| su t => su t[σ] +| su t => su t[σ,] -instance [SubstMap S T] : SubstMap (Action S) T where - smap := Action.hsmap +instance (priority := low) [SubstMap S V] : SubstMap (Action S) V where + smap := Action.smap0 @[simp] -theorem Action.hsmap_re [SubstMap S T] {σ : Subst T} {x : Nat} : (@re S x)[σ] = re x := by +theorem Action.smap0_re [SubstMap S V] {σ : SubstVec V} {x : Var S} : (@re S x)[σ,] = re x := by simp [SubstMap.smap] @[simp] -theorem Action.hsmap_su [SubstMap S T] {σ : Subst T} {t : S} : (su t)[σ] = su t[σ] := by +theorem Action.smap0_su [SubstMap S V] {σ : SubstVec V} {t : S} : (su t)[σ,] = su t[σ,] := by simp [SubstMap.smap] +---------------------------------------------------------------------------------------------------- +---- Subst +---------------------------------------------------------------------------------------------------- +def Subst.rmap [RenMap S V] (r : RenVec V) (σ : Subst S) : Subst S := .mk λ n => (σ.act n)⟨r,⟩ -@[simp] -theorem Subst.act_inner {f : Nat -> Action T} {x} : Subst.act { inner := f } x = f x := by - simp [act, SubstAction.act] +instance [RenMap S V] : RenMap (Subst S) V where + rmap := Subst.rmap + +def Subst.smap [SubstMap S V] (τ : SubstVec V) (σ : Subst S) : Subst S := .mk λ n => (σ.act n)[τ,] + +instance [SubstMap S V] : SubstMap (Subst S) V where + smap := Subst.smap ---------------------------------------------------------------------------------------------------- ---- Identity ---------------------------------------------------------------------------------------------------- def Ren.id T : Ren T := ⟨λ x => x⟩ -notation "+0r" => Ren.id _ +notation "𝐫0" => Ren.id _ +notation "𝐫0(" T ")" => Ren.id T @[simp] -theorem Ren.id_action {x} : (id T).act x = x := by simp [id] +theorem Ren.id_action {x} : 𝐫0(T).act x = x := by simp [id] + +@[simp] +def Ren.ids : (V : List (Type u2)) -> RenVec V +| [] => .unit +| .cons x xs => (id x, ids xs) def Subst.id T : Subst T := ⟨λ x => re x⟩ -notation "+0σ" => Subst.id _ +notation "𝐬0" => Subst.id _ +notation "𝐬0(" T ")" => Subst.id T + +@[simp] +theorem Subst.id_action {x} : 𝐬0(T).act x = re x := by simp [id, act, SubstAction.act] @[simp] -theorem Subst.id_action {x} : (id T).act x = re x := by simp [id, act, SubstAction.act] +def Subst.ids : (V : List (Type u2)) -> SubstVec V +| [] => .unit +| .cons x xs => (id x, ids xs) ---------------------------------------------------------------------------------------------------- ---- Successor ---------------------------------------------------------------------------------------------------- def Ren.succ T : Ren T := ⟨(· + 1)⟩ -notation "+1r" => Ren.succ _ +notation "𝐫1" => Ren.succ _ +notation "𝐫1(" T ")" => Ren.succ T @[simp] -theorem Ren.succ_action {x} : (succ T).act x = x + 1 := by simp [succ] +theorem Ren.succ_action {x} : 𝐫1(T).act x = x + 1 := by simp [succ] def Subst.succ T : Subst T := ⟨λ x => re $ x + 1⟩ -notation "+1σ" => Subst.succ _ +notation "𝐬1" => Subst.succ _ +notation "𝐬1(" T ")" => Subst.succ T @[simp] -theorem Subst.succ_action {x} : (succ T).act x = re (x + 1) := by simp [succ, act, SubstAction.act] +theorem Subst.succ_action {x} : 𝐬1(T).act x = re (x + 1) := by simp [succ, act, SubstAction.act] ---------------------------------------------------------------------------------------------------- ---- Predecessor ---------------------------------------------------------------------------------------------------- def Ren.pred T : Ren T := ⟨(· - 1)⟩ -notation "-1r" => Ren.pred _ @[simp] theorem Ren.pred_action {x} : (pred T).act x = x - 1 := by simp [pred] def Subst.pred T : Subst T := ⟨λ x => re $ x - 1⟩ -notation "-1σ" => Subst.pred _ @[simp] theorem Subst.pred_action {x} : (pred T).act x = re (x - 1) := by simp [pred, act, SubstAction.act] @@ -122,55 +213,51 @@ theorem Subst.pred_action {x} : (pred T).act x = re (x - 1) := by simp [pred, ac ---- Addition ---------------------------------------------------------------------------------------------------- def Ren.add T (k : Nat) : Ren T := ⟨(· + k)⟩ -notation "+r" => Ren.add _ @[simp] theorem Ren.add_action {k x} : (add T k).act x = x + k := by simp [Ren.add] @[simp] -theorem Ren.add_zero : add T 0 = +0r := by simp [Ren.add, Ren.id] +theorem Ren.add_zero : add T 0 = 𝐫0 := by simp [Ren.add, Ren.id] @[simp] -theorem Ren.add_one : add T 1 = +1r := by simp [Ren.add, Ren.succ] +theorem Ren.add_one : add T 1 = 𝐫1 := by simp [Ren.add, Ren.succ] def Subst.add T (k : Nat) : Subst T := ⟨λ x => re $ x + k⟩ -notation "+σ" => Subst.add _ @[simp] theorem Subst.add_action {k x} : (add T k).act x = re (x + k) := by simp [add, act, SubstAction.act] @[simp] -theorem Subst.add_zero : add T 0 = +0σ := by simp [add, id] +theorem Subst.add_zero : add T 0 = 𝐬0 := by simp [add, id] @[simp] -theorem Subst.add_one : add T 1 = +1σ := by simp [add, succ] +theorem Subst.add_one : add T 1 = 𝐬1 := by simp [add, succ] ---------------------------------------------------------------------------------------------------- ---- Subtraction ---------------------------------------------------------------------------------------------------- def Ren.sub T (k : Nat) : Ren T := ⟨(· - k)⟩ -notation "-r" => Ren.sub _ @[simp] theorem Ren.sub_action {k x} : (sub T k).act x = x - k := by simp [sub] @[simp] -theorem Ren.sub_zero : sub T 0 = +0r := by simp [sub, id] +theorem Ren.sub_zero : sub T 0 = 𝐫0 := by simp [sub, id] @[simp] -theorem Ren.sub_one : sub T 1 = -1r := by simp [sub, pred] +theorem Ren.sub_one : sub T 1 = pred _ := by simp [sub, pred] def Subst.sub T (k : Nat) : Subst T := ⟨λ x => re $ x - k⟩ -notation "-σ" => Subst.sub _ @[simp] theorem Subst.sub_action {k x} : (@sub T k).act x = re (x - k) := by simp [sub, act, SubstAction.act] @[simp] -theorem Subst.sub_zero : sub T 0 = +0σ := by simp [sub, id] +theorem Subst.sub_zero : sub T 0 = 𝐬0 := by simp [sub, id] @[simp] -theorem Subst.sub_one : sub T 1 = -1σ := by simp [sub, pred] +theorem Subst.sub_one : sub T 1 = pred _ := by simp [sub, pred] ---------------------------------------------------------------------------------------------------- ---- Cons @@ -303,101 +390,153 @@ theorem Subst.append_ren_action_ge {σ : Subst T} {i} ---------------------------------------------------------------------------------------------------- def Ren.compose : Ren T -> Ren T -> Ren T | r1, r2 => .mk λ n => r2.act (r1.act n) -infixr:85 " ∘ " => Ren.compose + +instance : AndThen (Ren T) where + andThen r f := Ren.compose r (f ()) + +def RenVec.compose : {V : List (Type u2)} -> RenVec V -> RenVec V -> RenVec V +| [], _, _ => .unit +| .cons _ _, (v1, v1s), (v2, v2s) => (v1 >> v2, compose v1s v2s) + +instance : AndThen (RenVec V) where + andThen r f := RenVec.compose r (f ()) @[simp] -theorem Ren.compose_action {r1 r2 : Ren T} {x} : (r1 ∘ r2).act x = r2.act (r1.act x) := by - simp [compose] +theorem Ren.compose_action {r1 r2 : Ren T} {x} : (r1 >> r2).act x = r2.act (r1.act x) := by + simp [HAndThen.hAndThen, AndThen.andThen, compose] @[simp] -theorem Ren.compose_id_left {r : Ren T} : +0r ∘ r = r := by simp [compose, id] +theorem Ren.compose_id_left {r : Ren T} : 𝐫0 >> r = r := by + simp [HAndThen.hAndThen, AndThen.andThen, compose, id] @[simp] -theorem Ren.compose_id_right {r : Ren T} : r ∘ +0r = r := by simp [compose, id] +theorem Ren.compose_id_right {r : Ren T} : r >> 𝐫0 = r := by + simp [HAndThen.hAndThen, AndThen.andThen, compose, id] @[simp] -theorem Ren.compose_assoc {r1 r2 r3 : Ren T} : (r1 ∘ r2) ∘ r3 = r1 ∘ r2 ∘ r3 := by simp [compose] +theorem Ren.compose_assoc {r1 r2 r3 : Ren T} : (r1 >> r2) >> r3 = r1 >> r2 >> r3 := by + simp [HAndThen.hAndThen, AndThen.andThen, compose] @[simp] -theorem Ren.compose_pred_succ : +1r ∘ -1r = id T := by simp [succ, pred, id, compose] +theorem Ren.compose_pred_succ : 𝐫1 >> pred T = id T := by + simp [HAndThen.hAndThen, AndThen.andThen, succ, pred, id, compose] @[simp] -theorem Ren.compose_sub_add {k} : +r k ∘ -r k = id T := by simp [sub, add, id, compose] +theorem Ren.compose_sub_add {k} : add T k >> sub T k = id T := by + simp [HAndThen.hAndThen, AndThen.andThen, sub, add, id, compose] @[grind =] -theorem Ren.compose_add_succ_right {k} : add T (k + 1) = +r k ∘ +1r := by - simp [add, succ, compose]; grind +theorem Ren.compose_add_succ_right {k} : add T (k + 1) = add T k >> 𝐫1 := by + simp [HAndThen.hAndThen, AndThen.andThen, add, succ, compose]; grind @[grind =] -theorem Ren.compose_add_succ_left {k} : add T (k + 1) = +1r ∘ +r k := by - simp [add, succ, compose]; grind +theorem Ren.compose_add_succ_left {k} : add T (k + 1) = 𝐫1 >> add T k := by + simp [HAndThen.hAndThen, AndThen.andThen, add, succ, compose]; grind -def Subst.compose [SubstMap T T] : Subst T -> Subst T -> Subst T +def Subst.compose [SubstMap T [T]] : Subst T -> Subst T -> Subst T | σ, τ => .mk λ n => (σ.act n)[τ] -infixr:85 (name := Subst.compose_notation) " ∘ " => Subst.compose + +instance [SubstMap T [T]] : AndThen (Subst T) where + andThen σ f := Subst.compose σ (f ()) + +def SubstVec.compose + : {V : List (Type u2)} -> [SubstMapAll V] -> + SubstVec V -> SubstVec V -> SubstVec V +| [], _, _, _ => .unit +| .cons _ _, _, (v1, v1s), (v2, v2s) => (v1 >> v2, compose v1s v2s) + +instance [SubstMapAll V] : AndThen (SubstVec V) where + andThen σ f := SubstVec.compose σ (f ()) @[simp] -theorem Subst.compose_action [SubstMap T T] {σ τ : Subst T} {x : Nat} - : (σ ∘ τ).act x = (σ.act x)[τ] -:= by simp [compose, act, SubstAction.act] +theorem Subst.compose_action [SubstMap T [T]] {σ τ : Subst T} {x : Var T} + : (σ >> τ).act x = (σ.act x)[τ] +:= by simp [HAndThen.hAndThen, AndThen.andThen, compose, act, SubstAction.act] @[simp] -theorem Subst.compose_pred_succ [SubstMap T T] : succ T ∘ pred T = id T := by - simp [succ, pred, id, compose, act, SubstAction.act] +theorem Subst.compose_pred_succ [SubstMap T [T]] : succ T >> pred T = id T := by + simp [HAndThen.hAndThen, AndThen.andThen, succ, pred, id, compose, act, SubstAction.act] @[simp] -theorem Subst.compose_sub_add [SubstMap T T] {k} : add T k ∘ sub T k = id T := by - simp [sub, add, id, compose, act, SubstAction.act] +theorem Subst.compose_sub_add [SubstMap T [T]] {k} : add T k >> sub T k = id T := by + simp [HAndThen.hAndThen, AndThen.andThen, sub, add, id, compose, act, SubstAction.act] @[grind =] -theorem Subst.compose_add_succ_right [SubstMap T T] {k} : add T (k + 1) = add T k ∘ succ T := by - simp [add, succ, compose, act, SubstAction.act]; grind +theorem Subst.compose_add_succ_right [SubstMap T [T]] {k} : add T (k + 1) = add T k >> succ T := by + simp [HAndThen.hAndThen, AndThen.andThen, add, succ, compose, act, SubstAction.act]; grind @[grind =] -theorem Subst.compose_add_succ_left [SubstMap T T] {k} : add T (k + 1) = succ T ∘ add T k := by - simp [add, succ, compose, act, SubstAction.act]; grind +theorem Subst.compose_add_succ_left [SubstMap T [T]] {k} : add T (k + 1) = succ T >> add T k := by + simp [HAndThen.hAndThen, AndThen.andThen, add, succ, compose, act, SubstAction.act]; grind 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 + +instance : HAndThen (Ren T) (Subst T) (Subst T) where + hAndThen r f := Subst.compose_ren_left r (f ()) + +def SubstVec.compose_ren_left + : {V : List (Type u2)} -> RenVec V -> SubstVec V -> SubstVec V +| [], _, _ => .unit +| .cons _ _, (v1, v1s), (v2, v2s) => (v1 >> v2, compose_ren_left v1s v2s) + +instance : HAndThen (RenVec V) (SubstVec V) (SubstVec V) where + hAndThen r f := SubstVec.compose_ren_left r (f ()) @[simp] theorem Subst.compose_ren_left_action {r : Ren T} {τ : Subst T} {x} - : (r ∘ τ).act x = τ.act (r.act x) -:= by simp [compose_ren_left, act, SubstAction.act] + : (r >> τ).act x = τ.act (r.act x) +:= by simp [HAndThen.hAndThen, compose_ren_left, act, SubstAction.act] -def Subst.compose_ren_right [RenMap T T] : Subst T -> Ren T -> Subst T +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_ren_right_action [RenMap T T] {σ : Subst T} {r : Ren T} {x : Nat} - : (σ ∘ r).act x = (σ.act x)⟨r⟩ -:= by simp [compose_ren_right, act, SubstAction.act] +instance [RenMap T [T]] : HAndThen (Subst T) (Ren T) (Subst T) where + hAndThen σ f := Subst.compose_ren_right σ (f ()) -def Subst.hcompose [SubstMap S T] : Subst S -> Subst T -> Subst S -| σ, τ => .mk λ n => (σ.act n)[τ] -infixr:85 " ◾ " => Subst.hcompose +def SubstVec.compose_ren_right + : {V : List (Type u2)} -> [RenMapAll V] -> + SubstVec V -> RenVec V -> SubstVec V +| [], _, _, _ => .unit +| .cons _ _, _, (v1, v1s), (v2, v2s) => (v1 >> v2, compose_ren_right v1s v2s) + +instance [RenMapAll V] : HAndThen (SubstVec V) (RenVec V) (SubstVec V) where + hAndThen σ f := SubstVec.compose_ren_right σ (f ()) @[simp] -theorem Subst.hcompose_action [SubstMap S T] {σ : Subst S} {τ : Subst T} {x : Nat} - : (σ ◾ τ).act x = (σ.act x)[τ] -:= by simp [hcompose, act, SubstAction.act] +theorem Subst.compose_ren_right_action [RenMap T [T]] {σ : Subst T} {r : Ren T} {x : Nat} + : (σ >> r).act x = (σ.act x)⟨r⟩ +:= by simp [HAndThen.hAndThen, compose_ren_right, act, SubstAction.act] -def Subst.hcompose_ren [RenMap S T] : Subst S -> Ren T -> Subst S -| σ, r => .mk λ n => (σ.act n)⟨r⟩ -infixr:85 " ◾ " => Subst.hcompose_ren +-- def Subst.hcompose [SubstMap S T] : Subst S -> Subst T -> Subst S +-- | σ, τ => .mk λ n => (σ.act n)[τ] +-- infixr:85 " ◾ " => Subst.hcompose -@[simp] -theorem Subst.hcompose_ren_action [RenMap S T] {σ : Subst S} {r : Ren T} {x : Nat} - : (σ ◾ r).act x = (σ.act x)⟨r⟩ -:= by simp [hcompose_ren, act, SubstAction.act] +-- @[simp] +-- theorem Subst.hcompose_action [SubstMap S T] {σ : Subst S} {τ : Subst T} {x : Nat} +-- : (σ ◾ τ).act x = (σ.act x)[τ] +-- := by simp [hcompose, act, SubstAction.act] + +-- 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.hcompose_ren_action [RenMap S T] {σ : Subst S} {r : Ren T} {x : Nat} +-- : (σ ◾ r).act x = (σ.act x)⟨r⟩ +-- := by simp [hcompose_ren, act, SubstAction.act] +-- ---------------------------------------------------------------------------------------------------- ---- Lift ---------------------------------------------------------------------------------------------------- def Ren.lift (r : Ren T) (k : Nat := 1) : Ren T := .mk λ n => if n < k then n else r.act (n - k) + k +def RenVec.lift : {V : List (Type u2)} -> RenVec V -> List Nat -> RenVec V +| [], _, _ => .unit +| .cons _ _, (t, ts), [] => (t, ts) +| .cons _ _, (t, ts), (.cons k ks) => (t.lift k, ts.lift ks) + @[simp, grind <-] theorem Ren.lift_action_lt {r : Ren T} {k i} (h : i < k) : (lift r k).act i = i := by simp [lift]; grind @@ -421,15 +560,15 @@ theorem Ren.lift_of_succ {r : Ren T} {k} : r.lift (k + 1) = (r.lift k).lift := b @[simp] theorem Ren.lift_id {k} : lift (id T) k = id T := by simp [id, lift]; congr; funext; case _ x => - cases x <;> simp; omega + cases x <;> simp; grind -theorem Ren.lift_compose1 {r1 r2 : Ren T} : (r1 ∘ r2).lift = r1.lift ∘ r2.lift := by - simp [compose, lift] +theorem Ren.lift_compose1 {r1 r2 : Ren T} : (r1 >> r2).lift = r1.lift >> r2.lift := by + simp [HAndThen.hAndThen, AndThen.andThen, compose, lift] funext; case _ x => cases x <;> simp @[simp] -theorem Ren.lift_compose {k} {r1 r2 : Ren T} : (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] @@ -437,17 +576,21 @@ theorem Ren.lift_compose {k} {r1 r2 : Ren T} : (r1 ∘ r2).lift k = r1.lift k rw [lift_of_succ (r := r2)] 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⟩ +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))⟨Ren.add T k⟩ + +def SubstVec.lift : {V : List (Type u2)} -> [RenMapAll V] -> (σ : SubstVec V) -> (k : Nat := 1) -> SubstVec V +| [], _, _, _ => .unit +| .cons _ _, _, (t, ts), k => (t.lift k, ts.lift k) @[simp, grind <-] -theorem Subst.lift_action_lt [RenMap T T] {σ : Subst T} {k i} (h : i < k) +theorem Subst.lift_action_lt [RenMap T [T]] {σ : Subst T} {k i} (h : i < k) : (lift σ k).act i = re i := by simp [lift, act, SubstAction.act]; 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⟩ +theorem Subst.lift_action_ge [RenMap T [T]] {σ : Subst T} {k i} (h : i ≥ k) + : (lift σ k).act i = (σ.act (i - k))⟨Ren.add T k⟩ := by simp [lift, act, SubstAction.act]; grind ---------------------------------------------------------------------------------------------------- ---- Action on variable list @@ -495,18 +638,21 @@ theorem Ren.to_add {k} : (add T k).to = .add T k := by simp [to, add, Subst.add] 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 +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, Subst.act, SubstAction.act]; 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 +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, Subst.act, SubstAction.act] + simp [to, HAndThen.hAndThen, AndThen.andThen, compose, Subst.compose, Subst.act, SubstAction.act] + +def RenVec.to : {V : List (Type u2)} -> (r : RenVec V) -> SubstVec V +| [], _ => .unit +| .cons _ _, (r, rs) => (r.to, rs.to) ---------------------------------------------------------------------------------------------------- ---- Range ---------------------------------------------------------------------------------------------------- diff --git a/LeanSubst/Rewriting/Normal.lean b/LeanSubst/Rewriting/Normal.lean index 596a13b..ad98306 100644 --- a/LeanSubst/Rewriting/Normal.lean +++ b/LeanSubst/Rewriting/Normal.lean @@ -3,121 +3,121 @@ import Init.WF import LeanSubst.Laws import LeanSubst.Rewriting.Reduction -namespace LeanSubst - universe u - - section - variable {T : Type} - - def Reducible (R : T -> T -> Prop) (t : T) := ∃ t', R t t' - def Normal (R : T -> T -> Prop) (t : T) := ¬ (Reducible R t) - def NormalForm (R : T -> T -> Prop) (t : T) (t' : T) := Star R t t' ∧ Normal R t' - def WN (R : T -> T -> Prop) (t : T) := ∃ t', NormalForm R t t' - - inductive SN (R : T -> T -> Prop) : T -> Prop where - | sn {x} : (∀ y, R x y -> SN R y) -> SN R x - - inductive SNPlus (R : T -> T -> Prop) : T -> Prop where - | sn {x} : (∀ y, Plus R x y -> SNPlus R y) -> SNPlus R x - - variable {R R1 R2 : T -> T -> Prop} - - namespace SNPlus - theorem impies_sn {t} : SNPlus R t -> SN R t := by - intro h; induction h; case _ t' _ ih => - constructor; intro t'' r - apply ih t'' (Plus.start r) - - theorem preservation_step {t t'} : SNPlus R t -> R t t' -> SNPlus R t' := by - intro h r; induction h; case _ z h _ => - apply h _ (Plus.start r) - - theorem preservation {t t'} : SNPlus R t -> Star R t t' -> SNPlus R t' := by - intro h r; induction r - case _ => apply h - case _ _ r2 ih => - apply preservation_step ih r2 - end SNPlus - - namespace SN - theorem preimage (f : T -> T) x : - (∀ x y, R x y -> R (f x) (f y)) -> - SN R (f x) -> - SN R x - := by - intro h sh - generalize zdef : f x = z at sh - induction sh generalizing f x - case _ x' h' ih => - subst zdef; constructor - intro y r - apply ih (f y) (h _ _ r) f y h rfl - - theorem preservation_step {t t'} : SN R t -> R t t' -> SN R t' := by - intro h red - induction h - case _ z h1 _h2 => - apply h1 _ red - - theorem preservation {t t'} : SN R t -> Star R t t' -> SN R t' := by - intro h red - induction red - case _ => simp [*] - case _ _ r2 ih => apply preservation_step ih r2 - - theorem star {t} : (∀ y, Star R t y -> SN R y) -> SN R t := by - intro h - constructor - intro y r - apply h y (Star.step Star.refl r) - - theorem implies_snplus {t} : SN R t -> SNPlus R t := by - intro h; induction h; case _ t' _ ih => - constructor; intro t'' r - have lem := Plus.destruct r - cases lem; case _ z lem => - have lem2 := ih z lem.1 - apply SNPlus.preservation lem2 lem.2 - - theorem expansion_step {t t' : T} (f : FunctionalTerm R t) : SN R t' -> R t t' -> SN R t := by - intro h r - apply SN.sn; intro y r' - rw [<-f r r'] - apply h - - theorem expansion {t t' : T} [Functional R] : SN R t' -> Star R t t' -> SN R t := by - intro h r - induction r; apply h - case _ r1 r2 ih => - have lem := expansion_step Functional.functional h r2 - apply ih lem - - theorem equiv_acc {t} : SN R t <-> Acc (flip $ R) t := by - apply Iff.intro - case _ => - intro h; induction h - case _ x h ih => - constructor - simp [flip] - exact ih - case _ => - intro h; induction h - case _ x h ih => - constructor - simp [flip] at ih - exact ih - - theorem wellfounded : (∀ t, SN R t) -> WellFounded (flip $ R) := by - intro h; constructor - intro a; replace h := h a - apply equiv_acc.1 h - - 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 - intro x y r; apply Substitutive.subst - apply r - end SN - end -end LeanSubst +-- namespace LeanSubst +-- universe u + +-- section +-- variable {T : Type} + +-- def Reducible (R : T -> T -> Prop) (t : T) := ∃ t', R t t' +-- def Normal (R : T -> T -> Prop) (t : T) := ¬ (Reducible R t) +-- def NormalForm (R : T -> T -> Prop) (t : T) (t' : T) := Star R t t' ∧ Normal R t' +-- def WN (R : T -> T -> Prop) (t : T) := ∃ t', NormalForm R t t' + +-- inductive SN (R : T -> T -> Prop) : T -> Prop where +-- | sn {x} : (∀ y, R x y -> SN R y) -> SN R x + +-- inductive SNPlus (R : T -> T -> Prop) : T -> Prop where +-- | sn {x} : (∀ y, Plus R x y -> SNPlus R y) -> SNPlus R x + +-- variable {R R1 R2 : T -> T -> Prop} + +-- namespace SNPlus +-- theorem impies_sn {t} : SNPlus R t -> SN R t := by +-- intro h; induction h; case _ t' _ ih => +-- constructor; intro t'' r +-- apply ih t'' (Plus.start r) + +-- theorem preservation_step {t t'} : SNPlus R t -> R t t' -> SNPlus R t' := by +-- intro h r; induction h; case _ z h _ => +-- apply h _ (Plus.start r) + +-- theorem preservation {t t'} : SNPlus R t -> Star R t t' -> SNPlus R t' := by +-- intro h r; induction r +-- case _ => apply h +-- case _ _ r2 ih => +-- apply preservation_step ih r2 +-- end SNPlus + +-- namespace SN +-- theorem preimage (f : T -> T) x : +-- (∀ x y, R x y -> R (f x) (f y)) -> +-- SN R (f x) -> +-- SN R x +-- := by +-- intro h sh +-- generalize zdef : f x = z at sh +-- induction sh generalizing f x +-- case _ x' h' ih => +-- subst zdef; constructor +-- intro y r +-- apply ih (f y) (h _ _ r) f y h rfl + +-- theorem preservation_step {t t'} : SN R t -> R t t' -> SN R t' := by +-- intro h red +-- induction h +-- case _ z h1 _h2 => +-- apply h1 _ red + +-- theorem preservation {t t'} : SN R t -> Star R t t' -> SN R t' := by +-- intro h red +-- induction red +-- case _ => simp [*] +-- case _ _ r2 ih => apply preservation_step ih r2 + +-- theorem star {t} : (∀ y, Star R t y -> SN R y) -> SN R t := by +-- intro h +-- constructor +-- intro y r +-- apply h y (Star.step Star.refl r) + +-- theorem implies_snplus {t} : SN R t -> SNPlus R t := by +-- intro h; induction h; case _ t' _ ih => +-- constructor; intro t'' r +-- have lem := Plus.destruct r +-- cases lem; case _ z lem => +-- have lem2 := ih z lem.1 +-- apply SNPlus.preservation lem2 lem.2 + +-- theorem expansion_step {t t' : T} (f : FunctionalTerm R t) : SN R t' -> R t t' -> SN R t := by +-- intro h r +-- apply SN.sn; intro y r' +-- rw [<-f r r'] +-- apply h + +-- theorem expansion {t t' : T} [Functional R] : SN R t' -> Star R t t' -> SN R t := by +-- intro h r +-- induction r; apply h +-- case _ r1 r2 ih => +-- have lem := expansion_step Functional.functional h r2 +-- apply ih lem + +-- theorem equiv_acc {t} : SN R t <-> Acc (flip $ R) t := by +-- apply Iff.intro +-- case _ => +-- intro h; induction h +-- case _ x h ih => +-- constructor +-- simp [flip] +-- exact ih +-- case _ => +-- intro h; induction h +-- case _ x h ih => +-- constructor +-- simp [flip] at ih +-- exact ih + +-- theorem wellfounded : (∀ t, SN R t) -> WellFounded (flip $ R) := by +-- intro h; constructor +-- intro a; replace h := h a +-- apply equiv_acc.1 h + +-- 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 +-- intro x y r; apply Substitutive.subst +-- apply r +-- end SN +-- end +-- end LeanSubst diff --git a/LeanSubst/Rewriting/Reduction.lean b/LeanSubst/Rewriting/Reduction.lean index 927c24a..fd0ff94 100644 --- a/LeanSubst/Rewriting/Reduction.lean +++ b/LeanSubst/Rewriting/Reduction.lean @@ -1,329 +1,329 @@ import LeanSubst.Laws -namespace LeanSubst - universe u - - 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 - complete : T -> T - triangle {t s} : R t s -> R s (complete t) - - section - variable {T : Type} - - 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) - - inductive Star (R : T -> T -> Prop) : T -> T -> Prop where - | refl {t} : Star R t t - | step {x y z} : Star R x y -> R y z -> Star R x z - - inductive Plus (R : T -> T -> Prop) : T -> T -> Prop where - | start {t s} : R t s -> Plus R t s - | step {x y z} : Plus R x y -> R y z -> Plus R x z - - inductive Conv (R : T -> T -> Prop) : T -> T -> Prop where - | refl {x} : Conv R x x - | forward {x y z} : Conv R x z -> R x y -> Conv R y z - | backward {x y z} : Conv R y z -> R x y -> Conv R x z - - class HasConfluence (R : T -> T -> Prop) where - confluence {s t1 t2} : Star R s t1 -> Star R s t2 -> ∃ t, Star R t1 t ∧ Star R t2 t - - variable {R R1 R2 : T -> T -> Prop} - - namespace Star - theorem trans {x y z} : Star R x y -> Star R y z -> Star R x z := by - intro r1 r2; induction r2 generalizing x - case _ => apply r1 - case _ a b _ r2 ih => apply Star.step (ih r1) r2 - - theorem promote {x y} (Rprm : ∀ {x y}, R1 x y -> R2 x y) : - Star R1 x y -> Star R2 x y - := by - intro r; induction r - case _ => constructor - case _ _ r ih => constructor; apply ih; apply Rprm r - - theorem stepr {x y z} : R x y -> Star R y z -> Star R x z := by - intro h r; induction r generalizing x - case _ => apply Star.step Star.refl h - case _ r1 r2 ih => - replace ih := ih h - apply Star.step ih r2 - - theorem destruct {x z} : Star R x z -> (∃ y, R x y ∧ Star R y z) ∨ x = z := by - intro h; induction h - case _ => apply Or.inr rfl - case _ u v r1 r2 ih => - cases ih - case _ ih => - cases ih; case _ w ih => - apply Or.inl; apply Exists.intro w - apply And.intro ih.1 - apply Star.step ih.2 r2 - case _ ih => - subst ih; apply Or.inl - apply Exists.intro v; apply And.intro r2 Star.refl - - theorem congr3_1 {t1 t1'} t2 t3 (f : T -> T -> T -> T) : - (∀ {t1 t2 t3 t1'}, R t1 t1' -> R (f t1 t2 t3) (f t1' t2 t3)) -> - Star R t1 t1' -> - Star R (f t1 t2 t3) (f t1' t2 t3) - := by - intro fh h2 - induction h2 - case _ => apply refl - case _ h4 ih => - have h5 := @fh _ t2 t3 _ h4 - apply trans ih (Star.step Star.refl h5) - - theorem congr3_2 {t2 t2'} t1 t3 (f : T -> T -> T -> T) : - (∀ {t1 t2 t3 t2'}, R t2 t2' -> R (f t1 t2 t3) (f t1 t2' t3)) -> - Star R t2 t2' -> - Star R (f t1 t2 t3) (f t1 t2' t3) - := by - intro fh h2 - induction h2 - case _ => apply refl - case _ h4 ih => - have h5 := @fh t1 _ t3 _ h4 - apply trans ih (Star.step Star.refl h5) - - theorem congr3_3 {t3 t3'} t1 t2 (f : T -> T -> T -> T) : - (∀ {t1 t2 t3 t3'}, R t3 t3' -> R (f t1 t2 t3) (f t1 t2 t3')) -> - Star R t3 t3' -> - Star R (f t1 t2 t3) (f t1 t2 t3') - := by - intro fh h2 - induction h2 - case _ => apply refl - case _ h4 ih => - have h5 := @fh t1 t2 _ _ h4 - apply trans ih (Star.step Star.refl h5) - - theorem congr3 {t1 t1' t2 t2' t3 t3'} (f : T -> T -> T -> T) : - (∀ {t1 t2 t3 t1'}, R t1 t1' -> R (f t1 t2 t3) (f t1' t2 t3)) -> - (∀ {t1 t2 t3 t2'}, R t2 t2' -> R (f t1 t2 t3) (f t1 t2' t3)) -> - (∀ {t1 t2 t3 t3'}, R t3 t3' -> R (f t1 t2 t3) (f t1 t2 t3')) -> - Star R t1 t1' -> Star R t2 t2' -> Star R t3 t3' -> - Star R (f t1 t2 t3) (f t1' t2' t3') - := by - intro f1 f2 f3 h1 h2 h3 - have r1 := congr3_1 t2 t3 f f1 h1 - have r2 := congr3_2 t1' t3 f f2 h2 - have r3 := congr3_3 t1' t2' f f3 h3 - apply trans r1; apply trans r2; apply trans r3; apply refl - - theorem congr2_1 {t1 t1'} t2 (f : T -> T -> T) : - (∀ {t1 t2 t1'}, R t1 t1' -> R (f t1 t2) (f t1' t2)) -> - Star R t1 t1' -> - Star R (f t1 t2) (f t1' t2) - := by - intro fh h - apply congr3_1 t2 t2 (λ t1 t2 _t3 => f t1 t2) - intro t1 t2 _t3 t1' h; apply fh h - exact h - - theorem congr2_2 {t2 t2'} t1 (f : T -> T -> T) : - (∀ {t1 t2 t2'}, R t2 t2' -> R (f t1 t2) (f t1 t2')) -> - Star R t2 t2' -> - Star R (f t1 t2) (f t1 t2') - := by - intro fh h - apply congr3_2 t1 t1 (λ t1 t2 _t3 => f t1 t2) - intro t1 t2 _t3 t1' h; apply fh h - exact h - - theorem congr2 {t1 t1' t2 t2'} (f : T -> T -> T) : - (∀ {t1 t2 t1'}, R t1 t1' -> R (f t1 t2) (f t1' t2)) -> - (∀ {t1 t2 t2'}, R t2 t2' -> R (f t1 t2) (f t1 t2')) -> - Star R t1 t1' -> Star R t2 t2' -> - Star R (f t1 t2) (f t1' t2') - := by - intro f1 f2 h1 h2 - have r1 := congr2_1 t2 f f1 h1 - have r2 := congr2_2 t1' f f2 h2 - apply trans r1; apply trans r2; apply refl - - theorem congr1 {t1 t1'} (f : T -> T) : - (∀ {t1 t1'}, R t1 t1' -> R (f t1) (f t1')) -> - Star R t1 t1' -> - Star R (f t1) (f t1') - := by - intro fh h - apply congr2_1 t1 (λ t1 _t2 => f t1) - intro t1 _t2 t1' h; apply fh h - exact h - - variable [HasTriangle R] - - theorem strip {s t1 t2} : R s t1 -> Star R s t2 -> ∃ t, Star R t1 t ∧ R t2 t := by - intro h1 h2 - induction h2 generalizing t1 - case _ t' => exists t1; apply And.intro; apply Star.refl; apply h1 - case _ x y z _r1 r2 ih => - replace ih := ih h1 - cases ih - case _ w ih => - replace r2 := HasTriangle.triangle r2 - have lem := HasTriangle.triangle ih.2 - replace lem := Star.step ih.1 lem - exists (HasTriangle.complete R y) - - theorem confluence {s t1 t2} : Star R s t1 -> Star R s t2 -> ∃ t, Star R t1 t ∧ Star R t2 t := by - intro h1 h2 - induction h1 generalizing t2 - case _ z => - exists t2; apply And.intro - apply h2; apply Star.refl - case _ s y t1 _r1 r2 ih => - replace ih := ih h2 - cases ih; case _ w ih => - have lem := strip r2 ih.1 - cases lem; case _ q lem => - exists q; apply And.intro - apply lem.1; apply Star.step ih.2 lem.2 - - 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 - intro r; induction r - case _ => apply Star.refl - case _ r1 r2 ih => - replace r2 := Substitutive.subst σ r2 - apply Star.step ih r2 - end Star - - instance HasConfluence_from_HasTriangle {T : Type} {R : T -> T -> Prop} [HasTriangle R] : HasConfluence R where - confluence := Star.confluence - - namespace Plus - theorem destruct {x z} : Plus R x z -> ∃ y, R x y ∧ Star R y z := by - intro r; induction r - case _ b r => - exists b; apply And.intro r Star.refl - case _ r1 r2 ih => - cases ih; case _ u ih => - exists u; apply And.intro ih.1 - apply Star.step ih.2 r2 - - theorem stepr {x y z} : R x y -> Plus R y z -> Plus R x z := by - intro r1 r2 - induction r2 generalizing x - case _ r2 => apply Plus.step (Plus.start r1) r2 - case _ r3 r4 ih => apply Plus.step (ih r1) r4 - - theorem stepr_from_star {x y z} : R x y -> Star R y z -> Plus R x z := by - intro r1 r2 - induction r2 generalizing x - case _ => apply Plus.start; apply r1 - case _ r3 r4 ih => apply Plus.step (ih r1) r4 - end Plus - - namespace Conv - theorem forward_right {x y z} : Conv R x y -> R y z -> Conv R x z := by - intro h r; induction h generalizing z - case _ => apply backward refl r - case _ r2 ih => apply forward (ih r) r2 - case _ r2 ih => apply backward (ih r) r2 - - theorem backward_right {x y z} : Conv R x y -> R z y -> Conv R x z := by - intro h r; induction h generalizing z - case _ => apply forward refl r - case _ r2 ih => apply forward (ih r) r2 - case _ r2 ih => apply backward (ih r) r2 - - theorem sym {x y} : Conv R x y -> Conv R y x := by - intro h; induction h - case _ => constructor - case _ r ih => apply forward_right ih r - case _ r ih => apply backward_right ih r - - theorem star_forward {x y z} : Conv R x z -> Star R x y -> Conv R y z := by - intro cv r - induction r; simp [*] - case _ r1 r2 ih => apply forward ih r2 - - theorem star_backward {x y z} : Conv R y z -> Star R x y -> Conv R x z := by - intro cv r - induction r; simp [*] - case _ r1 r2 ih => - apply ih - apply backward cv r2 - - theorem star_forward_right {x y z} : Conv R x y -> Star R y z -> Conv R x z := by - intro cv r - induction r; simp [*] - case _ r1 r2 ih => apply forward_right ih r2 - - theorem star_backward_right {x y z} : Conv R x y -> Star R z y -> Conv R x z := by - intro cv r - induction r; simp [*] - case _ r1 r2 ih => - apply ih - apply backward_right cv r2 - - theorem star_equiv {x y} [HasConfluence R] : Conv R x y <-> (∃ t, Star R x t ∧ Star R y t) := by - apply Iff.intro - case _ => - intro cv - induction cv - case _ t => - exists t - apply And.intro Star.refl Star.refl - case _ a b c cv r ih => - cases ih; case _ t ih => - have lem := HasConfluence.confluence (Star.step Star.refl r) ih.1 - cases lem; case _ z lem => - have lem2 := Star.trans ih.2 lem.2 - exists z; apply And.intro lem.1 lem2 - case _ a b c cv r ih => - cases ih; case _ t ih => - have lem := Star.stepr r ih.1 - exists t; simp [*] - case _ => - intro h - cases h; case _ t h => - apply star_backward _ h.1 - apply star_backward_right _ h.2 - apply refl - - theorem trans {x y z} [HasConfluence R] : Conv R x y -> Conv R y z -> Conv R x z := by - intro h1 h2 - replace h1 := star_equiv.1 h1 - replace h2 := star_equiv.1 h2 - cases h1; case _ t1 h1 => - cases h2; case _ t2 h2 => - have lem := HasConfluence.confluence h1.2 h2.1 - cases lem; case _ w lem => - replace h1 := Star.trans h1.1 lem.1 - replace h2 := Star.trans h2.2 lem.2 - apply star_backward _ h1 - apply star_backward_right _ h2 - apply refl - - -- theorem subst {x y} [SubstMap T] [Substitutive R] σ : Conv R x y -> Conv R (x[σ]) (y[σ]) := by - -- intro cv - - -- sorry - end Conv - end - - section - variable {T : Type u} (R : T -> T -> Prop) {t t' : T} - - @[simp] - def FunctionalTerm (t : T) := - ∀ {x y}, R t x -> R t y -> x = y - - class Functional where - functional : ∀ {t}, FunctionalTerm R t - end - -end LeanSubst +-- namespace LeanSubst +-- universe u + +-- 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 +-- complete : T -> T +-- triangle {t s} : R t s -> R s (complete t) + +-- section +-- variable {T : Type} + +-- 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) + +-- inductive Star (R : T -> T -> Prop) : T -> T -> Prop where +-- | refl {t} : Star R t t +-- | step {x y z} : Star R x y -> R y z -> Star R x z + +-- inductive Plus (R : T -> T -> Prop) : T -> T -> Prop where +-- | start {t s} : R t s -> Plus R t s +-- | step {x y z} : Plus R x y -> R y z -> Plus R x z + +-- inductive Conv (R : T -> T -> Prop) : T -> T -> Prop where +-- | refl {x} : Conv R x x +-- | forward {x y z} : Conv R x z -> R x y -> Conv R y z +-- | backward {x y z} : Conv R y z -> R x y -> Conv R x z + +-- class HasConfluence (R : T -> T -> Prop) where +-- confluence {s t1 t2} : Star R s t1 -> Star R s t2 -> ∃ t, Star R t1 t ∧ Star R t2 t + +-- variable {R R1 R2 : T -> T -> Prop} + +-- namespace Star +-- theorem trans {x y z} : Star R x y -> Star R y z -> Star R x z := by +-- intro r1 r2; induction r2 generalizing x +-- case _ => apply r1 +-- case _ a b _ r2 ih => apply Star.step (ih r1) r2 + +-- theorem promote {x y} (Rprm : ∀ {x y}, R1 x y -> R2 x y) : +-- Star R1 x y -> Star R2 x y +-- := by +-- intro r; induction r +-- case _ => constructor +-- case _ _ r ih => constructor; apply ih; apply Rprm r + +-- theorem stepr {x y z} : R x y -> Star R y z -> Star R x z := by +-- intro h r; induction r generalizing x +-- case _ => apply Star.step Star.refl h +-- case _ r1 r2 ih => +-- replace ih := ih h +-- apply Star.step ih r2 + +-- theorem destruct {x z} : Star R x z -> (∃ y, R x y ∧ Star R y z) ∨ x = z := by +-- intro h; induction h +-- case _ => apply Or.inr rfl +-- case _ u v r1 r2 ih => +-- cases ih +-- case _ ih => +-- cases ih; case _ w ih => +-- apply Or.inl; apply Exists.intro w +-- apply And.intro ih.1 +-- apply Star.step ih.2 r2 +-- case _ ih => +-- subst ih; apply Or.inl +-- apply Exists.intro v; apply And.intro r2 Star.refl + +-- theorem congr3_1 {t1 t1'} t2 t3 (f : T -> T -> T -> T) : +-- (∀ {t1 t2 t3 t1'}, R t1 t1' -> R (f t1 t2 t3) (f t1' t2 t3)) -> +-- Star R t1 t1' -> +-- Star R (f t1 t2 t3) (f t1' t2 t3) +-- := by +-- intro fh h2 +-- induction h2 +-- case _ => apply refl +-- case _ h4 ih => +-- have h5 := @fh _ t2 t3 _ h4 +-- apply trans ih (Star.step Star.refl h5) + +-- theorem congr3_2 {t2 t2'} t1 t3 (f : T -> T -> T -> T) : +-- (∀ {t1 t2 t3 t2'}, R t2 t2' -> R (f t1 t2 t3) (f t1 t2' t3)) -> +-- Star R t2 t2' -> +-- Star R (f t1 t2 t3) (f t1 t2' t3) +-- := by +-- intro fh h2 +-- induction h2 +-- case _ => apply refl +-- case _ h4 ih => +-- have h5 := @fh t1 _ t3 _ h4 +-- apply trans ih (Star.step Star.refl h5) + +-- theorem congr3_3 {t3 t3'} t1 t2 (f : T -> T -> T -> T) : +-- (∀ {t1 t2 t3 t3'}, R t3 t3' -> R (f t1 t2 t3) (f t1 t2 t3')) -> +-- Star R t3 t3' -> +-- Star R (f t1 t2 t3) (f t1 t2 t3') +-- := by +-- intro fh h2 +-- induction h2 +-- case _ => apply refl +-- case _ h4 ih => +-- have h5 := @fh t1 t2 _ _ h4 +-- apply trans ih (Star.step Star.refl h5) + +-- theorem congr3 {t1 t1' t2 t2' t3 t3'} (f : T -> T -> T -> T) : +-- (∀ {t1 t2 t3 t1'}, R t1 t1' -> R (f t1 t2 t3) (f t1' t2 t3)) -> +-- (∀ {t1 t2 t3 t2'}, R t2 t2' -> R (f t1 t2 t3) (f t1 t2' t3)) -> +-- (∀ {t1 t2 t3 t3'}, R t3 t3' -> R (f t1 t2 t3) (f t1 t2 t3')) -> +-- Star R t1 t1' -> Star R t2 t2' -> Star R t3 t3' -> +-- Star R (f t1 t2 t3) (f t1' t2' t3') +-- := by +-- intro f1 f2 f3 h1 h2 h3 +-- have r1 := congr3_1 t2 t3 f f1 h1 +-- have r2 := congr3_2 t1' t3 f f2 h2 +-- have r3 := congr3_3 t1' t2' f f3 h3 +-- apply trans r1; apply trans r2; apply trans r3; apply refl + +-- theorem congr2_1 {t1 t1'} t2 (f : T -> T -> T) : +-- (∀ {t1 t2 t1'}, R t1 t1' -> R (f t1 t2) (f t1' t2)) -> +-- Star R t1 t1' -> +-- Star R (f t1 t2) (f t1' t2) +-- := by +-- intro fh h +-- apply congr3_1 t2 t2 (λ t1 t2 _t3 => f t1 t2) +-- intro t1 t2 _t3 t1' h; apply fh h +-- exact h + +-- theorem congr2_2 {t2 t2'} t1 (f : T -> T -> T) : +-- (∀ {t1 t2 t2'}, R t2 t2' -> R (f t1 t2) (f t1 t2')) -> +-- Star R t2 t2' -> +-- Star R (f t1 t2) (f t1 t2') +-- := by +-- intro fh h +-- apply congr3_2 t1 t1 (λ t1 t2 _t3 => f t1 t2) +-- intro t1 t2 _t3 t1' h; apply fh h +-- exact h + +-- theorem congr2 {t1 t1' t2 t2'} (f : T -> T -> T) : +-- (∀ {t1 t2 t1'}, R t1 t1' -> R (f t1 t2) (f t1' t2)) -> +-- (∀ {t1 t2 t2'}, R t2 t2' -> R (f t1 t2) (f t1 t2')) -> +-- Star R t1 t1' -> Star R t2 t2' -> +-- Star R (f t1 t2) (f t1' t2') +-- := by +-- intro f1 f2 h1 h2 +-- have r1 := congr2_1 t2 f f1 h1 +-- have r2 := congr2_2 t1' f f2 h2 +-- apply trans r1; apply trans r2; apply refl + +-- theorem congr1 {t1 t1'} (f : T -> T) : +-- (∀ {t1 t1'}, R t1 t1' -> R (f t1) (f t1')) -> +-- Star R t1 t1' -> +-- Star R (f t1) (f t1') +-- := by +-- intro fh h +-- apply congr2_1 t1 (λ t1 _t2 => f t1) +-- intro t1 _t2 t1' h; apply fh h +-- exact h + +-- variable [HasTriangle R] + +-- theorem strip {s t1 t2} : R s t1 -> Star R s t2 -> ∃ t, Star R t1 t ∧ R t2 t := by +-- intro h1 h2 +-- induction h2 generalizing t1 +-- case _ t' => exists t1; apply And.intro; apply Star.refl; apply h1 +-- case _ x y z _r1 r2 ih => +-- replace ih := ih h1 +-- cases ih +-- case _ w ih => +-- replace r2 := HasTriangle.triangle r2 +-- have lem := HasTriangle.triangle ih.2 +-- replace lem := Star.step ih.1 lem +-- exists (HasTriangle.complete R y) + +-- theorem confluence {s t1 t2} : Star R s t1 -> Star R s t2 -> ∃ t, Star R t1 t ∧ Star R t2 t := by +-- intro h1 h2 +-- induction h1 generalizing t2 +-- case _ z => +-- exists t2; apply And.intro +-- apply h2; apply Star.refl +-- case _ s y t1 _r1 r2 ih => +-- replace ih := ih h2 +-- cases ih; case _ w ih => +-- have lem := strip r2 ih.1 +-- cases lem; case _ q lem => +-- exists q; apply And.intro +-- apply lem.1; apply Star.step ih.2 lem.2 + +-- 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 +-- intro r; induction r +-- case _ => apply Star.refl +-- case _ r1 r2 ih => +-- replace r2 := Substitutive.subst σ r2 +-- apply Star.step ih r2 +-- end Star + +-- instance HasConfluence_from_HasTriangle {T : Type} {R : T -> T -> Prop} [HasTriangle R] : HasConfluence R where +-- confluence := Star.confluence + +-- namespace Plus +-- theorem destruct {x z} : Plus R x z -> ∃ y, R x y ∧ Star R y z := by +-- intro r; induction r +-- case _ b r => +-- exists b; apply And.intro r Star.refl +-- case _ r1 r2 ih => +-- cases ih; case _ u ih => +-- exists u; apply And.intro ih.1 +-- apply Star.step ih.2 r2 + +-- theorem stepr {x y z} : R x y -> Plus R y z -> Plus R x z := by +-- intro r1 r2 +-- induction r2 generalizing x +-- case _ r2 => apply Plus.step (Plus.start r1) r2 +-- case _ r3 r4 ih => apply Plus.step (ih r1) r4 + +-- theorem stepr_from_star {x y z} : R x y -> Star R y z -> Plus R x z := by +-- intro r1 r2 +-- induction r2 generalizing x +-- case _ => apply Plus.start; apply r1 +-- case _ r3 r4 ih => apply Plus.step (ih r1) r4 +-- end Plus + +-- namespace Conv +-- theorem forward_right {x y z} : Conv R x y -> R y z -> Conv R x z := by +-- intro h r; induction h generalizing z +-- case _ => apply backward refl r +-- case _ r2 ih => apply forward (ih r) r2 +-- case _ r2 ih => apply backward (ih r) r2 + +-- theorem backward_right {x y z} : Conv R x y -> R z y -> Conv R x z := by +-- intro h r; induction h generalizing z +-- case _ => apply forward refl r +-- case _ r2 ih => apply forward (ih r) r2 +-- case _ r2 ih => apply backward (ih r) r2 + +-- theorem sym {x y} : Conv R x y -> Conv R y x := by +-- intro h; induction h +-- case _ => constructor +-- case _ r ih => apply forward_right ih r +-- case _ r ih => apply backward_right ih r + +-- theorem star_forward {x y z} : Conv R x z -> Star R x y -> Conv R y z := by +-- intro cv r +-- induction r; simp [*] +-- case _ r1 r2 ih => apply forward ih r2 + +-- theorem star_backward {x y z} : Conv R y z -> Star R x y -> Conv R x z := by +-- intro cv r +-- induction r; simp [*] +-- case _ r1 r2 ih => +-- apply ih +-- apply backward cv r2 + +-- theorem star_forward_right {x y z} : Conv R x y -> Star R y z -> Conv R x z := by +-- intro cv r +-- induction r; simp [*] +-- case _ r1 r2 ih => apply forward_right ih r2 + +-- theorem star_backward_right {x y z} : Conv R x y -> Star R z y -> Conv R x z := by +-- intro cv r +-- induction r; simp [*] +-- case _ r1 r2 ih => +-- apply ih +-- apply backward_right cv r2 + +-- theorem star_equiv {x y} [HasConfluence R] : Conv R x y <-> (∃ t, Star R x t ∧ Star R y t) := by +-- apply Iff.intro +-- case _ => +-- intro cv +-- induction cv +-- case _ t => +-- exists t +-- apply And.intro Star.refl Star.refl +-- case _ a b c cv r ih => +-- cases ih; case _ t ih => +-- have lem := HasConfluence.confluence (Star.step Star.refl r) ih.1 +-- cases lem; case _ z lem => +-- have lem2 := Star.trans ih.2 lem.2 +-- exists z; apply And.intro lem.1 lem2 +-- case _ a b c cv r ih => +-- cases ih; case _ t ih => +-- have lem := Star.stepr r ih.1 +-- exists t; simp [*] +-- case _ => +-- intro h +-- cases h; case _ t h => +-- apply star_backward _ h.1 +-- apply star_backward_right _ h.2 +-- apply refl + +-- theorem trans {x y z} [HasConfluence R] : Conv R x y -> Conv R y z -> Conv R x z := by +-- intro h1 h2 +-- replace h1 := star_equiv.1 h1 +-- replace h2 := star_equiv.1 h2 +-- cases h1; case _ t1 h1 => +-- cases h2; case _ t2 h2 => +-- have lem := HasConfluence.confluence h1.2 h2.1 +-- cases lem; case _ w lem => +-- replace h1 := Star.trans h1.1 lem.1 +-- replace h2 := Star.trans h2.2 lem.2 +-- apply star_backward _ h1 +-- apply star_backward_right _ h2 +-- apply refl + +-- -- theorem subst {x y} [SubstMap T] [Substitutive R] σ : Conv R x y -> Conv R (x[σ]) (y[σ]) := by +-- -- intro cv + +-- -- sorry +-- end Conv +-- end + +-- section +-- variable {T : Type u} (R : T -> T -> Prop) {t t' : T} + +-- @[simp] +-- def FunctionalTerm (t : T) := +-- ∀ {x y}, R t x -> R t y -> x = y + +-- class Functional where +-- functional : ∀ {t}, FunctionalTerm R t +-- end + +-- end LeanSubst diff --git a/LeanSubst/Types/List.lean b/LeanSubst/Types/List.lean index 519d7ca..cf747bf 100644 --- a/LeanSubst/Types/List.lean +++ b/LeanSubst/Types/List.lean @@ -4,53 +4,54 @@ import LeanSubst.Class namespace LeanSubst universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} {U : Type u3} +variable {S : Type u1} {T T1 T2 : Type u2} {U : Type u3} +variable {V : List (Type u2)} -def List.rmap [RenMap S T] (r : Ren T) : List S -> List S +def List.rmap [RenMap S V] (r : RenVec V) : List S -> List S | [] => [] -| .cons x xs => x⟨r⟩ :: rmap r xs +| .cons x xs => x⟨r,⟩ :: rmap r xs -instance [RenMap S T] : RenMap (List S) T where +instance [RenMap S V] : RenMap (List S) V where rmap := List.rmap @[simp, grind =] -theorem List.rmap_nil [RenMap S T] {r : Ren T} : (@List.nil S)⟨r⟩ = [] := by +theorem List.rmap_nil [RenMap S V] {r : RenVec V} : (@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 +theorem List.rmap_cons [RenMap S V] {x} {xs : List S} {r : RenVec V} : (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 +instance [RenMap S V] [RenMapId S V] : RenMapId (List S) V where apply_id := by intro t; induction t <;> simp [*] -instance [RenMap S T] [RenMapCompose S T] : RenMapCompose (List S) T where +instance [RenMap S V] [RenMapCompose S V] : RenMapCompose (List S) V where apply_compose := by intro s σ τ; induction s <;> simp [*] @[simp] -theorem List.rmap_append [RenMap S T] {xs ys : List S} {r : Ren T} - : (xs ++ ys)⟨r⟩ = xs⟨r⟩ ++ ys⟨r⟩ +theorem List.rmap_append [RenMap S V] {xs ys : List S} {r : RenVec V} + : (xs ++ ys)⟨r,⟩ = xs⟨r,⟩ ++ ys⟨r,⟩ := by induction xs generalizing ys <;> simp [*] -def List.smap [SubstMap S T] (σ : Subst T) : List S -> List S +def List.smap [SubstMap S V] (σ : SubstVec V) : List S -> List S | [] => [] -| .cons x xs => x[σ] :: smap σ xs +| .cons x xs => x[σ,] :: smap σ xs -instance [SubstMap S T] : SubstMap (List S) T where +instance [SubstMap S V] : SubstMap (List S) V where smap := List.smap @[simp, grind =] -theorem List.smap_none [SubstMap S T] {σ : Subst T} : (@List.nil S)[σ] = [] := by +theorem List.smap_none [SubstMap S V] {σ : SubstVec V} : (@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[σ] +theorem List.smap_some [SubstMap S V] {x} {xs : List S} {σ : SubstVec V} : (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 +instance [RenMap S V] [SubstMap S V] [SubstMapId S V] : SubstMapId (List S) V where apply_id := by intro t; induction t <;> simp [*] -instance [SubstMap T T] [SubstMap S T] [SubstMapCompose S T] : SubstMapCompose (List S) T where +instance [SubstMap S V] [SubstMapAll V] [SubstMapCompose S V] : SubstMapCompose (List S) V where apply_compose := by intro s σ τ; induction s <;> simp [*] end LeanSubst diff --git a/LeanSubst/Types/Nat.lean b/LeanSubst/Types/Nat.lean index 8cecf8c..9d5ff1c 100644 --- a/LeanSubst/Types/Nat.lean +++ b/LeanSubst/Types/Nat.lean @@ -4,13 +4,14 @@ import LeanSubst.Class namespace LeanSubst universe u1 u2 u3 -variable {S : Type u1} {T : Type u2} {U : Type u3} +variable {S : Type u1} {T T1 T2 : Type u2} {U : Type u3} +variable {V : List (Type u2)} def Nat.rmap (r : Ren T) : Nat -> Nat | n => r.act n -instance : RenMap Nat T where - rmap := Nat.rmap +instance : RenMap Nat [T] where + rmap r := Nat.rmap r.1 @[simp, grind =] theorem Nat.rmap_simp {r : Ren T} {n} : n⟨r⟩ = r.act n := by simp [RenMap.rmap, Nat.rmap] diff --git a/LeanSubst/Types/Option.lean b/LeanSubst/Types/Option.lean index ac46d4f..a82a3c7 100644 --- a/LeanSubst/Types/Option.lean +++ b/LeanSubst/Types/Option.lean @@ -1,51 +1,51 @@ -import LeanSubst.Laws +-- 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⟩ +-- 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 +-- 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_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] +-- @[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] [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 +-- 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[σ] +-- 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 +-- 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_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] +-- @[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 [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 +-- 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 diff --git a/lake-manifest.json b/lake-manifest.json index c363277..d8d6c3a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,5 +1,16 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", - "packages": [], + "packages": + [{"url": "https://github.com/amarmaduke/lilac", + "type": "git", + "subDir": null, + "scope": "amarmaduke", + "rev": "8924478f47eaff544494d1b9012e6731b3941d05", + "name": "lilac", + "manifestFile": "lake-manifest.json", + "inputRev": "8924478f47eaff544494d1b9012e6731b3941d05", + "inherited": false, + "configFile": "lakefile.toml"}], "name": "«lean-subst»", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index f91963d..a758dfd 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,6 +4,12 @@ defaultTargets = ["lean-subst"] leanOptions = { autoImplicit = false } +[[require]] +name = "lilac" +scope = "amarmaduke" +git = "https://github.com/amarmaduke/lilac" +rev = "8924478f47eaff544494d1b9012e6731b3941d05" + [[lean_lib]] name = "LeanSubst" diff --git a/lean-toolchain b/lean-toolchain index d324cad..cd7198b 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 \ No newline at end of file +leanprover/lean4:v4.32.2 \ No newline at end of file