The construction of the least closure operator that forces a given predicate to be true.

forcing.v

(* A proof that there is a least closure operator which forces a given
   predicate to be true. The construction can be found in, e.g.,
   Martin Hyland's “Effective topos” paper, Proposition 16.3. *)

(* A closure operator on [Prop] is an idempotent, monotone, inflationary enodmap.

   One often requires additionally that the operator preserves conjunctions,
   in which case these are also called j-operators and Lawvere-Tierney topologies.
   We eschew the condition to obtain a slighly more general result, but we
   also show that the closure operator of interst happens to preserve conjunctions.
*)

Require Import Utf8.

Structure Closure := {
  j :> Prop → Prop ;
  j_monotone : ∀ p q, (p → q) → j p → j q ;
  j_inflationary : ∀ p, p → j p ;
  j_idempotent : ∀ p, j (j p) → j p ;
}.

Section Forcing.

  (* Suppose [P] is a predicate on [A]. *)
  Variable (A : Type).
  Variable (P : A → Prop).

  (* The underlying map of the least operator that forces [P] to be the top predicate. *)
  Definition force (p : Prop) : Prop :=
    ∀ (r : Prop), (p → r) → (∀ a, (P a → r) → r) → r.

  (* It actually forced [P]. *)
  Theorem force_forces: ∀ a, force (P a).
  Proof.
    intros b r H G.
    exact (G b H).
  Qed.


  (* It is a monotone operator. *)
  Lemma force_monotone p q: (p → q) → force p → force q.
  Proof.
    intros pq jp r qr H.
    apply jp ; auto.
  Qed.

  (* It is a closure operator. *)
  Definition Force : Closure.
  Proof.
    exists force.
    - apply force_monotone.
    - firstorder.
    - intros p jjp r pr H.
      apply jjp.
      + intro G.
        exact (G _ pr H).
      + assumption.
  Defined.

  (* It is the least closure operator forcing [P]. *)
  Theorem force_least (j : Closure) :
    (∀ a, j (P a)) → ∀ p, force p → j p.
  Proof.
    intros H p fPp.
    apply fPp.
    - apply j_inflationary.
    - intros a G.
      apply j_idempotent.
      now apply j_monotone with (p := P a).
  Qed.

  (* It preserves conjunctions. *)
  Lemma force_lexp p q : force p ∧ force q ↔ force (p ∧ q).
  Proof.
    split.
    - intros [jp jq] r pqr H.
      apply jq.
      + intro G.
        apply jp.
        * tauto.
        * assumption.
      + assumption.
    - intro H.
      split ; generalize H ; now apply force_monotone.
  Qed.

End Forcing.


Section ForcingProp.

  (* As a special case of the above, here is forcing of a proposition. *)

  (* Suppose [p] is a proposition, which we wish to force. *)
  Variable p : Prop.

  Definition forceProp : Closure.
  Proof.
    exists (fun q => ∀ (r : Prop), (q → r) → ((p → r) → r) → r).
    - intros q r qr H r' rr' G.
      apply H ; tauto.
    - intros q H r qr G ; tauto.
    - intros q H r qr G.
      + apply H.
        intro L.
        * exact (L _ qr G).
        * assumption.
  Qed.

End ForcingProp.