Substitution and Helper Lemmas

The lemmas here are mostly from Sections 2.1 and 2.2.

Single-step replacing

def PDL.replInF (x : ℕ) (ψ : Formula) : Formula → Formula

Replace atomic proposition x by ψ in a formula.

Equations

• PDL.replInF x ψ PDL.Formula.bottom = ⊥
• PDL.replInF x ψ (PDL.Formula.atom_prop c) = if (c == x) = true then ψ else PDL.Formula.atom_prop c
• PDL.replInF x ψ φ.neg = (PDL.replInF x ψ φ).neg
• PDL.replInF x ψ (φ1.and φ2) = (PDL.replInF x ψ φ1).and (PDL.replInF x ψ φ2)
• PDL.replInF x ψ (PDL.Formula.box α φ) = PDL.Formula.box (PDL.replInP x ψ α) (PDL.replInF x ψ φ)

def PDL.replInP (x : ℕ) (ψ : Formula) : Program → Program

Replace atomic proposition x by ψ in a program.

Equations

• PDL.replInP x ψ (PDL.Program.atom_prog c) = PDL.Program.atom_prog c
• PDL.replInP x ψ (α.sequence β) = (PDL.replInP x ψ α).sequence (PDL.replInP x ψ β)
• PDL.replInP x ψ (α.union β) = (PDL.replInP x ψ α).union (PDL.replInP x ψ β)
• PDL.replInP x ψ α.star = (PDL.replInP x ψ α).star
• PDL.replInP x ψ (PDL.Program.test φ) = PDL.Program.test (PDL.replInF x ψ φ)

theorem PDL.repl_in_con {x : ℕ} {ψ : Formula} {l : List Formula} : replInF x ψ (con l) = con (List.map (replInF x ψ) l)

theorem PDL.repl_in_or {x : ℕ} {ψ φ1 φ2 : Formula} : replInF x ψ (φ1.or φ2) = (replInF x ψ φ1).or (replInF x ψ φ2)

theorem PDL.repl_in_dis {x : ℕ} {ψ : Formula} {l : List Formula} : replInF x ψ (dis l) = dis (List.map (replInF x ψ) l)

theorem PDL.repl_in_F_non_occ_eq {x : ℕ} {φ ρ : Formula} : Sum.inl x ∉ φ.voc → replInF x ρ φ = φ

theorem PDL.repl_in_P_non_occ_eq {x : ℕ} {α : Program} {ρ : Formula} : Sum.inl x ∉ α.voc → replInP x ρ α = α

theorem PDL.repl_in_boxes_non_occ_eq_neg {x : ℕ} {ψ : Formula} (δ : List Program) : Sum.inl x ∉ Vocab.fromList (List.map Program.voc δ) → replInF x ψ (Formula.boxes δ (Formula.atom_prop x).neg) = Formula.boxes δ ψ.neg

theorem PDL.repl_in_boxes_non_occ_eq_pos {x : ℕ} {ψ : Formula} (δ : List Program) : Sum.inl x ∉ Vocab.fromList (List.map Program.voc δ) → replInF x ψ (Formula.boxes δ (Formula.atom_prop x)) = Formula.boxes δ ψ

theorem PDL.repl_in_list_non_occ_eq {x : ℕ} {ρ : Formula} (F : List Formula) : Sum.inl x ∉ Vocab.fromList (List.map Formula.voc F) → List.map (replInF x ρ) F = F

theorem PDL.repl_in_F_voc_def (p : ℕ) (φ ψ : Formula) : (replInF p φ ψ).voc = ψ.voc \ {Sum.inl p} ∪ if Sum.inl p ∈ ψ.voc then φ.voc else ∅

theorem PDL.repl_in_P_voc_def (p : ℕ) (φ : Formula) (α : Program) : (replInP p φ α).voc = α.voc \ {Sum.inl p} ∪ if Sum.inl p ∈ α.voc then φ.voc else ∅

def PDL.replInModel {W : Type} (x : ℕ) (ψ : Formula) : KripkeModel W → KripkeModel W

Overwrite the valuation of x with the current value of ψ in a model.

Equations

• PDL.replInModel x ψ { val := V, Rel := R } = { val := fun (w : W) (c : ℕ) => if (c == x) = true then PDL.vDash.SemImplies ({ val := V, Rel := R }, w) ψ else V w c, Rel := R }

theorem PDL.repl_in_model_sat_iff (x : ℕ) (ψ φ : Formula) {W : Type} (M : KripkeModel W) (w : W) : vDash.SemImplies (M, w) (replInF x ψ φ) ↔ vDash.SemImplies (replInModel x ψ M, w) φ

theorem PDL.repl_in_model_rel_iff (x : ℕ) (ψ : Formula) (α : Program) {W : Type} (M : KripkeModel W) (w v : W) : relate M (replInP x ψ α) w v ↔ relate (replInModel x ψ M) α w v

theorem PDL.repl_in_F_equiv {φ1 φ2 : Formula} (x : ℕ) (ψ : Formula) : semEquiv φ1 φ2 → semEquiv (replInF x ψ φ1) (replInF x ψ φ2)

