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

(** The call-by-value implication **)

Definition cbvImpl (D : ι -> Prop) v (B : Prop) := D v -> B.
Notation "D '[' v ']'  '~>' B" := (cbvImpl D v B) (at level 70).

Definition comp {A B C} (f : B -> C) (g : A -> forall Z, (B -> Z) -> Z) := fun x => g x _ f.
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 CbvForcingType.
  Parameter C : ι -> Prop.
  Parameter product : ι -> ι -> ι.
  Parameter one : ι.
  Bind Scope forcing_scope with ι.
  Delimit Scope forcing_scope with forcing.
  Open Scope forcing_scope.

  Set Implicit Arguments.
(*  Notation "'C[' p ']'" := (C p%forcing).*)
  Notation "'CC[' p ']'" := (forall {Z : Prop}, (C [ p ] ~> Z) -> Z).
  Notation "1" := one : forcing_scope.
  Notation "p · q" := (product p%forcing q%forcing)
    (at level 46, format "p '·' q", no associativity) : forcing_scope.

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


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

Module CbvForcing (Def : CbvForcingType).

Import Def.
Set Implicit Arguments.

(** 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", no associativity) : forcing_scope.

(** Equivalence between [C[p]] and [CC[p]] **)
Theorem C_CC_equiv : forall p (A : Prop), (C[p] ~> A) <-> (CC[p] -> A).
Proof. exact (fun p A => conj (fun v f => f _ v) (fun f v => f (fun _ g => g v))). Qed.

(** Derived combinators **)
Definition α₉ {p q r} : C[(p·q)·r] ~> CC[p·r] := fun c => α₃ c α₆ _ α₁ _ α₃.
Definition α₁₀ {p q r} : C[(p·q)·r] ~> CC[q·r] := fun c => α₅ c α₂.
Definition α₁₁ {p q} : C[p·q] ~> CC[p·(p·q)] := fun c => α₄ c α₆ _ α₁ _ α₃.
Definition α₁₂ {p q r} : C[p·(q·r)] ~> CC[q·(r·p)] := fun c => α₃ c α₅.
Definition α₁₃ {p q r} : C[p·(q·r)] ~> CC[(r·p)·q] := fun c => α₁₂ c α₃.
Definition α₁₄ {p q r} : C[p·(q·r)] ~> CC[q·(r·r)] := fun c => α₂ c α₄ _ α₁₀ _ α₃ _ α₅.
Definition α₁₅ {p q r} : C[p·(q·r)] ~> CC[q·p] := fun c => α₆ c α₁ _ α₃.
Definition α₁₆ {p q r s} : C[((p·q)·r)·s] ~> CC[(q·r)·s] := fun c => α₅ c α₁₀ _ α₆.


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

Definition forcing_le p q := forall r, C[p·r] ~> CC[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 Z f => f c;
  PreOrder_Transitive := fun p q r x y c Hc => (x c Hc) _ (y c)}.

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

(** The associated equivalence **)
Definition forcing_eq p q := forall r, CC[p·r] <-> CC[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. split; intros r V; rewrite (Hpq r) || rewrite <- (Hpq r); exact (fun _ f => f V).
  intros [Hpq Hqp]. now intro r; split; intro f; apply f; apply Hpq || apply Hqp.
Qed.

(** Forcing condition form a meet semi-lattice whose maximal element is [1]
    and whose minimal element 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 => α₁ Hc x _). Qed.

Lemma not_wf_identify : forall p q, (C[p] ~> ⊥) -> (C[q] ~> ⊥) -> p ≈ q.
Proof. intros p q x y r. now split; intro f; apply f; apply not_wf_min. Qed.

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


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

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

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

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 => α₁₁ c α₉ _ (x _) _ α₁₂ _ α₁₀ _ (y _) _ α₁₃.


(*****************************)
(** *  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 *)
Axiom data_translation : forall (D : ι -> Prop) (A : Prop) p r,
  (D[p] ~> A)° r = forall q r', r = q·r' -> D[p] ~> A° r'.

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 => (x _ c) _ (y _).
Definition β₂ : forall A p, (C[p] ~> ⊥) -> p 𝔽 A := fun A p x r c => α₁ c x _.
Definition β₃ : forall A p q, p 𝔽 A -> p·q 𝔽 A := fun A p q x r c => α₉ c (x _).
Definition β₄ : forall A p q, q 𝔽 A -> p·q 𝔽 A := fun A p q x r c => α₁₀ c (x _).

(* 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 3. rewrite impl_translation. revert A B p.
exact (fun A B p x r c q r' Heq y => (α₆ (eq_ind r (fun x => C (p·x)) c _ Heq)) _ (x _ y _)).
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 =>  (α₅ c) _ (x _) _ _ 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 => (α₁₁ c) _ (x _) _ _ 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 ((α₁₅ (eq_ind r (fun x => C (p·x)) c _ Heq)) _ (y p)))).
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.

(* Proofs for the other definition of (D[v] ~> A)^*: D[v] ~> A^* *)
Lemma force_cbvImpl₁ : forall p (D : ι -> Prop) v (A : Prop), p 𝔽 (D[v] ~> A) -> D[v] ~> p 𝔽 A.
Proof.
intros p D v A x y r c.
apply x in c. rewrite data_translation in c. apply (c 1 r). admit. exact y. Qed.

Lemma force_cbvImpl₂ : forall p (D : ι -> Prop) v (A : Prop), (D[v] ~> p 𝔽 A) -> p 𝔽 (D[v] ~> A).
Proof.
intros p D v A f r c. rewrite data_translation. intros q r' Heq x. subst r.
apply (α₆ c α₉). apply (f x). Qed.

Require Classical.
Definition ccS : forall p (A B : Prop), p  𝔽 (((A -> B) -> A) -> A).
Proof.
intros p A B r c. do 2 rewrite impl_translation. intros q r' Heq x. subst.
apply Classical_Prop.Peirce. exact (fun k => α₁₄ c (fun c' => x _ c' r' _ eq_refl (γ₄ _ k))).
Defined.


(** **  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₁ ⊥.
Proof. unfold Abs₁. intros r z c. rewrite <- (var_translation _ 1). apply (α₇ c). apply z. Defined.
Definition ξbot₂ : Abs₂ ⊥ := fun _ z _ c => (α₁ c) _ z _.

(** **** -> **)
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 => (α₁ c) _ z ((α₂ c) _ (ξA _ x)))).

(** **** ∀ **)
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 **)
(* ξeq2₁ := λz c x. α₇ c (γ₃ z (λ_. x)) *)
Definition ξeq2₁ {T} : forall a b, Abs₁ (forall Z : T -> Prop, Z a -> Z b) :=
  fun _ _ _ z c _ x => eq_ind _ id
    ((α₇ c) _ (@γ₃ _ _ _ (force_forall₁ _ z _) (fun _ dummy => eq_ind_r id x (var_translation _ _)) 1))
    _ (var_translation _ _).
(* ξeq2₂ := λz. γ₁ (λx c. α₁ c α₁ z (α₁₀ c x)) *)
Definition ξeq2₂ {T} : forall x y, Abs₂ (forall Z : T -> Prop, Z x -> Z y) :=
  fun _ _ _ z => force_forall₂ _ 
    (fun _ => γ₁ (fun _ x _ c => (α₁ c) _ α₁ _ z (fun b : T => (_ b)° _) ((α₁₀ c) _ (x _)))).

(** **** Data implication **)
(* ξcbvImpl₁ := λz c d. ξA (γ₃ z d) c *)
Definition ξcbvImpl₁ {A} (ξA : forall p, (p 𝔽 A) -> C[p] ~> A) (D : ι -> Prop) (v : ι)
 : Abs₁ (D[v] ~> A).
Proof.
intros ? z c d. apply force_cbvImpl₁ in z. apply ξA in z. apply (z c). exact d.
Restart.
refine (fun _ z c d => ξA _ (force_cbvImpl₁ z d) c).
Defined.

(* λz. γ₅ (λd. ξA' (λc. z c d)) *)
Definition ξcbvImpl₂ {A} (ξA' : forall p, (C[p] ~> A) -> (p 𝔽 A)) (D : ι -> Prop) (v : ι) : Abs₂ (D[v] ~> A) :=
  fun _ z => force_cbvImpl₂ (fun d => ξA' _ (fun c' => z c' d)).

(** **** Datatypes **)
(* λz c f. α₇ c (γ₃ z (λ_. f)) *)
Definition ξd₁ : forall (D : ι -> Prop) (v : ι), Abs₁ (forall Z, (D[v] ~> Z) -> Z).
Proof.
intros D v p z c Z f. apply force_forall₁ with _ _ Z in z.
assert (p 𝔽 (D[v] ~> Z)) as fr. intros r _. rewrite data_translation. intros. now rewrite var_translation.
rewrite <- (var_translation _ 1). apply (α₇ c). apply (γ₃ z fr).
Restart.
exact 
(fun _ _ _ z c _ f =>
   eq_ind _ id (α₇ c (γ₃ (force_forall₁ _ z _) (fun _ dummy =>
     eq_ind_r id
       (fun _ _ _ =>
        eq_ind_r _ f (var_translation _ _))
       (data_translation _ _ _ _)) (r:=1))) _
     (var_translation _ _)).
Defined.

(* λz. γ₁ (λx c. α₁₀ c (α₁ c α₁ z (swap x))) *)
Definition ξd₂ : forall (D : ι -> Prop) (v : ι), Abs₂ (forall Z, (D[v] ~> Z) -> Z).
Proof.
intros D v p z. apply force_forall₂. intro Z. apply γ₁. intros q x r c.
apply (α₁₀ c). generalize r. change (q 𝔽 Z). apply (α₁ c α₁ _ z). apply (force_cbvImpl₁ x).
Restart.
exact (fun _ _ _ z => force_forall₂ _ (fun Z => γ₁ (fun _ x _ c => α₁₀ c (α₁ c α₁ _ z _ (force_cbvImpl₁ x) _)))).
Defined.

(** **** 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 (α₇ c). apply (γ₃ (γ₃ x pZ1) pZO).
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 ((α₁ c) _ α₁ _ α₁ _ x).
  rewrite <- (var_translation _ r). apply ((α₉ c) _ α₁₀ _ (Hq1 _)).
  rewrite <- (var_translation _ r). apply ((α₁₀ c) _ (HqO _)).
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 (α₇ c). apply bla.
apply force_forall₂. intro m. apply γ₁. intros q u r c'. rewrite var_translation. apply y.
rewrite <- (var_translation _ r). now apply ((α₁₀ c') _ (u _)).
Qed.

(** λz c x y. α₇ c (γ₃ (γ₃ z (λ_. x)) (γ₁ (λu c'. y (α₁₀ c' u)))) **)
Definition ξnat₁ n : Abs₁ (ℕ n) :=
fun _ z c _ x y => eq_ind _ id
   ((α₇ c) _ (@γ₃ _ _ _ (γ₃ (force_forall₁ _ z _)
           (fun r dummy => 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 ((α₁₀ c') _ (u r)) _ (var_translation _ _)))
                                        (var_translation _ _)))) _
       )) _
   (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 => (α₁₆ c) _ (g _ )).
apply ((α₁ c) _ α₁ _ α₁ _ z).
  exact (β₃ Hq₀).
  intro y. apply γ₃. revert y. apply force_forall₁. exact (β₄ Hq₁).
Defined.

Definition ξnat₂_proof' n : Abs₂ (ℕ n).
Proof.
intros p z. cut (CC[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 (c _ z).
  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 =>
(α₁₆ c) _ (((((α₁ c) _ α₁ _ α₁ _ z) _ (β₃ Hq₀) (fun y => γ₃ (force_forall₁ _ (β₄ Hq₁) y))) : q₀·q₁ 𝔽 Z n) r)))).

(** λz c. γ₁ (λx. γ₁ (λy. α₁ c z (β₃ (β₄ x)) (γ₃ (β₄ y)))) c **)
Definition ξnat₂' n : Abs₂ (ℕ n) :=
fun _ z _ c =>
  (force_forall₂ _
     (fun Z : ι → Prop =>
      γ₁ (fun q₀ x => γ₁ (fun q₁ (y : q₁ 𝔽 (∀y : ι, Z y → Z (S y))) =>
            (α₁ c) _ z _ (β₃ (β₄ x)) (fun n => γ₃ (force_forall₁ _ (β₄ y) n)))))) _ 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 (α₇ c). apply (@γ₃ (forall x, A x -> Z) _ p).
  generalize Z. apply force_forall₁. exact t.
  apply force_forall₂. intro x. apply γ₁. intros q Hq r c'.
    rewrite var_translation. exact (f x ((α₁ c') _ α₂ _ (ξA _ _ Hq))).
Defined.

(** **** 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  **)
(*************************)


Parameter G : ι -> Prop.
Notation "p '∈'  'G'" := (G p) (at level 48).
Axiom G_forcing : forall p r, (r 𝔽 p ∈ G) = (r ≤ p).
(* We cannot take r = p because of β₁. *)

(** G is non empty: λc. α₂ c α₈ **)
Definition G_1 : forall p, p 𝔽 1 ∈ G := fun _ => eq_ind_r id (fun _ c => (α₂ c) _ α₈) (G_forcing _ _).

(** G is a subset of C: γ₁ (λx. ξ'_~> (λc. α₃ c x α₁)) **)
Definition G_sub_C : forall p r, r 𝔽 (p ∈ G -> CC[p]) :=
  fun p r => γ₁ (fun _ x => ξd₂ (fun c => (α₃ c) _ (eq_ind _ id x _ (G_forcing p _) _) _ α₁)).

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

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


Lemma ξaux {A : ι -> Prop} (ξA : forall x, Abs₁ (A x)) k : Abs₁ (∀Z : Prop, (∀x, C[k·x] ~> (A (k·x) -> Z)) -> Z).
Proof.
intros p x c Z f. rewrite <- (var_translation _ p). apply (α₄ c). apply (@γ₃ (forall x, C[k·x] ~> (A (k·x) -> Z)) _ p).
  generalize Z. apply force_forall₁. exact x.
  apply force_forall₂. intro e. apply force_cbvImpl₂. intro c'. apply γ₁. intros r z.
  intros s c''. rewrite var_translation. apply (f e c').
    exact ((α₁ c'') _ α₂ _ (ξA (k·e) _ z)).
(** λx c f. α c (γ₃ x ?? (λc'. γ₁ (λz c''. f c' (α₁ c'' α₂ (ξA z))))) **)
Restart.
exact (fun _ x c _ f => eq_ind _ id
   (α₄ c (γ₃ (force_forall₁ _ x _)
         (force_forall₂ _ (fun _ => force_cbvImpl₂
               (fun c' => γ₁ (fun _ z _ c'' =>
                   eq_ind_r id
                     (f _ c' (α₁ c'' α₂ _ (ξA _ _ z)))
                     (var_translation _ _))))) (r:=_))) _
   (var_translation _ _)).
Qed.

(** 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) r,
  r 𝔽 ((forall p, C[p] ~> (∀Z : Prop, (∀q, C[p·q] ~> (D x (p·q) -> Z)) -> Z)) -> (∃p, p ∈ G & D x p)).
Proof.
intros n r. apply γ₁. intros r₁ x. (*apply β₄.*) apply force_forall₂. intro Z. apply γ₁. intros r₂ y.
intros s c. apply (α₁ c α₁ _ α₂). intro c'.
assert (Abs₁ (∀Z : Prop, (∀x, C[r·r₁·r₂·s·x] ~> (D n (r·r₁·r₂·s·x) -> Z)) -> Z)) as mix.
  apply (@ξaux _ (ξD n) (r·r₁·r₂·s)).
apply mix with r₁; try exact c'.
  generalize c. apply force_cbvImpl₁. generalize (r·r₁·r₂·s). now apply force_forall₁.
  intros q Cq Dq. apply (α₁₁ Cq α₅ _ α₂ _ α₃).
  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)).
    exact (fun Hf => γ₃ (γ₃ (β₁ (fun t c => α₉ c α₉ _ α₁₀) (force_forall₁ _ y _)) Hf)).
  apply Hr₂'.
    rewrite G_forcing; reflexivity.
    apply ξD'; now intro.
Qed.

(** γ₁ (λx. (γ₁ (λy c. α₁ c α₁ α₂ (λc'. ξaux ξD (γ₃ x c) c'
                                        (λc₃ d. α₁₁ c₃ α₅ α₂ α₃ (γ₃ (γ₃ (β₁ (α₁₀ ∘ α₉ ∘ α₉) y) id)
                                                                    (ξD' (λ_. d)))))))) **)
Definition M_genericity {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] ~> (∀Z : Prop, (∀q, C[p·q] ~> (D x (p·q) -> Z)) -> Z)) -> (∃p, p ∈ G & D x p)) :=
fun (n : T) _ =>
γ₁ (fun _ x => (force_forall₂ _
        (fun _ =>
         γ₁
           (fun _ y _ c =>
            α₁ c α₁ _ α₂ _
              (fun c' =>
                (ξaux (ξD _) (k:=_)) _
                  (force_cbvImpl₁
                     (force_forall₁ _ x (_·_)) c) c' _
                  (fun _ c₃ Dq =>
                   α₁₁ c₃ α₅ _ α₂ _ α₃ _
                     ((
                         γ₃ (γ₃ (β₁ (fun _ c => α₉ c α₉ _ α₁₀) (force_forall₁ _ y _))
                                (eq_ind_r id (reflexivity _) (G_forcing _ _))))
                         (ξD' n _ _ (fun dummy => Dq)) _))))))).

End CbvForcing.