Helpers for Decidability / Model Checking

This file does not import anything and thus is not specifically about Gossip.

theorem exists_in_all_iff_exists {α : Type u_1} {all : List α} (all_spec : ∀ (x : α), x ∈ all) {P : α → Prop} : (∃ (x : α), x ∈ all ∧ P x) ↔ ∃ (x : α), P x

def Decidable.exists_of_list_mem {α : Type u_1} {all : List α} (all_spec : ∀ (x : α), x ∈ all) {P : α → Prop} (h : DecidablePred P) : Decidable (∃ (x : α), P x)

Equations

• Decidable.exists_of_list_mem all_spec h = decidable_of_iff (∃ (x : α), x ∈ all ∧ P x) ⋯

theorem forall_in_all_iff_forall {α : Type u_1} {all : List α} (all_spec : ∀ (x : α), x ∈ all) {P : α → Prop} : (∀ (x : α), x ∈ all → P x) ↔ ∀ (x : α), P x

def Decidable.forall_of_list_mem {α : Type u_1} {all : List α} (all_spec : ∀ (x : α), x ∈ all) {P : α → Prop} (h : DecidablePred P) : Decidable (∀ (x : α), P x)

Equations

• Decidable.forall_of_list_mem all_spec h = decidable_of_iff (∀ (x : α), x ∈ all → P x) ⋯

def Decidable.forall_implies_of_list_mem {α : Type u_1} {P Q : α → Prop} (all : List α) (all_spec : ∀ (x : α), Q x ↔ x ∈ all) (h : DecidablePred P) : Decidable (∀ (x : α), Q x → P x)

Equations

• Decidable.forall_implies_of_list_mem all all_spec h = decidable_of_iff (∀ (x : α), x ∈ all → P x) ⋯

def Decidable.forall_attach_list {α : Type u_1} {L : List α} {P : { x : α // x ∈ L } → Prop} (h : DecidablePred P) : Decidable (∀ (x : α) (h : x ∈ L), P ⟨x, h⟩)

Equations

• Decidable.forall_attach_list h = decidable_of_iff (∀ (x : { x : α // x ∈ L }), x ∈ L.attach → P x) ⋯