(Big) Disjunction and Conjunction

Here we define ⋀ and ⋁ on formulas and seveal helper lemmas.

Conjunction

def PDL.con : List Formula → Formula

Conjunction of a list of formulas, with the empty conjunction equal to truth.

Equations

• PDL.con [] = ⊤
• PDL.con [f] = f
• PDL.con (f :: rest) = f.and (PDL.con rest)

theorem PDL.conempty : con ∅ = ⊤

@[simp]

theorem PDL.consingle {f : Formula} : con [f] = f

theorem PDL.listEq_to_conEq {l1 l2 : List Formula} : l1 = l2 → con l1 = con l2

theorem PDL.conEvalHT {X : List Formula} {f : Formula} {W : Type} {M : KripkeModel W} {w : W} : evaluate M w (con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (con X)

theorem PDL.conEval {W : Type} {M : KripkeModel W} {X : List Formula} {w : W} : evaluate M w (con X) ↔ ∀ f ∈ X, evaluate M w f

theorem PDL.in_voc_con (n : ℕ ⊕ ℕ) (L : List Formula) : n ∈ (con L).voc ↔ ∃ φ ∈ L, n ∈ φ.voc

Vocabulary of Conjunction

def Finset.pdlCon (X : Finset PDL.Formula) : PDL.Formula

The conjunction of a Finset of formulas, via Finset.pdlSort.

Equations

• X.pdlCon = PDL.con X.pdlSort

@[simp]

theorem PDL.Finset.con_empty : ∅.pdlCon = ⊤

@[simp]

theorem PDL.Finset.con_singleton {f : Formula} : {f}.pdlCon = f

theorem PDL.Finset.conEval {W : Type} {M : KripkeModel W} {X : Finset Formula} {w : W} : evaluate M w X.pdlCon ↔ ∀ f ∈ X, evaluate M w f

theorem PDL.evaluate_con_sort {W✝ : Type} {M : KripkeModel W✝} {w : W✝} (X : Finset Formula) : evaluate M w (con (X.sort fun (a b : Formula) => a ≤ b)) ↔ ∀ φ ∈ X, evaluate M w φ

Evaluating a conjunction does not care about sorting.

theorem PDL.Finset.in_voc_con (n : ℕ ⊕ ℕ) (X : Finset Formula) : n ∈ X.pdlCon.voc ↔ ∃ φ ∈ X, n ∈ φ.voc

Vocabulary of the conjunction of a Finset.

Disjunction

def PDL.dis : List Formula → Formula

Disjunction of a list of formulas, with the empty disjunction equal to falsity.

Equations

• PDL.dis [] = ⊥
• PDL.dis [f] = f
• PDL.dis (f :: rest) = f.or (PDL.dis rest)

@[simp]

theorem PDL.disempty : dis ∅ = ⊥

@[simp]

theorem PDL.dissingle {f : Formula} : dis [f] = f

theorem PDL.listEq_to_disEq {l1 l2 : List Formula} : l1 = l2 → dis l1 = dis l2

theorem PDL.disEvalHT {X : List Formula} {f : Formula} {W : Type} {M : KripkeModel W} {w : W} : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)

theorem PDL.disEval {W : Type} {M : KripkeModel W} {X : List Formula} {w : W} : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f

theorem PDL.in_voc_dis (n : ℕ ⊕ ℕ) (L : List Formula) : n ∈ (dis L).voc ↔ ∃ φ ∈ L, n ∈ φ.voc

Vocabulary of Disjunction

def Finset.pdlDis (X : Finset PDL.Formula) : PDL.Formula

The disjunction of a Finset of formulas, via Finset.pdlSort.

Equations

• X.pdlDis = PDL.dis X.pdlSort

@[simp]

theorem PDL.Finset.dis_empty : ∅.pdlDis = ⊥

@[simp]

theorem PDL.Finset.dis_singleton {f : Formula} : {f}.pdlDis = f

theorem PDL.Finset.disEval {W : Type} {M : KripkeModel W} {X : Finset Formula} {w : W} : evaluate M w X.pdlDis ↔ ∃ f ∈ X, evaluate M w f

theorem PDL.Finset.in_voc_dis (n : ℕ ⊕ ℕ) (X : Finset Formula) : n ∈ X.pdlDis.voc ↔ ∃ φ ∈ X, n ∈ φ.voc

Vocabulary of the disjunction of a Finset.

Disjunction of Conjunctions

def PDL.discon : List (List Formula) → Formula

Disjunction of the conjunctions represented by a list of formula lists.

Equations

• PDL.discon [] = ⊥
• PDL.discon [X] = PDL.con X
• PDL.discon (X :: rest) = (PDL.con X).or (PDL.discon rest)

theorem PDL.disconempty : discon {∅} = ⊤

@[simp]

theorem PDL.disconsingle {f : Formula} : discon [[f]] = f

theorem PDL.disconEvalHT {X : List Formula} (XS : List (List Formula)) : semEquiv (discon (X :: XS)) ((con X).or (discon XS))

