diff --git a/Foundation/FirstOrder/Basic/Calculus.lean b/Foundation/FirstOrder/Basic/Calculus.lean index 38a693b1..0e5022f2 100644 --- a/Foundation/FirstOrder/Basic/Calculus.lean +++ b/Foundation/FirstOrder/Basic/Calculus.lean @@ -36,69 +36,17 @@ namespace Derivation variable {T U : Theory L} {Δ Δ₁ Δ₂ Γ : Sequent L} {φ ψ r : SyntacticFormula L} open Rewriting LawfulSyntacticRewriting -/- -inductive CutRestricted (C : Set (SyntacticFormula L)) : {Δ : Sequent L} → ⊢ᵀ Δ → Prop -| axL (Δ) {k} (r : L.Rel k) (v) : CutRestricted C (axL Δ r v) -| verum (Δ) : CutRestricted C (verum Δ) -| or {Δ φ ψ} {d : ⊢ᵀ φ :: ψ :: Δ} : CutRestricted C d → CutRestricted C d.or -| and {Δ φ ψ} {dp : ⊢ᵀ φ :: Δ} {dq : ⊢ᵀ ψ :: Δ} : CutRestricted C dp → CutRestricted C dq → CutRestricted C (dp.and dq) -| all {Δ φ} {d : ⊢ᵀ Rewriting.free φ :: Δ⁺} : CutRestricted C d → CutRestricted C d.all -| ex {Δ φ} (t) {d : ⊢ᵀ φ/[t] :: Δ} : CutRestricted C d → CutRestricted C d.ex -| wk {Δ Γ} {d : ⊢ᵀ Δ} (ss : Δ ⊆ Γ) : CutRestricted C d → CutRestricted C (d.wk ss) -| cut {Δ φ} {dp : ⊢ᵀ φ :: Δ} {dn : ⊢ᵀ ∼φ :: Δ} : CutRestricted C dp → CutRestricted C dn → φ ∈ C → CutRestricted C (dp.cut dn) - -def CutFree {Δ : Sequent L} (d : ⊢ᵀ Δ) : Prop := CutRestricted ∅ d - -namespace CutRestricted -variable {C C' : Set (SyntacticFormula L)} {Δ Γ : Sequent L} {φ ψ : SyntacticFormula L} - -attribute [simp] CutRestricted.axL CutRestricted.verum - -@[simp] lemma or' {d : ⊢ᵀ φ :: ψ :: Δ} : CutRestricted C (Derivation.or d) ↔ CutRestricted C d := - ⟨by rintro ⟨⟩; assumption, CutRestricted.or⟩ - -@[simp] lemma and' {dp : ⊢ᵀ φ :: Δ} {dq : ⊢ᵀ ψ :: Δ} : - CutRestricted C (Derivation.and dp dq) ↔ CutRestricted C dp ∧ CutRestricted C dq := - ⟨by rintro ⟨⟩; constructor <;> assumption, by rintro ⟨dp, dq⟩; exact CutRestricted.and dp dq⟩ - -@[simp] lemma all' {φ} {d : ⊢ᵀ Rewriting.free φ :: Δ⁺} : CutRestricted C (Derivation.all d) ↔ CutRestricted C d := - ⟨by rintro ⟨⟩; assumption, CutRestricted.all⟩ - -@[simp] lemma ex' {φ} (t) {d : ⊢ᵀ φ/[t] :: Δ} : CutRestricted C (Derivation.ex t d) ↔ CutRestricted C d := - ⟨by rintro ⟨⟩; assumption, CutRestricted.ex t⟩ - -@[simp] lemma wk' {d : ⊢ᵀ Δ} {ss : Δ ⊆ Γ} : CutRestricted C (Derivation.wk d ss) ↔ CutRestricted C d := - ⟨by rintro ⟨⟩; assumption, CutRestricted.wk ss⟩ - -@[simp] lemma cut' {dp : ⊢ᵀ φ :: Δ} {dn : ⊢ᵀ ∼φ :: Δ} : - CutRestricted C (Derivation.cut dp dn) ↔ φ ∈ C ∧ CutRestricted C dp ∧ CutRestricted C dn := - ⟨by { rintro ⟨⟩; constructor; { assumption }; constructor <;> assumption }, - by rintro ⟨h, dp, dq⟩; exact CutRestricted.cut dp dq h⟩ - -lemma of_subset (d : ⊢ᵀ Δ) (ss : C ⊆ C') : CutRestricted C d → CutRestricted C' d := by - induction d <;> try simp [*] - case and _ _ _ _ ihp ihq => intro hp hq; exact ⟨ihp hp, ihq hq⟩ - case or _ _ _ _ ih => exact ih - case all _ _ _ _ ih => exact ih - case ex _ _ _ _ ih => exact ih - case wk _ _ _ _ ih => exact ih - case cut _ _ _ ihp ihn => - intro h hp hn; exact ⟨ss h, ihp hp, ihn hn⟩ - case root h => simp at h - -end CutRestricted --/ -def length : {Δ : Sequent L} → T ⟹ Δ → ℕ - | _, axL _ _ _ => 0 - | _, verum _ => 0 - | _, or d => d.length.succ - | _, and dp dq => (max (length dp) (length dq)).succ - | _, all d => d.length.succ - | _, ex _ d => d.length.succ - | _, wk d _ => d.length.succ - | _, cut dp dn => (max (length dp) (length dn)).succ - | _, root _ => 0 +def length {Δ : Sequent L} : T ⟹ Δ → ℕ + | axL _ _ _ => 0 + | verum _ => 0 + | or d => d.length.succ + | and dp dq => (max (length dp) (length dq)).succ + | all d => d.length.succ + | ex _ d => d.length.succ + | wk d _ => d.length.succ + | cut dp dn => (max (length dp) (length dn)).succ + | root _ => 0 section length @@ -126,42 +74,42 @@ end length section Repr variable [∀ k, ToString (L.Func k)] [∀ k, ToString (L.Rel k)] -protected unsafe def repr : {Δ : Sequent L} → T ⟹ Δ → String - | _, axL Δ _ _ => +protected unsafe def repr {Δ : Sequent L} : T ⟹ Δ → String + | axL Δ _ _ => "\\AxiomC{}\n" ++ "\\RightLabel{\\scriptsize(axL)}\n" ++ "\\UnaryInfC{$" ++ reprStr Δ ++ "$}\n\n" - | _, verum Δ => + | verum Δ => "\\AxiomC{}\n" ++ "\\RightLabel{\\scriptsize($\\top$)}\n" ++ "\\UnaryInfC{$" ++ reprStr Δ ++ "$}\n\n" - | _, @or _ _ Δ φ ψ d => + | @or _ _ Δ φ ψ d => Derivation.repr d ++ "\\RightLabel{\\scriptsize($\\lor$)}\n" ++ "\\UnaryInfC{$" ++ reprStr ((φ ⋎ ψ) :: Δ) ++ "$}\n\n" - | _, @and _ _ Δ φ ψ dp dq => + | @and _ _ Δ φ ψ dp dq => Derivation.repr dp ++ Derivation.repr dq ++ "\\RightLabel{\\scriptsize($\\land$)}\n" ++ "\\BinaryInfC{$" ++ reprStr ((φ ⋏ ψ) :: Δ) ++ "$}\n\n" - | _, @all _ _ Δ φ d => + | @all _ _ Δ φ d => Derivation.repr d ++ "\\RightLabel{\\scriptsize($\\forall$)}\n" ++ "\\UnaryInfC{$" ++ reprStr ((∀' φ) :: Δ) ++ "$}\n\n" - | _, @ex _ _ Δ φ _ d => + | @ex _ _ Δ φ _ d => Derivation.repr d ++ "\\RightLabel{\\scriptsize($\\exists$)}\n" ++ "\\UnaryInfC{$" ++ reprStr ((∃' φ) :: Δ) ++ "$}\n\n" - | _, @wk _ _ _ Γ d _ => + | @wk _ _ _ Γ d _ => Derivation.repr d ++ "\\RightLabel{\\scriptsize(wk)}\n" ++ "\\UnaryInfC{$" ++ reprStr Γ ++ "$}\n\n" - | _, @cut _ _ Δ _ dp dn => + | @cut _ _ Δ _ dp dn => Derivation.repr dp ++ Derivation.repr dn ++ "\\RightLabel{\\scriptsize(Cut)}\n" ++ "\\BinaryInfC{$" ++ reprStr Δ ++ "$}\n\n" - | _, root (φ := φ) _ => + | root (φ := φ) _ => "\\AxiomC{}\n" ++ "\\RightLabel{\\scriptsize(ROOT)}\n" ++ "\\UnaryInfC{$" ++ reprStr φ ++ ", " ++ reprStr (∼φ) ++ "$}\n\n" @@ -180,14 +128,6 @@ protected abbrev cast (d : T ⟹ Δ) (e : Δ = Γ) : T ⟹ Γ := e ▸ d @[simp] lemma length_cast' (d : T ⟹ Δ) (e : Δ = Γ) : length (e ▸ d) = length d := by rcases e with rfl; simp[Derivation.cast] -/- -@[simp] lemma CutRestricted.cast {C : Set (SyntacticFormula L)} {Δ Γ : Sequent L} {e : Δ = Γ} {d : ⊢ᵀ Δ} : - CutRestricted C (Derivation.cast d e) ↔ CutRestricted C d := by rcases e with ⟨rfl⟩; simp - -@[simp] lemma CutFree.cast {Δ Γ : Sequent L} {e : Δ = Γ} {d : ⊢ᵀ Δ} : - CutFree (Derivation.cast d e) ↔ CutFree d := by rcases e with ⟨rfl⟩; simp --/ - alias weakening := wk def verum' (h : ⊤ ∈ Δ) : T ⟹ Δ := (verum Δ).wk (by simp[h]) @@ -206,38 +146,40 @@ def ex' {φ} (h : ∃' φ ∈ Δ) (t) (d : T ⟹ φ/[t] :: Δ) : T ⟹ Δ := (d. ne_of_lt $ Nat.lt_succ_of_le $ by simp private lemma neg_ne_and {φ ψ : SyntacticFormula L} : ¬∼φ = φ ⋏ ψ := -ne_of_ne_complexity (by simp) - -def em {φ : SyntacticFormula L} {Δ : Sequent L} (hpos : φ ∈ Δ) (hneg : ∼φ ∈ Δ) : T ⟹ Δ := by - induction φ using Semiformula.formulaRec generalizing Δ <;> simp at hneg - case verum => exact verum' hpos - case falsum => exact verum' hneg - case rel r v => exact axL' r v hpos hneg - case nrel r v => exact axL' r v hneg hpos - case all φ ih => - have : T ⟹ ∼Rewriting.free φ :: Rewriting.free φ :: Δ⁺ := ih (by simp) (by simp) + ne_of_ne_complexity (by simp) + +def em {Δ : Sequent L} : {φ : SyntacticFormula L} → (hpos : φ ∈ Δ) → (hneg : ∼φ ∈ Δ) → T ⟹ Δ + | ⊤, hpos, hneg => verum' hpos + | ⊥, hpos, hneg => verum' hneg + | .rel R v, hpos, hneg => axL' R v hpos hneg + | .nrel R v, hpos, hneg => axL' R v hneg hpos + | φ ⋏ ψ, hpos, hneg => + have ihp : T ⟹ φ :: ∼φ :: ∼ψ :: Δ := em (φ := φ) (by simp) (by simp) + have ihq : T ⟹ ψ :: ∼φ :: ∼ψ :: Δ := em (φ := ψ) (by simp) (by simp) + have : T ⟹ ∼φ :: ∼ψ :: Δ := (ihp.and ihq).wk (by simp[hpos]) + this.or.wk (by simpa using hneg) + | φ ⋎ ψ, hpos, hneg => + have ihp : T ⟹ ∼φ :: φ :: ψ :: Δ := em (φ := φ) (by simp) (by simp) + have ihq : T ⟹ ∼ψ :: φ :: ψ :: Δ := em (φ := ψ) (by simp) (by simp) + have : T ⟹ φ :: ψ :: Δ := (ihp.and ihq).wk (by simp [by simpa using hneg]) + this.or.wk (by simp[hpos]) + | ∀' φ, hpos, hneg => + have : T ⟹ ∼Rewriting.free φ :: Rewriting.free φ :: Δ⁺ := em (φ := Rewriting.free φ) (by simp) (by simp) have : T ⟹ (∼Rewriting.shift φ)/[&0] :: Rewriting.free φ :: Δ⁺ := Derivation.cast this (by simp[←TransitiveRewriting.comp_app]) have : T ⟹ Rewriting.free φ :: Δ⁺ := (ex &0 this).wk - (by simp; right; simpa using mem_shifts_iff.mpr hneg) - exact this.all.wk (by simp[hpos]) - case ex φ ih => - have : T ⟹ Rewriting.free φ :: ∼Rewriting.free φ :: Δ⁺ := ih (by simp) (by simp) + (List.cons_subset_of_subset_of_mem + (List.mem_cons_of_mem (free φ) <| by simpa using mem_shifts_iff.mpr hneg) (by rfl)) + this.all.wk (by simp[hpos]) + | ∃' φ, hpos, hneg => + have : T ⟹ Rewriting.free φ :: ∼Rewriting.free φ :: Δ⁺ := em (φ := Rewriting.free φ) (by simp) (by simp) have : T ⟹ (Rewriting.shift φ)/[&0] :: ∼Rewriting.free φ :: Δ⁺ := Derivation.cast this (by simp[←TransitiveRewriting.comp_app]) have : T ⟹ Rewriting.free (∼φ) :: Δ⁺ := (ex &0 this).wk - (by simp; right; simpa using mem_shifts_iff.mpr hpos) - exact this.all.wk (by simp[hneg]) - case and φ ψ ihp ihq => - have ihp : T ⟹ φ :: ∼φ :: ∼ψ :: Δ := ihp (by simp) (by simp) - have ihq : T ⟹ ψ :: ∼φ :: ∼ψ :: Δ := ihq (by simp) (by simp) - have : T ⟹ ∼φ :: ∼ψ :: Δ := (ihp.and ihq).wk (by simp[hpos]) - exact this.or.wk (by simp[hneg]) - case or φ ψ ihp ihq => - have ihp : T ⟹ ∼φ :: φ :: ψ :: Δ := ihp (by simp) (by simp) - have ihq : T ⟹ ∼ψ :: φ :: ψ :: Δ := ihq (by simp) (by simp) - have : T ⟹ φ :: ψ :: Δ := (ihp.and ihq).wk (by simp[hneg]) - exact this.or.wk (by simp[hpos]) + (List.cons_subset_of_subset_of_mem + (List.mem_cons_of_mem (free (∼φ)) <| by simpa using mem_shifts_iff.mpr hpos) (by simp)) + this.all.wk (by simpa using hneg) + termination_by φ => φ.complexity instance : Tait (SyntacticFormula L) (Theory L) where verum := fun _ Δ => verum Δ @@ -267,7 +209,7 @@ def specializes : {k : ℕ} → {φ : SyntacticSemiformula L k} → {Γ : Sequen | k + 1, φ, Γ, v, b => have : T ⟹ (∀' (Rew.substs (v ·.succ)).q ▹ φ) :: Γ := by simpa using specializes (φ := ∀' φ) (v ·.succ) b Derivation.cast (specialize (v 0) this) (by - simp [←TransitiveRewriting.comp_app]; congr 2 + simp only [Nat.reduceAdd, ← TransitiveRewriting.comp_app, List.cons.injEq, and_true]; congr 2 ext x <;> simp [Rew.comp_app] cases x using Fin.cases <;> simp) @@ -296,7 +238,8 @@ def rewrite₁ (b : T ⊢ φ) (f : ℕ → SyntacticTerm L) : T ⊢ (Rew.rewrite Derivation.cast (specializes (fun x ↦ f x) (allClosureFixitr b φ.fvSup)) (by simp) def rewrite {Δ} : T ⟹ Δ → ∀ (f : ℕ → SyntacticTerm L), T ⟹ Δ.map fun φ ↦ Rew.rewrite f ▹ φ - | axL Δ r v, f => by simp[rew_rel, rew_nrel]; exact axL _ _ _ + | axL Δ r v, f => + Derivation.cast (axL (Δ.map fun φ ↦ Rew.rewrite f ▹ φ) r (fun i ↦ Rew.rewrite f (v i))) (by simp[rew_rel, rew_nrel]) | verum Δ, f => Derivation.cast (verum (Δ.map fun φ ↦ Rew.rewrite f ▹ φ)) (by simp) | @or _ _ Δ φ ψ d, f => have : T ⟹ Rew.rewrite f ▹ φ ⋎ Rew.rewrite f ▹ ψ :: Δ.map fun φ ↦ Rew.rewrite f ▹ φ := @@ -330,44 +273,16 @@ protected def map {Δ : Sequent L} (d : T ⟹ Δ) (f : ℕ → ℕ) : protected def shift {Δ : Sequent L} (d : T ⟹ Δ) : T ⟹ Δ⁺ := Derivation.cast (Derivation.map d Nat.succ) (by simp only [Rewriting.shifts, List.map_inj_left]; intro _ _; rfl) -/- -lemma CutRestricted.rewrite {C : Set (SyntacticFormula L)} - (hC : ∀ f : ℕ → SyntacticTerm L, ∀ φ, φ ∈ C → Rew.rewrite f ▹ φ ∈ C) - {Δ : Sequent L} (f : ℕ → SyntacticTerm L) {d : ⟹ Δ} : - CutRestricted C d → CutRestricted C (rewrite d f) := by - induction d generalizing f <;> simp[-List.map_cons, Derivation.rewrite, *] - case axL _ _ _ _ => simp[Rew.rel, Rew.nrel] - case and _ _ _ ihp ihq => intro hp hq; exact ⟨ihp _ hp, ihq _ hq⟩ - case or _ _ ih => intro h; exact ih _ h - case all _ _ _ ih => - rw [CutRestricted.cast, CutRestricted.all', CutRestricted.cast] - exact ih _; simp - case ex _ _ _ ih => - rw [CutRestricted.cast, CutRestricted.ex', CutRestricted.cast] - exact ih _; simp - case wk _ _ ih => intro h; exact ih _ h - case cut _ _ ih ihn => intro hp h hn; exact ⟨hC _ _ hp, ih _ h, ihn _ hn⟩ - -@[simp] lemma length_rewrite (d : T ⟹ Δ) (f : ℕ → SyntacticTerm L) : - length (rewrite d f) = length d := by - induction d generalizing f <;> simp[*, Derivation.rewrite, -List.map_cons] - case axL => simp[Rew.rel, Rew.nrel] - case all => simp [Rew.q_rewrite, *] - case ex => simp [Rew.q_rewrite, *] - case root => simp [] - --/ - -def trans (F : U ⊢* T) : {Γ : Sequent L} → T ⟹ Γ → U ⟹ Γ - | _, axL Γ R v => axL Γ R v - | _, verum Γ => verum Γ - | _, and d₁ d₂ => and (trans F d₁) (trans F d₂) - | _, or d => or (trans F d) - | _, all d => all (trans F d) - | _, ex t d => ex t (trans F d) - | _, wk d ss => wk (trans F d) ss - | _, cut d₁ d₂ => cut (trans F d₁) (trans F d₂) - | _, root h => F h +def trans (F : U ⊢* T) {Γ : Sequent L} : T ⟹ Γ → U ⟹ Γ + | axL Γ R v => axL Γ R v + | verum Γ => verum Γ + | and d₁ d₂ => and (trans F d₁) (trans F d₂) + | or d => or (trans F d) + | all d => all (trans F d) + | ex t d => ex t (trans F d) + | wk d ss => wk (trans F d) ss + | cut d₁ d₂ => cut (trans F d₁) (trans F d₂) + | root h => F h instance : Tait.Axiomatized (SyntacticFormula L) (Theory L) where root {_ _ h} := root h @@ -383,16 +298,16 @@ def invClose (b : T ⊢ ∀∀φ) : T ⊢ φ := cut (wk b (by simp)) (not_close' def invClose! (b : T ⊢! ∀∀φ) : T ⊢! φ := ⟨invClose b.get⟩ -private def deductionAux : {Γ : Sequent L} → T ⟹ Γ → T \ {φ} ⟹ ∼(∀∀φ) :: Γ - | _, axL Γ R v => Tait.wkTail <| axL Γ R v - | _, verum Γ => Tait.wkTail <| verum Γ - | _, and d₁ d₂ => Tait.rotate₁ <| and (Tait.rotate₁ (deductionAux d₁)) (Tait.rotate₁ (deductionAux d₂)) - | _, or d => Tait.rotate₁ <| or (Tait.rotate₂ (deductionAux d)) - | _, all d => Tait.rotate₁ <| all (Derivation.cast (Tait.rotate₁ (deductionAux d)) (by simp)) - | _, ex t d => Tait.rotate₁ <| ex t <| Tait.rotate₁ (deductionAux d) - | _, wk d ss => wk (deductionAux d) (by simp [List.subset_cons_of_subset _ ss]) - | _, cut d₁ d₂ => (Tait.rotate₁ <| deductionAux d₁).cut (Tait.rotate₁ <| deductionAux d₂) - | _, root (φ := ψ) h => if hq : φ = ψ then Derivation.cast (not_close' φ) (by simp [hq]) else +private def deductionAux {Γ : Sequent L} : T ⟹ Γ → T \ {φ} ⟹ ∼(∀∀φ) :: Γ + | axL Γ R v => Tait.wkTail <| axL Γ R v + | verum Γ => Tait.wkTail <| verum Γ + | and d₁ d₂ => Tait.rotate₁ <| and (Tait.rotate₁ (deductionAux d₁)) (Tait.rotate₁ (deductionAux d₂)) + | or d => Tait.rotate₁ <| or (Tait.rotate₂ (deductionAux d)) + | all d => Tait.rotate₁ <| all (Derivation.cast (Tait.rotate₁ (deductionAux d)) (by simp)) + | ex t d => Tait.rotate₁ <| ex t <| Tait.rotate₁ (deductionAux d) + | wk d ss => wk (deductionAux d) (by simp [List.subset_cons_of_subset _ ss]) + | cut d₁ d₂ => (Tait.rotate₁ <| deductionAux d₁).cut (Tait.rotate₁ <| deductionAux d₂) + | root (φ := ψ) h => if hq : φ = ψ then Derivation.cast (not_close' φ) (by simp [hq]) else have : T \ {φ} ⟹. ψ := root (by simp [h, Ne.symm hq]) wk this (by simp) @@ -419,47 +334,37 @@ lemma shifts_image (Φ : L₁ →ᵥ L₂) {Δ : List (SyntacticFormula L₁)} : (Δ.map <| Semiformula.lMap Φ)⁺ = (Δ⁺.map <| Semiformula.lMap Φ) := by simp [Rewriting.shifts, shiftEmb, Finset.map_eq_image, Finset.image_image, Function.comp_def, Semiformula.lMap_shift] -def lMap (Φ : L₁ →ᵥ L₂) : ∀ {Δ}, T₁ ⟹ Δ → T₁.lMap Φ ⟹ Δ.map (.lMap Φ) - | _, axL Δ r v => - by simp[Semiformula.lMap_rel, Semiformula.lMap_nrel]; exact axL _ _ _ - | _, verum Δ => by simpa using verum _ - | _, @or _ _ Δ φ ψ d => by - have : T₁.lMap Φ ⟹ (.lMap Φ φ ⋎ .lMap Φ ψ :: Δ.map (.lMap Φ) : Sequent L₂) := - or (by simpa using lMap Φ d) - exact Derivation.cast this (by simp) - | _, @and _ _ Δ φ ψ dp dq => - have : T₁.lMap Φ ⟹ (.lMap Φ φ ⋏ .lMap Φ ψ :: (Δ.map (.lMap Φ)) : Sequent L₂) := - and (Derivation.cast (lMap Φ dp) (by simp)) (Derivation.cast (lMap Φ dq) (by simp)) - Derivation.cast this (by simp) - | _, @all _ _ Δ φ d => - have : T₁.lMap Φ ⟹ ((∀' .lMap Φ φ) :: (Δ.map (.lMap Φ)) : Sequent L₂) := - all (Derivation.cast (lMap Φ d) (by simp[←Semiformula.lMap_free, shifts_image])) - Derivation.cast this (by simp) - | _, @ex _ _ Δ φ t d => - have : T₁.lMap Φ ⟹ ((∃' .lMap Φ φ) :: (Δ.map (.lMap Φ)) : Sequent L₂) := - ex (Semiterm.lMap Φ t) - (Derivation.cast (lMap Φ d) (by simp[Semiformula.lMap_substs, Matrix.constant_eq_singleton])) - Derivation.cast this (by simp) - | _, @wk _ _ Δ Γ d ss => (lMap Φ d).wk (List.map_subset _ ss) - | _, @cut _ _ Δ φ d dn => - have : T₁.lMap Φ ⟹ (Δ.map (.lMap Φ) : Sequent L₂) := - cut (φ := .lMap Φ φ) (Derivation.cast (lMap Φ d) (by simp)) (Derivation.cast (lMap Φ dn) (by simp)) - Derivation.cast this (by simp[Finset.image_union]) - | _, root h => root (Set.mem_image_of_mem _ h) - -/- -def _root_.LO.FirstOrder.Derivation₀.lMap (Φ : L₁ →ᵥ L₂) (d : ⊢ᵀ Δ₁) : ⊢ᵀ Δ₁.map (.lMap Φ) := by simpa [Theory.lMap] using Derivation.lMap Φ d - -lemma CutRestricted.lMap {C : Set (SyntacticFormula L₂)} {Δ : Sequent L₁} (Φ : L₁ →ᵥ L₂) (d : ⊢ᵀ Δ) : - CutRestricted C (d.lMap Φ) ↔ CutRestricted (.lMap Φ ⁻¹' C) d := by - induction d <;> simp [Derivation.lMap, Derivation₀.lMap, *] - -@[simp] lemma CutFree.lMap {Δ : Sequent L₁} (Φ : L₁ →ᵥ L₂) (d : ⟹ Δ) : - CutFree (lMap Φ d) ↔ CutFree d := by simp[CutFree, CutRestricted.lMap] --/ +def lMap (Φ : L₁ →ᵥ L₂) {Δ} : T₁ ⟹ Δ → T₁.lMap Φ ⟹ Δ.map (.lMap Φ) + | axL Δ r v => + .cast (axL (Δ.map (.lMap Φ)) (Φ.rel r) (fun i ↦ .lMap Φ (v i))) + (by simp [Semiformula.lMap_rel, Semiformula.lMap_nrel]) + | verum Δ => by simpa using verum _ + | @or _ _ Δ φ ψ d => by + have : T₁.lMap Φ ⟹ (.lMap Φ φ ⋎ .lMap Φ ψ :: Δ.map (.lMap Φ) : Sequent L₂) := + or (by simpa using lMap Φ d) + exact Derivation.cast this (by simp) + | @and _ _ Δ φ ψ dp dq => + have : T₁.lMap Φ ⟹ (.lMap Φ φ ⋏ .lMap Φ ψ :: (Δ.map (.lMap Φ)) : Sequent L₂) := + and (Derivation.cast (lMap Φ dp) (by simp)) (Derivation.cast (lMap Φ dq) (by simp)) + Derivation.cast this (by simp) + | @all _ _ Δ φ d => + have : T₁.lMap Φ ⟹ ((∀' .lMap Φ φ) :: (Δ.map (.lMap Φ)) : Sequent L₂) := + all (Derivation.cast (lMap Φ d) (by simp[←Semiformula.lMap_free, shifts_image])) + Derivation.cast this (by simp) + | @ex _ _ Δ φ t d => + have : T₁.lMap Φ ⟹ ((∃' .lMap Φ φ) :: (Δ.map (.lMap Φ)) : Sequent L₂) := + ex (Semiterm.lMap Φ t) + (Derivation.cast (lMap Φ d) (by simp[Semiformula.lMap_substs, Matrix.constant_eq_singleton])) + Derivation.cast this (by simp) + | @wk _ _ Δ Γ d ss => (lMap Φ d).wk (List.map_subset _ ss) + | @cut _ _ Δ φ d dn => + have : T₁.lMap Φ ⟹ (Δ.map (.lMap Φ) : Sequent L₂) := + cut (φ := .lMap Φ φ) (Derivation.cast (lMap Φ d) (by simp)) (Derivation.cast (lMap Φ dn) (by simp)) + Derivation.cast this (by simp[Finset.image_union]) + | root h => root (Set.mem_image_of_mem _ h) lemma inconsistent_lMap (Φ : L₁ →ᵥ L₂) : System.Inconsistent T₁ → System.Inconsistent (T₁.lMap Φ) := by - simp [System.inconsistent_iff_provable_bot]; intro ⟨b⟩; exact ⟨by simpa using lMap Φ b⟩ + simp only [System.inconsistent_iff_provable_bot]; intro ⟨b⟩; exact ⟨by simpa using lMap Φ b⟩ end Hom @@ -467,14 +372,15 @@ omit [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k) private lemma map_subst_eq_free (φ : SyntacticSemiformula L 1) (h : ¬φ.FVar? m) : (@Rew.rewriteMap L ℕ ℕ 0 (fun x ↦ if x = m then 0 else x + 1)) ▹ (φ/[&m] : SyntacticFormula L) = Rewriting.free φ := by - simp[←TransitiveRewriting.comp_app]; + simp only [← TransitiveRewriting.comp_app] exact Semiformula.rew_eq_of_funEqOn (by simp[Rew.comp_app, Fin.eq_zero]) - (fun x hx => by simp[Rew.comp_app]; rintro rfl; contradiction) + (fun x hx => by simp [Rew.comp_app, ne_of_mem_of_not_mem hx h]) private lemma map_rewriteMap_eq_shifts (Δ : Sequent L) (h : ∀ φ ∈ Δ, ¬φ.FVar? m) : Δ.map (fun φ ↦ @Rew.rewriteMap L ℕ ℕ 0 (fun x ↦ if x = m then 0 else x + 1) ▹ φ) = Δ⁺ := by apply List.map_congr_left - intro φ hp; exact rew_eq_of_funEqOn₀ (by intro x hx; simp; rintro rfl; have := h φ hp; contradiction) + intro φ hp; exact rew_eq_of_funEqOn₀ + (by intro x hx; simp [ne_of_mem_of_not_mem hx (h φ hp)]) def genelalizeByNewver {φ : SyntacticSemiformula L 1} (hp : ¬φ.FVar? m) (hΔ : ∀ ψ ∈ Δ, ¬ψ.FVar? m) (d : T ⟹ φ/[&m] :: Δ) : T ⟹ (∀' φ) :: Δ := by @@ -485,7 +391,7 @@ def genelalizeByNewver {φ : SyntacticSemiformula L 1} (hp : ¬φ.FVar? m) (hΔ def exOfInstances (v : List (SyntacticTerm L)) (φ : SyntacticSemiformula L 1) (h : T ⟹ v.map (φ/[·]) ++ Γ) : T ⟹ (∃' φ) :: Γ := by - induction' v with t v ih generalizing Γ <;> simp at h + induction' v with t v ih generalizing Γ · exact weakening h (List.subset_cons_self _ _) · exact (ih (Γ := (∃' φ) :: Γ) ((ex t h).wk (by simp))).wk (by simp)