Library filters
A proof that every filter F over a countable boolean algebra can
be extended to a complete filter equiconsistent with
F. (Ultrafilter Theorem)
This file is used by the completeness theorem from classcomp.v, but
it can be used in other contexts, it is a standalone module. It
also includes an instantiation of the ring tactic with the
semi-ring boolean algebra.
From Stdlib Require Import Ring.
From Stdlib Require Import List.
From Stdlib Require Import Compare_dec.
From Stdlib Require Import Setoid.
From Stdlib Require Import Morphisms.
From Stdlib Require Import PeanoNat.
Set Implicit Arguments.
From Stdlib Require Import List.
From Stdlib Require Import Compare_dec.
From Stdlib Require Import Setoid.
From Stdlib Require Import Morphisms.
From Stdlib Require Import PeanoNat.
Set Implicit Arguments.
Definition of Countable Boolean Algebra (over a setoid)
Module Type CBA.
Parameter Inline B:Set.
Parameters (meet join:B → B → B)(bott top:B)(compl:B → B).
Parameter eq_B : B → B → Prop.
Notation "x == y" := (eq_B x y) (at level 70, no associativity).
Axiom eq_B_refl : reflexive B eq_B.
Axiom eq_B_symm : symmetric B eq_B.
Axiom eq_B_trans : transitive B eq_B.
Axiom eq_B_meet_morph : Proper (eq_B ==> eq_B ==> eq_B) meet.
Axiom eq_B_join_morph : Proper (eq_B ==> eq_B ==> eq_B) join.
Axiom enum : B → nat.
Axiom countable : ∀ x y, enum x = enum y → x = y.
Axiom meet_idem : ∀ x, meet x x == x.
Axiom join_idem : ∀ x, join x x == x.
Axiom meet_comm : ∀ x y, meet x y == meet y x.
Axiom join_comm : ∀ x y, join x y == join y x.
Axiom meet_assoc : ∀ x y z, meet x (meet y z) == meet (meet x y) z.
Axiom join_assoc : ∀ x y z, join x (join y z) == join (join x y) z.
Axiom meet_absorb : ∀ x y, meet x (join x y) == x.
Axiom join_absorb : ∀ x y, join x (meet x y) == x.
Axiom meet_distrib : ∀ x y z,
meet (join x y) z == join (meet x z) (meet y z).
Axiom join_distrib : ∀ x y z,
join (meet x y) z == meet (join x z) (join y z).
Axiom meet_bott : ∀ x, meet bott x == bott.
Axiom join_bott : ∀ x, join bott x == x.
Axiom meet_top : ∀ x, meet top x == x.
Axiom join_top : ∀ x, join top x == top.
Axiom meet_compl : ∀ x, meet x (compl x) == bott.
Axiom join_compl : ∀ x, join x (compl x) == top.
Parameter Inline B:Set.
Parameters (meet join:B → B → B)(bott top:B)(compl:B → B).
Parameter eq_B : B → B → Prop.
Notation "x == y" := (eq_B x y) (at level 70, no associativity).
Axiom eq_B_refl : reflexive B eq_B.
Axiom eq_B_symm : symmetric B eq_B.
Axiom eq_B_trans : transitive B eq_B.
Axiom eq_B_meet_morph : Proper (eq_B ==> eq_B ==> eq_B) meet.
Axiom eq_B_join_morph : Proper (eq_B ==> eq_B ==> eq_B) join.
Axiom enum : B → nat.
Axiom countable : ∀ x y, enum x = enum y → x = y.
Axiom meet_idem : ∀ x, meet x x == x.
Axiom join_idem : ∀ x, join x x == x.
Axiom meet_comm : ∀ x y, meet x y == meet y x.
Axiom join_comm : ∀ x y, join x y == join y x.
Axiom meet_assoc : ∀ x y z, meet x (meet y z) == meet (meet x y) z.
Axiom join_assoc : ∀ x y z, join x (join y z) == join (join x y) z.
Axiom meet_absorb : ∀ x y, meet x (join x y) == x.
Axiom join_absorb : ∀ x y, join x (meet x y) == x.
Axiom meet_distrib : ∀ x y z,
meet (join x y) z == join (meet x z) (meet y z).
Axiom join_distrib : ∀ x y z,
join (meet x y) z == meet (join x z) (join y z).
Axiom meet_bott : ∀ x, meet bott x == bott.
Axiom join_bott : ∀ x, join bott x == x.
Axiom meet_top : ∀ x, meet top x == x.
Axiom join_top : ∀ x, join top x == top.
Axiom meet_compl : ∀ x, meet x (compl x) == bott.
Axiom join_compl : ∀ x, join x (compl x) == top.
We also need that identity id_B is decidable in 1 place. Note
that this id_B is definitional equality, it has nothing to do
with the equality of the setoid.
Axiom id_B_dec : ∀ x y : B, {x = y}+{x ≠ y}.
Axiom id_B_dec_right : ∀ (x y:B), x≠y →
∃ H:x≠y, id_B_dec x y = right (x=y) H.
Axiom id_B_dec_left : ∀ x:B,
∃ H:x=x, id_B_dec x x = left (x≠x) H.
End CBA.
Module filter_completion (cba : CBA).
Export cba.
Add Relation B eq_B
reflexivity proved by eq_B_refl
symmetry proved by eq_B_symm
transitivity proved by eq_B_trans
as eq_B_relation.
Add Morphism meet with signature eq_B ==> eq_B ==> eq_B as meet_morphism.
Qed.
Add Morphism join with signature eq_B ==> eq_B ==> eq_B as join_morphism.
Qed.
Axiom id_B_dec_right : ∀ (x y:B), x≠y →
∃ H:x≠y, id_B_dec x y = right (x=y) H.
Axiom id_B_dec_left : ∀ x:B,
∃ H:x=x, id_B_dec x x = left (x≠x) H.
End CBA.
Module filter_completion (cba : CBA).
Export cba.
Add Relation B eq_B
reflexivity proved by eq_B_refl
symmetry proved by eq_B_symm
transitivity proved by eq_B_trans
as eq_B_relation.
Add Morphism meet with signature eq_B ==> eq_B ==> eq_B as meet_morphism.
Qed.
Add Morphism join with signature eq_B ==> eq_B ==> eq_B as join_morphism.
Qed.
A boolean algebra is also a semi-ring, useful because Coq can
automatically solve equations in such cases.
Theorem CBA_semiring : semi_ring_theory bott top join meet eq_B.
Add Ring B_semiring : CBA_semiring.
Add Ring B_semiring : CBA_semiring.
Lattice as an algebra is equivalent to a lattice as a poset, so
we can define an ordering.
Definition leq := fun x y ⇒ meet x y == x.
Lemma leq' : ∀ x y, leq x y ↔ join x y == y.
Declare Scope B_scope.
Bind Scope B_scope with B.
Open Scope B_scope.
Notation "x && y" := (meet x y) (at level 40, left associativity) : B_scope.
Notation "- x" := (compl x) (at level 35, right associativity) : B_scope.
Notation "x || y" := (join x y) (at level 50, left associativity) : B_scope.
Notation "x <= y" := (leq x y) : B_scope.
Lemma leq' : ∀ x y, leq x y ↔ join x y == y.
Declare Scope B_scope.
Bind Scope B_scope with B.
Open Scope B_scope.
Notation "x && y" := (meet x y) (at level 40, left associativity) : B_scope.
Notation "- x" := (compl x) (at level 35, right associativity) : B_scope.
Notation "x || y" := (join x y) (at level 50, left associativity) : B_scope.
Notation "x <= y" := (leq x y) : B_scope.
When a subset F of B is a filter
Record Filter (F:B → Prop) : Prop := {
nonempty : ∃ x:B, F x;
upwards_closed : ∀ x y:B, F x → leq x y → F y;
meet_closed : ∀ x y:B, F x → F y → F (meet x y)
}.
nonempty : ∃ x:B, F x;
upwards_closed : ∀ x y:B, F x → leq x y → F y;
meet_closed : ∀ x y:B, F x → F y → F (meet x y)
}.
The closure of the subset X, up X, is the least filter containing X.
Conjuction of finite (but arbitrary) lenght is represented by the
List operation fold_left.
Definition up (X:B → Prop) := fun z:B ⇒
∃ n:nat, ∃ ys:list B, length ys = n ∧
fold_left (fun (a:Prop)(b:B) ⇒ and a (X b)) ys True ∧
leq (fold_left meet ys top) z.
Definition union_singl (F:B → Prop)(x:B) := fun b:B ⇒ F b ∨ b=x.
Definition inconsistent (F:B → Prop) := F bott.
Definition equiconsistent (F G:B → Prop) := inconsistent F ↔ inconsistent G.
Definition element_complete (F:B → Prop)(x:B) :=
equiconsistent F (up (union_singl F x)) → F x.
∃ n:nat, ∃ ys:list B, length ys = n ∧
fold_left (fun (a:Prop)(b:B) ⇒ and a (X b)) ys True ∧
leq (fold_left meet ys top) z.
Definition union_singl (F:B → Prop)(x:B) := fun b:B ⇒ F b ∨ b=x.
Definition inconsistent (F:B → Prop) := F bott.
Definition equiconsistent (F G:B → Prop) := inconsistent F ↔ inconsistent G.
Definition element_complete (F:B → Prop)(x:B) :=
equiconsistent F (up (union_singl F x)) → F x.
This notion of completeness of a filter is the key to having a
constructive proof. This notion is constructivelly weaker than,
but classically equivalent to, the more usual notion: either x
in F, or ~x in F.
Definition complete (F:B → Prop) := ∀ x:B, element_complete F x.
Lemma leq_refl : ∀ x:B, x ≤ x.
Lemma leq_trans : ∀ x y z:B, leq x y → leq y z → leq x z.
Lemma eq_B_leq : ∀ x y:B, x==y → x ≤ y.
Add Morphism leq with signature eq_B ==> eq_B ==> iff as leq_morphism.
Lemma meet_leq_compat : ∀ a b c d, a ≤ b → c ≤ d → a && c ≤ b && d.
Lemma leq_refl : ∀ x:B, x ≤ x.
Lemma leq_trans : ∀ x y z:B, leq x y → leq y z → leq x z.
Lemma eq_B_leq : ∀ x y:B, x==y → x ≤ y.
Add Morphism leq with signature eq_B ==> eq_B ==> iff as leq_morphism.
Lemma meet_leq_compat : ∀ a b c d, a ≤ b → c ≤ d → a && c ≤ b && d.
The next few lemmas with names "fold_left*" and "lemma*" are
used to handle the representation of a finite number of
conjunctions by a list.
Lemma fold_left_meet_morphism : ∀ x y bs, x==y →
fold_left meet bs x == fold_left meet bs y.
Lemma fold_left_meet_cons : ∀ bs b, fold_left meet (cons b bs) top == b && (fold_left meet bs top).
Lemma fold_left_impl : ∀ (X:B → Prop)(xs:list B)(Q P:Prop), (Q → P) → fold_left (fun (a : Prop) (b : B) ⇒ a ∧ X b) xs Q → fold_left (fun (a : Prop) (b : B) ⇒ a ∧ X b) xs P.
Lemma fold_left_app_lem : ∀ xs ys,
fold_left meet (xs ++ ys) top ==
fold_left meet xs top && fold_left meet ys top.
Lemma up_filter : ∀ X:B → Prop, Filter (up X).
Lemma filter_top : ∀ F:B → Prop, Filter F → F top.
Lemma lemma3 : ∀ (T:Type)(Hdec:∀ x y : T, {x = y} + {x ≠ y})(x:T)(ys:list T),
incl ys (x :: remove Hdec x ys).
Lemma lemma2 : ∀ A C:list B, incl A C →
leq (fold_left meet C top) (fold_left meet A top).
Lemma filter_memb_morph : ∀ F, Filter F →
∀ (x y:B), x==y → F x → F y.
Lemma lemma4 : ∀ xs F, Filter F →
fold_left (fun (A : Prop) (b : B) ⇒ A ∧ F b) xs True →
F (fold_left meet xs top).
Lemma lemma61 : ∀ (f:B → Prop)(l:list B)(basecase:Prop)(P:Prop),
fold_left (fun (R:Prop)(x:B) ⇒ R ∧ (f x)) l (basecase ∧ P) →
(fold_left (fun (R:Prop)(x:B) ⇒ R ∧ (f x)) l basecase) ∧ P.
Lemma lemma62 : ∀ (f:B → Prop)(l:list B)(basecase:Prop)(P:Prop),
(fold_left (fun (R:Prop)(x:B) ⇒ R ∧ (f x)) l basecase) ∧ P →
fold_left (fun (R:Prop)(x:B) ⇒ R ∧ (f x)) l (basecase ∧ P).
Lemma lemma5 (X:B → Prop)(ys:list B)(n:nat)
(H:fold_left (fun (P : Prop) (x : B) ⇒ P ∧ (X x ∨
(enum x = n ∧ equiconsistent X (up (union_singl X x))))) ys True) :
fold_left (fun (P : Prop) (x : B) ⇒ P ∧ X x) ys True ∨
(∃ x_n : B,
In x_n ys ∧
n = enum x_n ∧
fold_left (fun (P : Prop) (x : B) ⇒ P ∧ X x) (remove id_B_dec x_n ys) True ∧
equiconsistent X (up (union_singl X x_n))
).
Section completion.
This is the heart of the argument, a fixpoint that, starting
from a filter F, builds a complete filter extending F and
equiconsistent to F.
Variable F:B → Prop.
Fixpoint F_ (n':nat) {struct n'} :=
match n' with
| (S n) ⇒
let Fn := F_ n in
let X := fun b:B ⇒ Fn b ∨
(enum b=n ∧ equiconsistent Fn (up (union_singl Fn b)))
in up X
| O ⇒ F
end.
Definition Z := fun b:B ⇒ ∃ n:nat, (F_ n) b.
Lemma lem223 : ∀ (X:B → Prop) x, X x → (up X) x.
Lemma lem222 : ∀ n m, (n ≤ m)%nat → ∀ x, (F_ n) x → (F_ m) x.
Theorem thm22 : Filter F →
Filter Z ∧ equiconsistent F Z ∧ complete Z.
End completion.
Fixpoint F_ (n':nat) {struct n'} :=
match n' with
| (S n) ⇒
let Fn := F_ n in
let X := fun b:B ⇒ Fn b ∨
(enum b=n ∧ equiconsistent Fn (up (union_singl Fn b)))
in up X
| O ⇒ F
end.
Definition Z := fun b:B ⇒ ∃ n:nat, (F_ n) b.
Lemma lem223 : ∀ (X:B → Prop) x, X x → (up X) x.
Lemma lem222 : ∀ n m, (n ≤ m)%nat → ∀ x, (F_ n) x → (F_ m) x.
Theorem thm22 : Filter F →
Filter Z ∧ equiconsistent F Z ∧ complete Z.
End completion.
Some additional lemmas that are needed by classcomp.v
Section additional_lemmas.
Lemma lemma8 : ∀ (X:B → Prop)(f:B)(ys:list B),
fold_left (fun (a : Prop) (b : B) ⇒ a ∧ (union_singl X f) b) ys True →
fold_left (fun (a : Prop) (b : B) ⇒ a ∧ X b) ys True ∨
fold_left (fun (a : Prop) (b : B) ⇒ a ∧ X b)
(remove id_B_dec f ys) True
.
Lemma leq_bott : ∀ x:B, leq bott x.
End additional_lemmas.
End filter_completion.
Lemma lemma8 : ∀ (X:B → Prop)(f:B)(ys:list B),
fold_left (fun (a : Prop) (b : B) ⇒ a ∧ (union_singl X f) b) ys True →
fold_left (fun (a : Prop) (b : B) ⇒ a ∧ X b) ys True ∨
fold_left (fun (a : Prop) (b : B) ⇒ a ∧ X b)
(remove id_B_dec f ys) True
.
Lemma leq_bott : ∀ x:B, leq bott x.
End additional_lemmas.
End filter_completion.
This page has been generated by coqdoc