theorem PDL.disconEval' {W : Type} {M : KripkeModel W} {w : W} {N : ℕ} (XS : List (List Formula)) : XS.length = N → (evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f)

Variant of disconEval for a specific length of XS to be provable by induction.

theorem PDL.disconEval {W : Type} {M : KripkeModel W} {w : W} (XS : List (List Formula)) : evaluate M w (discon XS) ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

theorem PDL.disconOr {XS YS : List (List Formula)} : semEquiv (discon (XS ∪ YS)) ((discon XS).or (discon YS))

Sorting lists of formulas

To also sort a Finset (Finset Formula) we need an order on List Formula. We use the lexicographic order List.le coming from the order on formulas.

TODO: these could be moved to Pdl.Syntax, next to Finset.pdlSort.

@[instance_reducible]

def PDL.Formula.linearOrder : LinearOrder Formula

The linear order on formulas, bundling the results from Pdl.Syntax. This is only used locally, to get the lexicographic order on List Formula.

Equations

• One or more equations did not get rendered due to their size.

theorem PDL.List.le_iff_le_formula (l1 l2 : List Formula) : l1.le l2 ↔ l1 ≤ l2

The lexicographic List.le on List Formula agrees with the ≤ coming from the linear order Formula.linearOrder.

@[instance_reducible]

instance PDL.instDecidableRelListFormulaLe : DecidableRel List.le

Equations

• PDL.instDecidableRelListFormulaLe l1 l2 = decidable_of_iff (l1 ≤ l2) ⋯

instance PDL.instIsTransListFormulaLe : IsTrans (List Formula) List.le

instance PDL.instAntisymmListFormulaLe : Std.Antisymm List.le

instance PDL.instTotalListFormulaLe : Std.Total List.le

def Finset.pdlDiscon : Finset (Finset PDL.Formula) → PDL.Formula

The disjunction of conjunctions given by a Finset (Finset Formula). The inner sets are sorted with Finset.pdlSort and the outer set is then sorted lexicographically with List.le.

Equations

• x✝.pdlDiscon = PDL.discon ((Finset.image Finset.pdlSort x✝).sort List.le)

theorem PDL.Finset.disconEval {W : Type} {M : KripkeModel W} {w : W} (XS : Finset (Finset Formula)) : evaluate M w XS.pdlDiscon ↔ ∃ Y ∈ XS, ∀ f ∈ Y, evaluate M w f

Pairwise Union

def PDL.pairunionList : List (List Formula) → List (List Formula) → List (List Formula)

All concatenations of one formula list from each input family.

Equations

• PDL.pairunionList x✝¹ x✝ = (List.map (fun (xl : List PDL.Formula) => List.map (fun (yl : List PDL.Formula) => xl ++ yl) x✝) x✝¹).flatten

def PDL.pairunionFinset : Finset (Finset Formula) → Finset (Finset Formula) → Finset (Finset Formula)

All unions of one formula finset from each input family.

Equations

• PDL.pairunionFinset x✝¹ x✝ = x✝¹.biUnion fun (ga : Finset PDL.Formula) => x✝.biUnion fun (gb : Finset PDL.Formula) => {ga ∪ gb}

class PDL.HasUplus (α : Type → Type) : Type

Containers supporting pairwise combination of families of formula collections.

• pairunion : α (α Formula) → α (α Formula) → α (α Formula)

  Combine every collection from the first family with every collection from the second.

def PDL.«term_⊎_» : Lean.TrailingParserDescr

Pairwise combination of two families of formula collections.

Equations

• PDL.«term_⊎_» = Lean.ParserDescr.trailingNode `PDL.«term_⊎_» 77 77 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊎") (Lean.ParserDescr.cat `term 78))

@[instance_reducible]

instance PDL.listHasUplus : HasUplus List

Equations

• PDL.listHasUplus = { pairunion := PDL.pairunionList }

@[instance_reducible]

instance PDL.finsetHasUplus : HasUplus Finset

Equations

• PDL.finsetHasUplus = { pairunion := PDL.pairunionFinset }

theorem PDL.disconAnd {XS YS : List (List Formula)} : semEquiv (discon (HasUplus.pairunion XS YS)) ((discon XS).and (discon YS))

theorem PDL.union_elem_uplus {XS YS : Finset (Finset Formula)} {X Y : Finset Formula} : X ∈ XS → Y ∈ YS → X ∪ Y ∈ HasUplus.pairunion XS YS

theorem PDL.mapCon_mapForall {W : Type} {X : List (List Formula × List Program)} (M : KripkeModel W) (w : W) (φ : Formula) (g : List Formula × List Program → Formula → List Formula) : (∃ f ∈ List.map (fun (Fδ : List Formula × List Program) => con (g Fδ φ)) X, evaluate M w f) ↔ ∃ fs ∈ List.map (fun (Fδ : List Formula × List Program) => g Fδ φ) X, ∀ f ∈ fs, evaluate M w f

Helper for oneSidedLocalRuleTruth, used with g = Yset.