(Big) Disjunction and Conjunction

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

Conjunction

def con : List Formula → Formula

Equations

• con [] = ⊤
• con [f] = f
• con (f :: rest) = f ⋀ con rest

@[simp]

theorem conempty : con ∅ = ⊤

@[simp]

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

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

theorem 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 conEval {W : Type} {M : KripkeModel W} {X : List Formula} {w : W} : evaluate M w (con X) ↔ ∀ f ∈ X, evaluate M w f

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

Vocabulary of Conjunction

def Finset.con (X : Finset Formula) : Formula

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

Equations

• X.con = con X.fsort

@[simp]

theorem Finset.con_empty : ∅.con = ⊤

@[simp]

theorem Finset.con_singleton {f : Formula} : {f}.con = f

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

theorem 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 Finset.in_voc_con (n : ℕ ⊕ ℕ) (X : Finset Formula) : n ∈ X.con.voc ↔ ∃ φ ∈ X, n ∈ φ.voc

Vocabulary of the conjunction of a Finset.

Disjunction

def dis : List Formula → Formula

Equations

• dis [] = ⊥
• dis [f] = f
• dis (f :: rest) = f ⋁ dis rest

@[simp]

theorem disempty : dis ∅ = ⊥

@[simp]

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

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

theorem 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 disEval {W : Type} {M : KripkeModel W} {X : List Formula} {w : W} : evaluate M w (dis X) ↔ ∃ f ∈ X, evaluate M w f

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

Vocabulary of Disjunction

def Finset.dis (X : Finset Formula) : Formula

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

Equations

• X.dis = dis X.fsort

@[simp]

theorem Finset.dis_empty : ∅.dis = ⊥

@[simp]

theorem Finset.dis_singleton {f : Formula} : {f}.dis = f

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

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

Vocabulary of the disjunction of a Finset.

Disjunction of Conjunctions

def discon : List (List Formula) → Formula

Equations

• discon [] = ⊥
• discon [X] = con X
• discon (X :: rest) = con X ⋁ discon rest

@[simp]

theorem disconempty : discon {∅} = ⊤

@[simp]

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

theorem disconEvalHT {X : List Formula} (XS : List (List Formula)) : discon (X :: XS) ≡ con X ⋁ discon XS

theorem 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 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 disconOr {XS YS : List (List Formula)} : discon (XS ∪ YS) ≡ discon XS ⋁ 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.fsort.

@[instance_reducible]

def 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 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 instDecidableRelListFormulaLe : DecidableRel List.le

Equations

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

instance instIsTransListFormulaLe : IsTrans (List Formula) List.le

instance instAntisymmListFormulaLe : Std.Antisymm List.le

instance instTotalListFormulaLe : Std.Total List.le

def Finset.discon : Finset (Finset Formula) → Formula

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

Equations

• x✝.discon = discon ((Finset.image Finset.fsort x✝).sort List.le)

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

Pairwise Union

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

Equations

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

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

Equations

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

class HasUplus (α : Type → Type) : Type

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

def «term_⊎_» : Lean.TrailingParserDescr

Equations

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

@[instance_reducible]

instance listHasUplus : HasUplus List

Equations

• listHasUplus = { pairunion := pairunionList }

@[instance_reducible]

instance finsetHasUplus : HasUplus Finset

Equations

• finsetHasUplus = { pairunion := pairunionFinset }

theorem disconAnd {XS YS : List (List Formula)} : discon (XS⊎YS) ≡ discon XS ⋀ discon YS

theorem union_elem_uplus {XS YS : Finset (Finset Formula)} {X Y : Finset Formula} : X ∈ XS → Y ∈ YS → X ∪ Y ∈ XS⊎YS

theorem 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.