PdlTestFree.WithTest

PdlTestFree
WithTest

Imports

module

public import PdlTestFree.NoInterpolation

@[expose] public sectionopen TestfreeNoItp

With a test there is an interpolant

If we allow test operators, then there is an interpolant for ⋀Γ₁ → ¬⋀Γ₂.

The formula [(p?;a)*](p → ⟨a⟩⊤) which uses a test. This formulas says that along every p-path, every p-state has a successor.

def testIP : Formula := ⌈∗((?'p) ;' a)⌉(p ↣ Formula.neg (⌈a⌉⊥))

The formula testIP is not test-free..

lemma not_testFree_withTest : ¬ testIP.testFree := by⊢ ¬testIP.testFree
  simp [testIP]All goals completed! 🐙

Γ₁ implies `testIP`

Γ₁ ⊨ [(p?;a)*](p → ⟨a⟩⊤).

lemma gammaOne_withTest {W : Type} (M : KripkeModel W) (w : W)
    (h1 : ∀ φ ∈ gammaOne, evaluate M w φ) : evaluate M w testIP := byW:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φ⊢ evaluate M w testIP
  obtain ⟨hs, hbody⟩ := (gammaOne_iff M w).mp h1W:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2⊢ evaluate M w testIP
  simp only [testIP, evaluate, relate, not_and, not_not]W:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2⊢ ∀ (v : W),
  Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w v →
    M.val v 0 → ¬∀ (v_1 : W), M.Rel 0 v v_1 → False
  intro v hvW:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2v:Whv:Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w v⊢ M.val v 0 → ¬∀ (v_1 : W), M.Rel 0 v v_1 → False
  -- every state reached along `(p?;a)*` from `w` is `a*`-reachable and satisfies `s`
  have key : Relation.ReflTransGen (M.Rel 0) w v ∧ M.val v 2 := byW:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φ⊢ evaluate M w testIP
    induction hv with
    | refl =>reflW:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2v:W⊢ Relation.ReflTransGen (M.Rel 0) w w ∧ M.val w 2 exact ⟨.refl, hs⟩All goals completed! 🐙
    | tail _ hvu IH =>tailW:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2v:Wb✝:Wc✝:Wa✝:Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w b✝hvu:∃ y, (b✝ = y ∧ M.val b✝ 0) ∧ M.Rel 0 y c✝IH:Relation.ReflTransGen (M.Rel 0) w b✝ ∧ M.val b✝ 2⊢ Relation.ReflTransGen (M.Rel 0) w c✝ ∧ M.val c✝ 2
        obtain ⟨y, ⟨rfl, hpv⟩, hvu⟩ := hvutailW:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2v:Wb✝:Wc✝:Wa✝:Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w b✝IH:Relation.ReflTransGen (M.Rel 0) w b✝ ∧ M.val b✝ 2hpv:M.val b✝ 0hvu:M.Rel 0 b✝ c✝⊢ Relation.ReflTransGen (M.Rel 0) w c✝ ∧ M.val c✝ 2
        exact ⟨IH.1.tail hvu, (hbody _ IH.1 hpv IH.2).2 _ hvu⟩W:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2v:Whv:Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w vkey:Relation.ReflTransGen (M.Rel 0) w v ∧ M.val v 2⊢ M.val v 0 → ¬∀ (v_1 : W), M.Rel 0 v v_1 → False
  intro hpv hdeadW:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2v:Whv:Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w vkey:Relation.ReflTransGen (M.Rel 0) w v ∧ M.val v 2hpv:M.val v 0hdead:∀ (v_1 : W), M.Rel 0 v v_1 → False⊢ False
  obtain ⟨u, hu⟩ := (hbody v key.1 hpv key.2).1W:TypeM:KripkeModel Ww:Wh1:∀ φ ∈ gammaOne, evaluate M w φhs:M.val w 2hbody:∀ (v : W),
  Relation.ReflTransGen (M.Rel 0) w v → M.val v 0 → M.val v 2 → (∃ u, M.Rel 0 v u) ∧ ∀ (u : W), M.Rel 0 v u → M.val u 2v:Whv:Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w vkey:Relation.ReflTransGen (M.Rel 0) w v ∧ M.val v 2hpv:M.val v 0hdead:∀ (v_1 : W), M.Rel 0 v v_1 → Falseu:Whu:M.Rel 0 v u⊢ False
  exact hdead u huAll goals completed! 🐙

Γ₂ implies the negation of `testIP`

Γ₂ ⊨ ¬[(p?;a)*](p → ⟨a⟩⊤).

lemma gammaTwo_not_withTest {W : Type} (M : KripkeModel W) (w : W)
    (h2 : ∀ φ ∈ gammaTwo, evaluate M w φ) : ¬ evaluate M w testIP := byW:TypeM:KripkeModel Ww:Wh2:∀ φ ∈ gammaTwo, evaluate M w φ⊢ ¬evaluate M w testIP
  obtain ⟨hqp, -, v, hv, hqv, hdead⟩ := (gammaTwo_iff M w).mp h2W:TypeM:KripkeModel Ww:Wh2:∀ φ ∈ gammaTwo, evaluate M w φhqp:∀ (v : W), Relation.ReflTransGen (M.Rel 0) w v → M.val v 1 → M.val v 0v:Whv:Relation.ReflTransGen (M.Rel 0) w vhqv:M.val v 1hdead:∀ (u : W), ¬M.Rel 0 v u⊢ ¬evaluate M w testIP
  simp only [testIP, evaluate, relate, not_forall, not_and, not_not, not_exists, exists_prop,
    not_false_eq_true, and_true]W:TypeM:KripkeModel Ww:Wh2:∀ φ ∈ gammaTwo, evaluate M w φhqp:∀ (v : W), Relation.ReflTransGen (M.Rel 0) w v → M.val v 1 → M.val v 0v:Whv:Relation.ReflTransGen (M.Rel 0) w vhqv:M.val v 1hdead:∀ (u : W), ¬M.Rel 0 v u⊢ ∃ x,
  Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w x ∧
    M.val x 0 ∧ ∀ (x_1 : W), ¬M.Rel 0 x x_1
  refine ⟨v, ?_, hqp v hv hqv, hdead⟩W:TypeM:KripkeModel Ww:Wh2:∀ φ ∈ gammaTwo, evaluate M w φhqp:∀ (v : W), Relation.ReflTransGen (M.Rel 0) w v → M.val v 1 → M.val v 0v:Whv:Relation.ReflTransGen (M.Rel 0) w vhqv:M.val v 1hdead:∀ (u : W), ¬M.Rel 0 v u⊢ Relation.ReflTransGen (fun x x_1 ↦ ∃ y, (x = y ∧ M.val x 0) ∧ M.Rel 0 y x_1) w v
  -- the path to `v` consists of `p`-states, hence is a `(p?;a)*`-path
  exact Relation.ReflTransGen.mono (fun x y ⟨hxy, hpx, _⟩ => ⟨x, ⟨rfl, hpx⟩, hxy⟩) _ _
    (gammaTwo_path h2 hv hqv)All goals completed! 🐙

`testIP` is an interpolant for Γ₁;Γ₂

[(p?;a)*](p → ⟨a⟩⊤) is an Interpolant for ⋀Γ₁ → ¬⋀Γ₂ (with a test).

theorem withTest_Interpolant :
    Interpolant (con gammaOne) (~ con gammaTwo) testIP := by⊢ Interpolant (con gammaOne) (~con gammaTwo) testIP
  refine ⟨?_, ?_, ?_⟩refine_1⊢ testIP.voc ⊆ (con gammaOne).voc ∩ (~con gammaTwo).vocrefine_2⊢ tautology (~(con gammaOne ⋀ ~testIP))refine_3⊢ tautology (~(testIP ⋀ ~~con gammaTwo))
  ·refine_1⊢ testIP.voc ⊆ (con gammaOne).voc ∩ (~con gammaTwo).voc rw [voc_gammaOne_gammaTworefine_1⊢ testIP.voc ⊆ commonVoc]refine_1⊢ testIP.voc ⊆ commonVoc
    decideAll goals completed! 🐙
  ·refine_2⊢ tautology (~(con gammaOne ⋀ ~testIP)) intro W M wrefine_2W:TypeM:KripkeModel Ww:W⊢ evaluate M w (~(con gammaOne ⋀ ~testIP))
    simp only [evaluate, conEval, not_and, not_not]refine_2W:TypeM:KripkeModel Ww:W⊢ (∀ f ∈ gammaOne, evaluate M w f) → evaluate M w testIP
    exact gammaOne_withTest M wAll goals completed! 🐙
  ·refine_3⊢ tautology (~(testIP ⋀ ~~con gammaTwo)) intro W M wrefine_3W:TypeM:KripkeModel Ww:W⊢ evaluate M w (~(testIP ⋀ ~~con gammaTwo))
    simp only [evaluate, conEval, not_and, not_not]refine_3W:TypeM:KripkeModel Ww:W⊢ evaluate M w testIP → ¬∀ f ∈ gammaTwo, evaluate M w f
    exact fun hθ h2 => gammaTwo_not_withTest M w h2 hθAll goals completed! 🐙

With a test there is an interpolant

Γ₁ implies testIP

Γ₂ implies the negation of testIP

testIP is an interpolant for Γ₁;Γ₂

Γ₁ implies `testIP`

Γ₂ implies the negation of `testIP`

`testIP` is an interpolant for Γ₁;Γ₂