Cardinality specification predicates

This file defines useful predicates for specifying the behavior of cardinality encodings.

def Trestle.Encode.Cardinality.card {ν : Type u_1} (lits : Multiset (Literal ν)) (τ : Model.PropAssignment ν) : ℕ

Equations

• Trestle.Encode.Cardinality.card lits τ = Multiset.countP (fun (x : Trestle.Literal ν) => τ ⊨ Trestle.LitVar.toPropFun x) lits

def Trestle.Encode.Cardinality.cardPred {ν : Type u_1} (lits : Multiset (Literal ν)) (P : ℕ → Prop) [DecidablePred P] (τ : Model.PropAssignment ν) : Prop

Equations

• Trestle.Encode.Cardinality.cardPred lits P τ = P (Trestle.Encode.Cardinality.card lits τ)

@[simp]

theorem Trestle.Encode.Cardinality.satisfies_cardPred {ν : Type u_1} (lits : Multiset (Literal ν)) (P : ℕ → Prop) [DecidablePred P] (τ : Model.PropAssignment ν) : cardPred lits P τ ↔ P (card lits τ)

@[reducible, inline]

abbrev Trestle.Encode.Cardinality.atMost {ν : Type u_1} (k : ℕ) (lits : Multiset (Literal ν)) (τ : Model.PropAssignment ν) : Prop

Equations

• Trestle.Encode.Cardinality.atMost k lits = Trestle.Encode.Cardinality.cardPred lits fun (x : ℕ) => x ≤ k

@[reducible, inline]

abbrev Trestle.Encode.Cardinality.atLeast {ν : Type u_1} (k : ℕ) (lits : Multiset (Literal ν)) (τ : Model.PropAssignment ν) : Prop

Equations

• Trestle.Encode.Cardinality.atLeast k lits = Trestle.Encode.Cardinality.cardPred lits fun (x : ℕ) => x ≥ k

@[reducible, inline]

abbrev Trestle.Encode.Cardinality.exactly {ν : Type u_1} (k : ℕ) (lits : Multiset (Literal ν)) (τ : Model.PropAssignment ν) : Prop

Equations

• Trestle.Encode.Cardinality.exactly k lits = Trestle.Encode.Cardinality.cardPred lits fun (x : ℕ) => x = k

@[reducible, inline]

abbrev Trestle.Encode.Cardinality.lessThan {ν : Type u_1} (k : ℕ) (lits : Multiset (Literal ν)) (τ : Model.PropAssignment ν) : Prop

Equations

• Trestle.Encode.Cardinality.lessThan k lits = Trestle.Encode.Cardinality.cardPred lits fun (x : ℕ) => x < k

theorem Trestle.Encode.Cardinality.ofList_eq_map_get {α : Type u_1} (L : List α) : ↑L = Multiset.map (fun (i : Fin L.length) => L.get i) Finset.univ.val

@[simp]

theorem Trestle.Encode.Cardinality.card_singleton' {ν : Type u_1} (l : Literal ν) : card ↑[l] = fun (τ : Model.PropAssignment ν) => if τ ⊨ LitVar.toPropFun l then 1 else 0

@[simp]

theorem Trestle.Encode.Cardinality.card_singleton {ν : Type u_1} (l : Literal ν) : card {l} = fun (τ : Model.PropAssignment ν) => if τ ⊨ LitVar.toPropFun l then 1 else 0

@[simp]

theorem Trestle.Encode.Cardinality.card_append {ν : Type u_1} (L₁ L₂ : List (Literal ν)) : card ↑(L₁ ++ L₂) = card ↑L₁ + card ↑L₂

@[simp]

theorem Trestle.Encode.Cardinality.card_cons {ν : Type u_1} (l : Literal ν) (L : List (Literal ν)) : card ↑(l :: L) = card ↑[l] + card ↑L

@[simp]

theorem Trestle.Encode.Cardinality.card_map {ν : Type u_1} {ν' : Type u_2} (L : List (Literal ν)) (f : ν → ν') (τ : Model.PropAssignment ν') : card (↑(List.map (LitVar.map f) L)) τ = card (↑L) (τ ∘ f)

theorem Trestle.Encode.Cardinality.card_eq_one {ν : Type u_1} {τ : Model.PropAssignment ν} (ls : Multiset (Literal ν)) (nodup : ls.Nodup) : card ls τ = 1 ↔ ∃! l : Literal ν, l ∈ ls ∧ τ ⊨ LitVar.toPropFun l