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.
Require Import Ring.
Require Import List.
Require Import Compare_dec.
Require Import Setoid.
Require Import Morphisms.


Definition of Countable Boolean Algebra (over a setoid)
Module Type CBA.
  Parameter Inline B:Set.
  Parameters (meet join:B → BB)(bott top:B)(compl:B → B).
  Parameter eq_B : BBProp.

  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 : Morphism (eq_Beq_Beq_B) meet.
  Axiom eq_B_join_morph : Morphism (eq_Beq_Beq_B) join.

  Axiom enum : Bnat.
  Axiom countable : ∀ x y, enum x = enum yx = 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 is not that 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_Beq_Beq_B as meet_morphism.
  Qed.

  Add Morphism join with signature eq_Beq_Beq_B as join_morphism.
  Qed.

A boolean algebra is also a semi-ring, useful because Coq can automatically solve equations for in such cases.
  Theorem CBA_semiring : semi_ring_theory bott top join meet eq_B.

  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 ymeet x y == x.

  Lemma leq' : ∀ x y, leq x yjoin x y == y.

  Delimit 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 xleq x yF y;
    meet_closed : ∀ x y:B, F xF yF (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 bb=x.

  Definition inconsistent (F:B → Prop) := F bott.

  Definition equiconsistent (F G:B → Prop) := inconsistent Finconsistent 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, xx.

  Lemma leq_trans : ∀ x y z:B, leq x yleq y zleq x z.

  Lemma eq_B_leq : ∀ x y:B, x==y → xy.

  Add Morphism leq with signature eq_Beq_Biff as leq_morphism.

  Lemma meet_leq_compat : ∀ a b c d, abcda && cb && 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), (QP) → fold_left (fun (a : Prop) (b : B) ⇒ aX b) xs Qfold_left (fun (a : Prop) (b : B) ⇒ aX 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 FF top.

  Lemma lemma3 : ∀ (T:Type)(Hdec:forall x y : T, {x = y} + {xy})(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 xF y.

  Lemma lemma4 : ∀ xs F, Filter F
    fold_left (fun (A : Prop) (b : B) ⇒ AF 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 (basecaseP) →
    (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 (basecaseP).

  Lemma lemma5 (X:B → Prop)(ys:list B)(n:nat)
    (H:fold_left (fun (P : Prop) (x : B) ⇒ P ∧ (X x
      (enum x = nequiconsistent X (up (union_singl X x))))) ys True) :
    fold_left (fun (P : Prop) (x : B) ⇒ PX x) ys True
    (∃ x_n : B,
      In x_n ys
      n = enum x_n
      fold_left (fun (P : Prop) (x : B) ⇒ PX x) (remove id_B_dec x_n ys) True
      equiconsistent X (up (union_singl X x_n))
    ).

  Section completion.

This is the hearth 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
      | OF
    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, (nm)%nat → ∀ x, (F_ n) x → (F_ m) x.

  Theorem thm22 : Filter F
    Filter Zequiconsistent F Zcomplete 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) ⇒ aX b) ys True
      fold_left (fun (a : Prop) (b : B) ⇒ aX 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