From 4a0e19111cfd1f3d4926ab21b5ee1eba12d9baa8 Mon Sep 17 00:00:00 2001 From: Andrew Marmaduke Date: Fri, 4 Sep 2026 23:26:56 -0500 Subject: [PATCH] all the examples --- Examples.lean | 6 +- Examples/STLC.lean | 2 + Examples/STLC/Normalization.lean | 139 +++ Examples/STLC/Term.lean | 201 ++-- Examples/STLC/Theory.lean | 111 ++ Examples/Symbolic.lean | 2 + Examples/Symbolic/Term.lean | 147 +++ Examples/SystemFCallByValue.lean | 2 + Examples/SystemFCallByValue/Term.lean | 1011 ++++++++++++++++++ Examples/SystemFWithNat/Term.lean | 1403 +++++++++++++------------ LeanSubst/Misc.lean | 145 +-- LeanSubst/Rewriting/Normal.lean | 236 ++--- LeanSubst/Rewriting/Reduction.lean | 647 ++++++------ 13 files changed, 2737 insertions(+), 1315 deletions(-) create mode 100644 Examples/STLC/Normalization.lean create mode 100644 Examples/STLC/Theory.lean create mode 100644 Examples/Symbolic.lean create mode 100644 Examples/Symbolic/Term.lean create mode 100644 Examples/SystemFCallByValue.lean create mode 100644 Examples/SystemFCallByValue/Term.lean diff --git a/Examples.lean b/Examples.lean index d42ad1d..86321df 100644 --- a/Examples.lean +++ b/Examples.lean @@ -1,8 +1,10 @@ -import Examples.CCOmegaVarSorted import Examples.STLC -import Examples.SystemFWithNat import Examples.VariadicSTLC +import Examples.SystemFWithNat +import Examples.SystemFCallByValue +import Examples.Symbolic +import Examples.CCOmegaVarSorted def main : IO Unit := IO.println s!"Examples Build" diff --git a/Examples/STLC.lean b/Examples/STLC.lean index 3e6f6b4..3245ecf 100644 --- a/Examples/STLC.lean +++ b/Examples/STLC.lean @@ -1,2 +1,4 @@ import Examples.STLC.Term +import Examples.STLC.Theory +import Examples.STLC.Normalization diff --git a/Examples/STLC/Normalization.lean b/Examples/STLC/Normalization.lean new file mode 100644 index 0000000..cd5697b --- /dev/null +++ b/Examples/STLC/Normalization.lean @@ -0,0 +1,139 @@ + +import Examples.STLC.Theory +open LeanSubst + +namespace STLC + +universe u + +def Set (A : Sort u) := A -> Prop + +def ℛ (S : Set Term) : Set Term +| t => ∀ (r:Ren Term), S t⟨r⟩ + +@[simp] +def is_lam : Term -> Bool +| .lam _ _ => true +| _ => false + +inductive ℒ (S : Set Term) : Set Term where +| lift {t : Term} : + (is_lam t -> ℛ S t) -> + (∀ {t' : Term}, Red t t' -> ℒ S t') -> + ℒ S t + +def LR : Ty -> Set Term +| .base, t => SN Red t +| .arrow A B, .lam _ t => ∀ a, ℒ (LR A) a -> ℒ (LR B) t[su a::𝐬0] +| _, _ => False + +def ℰ A := ℒ (LR A) + +def 𝒞 (Γ : List Ty) (σ : Subst Term) : Prop := + ∀ {i : Nat} {T}, Γ[i]? = .some T -> ℰ T (σ.act i) + +@[simp] +def SemanticTyping (Γ : List Ty) (t : Term) (A : Ty) := + ∀ (σ : Subst Term), 𝒞 Γ σ -> ℰ A t[σ] + +notation:170 Γ:170 " ⊨ " t:170 " : " A:170 => SemanticTyping Γ t A + +theorem ℒ.sound {A t} : ℒ A t -> SN Red t +| .lift _ j => SN.sn (λ _ h => (j h).sound) + +theorem ℒ.preservation {A t t'} : ℒ A t -> Red t t' -> ℒ A t' +| .lift _ j, d => j d + +theorem ℒ.var A x : ℒ A #x := ℒ.lift (by simp) (λ r => by cases r) + +theorem is_lam_rename {r : Ren Term} : {t : Term} -> is_lam t <-> is_lam t⟨r⟩ +| .var x => by simp +| .lam A t => by simp +| .app f a => by simp + +theorem ℒ.rename {A t} (r : Ren Term) : ℒ A t -> ℒ A t⟨r⟩ +| .lift (t := t') j1 j2 => + have lem1 (h : is_lam t'⟨r⟩) : ℛ A t'⟨r⟩ := λ k => j1 (is_lam_rename.2 h) (r >> k) |> cast (by simp) + have lem2 {t''} (d : Red t'⟨r⟩ t'') : ℒ A t'' := + have ⟨z, d', e⟩ := d.antirename + (j2 d').rename r |> cast (by simp [e]) + .lift lem1 lem2 + +theorem ℛ.lam_mp {A B C b} : ℛ (LR $ A -:> B) (λ[C] b) -> ∀ (r:Ren Term) a, ℰ A a -> ℰ B b[su a::r.to] +| j1, r, a, j2 => j1 r a j2 |> cast (by simp [ℰ]) + +theorem ℛ.lam_mpr {A B C b} : (∀ (r:Ren Term) a, ℰ A a -> ℰ B b[su a::r.to]) -> ℛ (LR $ A -:> B) (λ[C] b) +| j1, r, a, j2 => j1 r a j2 |> cast (by simp [ℰ]) + +theorem ℛ.lam {A B C b} : ℛ (LR $ A -:> B) (λ[C] b) <-> ∀ (r:Ren Term) a, ℰ A a -> ℰ B b[su a::r.to] := + ⟨lam_mp, lam_mpr⟩ + +theorem 𝒞.su {Γ A t σ} : ℰ A t -> 𝒞 Γ σ -> 𝒞 (A::Γ) (su t::σ) +| j1, _, 0, _, _ => j1 |> cast (by simp_all) +| _, j2, _ + 1, _, h => j2 h + +theorem 𝒞.re {Γ σ} A x : 𝒞 Γ σ -> 𝒞 (A::Γ) (re x::σ) +| _, 0, _, _ => ℒ.var _ x +| j, _ + 1, _, h => j h + +theorem 𝒞.rename {Γ} {σ : Subst Term} (r : Ren Term) : 𝒞 Γ σ -> 𝒞 Γ (σ >> r) +| j, i, T, h => ℒ.rename r (j h) |> cast (by simp [ℰ]) + +theorem 𝒞.weaken {Γ σ} : 𝒞 Γ σ -> 𝒞 Γ (σ >> Ren.succ Term) := rename _ + +theorem 𝒞.lift A {Γ} {σ : Subst Term} : 𝒞 Γ σ -> 𝒞 (A::Γ) σ.lift +| h, i, T => re A 0 (weaken h) (i := i) (T := T) |> cast (by simp [Subst.rewrite_lift]) + +theorem ℰ.ind2 {A B s t} {P : Term -> Term -> Prop} + (ih : ∀ s t, + ℰ A s -> + ℰ B t -> + (∀ s', Red s s' -> P s' t) -> + (∀ t', Red t t' -> P s t') -> + P s t) + : ℰ A s -> ℰ B t -> P s t +:= by + intro j1 j2 + have j1' := j1 + have j2' := j2 + induction j1 generalizing t; case _ s' q1 q2 qih => + induction j2; case _ t' w1 w2 wih => + apply ih _ _ j1' j2' + intro s'' r; apply qih _ j2'; apply ℒ.preservation j1' r; apply j2'; apply r + intro t'' r; apply wih; apply r; apply ℒ.preservation j2' r + +theorem ℰ.lam {A B C b} : SN Red b -> ℛ (LR (A -:> B)) (λ[C] b) -> ℰ (A -:> B) (λ[C] b) +| .sn r, j => .lift (λ _ => j) (λ r' => + match r' with + | .lam (t' := b') r' => + have r'' a (k : Ren Term) : Red b[su a :: k.to] b'[su a :: k.to] := Red.subst r' + ℰ.lam (r _ r') (λ k a ah => ℒ.preservation (j k a ah) (r'' a k |> cast (by simp)))) + +theorem ℰ.app {A B f a} : ℰ (A -:> B) f -> ℰ A a -> ℰ B (.app f a) +| j1, j2 => + ind2 (P := λ f a => ℰ B (.app f a)) + (λ s t j1 j2 ih1 ih2 => ℒ.lift (by simp) (λ r => + match r with + | .beta => + match j1 with + | .lift j1 j3 => ℛ.lam.1 (j1 rfl) 𝐫0 _ j2 + | .app1 r => ih1 _ r + | .app2 r => ih2 _ r)) + j1 j2 + +theorem Typing.fundamental {Γ t A} : Γ ⊢ t : A -> Γ ⊨ t : A +| .var j, σ, h => h j +| .lam (A := A) (B := B) (t := t) tj, σ, h => + have norm : SN Red t[σ.lift] := ℒ.sound $ tj.fundamental σ.lift (𝒞.lift A h) + have body (r : Ren Term) (a : Term) (j : ℰ A a) : ℰ B t[σ.lift >> su a :: r.to] := by + simp [Subst.rewrite_lift, Subst.compose_compose_left_succ (T := Term)] + exact tj.fundamental (su a :: (σ >> r)) (𝒞.su j $ 𝒞.rename r h) + ℰ.lam norm (ℛ.lam.2 $ body |> cast (by simp)) +| .app fj aj, σ, h => ℰ.app (fj.fundamental σ h) (aj.fundamental σ h) + +theorem Typing.strong_normalization {Γ t A} (j : Γ ⊢ t : A) : SN Red t := + have lem : Γ ⊨ t : A := j.fundamental + have lem : ℰ A t := lem 𝐬0 (λ {i} {T} h => ℒ.var (LR T) i) |> cast (by simp) + ℒ.sound lem + +end STLC diff --git a/Examples/STLC/Term.lean b/Examples/STLC/Term.lean index 40a0417..2460cb5 100644 --- a/Examples/STLC/Term.lean +++ b/Examples/STLC/Term.lean @@ -7,7 +7,7 @@ namespace STLC inductive Ty where | base : Ty -| arrow : Ty -> Ty +| arrow : Ty -> Ty -> Ty notation "★" => Ty.base infixr:64 " -:> " => Ty.arrow @@ -20,145 +20,134 @@ inductive Term where prefix:max "#" => Term.var notation "λ[" A "]" t => Term.lam A t -#leansubst var Term.var -#leansubst bind Term at pos 1 in Term.lam +@[coe] +def Term.from_action : Action Term -> Term +| re y => var y +| su t => t -set_option diagnostics true +@[simp] +theorem Term.from_action_id {n} : from_action (𝐬0.act n) = var n := by + simp [from_action] -#leansubst generate Term +@[simp] +theorem Term.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by + simp [from_action] --- @[simp] --- instance : HSMul Term Term Term where --- hSMul := Term.app +@[simp] +theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] --- @[coe] --- def Term.from_action : Action Term -> Term --- | re y => var y --- | su t => t +@[simp] +theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] --- @[simp] --- theorem Term.from_action_id {n} : from_action (𝐬0.act n) = var n := by --- simp [from_action] +instance : Coe (Action Term) Term where + coe := Term.from_action --- @[simp] --- theorem Term.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by --- simp [from_action] +@[simp] +def Term.rmap (r : RenVec [Term]) : Term -> Term +| var x => var (r.1.act x) +| app t1 t2 => app (t1.rmap r) (t2.rmap r) +| λ[A] t => λ[A] t.rmap $ r.lift [1] --- @[simp] --- theorem Term.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] +instance : RenMap Term [Term] where + rmap := Term.rmap --- @[simp] --- theorem Term.from_action_su {t} : from_action (su t) = t := by simp [from_action] +instance : RenSuffix Term [] := ⟨⟩ +instance : RenMap Term [] where + rmap _ := id --- instance : Coe (Action Term) Term where --- coe := Term.from_action +@[simp] +theorem Term.rmap_empty {t : Term} {r : RenVec []} : t⟨r,⟩ = t := by + simp only [RenMap.rmap, id] --- @[simp] --- def Term.rmap (r : RenVec [Term]) : Term -> Term --- | var x => var (r.1.act x) --- | app t1 t2 => app (t1.rmap r) (t2.rmap r) --- | λ[A] t => λ[A] t.rmap $ r.lift [1] +@[reducible, simp] +instance instRenMapAll_Term : RenMapAll [Term] := .cons .nil --- instance : RenMap Term [Term] where --- rmap := Term.rmap +@[simp] +theorem Term.rmap_fix {r : RenVec [Term]} {t : Term} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] --- instance : RenSuffix Term [] := ⟨⟩ --- instance : RenMap Term [] where --- rmap _ := id +@[simp] +theorem Term.rmap_var {x} {r : RenVec [Term]} : (#x)⟨r,⟩ = .var (r.1.act x) := by + simp only [RenMap.rmap]; rw [rmap] --- @[simp] --- theorem Term.rmap_empty {t : Term} {r : RenVec []} : t⟨r,⟩ = t := by --- simp only [RenMap.rmap, id] +@[simp] +theorem Term.rmap_app {t1 t2 : Term} {r : RenVec [Term]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap] --- @[reducible, simp] --- instance instRenMapAll_Term : RenMapAll [Term] := .cons .nil +@[simp] +theorem Term.rmap_lam {A t} {r : RenVec [Term]} : (λ[A] t)⟨r,⟩ = λ[A] t⟨r.lift [1],⟩ := by + simp only [RenMap.rmap]; rw [rmap] --- @[simp] --- theorem Term.rmap_fix {r : RenVec [Term]} {t : Term} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] +@[simp] +theorem Term.from_action_rmap {t : Action Term} {r : RenVec [Term]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp --- @[simp] --- theorem Term.rmap_var {x} {r : RenVec [Term]} : (#x)⟨r,⟩ = .var (r.1.act x) := by --- simp only [RenMap.rmap]; rw [rmap] +instance : RenMapEmpty Term where + apply_empty := by intro s; simp --- @[simp] --- theorem Term.rmap_app {t1 t2 : Term} {r : RenVec [Term]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by --- simp only [RenMap.rmap]; rw [rmap] +instance : RenMapId Term [Term] where + apply_id := by subst_solve_id --- @[simp] --- theorem Term.rmap_lam {A t} {r : RenVec [Term]} : (λ[A] t)⟨r,⟩ = λ[A] t⟨r.lift [1],⟩ := by --- simp only [RenMap.rmap]; rw [rmap] +instance : RenMapCompose Term [Term] where + apply_compose := by subst_solve_compose --- @[simp] --- theorem Term.from_action_rmap {t : Action Term} {r : RenVec [Term]} --- : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ --- := by cases t <;> simp +@[simp] +def Term.smap (σ : SubstVec [Term]) : Term -> Term +| var x => σ.1.act x +| app t1 t2 => app (t1.smap σ) (t2.smap σ) +| λ[A] t => λ[A] t.smap $ σ.lift [1] --- instance : RenMapEmpty Term where --- apply_empty := by intro s; simp +instance : SubstMap Term [Term] where + smap := Term.smap --- instance : RenMapId Term [Term] where --- apply_id := by subst_solve_id +instance : SubstSuffix Term [] := ⟨⟩ +instance : SubstMap Term [] where + smap _ := id --- instance : RenMapCompose Term [Term] where --- apply_compose := by subst_solve_compose +@[simp] +theorem Term.smap_empty {t : Term} {σ : SubstVec []} : t[σ,] = t := by + simp only [SubstMap.smap, id] --- @[simp] --- def Term.smap (σ : SubstVec [Term]) : Term -> Term --- | var x => σ.1.act x --- | app t1 t2 => app (t1.smap σ) (t2.smap σ) --- | λ[A] t => λ[A] t.smap $ σ.lift [1] +@[reducible, simp] +instance instSubstMapAll_Ty : SubstMapAll [Term] := .cons .nil --- instance : SubstMap Term [Term] where --- smap := Term.smap +@[simp] +theorem Term.smap_fix {σ : SubstVec [Term]} {t : Term} : smap σ t = t[σ,] := by simp [SubstMap.smap] --- instance : SubstSuffix Term [] := ⟨⟩ --- instance : SubstMap Term [] where --- smap _ := id +@[simp] +theorem Term.smap_var {x} {σ : SubstVec [Term]} : (#x)[σ,] = from_action (σ.1.act x) := by + simp only [SubstMap.smap]; rw [smap] --- @[simp] --- theorem Term.smap_empty {t : Term} {σ : SubstVec []} : t[σ,] = t := by --- simp only [SubstMap.smap, id] +@[simp] +theorem Term.smap_app {t1 t2 : Term} {σ : SubstVec [Term]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by + simp only [SubstMap.smap]; rw [smap] --- @[reducible, simp] --- instance instSubstMapAll_Ty : SubstMapAll [Term] := .cons .nil +@[simp] +theorem Term.smap_lam {A t} {σ : SubstVec [Term]} : (λ[A] t)[σ,] = λ[A] t[σ.lift [1],] := by + simp only [SubstMap.smap]; rw [smap] --- @[simp] --- theorem Term.smap_fix {σ : SubstVec [Term]} {t : Term} : smap σ t = t[σ,] := by simp [SubstMap.smap] +@[simp] +theorem Term.from_action_smap {t : Action Term} {σ : SubstVec [Term]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp --- @[simp] --- theorem Term.smap_var {x} {σ : SubstVec [Term]} : (#x)[σ,] = from_action (σ.1.act x) := by --- simp only [SubstMap.smap]; rw [smap] +instance : SubstMapEmpty Term where + apply_empty := by intro s; simp --- @[simp] --- theorem Term.smap_app {t1 t2 : Term} {σ : SubstVec [Term]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by --- simp only [SubstMap.smap]; rw [smap] +instance : SubstMapId Term [Term] where + apply_id := by subst_solve_id --- @[simp] --- theorem Term.smap_lam {A t} {σ : SubstVec [Term]} : (λ[A] t)[σ,] = λ[A] t[σ.lift [1],] := by --- simp only [SubstMap.smap]; rw [smap] +instance : SubstMapStable Term [Term] where + apply_stable := by subst_solve_stable --- @[simp] --- theorem Term.from_action_smap {t : Action Term} {σ : SubstVec [Term]} --- : (from_action t)[σ,] = from_action t[σ,] --- := by cases t <;> simp +instance : SubstMapRenComposeLeft Term [Term] where + apply_ren_compose_left := by subst_solve_compose --- instance : SubstMapEmpty Term where --- apply_empty := by intro s; simp +instance : SubstMapRenComposeRight Term [Term] where + apply_ren_compose_right := by subst_solve_compose --- 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 : SubstMapCompose Term [Term] where --- apply_compose := by subst_solve_compose +instance : SubstMapCompose Term [Term] where + apply_compose := by subst_solve_compose end STLC diff --git a/Examples/STLC/Theory.lean b/Examples/STLC/Theory.lean new file mode 100644 index 0000000..c4a179b --- /dev/null +++ b/Examples/STLC/Theory.lean @@ -0,0 +1,111 @@ + +import Examples.STLC.Term +open LeanSubst + +namespace STLC + +inductive Red : Term -> Term -> Prop where +| beta {A b t} : Red (.app (λ[A] b) t) (b[su t::𝐬0]) +| app1 {f f' a} : Red f f' -> Red (.app f a) (.app f' a) +| app2 {a a' f} : Red a a' -> Red (.app f a) (.app f a') +| lam {A t t'} : Red t t' -> Red (λ[A] t) (λ[A] t') + +inductive Typing : List Ty -> Term -> Ty -> Prop where +| var {Γ x A} : + Γ[x]? = some A -> + Typing Γ #x A +| lam {Γ A B t} : + Typing (A::Γ) t B -> + Typing Γ (λ[A] t) (A -:> B) +| app {Γ A B f a} : + Typing Γ f (A -:> B) -> + Typing Γ a A -> + Typing Γ (.app f a) B + +notation:170 Γ:170 " ⊢ " t:170 " : " A:170 => Typing Γ t A + +structure TypingRen (r : Ren Term) (Γ Δ : List Ty) where + act : ∀ {x T}, Γ[x]? = some T -> Δ[r.act x]? = some T + +notation:35 Γ:35 " -⟨" r "⟩> " Δ:35 => TypingRen r Γ Δ + +theorem TypingRen.lift {Γ Δ : List Ty} A {r : Ren Term} (h : Γ -⟨r⟩> Δ) : A::Γ -⟨r.lift⟩> A::Δ := + ⟨λ {x} _ j => + match x with + | 0 => j + | _ + 1 => h.act j⟩ + +theorem TypingRen.id {X} : X -⟨.id Term⟩> X := ⟨λ h => h⟩ + +theorem TypingRen.succ {A X} : X -⟨.succ Term⟩> A::X := ⟨λ h => h⟩ + +theorem TypingRen.comp {X Y Z} {r1 r2 : Ren Term} : X -⟨r1⟩> Y -> Y -⟨r2⟩> Z -> X -⟨r1 >> r2⟩> Z := + λ j1 j2 => ⟨λ h => j2.act (j1.act h)⟩ + +theorem Typing.rename {Γ Δ t A} {r : Ren Term} (m : Γ -⟨r⟩> Δ) : Γ ⊢ t : A -> Δ ⊢ t⟨r⟩ : A +| var h => var (m.act h) +| app f a => app (f.rename m) (a.rename m) +| lam (A := C) t => lam (t.rename (m.lift C)) + +structure TypingSubst (σ : Subst Term) (Γ Δ : List Ty) where + act : ∀ {x : Nat} {T}, Γ[x]? = some T -> Δ ⊢ σ.act x : T + +notation:35 Γ:35 " -[" σ "]> " Δ:35 => TypingSubst σ Γ Δ + +theorem TypingSubst.succ {A X} : X -[.succ Term]> A::X := ⟨λ h => .var h⟩ + +theorem TypingSubst.re {Γ Δ A y σ} (j : Δ[y]? = some A) (m : Γ -[σ]> Δ) : A::Γ -[re y::σ]> Δ := + mk (λ {x} _ h => + match x with + | 0 => .var $ j |> cast (by simp at h; rw [h]) + | _ + 1 => m.act h) + +theorem TypingSubst.su {Γ Δ A a σ} (j : Δ ⊢ a : A) (m : Γ -[σ]> Δ) : A::Γ -[su a::σ]> Δ := + mk (λ {x} _ h => + match x with + | 0 => j |> cast (by simp; grind) + | _ + 1 => m.act h) + +theorem TypingSubst.lift {Γ Δ : List Ty} A {σ : Subst Term} (m : Γ -[σ]> Δ) : A::Γ -[σ.lift]> A::Δ := + ⟨λ {x} _ h => + match x with + | 0 => .var h + | _ + 1 => + let lem := Typing.rename (Δ := A::Δ) TypingRen.succ (m.act h) + by simp at lem; exact lem⟩ + +theorem Typing.subst {Γ Δ t A} {σ : Subst Term} (m : Γ -[σ]> Δ) : Γ ⊢ t : A -> Δ ⊢ t[σ] : A +| var h => m.act h +| app f a => app (f.subst m) (a.subst m) +| lam (A := C) t => lam (t.subst (m.lift C)) + +theorem Typing.beta {Γ A B b t} (j1 : (A::Γ) ⊢ b : B) (j2 : Γ ⊢ t : A) : Γ ⊢ b[su t::.id Term] : B := + Typing.subst + ⟨λ {x} _ h => + match x with + | 0 => j2 |> cast (by simp at *; rw [h]) + | _ + 1 => .var h⟩ + j1 + +theorem Red.subst {t t'} {σ : Subst Term} : Red t t' -> Red t[σ] t'[σ] +| @Red.beta A b t => @Red.beta A b[σ.lift] t[σ] |> cast (by simp [Subst.rewrite_lift]) +| .app1 r => .app1 r.subst +| .app2 r => .app2 r.subst +| .lam r => .lam r.subst + +theorem Red.antirename' {s' t : Term} (r : Ren Term) : Red s' t -> ∀ s, s' = s⟨r⟩ -> ∃ z, Red s z ∧ t = z⟨r⟩ +| @Red.beta A b t, .app (.lam A' b') t', h => ⟨b'[su t'::𝐬0], .beta, by simp_all⟩ +| .app1 (f := f) d, .app f' a', h => + have ⟨z, d', e⟩ := d.antirename' r f' (by simp_all) + ⟨.app z a', .app1 d', by simp_all⟩ +| .app2 (a := a) d, .app f' a', h => + have ⟨z, d', e⟩ := d.antirename' r a' (by simp_all) + ⟨.app f' z, .app2 d', by simp_all⟩ +| .lam (t := t) d, .lam A' t', h => + have ⟨z, d', e⟩ := d.antirename' r.lift t' (by simp_all) + ⟨.lam A' z, .lam d', by simp_all⟩ + +theorem Red.antirename {s t : Term} (r : Ren Term) (d : Red s⟨r⟩ t) : ∃ z, Red s z ∧ t = z⟨r⟩ := + Red.antirename' r d _ rfl + +end STLC diff --git a/Examples/Symbolic.lean b/Examples/Symbolic.lean new file mode 100644 index 0000000..730d8ac --- /dev/null +++ b/Examples/Symbolic.lean @@ -0,0 +1,2 @@ + +import Examples.Symbolic.Term diff --git a/Examples/Symbolic/Term.lean b/Examples/Symbolic/Term.lean new file mode 100644 index 0000000..1b44a44 --- /dev/null +++ b/Examples/Symbolic/Term.lean @@ -0,0 +1,147 @@ + +import LeanSubst +open LeanSubst + +namespace STLCWithData + +variable {V : Type} {B : V -> Nat -> Prop} {C : V -> Nat -> Prop} + +inductive Term (V : Type) (B : V -> Nat -> Prop) (C : V -> Nat -> Prop) where +| var : Nat -> Term V B C +| bind {n} (v : V) {h : B v n} (t : Term V B C) (ts : Fin n -> Term V B C) : Term V B C +| ctor {n} (v : V) {h : C v n} (ts : Fin n -> Term V B C) : Term V B C + +@[coe] +def Term.from_action : Action (Term V B C) -> (Term V B C) +| re y => var y +| su t => t + +@[simp] +theorem Term.from_action_id {n} : from_action (𝐬0.act n) = @var V B C n := by + simp [from_action] + +@[simp] +theorem Term.from_action_succ {n} : from_action (𝐬1.act n) = @var V B C (n + 1) := by + simp [from_action] + +@[simp] +theorem Term.from_acton_re {n} : from_action (re n) = @var V B C n := by simp [from_action] + +@[simp] +theorem Term.from_action_su {t : Term V B C} : from_action (su t) = t := by simp [from_action] + +instance : Coe (Action $ Term V B C) (Term V B C) where + coe := Term.from_action + +@[simp] +def Term.rmap (r : RenVec [Term V B C]) : Term V B C -> Term V B C +| var x => var (r.1.act x) +| bind (h := h) v t ts => bind (h := h) v (t.rmap $ r.lift [1]) (λ i => (ts i).rmap r) +| ctor (h := h) v ts => ctor (h := h) v (λ i => (ts i).rmap r) + +instance : RenMap (Term V B C) [Term V B C] where + rmap := Term.rmap + +instance : RenSuffix (Term V B C) [] := ⟨⟩ +instance : RenMap (Term V B C) [] where + rmap _ := id + +@[simp] +theorem Term.rmap_empty {t : Term V B C} {r : RenVec []} : t⟨r,⟩ = t := by + simp only [RenMap.rmap, id] + +@[reducible, simp] +instance instRenMapAll_Term : RenMapAll [Term V B C] := .cons .nil + +@[simp] +theorem Term.rmap_fix {r : RenVec [Term V B C]} {t : Term V B C} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] + +@[simp] +theorem Term.rmap_var {x} {r : RenVec [Term V B C]} : (@var V B C x)⟨r,⟩ = .var (r.1.act x) := by + simp only [RenMap.rmap]; rw [rmap] + +@[simp] +theorem Term.rmap_ctor {n} {v} {h : C v n} {ts : Fin n -> Term V B C} {r : RenVec [Term V B C]} : + (ctor (h := h) v ts)⟨r,⟩ = ctor (h := h) v (λ i => (ts i)⟨r,⟩) +:= by simp only [RenMap.rmap]; rw [rmap] + +@[simp] +theorem Term.rmap_bind {n} {v} {h : B v n} {t : Term V B C} {ts : Fin n -> Term V B C} {r : RenVec [Term V B C]} : + (bind (h := h) v t ts)⟨r,⟩ = bind (h := h) v t⟨r.lift [1],⟩ (λ i => (ts i)⟨r,⟩) +:= by simp only [RenMap.rmap]; rw [rmap] + +@[simp] +theorem Term.from_action_rmap {t : Action $ Term V B C} {r : RenVec [Term V B C]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp + +instance : RenMapEmpty $ Term V B C where + apply_empty := by intro s; simp + +instance : RenMapId (Term V B C) [Term V B C] where + apply_id := by subst_solve_id + +instance : RenMapCompose (Term V B C) [Term V B C] where + apply_compose := by subst_solve_compose + +@[simp] +def Term.smap (σ : SubstVec [Term V B C]) : Term V B C -> Term V B C +| var x => σ.1.act x +| bind (h := h) v t ts => bind (h := h) v (t.smap $ σ.lift [1]) (λ i => (ts i).smap σ) +| ctor (h := h) v ts => ctor (h := h) v (λ i => (ts i).smap σ) + +instance : SubstMap (Term V B C) [Term V B C] where + smap := Term.smap + +instance : SubstSuffix (Term V B C) [] := ⟨⟩ +instance : SubstMap (Term V B C) [] where + smap _ := id + +@[simp] +theorem Term.smap_empty {t : Term V B C} {σ : SubstVec []} : t[σ,] = t := by + simp only [SubstMap.smap, id] + +@[reducible, simp] +instance instSubstMapAll_Ty : SubstMapAll [Term V B C] := .cons .nil + +@[simp] +theorem Term.smap_fix {σ : SubstVec [Term V B C]} {t : Term V B C} : smap σ t = t[σ,] := by simp [SubstMap.smap] + +@[simp] +theorem Term.smap_var {x} {σ : SubstVec [Term V B C]} : (@var V B C x)[σ,] = σ.1.act x := by + simp only [SubstMap.smap]; rw [smap] + +@[simp] +theorem Term.smap_ctor {n} {v} {h : C v n} {ts : Fin n -> Term V B C} {σ : SubstVec [Term V B C]} : + (ctor (h := h) v ts)[σ,] = ctor (h := h) v (λ i => (ts i)[σ,]) +:= by simp only [SubstMap.smap]; rw [smap] + +@[simp] +theorem Term.smap_bind {n} {v} {h : B v n} {t : Term V B C} {ts : Fin n -> Term V B C} {σ : SubstVec [Term V B C]} : + (bind (h := h) v t ts)[σ,] = bind (h := h) v t[σ.lift [1],] (λ i => (ts i)[σ,]) +:= by simp only [SubstMap.smap]; rw [smap] + +@[simp] +theorem Term.from_action_smap {t : Action (Term V B C)} {σ : SubstVec [Term V B C]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp + +instance : SubstMapEmpty (Term V B C) where + apply_empty := by intro s; simp + +instance : SubstMapId (Term V B C) [Term V B C] where + apply_id := by subst_solve_id + +instance : SubstMapStable (Term V B C) [Term V B C] where + apply_stable := by subst_solve_stable + +instance : SubstMapRenComposeLeft (Term V B C) [Term V B C] where + apply_ren_compose_left := by subst_solve_compose + +instance : SubstMapRenComposeRight (Term V B C) [Term V B C] where + apply_ren_compose_right := by subst_solve_compose + +instance : SubstMapCompose (Term V B C) [Term V B C] where + apply_compose := by subst_solve_compose + +end STLCWithData diff --git a/Examples/SystemFCallByValue.lean b/Examples/SystemFCallByValue.lean new file mode 100644 index 0000000..ece7877 --- /dev/null +++ b/Examples/SystemFCallByValue.lean @@ -0,0 +1,2 @@ + +import Examples.SystemFCallByValue.Term diff --git a/Examples/SystemFCallByValue/Term.lean b/Examples/SystemFCallByValue/Term.lean new file mode 100644 index 0000000..728ad2a --- /dev/null +++ b/Examples/SystemFCallByValue/Term.lean @@ -0,0 +1,1011 @@ +import LeanSubst +import LeanSubst.Automation.Basic + +open LeanSubst + +namespace SystemFCallByValue + +inductive Ty where +| var : Nat -> Ty +| arrow : Ty -> Ty -> Ty +| all : Ty -> Ty +| nat : Ty + +#leansubst var Ty.var +#leansubst bind Ty at pos 0 in Ty.all +#leansubst generate Ty + +mutual +inductive Value where +| var (x : Nat) : Value +| lam (A : Ty) (t : Term) : Value +| tlam (t : Term) : Value + +inductive Term where +| val (v : Value) : Term +| app (f a : Term) : Term +| tapp (f : Term) (A : Ty) : Term +end + +@[coe] +def Value.from_action : Action Value -> Value +| re y => var y +| su t => t + +@[simp, grind =] +theorem Value.from_action_id {n} : from_action (𝐬0.act n) = var n := by + simp [from_action] + +@[simp, grind =] +theorem Value.from_action_succ {n} : from_action (𝐬1.act n) = var (n + 1) := by + simp [from_action] + +@[simp, grind =] +theorem Value.from_acton_re {n} : from_action (re n) = var n := by simp [from_action] + +@[simp, grind =] +theorem Value.from_action_su {t} : from_action (su t) = t := by simp [from_action] + +instance : Coe (Action Value) Value where + coe := Value.from_action + +mutual +@[simp] +def Value.rmap (r : RenVec [Value, Ty]) : Value -> Value +| .var x => .var (r.1.act x) +| .lam A t => .lam A⟨r.2.1⟩ (t.rmap $ r.lift [1, 0]) +| .tlam t => .tlam (t.rmap $ r.lift [0, 1]) + +@[simp] +def Term.rmap (r : RenVec [Value, Ty]) : Term -> Term +| .val v => .val (v.rmap r) +| .app f a => .app (f.rmap r) (a.rmap r) +| .tapp f A => .tapp (f.rmap r) A⟨r.2.1⟩ +end + +instance : RenMap Value [Value, Ty] where + rmap := Value.rmap + +instance : RenMap Term [Value, Ty] where + rmap := Term.rmap + +@[simp] +theorem Value.rmap_fix {r : RenVec [Value, Ty]} {t : Value} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] + +@[simp] +theorem Term.rmap_fix {r : RenVec [Value, Ty]} {t : Term} : rmap r t = t⟨r,⟩ := by simp [RenMap.rmap] + +@[simp] +theorem Value.rmap_term_ty_var {x} {r : RenVec [Value, Ty]} : (var x)⟨r,⟩ = var (r.1.act x) := rfl + +@[simp] +theorem Term.rmap_term_ty_app {t1 t2} {r : RenVec [Value, Ty]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap] + +@[simp] +theorem Value.rmap_term_ty_lam {A t} {r : RenVec [Value, 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 [Value, Ty]} + : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2⟨r.2.1⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Value.rmap_term_ty_tlam {t} {r : RenVec [Value, 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_val {t1} {r : RenVec [Value, Ty]} + : (val t1)⟨r,⟩ = val t1⟨r,⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +instance : RenSuffix Value [Ty] := ⟨⟩ +instance : RenMap Value [Ty] where + rmap r := Value.rmap (Ren.id Value, r.1, .nil) + +instance : RenSuffix Term [Ty] := ⟨⟩ +instance : RenMap Term [Ty] where + rmap r := Term.rmap (Ren.id Value, r.1, .nil) + +@[simp] +theorem Value.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 Value.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 Value.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_val {t1} {r : RenVec [Ty]} + : (val t1)⟨r,⟩ = val t1⟨r,⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +instance : RenMap Value [Value] where + rmap r := Value.rmap (r.1, Ren.id Ty, .nil) + +instance : RenMap Term [Value] where + rmap r := Term.rmap (r.1, Ren.id Ty, .nil) + +@[simp] +theorem Value.rmap_term_var {x} {r : RenVec [Value]} : (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 [Value]} : (app t1 t2)⟨r,⟩ = app t1⟨r,⟩ t2⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Value.rmap_term_lam {A t} {r : RenVec [Value]} + : (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 [Value]} + : (tapp t1 t2)⟨r,⟩ = tapp t1⟨r,⟩ t2 +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Value.rmap_term_tlam {t} {r : RenVec [Value]} : (tlam t)⟨r,⟩ = tlam t⟨r,⟩ := by + simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Term.rmap_term_val {t1} {r : RenVec [Value]} + : (val t1)⟨r,⟩ = val t1⟨r,⟩ +:= by simp only [RenMap.rmap]; rw [rmap]; try simp + +@[simp] +theorem Value.from_action_rmap {t : Action Value} {r : RenVec [Value, Ty]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp [from_action] + +@[simp] +theorem Value.from_action_rmap0 {t : Action Value} {r : RenVec [Value]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp [from_action] + +@[simp] +theorem Value.from_action_rmap1 {t : Action Value} {r : RenVec [Ty]} + : (from_action t)⟨r,⟩ = from_action t⟨r,⟩ +:= by cases t <;> simp [from_action] + +instance : RenSuffix Value [] := ⟨⟩ +instance : RenMap Value [] where + rmap _ := id + +instance : RenSuffix Term [] := ⟨⟩ +instance : RenMap Term [] where + rmap _ := id + +@[reducible, simp] +instance instRenMapAll_Value : RenMapAll [Value] := .cons .nil + +@[reducible, simp] +instance instRenMapAll_Value_Ty : RenMapAll [Value, Ty] := .cons instRenMapAll_Ty + +instance : RenMapEmpty Value where + apply_empty := by intro s; simp [RenMap.rmap] + +instance : RenMapEmpty Term where + apply_empty := by intro s; simp [RenMap.rmap] + +mutual + theorem Value.rmap_vecdef : ∀ {s : Value} {r : RenVec [Value, Ty]}, s⟨r,⟩ = s⟨r.2,⟩⟨r.1⟩ + | .var x, _ => by simp + | .lam A t, r => + have ih := t.rmap_vecdef (r := r.lift [1, 0]) + by simp [*] + | .tlam t, r => + have ih := t.rmap_vecdef (r := r.lift [0, 1]) + by simp [*] + + theorem Term.rmap_vecdef : ∀ {s : Term} {r : RenVec [Value, Ty]}, s⟨r,⟩ = s⟨r.2,⟩⟨r.1⟩ + | .val v, r => + have ih := v.rmap_vecdef (r := r) + by simp [*] + | .app f a, r => + have ih1 := f.rmap_vecdef (r := r) + have ih2 := a.rmap_vecdef (r := r) + by simp [*] + | .tapp f A, r => + have ih := f.rmap_vecdef (r := r) + by simp [*] +end + +instance : RenMapVecDef Value Value [Ty] where + apply_vecdef := Value.rmap_vecdef + +instance : RenMapVecDef Term Value [Ty] where + apply_vecdef := Term.rmap_vecdef + +mutual + @[simp] + theorem Value.rmap_id : ∀ {s : Value}, s⟨RenVec.id [Value, Ty],⟩ = s + | .var x => by simp + | .lam A t => + have ih := t.rmap_id + by simp [*] + | .tlam t => + have ih := t.rmap_id + by simp [*] + + @[simp] + theorem Term.rmap_id : ∀ {s : Term}, s⟨RenVec.id [Value, Ty],⟩ = s + | .val v => + have ih := v.rmap_id + by simp [*] + | .app f a => + have ih1 := f.rmap_id + have ih2 := a.rmap_id + by simp [*] + | .tapp f A => + have ih := f.rmap_id + by simp [*] +end + +instance : RenMapId Value [Value, Ty] where + apply_id := Value.rmap_id + +instance : RenMapId Term [Value, Ty] where + apply_id := Term.rmap_id + +mutual + @[simp] + theorem Value.rmap_compose : ∀ {s : Value} {r1 r2 : RenVec [Value, Ty]}, s⟨r1,⟩⟨r2,⟩ = s⟨r1 >> r2,⟩ + | .var x, _, _ => by simp + | .lam A t, r1, r2 => + have ih := t.rmap_compose (r1 := r1.lift [1, 0]) (r2 := r2.lift [1, 0]) + by simp [*] + | .tlam t, r1, r2 => + have ih := t.rmap_compose (r1 := r1.lift [0, 1]) (r2 := r2.lift [0, 1]) + by simp [*] + + @[simp] + theorem Term.rmap_compose : ∀ {s : Term} {r1 r2 : RenVec [Value, Ty]}, s⟨r1,⟩⟨r2,⟩ = s⟨r1 >> r2,⟩ + | .val v, r1, r2 => + have ih := v.rmap_compose (r1 := r1) (r2 := r2) + by simp [*] + | .app f a, r1, r2 => + have ih1 := f.rmap_compose (r1 := r1) (r2 := r2) + have ih2 := a.rmap_compose (r1 := r1) (r2 := r2) + by simp [*] + | .tapp f A, r1, r2 => + have ih := f.rmap_compose (r1 := r1) (r2 := r2) + by simp [*] +end + +instance : RenMapCompose Value [Value, Ty] where + apply_compose := Value.rmap_compose + +instance : RenMapCompose Term [Value, Ty] where + apply_compose := Term.rmap_compose + +instance : RenMapVecDef Value Value [] where + apply_vecdef := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapVecDef Term Value [] where + apply_vecdef := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapId Value [Value] where + apply_id := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapId Term [Value] where + apply_id := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapCompose Value [Value] where + apply_compose := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapCompose Term [Value] where + apply_compose := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapId Value [Ty] where + apply_id := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapId Term [Ty] where + apply_id := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapCompose Value [Ty] where + apply_compose := by intro s; simp only [RenMap.rmap]; simp + +instance : RenMapCompose Term [Ty] where + apply_compose := by intro s; simp only [RenMap.rmap]; simp + +mutual +@[simp] +def Value.smap (σ : SubstVec [Value, Ty]) : Value -> Value +| .var x => σ.1.act x +| .lam A t => .lam A[σ.2.1] (t.smap $ σ.lift [1, 0]) +| .tlam t => .tlam (t.smap $ σ |> .lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + +@[simp] +def Term.smap (σ : SubstVec [Value, Ty]) : Term -> Term +| .val v => .val (v.smap σ) +| .app f a => .app (f.smap σ) (a.smap σ) +| .tapp f A => .tapp (f.smap σ) A[σ.2.1] +end + +instance : SubstMap Value [Value, Ty] where + smap := Value.smap + +instance : SubstMap Term [Value, Ty] where + smap := Term.smap + +@[simp] +theorem Value.smap_fix {σ : SubstVec [Value, Ty]} {t : Value} : smap σ t = t[σ,] := by simp [SubstMap.smap] + +@[simp] +theorem Term.smap_fix {σ : SubstVec [Value, Ty]} {t : Term} : smap σ t = t[σ,] := by simp [SubstMap.smap] + +@[simp] +theorem Value.smap_term_ty_var {x} {σ : SubstVec [Value, Ty]} : (var x)[σ,] = σ.1.act x := rfl + +@[simp] +theorem Term.smap_term_ty_app {t1 t2} {σ : SubstVec [Value, Ty]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by + simp only [SubstMap.smap]; rw [smap] + +@[simp] +theorem Value.smap_term_ty_lam {A t} {σ : SubstVec [Value, 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 [Value, Ty]} + : (tapp t1 t2)[σ,] = tapp t1[σ,] t2[σ.2.1] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Value.smap_term_ty_tlam {t} {σ : SubstVec [Value, Ty]} : (tlam t)[σ,] = tlam t[σ |> .lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl,] := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_ty_val {t1} {σ : SubstVec [Value, Ty]} + : (val t1)[σ,] = val t1[σ,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +instance : SubstSuffix Value [Ty] := ⟨⟩ +instance : SubstMap Value [Ty] where + smap r := Value.smap (Subst.id Value, r.1, .nil) + +instance : SubstSuffix Term [Ty] := ⟨⟩ +instance : SubstMap Term [Ty] where + smap r := Term.smap (Subst.id Value, r.1, .nil) + +@[simp] +theorem Value.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 Value.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 Value.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_val {t1} {σ : SubstVec [Ty]} + : (val t1)[σ,] = val t1[σ,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +instance : SubstMap Value [Value] where + smap r := Value.smap (r.1, Subst.id Ty, .nil) + +instance : SubstMap Term [Value] where + smap r := Term.smap (r.1, Subst.id Ty, .nil) + +@[simp] +theorem Value.smap_term_var {x} {σ : SubstVec [Value]} : (var x)[σ,] = σ.1.act x := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_app {t1 t2} {σ : SubstVec [Value]} : (app t1 t2)[σ,] = app t1[σ,] t2[σ,] := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Value.smap_term_lam {A t} {σ : SubstVec [Value]} + : (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 [Value]} + : (tapp t1 t2)[σ,] = tapp t1[σ,] t2 +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Value.smap_term_tlam {t} {σ : SubstVec [Value]} : (tlam t)[σ,] = tlam t[σ |> .ren Value [Ty] (𝐫1, .nil) 0 rfl,] := by + simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Term.smap_term_val {t1} {σ : SubstVec [Value]} + : (val t1)[σ,] = val t1[σ,] +:= by simp only [SubstMap.smap]; rw [smap]; try simp + +@[simp] +theorem Value.from_action_smap {t : Action Value} {σ : SubstVec [Value, Ty]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp [from_action] + +@[simp] +theorem Value.from_action_smap0 {t : Action Value} {σ : SubstVec [Value]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp [from_action] + +@[simp] +theorem Value.from_action_smap1 {t : Action Value} {σ : SubstVec [Ty]} + : (from_action t)[σ,] = from_action t[σ,] +:= by cases t <;> simp [from_action] + +instance : SubstSuffix Value [] := ⟨⟩ +instance : SubstMap Value [] where + smap _ := id + +instance : SubstSuffix Term [] := ⟨⟩ +instance : SubstMap Term [] where + smap _ := id + +@[reducible, simp] +instance instSubstMapAll_Value : SubstMapAll [Value] := .cons .nil + +@[reducible, simp] +instance instSubstMapAll_Value_Ty : SubstMapAll [Value, Ty] := .cons instSubstMapAll_Ty + +instance : SubstMapEmpty Value where + apply_empty := by intro s; simp [SubstMap.smap] + +instance : SubstMapEmpty Term where + apply_empty := by intro s; simp [SubstMap.smap] + +mutual + @[grind =] + theorem Value.ren_ren : ∀ {s : Value} {r1 : Ren Value} {r2 : RenVec [Ty]}, s⟨r1⟩⟨r2,⟩ = s⟨r2,⟩⟨r1⟩ + | .var x, r1, r2 => by simp + | .lam A t, r1, r2 => + have ih := t.ren_ren (r1 := r1.lift) (r2 := r2) + by simp [*] + | .tlam t, r1, r2 => + have ih := t.ren_ren (r1 := r1) (r2 := r2.lift [1]) + by simp [*] + + @[grind =] + theorem Term.ren_ren : ∀ {s : Term} {r1 : Ren Value} {r2 : RenVec [Ty]}, s⟨r1⟩⟨r2,⟩ = s⟨r2,⟩⟨r1⟩ + | .val v, r1, r2 => + have ih := v.ren_ren (r1 := r1) (r2 := r2) + by simp [*] + | .app f a, r1, r2 => + have ih1 := f.ren_ren (r1 := r1) (r2 := r2) + have ih2 := a.ren_ren (r1 := r1) (r2 := r2) + by simp [*] + | .tapp f A, r1, r2 => + have ih1 := f.ren_ren (r1 := r1) (r2 := r2) + by simp [*] +end + +instance : SuffixCommuteRenRen Value [Ty] where + ren_ren := Value.ren_ren + +mutual + theorem Value.ren_sub : ∀ {s : Value} {r : Ren Value} {τ : SubstVec [Ty]}, s⟨r⟩[τ,] = s[τ,]⟨r⟩ + | .var x, r, τ => by simp + | .lam A t, r, τ => + have ih := t.ren_sub (r := r.lift) (τ := τ) + by simp [*] + | .tlam t, r, τ => + have ih := t.ren_sub (r := r) (τ := τ.lift [1]) + by simp [*] + + theorem Term.ren_sub : ∀ {s : Term} {r : Ren Value} {τ : SubstVec [Ty]}, s⟨r⟩[τ,] = s[τ,]⟨r⟩ + | .val v, r, τ => + have ih := v.ren_sub (r := r) (τ := τ) + by simp [*] + | .app f a, r, τ => + have ih1 := f.ren_sub (r := r) (τ := τ) + have ih2 := a.ren_sub (r := r) (τ := τ) + by simp [*] + | .tapp f A, r, τ => + have ih1 := f.ren_sub (r := r) (τ := τ) + by simp [*] +end + +instance : SuffixCommuteRenSub Value [Ty] where + ren_sub := Value.ren_sub + +mutual + theorem Value.smap_vecdef : ∀ {s : Value} {σ : SubstVec [Value, Ty]}, s[σ,] = s[σ.snd,][σ.fst] + | .var x, σ => by simp + | .lam A t, σ => + have ih := t.smap_vecdef (σ := σ.lift [1, 0]) + by simp [*] + | .tlam t, σ => + have ih := t.smap_vecdef (σ := σ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + by simp [*] + + theorem Term.smap_vecdef : ∀ {s : Term} {σ : SubstVec [Value, Ty]}, s[σ,] = s[σ.snd,][σ.fst] + | .val v, σ => + have ih := v.smap_vecdef (σ := σ) + by simp [*] + | .app f a, σ => + have ih1 := f.smap_vecdef (σ := σ) + have ih2 := a.smap_vecdef (σ := σ) + by simp [*] + | .tapp f A, σ => + have ih := f.smap_vecdef (σ := σ) + by simp [*] +end + +instance : SubstMapVecDef Value Value [Ty] where + apply_vecdef := Value.smap_vecdef + +instance : SubstMapVecDef Term Value [Ty] where + apply_vecdef := Term.smap_vecdef + +mutual + @[simp] + theorem Value.smap_id : ∀ {s : Value}, s[SubstVec.id [Ty],] = s + | .var x => by simp + | .lam A t => + have ih := t.smap_id + by simp [*] + | .tlam t => + have ih := t.smap_id + by simp [*] + + @[simp] + theorem Term.smap_id : ∀ {s : Term}, s[SubstVec.id [Ty],] = s + | .val v => + have ih := v.smap_id + by simp [*] + | .app f a => + have ih := f.smap_id + have ih := a.smap_id + by simp [*] + | .tapp f A => + have ih := f.smap_id + by simp [*] +end + +instance : SubstMapId Value [Value, Ty] where + apply_id := Value.smap_id + +instance : SubstMapId Term [Value, Ty] where + apply_id := Term.smap_id + +instance : SubstMapId Value [Value] where + apply_id := by intro s; simp only [SubstMap.smap]; simp + +instance : SubstMapId Term [Value] where + apply_id := by intro s; simp only [SubstMap.smap]; simp + +instance : SubstMapId Value [Ty] where + apply_id := by intro s; simp only [SubstMap.smap]; simp + +instance : SubstMapId Term [Ty] where + apply_id := by intro s; simp only [SubstMap.smap]; simp + +mutual + @[simp] + theorem Value.smap_ren_compose_left_ty : ∀ {s : Value} {r : RenVec [Ty]} {τ : SubstVec [Ty]}, s⟨r,⟩[τ,] = s[r >> τ,] + | .var x, r, τ => by simp + | .lam A t, r, τ => + have ih1 := t.smap_ren_compose_left_ty (r := r) (τ := τ) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + simp [*] at *; congr + } + | .tlam t, r, τ => + have ih := t.smap_ren_compose_left_ty + (r := r.lift [1]) + (τ := τ.lift [1]) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + simp at *; rw [ih] + } + + @[simp] + theorem Term.smap_ren_compose_left_ty : ∀ {s : Term} {r : RenVec [Ty]} {τ : SubstVec [Ty]}, s⟨r,⟩[τ,] = s[r >> τ,] + | .val v, r, τ => + have ih1 := v.smap_ren_compose_left_ty (r := r) (τ := τ) + by simp [*] + | .app f a, r, τ => + have ih1 := f.smap_ren_compose_left_ty (r := r) (τ := τ) + have ih2 := a.smap_ren_compose_left_ty (r := r) (τ := τ) + by simp [*] + | .tapp f A, r, τ => + have ih1 := f.smap_ren_compose_left_ty (r := r) (τ := τ) + by simp [*] +end + +instance : SubstMapRenComposeLeft Value [Ty] where + apply_ren_compose_left := Value.smap_ren_compose_left_ty + +instance : SubstMapRenComposeLeft Term [Ty] where + apply_ren_compose_left := Term.smap_ren_compose_left_ty + +mutual + @[simp] + theorem Value.smap_ren_compose_right_ty : ∀ {s : Value} {r : RenVec [Ty]} {σ : SubstVec [Ty]}, s[σ,]⟨r,⟩ = s[σ >> r,] + | .var x, r, σ => by simp + | .lam A t, r, σ => + have ih1 := t.smap_ren_compose_right_ty (r := r) (σ := σ) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases σ with ⟨σ1, σ2, _, _⟩ + simp [*] at *; congr + } + | .tlam t, r, σ => + have ih := t.smap_ren_compose_right_ty + (r := r.lift [1]) + (σ := σ.lift [1]) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases σ with ⟨σ1, σ2, _, _⟩ + simp at *; rw [ih] + } + + @[simp] + theorem Term.smap_ren_compose_right_ty : ∀ {s : Term} {r : RenVec [Ty]} {σ : SubstVec [Ty]}, s[σ,]⟨r,⟩ = s[σ >> r,] + | .val v, r, σ => + have ih1 := v.smap_ren_compose_right_ty (r := r) (σ := σ) + by simp [*] + | .app f a, r, σ => + have ih1 := f.smap_ren_compose_right_ty (r := r) (σ := σ) + have ih2 := a.smap_ren_compose_right_ty (r := r) (σ := σ) + by simp [*] + | .tapp f A, r, σ => + have ih1 := f.smap_ren_compose_right_ty (r := r) (σ := σ) + by simp [*] +end + +instance : SubstMapRenComposeRight Value [Ty] where + apply_ren_compose_right := Value.smap_ren_compose_right_ty + +instance : SubstMapRenComposeRight Term [Ty] where + apply_ren_compose_right := Term.smap_ren_compose_right_ty + +mutual + @[simp] + theorem Value.smap_compose_ty : ∀ {s : Value} {σ τ : SubstVec [Ty]}, s[σ,][τ,] = s[σ >> τ,] + | .var x, σ, τ => by simp + | .lam A t, σ, τ => + have ih1 := t.smap_compose_ty (σ := σ) (τ := τ) + by { + rcases σ with ⟨σ1, σ2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + try simp [Subst.rewrite_lift_compose (T := Value), *] + simp [*] at *; congr + } + | .tlam t, σ, τ => + have ih := t.smap_compose_ty (σ := σ.lift [1]) (τ := τ.lift [1]) + by { + rcases σ with ⟨σ1, σ2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + try simp [Subst.rewrite_lift_compose (T := Value), *] + simp at *; rw [ih] + } + + @[simp] + theorem Term.smap_compose_ty : ∀ {s : Term} {σ τ : SubstVec [Ty]}, s[σ,][τ,] = s[σ >> τ,] + | .val v, σ, τ => + have ih1 := v.smap_compose_ty (σ := σ) (τ := τ) + by simp [*] + | .app f a, σ, τ => + have ih1 := f.smap_compose_ty (σ := σ) (τ := τ) + have ih2 := a.smap_compose_ty (σ := σ) (τ := τ) + by simp [*] + | .tapp f A, σ, τ => + have ih1 := f.smap_compose_ty (σ := σ) (τ := τ) + by simp [*] +end + +instance : SubstMapCompose Value [Ty] where + apply_compose := Value.smap_compose_ty + +instance : SubstMapCompose Term [Ty] where + apply_compose := Term.smap_compose_ty + +mutual + @[simp] + theorem Value.smap_ren_compose_left_value : ∀ {s : Value} {r : RenVec [Value]} {τ : SubstVec [Value]}, s⟨r,⟩[τ,] = s[r >> τ,] + | .var x, r, τ => by simp + | .lam A t, r, τ => + have ih1 := t.smap_ren_compose_left_value (r := r.lift [1, 0]) (τ := τ.lift [1, 0]) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + simp [*] at *; congr + } + | .tlam t, r, τ => + have ih := t.smap_ren_compose_left_value + (r := r.lift [0, 1]) + (τ := τ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + simp at *; rw [ih] + } + + @[simp] + theorem Term.smap_ren_compose_left_value : ∀ {s : Term} {r : RenVec [Value]} {τ : SubstVec [Value]}, s⟨r,⟩[τ,] = s[r >> τ,] + | .val v, r, τ => + have ih1 := v.smap_ren_compose_left_value (r := r) (τ := τ) + by simp [*] + | .app f a, r, τ => + have ih1 := f.smap_ren_compose_left_value (r := r) (τ := τ) + have ih2 := a.smap_ren_compose_left_value (r := r) (τ := τ) + by simp [*] + | .tapp f A, r, τ => + have ih1 := f.smap_ren_compose_left_value (r := r) (τ := τ) + by simp [*] +end + +instance : SubstMapRenComposeLeft Value [Value] where + apply_ren_compose_left := Value.smap_ren_compose_left_value + +instance : SubstMapRenComposeLeft Term [Value] where + apply_ren_compose_left := Term.smap_ren_compose_left_value + +mutual + @[simp] + theorem Value.smap_ren_compose_right_value : ∀ {s : Value} {r : RenVec [Value]} {σ : SubstVec [Value]}, s[σ,]⟨r,⟩ = s[σ >> r,] + | .var x, r, σ => by simp; grind + | .lam A t, r, σ => + have ih1 := t.smap_ren_compose_right_value (r := r.lift [1, 0]) (σ := σ.lift [1, 0]) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases σ with ⟨σ1, σ2, _, _⟩ + simp [*] at *; congr + } + | .tlam t, r, σ => + have ih := t.smap_ren_compose_right_value + (r := r.lift [0, 1]) + (σ := σ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases σ with ⟨σ1, σ2, _, _⟩ + simp at *; rw [ih] + } + + @[simp] + theorem Term.smap_ren_compose_right_value : ∀ {s : Term} {r : RenVec [Value]} {σ : SubstVec [Value]}, s[σ,]⟨r,⟩ = s[σ >> r,] + | .val v, r, σ => + have ih1 := v.smap_ren_compose_right_value (r := r) (σ := σ) + by simp [*] + | .app f a, r, σ => + have ih1 := f.smap_ren_compose_right_value (r := r) (σ := σ) + have ih2 := a.smap_ren_compose_right_value (r := r) (σ := σ) + by simp [*] + | .tapp f A, r, σ => + have ih1 := f.smap_ren_compose_right_value (r := r) (σ := σ) + by simp [*] +end + +instance : SubstMapRenComposeRight Value [Value] where + apply_ren_compose_right := Value.smap_ren_compose_right_value + +instance : SubstMapRenComposeRight Term [Value] where + apply_ren_compose_right := Term.smap_ren_compose_right_value + +mutual + theorem Value.sub_ren : ∀ {s : Value} {σ : Subst Value} {r : RenVec [Ty]}, s[σ]⟨r,⟩ = s⟨r,⟩[σ⟨r,⟩] + | .var x, σ, r => by simp + | .lam A t, σ, r => + have ih := t.sub_ren (σ := σ.lift) (r := r) + by simp [*] + | .tlam t, σ, r => + have ih := t.sub_ren (σ := σ⟨𝐫1(Ty)⟩) (r := r.lift [1]) + by { + simp; rw [ih]; congr 2; simp + rcases r with ⟨r, _, _⟩; simp + grind + } + + theorem Term.sub_ren : ∀ {s : Term} {σ : Subst Value} {r : RenVec [Ty]}, s[σ]⟨r,⟩ = s⟨r,⟩[σ⟨r,⟩] + | .val v, σ, r => + have ih := v.sub_ren (σ := σ) (r := r) + by simp [*] + | .app f a, σ, r => + have ih1 := f.sub_ren (σ := σ) (r := r) + have ih2 := a.sub_ren (σ := σ) (r := r) + by simp [*] + | .tapp f A, σ, r => + have ih1 := f.sub_ren (σ := σ) (r := r) + by simp [*] +end + +instance : SuffixCommuteSubRen Value [Ty] where + sub_ren := Value.sub_ren + +mutual + @[simp] + theorem Value.smap_compose_value : ∀ {s : Value} {σ τ : SubstVec [Value]}, s[σ,][τ,] = s[σ >> τ,] + | .var x, σ, τ => by simp; grind + | .lam A t, σ, τ => + have ih1 := t.smap_compose_value (σ := σ.lift [1, 0]) (τ := τ.lift [1, 0]) + by { + rcases σ with ⟨σ1, σ2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + try simp [Subst.rewrite_lift_compose (T := Value), *] + simp [*] at *; congr + } + | .tlam t, σ, τ => + have ih := t.smap_compose_value + (σ := σ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + (τ := τ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + by { + rcases σ with ⟨σ1, σ2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + simp at *; rw [ih] + } + + @[simp] + theorem Term.smap_compose_value : ∀ {s : Term} {σ τ : SubstVec [Value]}, s[σ,][τ,] = s[σ >> τ,] + | .val v, σ, τ => + have ih1 := v.smap_compose_value (σ := σ) (τ := τ) + by simp [*] + | .app f a, σ, τ => + have ih1 := f.smap_compose_value (σ := σ) (τ := τ) + have ih2 := a.smap_compose_value (σ := σ) (τ := τ) + by simp [*] + | .tapp f A, σ, τ => + have ih1 := f.smap_compose_value (σ := σ) (τ := τ) + by simp [*] +end + +instance : SubstMapCompose Value [Value] where + apply_compose := Value.smap_compose_value + +instance : SubstMapCompose Term [Value] where + apply_compose := Term.smap_compose_value + +mutual + @[simp] + theorem Value.smap_ren_compose_left : ∀ {s : Value} {r : RenVec [Value, Ty]} {τ : SubstVec [Value, Ty]}, s⟨r,⟩[τ,] = s[r >> τ,] + | .var x, r, τ => by simp + | .lam A t, r, τ => + have ih1 := t.smap_ren_compose_left (r := r.lift [1, 0]) (τ := τ.lift [1, 0]) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + simp [*] at *; congr + } + | .tlam t, r, τ => + have ih := t.smap_ren_compose_left + (r := r.lift [0, 1]) + (τ := τ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + simp at *; rw [ih] + } + + @[simp] + theorem Term.smap_ren_compose_left : ∀ {s : Term} {r : RenVec [Value, Ty]} {τ : SubstVec [Value, Ty]}, s⟨r,⟩[τ,] = s[r >> τ,] + | .val v, r, τ => + have ih1 := v.smap_ren_compose_left (r := r) (τ := τ) + by simp [*] + | .app f a, r, τ => + have ih1 := f.smap_ren_compose_left (r := r) (τ := τ) + have ih2 := a.smap_ren_compose_left (r := r) (τ := τ) + by simp [*] + | .tapp f A, r, τ => + have ih1 := f.smap_ren_compose_left (r := r) (τ := τ) + by simp [*] +end + +instance : SubstMapRenComposeLeft Value [Value, Ty] where + apply_ren_compose_left := Value.smap_ren_compose_left + +instance : SubstMapRenComposeLeft Term [Value, Ty] where + apply_ren_compose_left := Term.smap_ren_compose_left + +mutual + @[simp] + theorem Value.smap_ren_compose_right : ∀ {s : Value} {r : RenVec [Value, Ty]} {σ : SubstVec [Value, Ty]}, s[σ,]⟨r,⟩ = s[σ >> r,] + | .var x, r, σ => by simp; grind + | .lam A t, r, σ => + have ih1 := t.smap_ren_compose_right (r := r.lift [1, 0]) (σ := σ.lift [1, 0]) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases σ with ⟨σ1, σ2, _, _⟩ + simp [*] at *; congr + } + | .tlam t, r, σ => + have ih := t.smap_ren_compose_right + (r := r.lift [0, 1]) + (σ := σ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + by { + rcases r with ⟨r1, r2, _, _⟩ + rcases σ with ⟨σ1, σ2, _, _⟩ + simp at *; rw [ih]; congr 1 + } + + @[simp] + theorem Term.smap_ren_compose_right : ∀ {s : Term} {r : RenVec [Value, Ty]} {σ : SubstVec [Value, Ty]}, s[σ,]⟨r,⟩ = s[σ >> r,] + | .val v, r, σ => + have ih1 := v.smap_ren_compose_right (r := r) (σ := σ) + by simp [*] + | .app f a, r, σ => + have ih1 := f.smap_ren_compose_right (r := r) (σ := σ) + have ih2 := a.smap_ren_compose_right (r := r) (σ := σ) + by simp [*] + | .tapp f A, r, σ => + have ih1 := f.smap_ren_compose_right (r := r) (σ := σ) + by simp [*] +end + +instance : SubstMapRenComposeRight Value [Value, Ty] where + apply_ren_compose_right := Value.smap_ren_compose_right + +instance : SubstMapRenComposeRight Term [Value, Ty] where + apply_ren_compose_right := Term.smap_ren_compose_right + +mutual + @[simp] + theorem Value.smap_compose : ∀ {s : Value} {σ τ : SubstVec [Value, Ty]}, s[σ,][τ,] = s[σ >> τ,] + | .var x, σ, τ => by simp; grind + | .lam A t, σ, τ => + have ih1 := t.smap_compose (σ := σ.lift [1, 0]) (τ := τ.lift [1, 0]) + by { + rcases σ with ⟨σ1, σ2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + try simp [Subst.rewrite_lift_compose (T := Value), *] + simp [*] at *; congr + } + | .tlam t, σ, τ => + have ih := t.smap_compose + (σ := σ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + (τ := τ.lift [0, 1] |> .ren Value [Ty] (𝐫1, .nil) 0 rfl) + by { + rcases σ with ⟨σ1, σ2, _, _⟩ + rcases τ with ⟨τ1, τ2, _, _⟩ + try simp [Subst.rewrite_lift_compose (T := Value), *] + simp at *; rw [ih]; congr 1 + } + + @[simp] + theorem Term.smap_compose : ∀ {s : Term} {σ τ : SubstVec [Value, Ty]}, s[σ,][τ,] = s[σ >> τ,] + | .val v, σ, τ => + have ih1 := v.smap_compose (σ := σ) (τ := τ) + by simp [*] + | .app f a, σ, τ => + have ih1 := f.smap_compose (σ := σ) (τ := τ) + have ih2 := a.smap_compose (σ := σ) (τ := τ) + by simp [*] + | .tapp f A, σ, τ => + have ih1 := f.smap_compose (σ := σ) (τ := τ) + by simp [*] +end + +instance : SubstMapCompose Value [Value, Ty] where + apply_compose := Value.smap_compose + +instance : SubstMapCompose Term [Value, Ty] where + apply_compose := Term.smap_compose + +end SystemFCallByValue diff --git a/Examples/SystemFWithNat/Term.lean b/Examples/SystemFWithNat/Term.lean index 891c22a..75445c4 100644 --- a/Examples/SystemFWithNat/Term.lean +++ b/Examples/SystemFWithNat/Term.lean @@ -12,6 +12,9 @@ inductive Ty where | all : Ty -> Ty | nat : Ty +#leansubst var Ty.var +#leansubst bind Ty at pos 0 in Ty.all + inductive Term where | var : Nat -> Term | app : Term -> Term -> Term @@ -22,8 +25,6 @@ inductive Term where | succ : Term -> Term | nrec (motive : Ty) (z : Term) (s : Term) (n : Term) : Term -- binds 2 Term's in s -#leansubst var Ty.var -#leansubst bind Ty at pos 0 in Ty.all #leansubst var Term.var #leansubst bind Term at pos 1 in Term.lam @@ -32,768 +33,768 @@ inductive Term where --set_option diagnostics true -#leansubst generate Ty, Term - --- Checking Ty -- -#print Ty.from_action -#print Ty.from_action_id -#print Ty.from_action_succ -#print Ty.from_action_re -#print Ty.from_action_su - -#check (inferInstance : Coe (Action Ty) Ty) - -#print Ty.rmap -#print Ty.rmap._f - -#check (inferInstance : RenMap Ty [Ty]) - -#print Ty.rmap_fix -#print Ty.rmap_empty -- should be removed - -#check (inferInstance : RenSuffix Ty []) -#check (inferInstance : RenMap Ty []) -#check (inferInstance : RenMapAll [Ty]) - -#print Ty.rmap_var -#print Ty.rmap_arrow -#print Ty.rmap_all -#print Ty.rmap_nat -#print Ty.from_action_rmap - -#check (inferInstance : RenMapEmpty Ty) -#check (inferInstance : RenMapId Ty [Ty]) -#check (inferInstance : RenMapCompose Ty [Ty]) - -#print Ty.smap -#print Ty.smap._f - -#check (inferInstance : SubstMap Ty [Ty]) - -#print Ty.smap_fix -#print Ty.smap_empty -- to be removed - -#check (inferInstance : SubstSuffix Ty []) -#check (inferInstance : SubstMap Ty []) -#check (inferInstance : SubstMapAll [Ty]) - -#print Ty.smap_var -#print Ty.smap_arrow -#print Ty.smap_all -#print Ty.smap_nat -#print Ty.from_action_smap - -#check (inferInstance : SubstMapEmpty Ty) -#check (inferInstance : SubstMapId Ty [Ty]) -#check (inferInstance : SubstMapStable Ty [Ty]) -#check (inferInstance : SubstMapRenComposeLeft Ty [Ty]) -#check (inferInstance : SubstMapRenComposeRight Ty [Ty]) -#check (inferInstance : SubstMapCompose Ty [Ty]) - --- Checking Term -- -#print Term.from_action -#print Term.from_action_id -#print Term.from_action_succ -#print Term.from_action_re -#print Term.from_action_su - -#check (inferInstance : Coe (Action Term) Term) - --- rmap -#print Term.rmap -#print Term.rmap._f - -#check (inferInstance : RenMap Term [Term, Ty]) -#check (inferInstance : RenSuffix Term [Ty]) -#check (inferInstance : RenMap Term [Ty]) -#check (inferInstance : RenMap Term [Term]) -#check (inferInstance : RenSuffix Term []) -#check (inferInstance : RenMap Term []) -#check (inferInstance : RenMapAll [Term]) -#check (inferInstance : RenMapAll [Term, Ty]) - -#print Term.rmap_empty -- to be removed -#print Term.rmap_fix - -#print Term.rmap_term_var -#print Term.rmap_term_app -#print Term.rmap_term_lam -#print Term.rmap_term_tapp -#print Term.rmap_term_tlam -#print Term.rmap_term_zero -#print Term.rmap_term_succ -#print Term.rmap_term_nrec - -#print Term.rmap_ty_var -#print Term.rmap_ty_app -#print Term.rmap_ty_lam -#print Term.rmap_ty_tapp -#print Term.rmap_ty_tlam -#print Term.rmap_ty_zero -#print Term.rmap_ty_succ -#print Term.rmap_ty_nrec - -#print Term.rmap_term_ty_var -#print Term.rmap_term_ty_app -#print Term.rmap_term_ty_lam -#print Term.rmap_term_ty_tapp -#print Term.rmap_term_ty_tlam -#print Term.rmap_term_ty_zero -#print Term.rmap_term_ty_succ -#print Term.rmap_term_ty_nrec - -#print Term.from_action_rmap -#print Term.from_action_rmap0 -#print Term.from_action_rmap1 - -#check (inferInstance : RenMapEmpty Term) -#check (inferInstance : RenMapVecDef Term Term [Ty]) -#check (inferInstance : RenMapId Term [Term, Ty]) -#check (inferInstance : RenMapCompose Term [Term, Ty]) -#check (inferInstance : RenMapVecDef Term Term []) -#check (inferInstance : RenMapId Term [Term]) -#check (inferInstance : RenMapCompose Term [Term]) -#check (inferInstance : RenMapId Term [Ty]) -#check (inferInstance : RenMapCompose Term [Ty]) - --- smap -#print Term.smap -#print Term.smap._f - -#check (inferInstance : SubstMap Term [Term, Ty]) -#check (inferInstance : SubstSuffix Term [Ty]) -#check (inferInstance : SubstMap Term [Ty]) -#check (inferInstance : SubstMap Term [Term]) -#check (inferInstance : SubstSuffix Term []) -#check (inferInstance : SubstMap Term []) -#check (inferInstance : SubstMapAll [Term]) -#check (inferInstance : SubstMapAll [Term, Ty]) - -#print Term.smap_empty -- remove -#print Term.smap_fix - -#print Term.smap_term_var -#print Term.smap_term_app -#print Term.smap_term_lam -#print Term.smap_term_tapp -#print Term.smap_term_tlam -#print Term.smap_term_zero -#print Term.smap_term_succ -#print Term.smap_term_nrec - -#print Term.smap_ty_var -#print Term.smap_ty_app -#print Term.smap_ty_lam -#print Term.smap_ty_tapp -#print Term.smap_ty_tlam -#print Term.smap_ty_zero -#print Term.smap_ty_succ -#print Term.smap_ty_nrec - -#print Term.smap_term_ty_var -#print Term.smap_term_ty_app -#print Term.smap_term_ty_lam -#print Term.smap_term_ty_tapp -#print Term.smap_term_ty_tlam -#print Term.smap_term_ty_zero -#print Term.smap_term_ty_succ -#print Term.smap_term_ty_nrec - -#print Term.from_action_smap -#print Term.from_action_smap0 -#print Term.from_action_smap1 - -#check (inferInstance : SuffixCommuteRenRen Term [Ty]) -#check (inferInstance : SuffixCommuteRenSub Term [Ty]) -#check (inferInstance : SuffixCommuteSubRen Term [Ty]) -#check (inferInstance : SubstMapEmpty Term) - -#check (inferInstance : SubstMapVecDef Term Term [Ty]) -#check (inferInstance : SubstMapId Term [Term, Ty]) -#check (inferInstance : SubstMapStable Term [Term, Ty]) -#check (inferInstance : SubstMapRenComposeLeft Term [Term, Ty]) -#check (inferInstance : SubstMapRenComposeRight Term [Term, Ty]) - -#check (inferInstance : SubstMapVecDef Term Term []) -#check (inferInstance : SubstMapId Term [Term]) -#check (inferInstance : SubstMapStable Term [Term]) -#check (inferInstance : SubstMapRenComposeLeft Term [Term]) -#check (inferInstance : SubstMapRenComposeRight Term [Term]) - -#check (inferInstance : SubstMapId Term [Ty]) -#check (inferInstance : SubstMapStable Term [Ty]) -#check (inferInstance : SubstMapRenComposeLeft Term [Ty]) -#check (inferInstance : SubstMapRenComposeRight Term [Ty]) - -#check (inferInstance : SubstMapCompose Term [Term, Ty]) -#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 - --- @[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_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] - --- 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] - --- 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] - --- instance : RenSuffix Ty [] := ⟨⟩ --- instance : RenMap Ty [] where --- rmap _ := id - --- @[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_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_all {t} {r : RenVec [Ty]} : (all t)⟨r,⟩ = all t⟨r.lift [1],⟩ := by --- simp only [RenMap.rmap]; rw [rmap] +-- #leansubst generate Ty, Term + +-- -- Checking Ty -- +-- #print Ty.from_action +-- #print Ty.from_action_id +-- #print Ty.from_action_succ +-- #print Ty.from_action_re +-- #print Ty.from_action_su + +-- #check (inferInstance : Coe (Action Ty) Ty) + +-- #print Ty.rmap +-- #print Ty.rmap._f + +-- #check (inferInstance : RenMap Ty [Ty]) + +-- #print Ty.rmap_fix +-- #print Ty.rmap_empty -- should be removed + +-- #check (inferInstance : RenSuffix Ty []) +-- #check (inferInstance : RenMap Ty []) +-- #check (inferInstance : RenMapAll [Ty]) + +-- #print Ty.rmap_var +-- #print Ty.rmap_arrow +-- #print Ty.rmap_all +-- #print Ty.rmap_nat +-- #print Ty.from_action_rmap + +-- #check (inferInstance : RenMapEmpty Ty) +-- #check (inferInstance : RenMapId Ty [Ty]) +-- #check (inferInstance : RenMapCompose Ty [Ty]) + +-- #print Ty.smap +-- #print Ty.smap._f + +-- #check (inferInstance : SubstMap Ty [Ty]) + +-- #print Ty.smap_fix +-- #print Ty.smap_empty -- to be removed + +-- #check (inferInstance : SubstSuffix Ty []) +-- #check (inferInstance : SubstMap Ty []) +-- #check (inferInstance : SubstMapAll [Ty]) + +-- #print Ty.smap_var +-- #print Ty.smap_arrow +-- #print Ty.smap_all +-- #print Ty.smap_nat +-- #print Ty.from_action_smap + +-- #check (inferInstance : SubstMapEmpty Ty) +-- #check (inferInstance : SubstMapId Ty [Ty]) +-- #check (inferInstance : SubstMapStable Ty [Ty]) +-- #check (inferInstance : SubstMapRenComposeLeft Ty [Ty]) +-- #check (inferInstance : SubstMapRenComposeRight Ty [Ty]) +-- #check (inferInstance : SubstMapCompose Ty [Ty]) + +-- -- Checking Term -- +-- #print Term.from_action +-- #print Term.from_action_id +-- #print Term.from_action_succ +-- #print Term.from_action_re +-- #print Term.from_action_su + +-- #check (inferInstance : Coe (Action Term) Term) + +-- -- rmap +-- #print Term.rmap +-- #print Term.rmap._f + +-- #check (inferInstance : RenMap Term [Term, Ty]) +-- #check (inferInstance : RenSuffix Term [Ty]) +-- #check (inferInstance : RenMap Term [Ty]) +-- #check (inferInstance : RenMap Term [Term]) +-- #check (inferInstance : RenSuffix Term []) +-- #check (inferInstance : RenMap Term []) +-- #check (inferInstance : RenMapAll [Term]) +-- #check (inferInstance : RenMapAll [Term, Ty]) + +-- #print Term.rmap_empty -- to be removed +-- #print Term.rmap_fix + +-- #print Term.rmap_term_var +-- #print Term.rmap_term_app +-- #print Term.rmap_term_lam +-- #print Term.rmap_term_tapp +-- #print Term.rmap_term_tlam +-- #print Term.rmap_term_zero +-- #print Term.rmap_term_succ +-- #print Term.rmap_term_nrec + +-- #print Term.rmap_ty_var +-- #print Term.rmap_ty_app +-- #print Term.rmap_ty_lam +-- #print Term.rmap_ty_tapp +-- #print Term.rmap_ty_tlam +-- #print Term.rmap_ty_zero +-- #print Term.rmap_ty_succ +-- #print Term.rmap_ty_nrec + +-- #print Term.rmap_term_ty_var +-- #print Term.rmap_term_ty_app +-- #print Term.rmap_term_ty_lam +-- #print Term.rmap_term_ty_tapp +-- #print Term.rmap_term_ty_tlam +-- #print Term.rmap_term_ty_zero +-- #print Term.rmap_term_ty_succ +-- #print Term.rmap_term_ty_nrec + +-- #print Term.from_action_rmap +-- #print Term.from_action_rmap0 +-- #print Term.from_action_rmap1 + +-- #check (inferInstance : RenMapEmpty Term) +-- #check (inferInstance : RenMapVecDef Term Term [Ty]) +-- #check (inferInstance : RenMapId Term [Term, Ty]) +-- #check (inferInstance : RenMapCompose Term [Term, Ty]) +-- #check (inferInstance : RenMapVecDef Term Term []) +-- #check (inferInstance : RenMapId Term [Term]) +-- #check (inferInstance : RenMapCompose Term [Term]) +-- #check (inferInstance : RenMapId Term [Ty]) +-- #check (inferInstance : RenMapCompose Term [Ty]) + +-- -- smap +-- #print Term.smap +-- #print Term.smap._f + +-- #check (inferInstance : SubstMap Term [Term, Ty]) +-- #check (inferInstance : SubstSuffix Term [Ty]) +-- #check (inferInstance : SubstMap Term [Ty]) +-- #check (inferInstance : SubstMap Term [Term]) +-- #check (inferInstance : SubstSuffix Term []) +-- #check (inferInstance : SubstMap Term []) +-- #check (inferInstance : SubstMapAll [Term]) +-- #check (inferInstance : SubstMapAll [Term, Ty]) + +-- #print Term.smap_empty -- remove +-- #print Term.smap_fix + +-- #print Term.smap_term_var +-- #print Term.smap_term_app +-- #print Term.smap_term_lam +-- #print Term.smap_term_tapp +-- #print Term.smap_term_tlam +-- #print Term.smap_term_zero +-- #print Term.smap_term_succ +-- #print Term.smap_term_nrec + +-- #print Term.smap_ty_var +-- #print Term.smap_ty_app +-- #print Term.smap_ty_lam +-- #print Term.smap_ty_tapp +-- #print Term.smap_ty_tlam +-- #print Term.smap_ty_zero +-- #print Term.smap_ty_succ +-- #print Term.smap_ty_nrec + +-- #print Term.smap_term_ty_var +-- #print Term.smap_term_ty_app +-- #print Term.smap_term_ty_lam +-- #print Term.smap_term_ty_tapp +-- #print Term.smap_term_ty_tlam +-- #print Term.smap_term_ty_zero +-- #print Term.smap_term_ty_succ +-- #print Term.smap_term_ty_nrec + +-- #print Term.from_action_smap +-- #print Term.from_action_smap0 +-- #print Term.from_action_smap1 + +-- #check (inferInstance : SuffixCommuteRenRen Term [Ty]) +-- #check (inferInstance : SuffixCommuteRenSub Term [Ty]) +-- #check (inferInstance : SuffixCommuteSubRen Term [Ty]) +-- #check (inferInstance : SubstMapEmpty Term) + +-- #check (inferInstance : SubstMapVecDef Term Term [Ty]) +-- #check (inferInstance : SubstMapId Term [Term, Ty]) +-- #check (inferInstance : SubstMapStable Term [Term, Ty]) +-- #check (inferInstance : SubstMapRenComposeLeft Term [Term, Ty]) +-- #check (inferInstance : SubstMapRenComposeRight Term [Term, Ty]) + +-- #check (inferInstance : SubstMapVecDef Term Term []) +-- #check (inferInstance : SubstMapId Term [Term]) +-- #check (inferInstance : SubstMapStable Term [Term]) +-- #check (inferInstance : SubstMapRenComposeLeft Term [Term]) +-- #check (inferInstance : SubstMapRenComposeRight Term [Term]) + +-- #check (inferInstance : SubstMapId Term [Ty]) +-- #check (inferInstance : SubstMapStable Term [Ty]) +-- #check (inferInstance : SubstMapRenComposeLeft Term [Ty]) +-- #check (inferInstance : SubstMapRenComposeRight Term [Ty]) + +-- #check (inferInstance : SubstMapCompose Term [Term, Ty]) +-- #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 + +@[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_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] + +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] + +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] + +instance : RenSuffix Ty [] := ⟨⟩ +instance : RenMap Ty [] where + rmap _ := id + +@[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_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_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 - --- instance : RenMapEmpty Ty where --- apply_empty := by intro s; 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 (σ : 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] +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 : 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 (σ : 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/LeanSubst/Misc.lean b/LeanSubst/Misc.lean index 183659f..415f793 100644 --- a/LeanSubst/Misc.lean +++ b/LeanSubst/Misc.lean @@ -26,7 +26,8 @@ theorem Subst.rewrite3_cons_ren_fix [RenMap T [T]] [SubstMap T [T]] {a} {σ : Su simp [cons, HAndThen.hAndThen, compose_ren_right] funext; case _ x => cases x; all_goals simp [act, SubstAction.act] - sorry + cases σ; case _ f => + simp [RenMap.rmap, rmap0] @[simp] theorem Subst.rewrite3_cons_ren_subst [SubstMap T [T]] {x} {σ : Subst T} {r : Ren T} @@ -55,14 +56,12 @@ 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 -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 - sorry - -- simp [HAndThen.hAndThen, AndThen.andThen, compose]; funext; case _ x => - -- generalize zdef : τ.act x = z - -- cases z <;> simp - -- rw [SubstMapStable.apply_stable]; simp [RenVec.to] +-- 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 [HAndThen.hAndThen, AndThen.andThen, compose]; funext; case _ x => +-- generalize zdef : τ.act x = z +-- cases z 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 @@ -219,7 +218,9 @@ theorem Subst.rewrite4_append_add_indirect {k} {σ : Subst T} {ℓ : List (Actio 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 - sorry + simp [Ren.lift, HAndThen.hAndThen, compose_ren_left, cons] + funext; case _ i => + cases i <;> simp @[simp] theorem Subst.compose_ren_left_cons_lift_k1 [RenMap T [T]] [SubstMap T [T]] {k} {a : Action T} {r : Ren T} {σ : Subst T} @@ -231,13 +232,13 @@ 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 >> σ) := by - induction ℓ generalizing r <;> simp [-Subst.rewrite_lift_k_ren, *] + induction ℓ generalizing r <;> 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 >> σ) -:= by - sorry +-- 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 >> σ) +-- := by +-- sorry --induction ℓ generalizing r <;> simp [-Subst.rewrite_lift_k_ren, *] @[simp] @@ -247,40 +248,49 @@ theorem Subst.compose_ren_right_append [RenMap T [T]] [SubstMap T [T]] {ℓ : Li induction ℓ generalizing σ r <;> simp case _ hd tl ih => rw [<-ih] +@[simp] theorem Subst.compose_ren_right_assoc [RenMap S [S]] [SubstMap S [S]] [SubstMapRenComposeLeft S [S]] {σ τ : Subst S} {r : Ren S} : (σ >> r) >> τ = σ >> r >> τ := by - sorry - -- simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_left, compose_ren_right] - -- funext; case _ i => - -- generalize zdef : σ.act i = z - -- cases z <;> simp - -- congr + simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_left, compose_ren_right] + funext; case _ i => + generalize zdef : σ.act i = z + cases z + case re i => + simp [SubstVec.compose_ren_left] + simp [HAndThen.hAndThen, compose_ren_left] + case su t => + simp [SubstVec.compose_ren_left] + simp [HAndThen.hAndThen, compose_ren_left] +@[simp] theorem Subst.compose_ren_right_assoc2 - [RenMapAll [S]] [SubstMap S [S]] [SubstMapRenComposeRight S [S]] + [RenMapAll [S]] [SubstMap S [S]] [RenMapVecDef S S []] [RenMapEmpty S] [SubstMapRenComposeRight S [S]] {σ τ : Subst S} {r : Ren S} : (σ >> τ) >> r = σ >> τ >> r := by - sorry - -- simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_right]; funext; case _ i => - -- generalize zdef : σ.act i = z - -- cases z <;> simp - -- congr - -- sorry + simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_right]; funext; case _ i => + generalize zdef : σ.act i = z + cases z + case re => + simp [SubstVec.compose_ren_right] + simp [HAndThen.hAndThen, compose_ren_right] + case su => + simp [SubstVec.compose_ren_right] + simp [HAndThen.hAndThen, compose_ren_right] -- 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; sorry - -theorem Subst.lift_of_succ_rev [RenMap S [S]] [RenMapCompose S [S]] {k} {σ : Subst S} : σ.lift (1 + k) = σ.lift.lift k := by - sorry +-- 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; 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 @@ -293,9 +303,9 @@ theorem Subst.lift_of_succ_rev [RenMap S [S]] [RenMapCompose S [S]] {k} {σ : Su -- · split <;> -- · simp [Ren.succ, Ren.add, Ren.compose_tuple, Ren.compose] ; grind -@[grind =] -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 - sorry +-- @[grind =] +-- 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 +-- sorry --induction a generalizing σ <;> grind [lift_of_succ_rev] -- @[simp] @@ -323,17 +333,28 @@ theorem Subst.ren_rewrite1_left {r : Ren T} : r >> id T = r.to := by -- {x : Action T} {τ : Subst T} {t : T} -- : t⟨Ren.succ T⟩[x :: τ] = t[τ] := by simp [compose_ren_left_tuple] +@[simp] +theorem Subst.compose_ren_right_from_to + [SubstMap T [T]] [RenMap T [T]] [SubstMapStable T [T]] + {σ : Subst T} {r : Ren T} : + σ >> r.to = σ >> r +:= by + simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_right] + funext; case _ i => + simp [Subst.act, SubstAction.act] + cases σ; case _ f => + simp [SubstMap.smap, RenMap.rmap, smap0, rmap0] + cases (f i) <;> simp + rw [SubstMapStable.apply_stable]; simp [RenVec.to] + +@[simp] theorem Subst.compose_compose_left_succ [RenMap T [T]] [RenMapId T [T]] [SubstMapAll [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] {x : Action T} {σ τ : Subst T} : (σ >> Ren.succ T) >> (x :: τ) = σ >> τ := by - sorry - -- simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_right] - -- congr ; funext n - -- generalize zdef : σ.act n = z - -- induction z <;> simp [HAndThen.hAndThen, SubstVec.compose_ren_left, compose_ren_left]; congr + simp [HAndThen.hAndThen, AndThen.andThen, compose, compose_ren_right]; congr theorem Subst.compose_left_cons_lift1_indirect [RenMap T [T]] [RenMapId T [T]] @@ -344,22 +365,22 @@ theorem Subst.compose_left_cons_lift1_indirect congr 1 exact compose_compose_left_succ -theorem Subst.compose_left_cons_lift_indirect {k} - [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] - [SubstMapAll [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] - {ℓ : List $ Action T} {σ τ : Subst T} {h : k = ℓ.length} - : σ.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]] - [SubstMapAll [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 - sorry - -- grind [compose_left_cons_lift_indirect] +-- theorem Subst.compose_left_cons_lift_indirect {k} +-- [RenMap T [T]] [RenMapId T [T]] [RenMapCompose T [T]] +-- [SubstMapAll [T]] [SubstMapCompose T [T]] [SubstMapRenComposeLeft T [T]] +-- {ℓ : List $ Action T} {σ τ : Subst T} {h : k = ℓ.length} +-- : σ.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]] +-- [SubstMapAll [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 +-- sorry +-- -- grind [compose_left_cons_lift_indirect] @[simp] theorem Subst.List.smap_append [SubstMap S V] {a b : List S} {σ : SubstVec V} diff --git a/LeanSubst/Rewriting/Normal.lean b/LeanSubst/Rewriting/Normal.lean index ad98306..a64effa 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 fd0ff94..5370bd7 100644 --- a/LeanSubst/Rewriting/Reduction.lean +++ b/LeanSubst/Rewriting/Reduction.lean @@ -1,329 +1,324 @@ 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 + 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