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.