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.