Soundness (Section 6) #
Soundness of the PDL rules #
The PDL rules are sound.
Navigating through tableaux with PathIn #
A path in a tableau. Three constructors for the empty path, a local step or a pdl step.
The loc ad pdl steps correspond to two out of three constructors of Tableau.
- nil {H : History} {X : Sequent} {a✝ : Tableau H X} : PathIn a✝
- loc {H : List Sequent} {X Y : Sequent} {lt : LocalTableau X} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: H) Y} (Y_in : Y ∈ endNodesOf lt) (tail : PathIn (next Y Y_in)) : PathIn (Tableau.loc lt next)
- pdl {Γ Δ : Sequent} {Hist : List Sequent} {child : Tableau (Γ :: Hist) Δ} (r : PdlRule Γ Δ) : PathIn child → PathIn (Tableau.pdl r child)
Instances For
instance
instDecidableEqPathIn
{H✝ : History}
{X✝ : Sequent}
{a✝ : Tableau H✝ X✝}
:
DecidableEq (PathIn a✝)
Equations
def
PathIn.append
{a✝ : History}
{a✝¹ : Sequent}
{tab : Tableau a✝ a✝¹}
(p : PathIn tab)
(q : PathIn (tabAt p).snd.snd)
:
PathIn tab
Equations
- PathIn.nil.append q_2 = q_2
- (PathIn.loc Y_in tail).append q_2 = PathIn.loc Y_in (tail.append q_2)
- (PathIn.pdl r p_child).append q_2 = PathIn.pdl r (p_child.append q_2)
Instances For
theorem
PathIn.nil_eq_append_iff_both_eq_nil
{a✝ : History}
{a✝¹ : Sequent}
{tab : Tableau a✝ a✝¹}
(p : PathIn tab)
(q : PathIn (tabAt p).snd.snd)
:
PathIn.nil = p.append q ↔ p = PathIn.nil ∧ q = PathIn.nil
@[simp]
theorem
tabAt_loc
{X✝ : Sequent}
{a✝ : LocalTableau X✝}
{a✝¹ : Sequent}
{Y_in : a✝¹ ∈ endNodesOf a✝}
{tail✝ : History}
{a✝² : (Y : Sequent) → Y ∈ endNodesOf a✝ → Tableau (X✝ :: tail✝) Y}
{tail : PathIn (a✝² a✝¹ Y_in)}
:
tabAt (PathIn.loc Y_in tail) = tabAt tail
@[simp]
@[simp]
theorem
nodeAt_loc
{X✝ : Sequent}
{a✝ : LocalTableau X✝}
{a✝¹ : Sequent}
{Y_in : a✝¹ ∈ endNodesOf a✝}
{tail✝ : History}
{a✝² : (Y : Sequent) → Y ∈ endNodesOf a✝ → Tableau (X✝ :: tail✝) Y}
{tail : PathIn (a✝² a✝¹ Y_in)}
:
nodeAt (PathIn.loc Y_in tail) = nodeAt tail
The length of a path is the number of actual steps.
Equations
- PathIn.nil.length = 0
- (PathIn.pdl r tail).length = tail.length + 1
- (PathIn.loc Y_in tail).length = tail.length + 1
Instances For
theorem
PathIn.loc_Yin_irrel
{X : Sequent}
{rest : List Sequent}
{lt : LocalTableau X}
{next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: rest) Y}
{Y : Sequent}
(Y_in1 Y_in2 : Y ∈ endNodesOf lt)
{tail : PathIn (next Y Y_in1)}
:
PathIn.loc Y_in1 tail = PathIn.loc Y_in2 tail
The Y_in proof does not matter for a local path step.
Edge Relation #
Notation ⋖_ for edge (because ⋖ is taken in Mathlib).
Equations
- «term_⋖__» = Lean.ParserDescr.trailingNode `«term_⋖__» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋖_ ") (Lean.ParserDescr.cat `term 1023))
Instances For
theorem
edge_append_loc_nil
{sX : Sequent}
{sHist : List Sequent}
{X : History}
{Hist : Sequent}
{tab : Tableau X Hist}
(s : PathIn tab)
{lt : LocalTableau sX}
(next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (sX :: sHist) Y)
{Y : Sequent}
(Y_in : Y ∈ endNodesOf lt)
(tabAt_s_def : tabAt s = ⟨sHist, ⟨sX, Tableau.loc lt next⟩⟩)
:
s ⋖_ (s.append (⋯ ▸ PathIn.loc Y_in PathIn.nil))
Appending a one-step loc path is also a ⋖_ child.
When using this, this may be helpful:
convert this; rw [← heq_iff_eq, heq_eqRec_iff_heq, eqRec_heq_iff_heq].
@[simp]
theorem
edge_append_pdl_nil
{a✝ : History}
{a✝¹ : Sequent}
{a✝² : Tableau a✝ a✝¹}
{s : PathIn a✝²}
{Δ✝ : Sequent}
{r : PdlRule (tabAt s).snd.fst Δ✝}
{next : Tableau ((tabAt s).snd.fst :: (tabAt s).fst) Δ✝}
(h : (tabAt s).snd.snd = Tableau.pdl r next)
:
s ⋖_ (s.append (⋯ ▸ PathIn.pdl r PathIn.nil))
Appending a one-step pdl path is also a ⋖_ child.
@[simp]
theorem
nil_edge_loc_nil
{Y X : Sequent}
{lt : LocalTableau X}
{Y_in : Y ∈ endNodesOf lt}
{tail : List Sequent}
{next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: tail) Y}
:
PathIn.nil ⋖_ (PathIn.loc Y_in PathIn.nil)
@[simp]
theorem
loc_edge_loc_iff_edge
{Y X : Sequent}
{lt : LocalTableau X}
{Y_in : Y ∈ endNodesOf lt}
{tail : List Sequent}
{next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: tail) Y}
{t s : PathIn (next Y Y_in)}
:
(PathIn.loc Y_in t) ⋖_ (PathIn.loc Y_in s) ↔ t ⋖_ s
@[simp]
theorem
pdl_edge_pdl_iff_edge
{X Y : Sequent}
{r : PdlRule X Y}
{tail : List Sequent}
{a : Tableau (X :: tail) Y}
{t s : PathIn a}
:
(PathIn.pdl r t) ⋖_ (PathIn.pdl r s) ↔ t ⋖_ s
The root has no parent. Note this holds even when Hist ≠ [].
theorem
nodeAt_loc_nil
{X Y : Sequent}
{H : List Sequent}
{lt : LocalTableau X}
(next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: H) Y)
(Y_in : Y ∈ endNodesOf lt)
:
nodeAt (PathIn.loc Y_in PathIn.nil) = Y
theorem
nodeAt_pdl_nil
{X : Sequent}
{Hist : List Sequent}
{Y : Sequent}
(child : Tableau (X :: Hist) Y)
(r : PdlRule X Y)
:
nodeAt (PathIn.pdl r PathIn.nil) = Y
Equations
- edge_natLT_relHom = { toFun := PathIn.length, map_rel' := ⋯ }
Instances For
The ⋖_ relation in a tableau is well-founded.
Enable "<" notation for transitive closure of ⋖_.
Equations
- instLTPathIn = { lt := Relation.TransGen edge }
Enable "≤" notation for reflexive transitive closure of ⋖_
Equations
- instLEPathIn = { le := Relation.ReflTransGen edge }
instance
edge.TransGen_isAsymm
{a✝ : History}
{a✝¹ : Sequent}
{tab : Tableau a✝ a✝¹}
:
IsAsymm (PathIn tab) (Relation.TransGen edge)
The "<" in a tableau is antisymmetric.
theorem
PathIn.init_inductionOn
{a✝ : History}
{a✝¹ : Sequent}
{tab : Tableau a✝ a✝¹}
(t : PathIn tab)
{motive : PathIn tab → Prop}
(root : motive PathIn.nil)
(step : ∀ (t : PathIn tab), motive t → ∀ {s : PathIn tab}, t ⋖_ s → motive s)
:
motive t
An induction principle for PathIn that works by ... TODO EXPLAIN
-- QUESTIONS:
-- - Do I need any of these? @[induction_eliminator, elab_as_elim]
-- - Should it be a def or a theorem? (motive to Prop or to Sort u?)
theorem
PathIn.nil_le_anything
{a✝ : History}
{a✝¹ : Sequent}
{a✝² : Tableau a✝ a✝¹}
{t : PathIn a✝²}
:
PathIn.nil ≤ t
theorem
PathIn.loc_le_loc_of_le
{Hist : List Sequent}
{X Y : Sequent}
{lt : LocalTableau X}
{next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y}
{Z_in : Y ∈ endNodesOf lt}
{t1 t2 : PathIn (next Y Z_in)}
(h : t1 ≤ t2)
:
PathIn.loc Z_in t1 ≤ PathIn.loc Z_in t2
theorem
PathIn.pdl_le_pdl_of_le
{Hist X : Sequent}
{Y : List Sequent}
{r : Tableau (Hist :: Y) X}
{Z_in : PdlRule Hist X}
{t1 t2 : PathIn r}
(h : t1 ≤ t2)
:
PathIn.pdl Z_in t1 ≤ PathIn.pdl Z_in t2
Path Properties (UNUSED?) #
Equations
- PathIn.nil.isLoaded = (PathIn.nil.head.isLoaded = true)
- (PathIn.pdl r tail).isLoaded = ((PathIn.pdl r tail).head.isLoaded = true ∧ tail.isLoaded)
- (PathIn.loc Y_in tail).isLoaded = ((PathIn.loc Y_in tail).head.isLoaded = true ∧ tail.isLoaded)
Instances For
From Path to History #
Convert a path to a History.
Does not include the last node.
The history of .nil is [] because this will not go into Hist.
Equations
- PathIn.nil.toHistory = []
- (PathIn.pdl r tail).toHistory = tail.toHistory ++ [X]
- (PathIn.loc Y_in tail).toHistory = tail.toHistory ++ [X]
Instances For
Convert a path to a list of nodes. Reverse of the history and does include the last node.
The list of .nil is [X].
Equations
- PathIn.nil.toList = [X]
- (PathIn.pdl r tail).toList = X :: tail.toList
- (PathIn.loc Y_in tail).toList = X :: tail.toList
Instances For
theorem
tabAt_fst_length_eq_toHistory_length
{X : Sequent}
{tab : Tableau [] X}
(s : PathIn tab)
:
List.length (tabAt s).fst = List.length s.toHistory
@[simp]
theorem
PathIn.loc_length_eq
{X Y : Sequent}
{Hist : List Sequent}
{lt : LocalTableau X}
(Y_in : Y ∈ endNodesOf lt)
{next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y}
(tail : PathIn (next Y Y_in))
:
List.length (PathIn.loc Y_in tail).toHistory = List.length tail.toHistory + 1
@[simp]
theorem
PathIn.pdl_length_eq
{X Y : Sequent}
{Hist : List Sequent}
(r : PdlRule X Y)
{next : Tableau (X :: Hist) Y}
(tail : PathIn next)
:
List.length (PathIn.pdl r tail).toHistory = List.length tail.toHistory + 1
def
PathIn.prefix
{Hist : History}
{X : Sequent}
{tab : Tableau Hist X}
(t : PathIn tab)
(k : Fin (t.length + 1))
:
PathIn tab
Prefix of a path, taking only the first k steps.
Equations
- PathIn.nil.prefix x_2 = PathIn.nil
- (PathIn.pdl r tail).prefix k = Fin.cases PathIn.nil (fun (j : Fin (PathIn.pdl r tail).length) => PathIn.pdl r (tail.prefix j)) k
- (PathIn.loc Y_in tail).prefix k = Fin.cases PathIn.nil (fun (j : Fin (PathIn.loc Y_in tail).length) => PathIn.loc Y_in (tail.prefix j)) k
Instances For
Path Rewinding #
def
PathIn.rewind
{a✝ : History}
{a✝¹ : Sequent}
{tab : Tableau a✝ a✝¹}
(t : PathIn tab)
(k : Fin (List.length t.toHistory + 1))
:
PathIn tab
Rewinding a path, removing the last k steps. Cannot go into Hist.
Used to go to the companion of a repeat. Returns .nil when k is the length of the whole path.
We use +1 in the type because rewind 0 is always possible, even with history [].
Defined using Fin.lastCases.
Equations
- PathIn.nil.rewind x_2 = PathIn.nil
- (PathIn.loc Y_in tail).rewind k = Fin.lastCases PathIn.nil (PathIn.loc Y_in ∘ tail.rewind ∘ Fin.cast ⋯) k
- (PathIn.pdl r tail).rewind k = Fin.lastCases PathIn.nil (PathIn.pdl r ∘ tail.rewind ∘ Fin.cast ⋯) k
Instances For
theorem
PathIn.rewind_le
{a✝ : History}
{a✝¹ : Sequent}
{tab : Tableau a✝ a✝¹}
(t : PathIn tab)
(k : Fin (List.length t.toHistory + 1))
:
t.rewind k ≤ t
Companion, cEdge, etc. #
def
companionOf
{X : Sequent}
{tab : Tableau [] X}
(s : PathIn tab)
(lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst)
:
(tabAt s).snd.snd = Tableau.rep lpr → PathIn tab
To get the companion of an LPR node we go as many steps back as the LPR says.
Equations
- companionOf s lpr x✝ = s.rewind (⋯ ▸ ↑lpr).succ
Instances For
Equations
- «term_♥_» = Lean.ParserDescr.trailingNode `«term_♥_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ♥ ") (Lean.ParserDescr.cat `term 1023))
Instances For
theorem
nodeAt_companionOf_eq_toHistory_get_lpr_val
{a✝ : Sequent}
{tab : Tableau [] a✝}
(s : PathIn tab)
(lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst)
(h : (tabAt s).snd.snd = Tableau.rep lpr)
:
nodeAt (companionOf s lpr h) = List.get s.toHistory (⋯ ▸ ↑lpr)
The node at a companion is the same as the one in the history.
theorem
nodeAt_companionOf_setEq
{X : Sequent}
{tab : Tableau [] X}
(s : PathIn tab)
(lpr : LoadedPathRepeat (tabAt s).fst (tabAt s).snd.fst)
(h : (tabAt s).snd.snd = Tableau.rep lpr)
:
(nodeAt (companionOf s lpr h)).setEqTo (nodeAt s)
theorem
companionOf_length_lt_length
{a✝ : Sequent}
{tab : Tableau [] a✝}
{t : PathIn tab}
(lpr : LoadedPathRepeat (tabAt t).fst (tabAt t).snd.fst)
(h : (tabAt t).snd.snd = Tableau.rep lpr)
:
(companionOf t lpr h).length < t.length
The companion is strictly before the the repeat.
Equations
- «term_◃_» = Lean.ParserDescr.trailingNode `«term_◃_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 1023))
Instances For
Equations
- «term_◃⁺_» = Lean.ParserDescr.trailingNode `«term_◃⁺_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃⁺ ") (Lean.ParserDescr.cat `term 1023))
Instances For
Equations
- «term_◃*_» = Lean.ParserDescr.trailingNode `«term_◃*_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃* ") (Lean.ParserDescr.cat `term 1023))
Instances For
≡ᶜ and Clusters #
Equations
- «term_≡ᶜ_» = Lean.ParserDescr.trailingNode `«term_≡ᶜ_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ᶜ ") (Lean.ParserDescr.cat `term 1023))
Instances For
We have before s t iff there is a path from s to t but not from t to s.
This means the cluster of s comes before the cluster of t in tab.
NB: The notes use ◃* here but we use ◃⁺. The definitions are equivalent.
Instances For
s <ᶜ t means there is a ◃-path from s to t but not from t to s.
This means t is simpler to deal with first.
Equations
- «term_<ᶜ_» = Lean.ParserDescr.trailingNode `«term_<ᶜ_» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ᶜ ") (Lean.ParserDescr.cat `term 1023))
Instances For
theorem
PathIn.before_leaf_inductionOn
{X : Sequent}
{tab : Tableau [] X}
(t : PathIn tab)
{motive : PathIn tab → Prop}
(leaf : ∀ {u : PathIn tab}, (nodeAt u).isFree = true → (¬∃ (s : PathIn tab), u ⋖_ s) → motive u)
(up : ∀ {u : PathIn tab}, (∀ {s : PathIn tab}, u <ᶜ s → motive s) → motive u)
:
motive t
Soundness #
@[simp]
theorem
Sequent.isFree_then_without_isFree
(LRO : Sequent)
:
LRO.isFree = true → ∀ (anf : AnyNegFormula), (LRO.without anf).isFree = true
Equations
- (~''(AnyFormula.normal φ)).in_side Side.LL (L, fst, snd) = ((~φ) ∈ L)
- (~''(AnyFormula.normal φ)).in_side Side.RR (fst, R, snd) = ((~φ) ∈ R)
- (~''(AnyFormula.loaded χ)).in_side Side.LL (fst, fst_1, O) = (O = some (Sum.inl (~'χ)))
- (~''(AnyFormula.loaded χ)).in_side Side.RR (fst, fst_1, O) = (O = some (Sum.inr (~'χ)))
Instances For
theorem
AnyNegFormula.in_side_of_setEqTo
{side : Side}
{X Y : Sequent}
(h : X.setEqTo Y)
{anf : AnyNegFormula}
:
anf.in_side side X ↔ anf.in_side side Y
@[simp]
theorem
Sequent.without_loaded_in_side_isFree
(LRO : Sequent)
(ξ : LoadFormula)
(side : Side)
:
(~''(AnyFormula.loaded ξ)).in_side side LRO → (LRO.without (~''(AnyFormula.loaded ξ))).isFree = true
theorem
localLoadedDiamond
(α : Program)
{X : Sequent}
(ltab : LocalTableau X)
{W : Type}
{M : KripkeModel W}
{v w : W}
(v_α_w : relate M α v w)
(v_t : (M, v)⊨X)
(ξ : AnyFormula)
{side : Side}
(negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X)
(w_nξ : (M, w)⊨~''ξ)
:
Helper to deal with local tableau in loadedDiamondPaths.
theorem
Sequent.isLoaded_of_negAnyFormula_loaded
{α : Program}
{ξ : AnyFormula}
{side : Side}
{X : Sequent}
(negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X)
:
theorem
Vector.my_cast_head
{α : Type u_1}
(n m : ℕ)
(v : List.Vector α n.succ)
(h : n = m)
:
(h ▸ v).head = v.head
theorem
Vector.my_cast_eq_val_head
{α : Type u_1}
(n m : ℕ)
(v : List.Vector α n.succ)
(h : n = m)
(h2 : ↑v ≠ [])
:
(h ▸ v).head = (↑v).head h2
theorem
Vector.my_cast_toList
{α : Type u_1}
(n m : ℕ)
(t : List α)
(ht : t.length = n)
(h : n = m)
:
t = List.Vector.toList (h ▸ ⟨t, ht⟩)
theorem
Vector.my_drop_succ_cons
{α : Type u_1}
{m n : ℕ}
(x : α)
(t : List α)
(h : (x :: t).length = n.succ)
(hyp : m < n)
:
let help := ⋯;
List.Vector.drop (m + 1) ⟨x :: t, h⟩ = ⋯ ▸ List.Vector.drop m ⟨t, ⋯⟩
theorem
Vector.get_succ_eq_head_drop
{α : Type u_1}
{n : ℕ}
{v : List.Vector α n.succ}
(k : Fin n)
(j : ℕ)
(h : n + 1 - (↑k + 1) = j + 1)
:
v.get k.succ = (h ▸ List.Vector.drop (↑k + 1) v).head
theorem
Vector.drop_get_eq_get_add'
{α : Type u_1}
{n i : ℕ}
(v : List.Vector α n)
(l r : ℕ)
{h : i = l + r}
{hi : i < n}
{hr : r < n - l}
:
v.get ⟨i, hi⟩ = (List.Vector.drop l v).get ⟨r, hr⟩
Generalized vesrion of Vector.drop_get_eq_get_add.
theorem
Vector.drop_get_eq_get_add
{α : Type u_1}
{n : ℕ}
(v : List.Vector α n)
(k : ℕ)
(i : Fin (n - k))
(still_lt : k + ↑i < n)
:
(List.Vector.drop k v).get i = v.get ⟨k + ↑i, still_lt⟩
A Vector analogue of List.getElem_drop.
theorem
Vector.drop_last_eq_last
{α : Type u_1}
{n : ℕ}
{v : List.Vector α n.succ}
(k : Fin n)
(j : ℕ)
(h : n.succ - (↑k + 1) = j.succ)
:
(h ▸ List.Vector.drop (↑k + 1) v).last = v.last
theorem
Vector.my_cast_heq
{α : Type u_1}
(n m : ℕ)
(h : n = m)
(v : List.Vector α n)
:
HEq (h ▸ v) v
theorem
boxes_true_at_k_of_Vector_rel
{W : Type}
{M : KripkeModel W}
(ξ : AnyFormula)
(δ : List Program)
(h : ¬δ = [])
(ws : List.Vector W δ.length.succ)
(ws_rel : ∀ (i : Fin δ.length), relate M (δ.get i) (ws.get ↑↑i) (ws.get i.succ))
(k : Fin δ.length)
(w_nξ : (M, ws.last)⊨~''ξ)
:
(M, ws.get k.succ)⊨~''(AnyFormula.loadBoxes (List.drop (↑k.succ) δ) ξ)
@[irreducible]
theorem
loadedDiamondPaths
(α : Program)
{X : Sequent}
(tab : Tableau [] X)
(root_free : X.isFree = true)
(t : PathIn tab)
{W : Type}
{M : KripkeModel W}
{v w : W}
(v_t : (M, v)⊨nodeAt t)
(ξ : AnyFormula)
{side : Side}
(negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side (nodeAt t))
(v_α_w : relate M α v w)
(w_nξ : (M, w)⊨~''ξ)
:
Soundness of loading and repeats: a tableau can immitate all moves in a model.