Require Import Setoid.
Require Import Orders.
Require Import Common.

Definition comp {A B C} (f : B -> C) (g : A -> B) := fun x => f (g x).
Infix "∘" := comp (at level 40, left associativity).

Class Glb {T : Type} {Tle} (glb : T -> T -> T) `{PreOrder T Tle} := {
  glb_lower1 : forall x y, Tle (glb x y) x;
  glb_lower2 : forall x y, Tle (glb x y) y;
  glb_greatest : forall x y z, Tle z x -> Tle z y -> Tle z (glb x y)}.


(*********************)
(** *  Definitions  **)
(*********************)


(** **  The parameters of the forcing translation  **)
(*      ¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨   *)

Module Type ForcingType.
  Parameter κ : Type.
  Parameter C : κ -> Prop.
  Parameter product : κ -> κ -> κ.
  Parameter one : κ.
  Bind Scope forcing_scope with κ.
  Delimit Scope forcing_scope with forcing.
  Open Scope forcing_scope.

  Notation "'C[' p ']'" := (C p%forcing).
  Notation "1" := one : forcing_scope.
  Notation "p · q" := (product p%forcing q%forcing)
    (at level 46, format "p '·' q", left associativity) : forcing_scope.

  Parameter α₀ : C[1].
  Parameter α₁ : forall {p q}, C[p·q] -> C[p].
  Parameter α₂ : forall {p q}, C[p·q] -> C[q].
  Parameter α₃ : forall {p q}, C[p·q] -> C[q·p].
  Parameter α₄ : forall {p}, C[p] -> C[p·p].
  Parameter α₅ : forall {p q r}, C[(p·q)·r] -> C[p·(q·r)].
  Parameter α₆ : forall {p q r}, C[p·(q·r)] -> C[(p·q)·r].
  Parameter α₇ : forall {p}, C[p] -> C[p·1].
  Parameter α₈ : forall {p}, C[p] -> C[1·p].
End ForcingType.


(** **  The construction of the forcing translation  **)
(*      ¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨   *)

Module Forcing (Def : ForcingType).

Import Def.

(** useful notations **)
Bind Scope forcing_scope with κ.
Delimit Scope forcing_scope with forcing.
Open Scope forcing_scope.

Notation "'C[' p ']'" := (C p%forcing).
Notation "1" := one : forcing_scope.
Notation "p · q" := (product p%forcing q%forcing)
  (at level 46, format "p '·' q", left associativity) : forcing_scope.

Set Implicit Arguments.

(** Derived combinators **)
(* (* To get the minimum number of primitive combinators. *)
Hint Resolve α₀ α₃ α₄ α₅ α₆ α₇ α₈ : alpha.
Hint Extern 1 C[_] => eapply α₁ : alpha.
Hint Extern 1 C[_] => eapply α₂ : alpha.
Definition α : forall p q r, C[(p·q)·r] -> C[q·r].
intros. info_eauto 7 with alpha. *)

Definition α₉ : forall p q r, C[(p·q)·r] -> C[p·r] := fun p q r Cpqr => α₃ (α₁ (α₆ (α₃ Cpqr))).
Definition α₁₀ : forall p q r, C[(p·q)·r] -> C[q·r] := fun p q r Cpqr => α₂ (α₅ Cpqr).
Definition α₁₁ : forall p q, C[p·q] -> C[p·(p·q)] := fun p q Cpq => α₃ (α₁ (α₆ (α₄ Cpq))).
Definition α₁₂ : forall p q r, C[p·(q·r)] -> C[q·(r·p)] := fun p q r Cpqr => α₅ (α₃ Cpqr).
Definition α₁₃ : forall p q r, C[p·(q·r)] -> C[(r·p)·q] := fun p q r Cpqr => α₃ (α₁₂ Cpqr).
Definition α₁₄ : forall p q r, C[p·(q·r)] -> C[q·(r·r)] := fun p q r Cpqr => α₅ (α₃ (α₁₀ (α₄ (α₂ Cpqr)))).
Definition α₁₅ : forall p q r, C[p·(q·r)] -> C[q·p] := fun p q r Cpqr => α₃ (α₁ (α₆ Cpqr)).
Definition α₁₆ : forall p q r s, C[((p·q)·r)·s] -> C[(q·r)·s] := fun p q r s Cpqrs => α₆ (α₁₀ (α₅ Cpqrs)).

(** ****  Forcing preorder  **)

Definition forcing_le p q := forall r, C[p·r] -> C[q·r].
Notation "p ≤ q" := (forcing_le p q) (at level 70, no associativity) : forcing_scope.

Instance forcing_le_preorder : PreOrder forcing_le := {
  PreOrder_Reflexive := fun p q c => c;
  PreOrder_Transitive := fun p q r x y c Hc => y c (x c Hc)}.

Definition le_max : forall p, p ≤ 1 := fun p c Hc => α₈ (α₂ Hc).

(** The associated equivalence **)
Definition forcing_eq p q := forall r, C[p·r] <-> C[q·r].
Notation "p ≈ q" := (forcing_eq p q) (at level 70) : forcing_scope.

Instance forcing_eq_equiv : Equivalence forcing_eq.
Proof. split.
  intros p c. reflexivity.
  intros p q Hpq c. now rewrite (Hpq c).
  intros p q r Hpq Hqr c. rewrite (Hpq c). now rewrite (Hqr c).
Qed.

Instance forcing_PO : PartialOrder forcing_eq forcing_le.
Proof.
intros p q. split.
  intros Hpq. now split; intro r; rewrite (Hpq r).
  intros [Hpq Hqp]. now intro r; split; apply Hpq || apply Hqp.
Qed.

(** Forcing conditions form a meet semi-lattice whose maximal element is [1]
    and whose minimal elements are all non-well formed conditions. **)
Lemma not_wf_min : forall p q, ~C[p] -> p ≤ q.
Proof. exact (fun p q x c Hc => False_ind _ (x (α₁ Hc))). Qed.

Lemma not_wf_identify : forall p q, ~C[p] ->  ~C[q] -> p ≈ q.
Proof. exact (fun p q x y r => conj (not_wf_min _ x (r := r)) (not_wf_min _ y (r := r))). Qed.

Instance product_glb : Glb product := {
  glb_lower1 := α₉;
  glb_lower2 := α₁₀;
  glb_greatest := fun p q r x y c Hc => α₁₃ (y _ (α₁₂ (x _ (α₁₁ Hc))))}.

Lemma max_prod1 : forall p q, p·q ≈ 1 -> p ≈ 1.
Proof. exact (fun p q H r => conj (fun Cr => α₈ (α₂ Cr)) (fun Cr => α₉ (proj2 (H r) Cr))). Qed.

Lemma max_prod2 : forall p q, p·q ≈ 1 -> q ≈ 1.
Proof. exact (fun p q H r => conj (fun Cr => α₈ (α₂ Cr)) (fun Cr => α₁₀ (proj2 (H r) Cr))). Qed.


(** Some realizers that will be useful for the properties of G **)

Definition C_upper_closed : forall p r, r ≤ p -> C[r] -> C[p] := fun p r x Hc => α₁ (x _ (α₇ Hc)).

Definition product_le_weak1 : forall p q r, r ≤ p·q -> r ≤ p := fun p q r x c Hc => α₉ (x _ Hc).

Definition product_le_compat : forall p q r s, r ≤ p -> s ≤ q -> r·s ≤ p·q :=
  fun p q r s x y c Hc => α₁₃ (y _ (α₁₀ (α₁₂ (x _ (α₉ (α₁₁ Hc)))))).


(*****************************)
(** *  Forcing translation  **)
(*****************************)


Parameter translation : Prop -> κ -> Prop. (* should be on all HO terms but here it is enough on formulæ *)
Notation "T °" := (translation T) (at level 2, format "T '°'").

Axiom forall_translation : forall {T} (A : T -> Prop) s, (forall x, A x)° s <-> forall x, (A x)° s.
Axiom impl_translation : forall A B : Prop,
  (A -> B)° = fun r => forall q r', r = q·r' -> (forall s, C[q·s] -> A° s) -> B° r'.
Axiom eqimpl_translation : forall {T} (M N : T) A s, (Eqimpl M N A)° s = Eqimpl M N (A° s).
Axiom var_translation : forall x s, x° s = x. (* /!\ only for variables *)

Definition force p A := forall r, C[p·r] -> A° r.
Notation "p '𝔽' A" := (force p A) (at level 50).

Definition β₁ : forall A p q, q ≤ p -> p 𝔽 A -> q 𝔽 A := fun A p q x y r c => y _ (x _ c).
Definition β₂ : forall A p, ~C[p] -> p 𝔽 A := fun A p x r c => False_ind _ (x (α₁ c)).
Definition β₃ : forall A p q, p 𝔽 A -> p·q 𝔽 A := fun A p q x r c => x _ (α₉ c).
Definition β₄ : forall A p q, q 𝔽 A -> p·q 𝔽 A := fun A p q x r c => x _ (α₁₀ c).

(* The first lines are administrative steps that should disappear *)
Definition γ₁ : forall A B p, (forall q, (q 𝔽 A) -> (p·q 𝔽 B)) -> p 𝔽 (A -> B).
intros A B p. unfold force at 2 3. rewrite impl_translation. revert A B p.
exact (fun A B p x r c q r' Heq y => x _ y _ (α₆ (eq_ind r (fun x => C[p·x]) c _ Heq))).
Defined.

Definition γ₂ : forall (A B : Prop) p, (p 𝔽 (A -> B)) -> forall q, ((q 𝔽 A) -> (p·q 𝔽 B)).
Proof.
intros A B p. unfold force at 1. rewrite impl_translation. revert A B p.
exact (fun A B p x q y r c => x _ (α₅ c) _ _ eq_refl y).
Defined.

Definition γ₃ : forall (A B : Prop) p, (p 𝔽 (A -> B)) -> p 𝔽 A -> p 𝔽 B.
Proof.
intros A B p. unfold force at 1. rewrite impl_translation. revert A B p.
exact (fun A B p x y r c => x _ (α₁₁ c) _ _ eq_refl y).
Defined.

Definition γ₄ : forall (A B : Prop) p, ~A° p -> p 𝔽 (A -> B).
Proof.
intros A B p. unfold force at 1. rewrite impl_translation. revert A B p.
exact (fun A B p x r c q r' Heq y => False_ind _ (x (y p (α₁₅ (eq_ind r (fun x => C[p·x]) c (q·r') Heq))))).
Defined.

Lemma force_forall₁ : forall {T} (A : T -> Prop) p, (p 𝔽 (forall x, A x)) -> forall x, p 𝔽 (A x).
Proof. intros T A p Hp x s Hs. revert x. rewrite <- forall_translation. apply Hp. exact Hs. Qed.

Lemma force_forall₂ : forall {T} (A : T -> Prop) p, (forall x, p 𝔽 (A x)) -> p 𝔽 (forall x, A x).
Proof. intros T A p Hp s Hs. rewrite forall_translation. intro x. apply Hp. exact Hs. Qed.

Lemma force_eqimpl₁ : forall {T} (M N : T) A p, p 𝔽 (M = N ↦ A) -> M = N ↦ p 𝔽 A.
Proof.
intros T M N A p Hp Heq s Hs. revert Heq. fold (Eqimpl M N (A° s)).
rewrite <- eqimpl_translation. now apply Hp.
Qed.

Lemma force_eqimpl₂ : forall {T} (M N : T) A p, M = N ↦ p 𝔽 A -> p 𝔽 (M = N ↦ A).
Proof. intros T M N A p Hp s Hs. rewrite eqimpl_translation. intro Heq. now apply Hp. Qed.


(** **  Forcing invariance **)
(*      ¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨¨  *)

(** cf Alexandre's paper for the first ones **)

Definition Abs₁ (A : Prop) := forall r, (r 𝔽 A) -> C[r] -> A.
Definition Abs₂ (A : Prop) := forall r, (C[r] -> A) -> r 𝔽 A.

(** **** ⊥ **)
Definition ξbot₁ : Abs₁ ⊥ :=
  fun _ z c P => eq_ind (P° 1) id (force_forall₁ _ z P (α₇ c)) P (var_translation _ _).
Definition ξbot₂ : Abs₂ ⊥ := fun _ z _ c => z (α₁ c) _.

(** **** -> **)
Definition ξimp₁ {A B} (ξA' : Abs₂ A) (ξB : Abs₁ B) : Abs₁ (A -> B) :=
  fun _ z c x => ξB _ (γ₃ z (ξA' _ (fun _ => x))) c.
Definition ξimp₂ {A B} (ξA : Abs₁ A) (ξB' : Abs₂ B) : Abs₂ (A -> B) :=
  fun _ z => γ₁ (fun _ x => ξB' _ (fun c => z (α₁ c) (ξA _ x (α₂ c)))).

(** **** ∀ **)
Definition ξforall₁ {T} {A : T -> Prop} (ξA : forall x p, (p 𝔽 A x) -> C[p] -> A x) : Abs₁ (forall x, A x) :=
  fun _ z c _ => ξA _ _ (force_forall₁ _ z _) c.
Definition ξforall₂ {T} {A : T -> Prop} (ξA' : forall x p, (C[p] -> A x) -> p 𝔽 A x) : Abs₂ (forall x, A x) :=
  fun _ z => force_forall₂ _ (fun x => ξA' x _ (fun c => z c x)).

(** **** Leibniz equality **)
(* ξeq₁ := ξforall₁ (ξimp₁ (λx. x ∘ α₁) (λy. y ∘ α₇)) *)
Definition ξeq₁ {T} : forall x y, Abs₁ (forall Z : T -> Prop, Z x -> Z y) :=
  fun _ _ => ξforall₁ (fun Z => ξimp₁ (fun _ x _ c => eq_ind_r id (x (α₁ c)) (var_translation _ _))
                                      (fun _ y c => eq_ind _ id (y _ (α₇ c)) _ (var_translation _ _))).
(* ξeq₂ := ξforall₂ (ξimp₂ (λx. x ∘ α₇) (λy. y ∘ α₁)) *)
Definition ξeq₂ {T} : forall x y, Abs₂ (forall Z : T -> Prop, Z x -> Z y) :=
  fun _ _ => ξforall₂ (fun _ => ξimp₂ (fun _ y c => eq_ind _ id (y _ (α₇ c)) _ (var_translation _ _))
                                      (fun _ x _ c => eq_ind_r id (x (α₁ c)) (var_translation _ _))).
(** Bis repetita placent **)
(* ξeq2₁ := λz c x. γ₃ z (λ_. x) (α₇ c) *)
Definition ξeq2₁ {T} : forall a b, Abs₁ (forall Z : T -> Prop, Z a -> Z b) :=
  fun _ _ _ z c _ x => eq_ind _ id
    (γ₃ (force_forall₁ _ z _) (fun _ dummy => eq_ind_r id x (var_translation _ _)) (α₇ c)) _ (var_translation _ _).
(* ξeq2₂ := λz. γ₁ (λx c. z (α₁ (α₁ c)) (x (α₁₀ c))) *)
Definition ξeq2₂ {T} : forall x y, Abs₂ (forall Z : T -> Prop, Z x -> Z y) :=
  fun _ _ _ z => force_forall₂ _ (fun _ => γ₁ (fun _ x _ c => z (α₁ (α₁ c)) (fun b : T => (_ b)° _) (x _ (α₁₀ c)))).

(** **** bool **)
Definition ξbool₁ b : Abs₁ (Bool b).
Proof.
intros p x c Z Z1 Z0. unfold Bool in *. apply (force_forall₁ (fun Z : ι → Prop => Z 1%ι → Z O → Z b)) with p Z in x.
assert (p 𝔽 Z 1%ι) as pZ1 by now intros q _; rewrite var_translation.
assert (p 𝔽 Z O) as pZO by now intros q _; rewrite var_translation.
rewrite <- var_translation with _ 1. apply (γ₃ (γ₃ x pZ1) pZO). now apply α₇.
Defined.

Definition ξbool₂ b : Abs₂ (Bool b).
Proof.
intros p x. apply force_forall₂. intro Z. apply γ₁. intros q1 Hq1. apply γ₁. intros qO HqO r c.
rewrite var_translation. apply x.
  exact (α₁ (α₁ (α₁ c))).
  rewrite <- (var_translation _ 1). apply Hq1. apply α₇. apply (α₂ (α₁ (α₁ c))).
  rewrite <- (var_translation _ 1). apply HqO. apply α₇. apply (α₂ (α₁ c)).
Defined.

(** **** nat **)
Definition ξnat₁_proof n : Abs₁ (ℕ n).
Proof.
intros p z c P x y.
assert (z' : forall Z : ι -> Prop, p 𝔽 (Z O -> (forall y, Z y -> Z (S y)) -> Z n)) by now apply force_forall₁.
pose (bla := γ₃ (γ₃ (z' P) (fun r _ => eq_ind_r (fun P => P) x (var_translation _ _)))).
rewrite <- (var_translation _ 1). apply bla.
Focus 2. exact (α₇ c).
apply force_forall₂. intros m. apply γ₁. intros q u r c'. rewrite var_translation. apply y.
rewrite <- (var_translation _ r). now apply (u _ (α₁₀ c')).
Qed.

(** λzλcλxλy. γ₃ (γ₃ z (λ_. x)) (γ₁ (λuλc'. y (u (α₁₀ c'))) (α₇ c)) **)
Definition ξnat₁ n : Abs₁ (ℕ n) :=
fun _ z c _ x y => eq_ind _ id
   (γ₃ (γ₃ (force_forall₁ _ z _)
           (fun r _ => eq_ind_r id x (var_translation _ _)))
       (force_forall₂ _
          (fun m =>
           γ₁ (fun q u r c' => eq_ind_r id
                                        (y m (eq_ind _ id (u r (α₁₀ c')) _ (var_translation _ _)))
                                        (var_translation _ _))))
       (α₇ c)) _
   (var_translation _ _).

Definition ξnat₂_proof n : Abs₂ (ℕ n).
Proof.
intros p z. apply force_forall₂. intro Z. apply γ₁. intros q₀ Hq₀. apply γ₁. intros q₁ Hq₁.
intros r c. cut (q₀·q₁ 𝔽 Z n). exact (fun g => g _ (α₁₆ c)).
apply z. exact (α₁ (α₁ (α₁ c))).
  exact (β₃ Hq₀).
  intro y. apply γ₃. revert y. apply force_forall₁. exact (β₄ Hq₁).
Defined.

Definition ξnat₂_proof' n : Abs₂ (ℕ n).
Proof.
intros p z. cut (C[p] → p 𝔽 ℕ n). exact (fun g _ c => g (α₁ c) _ c).
intros c. apply force_forall₂. intro Z. apply γ₁. intros q₀ Hq₀. apply γ₁. intros q₁ Hq₁.
apply (z c).
  exact (β₃ (β₄ Hq₀)).
  intro y. apply γ₃. revert y. apply force_forall₁. exact (β₄ Hq₁).
Defined.

(** λz. γ₁ (λx. γ₁ (λyλc. z (α₁ (α₁ (α₁ c))) (β₃ x) (γ₃ (β₄ y)))) **)
Definition ξnat₂ n : Abs₂ (ℕ n) :=
fun _ z => force_forall₂ _ (fun Z => γ₁ (fun q₀ Hq₀ => γ₁
  (fun q₁ Hq₁ r c =>
(((z (α₁ (α₁ (α₁ c))) _ (β₃ Hq₀) (fun y => γ₃ (force_forall₁ _ (β₄ Hq₁) y))) : q₀·q₁ 𝔽 Z n) r (α₁₆ c))))).

(** λzλc. γ₁ (λx. γ₁ (λy. z (α₁ c) (β₃ (β₄ x)) (γ₃ (β₄ y)))) c **)
Definition ξnat₂' n : Abs₂ (ℕ n) :=
fun _ z _ c =>
  (force_forall₂ _
     (fun Z : ι → Prop =>
      γ₁ (fun q₀ Hq₀ => γ₁ (fun q₁ (Hq₁ : q₁ 𝔽 (∀y : ι, Z y → Z (S y))) =>
            z (α₁ c) _ (β₃ (β₄ Hq₀)) (fun y => γ₃ (force_forall₁ _ (β₄ Hq₁) y)))))) _ c.

(** **** ∃ **)
Definition ξex₁_proof T (A : T -> Prop) (ξA : forall x, Abs₁ (A x)) : Abs₁ (∃x, A x).
Proof.
intros p t c Z f. rewrite <- (var_translation _ 1).
apply (@γ₃ (forall x, A x -> Z) _ p).
  generalize Z. apply force_forall₁. exact t.
  apply force_forall₂. intro x. apply γ₁. intros q Hq r Cpqr.
    rewrite var_translation. exact (f x (ξA _ _ Hq (α₂ (α₁ Cpqr)))).
  exact (α₇ c).
Defined.

(** λt c f. γ₃ t (γ₁ (λ x c'. f (ξA x (α₂ (α₁ c'))))) (α₇ c) **)
Definition ξex₁ {T} (A : T -> Prop) (ξA : forall x, Abs₁ (A x)) : Abs₁ (∃x, A x) :=
  fun _ t c Z f => eq_ind _ id
    (γ₃ (force_forall₁ _ t _)
        (force_forall₂ _
          (fun _ => γ₁ (fun _ x s c' => eq_ind_r id (f _ (ξA _ _ x (α₂ (α₁ c')))) (var_translation _ _))))
        (α₇ c))
    _ (var_translation _ _).

Definition ξex₂_proof {T} (A : T -> Prop) (ξA' : forall x, Abs₂ (A x)) : Abs₂ (∃x, A x).
Proof.
intros p x. apply force_forall₂. intro Z. apply γ₁. intros q y s c. apply (x (α₁ (α₁ c))).
intros e z. apply (@γ₃ (A e) Z q).
  generalize e. apply force_forall₁. exact y.
  apply ξA'. intro. exact z.
  exact (α₂ (α₅ c)).
Defined.

(** λx. γ₁ (λy c. x (α₁ (α₁ c)) (λz. γ₃ y (ξA' (λ_. z)) (α₂ (α₅ c)))) **)
Definition ξex₂ {T} (A : T -> Prop) (ξA' : forall x, Abs₂ (A x)) : Abs₂ (∃x, A x) :=
  fun p x => force_forall₂ _
    (fun Z => γ₁ (fun q y s c => x (α₁ (α₁ c)) _
       (fun e z => γ₃ (force_forall₁ _ y e) (ξA' e q (fun _ : C[q] => z)) (α₂ (α₅ c))))).

(** **** ∧ **)
Corollary ξand₁_proof {A B} (ξA : Abs₁ A) (ξB : Abs₁ B) : Abs₁ (A ∧ B).
Proof.
intros p x c Z f. rewrite <- (var_translation _ p). apply (@γ₃ (A -> B -> Z) _ p).
  generalize Z. apply force_forall₁. apply x.
  apply γ₁. intros q a. apply γ₁. intros r b. intros s c'. rewrite var_translation. apply f.
    apply (ξA _ a). exact (α₂ (α₁ (α₁ c'))).
    apply (ξB _ b). exact (α₂ (α₁ c')).
  apply (α₄ c).
Qed.

(** λxλcλf. γ₃ x (γ₁ (λa. γ₁ (λbλc'. f (ξA q (α₂ (α₁ (α₁ c')))) (ξB b (α₂ (α₁ c')))))) (α₄ c) **)
Definition ξand₁ {A B} (ξA : Abs₁ A) (ξB : Abs₁ B) : Abs₁ (A ∧ B) :=
  fun _ x c _ f => eq_ind _ id
    (γ₃ (force_forall₁ _ x _) (γ₁ (fun _ a => γ₁ (fun _ b _ c' =>
      eq_ind_r id
      (f (ξA _ a (α₂ (α₁ (α₁ c')))) (ξB _ b (α₂ (α₁ c'))))
      (var_translation _ _)))) (α₄ c)) _ (var_translation _ _).

Corollary ξand₂_proof {A B} (ξA' : Abs₂ A) (ξB' : Abs₂ B) : Abs₂ (A ∧ B).
Proof.
intros p z. apply force_forall₂. intro Z. apply γ₁. intros q Hq r c.
cut (p·q 𝔽 Z). exact (fun g => g _ c).
apply (z (α₁ (α₁ c))). intros a b.
eapply γ₃. eapply γ₃. apply β₄. exact Hq.
exact (ξA' _ (fun _ => a)).
exact (ξB' _ (fun _ => b)).
Defined.

(** λz. γ₁ (λqλc. z (α₁ (α₁ c)) (λaλb. γ₃ (γ₃ (β₄ q) (ξA' (λ_. a))) (ξB' (λ_. b))) c) **)
Definition ξand₂ {A B} (ξA' : Abs₂ A) (ξB' : Abs₂ B) : Abs₂ (A ∧ B) :=
  fun p z => force_forall₂ _ (fun Z : Prop => γ₁ (fun q Hq r c =>
        (z (α₁ (α₁ c)) _ (fun a b => γ₃ (γ₃ (β₄ Hq) (ξA' _ (fun _ => a))) (ξB' _ (fun _ => b)))) r c)).

(** **** ∃_, _ & _ **)
Corollary ξexand₁_proof {T} {A B : T -> Prop} (ξA : forall x, Abs₁ (A x)) (ξB : forall x, Abs₁ (B x))
  : Abs₁ (∃ x, A x & B x).
Proof.
intros p x c Z f. rewrite <- (var_translation _ p). apply (@γ₃ (forall x, A x -> B x -> Z) _ p).
  generalize Z. apply force_forall₁. exact x.
  apply force_forall₂. intro e. apply γ₁. intros q y. apply γ₁. intros r z.
  intros s c'. rewrite var_translation. apply (f e).
    exact (ξA e _ y (α₂ (α₁ (α₁ c')))).
    exact (ξB e _ z (α₂ (α₁ c'))).
  exact (α₄ c).
Qed.

(** λx c f. γ₃ x (γ₁ (λy. γ₁ (λz c'. (f (ξA y (α₂ (α₁ (α₁ c')))) (ξB z (α₂ (α₁ c'))))))) (α₄ c) **)
Definition ξexand₁ {T} {A B : T -> Prop} (ξA : forall x, Abs₁ (A x)) (ξB : forall x, Abs₁ (B x))
  : Abs₁ (∃ x, A x & B x) :=
  fun p x c Z f => eq_ind _ id
  (γ₃ (force_forall₁ (fun x : Prop => (forall e : T, A e -> B e -> x) -> x) x _)
      (force_forall₂ _ (fun e =>
         γ₁ (fun q y =>
            γ₁ (fun r z s c' => eq_ind_r id
                                         (f e (ξA e q y (α₂ (α₁ (α₁ c')))) (ξB e r z (α₂ (α₁ c'))))
                                         (var_translation _ _)))))
      (α₄ c))
  _
  (var_translation _ _).

Corollary ξexand₂_proof {T} {A B : T -> Prop} (ξA' : forall x, Abs₂ (A x)) (ξB' : forall x, Abs₂ (B x))
  : Abs₂ (∃ x, A x & B x).
Proof.
intros p z. apply force_forall₂. intro Z. apply γ₁. intros q Hq r c.
cut (p·q 𝔽 Z). exact (fun g => g _ c).
apply (z (α₁ (α₁ c))). intros t HA HB. apply β₄. eapply γ₃. eapply γ₃.
  generalize t. eapply force_forall₁. exact Hq.
  exact (ξA' _ _ (fun _ => HA)).
  exact (ξB' _ _ (fun _ => HB)).  
Defined.

(** λz. γ₁ (λqλc. z (α₁ (α₁ c)) (λxλy. β₄ (γ₃ (γ₃ q (ξA' (λ_. x))) (ξB' (λ_. x)))) c) **)
Definition ξexand₂ {T} {A B : T -> Prop} (ξA' : forall x, Abs₂ (A x)) (ξB' : forall x, Abs₂ (B x))
  : Abs₂ (∃ x, A x & B x) :=
  fun _ z => force_forall₂ _ (fun _ =>
   γ₁ (fun _ Hq _ c => (z (α₁ (α₁ c)) _
           (fun _ HA HB => β₄ (γ₃ (γ₃ (force_forall₁ _ Hq _) (ξA' _ _ (fun _ => HA)))
                                  (ξB' _ _ (fun _ => HB))))) _ c)).

(** **** Specialisation of a formula **)
Definition ξspe₁ (A : κ -> Prop) (ξA : forall x, Abs₁ (A x)) : forall x y, Abs₁ (A (x·y)) := fun x y => ξA (x·y).
Definition ξspe₂ (A : κ -> Prop) (ξA' : forall x, Abs₂ (A x)) : forall x y, Abs₂ (A (x·y)) := fun x y => ξA' (x·y).


(*************************)
(** *  Properties of G  **)
(*************************)


(* Hypothesis: C is arithmetical *)
Parameter ξc : forall p r : κ, r 𝔽 C[p] → C[r] → C[p].
Parameter ξc' : forall p r, (C[r] → C[p]) → r 𝔽 C[p].

Parameter G : κ -> Prop.
Axiom G_forcing : forall p r, (r 𝔽 G(p)) = (r ≤ p).
(* We cannot take r = p because of β₁. *)

(** **  Proofs with the forcing condition 1  **)

(** G is non empty: λx.x **)
Definition G_1 : 1 𝔽 G(1) := eq_ind_r id (fun _ x => x) (G_forcing _ _).

(** G is a subset of C: γ₁ (λx. ξc' (λc. α₁ (x (α₃ c))))
                        γ₁ (λx. ξc' (α₁ ∘ x ∘ α₃)) **)
Definition G_sub_C : forall p, 1 𝔽 (G(p) → C[p]) :=
  fun p => γ₁ (fun q x => ξc' (fun c => α₁ (eq_ind _ id x _ (G_forcing p q) _ (α₃ c)))).

(** G is upper closed: γ₁ (λx c. α₉ (x (α₁₀ c)))
                       γ₁ (λx. α₉ ∘ x ∘ α₁₀) **)
Definition G_upper_closed : forall p q, 1 𝔽 (G(p·q) → G(p)) :=
fun _ _  => γ₁ (fun _ x => eq_ind_r id (fun _ c => α₉ (eq_ind _ id x _ (G_forcing _ _) _ (α₁₀ c))) (G_forcing _ _)).

(** G is stable by product: γ₁ (λx. γ₁ (λy c. α₁₃ (y (α₁₂ (x (α₂ (α₅ (α₅ c))))))))
                            γ₁ (λx. γ₁ (λy. α₁₃ ∘ y ∘ α₁₂ ∘ x ∘ α₂ ∘ α₅ ∘ α₅)) **)
Definition G_prod_closed : forall p q, 1 𝔽 (G(p) → G(q) → G(p·q)) :=
  fun p q => γ₁ (fun r₁ x => γ₁ (fun r₂ y => eq_ind_r id
    (fun _ Hc => α₁₃ ((eq_ind _ id y _ (G_forcing _ _)) _
                (α₁₂ ((eq_ind _ id x _ (G_forcing _ _)) _ (α₂ (α₅ (α₅ Hc)))))))
    (G_forcing _ _))).


(** G is M-generic: ∀x, 1 𝔽 (∀p, C[p] → ∃q, C[p·q] ∧ D(x, p·q)) → ∃p, G(p) & D(x, p) **)
Lemma M_genericity_proof {T} D (ξD : forall x p, Abs₁ (D x p)) (ξD' : forall x p, Abs₂ (D x p)) :
  forall x : T, 1 𝔽 ((forall p, C[p] → (∃q, C[p·q] & D x (p·q))) → (∃p, G(p) & D x p)).
Proof.
intro n. apply γ₁. intros r₁ Hr₁. apply β₄. apply force_forall₂. intro Z. apply γ₁. intros r₂ Hr₂. intros s c.
apply (ξexand₁ (ξspe₁ _ ξc ((r₁·r₂)·s)) (ξspe₁ _ (ξD n) ((r₁·r₂)·s))) with r₁.
  eapply γ₃ with (C[r₁·r₂·s]). generalize ((r₁·r₂)·s). now apply force_forall₁. exact (ξc' (fun _ => c)).
  exact (α₁ (α₁ c)).
intros q Cq Dq.
assert (Hr₂' : (r₁·r₂·s·q 𝔽 G (r₁·r₂·s·q)) -> (r₁·r₂·s·q 𝔽 D n (r₁·r₂·s·q)) -> (r₁·r₂·s·q 𝔽 Z)).
  intro Hf. apply γ₃. revert Hf. apply γ₃. apply β₁ with r₂.
  exact (fun t c => α₁₀ (α₉ (α₉ c))).
  generalize (((r₁·r₂)·s)·q). now apply force_forall₁.
apply Hr₂'.
  rewrite G_forcing; reflexivity.
  apply ξD'; now intro.
exact (α₃ (α₂ (α₅ (α₁₁ Cq)))).
Qed.

(** γ₁ (λx. β₄ (γ₁ (λy c. ξexand (ξspe ξc) (ξspe ξD) (γ₃ x (ξc' (λ_. c))) (α₁ (α₁ c))
                                 (λc' d. γ₃ (γ₃ (β₁ (λc. α₁₀ (α₉ (α₉ c))) y) id)
                                            (ξD' (λ_. d)) (α₃ (α₂ (α₅ (α₁₁ c')))))))) **)
Definition M_genericity {T} D (ξD : forall x p, Abs₁ (D x p)) (ξD' : forall x p, Abs₂ (D x p)) :
  forall x : T, 1 𝔽 ((forall p, C[p] → (∃q, C[p·q] & D x (p·q))) → (∃p, G(p) & D x p)) :=
 fun _ =>
  γ₁ (fun r₁ Hr₁ => β₄ (force_forall₂ _
    (fun Z : Prop =>
     γ₁ (fun r₂ Hr₂ s c =>
        ξexand₁ (ξspe₁ _ ξc _) (ξspe₁ _ (ξD _) _)
          (γ₃ (force_forall₁ _ Hr₁ _) (ξc' (fun _ => c))) (α₁ (α₁ c))
          (fun q Cq Dq =>
              γ₃ (γ₃ (β₁ (fun t c => α₁₀ (α₃ (α₁₀ (α₃ (α₅ (α₃ (α₁₀ (α₃ (α₅ c)))))))))
                         (force_forall₁ _ Hr₂ _))
                     (eq_ind_r id (reflexivity _) (G_forcing _ _)))
                 (ξD' _ _ _ (fun _ => Dq))
                 (α₃ (α₂ (α₅ (α₁₁ Cq))))))))).

(** **  Proofs for any forcing condition p  **)

(** G is non empty: α₈ ∘ α₂ **)
Definition G_1_bis : forall r, r 𝔽 G(1) :=
  fun _ => eq_ind_r id (fun _ => α₈ ∘ α₂) (G_forcing _ _).

(** G is a subset of C: γ₁ (λx. ξc' (λc. α₁ (x (α₃ c))))
                        γ₁ (λx. ξc' (α₁ ∘ x ∘ α₃)) **)
Definition G_sub_C_bis : forall p r, r 𝔽 (G(p) → C[p]) :=
  fun _ _ => γ₁ (fun _ x => ξc' (fun c => α₁ ((eq_ind _ id x _ (G_forcing _ _)) _ (α₃ c)))).

(** G is upper closed: γ₁ (λx c. α₉ (x (α₁₀ c)))
                       γ₁ (λx. α₉ ∘ x ∘ α₁₀) **)
Definition G_upper_closed_bis : forall p q r, r 𝔽 (G(p·q) → G(p)) :=
fun _ _ _ => γ₁ (fun _ x => eq_ind_r id
   (fun _ c => α₉ (eq_ind _ id x _ (G_forcing _ _) _ (α₁₀ c))) (G_forcing _ _)).

(** G is stable by product: γ₁ (λx. γ₁ (λy c. α₁₃ (y (α₁₂ (x (α₂ (α₅ (α₅ c))))))))
                            γ₁ (λx. γ₁ (λy. α₁₃ ∘ y ∘ α₁₂ ∘ x ∘ α₂ ∘ α₅ ∘ α₅)) **)
Definition G_prod_closed_bis : forall p q r, r 𝔽 (G(p) → G(q) → G(p·q)) :=
  fun _ _ _ => γ₁ (fun r₁ x => γ₁ (fun r₂ y => eq_ind_r id
    (fun _ c => α₁₃ ((eq_ind _ id y _ (G_forcing _ _)) _
               (α₁₂ ((eq_ind _ id x _ (G_forcing _ _)) _ (α₂ (α₅ (α₅ c)))))))
    (G_forcing _ _))).


(** G is M-generic: ∀x, r 𝔽 (∀p, C[p] -> ∃q, C[p·q] ∧ D(x, p·q)) -> ∃p, G(p) & D(x, p) **)
Lemma M_genericity_proof_bis {T} D (ξD : forall x p, Abs₁ (D x p)) (ξD' : forall x p, Abs₂ (D x p)) :
  forall (x : T) r, r 𝔽 ((forall p, C[p] → (∃q, C[p·q] & D x (p·q))) → (∃p, G(p) & D x p)).
Proof.
intros n r. apply γ₁. intros r₁ Hr₁. apply force_forall₂. intro Z. apply γ₁. intros r₂ Hr₂. intros s c.
apply (ξexand₁ (ξspe₁ _ ξc (((r·r₁)·r₂)·s)) (ξspe₁ _ (ξD n) (((r·r₁)·r₂)·s))) with r₁.
  eapply γ₃ with (C[r·r₁·r₂·s]). generalize (((r·r₁)·r₂)·s). now apply force_forall₁. exact (ξc' (fun _ => c)).
  exact (α₂ (α₁ (α₁ c))).
intros q Cq Dq.
assert (Hr₂' : (r·r₁·r₂·s·q 𝔽 G (r·r₁·r₂·s·q)) -> (r·r₁·r₂·s·q 𝔽 D n (r·r₁·r₂·s·q)) -> (r·r₁·r₂·s·q 𝔽 Z)).
  intro Hf. apply γ₃. revert Hf. apply γ₃. apply β₁ with r₂.
  exact (fun t c => α₁₀ (α₉ (α₉ c))).
  generalize (((r·r₁·r₂)·s)·q). now apply force_forall₁.
apply Hr₂'.
  rewrite G_forcing; reflexivity.
  apply ξD'; now intro.
exact (α₃ (α₂ (α₅ (α₁₁ Cq)))).
Qed.
Print M_genericity_proof_bis.

(** γ₁ (λx. γ₁ (λy c. ξexand (ξspe ξc) (ξspe ξD) (γ₃ x (ξc' (λ_. c))) (α₂ (α₁ (α₁ c)))
                              (λc' d. γ₃ (γ₃ (β₁ (α₁₀ ∘ α₉ ∘ α₉) y) id)
                                         (ξD' (λ_. d)) (α₃ (α₂ (α₅ (α₁₁ c'))))))) **)
Definition M_genericity_bis {T} D (ξD : forall x p, Abs₁ (D x p)) (ξD' : forall x p, Abs₂ (D x p)) :
  forall (x : T) r, r 𝔽 ((forall p, C[p] → (∃q, C[p·q] & D x (p·q))) → (∃p, G(p) & D x p)) :=
 fun _ _ =>
  γ₁ (fun r₁ Hr₁ => (force_forall₂ _
    (fun Z : Prop =>
     γ₁ (fun r₂ Hr₂ s c =>
        ξexand₁ (ξspe₁ _ ξc _) (ξspe₁ _ (ξD _) _)
          (γ₃ (force_forall₁ _ Hr₁ _) (ξc' (fun _ => c))) (α₂ (α₁ (α₁ c)))
          (fun _ Cq Dq =>
              γ₃ (γ₃ (β₁ (fun t c => α₁₀ (α₃ (α₁₀ (α₃ (α₅ (α₃ (α₁₀ (α₃ (α₅ c)))))))))
                         (force_forall₁ _ Hr₂ _))
                     (eq_ind_r id (reflexivity _) (G_forcing _ _)))
                 (ξD' _ _ _ (fun _ => Dq))
                 (α₃ (α₂ (α₅ (α₁₁ Cq))))))))).


(**************************)
(** *  Data implication  **)
(**************************)

Definition data_implication (A B : Prop) := A -> B.
Notation "d ⇒ A" := (data_implication d A) (at level 70).
Axiom data_translation : forall D A r, (D ⇒ A)° r = forall q r', r = q·r' ↦ (D ⇒ A° r').

Definition force_data₁ : forall D A p, p 𝔽 (D ⇒ A) -> D ⇒ (p 𝔽 A) :=
  fun _ _ _ x v _ c => eq_ind _ id  (x _ (α₁₁ c)) _ (data_translation _ _ _) _ _ eq_refl v.

Definition force_data₂ : forall D A p, D ⇒ (p 𝔽 A) -> p 𝔽 (D ⇒ A) :=
  fun _ _ _ x q c =>
    eq_ind_r id (fun _ _ Heq v => x v _ (α₉ (α₆ (eq_ind q (fun _ => C[_]) c _ Heq)))) (data_translation _ _ _).


End Forcing.