theorem PDL.repl_in_P_equiv {α1 α2 : Program} (x : ℕ) (ψ : Formula) : relEquiv α1 α2 → relEquiv (replInP x ψ α1) (replInP x ψ α2)

theorem PDL.repl_in_disMap {α : Type u_1} (x : ℕ) (ρ : Formula) (L : List α) (p : α → Prop) (f : α → Formula) [DecidablePred p] : replInF x ρ (dis (List.map (fun (Fδ : α) => if p Fδ then Formula.bottom else f Fδ) L)) = dis (List.map (fun (Fδ : α) => if p Fδ then Formula.bottom else replInF x ρ (f Fδ)) L)

Cancellation of replacements

@[simp]

theorem PDL.repl_in_F_cancel_via_non_occ (φ : Formula) (p q : ℕ) : Sum.inl q ∉ φ.voc → replInF q (Formula.atom_prop p) (replInF p (Formula.atom_prop q) φ) = φ

Replacing p with a fresh q and then replacing q by p results in the same formula.

theorem PDL.repl_in_P_cancel_via_non_occ (α : Program) (p q : ℕ) : Sum.inl q ∉ α.voc → replInP q (Formula.atom_prop p) (replInP p (Formula.atom_prop q) α) = α

Replacing p with a fresh q and then replacing q by p results in the same program.

Replacement of atoms in tautologies

theorem PDL.taut_repl (φ : Formula) (p q : ℕ) : tautology φ → tautology (replInF p (Formula.atom_prop q) φ)

Replacing an atom in a tautology results in a tautology.

theorem PDL.non_occ_taut_then_taut_repl_in_imp (φ ψ : Formula) (p q : ℕ) : Sum.inl p ∉ ψ.voc → tautology (φ.and ψ.neg).neg → tautology ((replInF p (Formula.atom_prop q) φ).and ψ.neg).neg

A special case of taut_repl for the proof of beth.

theorem PDL.non_occ_taut_then_taut_imp_repl_in (φ ψ : Formula) (p q : ℕ) : Sum.inl p ∉ ψ.voc → tautology (ψ.and φ.neg).neg → tautology (ψ.and (replInF p (Formula.atom_prop q) φ).neg).neg

Another special case of taut_repl for the proof of beth.

Simultaneous Substitutions

@[reducible, inline]

abbrev PDL.Substitution : Type

A substitution assigning a formula to each atomic proposition.

Equations

• PDL.Substitution = (ℕ → PDL.Formula)

def PDL.substInF (σ : Substitution) (φ : Formula) : Formula

Apply substitution σ to formula φ.

Equations

• PDL.substInF σ PDL.Formula.bottom = ⊥
• PDL.substInF σ (PDL.Formula.atom_prop c) = σ c
• PDL.substInF σ φ.neg = (PDL.substInF σ φ).neg
• PDL.substInF σ (φ1.and φ2) = (PDL.substInF σ φ1).and (PDL.substInF σ φ2)
• PDL.substInF σ (PDL.Formula.box α φ) = PDL.Formula.box (PDL.substInP σ α) (PDL.substInF σ φ)

def PDL.substInP (σ : Substitution) (α : Program) : Program

Apply substitution σ to program α.

Equations

• PDL.substInP σ (PDL.Program.atom_prog c) = PDL.Program.atom_prog c
• PDL.substInP σ (α.sequence β) = (PDL.substInP σ α).sequence (PDL.substInP σ β)
• PDL.substInP σ (α.union β) = (PDL.substInP σ α).union (PDL.substInP σ β)
• PDL.substInP σ α.star = (PDL.substInP σ α).star
• PDL.substInP σ (PDL.Program.test φ) = PDL.Program.test (PDL.substInF σ φ)

def PDL.substInModel {W : Type} (σ : Substitution) (M : KripkeModel W) : KripkeModel W

Overwrite the valuation in M with the substitution σ.

Equations

• PDL.substInModel σ { val := V, Rel := R } = { val := fun (w : W) (c : ℕ) => PDL.vDash.SemImplies ({ val := V, Rel := R }, w) (σ c), Rel := R }

theorem PDL.substitutionLemma (σ : Substitution) (φ : Formula) {W : Type} (M : KripkeModel W) (w : W) : vDash.SemImplies (M, w) (substInF σ φ) ↔ vDash.SemImplies (substInModel σ M, w) φ

theorem PDL.substitutionLemmaRel (σ : Substitution) (α : Program) {W : Type} (M : KripkeModel W) (w v : W) : relate M (substInP σ α) w v ↔ relate (substInModel σ M) α w v

Semantic Equivalents

The following does not hold in general, because frm might be sneaky: theorem wrong_equiv_repl φ1 φ2 (h : φ1 ≡ φ2) (frm : Formula → Formula) : frm φ1 ≡ frm φ2 := by ...

theorem PDL.equiv_con {φ1 φ2 : Formula} (h : semEquiv φ1 φ2) (ψ : Formula) : semEquiv (φ1.and ψ) (φ2.and ψ)

A true instance of wrong_equiv_repl, here we replaced frm with a special case.