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 List.
From Stdlib Require Import Compare_dec.
From Stdlib Require Import Setoid.
From Stdlib Require Import CMorphisms.
From Stdlib Require Import PeanoNat.
Require Import ListSet.
Require Extraction.
Set Implicit Arguments.
From Stdlib Require Import Compare_dec.
From Stdlib Require Import Setoid.
From Stdlib Require Import CMorphisms.
From Stdlib Require Import PeanoNat.
Require Import ListSet.
Require Extraction.
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 → Set.
Notation "x == y" := (eq_B x y) (at level 70, no associativity).
Axiom eq_B_refl : Reflexive eq_B.
Axiom eq_B_symm : Symmetric eq_B.
Axiom eq_B_trans : Transitive 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 → Set.
Notation "x == y" := (eq_B x y) (at level 70, no associativity).
Axiom eq_B_refl : Reflexive eq_B.
Axiom eq_B_symm : Symmetric eq_B.
Axiom eq_B_trans : Transitive 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}.
End CBA.
Module filter_completion (cba : CBA).
Export cba.
Instance eq_B_relation : @Equivalence B eq_B.
Instance meet_morphism : Proper (eq_B ==> eq_B ==> eq_B) meet.
Instance join_morphism : Proper (eq_B ==> eq_B ==> eq_B) join.
End CBA.
Module filter_completion (cba : CBA).
Export cba.
Instance eq_B_relation : @Equivalence B eq_B.
Instance meet_morphism : Proper (eq_B ==> eq_B ==> eq_B) meet.
Instance join_morphism : Proper (eq_B ==> eq_B ==> eq_B) join.
A boolean algebra is also a semi-ring, useful because Coq can
automatically solve equations in such cases.
However, Add Ring does not work for equivalence relations not
in Prop, so we do not use it anymore.
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.
Definition ciff (A B:Set) : Set := (A → B) × (B → A).
Lemma leq' : ∀ x y, ciff (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.
Definition ciff (A B:Set) : Set := (A → B) × (B → A).
Lemma leq' : ∀ x y, ciff (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 → Set) : Set := {
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 → Set) := fun z:B ⇒
{n:nat & {ys:list B & (length ys = n) ×
(fold_left (fun (a:Set)(b:B) ⇒ prod a (X b)) ys unit ×
leq (fold_left meet ys top) z)}}%type.
Definition union_singl (F:B → Set)(x:B) := fun b:B ⇒ (F b + {b=x})%type.
Definition inconsistent (F:B → Set) := F bott.
Definition equiconsistent (F G:B → Set) :=
((inconsistent F → inconsistent G) × (inconsistent G → inconsistent F))%type.
Definition element_complete (F:B → Set)(x:B) :=
equiconsistent F (up (union_singl F x)) → F x.
{n:nat & {ys:list B & (length ys = n) ×
(fold_left (fun (a:Set)(b:B) ⇒ prod a (X b)) ys unit ×
leq (fold_left meet ys top) z)}}%type.
Definition union_singl (F:B → Set)(x:B) := fun b:B ⇒ (F b + {b=x})%type.
Definition inconsistent (F:B → Set) := F bott.
Definition equiconsistent (F G:B → Set) :=
((inconsistent F → inconsistent G) × (inconsistent G → inconsistent F))%type.
Definition element_complete (F:B → Set)(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 → Set) := ∀ 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.
Instance leq_morphism : Proper (eq_B ==> eq_B ==> ciff) leq.
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.
Instance leq_morphism : Proper (eq_B ==> eq_B ==> ciff) leq.
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 → Set)(xs:list B)(Q P:Set), (Q → P) → fold_left (fun (a : Set) (b : B) ⇒ (a × X b)%type) xs Q → fold_left (fun (a : Set) (b : B) ⇒ (a × X b)%type) 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, Filter (up X).
Lemma filter_top : ∀ F, Filter F → F top.
Lemma lemma3 : ∀ (T:Set)(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 : Set) (b : B) ⇒ (A × F b)%type) xs unit →
F (fold_left meet xs top).
Open Scope type.
Lemma lemma61 : ∀ (f:B → Set)(l:list B)(basecase:Set)(P:Set),
fold_left (fun (R:Set)(x:B) ⇒ R × (f x)) l (basecase × P) →
(fold_left (fun (R:Set)(x:B) ⇒ R × (f x)) l basecase) × P.
Lemma lemma62 : ∀ (f:B → Set)(l:list B)(basecase:Set)(P:Set),
(fold_left (fun (R:Set)(x:B) ⇒ R × (f x)) l basecase) × P →
fold_left (fun (R:Set)(x:B) ⇒ R × (f x)) l (basecase × P).
Lemma lemma5 (X:B → Set)(ys:list B)(n:nat)
(H:fold_left (fun (P : Set) (x : B) ⇒ P × (X x +
((enum x = n) × equiconsistent X (up (union_singl X x))))) ys unit) :
fold_left (fun (P : Set) (x : B) ⇒ P × X x) ys unit +
{x_n : B &
In x_n ys ×
((n = enum x_n) ×
(fold_left (fun (P : Set) (x : B) ⇒ P × X x) (remove id_B_dec x_n ys) unit ×
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 → Set.
Open Scope type.
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 → Set) x, X x → (up X) x.
Inductive le (n0 : nat) : nat → Set :=
le_n : (le n0 n0)%nat | le_S : ∀ m : nat, (le n0 m)%nat → (le n0 (S m))%nat.
Definition lt := (fun n m : nat ⇒ (le (S n) m))
: nat → nat → Set.
Lemma le_lt_dec : ∀ n m, le n m + lt m n.
Lemma lt_le_incl : ∀ n m : nat, (lt n m) → (le n m).
Lemma lem222 : ∀ n m, (le n m)%nat → ∀ x, (F_ n) x → (F_ m) x.
Theorem thm22 : Filter F →
Filter Z × (equiconsistent F Z × complete Z).
End completion.
Open Scope type.
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 → Set) x, X x → (up X) x.
Inductive le (n0 : nat) : nat → Set :=
le_n : (le n0 n0)%nat | le_S : ∀ m : nat, (le n0 m)%nat → (le n0 (S m))%nat.
Definition lt := (fun n m : nat ⇒ (le (S n) m))
: nat → nat → Set.
Lemma le_lt_dec : ∀ n m, le n m + lt m n.
Lemma lt_le_incl : ∀ n m : nat, (lt n m) → (le n m).
Lemma lem222 : ∀ n m, (le 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 → Set)(f:B)(ys:list B),
fold_left (fun (a : Set) (b : B) ⇒ a × (union_singl X f) b) ys unit →
fold_left (fun (a : Set) (b : B) ⇒ a × X b) ys unit +
fold_left (fun (a : Set) (b : B) ⇒ a × X b)
(remove id_B_dec f ys) unit
.
Lemma leq_bott : ∀ x:B, leq bott x.
End additional_lemmas.
Extraction "filters" thm22.
End filter_completion.
Lemma lemma8 : ∀ (X:B → Set)(f:B)(ys:list B),
fold_left (fun (a : Set) (b : B) ⇒ a × (union_singl X f) b) ys unit →
fold_left (fun (a : Set) (b : B) ⇒ a × X b) ys unit +
fold_left (fun (a : Set) (b : B) ⇒ a × X b)
(remove id_B_dec f ys) unit
.
Lemma leq_bott : ∀ x:B, leq bott x.
End additional_lemmas.
Extraction "filters" thm22.
End filter_completion.
This page has been generated by coqdoc