From 44b6c8093b28a7cb69d712d52d3ea4cbfb15d5ce Mon Sep 17 00:00:00 2001 From: Sage Binder Date: Fri, 4 Sep 2026 22:49:21 +0100 Subject: [PATCH 1/3] implemented new map/ren but there's a bug --- Examples/SystemFWithNat/Term.lean | 994 +++++++++++++++--------------- Examples/VariadicSTLC/Term.lean | 7 +- LeanSubst/Automation/Basic.lean | 60 +- 3 files changed, 548 insertions(+), 513 deletions(-) diff --git a/Examples/SystemFWithNat/Term.lean b/Examples/SystemFWithNat/Term.lean index 891c22a..cb649f7 100644 --- a/Examples/SystemFWithNat/Term.lean +++ b/Examples/SystemFWithNat/Term.lean @@ -34,6 +34,32 @@ inductive Term where #leansubst generate Ty, Term +-- | tlam t => tlam (t.smap $ σ |> .lift [0, 1] |> .ren Term [Ty] ⟨𝐫1, .nil⟩ 0 rfl) +-- | x0.tlam => fun x => (x.1 (SubstVec.ren Term [Ty] (Ren.add Ty 1, RenVec.nil) 0 ⋯ (SubstVec.lift [0, 1] σ))).tlam +#print Term.smap._f +#print Term.smap_term_tlam + +theorem SystemFWithNat.Term.smap_term_tlam' : ∀ {x0 : Term} {σ : SubstVec [Term]}, x0.tlam[σ,] = x0[σ,].tlam := by + intros + simp only [SubstMap.smap] + simp [-Term.smap_term_tlam] + + + +instance : RenMapVecDef Term Term [Ty] where + apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] + +instance : RenMapId Term [Term, Ty] where + apply_id := by subst_solve_id + +instance : RenMapCompose Term [Term, Ty] where + apply_compose := by subst_solve_compose + +instance : RenMapVecDef Term Term [] where + apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] + + + -- Checking Ty -- #print Ty.from_action #print Ty.from_action_id @@ -229,571 +255,571 @@ inductive Term where #check (inferInstance : SubstMapCompose Term [Ty]) #check (inferInstance : SubstMapCompose Term [Term]) --- ---------------------------------------------------------------------------------------------------- --- -- Ty Renaming & Substitution --- ---------------------------------------------------------------------------------------------------- --- @[coe] --- def Ty.from_action : Action Ty -> Ty --- | re y => var y --- | su t => t +---------------------------------------------------------------------------------------------------- +-- Ty Renaming & Substitution +---------------------------------------------------------------------------------------------------- +@[coe] +def Ty.from_action : Action Ty -> Ty +| re y => var y +| su t => t --- @[simp] --- theorem Ty.from_action_id {n} : from_action (𝐬0.act n) = var n := by --- simp [from_action] +@[simp] +theorem Ty.from_action_id {n} : from_action (𝐬0.act n) = var n := by + simp [from_action] --- @[simp] --- theorem Ty.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by --- simp [from_action] +@[simp] +theorem Ty.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by + simp [from_action] --- @[simp] --- theorem Ty.from_action_re {n} : from_action (re n) = var n := by simp [from_action] +@[simp] +theorem Ty.from_action_re {n} : from_action (re n) = var n := by simp [from_action] --- @[simp] --- theorem Ty.from_action_su {t} : from_action (su t) = t := by simp [from_action] +@[simp] +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 +instance : Coe (Action Ty) Ty where + coe := Ty.from_action --- @[simp] --- def Ty.rmap (r : RenVec [Ty]) : Ty -> Ty --- | var x => var (r.1.act x) --- | nat => nat --- | arrow t1 t2 => arrow (t1.rmap r) (t2.rmap r) --- | all t => all $ t.rmap $ r.lift [1] +@[simp] +def Ty.rmap (r : RenVec [Ty]) : Ty -> Ty +| var x => var (r.1.act x) +| nat => nat +| arrow t1 t2 => arrow (t1.rmap r) (t2.rmap r) +| all t => all $ t.rmap $ r.lift [1] --- instance : RenMap Ty [Ty] where --- rmap := Ty.rmap +instance : RenMap Ty [Ty] where + rmap := Ty.rmap --- @[simp] --- theorem Ty.rmap_fix {r : RenVec [Ty]} {t : Ty} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] +@[simp] +theorem Ty.rmap_fix {r : RenVec [Ty]} {t : Ty} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] --- instance : RenSuffix Ty [] := ⟨⟩ --- instance : RenMap Ty [] where --- rmap _ := id +instance : RenSuffix Ty [] := ⟨⟩ +instance : RenMap Ty [] where + rmap _ := id --- @[reducible, simp] --- instance instRenMapAll_Ty : RenMapAll [Ty] := .cons .nil +@[reducible, simp] +instance instRenMapAll_Ty : RenMapAll [Ty] := .cons .nil --- @[simp] --- theorem Ty.rmap_var {x} {r : RenVec [Ty]} : (var x)⟨r,⟩ = .var (r.1.act x) := by --- simp only [RenMap.rmap]; rw [rmap] +@[simp] +theorem Ty.rmap_var {x} {r : RenVec [Ty]} : (var x)⟨r,⟩ = .var (r.1.act x) := by + simp only [RenMap.rmap]; rw [rmap] --- @[simp] --- theorem Ty.rmap_nat {r : RenVec [Ty]} : (nat)⟨r,⟩ = nat := by --- simp only [RenMap.rmap]; rw [rmap] +@[simp] +theorem Ty.rmap_nat {r : RenVec [Ty]} : (nat)⟨r,⟩ = nat := by + simp only [RenMap.rmap]; rw [rmap] --- @[simp] --- theorem Ty.rmap_arrow {t1 t2 : Ty} {r : RenVec [Ty]} : (arrow t1 t2)⟨r,⟩ = arrow t1⟨r,⟩ t2⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap] +@[simp] +theorem Ty.rmap_arrow {t1 t2 : Ty} {r : RenVec [Ty]} : (arrow t1 t2)⟨r,⟩ = arrow t1⟨r,⟩ t2⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap] --- @[simp] --- theorem Ty.rmap_all {t} {r : RenVec [Ty]} : (all t)⟨r,⟩ = all t⟨r.lift [1],⟩ := by --- simp only [RenMap.rmap]; rw [rmap] +@[simp] +theorem Ty.rmap_all {t} {r : RenVec [Ty]} : (all t)⟨r,⟩ = all t⟨r.lift [1],⟩ := by + simp only [RenMap.rmap]; rw [rmap] --- @[simp] --- theorem Ty.from_action_rmap {t : Action Ty} {r : RenVec [Ty]} --- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ --- := by cases t <;> simp +@[simp] +theorem Ty.from_action_rmap {t : Action Ty} {r : RenVec [Ty]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp --- instance : RenMapEmpty Ty where --- apply_empty := by intro s; simp [RenMap.rmap] +instance : RenMapEmpty Ty where + apply_empty := by intro s; simp [RenMap.rmap] --- instance : RenMapId Ty [Ty] where --- apply_id := by subst_solve_id +instance : RenMapId Ty [Ty] where + apply_id := by subst_solve_id --- instance : RenMapCompose Ty [Ty] where --- apply_compose := by subst_solve_compose +instance : RenMapCompose Ty [Ty] where + apply_compose := by subst_solve_compose --- @[simp] --- def Ty.smap (σ : SubstVec [Ty]) : Ty -> Ty --- | var x => σ.1.act x --- | nat => nat --- | arrow t1 t2 => arrow (t1.smap σ) (t2.smap σ) --- | all t => all $ t.smap $ σ.lift [1] +@[simp] +def Ty.smap (σ : SubstVec [Ty]) : Ty -> Ty +| var x => σ.1.act x +| nat => nat +| arrow t1 t2 => arrow (t1.smap σ) (t2.smap σ) +| all t => all $ t.smap $ σ.lift [1] --- instance : SubstMap Ty [Ty] where --- smap := Ty.smap +instance : SubstMap Ty [Ty] where + smap := Ty.smap --- @[simp] --- theorem Ty.smap_fix {σ : SubstVec [Ty]} {t : Ty} : smap σ t = t[σ,] := by simp [SubstMap.smap] +@[simp] +theorem Ty.smap_fix {σ : SubstVec [Ty]} {t : Ty} : smap σ t = t[σ,] := by simp [SubstMap.smap] --- instance : SubstSuffix Ty [] := ⟨⟩ --- instance : SubstMap Ty [] where --- smap _ := id +instance : SubstSuffix Ty [] := ⟨⟩ +instance : SubstMap Ty [] where + smap _ := id --- @[reducible, simp] --- instance instSubstMapAll_Ty : SubstMapAll [Ty] := .cons .nil +@[reducible, simp] +instance instSubstMapAll_Ty : SubstMapAll [Ty] := .cons .nil --- @[simp] --- theorem Ty.smap_var {x} {σ : SubstVec [Ty]} : (var x)[σ,] = σ.1.act x := by --- simp only [SubstMap.smap]; rw [smap] +@[simp] +theorem Ty.smap_var {x} {σ : SubstVec [Ty]} : (var x)[σ,] = σ.1.act x := by + simp only [SubstMap.smap]; rw [smap] --- @[simp] --- theorem Ty.smap_nat {σ : SubstVec [Ty]} : (nat)[σ,] = nat := by --- simp only [SubstMap.smap]; rw [smap] +@[simp] +theorem Ty.smap_nat {σ : SubstVec [Ty]} : (nat)[σ,] = nat := by + simp only [SubstMap.smap]; rw [smap] --- @[simp] --- theorem Ty.smap_arrow {t1 t2 : Ty} {σ : SubstVec [Ty]} : (arrow t1 t2)[σ,] = arrow t1[σ,] t2[σ,] := by --- simp only [SubstMap.smap]; rw [smap] +@[simp] +theorem Ty.smap_arrow {t1 t2 : Ty} {σ : SubstVec [Ty]} : (arrow t1 t2)[σ,] = arrow t1[σ,] t2[σ,] := by + simp only [SubstMap.smap]; rw [smap] --- @[simp] --- theorem Ty.smap_all {t} {σ : SubstVec [Ty]} : (all t)[σ,] = all t[σ.lift [1],] := by --- simp only [SubstMap.smap]; rw [smap] +@[simp] +theorem Ty.smap_all {t} {σ : SubstVec [Ty]} : (all t)[σ,] = all t[σ.lift [1],] := by + simp only [SubstMap.smap]; rw [smap] --- @[simp] --- theorem Ty.from_action_smap {t : Action Ty} {σ : SubstVec [Ty]} --- : (from_action t)[σ,] = from_action t[σ,] --- := by cases t <;> simp +@[simp] +theorem Ty.from_action_smap {t : Action Ty} {σ : SubstVec [Ty]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp --- instance : SubstMapEmpty Ty where --- apply_empty := by intro s; simp [SubstMap.smap] +instance : SubstMapEmpty Ty where + apply_empty := by intro s; simp [SubstMap.smap] --- instance : SubstMapId Ty [Ty] where --- apply_id := by subst_solve_id +instance : SubstMapId Ty [Ty] where + apply_id := by subst_solve_id --- instance : SubstMapStable Ty [Ty] where --- apply_stable := by subst_solve_stable +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 : 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 : SubstMapRenComposeRight Ty [Ty] where + apply_ren_compose_right := by subst_solve_compose --- instance : SubstMapCompose Ty [Ty] where --- apply_compose := by subst_solve_compose +instance : SubstMapCompose Ty [Ty] where + apply_compose := by subst_solve_compose --- ---------------------------------------------------------------------------------------------------- --- -- Term Renaming & Substitution --- ---------------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------- +-- Term Renaming & Substitution +---------------------------------------------------------------------------------------------------- --- @[coe] --- def Term.from_action : Action Term -> Term --- | re y => var y --- | su t => t +@[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_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_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_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] +@[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 +instance : Coe (Action Term) Term where + coe := Term.from_action --- @[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, 1]) (n.rmap r) +@[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, 1]) (n.rmap r) --- instance : RenMap Term [Term, Ty] where --- rmap := Term.rmap - --- @[simp] --- theorem Term.rmap_fix {r : RenVec [Term, Ty]} {t : Term} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] - --- @[simp] --- theorem Term.rmap_term_ty_var {x} {r : RenVec [Term, Ty]} : (var x)⟨r,⟩ = var (r.1.act x) := rfl +instance : RenMap Term [Term, Ty] where + rmap := Term.rmap + +@[simp] +theorem Term.rmap_fix {r : RenVec [Term, Ty]} {t : Term} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] + +@[simp] +theorem Term.rmap_term_ty_var {x} {r : RenVec [Term, Ty]} : (var x)⟨r,⟩ = var (r.1.act x) := rfl --- @[simp] --- theorem Term.rmap_term_ty_app {t1 t2} {r : RenVec [Term, Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap] +@[simp] +theorem Term.rmap_term_ty_app {t1 t2} {r : RenVec [Term, Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap] --- @[simp] --- theorem Term.rmap_term_ty_lam'' {A t} {r : RenVec [Term, Ty]} --- : (lam A t)⟨r,⟩ = lam A⟨r.2.1⟩ t⟨r.lift [1, 0],⟩ --- := by simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_ty_tapp {t1 t2} {r : RenVec [Term, Ty]} --- : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.2.1⟩ --- := by simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_ty_tlam {t} {r : RenVec [Term, Ty]} : (tlam t)⟨r,⟩ = tlam t⟨r.lift [0, 1],⟩ := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_ty_zero {r : RenVec [Term, Ty]} : zero⟨r,⟩ = zero := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_ty_succ {t} {r : RenVec [Term, Ty]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_ty_nrec {m z s n} {r : RenVec [Term, Ty]} --- : (nrec m z s n)⟨r,⟩ = nrec m⟨r.2.1⟩ z⟨r,⟩ s⟨r.lift [2, 1],⟩ n⟨r,⟩ --- := by simp only [RenMap.rmap]; rw [rmap]; try simp - --- instance : RenSuffix Term [Ty] := ⟨⟩ --- instance : RenMap Term [Ty] where --- rmap r := Term.rmap (Ren.id Term, r.1, .nil) - --- @[simp] --- theorem Term.rmap_ty_var {x} {r : RenVec [Ty]} : (var x)⟨r,⟩ = var x := by --- simp only [RenMap.rmap]; rw [rmap]; try simp +@[simp] +theorem Term.rmap_term_ty_lam'' {A t} {r : RenVec [Term, Ty]} + : (lam A t)⟨r,⟩ = lam A⟨r.2.1⟩ t⟨r.lift [1, 0],⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_ty_tapp {t1 t2} {r : RenVec [Term, Ty]} + : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.2.1⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_ty_tlam {t} {r : RenVec [Term, Ty]} : (tlam t)⟨r,⟩ = tlam t⟨r.lift [0, 1],⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_ty_zero {r : RenVec [Term, Ty]} : zero⟨r,⟩ = zero := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_ty_succ {t} {r : RenVec [Term, Ty]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_ty_nrec {m z s n} {r : RenVec [Term, Ty]} + : (nrec m z s n)⟨r,⟩ = nrec m⟨r.2.1⟩ z⟨r,⟩ s⟨r.lift [2, 1],⟩ n⟨r,⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +instance : RenSuffix Term [Ty] := ⟨⟩ +instance : RenMap Term [Ty] where + rmap r := Term.rmap (Ren.id Term, r.1, .nil) + +@[simp] +theorem Term.rmap_ty_var {x} {r : RenVec [Ty]} : (var x)⟨r,⟩ = var x := by + simp only [RenMap.rmap]; rw [rmap]; try simp --- @[simp] --- theorem Term.rmap_ty_app {t1 t2} {r : RenVec [Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_ty_lam {A t} {r : RenVec [Ty]} --- : (lam A t)⟨r,⟩ = lam A⟨r.1⟩ t⟨r,⟩ --- := by simp only [RenMap.rmap]; rw [rmap]; try simp +@[simp] +theorem Term.rmap_ty_app {t1 t2} {r : RenVec [Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_ty_lam {A t} {r : RenVec [Ty]} + : (lam A t)⟨r,⟩ = lam A⟨r.1⟩ t⟨r,⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp --- @[simp] --- theorem Term.rmap_ty_tapp {t1 t2} {r : RenVec [Ty]} --- : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.1⟩ --- := by simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_ty_tlam {t} {r : RenVec [Ty]} : (tlam t)⟨r,⟩ = tlam t⟨r.lift [1],⟩ := by --- simp only [RenMap.rmap]; rw [rmap]; try simp +@[simp] +theorem Term.rmap_ty_tapp {t1 t2} {r : RenVec [Ty]} + : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.1⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_ty_tlam {t} {r : RenVec [Ty]} : (tlam t)⟨r,⟩ = tlam t⟨r.lift [1],⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp --- @[simp] --- theorem Term.rmap_ty_zero {r : RenVec [Ty]} : zero⟨r,⟩ = zero := by --- simp only [RenMap.rmap]; rw [rmap]; try simp +@[simp] +theorem Term.rmap_ty_zero {r : RenVec [Ty]} : zero⟨r,⟩ = zero := by + simp only [RenMap.rmap]; rw [rmap]; try simp --- @[simp] --- theorem Term.rmap_ty_succ {t} {r : RenVec [Ty]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_ty_nrec {m z s n} {r : RenVec [Ty]} --- : (nrec m z s n)⟨r,⟩ = nrec m⟨r.1⟩ z⟨r,⟩ s⟨r.lift [1],⟩ n⟨r,⟩ --- := by simp only [RenMap.rmap]; rw [rmap]; try simp - --- instance : RenMap Term [Term] where --- rmap r := Term.rmap (r.1, Ren.id Ty, .nil) - --- @[simp] --- theorem Term.rmap_term_var {x} {r : RenVec [Term]} : (var x)⟨r,⟩ = var (r.1.act x) := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_app {t1 t2} {r : RenVec [Term]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_lam' {A t} {r : RenVec [Term]} --- : (lam A t)⟨r,⟩ = lam A t⟨r.lift [1],⟩ --- := by simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_tapp {t1 t2} {r : RenVec [Term]} --- : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2 --- := by simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_tlam {t} {r : RenVec [Term]} : (tlam t)⟨r,⟩ = tlam t⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_zero {r : RenVec [Term]} : zero⟨r,⟩ = zero := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_succ {t} {r : RenVec [Term]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.rmap_term_nrec {m z s n} {r : RenVec [Term]} --- : (nrec m z s n)⟨r,⟩ = nrec m z⟨r,⟩ s⟨r.lift [2],⟩ n⟨r,⟩ --- := by simp only [RenMap.rmap]; rw [rmap]; try simp - --- @[simp] --- theorem Term.from_action_rmap {t : Action Term} {r : RenVec [Term, Ty]} --- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ --- := by cases t <;> simp [from_action] - --- @[simp] --- theorem Term.from_action_rmap0 {t : Action Term} {r : RenVec [Term]} --- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ --- := by cases t <;> simp [from_action] - --- @[simp] --- theorem Term.from_action_rmap1 {t : Action Term} {r : RenVec [Ty]} --- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ --- := by cases t <;> simp [from_action] - --- instance : RenSuffix Term [] := ⟨⟩ --- instance : RenMap Term [] where --- rmap _ := id - --- @[reducible, simp] --- instance instRenMapAll_Term : RenMapAll [Term] := .cons .nil - --- @[reducible, simp] --- instance instRenMapAll_Term_Ty : RenMapAll [Term, Ty] := .cons instRenMapAll_Ty - --- instance : RenMapEmpty Term where --- apply_empty := by intro s; simp [RenMap.rmap] - --- instance : RenMapVecDef Term Term [Ty] where --- apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] - --- instance : RenMapId Term [Term, Ty] where --- apply_id := by subst_solve_id - --- instance : RenMapCompose Term [Term, Ty] where --- apply_compose := by subst_solve_compose - --- instance : RenMapVecDef Term Term [] where --- apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] - --- instance : RenMapId Term [Term] where --- apply_id := by subst_solve_id - --- instance : RenMapCompose Term [Term] where --- apply_compose := by subst_solve_compose - --- 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.smap (σ : SubstVec [Term, Ty]) : Term -> Term --- | var x => σ.1.act x --- | app t1 t2 => app (t1.smap σ) (t2.smap σ) --- | lam A t => lam A[σ.2.1] (t.smap $ σ.lift [1, 0]) --- | tapp t A => tapp (t.smap σ) A[σ.2.1] --- | tlam t => tlam (t.smap $ σ |> .lift [0, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl) --- | zero => zero --- | succ t => succ (t.smap σ) --- | nrec motive z s n => --- nrec motive[σ.2.1] (z.smap σ) (s.smap $ σ |> .lift [2, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl) (n.smap σ) - --- instance : SubstMap Term [Term, Ty] where --- smap := Term.smap - --- @[simp] --- theorem Term.smap_fix {σ : SubstVec [Term, Ty]} {t : Term} : smap σ t = t[σ,] := by --- simp [SubstMap.smap] - --- @[simp] --- theorem Term.smap_term_ty_var {x} {σ : SubstVec [Term, Ty]} : (var x)[σ,] = σ.1.act x := by --- simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_term_ty_app {t1 t2} {σ : SubstVec [Term, Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by --- simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_term_ty_lam {A t} {σ : SubstVec [Term, Ty]} --- : (lam A t)[σ,] = lam A[σ.2.1] t[σ.lift [1, 0],] --- := by simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_term_ty_tapp {t1 t2} {σ : SubstVec [Term, Ty]} --- : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.2.1] --- := by simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_term_ty_tlam {t} {σ : SubstVec [Term, Ty]} --- : (tlam t)[σ,] = tlam t[σ |> .lift [0, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] --- := by simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_term_ty_zero {σ : SubstVec [Term, Ty]} : zero[σ,] = zero := by --- simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_term_ty_succ {t} {σ : SubstVec [Term, Ty]} : (succ t)[σ,] = succ t[σ,] := by --- simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_term_ty_nrec {m z s n} {σ : SubstVec [Term, Ty]} --- : (nrec m z s n)[σ,] = nrec m[σ.2.1] z[σ,] s[σ |> .lift [2, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] n[σ,] --- := by simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.from_action_smap {t : Action Term} {σ : SubstVec [Term, Ty]} --- : (from_action t)[σ,] = from_action t[σ,] --- := by cases t <;> simp [from_action] - --- instance : SubstSuffix Term [Ty] := ⟨⟩ --- @[simp] --- instance : SubstMap Term [Ty] where --- smap σ := Term.smap (Subst.id Term, σ.1, .nil) - --- @[simp] --- theorem Term.smap_ty_var {x} {σ : SubstVec [Ty]} : (var x)[σ,] = var x := by --- simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_ty_app {t1 t2} {σ : SubstVec [Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by --- simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_ty_lam {A t} {σ : SubstVec [Ty]} --- : (lam A t)[σ,] = lam A[σ.1] t[σ,] --- := by simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_ty_tapp {t1 t2} {σ : SubstVec [Ty]} --- : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.1] --- := by simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_ty_tlam {t} {σ : SubstVec [Ty]} --- : (tlam t)[σ,] = tlam t[σ |> .lift [1],] --- := by simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_ty_zero {σ : SubstVec [Ty]} : zero[σ,] = zero := by --- simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_ty_succ {t} {σ : SubstVec [Ty]} : (succ t)[σ,] = succ t[σ,] := by --- simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.smap_ty_nrec {m z s n} {σ : SubstVec [Ty]} --- : (nrec m z s n)[σ,] = nrec m[σ.1] z[σ,] s[σ |> .lift [1],] n[σ,] --- := by simp only [SubstMap.smap]; rw [smap]; try simp - --- @[simp] --- theorem Term.from_action_smap1 {t : Action Term} {σ : SubstVec [Ty]} --- : (from_action t)[σ,] = from_action t[σ,] --- := by cases t <;> simp [from_action] - --- @[simp] --- instance : SubstMap Term [Term] where --- smap σ := Term.smap (σ.1, Subst.id Ty, .nil) +@[simp] +theorem Term.rmap_ty_succ {t} {r : RenVec [Ty]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_ty_nrec {m z s n} {r : RenVec [Ty]} + : (nrec m z s n)⟨r,⟩ = nrec m⟨r.1⟩ z⟨r,⟩ s⟨r.lift [1],⟩ n⟨r,⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +instance : RenMap Term [Term] where + rmap r := Term.rmap (r.1, Ren.id Ty, .nil) + +@[simp] +theorem Term.rmap_term_var {x} {r : RenVec [Term]} : (var x)⟨r,⟩ = var (r.1.act x) := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_app {t1 t2} {r : RenVec [Term]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_lam' {A t} {r : RenVec [Term]} + : (lam A t)⟨r,⟩ = lam A t⟨r.lift [1],⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_tapp {t1 t2} {r : RenVec [Term]} + : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2 +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_tlam {t} {r : RenVec [Term]} : (tlam t)⟨r,⟩ = tlam t⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_zero {r : RenVec [Term]} : zero⟨r,⟩ = zero := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_succ {t} {r : RenVec [Term]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_nrec {m z s n} {r : RenVec [Term]} + : (nrec m z s n)⟨r,⟩ = nrec m z⟨r,⟩ s⟨r.lift [2],⟩ n⟨r,⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.from_action_rmap {t : Action Term} {r : RenVec [Term, Ty]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp [from_action] + +@[simp] +theorem Term.from_action_rmap0 {t : Action Term} {r : RenVec [Term]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp [from_action] + +@[simp] +theorem Term.from_action_rmap1 {t : Action Term} {r : RenVec [Ty]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp [from_action] + +instance : RenSuffix Term [] := ⟨⟩ +instance : RenMap Term [] where + rmap _ := id + +@[reducible, simp] +instance instRenMapAll_Term : RenMapAll [Term] := .cons .nil + +@[reducible, simp] +instance instRenMapAll_Term_Ty : RenMapAll [Term, Ty] := .cons instRenMapAll_Ty + +instance : RenMapEmpty Term where + apply_empty := by intro s; simp [RenMap.rmap] + +instance : RenMapVecDef Term Term [Ty] where + apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] + +instance : RenMapId Term [Term, Ty] where + apply_id := by subst_solve_id + +instance : RenMapCompose Term [Term, Ty] where + apply_compose := by subst_solve_compose + +instance : RenMapVecDef Term Term [] where + apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] + +instance : RenMapId Term [Term] where + apply_id := by subst_solve_id + +instance : RenMapCompose Term [Term] where + apply_compose := by subst_solve_compose + +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.smap' (σ : SubstVec [Term, Ty]) : Term -> Term +| var x => σ.1.act x +| app t1 t2 => app (t1.smap σ) (t2.smap σ) +| lam A t => lam A[σ.2.1] (t.smap $ σ.lift [1, 0]) +| tapp t A => tapp (t.smap σ) A[σ.2.1] +| tlam t => tlam (t.smap $ σ |> .lift [0, 1] |> .ren Term [Ty] ⟨𝐫1, .nil⟩ 0 rfl) +| zero => zero +| succ t => succ (t.smap σ) +| nrec motive z s n => + nrec motive[σ.2.1] (z.smap σ) (s.smap $ σ |> .lift [2, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl) (n.smap σ) + +instance : SubstMap Term [Term, Ty] where + smap := Term.smap + +@[simp] +theorem Term.smap_fix {σ : SubstVec [Term, Ty]} {t : Term} : smap σ t = t[σ,] := by + simp [SubstMap.smap] + +@[simp] +theorem Term.smap_term_ty_var {x} {σ : SubstVec [Term, Ty]} : (var x)[σ,] = σ.1.act x := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_ty_app {t1 t2} {σ : SubstVec [Term, Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_ty_lam {A t} {σ : SubstVec [Term, Ty]} + : (lam A t)[σ,] = lam A[σ.2.1] t[σ.lift [1, 0],] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_ty_tapp {t1 t2} {σ : SubstVec [Term, Ty]} + : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.2.1] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_ty_tlam {t} {σ : SubstVec [Term, Ty]} + : (tlam t)[σ,] = tlam t[σ |> .lift [0, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_ty_zero {σ : SubstVec [Term, Ty]} : zero[σ,] = zero := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_ty_succ {t} {σ : SubstVec [Term, Ty]} : (succ t)[σ,] = succ t[σ,] := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_ty_nrec {m z s n} {σ : SubstVec [Term, Ty]} + : (nrec m z s n)[σ,] = nrec m[σ.2.1] z[σ,] s[σ |> .lift [2, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] n[σ,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.from_action_smap {t : Action Term} {σ : SubstVec [Term, Ty]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp [from_action] + +instance : SubstSuffix Term [Ty] := ⟨⟩ +@[simp] +instance : SubstMap Term [Ty] where + smap σ := Term.smap (Subst.id Term, σ.1, .nil) + +@[simp] +theorem Term.smap_ty_var {x} {σ : SubstVec [Ty]} : (var x)[σ,] = var x := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_ty_app {t1 t2} {σ : SubstVec [Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_ty_lam {A t} {σ : SubstVec [Ty]} + : (lam A t)[σ,] = lam A[σ.1] t[σ,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_ty_tapp {t1 t2} {σ : SubstVec [Ty]} + : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.1] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_ty_tlam {t} {σ : SubstVec [Ty]} + : (tlam t)[σ,] = tlam t[σ |> .lift [1],] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_ty_zero {σ : SubstVec [Ty]} : zero[σ,] = zero := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_ty_succ {t} {σ : SubstVec [Ty]} : (succ t)[σ,] = succ t[σ,] := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_ty_nrec {m z s n} {σ : SubstVec [Ty]} + : (nrec m z s n)[σ,] = nrec m[σ.1] z[σ,] s[σ |> .lift [1],] n[σ,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.from_action_smap1 {t : Action Term} {σ : SubstVec [Ty]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp [from_action] + +@[simp] +instance : SubstMap Term [Term] where + smap σ := Term.smap (σ.1, Subst.id Ty, .nil) --- @[simp] --- theorem Term.smap_term_var {x} {σ : SubstVec [Term]} : (var x)[σ,] = σ.1.act x := by --- simp only [SubstMap.smap]; rw [smap]; try simp +@[simp] +theorem Term.smap_term_var {x} {σ : SubstVec [Term]} : (var x)[σ,] = σ.1.act x := by + simp only [SubstMap.smap]; rw [smap]; try simp --- @[simp] --- theorem Term.smap_term_app {t1 t2} {σ : SubstVec [Term]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by --- simp only [SubstMap.smap]; rw [smap]; try simp +@[simp] +theorem Term.smap_term_app {t1 t2} {σ : SubstVec [Term]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by + simp only [SubstMap.smap]; rw [smap]; try simp --- @[simp] --- theorem Term.smap_term_lam {A t} {σ : SubstVec [Term]} --- : (lam A t)[σ,] = lam A t[σ.lift [1],] --- := by simp only [SubstMap.smap]; rw [smap]; try simp +@[simp] +theorem Term.smap_term_lam {A t} {σ : SubstVec [Term]} + : (lam A t)[σ,] = lam A t[σ.lift [1],] +:= by simp only [SubstMap.smap]; rw [smap]; try simp --- @[simp] --- theorem Term.smap_term_tapp {t1 t2} {σ : SubstVec [Term]} --- : (tapp t1 t2)[σ,] = tapp t1[σ,] t2 --- := by simp only [SubstMap.smap]; rw [smap]; try simp +@[simp] +theorem Term.smap_term_tapp {t1 t2} {σ : SubstVec [Term]} + : (tapp t1 t2)[σ,] = tapp t1[σ,] t2 +:= by simp only [SubstMap.smap]; rw [smap]; try simp --- @[simp] --- theorem Term.smap_term_tlam {t} {σ : SubstVec [Term]} --- : (tlam t)[σ,] = tlam t[σ |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] --- := by simp only [SubstMap.smap]; rw [smap]; try simp +@[simp] +theorem Term.smap_term_tlam {t} {σ : SubstVec [Term]} + : (tlam t)[σ,] = tlam t[σ |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp --- @[simp] --- theorem Term.smap_term_zero {σ : SubstVec [Term]} : zero[σ,] = zero := by --- simp only [SubstMap.smap]; rw [smap]; try simp +@[simp] +theorem Term.smap_term_zero {σ : SubstVec [Term]} : zero[σ,] = zero := by + simp only [SubstMap.smap]; rw [smap]; try simp --- @[simp] --- theorem Term.smap_term_succ {t} {σ : SubstVec [Term]} : (succ t)[σ,] = succ t[σ,] := by --- simp only [SubstMap.smap]; rw [smap]; try simp +@[simp] +theorem Term.smap_term_succ {t} {σ : SubstVec [Term]} : (succ t)[σ,] = succ t[σ,] := by + simp only [SubstMap.smap]; rw [smap]; try simp --- @[simp] --- theorem Term.smap_term_nrec {m z s n} {σ : SubstVec [Term]} --- : (nrec m z s n)[σ,] = nrec m z[σ,] s[σ |> .lift [2] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] n[σ,] --- := by simp only [SubstMap.smap]; rw [smap]; try simp +@[simp] +theorem Term.smap_term_nrec {m z s n} {σ : SubstVec [Term]} + : (nrec m z s n)[σ,] = nrec m z[σ,] s[σ |> .lift [2] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] n[σ,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp --- @[simp] --- theorem Term.from_action_smap0 {t : Action Term} {σ : SubstVec [Term]} --- : (from_action t)[σ,] = from_action t[σ,] --- := by cases t <;> simp [from_action] +@[simp] +theorem Term.from_action_smap0 {t : Action Term} {σ : SubstVec [Term]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp [from_action] --- instance : SubstSuffix Term [] := ⟨⟩ --- instance : SubstMap Term [] where --- smap _ := id +instance : SubstSuffix Term [] := ⟨⟩ +instance : SubstMap Term [] where + smap _ := id --- @[reducible, simp] --- instance instSubstMapAll_Term : SubstMapAll [Term] := .cons .nil +@[reducible, simp] +instance instSubstMapAll_Term : SubstMapAll [Term] := .cons .nil --- @[reducible, simp] --- instance instSubstMapAll_Term_Ty : SubstMapAll [Term, Ty] := .cons instSubstMapAll_Ty +@[reducible, simp] +instance instSubstMapAll_Term_Ty : SubstMapAll [Term, Ty] := .cons instSubstMapAll_Ty --- instance : SubstMapEmpty Term where --- apply_empty := by intro s; simp [SubstMap.smap] +instance : SubstMapEmpty Term where + apply_empty := by intro s; simp [SubstMap.smap] --- instance : SubstMapVecDef Term Term [] where --- apply_vecdef := by intro s σ; induction s generalizing σ <;> simp [*] +instance : SubstMapVecDef Term Term [] where + apply_vecdef := by intro s σ; induction s generalizing σ <;> simp [*] --- -- The `[Ty]` Suffix: --- instance : SuffixCommuteRenRen Term [Ty] where --- ren_ren := by subst_solve_compose +-- The `[Ty]` Suffix: +instance : SuffixCommuteRenRen Term [Ty] where + ren_ren := by subst_solve_compose --- instance : SuffixCommuteRenSub Term [Ty] where --- ren_sub := by subst_solve_compose +instance : SuffixCommuteRenSub Term [Ty] where + ren_sub := by subst_solve_compose --- instance : SuffixCommuteSubRen Term [Ty] where --- sub_ren := by subst_solve_compose +instance : SuffixCommuteSubRen Term [Ty] where + sub_ren := by subst_solve_compose --- instance : SubstMapVecDef Term Term [Ty] where --- apply_vecdef := by intro s σ; induction s generalizing σ <;> simp [*] +instance : SubstMapVecDef Term Term [Ty] where + apply_vecdef := by intro s σ; induction s generalizing σ <;> simp [*] --- instance : SubstMapId Term [Ty] where --- apply_id := by subst_solve_id +instance : SubstMapId Term [Ty] where + apply_id := by subst_solve_id --- instance : SubstMapStable Term [Ty] where --- apply_stable := by sorry --subst_solve_stable +instance : SubstMapStable Term [Ty] where + apply_stable := by sorry --subst_solve_stable --- instance : SubstMapRenComposeLeft Term [Ty] where --- apply_ren_compose_left := by subst_solve_compose +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 : SubstMapRenComposeRight Term [Ty] where + apply_ren_compose_right := by subst_solve_compose --- instance : SubstMapCompose Term [Ty] where --- apply_compose := by subst_solve_compose +instance : SubstMapCompose Term [Ty] where + apply_compose := by subst_solve_compose --- -- The `[Term]` Singleton: --- instance : SubstMapId Term [Term] where --- apply_id := by subst_solve_id +-- The `[Term]` Singleton: +instance : SubstMapId Term [Term] where + apply_id := by subst_solve_id --- instance : SubstMapStable Term [Term] where --- apply_stable := by sorry --subst_solve_stable +instance : SubstMapStable Term [Term] where + apply_stable := by sorry --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 --- -- The `[Term, Ty]` Original: --- instance : SubstMapId Term [Term, Ty] where --- apply_id := by subst_solve_id +-- The `[Term, Ty]` Original: +instance : SubstMapId Term [Term, Ty] where + apply_id := by subst_solve_id --- instance : SubstMapStable Term [Term, Ty] where --- apply_stable := by sorry --subst_solve_stable +instance : SubstMapStable Term [Term, Ty] where + apply_stable := by sorry --subst_solve_stable --- instance : SubstMapRenComposeLeft Term [Term, Ty] where --- apply_ren_compose_left := by subst_solve_compose +instance : SubstMapRenComposeLeft Term [Term, Ty] where + apply_ren_compose_left := by subst_solve_compose --- instance : SubstMapRenComposeRight Term [Term, Ty] where --- apply_ren_compose_right := by subst_solve_compose +instance : SubstMapRenComposeRight Term [Term, Ty] where + apply_ren_compose_right := by subst_solve_compose --- instance : SubstMapCompose Term [Term, Ty] where --- apply_compose := by subst_solve_compose +instance : SubstMapCompose Term [Term, Ty] where + apply_compose := by subst_solve_compose end SystemFWithNat diff --git a/Examples/VariadicSTLC/Term.lean b/Examples/VariadicSTLC/Term.lean index 8dbf78c..3c08659 100644 --- a/Examples/VariadicSTLC/Term.lean +++ b/Examples/VariadicSTLC/Term.lean @@ -8,10 +8,13 @@ inductive Ty where | base : Ty | arrow : Ty -> Ty +@[reducible] +def Variadic (n : Nat) (ty : Type) := Fin n → ty + inductive Term where | var : Nat -> Term -| app n : Term -> (Fin n -> Term) -> Term -| lam n : (Fin n -> Ty) -> Term -> Term +| app n : Term -> Variadic n Term -> Term +| lam n : Variadic n Ty -> Term -> Term @[coe] def Term.from_action : Action Term -> Term diff --git a/LeanSubst/Automation/Basic.lean b/LeanSubst/Automation/Basic.lean index 578b470..376f00b 100644 --- a/LeanSubst/Automation/Basic.lean +++ b/LeanSubst/Automation/Basic.lean @@ -176,19 +176,24 @@ namespace Automation `($stx.1) -- Applies a computation for each suffix in the list Tys. - def forEachSuffix : (tys : List Ident) → (f : List Ident → CommandElabM Unit) → CommandElabM Unit + def forEachSuffix {A : Type} : (tys : List A) → (f : List A → CommandElabM Unit) → CommandElabM Unit | [], _ => pure () | tys@(.cons _ tys'), f => do f tys forEachSuffix tys' f - def forEachPrefix : (tys : List Ident) → (f : List Ident → CommandElabM Unit) → CommandElabM Unit + def mapEachSuffix {A B : Type} : (tys : List A) → (f : List A → CommandElabM B) → CommandElabM $ List B + | [], _ => pure [] + | tys@(.cons _ tys'), f => do + pure $ (← (f tys)) :: (← mapEachSuffix tys' f) + + def forEachPrefix {A : Type} : (tys : List A) → (f : List A → CommandElabM Unit) → CommandElabM Unit | [], _ => pure () | tys@(.cons _ _), f => do f tys forEachSuffix tys.reverse.tail.reverse f - def forHeadAndEachSuffix : (tys : List Ident) → (f : List Ident → CommandElabM Unit) → CommandElabM Unit + def forHeadAndEachSuffix {A : Type} : (tys : List A) → (f : List A → CommandElabM Unit) → CommandElabM Unit | [], _ => pure () | .cons ty [], f => do f [ty] | tys@(.cons ty _), f => do @@ -209,6 +214,8 @@ namespace Automation -- The main function def genTy (tys : List Ident) : CommandElabM Unit := do + let numTotalTys := tys.length + let toGlobal (ty : Ident) : CommandElabM Name := Command.liftCoreM $ realizeGlobalConstNoOverload ty.raw let ty := tys[0]! let tyName := ty.raw.getId @@ -355,35 +362,30 @@ namespace Automation pure ⟨mkIdent ty', Syntax.mkNatLit 0⟩) pure $ increments.filter (fun (_, stx) ↦ match stx with | `(0) => false | _ => true) - let mkMapArr (data : ArgData) (xs : List Ident) (tys : List Ident) : CommandElabM $ Option MapOrLift := + let mkLiftsAndRens (data : ArgData) (xs : List Ident) (tys : List Ident) : CommandElabM $ Option $ Term × List Term := match data with | .binder _ => do let lifts ← tys.mapM $ getLiftsOfTy data xs let optionLifts := lifts.map (fun stx : Term ↦ if BEq.beq stx $ Syntax.mkNatLit 0 then none else some stx) -- Check if all lifts are syntactically just 0 - if optionLifts.all (fun | none => true | some _ => false) then + if optionLifts.all (fun | .none => true | .some _ => false) then pure none else let tysNamesGlobal ← tys.mapM toGlobal - let incrementsList ← tysNamesGlobal.mapM $ getIncrementsOfTy lifts tysNamesGlobal - let zipped := incrementsList.zip optionLifts - let ops : List $ Term × Bool ← zipped.mapM (fun ⟨incs, lift⟩ ↦ do - let incOps ← incs.mapM (fun ⟨ty, inc⟩ ↦ - if BEq.beq inc $ Syntax.mkNatLit 0 then `(Ren.id $ty:ident) else `(Ren.add $ty:ident $inc)) - let anyIncs := incs.tail.any (fun ⟨_, inc⟩ ↦ ¬ (BEq.beq inc $ Syntax.mkNatLit 0)) - - let tyTail := tysNamesGlobal.tail.toArray.map mkIdent - let op ← match (anyIncs, lift) with - | (false, none) => `(.skip) - | (true, none) => `(.ren [$tyTail,*] ⟨$incOps.tail.toArray,*, .nil⟩) - | (false, some ℓ) => `(.lift $ℓ) - | (true, some ℓ) => `(.both [$tyTail,*] ⟨$incOps.tail.toArray,*, .nil⟩ $ℓ) - pure ⟨op, anyIncs⟩ + let zipped := tysNamesGlobal.zip optionLifts + let rens : List $ Term ← mapEachSuffix zipped (fun zippedSfx ↦ do + let ⟨tys, optionLifts⟩ := zippedSfx.unzip + let lifts ← zippedSfx.tail.mapM (fun | ⟨ty, .none⟩ => `(Ren.id $(mkIdent ty)) | ⟨ty, .some n⟩ => `(Ren.add $(mkIdent ty) $n)) + let tysHd := mkIdent tys.head! + let tysTail := (tys.tail!.map mkIdent).toArray + let i := Syntax.mkNatLit $ numTotalTys - tys.length -- shadowing is bad, kids + `(.ren $tysHd [$tysTail,*] ⟨$lifts.toArray,*, .nil⟩ $i rfl) ) - if ops.all (¬ ·.2) then -- If we don't have to apply any renamings - pure $ MapOrLift.lift $ ← `([$lifts.toArray,*]) - else - pure $ MapOrLift.map $ ← (ops.map Prod.fst).foldrM (fun t1 t2 ↦ `($t1 $ $t2)) $ ← `(LeanSubst.SubstVec.MapOps.nil) + let rens := rens.reverse.tail.reverse -- dropLast + dbg_trace s!"\n For ty list {tys}, rens is {rens} \n" + let liftsTm ← `([$lifts.toArray,*]) + pure $ some ⟨liftsTm, rens⟩ + | _ => pure none let smap_fVar (tys : List Ident) xs ctor : CommandElabM Term := do @@ -412,10 +414,13 @@ namespace Automation else if useTCSyntax then `(($x)⟨$(r),⟩) else `($rmap $r $x) | .smap => - if let MapOrLift.map opsArr ← mkMapArr data xs tys then - if useTCSyntax then `(($x)[$(σ).map $opsArr,]) else `($smap ($(σ).map $opsArr) $x) - else if let MapOrLift.lift opsArr ← mkMapArr data xs tys then - if useTCSyntax then `(($x)[$(σ).lift $opsArr,]) else `($smap ($(σ).lift $opsArr) $x) + if let some ⟨lift, []⟩ ← mkLiftsAndRens data xs tys then + if useTCSyntax then `(($x)[($(σ).lift $lift),]) else `($smap ($(σ).lift $lift) $x) + else if let some ⟨lift, rens⟩ ← mkLiftsAndRens data xs tys then + let mut σ' ← `($(σ) |> SubstVec.lift $lift) + for ren in rens do + σ' ← `($σ' |> $ren) + if useTCSyntax then `(($x)[$(σ'),]) else `($smap ($σ') $x) else if useTCSyntax then `(($x)[$(σ),]) else `($smap $σ $x) else if let some theTy ← List.findM? (fun (ty : Ident) ↦ do pure (← liftCoreM $ runMetaMAsCoreM $ isDefEq (← liftTermElabM $ Term.elabTerm ty.raw none) ty')) tys then @@ -463,6 +468,7 @@ namespace Automation let fLhs lhs : CommandElabM Term := match mapType with | .rmap => `(($lhs)⟨$(rσ),⟩) | .smap => `(($lhs)[$(rσ),]) let eq ← mkCtorEq fLhs fRhs ctor (fVar := match mapType with | .rmap => none | .smap => some $ smap_fVar sfx) let args ← mkCtorArgs ctor + dbg_trace s!"\n MAKING THEOREM {thmName},\n suffix is {sfx}, \n equation is {eq}\n" elabCommand $ ← `( @[simp] theorem $thmName {$args.toArray*} {$rσ : $TheVec [$sfx.toArray,*]} : $eq := From daa86ff349e82a3bdea5562db017c9484e8df39f Mon Sep 17 00:00:00 2001 From: Sage Binder Date: Sat, 5 Sep 2026 15:07:03 +0100 Subject: [PATCH 2/3] bugs fixed, I think --- Examples/SystemFWithNat/Term.lean | 30 +----------------------------- LeanSubst/Automation/Basic.lean | 25 +++++++++++++++---------- 2 files changed, 16 insertions(+), 39 deletions(-) diff --git a/Examples/SystemFWithNat/Term.lean b/Examples/SystemFWithNat/Term.lean index cb649f7..a8b9332 100644 --- a/Examples/SystemFWithNat/Term.lean +++ b/Examples/SystemFWithNat/Term.lean @@ -20,7 +20,7 @@ inductive Term where | 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 +| nrec (motive : Ty) (z : Term) (s : Term) (n : Term) : Term -- binds 2 Terms in s #leansubst var Ty.var #leansubst bind Ty at pos 0 in Ty.all @@ -30,36 +30,8 @@ inductive Term where #leansubst bind Ty at pos 0 in Term.tlam #leansubst bind 2 of Term at pos 2 in Term.nrec ---set_option diagnostics true - #leansubst generate Ty, Term --- | tlam t => tlam (t.smap $ σ |> .lift [0, 1] |> .ren Term [Ty] ⟨𝐫1, .nil⟩ 0 rfl) --- | x0.tlam => fun x => (x.1 (SubstVec.ren Term [Ty] (Ren.add Ty 1, RenVec.nil) 0 ⋯ (SubstVec.lift [0, 1] σ))).tlam -#print Term.smap._f -#print Term.smap_term_tlam - -theorem SystemFWithNat.Term.smap_term_tlam' : ∀ {x0 : Term} {σ : SubstVec [Term]}, x0.tlam[σ,] = x0[σ,].tlam := by - intros - simp only [SubstMap.smap] - simp [-Term.smap_term_tlam] - - - -instance : RenMapVecDef Term Term [Ty] where - apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] - -instance : RenMapId Term [Term, Ty] where - apply_id := by subst_solve_id - -instance : RenMapCompose Term [Term, Ty] where - apply_compose := by subst_solve_compose - -instance : RenMapVecDef Term Term [] where - apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] - - - -- Checking Ty -- #print Ty.from_action #print Ty.from_action_id diff --git a/LeanSubst/Automation/Basic.lean b/LeanSubst/Automation/Basic.lean index 376f00b..a0cc82d 100644 --- a/LeanSubst/Automation/Basic.lean +++ b/LeanSubst/Automation/Basic.lean @@ -222,8 +222,6 @@ namespace Automation -- let tyStr := tyName.toString let tyNameGlobal ← toGlobal ty - dbg_trace s!"Generating {ty} with list {tys}" - -- let tyArr ← `([$tys.toArray,*]) -- let tysNamesGlobal ← tys.mapM toGlobal @@ -362,9 +360,19 @@ namespace Automation pure ⟨mkIdent ty', Syntax.mkNatLit 0⟩) pure $ increments.filter (fun (_, stx) ↦ match stx with | `(0) => false | _ => true) - let mkLiftsAndRens (data : ArgData) (xs : List Ident) (tys : List Ident) : CommandElabM $ Option $ Term × List Term := + let mkLiftsAndRens (data : ArgData) (xs : List Ident) (tys' : List Ident) : CommandElabM $ Option $ Term × List Term := match data with | .binder _ => do + let ⟨tys, headOnly⟩ : (List Ident) × Bool ← + if tys'.length = 1 ∧ tys.length > 1 then do + let ty'0_eq_ty0 ← liftCoreM $ runMetaMAsCoreM $ isDefEq (← liftTermElabM $ Term.elabTerm (tys'.head!) none) (← liftTermElabM $ Term.elabTerm (tys.head!) none) + if ty'0_eq_ty0 then -- The head-only case (for instance, tys' = [Term] and tys = [Term, Ty]) + pure ⟨tys, true⟩ + else + pure ⟨tys', false⟩ + else + pure ⟨tys', false⟩ + let lifts ← tys.mapM $ getLiftsOfTy data xs let optionLifts := lifts.map (fun stx : Term ↦ if BEq.beq stx $ Syntax.mkNatLit 0 then none else some stx) -- Check if all lifts are syntactically just 0 @@ -382,10 +390,8 @@ namespace Automation `(.ren $tysHd [$tysTail,*] ⟨$lifts.toArray,*, .nil⟩ $i rfl) ) let rens := rens.reverse.tail.reverse -- dropLast - dbg_trace s!"\n For ty list {tys}, rens is {rens} \n" let liftsTm ← `([$lifts.toArray,*]) pure $ some ⟨liftsTm, rens⟩ - | _ => pure none let smap_fVar (tys : List Ident) xs ctor : CommandElabM Term := do @@ -414,10 +420,10 @@ namespace Automation else if useTCSyntax then `(($x)⟨$(r),⟩) else `($rmap $r $x) | .smap => - if let some ⟨lift, []⟩ ← mkLiftsAndRens data xs tys then - if useTCSyntax then `(($x)[($(σ).lift $lift),]) else `($smap ($(σ).lift $lift) $x) - else if let some ⟨lift, rens⟩ ← mkLiftsAndRens data xs tys then - let mut σ' ← `($(σ) |> SubstVec.lift $lift) + if let some ⟨lifts, []⟩ ← mkLiftsAndRens data xs tys then + if useTCSyntax then `(($x)[($(σ).lift $lifts),]) else `($smap ($(σ).lift $lifts) $x) + else if let some ⟨lifts, rens⟩ ← mkLiftsAndRens data xs tys then + let mut σ' ← `($(σ) |> SubstVec.lift $lifts) for ren in rens do σ' ← `($σ' |> $ren) if useTCSyntax then `(($x)[$(σ'),]) else `($smap ($σ') $x) @@ -468,7 +474,6 @@ namespace Automation let fLhs lhs : CommandElabM Term := match mapType with | .rmap => `(($lhs)⟨$(rσ),⟩) | .smap => `(($lhs)[$(rσ),]) let eq ← mkCtorEq fLhs fRhs ctor (fVar := match mapType with | .rmap => none | .smap => some $ smap_fVar sfx) let args ← mkCtorArgs ctor - dbg_trace s!"\n MAKING THEOREM {thmName},\n suffix is {sfx}, \n equation is {eq}\n" elabCommand $ ← `( @[simp] theorem $thmName {$args.toArray*} {$rσ : $TheVec [$sfx.toArray,*]} : $eq := From 12728b7e5f1d8245c56902c9c7038ffa3cb91ebc Mon Sep 17 00:00:00 2001 From: Sage Binder Date: Sat, 5 Sep 2026 15:27:45 +0100 Subject: [PATCH 3/3] Fix --- Examples/SystemFWithNat/Term.lean | 978 +++++++++++++++--------------- LeanSubst/Automation/Basic.lean | 18 +- 2 files changed, 504 insertions(+), 492 deletions(-) diff --git a/Examples/SystemFWithNat/Term.lean b/Examples/SystemFWithNat/Term.lean index a8b9332..04dc739 100644 --- a/Examples/SystemFWithNat/Term.lean +++ b/Examples/SystemFWithNat/Term.lean @@ -28,7 +28,10 @@ inductive Term where #leansubst var Term.var #leansubst bind Term at pos 1 in Term.lam #leansubst bind Ty at pos 0 in Term.tlam -#leansubst bind 2 of Term at pos 2 in Term.nrec +#leansubst bind + 2 of Term at pos 2, + 1 of Ty at pos 2 + in Term.nrec #leansubst generate Ty, Term @@ -227,571 +230,576 @@ inductive Term where #check (inferInstance : SubstMapCompose Term [Ty]) #check (inferInstance : SubstMapCompose Term [Term]) ----------------------------------------------------------------------------------------------------- --- Ty Renaming & Substitution ----------------------------------------------------------------------------------------------------- -@[coe] -def Ty.from_action : Action Ty -> Ty -| re y => var y -| su t => t +-- ---------------------------------------------------------------------------------------------------- +-- -- Ty Renaming & Substitution +-- ---------------------------------------------------------------------------------------------------- +-- @[coe] +-- def Ty.from_action : Action Ty -> Ty +-- | re y => var y +-- | su t => t -@[simp] -theorem Ty.from_action_id {n} : from_action (𝐬0.act n) = var n := by - simp [from_action] +-- @[simp] +-- theorem Ty.from_action_id {n} : from_action (𝐬0.act n) = var n := by +-- simp [from_action] -@[simp] -theorem Ty.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by - simp [from_action] +-- @[simp] +-- theorem Ty.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by +-- simp [from_action] -@[simp] -theorem Ty.from_action_re {n} : from_action (re n) = var n := by simp [from_action] +-- @[simp] +-- theorem Ty.from_action_re {n} : from_action (re n) = var n := by simp [from_action] -@[simp] -theorem Ty.from_action_su {t} : from_action (su t) = t := by simp [from_action] +-- @[simp] +-- 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 +-- instance : Coe (Action Ty) Ty where +-- coe := Ty.from_action -@[simp] -def Ty.rmap (r : RenVec [Ty]) : Ty -> Ty -| var x => var (r.1.act x) -| nat => nat -| arrow t1 t2 => arrow (t1.rmap r) (t2.rmap r) -| all t => all $ t.rmap $ r.lift [1] +-- @[simp] +-- def Ty.rmap (r : RenVec [Ty]) : Ty -> Ty +-- | var x => var (r.1.act x) +-- | nat => nat +-- | arrow t1 t2 => arrow (t1.rmap r) (t2.rmap r) +-- | all t => all $ t.rmap $ r.lift [1] -instance : RenMap Ty [Ty] where - rmap := Ty.rmap +-- instance : RenMap Ty [Ty] where +-- rmap := Ty.rmap -@[simp] -theorem Ty.rmap_fix {r : RenVec [Ty]} {t : Ty} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] +-- @[simp] +-- theorem Ty.rmap_fix {r : RenVec [Ty]} {t : Ty} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] -instance : RenSuffix Ty [] := ⟨⟩ -instance : RenMap Ty [] where - rmap _ := id +-- instance : RenSuffix Ty [] := ⟨⟩ +-- instance : RenMap Ty [] where +-- rmap _ := id -@[reducible, simp] -instance instRenMapAll_Ty : RenMapAll [Ty] := .cons .nil +-- @[reducible, simp] +-- instance instRenMapAll_Ty : RenMapAll [Ty] := .cons .nil -@[simp] -theorem Ty.rmap_var {x} {r : RenVec [Ty]} : (var x)⟨r,⟩ = .var (r.1.act x) := by - simp only [RenMap.rmap]; rw [rmap] +-- @[simp] +-- theorem Ty.rmap_var {x} {r : RenVec [Ty]} : (var x)⟨r,⟩ = .var (r.1.act x) := by +-- simp only [RenMap.rmap]; rw [rmap] -@[simp] -theorem Ty.rmap_nat {r : RenVec [Ty]} : (nat)⟨r,⟩ = nat := by - simp only [RenMap.rmap]; rw [rmap] +-- @[simp] +-- theorem Ty.rmap_nat {r : RenVec [Ty]} : (nat)⟨r,⟩ = nat := by +-- simp only [RenMap.rmap]; rw [rmap] -@[simp] -theorem Ty.rmap_arrow {t1 t2 : Ty} {r : RenVec [Ty]} : (arrow t1 t2)⟨r,⟩ = arrow t1⟨r,⟩ t2⟨r,⟩ := by - simp only [RenMap.rmap]; rw [rmap] +-- @[simp] +-- theorem Ty.rmap_arrow {t1 t2 : Ty} {r : RenVec [Ty]} : (arrow t1 t2)⟨r,⟩ = arrow t1⟨r,⟩ t2⟨r,⟩ := by +-- simp only [RenMap.rmap]; rw [rmap] -@[simp] -theorem Ty.rmap_all {t} {r : RenVec [Ty]} : (all t)⟨r,⟩ = all t⟨r.lift [1],⟩ := by - simp only [RenMap.rmap]; rw [rmap] +-- @[simp] +-- theorem Ty.rmap_all {t} {r : RenVec [Ty]} : (all t)⟨r,⟩ = all t⟨r.lift [1],⟩ := by +-- simp only [RenMap.rmap]; rw [rmap] -@[simp] -theorem Ty.from_action_rmap {t : Action Ty} {r : RenVec [Ty]} - : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ -:= by cases t <;> simp +-- @[simp] +-- theorem Ty.from_action_rmap {t : Action Ty} {r : RenVec [Ty]} +-- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +-- := by cases t <;> simp -instance : RenMapEmpty Ty where - apply_empty := by intro s; simp [RenMap.rmap] +-- instance : RenMapEmpty Ty where +-- apply_empty := by intro s; simp [RenMap.rmap] -instance : RenMapId Ty [Ty] where - apply_id := by subst_solve_id +-- instance : RenMapId Ty [Ty] where +-- apply_id := by subst_solve_id -instance : RenMapCompose Ty [Ty] where - apply_compose := by subst_solve_compose +-- instance : RenMapCompose Ty [Ty] where +-- apply_compose := by subst_solve_compose -@[simp] -def Ty.smap (σ : SubstVec [Ty]) : Ty -> Ty -| var x => σ.1.act x -| nat => nat -| arrow t1 t2 => arrow (t1.smap σ) (t2.smap σ) -| all t => all $ t.smap $ σ.lift [1] +-- @[simp] +-- def Ty.smap (σ : SubstVec [Ty]) : Ty -> Ty +-- | var x => σ.1.act x +-- | nat => nat +-- | arrow t1 t2 => arrow (t1.smap σ) (t2.smap σ) +-- | all t => all $ t.smap $ σ.lift [1] -instance : SubstMap Ty [Ty] where - smap := Ty.smap +-- instance : SubstMap Ty [Ty] where +-- smap := Ty.smap -@[simp] -theorem Ty.smap_fix {σ : SubstVec [Ty]} {t : Ty} : smap σ t = t[σ,] := by simp [SubstMap.smap] +-- @[simp] +-- theorem Ty.smap_fix {σ : SubstVec [Ty]} {t : Ty} : smap σ t = t[σ,] := by simp [SubstMap.smap] -instance : SubstSuffix Ty [] := ⟨⟩ -instance : SubstMap Ty [] where - smap _ := id +-- instance : SubstSuffix Ty [] := ⟨⟩ +-- instance : SubstMap Ty [] where +-- smap _ := id -@[reducible, simp] -instance instSubstMapAll_Ty : SubstMapAll [Ty] := .cons .nil +-- @[reducible, simp] +-- instance instSubstMapAll_Ty : SubstMapAll [Ty] := .cons .nil -@[simp] -theorem Ty.smap_var {x} {σ : SubstVec [Ty]} : (var x)[σ,] = σ.1.act x := by - simp only [SubstMap.smap]; rw [smap] +-- @[simp] +-- theorem Ty.smap_var {x} {σ : SubstVec [Ty]} : (var x)[σ,] = σ.1.act x := by +-- simp only [SubstMap.smap]; rw [smap] -@[simp] -theorem Ty.smap_nat {σ : SubstVec [Ty]} : (nat)[σ,] = nat := by - simp only [SubstMap.smap]; rw [smap] +-- @[simp] +-- theorem Ty.smap_nat {σ : SubstVec [Ty]} : (nat)[σ,] = nat := by +-- simp only [SubstMap.smap]; rw [smap] -@[simp] -theorem Ty.smap_arrow {t1 t2 : Ty} {σ : SubstVec [Ty]} : (arrow t1 t2)[σ,] = arrow t1[σ,] t2[σ,] := by - simp only [SubstMap.smap]; rw [smap] +-- @[simp] +-- theorem Ty.smap_arrow {t1 t2 : Ty} {σ : SubstVec [Ty]} : (arrow t1 t2)[σ,] = arrow t1[σ,] t2[σ,] := by +-- simp only [SubstMap.smap]; rw [smap] -@[simp] -theorem Ty.smap_all {t} {σ : SubstVec [Ty]} : (all t)[σ,] = all t[σ.lift [1],] := by - simp only [SubstMap.smap]; rw [smap] +-- @[simp] +-- theorem Ty.smap_all {t} {σ : SubstVec [Ty]} : (all t)[σ,] = all t[σ.lift [1],] := by +-- simp only [SubstMap.smap]; rw [smap] -@[simp] -theorem Ty.from_action_smap {t : Action Ty} {σ : SubstVec [Ty]} - : (from_action t)[σ,] = from_action t[σ,] -:= by cases t <;> simp +-- @[simp] +-- theorem Ty.from_action_smap {t : Action Ty} {σ : SubstVec [Ty]} +-- : (from_action t)[σ,] = from_action t[σ,] +-- := by cases t <;> simp -instance : SubstMapEmpty Ty where - apply_empty := by intro s; simp [SubstMap.smap] +-- instance : SubstMapEmpty Ty where +-- apply_empty := by intro s; simp [SubstMap.smap] -instance : SubstMapId Ty [Ty] where - apply_id := by subst_solve_id +-- instance : SubstMapId Ty [Ty] where +-- apply_id := by subst_solve_id -instance : SubstMapStable Ty [Ty] where - apply_stable := by subst_solve_stable +-- 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 : 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 : SubstMapRenComposeRight Ty [Ty] where +-- apply_ren_compose_right := by subst_solve_compose -instance : SubstMapCompose Ty [Ty] where - apply_compose := by subst_solve_compose +-- instance : SubstMapCompose Ty [Ty] where +-- apply_compose := by subst_solve_compose ----------------------------------------------------------------------------------------------------- --- Term Renaming & Substitution ----------------------------------------------------------------------------------------------------- +-- ---------------------------------------------------------------------------------------------------- +-- -- Term Renaming & Substitution +-- ---------------------------------------------------------------------------------------------------- -@[coe] -def Term.from_action : Action Term -> Term -| re y => var y -| su t => t +-- @[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_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_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_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] +-- @[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 +-- instance : Coe (Action Term) Term where +-- coe := Term.from_action -@[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, 1]) (n.rmap r) +-- @[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, 1]) (n.rmap r) -instance : RenMap Term [Term, Ty] where - rmap := Term.rmap - -@[simp] -theorem Term.rmap_fix {r : RenVec [Term, Ty]} {t : Term} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] - -@[simp] -theorem Term.rmap_term_ty_var {x} {r : RenVec [Term, Ty]} : (var x)⟨r,⟩ = var (r.1.act x) := rfl +-- instance : RenMap Term [Term, Ty] where +-- rmap := Term.rmap + +-- @[simp] +-- theorem Term.rmap_fix {r : RenVec [Term, Ty]} {t : Term} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] + +-- @[simp] +-- theorem Term.rmap_term_ty_var {x} {r : RenVec [Term, Ty]} : (var x)⟨r,⟩ = var (r.1.act x) := rfl -@[simp] -theorem Term.rmap_term_ty_app {t1 t2} {r : RenVec [Term, Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by - simp only [RenMap.rmap]; rw [rmap] +-- @[simp] +-- theorem Term.rmap_term_ty_app {t1 t2} {r : RenVec [Term, Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by +-- simp only [RenMap.rmap]; rw [rmap] -@[simp] -theorem Term.rmap_term_ty_lam'' {A t} {r : RenVec [Term, Ty]} - : (lam A t)⟨r,⟩ = lam A⟨r.2.1⟩ t⟨r.lift [1, 0],⟩ -:= by simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_ty_tapp {t1 t2} {r : RenVec [Term, Ty]} - : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.2.1⟩ -:= by simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_ty_tlam {t} {r : RenVec [Term, Ty]} : (tlam t)⟨r,⟩ = tlam t⟨r.lift [0, 1],⟩ := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_ty_zero {r : RenVec [Term, Ty]} : zero⟨r,⟩ = zero := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_ty_succ {t} {r : RenVec [Term, Ty]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_ty_nrec {m z s n} {r : RenVec [Term, Ty]} - : (nrec m z s n)⟨r,⟩ = nrec m⟨r.2.1⟩ z⟨r,⟩ s⟨r.lift [2, 1],⟩ n⟨r,⟩ -:= by simp only [RenMap.rmap]; rw [rmap]; try simp - -instance : RenSuffix Term [Ty] := ⟨⟩ -instance : RenMap Term [Ty] where - rmap r := Term.rmap (Ren.id Term, r.1, .nil) - -@[simp] -theorem Term.rmap_ty_var {x} {r : RenVec [Ty]} : (var x)⟨r,⟩ = var x := by - simp only [RenMap.rmap]; rw [rmap]; try simp +-- @[simp] +-- theorem Term.rmap_term_ty_lam'' {A t} {r : RenVec [Term, Ty]} +-- : (lam A t)⟨r,⟩ = lam A⟨r.2.1⟩ t⟨r.lift [1, 0],⟩ +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_ty_tapp {t1 t2} {r : RenVec [Term, Ty]} +-- : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.2.1⟩ +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_ty_tlam {t} {r : RenVec [Term, Ty]} : (tlam t)⟨r,⟩ = tlam t⟨r.lift [0, 1],⟩ := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_ty_zero {r : RenVec [Term, Ty]} : zero⟨r,⟩ = zero := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_ty_succ {t} {r : RenVec [Term, Ty]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_ty_nrec {m z s n} {r : RenVec [Term, Ty]} +-- : (nrec m z s n)⟨r,⟩ = nrec m⟨r.2.1⟩ z⟨r,⟩ s⟨r.lift [2, 1],⟩ n⟨r,⟩ +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp + +-- instance : RenSuffix Term [Ty] := ⟨⟩ +-- instance : RenMap Term [Ty] where +-- rmap r := Term.rmap (Ren.id Term, r.1, .nil) + +-- @[simp] +-- theorem Term.rmap_ty_var {x} {r : RenVec [Ty]} : (var x)⟨r,⟩ = var x := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp -@[simp] -theorem Term.rmap_ty_app {t1 t2} {r : RenVec [Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_ty_lam {A t} {r : RenVec [Ty]} - : (lam A t)⟨r,⟩ = lam A⟨r.1⟩ t⟨r,⟩ -:= by simp only [RenMap.rmap]; rw [rmap]; try simp +-- @[simp] +-- theorem Term.rmap_ty_app {t1 t2} {r : RenVec [Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_ty_lam {A t} {r : RenVec [Ty]} +-- : (lam A t)⟨r,⟩ = lam A⟨r.1⟩ t⟨r,⟩ +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp -@[simp] -theorem Term.rmap_ty_tapp {t1 t2} {r : RenVec [Ty]} - : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.1⟩ -:= by simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_ty_tlam {t} {r : RenVec [Ty]} : (tlam t)⟨r,⟩ = tlam t⟨r.lift [1],⟩ := by - simp only [RenMap.rmap]; rw [rmap]; try simp +-- @[simp] +-- theorem Term.rmap_ty_tapp {t1 t2} {r : RenVec [Ty]} +-- : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.1⟩ +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_ty_tlam {t} {r : RenVec [Ty]} : (tlam t)⟨r,⟩ = tlam t⟨r.lift [1],⟩ := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp -@[simp] -theorem Term.rmap_ty_zero {r : RenVec [Ty]} : zero⟨r,⟩ = zero := by - simp only [RenMap.rmap]; rw [rmap]; try simp +-- @[simp] +-- theorem Term.rmap_ty_zero {r : RenVec [Ty]} : zero⟨r,⟩ = zero := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp -@[simp] -theorem Term.rmap_ty_succ {t} {r : RenVec [Ty]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_ty_nrec {m z s n} {r : RenVec [Ty]} - : (nrec m z s n)⟨r,⟩ = nrec m⟨r.1⟩ z⟨r,⟩ s⟨r.lift [1],⟩ n⟨r,⟩ -:= by simp only [RenMap.rmap]; rw [rmap]; try simp - -instance : RenMap Term [Term] where - rmap r := Term.rmap (r.1, Ren.id Ty, .nil) - -@[simp] -theorem Term.rmap_term_var {x} {r : RenVec [Term]} : (var x)⟨r,⟩ = var (r.1.act x) := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_app {t1 t2} {r : RenVec [Term]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_lam' {A t} {r : RenVec [Term]} - : (lam A t)⟨r,⟩ = lam A t⟨r.lift [1],⟩ -:= by simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_tapp {t1 t2} {r : RenVec [Term]} - : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2 -:= by simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_tlam {t} {r : RenVec [Term]} : (tlam t)⟨r,⟩ = tlam t⟨r,⟩ := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_zero {r : RenVec [Term]} : zero⟨r,⟩ = zero := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_succ {t} {r : RenVec [Term]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by - simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.rmap_term_nrec {m z s n} {r : RenVec [Term]} - : (nrec m z s n)⟨r,⟩ = nrec m z⟨r,⟩ s⟨r.lift [2],⟩ n⟨r,⟩ -:= by simp only [RenMap.rmap]; rw [rmap]; try simp - -@[simp] -theorem Term.from_action_rmap {t : Action Term} {r : RenVec [Term, Ty]} - : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ -:= by cases t <;> simp [from_action] - -@[simp] -theorem Term.from_action_rmap0 {t : Action Term} {r : RenVec [Term]} - : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ -:= by cases t <;> simp [from_action] - -@[simp] -theorem Term.from_action_rmap1 {t : Action Term} {r : RenVec [Ty]} - : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ -:= by cases t <;> simp [from_action] - -instance : RenSuffix Term [] := ⟨⟩ -instance : RenMap Term [] where - rmap _ := id - -@[reducible, simp] -instance instRenMapAll_Term : RenMapAll [Term] := .cons .nil - -@[reducible, simp] -instance instRenMapAll_Term_Ty : RenMapAll [Term, Ty] := .cons instRenMapAll_Ty - -instance : RenMapEmpty Term where - apply_empty := by intro s; simp [RenMap.rmap] - -instance : RenMapVecDef Term Term [Ty] where - apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] - -instance : RenMapId Term [Term, Ty] where - apply_id := by subst_solve_id - -instance : RenMapCompose Term [Term, Ty] where - apply_compose := by subst_solve_compose - -instance : RenMapVecDef Term Term [] where - apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] - -instance : RenMapId Term [Term] where - apply_id := by subst_solve_id - -instance : RenMapCompose Term [Term] where - apply_compose := by subst_solve_compose - -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.smap' (σ : SubstVec [Term, Ty]) : Term -> Term -| var x => σ.1.act x -| app t1 t2 => app (t1.smap σ) (t2.smap σ) -| lam A t => lam A[σ.2.1] (t.smap $ σ.lift [1, 0]) -| tapp t A => tapp (t.smap σ) A[σ.2.1] -| tlam t => tlam (t.smap $ σ |> .lift [0, 1] |> .ren Term [Ty] ⟨𝐫1, .nil⟩ 0 rfl) -| zero => zero -| succ t => succ (t.smap σ) -| nrec motive z s n => - nrec motive[σ.2.1] (z.smap σ) (s.smap $ σ |> .lift [2, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl) (n.smap σ) - -instance : SubstMap Term [Term, Ty] where - smap := Term.smap - -@[simp] -theorem Term.smap_fix {σ : SubstVec [Term, Ty]} {t : Term} : smap σ t = t[σ,] := by - simp [SubstMap.smap] - -@[simp] -theorem Term.smap_term_ty_var {x} {σ : SubstVec [Term, Ty]} : (var x)[σ,] = σ.1.act x := by - simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_term_ty_app {t1 t2} {σ : SubstVec [Term, Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by - simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_term_ty_lam {A t} {σ : SubstVec [Term, Ty]} - : (lam A t)[σ,] = lam A[σ.2.1] t[σ.lift [1, 0],] -:= by simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_term_ty_tapp {t1 t2} {σ : SubstVec [Term, Ty]} - : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.2.1] -:= by simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_term_ty_tlam {t} {σ : SubstVec [Term, Ty]} - : (tlam t)[σ,] = tlam t[σ |> .lift [0, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] -:= by simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_term_ty_zero {σ : SubstVec [Term, Ty]} : zero[σ,] = zero := by - simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_term_ty_succ {t} {σ : SubstVec [Term, Ty]} : (succ t)[σ,] = succ t[σ,] := by - simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_term_ty_nrec {m z s n} {σ : SubstVec [Term, Ty]} - : (nrec m z s n)[σ,] = nrec m[σ.2.1] z[σ,] s[σ |> .lift [2, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] n[σ,] -:= by simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.from_action_smap {t : Action Term} {σ : SubstVec [Term, Ty]} - : (from_action t)[σ,] = from_action t[σ,] -:= by cases t <;> simp [from_action] - -instance : SubstSuffix Term [Ty] := ⟨⟩ -@[simp] -instance : SubstMap Term [Ty] where - smap σ := Term.smap (Subst.id Term, σ.1, .nil) - -@[simp] -theorem Term.smap_ty_var {x} {σ : SubstVec [Ty]} : (var x)[σ,] = var x := by - simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_ty_app {t1 t2} {σ : SubstVec [Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by - simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_ty_lam {A t} {σ : SubstVec [Ty]} - : (lam A t)[σ,] = lam A[σ.1] t[σ,] -:= by simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_ty_tapp {t1 t2} {σ : SubstVec [Ty]} - : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.1] -:= by simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_ty_tlam {t} {σ : SubstVec [Ty]} - : (tlam t)[σ,] = tlam t[σ |> .lift [1],] -:= by simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_ty_zero {σ : SubstVec [Ty]} : zero[σ,] = zero := by - simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_ty_succ {t} {σ : SubstVec [Ty]} : (succ t)[σ,] = succ t[σ,] := by - simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.smap_ty_nrec {m z s n} {σ : SubstVec [Ty]} - : (nrec m z s n)[σ,] = nrec m[σ.1] z[σ,] s[σ |> .lift [1],] n[σ,] -:= by simp only [SubstMap.smap]; rw [smap]; try simp - -@[simp] -theorem Term.from_action_smap1 {t : Action Term} {σ : SubstVec [Ty]} - : (from_action t)[σ,] = from_action t[σ,] -:= by cases t <;> simp [from_action] - -@[simp] -instance : SubstMap Term [Term] where - smap σ := Term.smap (σ.1, Subst.id Ty, .nil) +-- @[simp] +-- theorem Term.rmap_ty_succ {t} {r : RenVec [Ty]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_ty_nrec {m z s n} {r : RenVec [Ty]} +-- : (nrec m z s n)⟨r,⟩ = nrec m⟨r.1⟩ z⟨r,⟩ s⟨r.lift [1],⟩ n⟨r,⟩ +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp + +-- instance : RenMap Term [Term] where +-- rmap r := Term.rmap (r.1, Ren.id Ty, .nil) + +-- @[simp] +-- theorem Term.rmap_term_var {x} {r : RenVec [Term]} : (var x)⟨r,⟩ = var (r.1.act x) := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_app {t1 t2} {r : RenVec [Term]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_lam' {A t} {r : RenVec [Term]} +-- : (lam A t)⟨r,⟩ = lam A t⟨r.lift [1],⟩ +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_tapp {t1 t2} {r : RenVec [Term]} +-- : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2 +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_tlam {t} {r : RenVec [Term]} : (tlam t)⟨r,⟩ = tlam t⟨r,⟩ := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_zero {r : RenVec [Term]} : zero⟨r,⟩ = zero := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_succ {t} {r : RenVec [Term]} : (succ t)⟨r,⟩ = succ t⟨r,⟩ := by +-- simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.rmap_term_nrec {m z s n} {r : RenVec [Term]} +-- : (nrec m z s n)⟨r,⟩ = nrec m z⟨r,⟩ s⟨r.lift [2],⟩ n⟨r,⟩ +-- := by simp only [RenMap.rmap]; rw [rmap]; try simp + +-- @[simp] +-- theorem Term.from_action_rmap {t : Action Term} {r : RenVec [Term, Ty]} +-- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +-- := by cases t <;> simp [from_action] + +-- @[simp] +-- theorem Term.from_action_rmap0 {t : Action Term} {r : RenVec [Term]} +-- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +-- := by cases t <;> simp [from_action] + +-- @[simp] +-- theorem Term.from_action_rmap1 {t : Action Term} {r : RenVec [Ty]} +-- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +-- := by cases t <;> simp [from_action] + +-- instance : RenSuffix Term [] := ⟨⟩ +-- instance : RenMap Term [] where +-- rmap _ := id + +-- @[reducible, simp] +-- instance instRenMapAll_Term : RenMapAll [Term] := .cons .nil + +-- @[reducible, simp] +-- instance instRenMapAll_Term_Ty : RenMapAll [Term, Ty] := .cons instRenMapAll_Ty + +-- instance : RenMapEmpty Term where +-- apply_empty := by intro s; simp [RenMap.rmap] + +-- instance : RenMapVecDef Term Term [Ty] where +-- apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] + +-- instance : RenMapId Term [Term, Ty] where +-- apply_id := by subst_solve_id + +-- instance : RenMapCompose Term [Term, Ty] where +-- apply_compose := by subst_solve_compose + +-- instance : RenMapVecDef Term Term [] where +-- apply_vecdef := by intro s r; induction s generalizing r <;> simp [*] + +-- instance : RenMapId Term [Term] where +-- apply_id := by subst_solve_id + +-- instance : RenMapCompose Term [Term] where +-- apply_compose := by subst_solve_compose + +-- 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.smap' (σ : SubstVec [Term, Ty]) : Term -> Term +-- | var x => σ.1.act x +-- | app t1 t2 => app (t1.smap σ) (t2.smap σ) +-- | lam A t => lam A[σ.2.1] (t.smap $ σ.lift [1, 0]) +-- | tapp t A => tapp (t.smap σ) A[σ.2.1] +-- | tlam t => tlam (t.smap $ σ |> .lift [0, 1] |> .ren Term [Ty] ⟨𝐫1, .nil⟩ 0 rfl) +-- | zero => zero +-- | succ t => succ (t.smap σ) +-- | nrec motive z s n => +-- nrec motive[σ.2.1] (z.smap σ) (s.smap $ σ |> .lift [2, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl) (n.smap σ) + +-- -- Sanity check +-- theorem macroCorrect : Term.smap = Term.smap' := by +-- funext a b +-- induction b <;> simp + +-- instance : SubstMap Term [Term, Ty] where +-- smap := Term.smap + +-- @[simp] +-- theorem Term.smap_fix {σ : SubstVec [Term, Ty]} {t : Term} : smap σ t = t[σ,] := by +-- simp [SubstMap.smap] + +-- @[simp] +-- theorem Term.smap_term_ty_var {x} {σ : SubstVec [Term, Ty]} : (var x)[σ,] = σ.1.act x := by +-- simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_term_ty_app {t1 t2} {σ : SubstVec [Term, Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by +-- simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_term_ty_lam {A t} {σ : SubstVec [Term, Ty]} +-- : (lam A t)[σ,] = lam A[σ.2.1] t[σ.lift [1, 0],] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_term_ty_tapp {t1 t2} {σ : SubstVec [Term, Ty]} +-- : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.2.1] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_term_ty_tlam {t} {σ : SubstVec [Term, Ty]} +-- : (tlam t)[σ,] = tlam t[σ |> .lift [0, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_term_ty_zero {σ : SubstVec [Term, Ty]} : zero[σ,] = zero := by +-- simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_term_ty_succ {t} {σ : SubstVec [Term, Ty]} : (succ t)[σ,] = succ t[σ,] := by +-- simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_term_ty_nrec {m z s n} {σ : SubstVec [Term, Ty]} +-- : (nrec m z s n)[σ,] = nrec m[σ.2.1] z[σ,] s[σ |> .lift [2, 1] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] n[σ,] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.from_action_smap {t : Action Term} {σ : SubstVec [Term, Ty]} +-- : (from_action t)[σ,] = from_action t[σ,] +-- := by cases t <;> simp [from_action] + +-- instance : SubstSuffix Term [Ty] := ⟨⟩ +-- @[simp] +-- instance : SubstMap Term [Ty] where +-- smap σ := Term.smap (Subst.id Term, σ.1, .nil) + +-- @[simp] +-- theorem Term.smap_ty_var {x} {σ : SubstVec [Ty]} : (var x)[σ,] = var x := by +-- simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_ty_app {t1 t2} {σ : SubstVec [Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by +-- simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_ty_lam {A t} {σ : SubstVec [Ty]} +-- : (lam A t)[σ,] = lam A[σ.1] t[σ,] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_ty_tapp {t1 t2} {σ : SubstVec [Ty]} +-- : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.1] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_ty_tlam {t} {σ : SubstVec [Ty]} +-- : (tlam t)[σ,] = tlam t[σ |> .lift [1],] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_ty_zero {σ : SubstVec [Ty]} : zero[σ,] = zero := by +-- simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_ty_succ {t} {σ : SubstVec [Ty]} : (succ t)[σ,] = succ t[σ,] := by +-- simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.smap_ty_nrec {m z s n} {σ : SubstVec [Ty]} +-- : (nrec m z s n)[σ,] = nrec m[σ.1] z[σ,] s[σ |> .lift [1],] n[σ,] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp + +-- @[simp] +-- theorem Term.from_action_smap1 {t : Action Term} {σ : SubstVec [Ty]} +-- : (from_action t)[σ,] = from_action t[σ,] +-- := by cases t <;> simp [from_action] -@[simp] -theorem Term.smap_term_var {x} {σ : SubstVec [Term]} : (var x)[σ,] = σ.1.act x := by - simp only [SubstMap.smap]; rw [smap]; try simp +-- @[simp] +-- instance : SubstMap Term [Term] where +-- smap σ := Term.smap (σ.1, Subst.id Ty, .nil) -@[simp] -theorem Term.smap_term_app {t1 t2} {σ : SubstVec [Term]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by - simp only [SubstMap.smap]; rw [smap]; try simp +-- @[simp] +-- theorem Term.smap_term_var {x} {σ : SubstVec [Term]} : (var x)[σ,] = σ.1.act x := by +-- simp only [SubstMap.smap]; rw [smap]; try simp -@[simp] -theorem Term.smap_term_lam {A t} {σ : SubstVec [Term]} - : (lam A t)[σ,] = lam A t[σ.lift [1],] -:= by simp only [SubstMap.smap]; rw [smap]; try simp +-- @[simp] +-- theorem Term.smap_term_app {t1 t2} {σ : SubstVec [Term]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by +-- simp only [SubstMap.smap]; rw [smap]; try simp -@[simp] -theorem Term.smap_term_tapp {t1 t2} {σ : SubstVec [Term]} - : (tapp t1 t2)[σ,] = tapp t1[σ,] t2 -:= by simp only [SubstMap.smap]; rw [smap]; try simp +-- @[simp] +-- theorem Term.smap_term_lam {A t} {σ : SubstVec [Term]} +-- : (lam A t)[σ,] = lam A t[σ.lift [1],] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp -@[simp] -theorem Term.smap_term_tlam {t} {σ : SubstVec [Term]} - : (tlam t)[σ,] = tlam t[σ |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] -:= by simp only [SubstMap.smap]; rw [smap]; try simp +-- @[simp] +-- theorem Term.smap_term_tapp {t1 t2} {σ : SubstVec [Term]} +-- : (tapp t1 t2)[σ,] = tapp t1[σ,] t2 +-- := by simp only [SubstMap.smap]; rw [smap]; try simp -@[simp] -theorem Term.smap_term_zero {σ : SubstVec [Term]} : zero[σ,] = zero := by - simp only [SubstMap.smap]; rw [smap]; try simp +-- @[simp] +-- theorem Term.smap_term_tlam {t} {σ : SubstVec [Term]} +-- : (tlam t)[σ,] = tlam t[σ |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp -@[simp] -theorem Term.smap_term_succ {t} {σ : SubstVec [Term]} : (succ t)[σ,] = succ t[σ,] := by - simp only [SubstMap.smap]; rw [smap]; try simp +-- @[simp] +-- theorem Term.smap_term_zero {σ : SubstVec [Term]} : zero[σ,] = zero := by +-- simp only [SubstMap.smap]; rw [smap]; try simp -@[simp] -theorem Term.smap_term_nrec {m z s n} {σ : SubstVec [Term]} - : (nrec m z s n)[σ,] = nrec m z[σ,] s[σ |> .lift [2] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] n[σ,] -:= by simp only [SubstMap.smap]; rw [smap]; try simp +-- @[simp] +-- theorem Term.smap_term_succ {t} {σ : SubstVec [Term]} : (succ t)[σ,] = succ t[σ,] := by +-- simp only [SubstMap.smap]; rw [smap]; try simp -@[simp] -theorem Term.from_action_smap0 {t : Action Term} {σ : SubstVec [Term]} - : (from_action t)[σ,] = from_action t[σ,] -:= by cases t <;> simp [from_action] +-- @[simp] +-- theorem Term.smap_term_nrec {m z s n} {σ : SubstVec [Term]} +-- : (nrec m z s n)[σ,] = nrec m z[σ,] s[σ |> .lift [2] |> .ren Term [Ty] (𝐫1, .nil) 0 rfl,] n[σ,] +-- := by simp only [SubstMap.smap]; rw [smap]; try simp -instance : SubstSuffix Term [] := ⟨⟩ -instance : SubstMap Term [] where - smap _ := id +-- @[simp] +-- theorem Term.from_action_smap0 {t : Action Term} {σ : SubstVec [Term]} +-- : (from_action t)[σ,] = from_action t[σ,] +-- := by cases t <;> simp [from_action] -@[reducible, simp] -instance instSubstMapAll_Term : SubstMapAll [Term] := .cons .nil +-- instance : SubstSuffix Term [] := ⟨⟩ +-- instance : SubstMap Term [] where +-- smap _ := id -@[reducible, simp] -instance instSubstMapAll_Term_Ty : SubstMapAll [Term, Ty] := .cons instSubstMapAll_Ty +-- @[reducible, simp] +-- instance instSubstMapAll_Term : SubstMapAll [Term] := .cons .nil -instance : SubstMapEmpty Term where - apply_empty := by intro s; simp [SubstMap.smap] +-- @[reducible, simp] +-- instance instSubstMapAll_Term_Ty : SubstMapAll [Term, Ty] := .cons instSubstMapAll_Ty -instance : SubstMapVecDef Term Term [] where - apply_vecdef := by intro s σ; induction s generalizing σ <;> simp [*] +-- instance : SubstMapEmpty Term where +-- apply_empty := by intro s; simp [SubstMap.smap] --- The `[Ty]` Suffix: -instance : SuffixCommuteRenRen Term [Ty] where - ren_ren := by subst_solve_compose +-- instance : SubstMapVecDef Term Term [] where +-- apply_vecdef := by intro s σ; induction s generalizing σ <;> simp [*] -instance : SuffixCommuteRenSub Term [Ty] where - ren_sub := by subst_solve_compose +-- -- The `[Ty]` Suffix: +-- instance : SuffixCommuteRenRen Term [Ty] where +-- ren_ren := by subst_solve_compose -instance : SuffixCommuteSubRen Term [Ty] where - sub_ren := by subst_solve_compose +-- instance : SuffixCommuteRenSub Term [Ty] where +-- ren_sub := by subst_solve_compose -instance : SubstMapVecDef Term Term [Ty] where - apply_vecdef := by intro s σ; induction s generalizing σ <;> simp [*] +-- instance : SuffixCommuteSubRen Term [Ty] where +-- sub_ren := by subst_solve_compose -instance : SubstMapId Term [Ty] where - apply_id := by subst_solve_id +-- instance : SubstMapVecDef Term Term [Ty] where +-- apply_vecdef := by intro s σ; induction s generalizing σ <;> simp [*] -instance : SubstMapStable Term [Ty] where - apply_stable := by sorry --subst_solve_stable +-- instance : SubstMapId Term [Ty] where +-- apply_id := by subst_solve_id -instance : SubstMapRenComposeLeft Term [Ty] where - apply_ren_compose_left := by subst_solve_compose +-- instance : SubstMapStable Term [Ty] where +-- apply_stable := by sorry --subst_solve_stable -instance : SubstMapRenComposeRight Term [Ty] where - apply_ren_compose_right := by subst_solve_compose +-- instance : SubstMapRenComposeLeft Term [Ty] where +-- apply_ren_compose_left := by subst_solve_compose -instance : SubstMapCompose Term [Ty] where - apply_compose := by subst_solve_compose +-- instance : SubstMapRenComposeRight Term [Ty] where +-- apply_ren_compose_right := by subst_solve_compose --- The `[Term]` Singleton: -instance : SubstMapId Term [Term] where - apply_id := by subst_solve_id +-- instance : SubstMapCompose Term [Ty] where +-- apply_compose := by subst_solve_compose -instance : SubstMapStable Term [Term] where - apply_stable := by sorry --subst_solve_stable +-- -- The `[Term]` Singleton: +-- instance : SubstMapId Term [Term] where +-- apply_id := by subst_solve_id -instance : SubstMapRenComposeLeft Term [Term] where - apply_ren_compose_left := by subst_solve_compose +-- instance : SubstMapStable Term [Term] where +-- apply_stable := by sorry --subst_solve_stable -instance : SubstMapRenComposeRight Term [Term] where - apply_ren_compose_right := by subst_solve_compose +-- instance : SubstMapRenComposeLeft Term [Term] where +-- apply_ren_compose_left := by subst_solve_compose -instance : SubstMapCompose Term [Term] where - apply_compose := by subst_solve_compose +-- instance : SubstMapRenComposeRight Term [Term] where +-- apply_ren_compose_right := by subst_solve_compose --- The `[Term, Ty]` Original: -instance : SubstMapId Term [Term, Ty] where - apply_id := by subst_solve_id +-- instance : SubstMapCompose Term [Term] where +-- apply_compose := by subst_solve_compose -instance : SubstMapStable Term [Term, Ty] where - apply_stable := by sorry --subst_solve_stable +-- -- The `[Term, Ty]` Original: +-- instance : SubstMapId Term [Term, Ty] where +-- apply_id := by subst_solve_id -instance : SubstMapRenComposeLeft Term [Term, Ty] where - apply_ren_compose_left := by subst_solve_compose +-- instance : SubstMapStable Term [Term, Ty] where +-- apply_stable := by sorry --subst_solve_stable -instance : SubstMapRenComposeRight Term [Term, Ty] where - apply_ren_compose_right := by subst_solve_compose +-- instance : SubstMapRenComposeLeft Term [Term, Ty] where +-- apply_ren_compose_left := by subst_solve_compose -instance : SubstMapCompose Term [Term, Ty] where - apply_compose := by subst_solve_compose +-- instance : SubstMapRenComposeRight Term [Term, Ty] where +-- apply_ren_compose_right := by subst_solve_compose + +-- instance : SubstMapCompose Term [Term, Ty] where +-- apply_compose := by subst_solve_compose end SystemFWithNat diff --git a/LeanSubst/Automation/Basic.lean b/LeanSubst/Automation/Basic.lean index a0cc82d..5da3292 100644 --- a/LeanSubst/Automation/Basic.lean +++ b/LeanSubst/Automation/Basic.lean @@ -376,20 +376,24 @@ namespace Automation let lifts ← tys.mapM $ getLiftsOfTy data xs let optionLifts := lifts.map (fun stx : Term ↦ if BEq.beq stx $ Syntax.mkNatLit 0 then none else some stx) -- Check if all lifts are syntactically just 0 - if optionLifts.all (fun | .none => true | .some _ => false) then + if optionLifts.all Option.isNone then pure none else let tysNamesGlobal ← tys.mapM toGlobal let zipped := tysNamesGlobal.zip optionLifts - let rens : List $ Term ← mapEachSuffix zipped (fun zippedSfx ↦ do + let rens : List $ Option Term ← mapEachSuffix zipped (fun zippedSfx ↦ do let ⟨tys, optionLifts⟩ := zippedSfx.unzip - let lifts ← zippedSfx.tail.mapM (fun | ⟨ty, .none⟩ => `(Ren.id $(mkIdent ty)) | ⟨ty, .some n⟩ => `(Ren.add $(mkIdent ty) $n)) - let tysHd := mkIdent tys.head! - let tysTail := (tys.tail!.map mkIdent).toArray - let i := Syntax.mkNatLit $ numTotalTys - tys.length -- shadowing is bad, kids - `(.ren $tysHd [$tysTail,*] ⟨$lifts.toArray,*, .nil⟩ $i rfl) + if optionLifts.tail.all Option.isNone then + pure none + else + let lifts ← zippedSfx.tail.mapM (fun | ⟨ty, .none⟩ => `(Ren.id $(mkIdent ty)) | ⟨ty, .some n⟩ => `(Ren.add $(mkIdent ty) $n)) + let tysHd := mkIdent tys.head! + let tysTail := (tys.tail!.map mkIdent).toArray + let i := Syntax.mkNatLit $ numTotalTys - tys.length -- shadowing is bad, kids + pure $ some $ ← `(.ren $tysHd [$tysTail,*] ⟨$lifts.toArray,*, .nil⟩ $i rfl) ) let rens := rens.reverse.tail.reverse -- dropLast + let rens ← (rens.filter (Option.isSome)).mapM (fun | .none => `(0) | .some t => pure t) let liftsTm ← `([$lifts.toArray,*]) pure $ some ⟨liftsTm, rens⟩ | _ => pure none