Set Universe Polymorphism. Notation "( x ; y )" := (existT _ x y). Notation "t .1" := (projT1 t) (at level 3, format "t '.1'"). Notation "t .2" := (projT2 t) (at level 3, format "t '.2'"). (** To ease the presentation, we don't formally define a source calculus with its translation, but rather show how to inhabit the translation of any type in a shallow-embedding style. Therefore, we shall pay attention to the "core" translation of types, assuming we know by induction how to define the translation of its subtypes. *) (** * Definitions *) (** The dependent CPS translation of a type. *) Definition T A : A -> Prop := fun t => forall (R : A -> Prop), (forall x, R x) -> R t. Definition generous A :=({x: A & T A x}). Notation "[ A ]₁":=(T A). Notation "[ A ]":=(generous A). (** The usual negative translation of types. *) Definition Tneg A : Prop:= (A -> False) -> False. Notation "[ A ]ₙ ":=(Tneg A). (** Remark : here we will note [ ] both for the translations of terms and types (while the latter are written 〚·〛ₓ in the paper), only to avoid the notation 〚 which is not available in company-coq. *) (** Obviously, Tneg is a particular case of T. *) Proposition generous_neg:forall A t, [ A ]₁ t -> [A]ₙ. Proof. intros A t t1 k. simple refine (t1 _ k). Qed. (** * CPS Translation of terms/types *) Section CPS. (** From now on, we assume that we have two types A and B, B being dependent on A, and that we know their translation [A]₀ and [B]₀ that we denote here by A₀ and B₀. *) Context (A0 : Type) (B0 : A0 -> Type). (** ** Dependent product/application *) (** Translation of the dependent product: [Π(x:A).B]₀ = Π(x:[A]₀).[B] *) Definition Pi0 := forall x : A0, [B0 x]. (* Remember that [B₀ x] is {u : B0 x & T (B0 x) u}.*) (** *** λ(x:A).t / Π(x:A).B *) Section lam. (** We want to translate λ(x:A).t. We assume that we already have [t]₀ and [t]₁. *) Context (t0 : forall x : A0, B0 x) (t1 : forall x : A0, [B0 x]₁ (t0 x)). (** [λ(x:A).t]₀ = λ(x:[A]₀).([t]₀,[t]₁) *) Definition lam0 : Pi0 := fun x => (t0 x; t1 x). (** [λ(x:A).t]₁ = λ(R:[Π(x:A).B]₀ → □).λ(k:Π(z:[Π(x:A).B]₀).R z).k [λ(x:A).t]₀) *) Definition lam1 : T Pi0 lam0:= fun (R:Pi0 -> Type) (k:forall z,R z) => k lam0. (** [λ(x:A).t]ₙ = λ(k:[Π(x:A).B]₀) → ⊥).k [λ(x:A).t]₀ *) Definition lamneg : [ Pi0 ]ₙ:= fun k => k lam0. End lam. Section lamn. (** We want to translate λ(x:A).t with a negative translation. We assume that we already have [t]ₙ. *) (** In that setting : [Π(x:A).[B]]₀= Π(x:[A]₀).[B]ₙ [Π(x:A).[B]]₁ t= ∀(R:[Π(x:A).[B]]₀ → □). (Π(z:(Π(x:[A]₀).[B]ₙ)).R z) → R t [Π(x:A).[B]]ₙ= ¬¬ (Π(x:[A]₀).[B]ₙ). *) Definition Pin0:=forall x : A0, [B0 x]ₙ. Context (tn : forall x : A0, [B0 x]ₙ). (** [λ(x:A).t]₀ = λ(x:[A]₀).[t]ₙ *) Definition lamn0 : Pin0 := fun x => tn x. (** [λ(x:A).t]₁ = λ(R:[Π(x:A).B]₀ → □).λ(k:Π(z:[Π(x:A).B]₀).R z).k λ(x:[A]₀).[t]ₙ *) Definition lamn1 : [Pin0]₁ lamn0:= fun (R:Pin0 -> Type) (k:forall z,R z) => k lamn0. (** [λ(x:A).t]ₙ = λ(k:[Π(x:A).B]₀→⊥).k λ(x:[A]₀).[t]ₙ *) Definition lamn : [Pin0]ₙ:= fun k => k lamn0. End lamn. (** *** Application *) Section app. (** We want to translate the application rule: Γ⊢t:Π(x:A).B Γ⊢u:A —————————————————————– Γ⊢tu:B[u/x] By induction, we then suppose we have [t]₀,[t]₁,[u]₀ and [u]₁.*) Context (t0 : Pi0) (u0 : A0) (t1 : T Pi0 t0) (u1 : T A0 u0). (** [tu]₀ = π₁([t]₀[u]₀) *) Definition app0 : B0 u0 := (t0 u0).1. (** [tu]₁ = λRk. [t]₁ S λx₁.(([u]₁ T (λx₂.x₁x₂)) R k) for well-chosen S and T. *) Definition app1 : [B0 u0]₁ app0. intros R k. apply (t1 (fun(x1 : Pi0) => R (x1 u0).1)). intro f0. revert k. revert R. pose (T:=(fun x2 => forall (R0 : B0 x2 -> Prop), (forall x : B0 x2, R0 x) -> R0 (f0 x2).1 )). apply (u1 T). intros x2. apply ((f0 x2).2). Defined. (** Equivalently, we could have directly defined : app1 := fun R k => let S := (fun x1 : Pi0 => R (x1 u0).1) in let k1 := (fun x1 => let T:= fun x2 => forall (R0 : B0 x2 -> Type), (forall x : B0 x2, R0 x) -> R0 (x1 x2).1 in (u1 T (fun x2 => (x1 x2).2)) R k) in t1 S k1. *) End app. Section appn. (** We want to translate negatively a dependent application, i.e. we want a term of type ¬¬ [B[u/x]]ₙ. This requires to consider an application tu where: - t is of type Π(x:A).B - u is of type A and u NEF. By induction we thus assume that we have [t]ₙ,[u]₀ and [u]₁.*) Context (u0 : A0) (u1 : T A0 u0) (tn : [Pi0]ₙ). (** [tu]ₙ = λk. [t]ₙ λx.([u]₁ S (λy.xy)) k with S = (λ y ⇒ ¬¬ [B y]₀). *) Definition app_neg : [B0 u0]ₙ. intros k. apply tn. intro x. apply (u1 (fun y => ((B0 y) -> False ) -> False)). intros y. apply ((x y).2). apply k. Defined. End appn. (** *** let x := u in t *) Section letin. Context (t0 : forall x : A0, B0 x) (u0 : A0) (t1 : forall x : A0, [B0 x]₁ (t0 x)) (u1 : T A0 u0). (** [let x := u in t]₀ = let x := [u]₀ in [t]₀ *) Definition letin0 : B0 u0 := let x:=u0 in t0 x. (** [let x := u in t]₁ = [u]₁ S (λy.let x:=y in [t]₁) where S = λy.[B y]₁ (let x:=y in [t0]) *) Definition letin1 : T (B0 u0) letin0 :=(u1 (fun y => T (B0 y) (t0 y)) (fun y=> let x:=y in t1 x)). End letin. Section letinn. (** Here again, this requires to conside a term let x:= u in t where: - t is of type Π(x:A).B - u is of type A and u NEF. By induction we thus assume that we have [t]ₙ,[u]₀ and [u]₁.*) Context (u0 : A0) (u1 : T A0 u0) (tn : forall x : A0, [B0 x]ₙ). (** [let x := u in t]ₙ = [u]₁ S (λy.let x:=y in [t]ₙ) where *) Definition letinn : [B0 u0]ₙ :=(u1 (fun y => [B0 y]ₙ) (fun y=> let x:=y in tn x)). (* A VOIR *) End letinn. Section pairdep. (** We want to define the inhabitant of the translation of a Σ-type : [Σ(x:A).B]₀ = Σ(x:[A]₀).[B]₀ *) Context (t0 : A0) (u0 : B0 t0) (t1 : T A0 t0) (u1 : T (B0 t0) u0). (** [(t,u)]₀ = ([t]₀,[u]₀) *) Definition pair0 : { x : A0 & B0 x} := (t0;u0). (** [(t,u)]₁ = λRk . [u]₁ S ([t]₁ T (λxy.k (x,y))) with S = λy.R ([t]₀,y) T = λx.Π(y:[B x]₀).R (x,y) *) Definition pair1 : [{ x : A0 & B0 x}]₁ pair0. intros R k. apply (u1 (fun y => R (t0;y))). apply (t1 (fun x => forall y : B0 x, R (x; y))). intros x y. exact (k (x;y)). Defined. End pairdep. Section pairn. (** We want to define the negative translation for Σ: [Σ(x:A).B]ₙ = ¬¬(Σ(x:[A]₀).[B]₀) This requires to consider the translation of a pair (t,u) with t NEF. *) Context (t0 : A0) (t1 : T A0 t0) (un : [B0 t0]ₙ). (** [(t,u)]ₙ = λRk . [u]₁ ([t]₁ T (λxy.k (x,y))) with T = λx.Π(y:[B x]₀). ⊥ *) Definition pairn : [{ x : A0 & B0 x}]ₙ. intros k. apply un. apply (t1 (fun x => B0 x -> False)). intros x y. exact (k (x;y)). Qed. End pairn. Section proj. (** We want to define the translation of the rules: Γ ⊢ t : Σ(x:A).B Γ ⊢ t : Σ(x:A).B –————————————–———– ———————————————–———– Γ ⊢ π₁(t):A Γ ⊢ π₂(t):B[π₁(t)/x] *) Context (t0 : { x : A0 & B0 x}) (t1: [{ x : A0 & B0 x}]₁ t0). (** [π₁(t)]₀ = π₁([t]₀) [π₁(t)]₁ = λRk.[t]₁ (λx.R π₁(x)) (λx.k π₁(x)) *) Definition fst0 : A0:= t0.1. Definition fst1 : T A0 fst0:= fun R k => t1 (fun x => R (x.1)) (fun x => k (x.1)). (** [π₂(t)]₀ = π₂([t]₀) [π₂(t)]₁ = [t]₁ S (λxRk.k π₂(x)) with S = λ(z:Σ(x:[A]₀).[B]₀).∀(R:[B π₁(z)]₀ → □) (k:Π(x:[B π₁(z)]₀).R x). R π₂(z) *) Definition snd0 : B0 fst0:= t0.2. Definition snd1 : T (B0 fst0) snd0. unfold snd0. unfold fst0. pose (S:=(fun z : {x : A0 & B0 x} => forall R : B0 z.1 -> Prop, (forall x : B0 z.1, R x) -> R z.2)). simple refine (t1 S _). intros z R k. apply k. Defined. Definition sncdn : Tneg (B0 fst0). intros k. pose (k':=fun (z:{x:A0 & B0 x}) (k:forall (y:B0 (z.1)),False) => k (z.2)). revert k. unfold T in t1. apply (t1 (fun z => (B0 (z.1) -> False) -> False) k'). Defined. End proj. Section Bool. (** true/false *) Definition true0 : bool:= true. Definition true1 : [bool]₁ true0:= fun R k => k true0. Definition false0 : bool := false. Definition false1 : [bool]₁ false0:= fun R k => k false0. (** Dependent elimination *) (** We want to validate the following rule : Γ⊢b:B Γ⊢t:T true Γ⊢f:T false –————————————–———–———————————————–———— Γ ⊢ t : T b *) Section DependentElim. Context (T0:bool->Type) (e0:bool) (e1:[bool]₁ e0) (t0:T0 true) (t1:[T0 true]₁ t0) (f0:T0 false) (f1:[T0 false]₁ f0). Definition ifthenelseb b: T0 b:= if b as b0 return T0 b0 then t0 else f0. (** [if e then t else f]₀ = if [e]₀ then [t]₀ else [f]₀ *) Definition ifthenelse0 : T0 e0 := ifthenelseb e0. (** [if e then t else f]₁ = [e]₁ then [t]₀ else [f]₀ *) Definition ifthenelse1 : [T0 e0]₁ (ifthenelse0). pose (S:=fun (b:bool) => forall (R:T0 b -> Prop), (forall x, R x) -> R (ifthenelseb b)). apply (e1 S). intros b; destruct b;[apply t1|apply f1]. Defined. (* Definition ifthenelse2 : [T0 e0]₁ (ifthenelse0):= *) (* let S:=fun (b:bool) => *) (* forall (R:T0 b -> Prop), (forall x, R x) -> R (if b as b0 return (T0 b0) then t0 else f0) *) (* in e1 S (fun b => (if b as b0 return S b0 then t1 else f1)). *) End DependentElim. Section IfThenElsen. Context (T:bool->Type) (Tn: Type) (e0:bool) (e1:[bool]₁ e0) (t:[T true]ₙ) (f:[T false]ₙ). Definition ifthenelsen : [T e0]ₙ:= let S := fun b : bool => (T b -> False) -> False in e1 S (fun (b : bool) (k : T b -> False) => (if b as b0 return ((T b0 -> False) -> False) then fun k0 => t k0 else fun k0 => f k0) k). End IfThenElsen. Section IfThenElseNoDep. Context (T:bool->Type) (Tn: Type) (e:[bool]ₙ) (t:[T true]ₙ) (tn: [Tn]ₙ) (f:[T false]ₙ) (fn: [Tn]ₙ). Definition truen : [bool]ₙ := fun k => k true. Definition falsen : [bool]ₙ := fun k => k false. Definition ifthenelsenodep : [Tn]ₙ:= fun k => e (fun b:bool => if b then tn k else fn k). End IfThenElseNoDep. End Bool. Section Equality. Context (x y:A0). Context (p0:B0 y) (p1:[B0 y]₁ p0). Context (e0: x=y) (e1:[x=y]₁ e0). Definition refl0:= eq_refl x. Definition refl1: [x=x]₁ refl0:= fun R k => k refl0. Definition subst_aux (p:B0 y) z: B0 x := eq_rect_r (fun x : A0 => B0 x) p z. Definition subst0 : B0 x := subst_aux p0 e0. Definition subst1 : [B0 x]₁ subst0:= fun R k => e1 (fun z => R (subst_aux p0 z)) (fun e => p1 (fun p => R (subst_aux p e)) (fun p => k (subst_aux p e))). Definition substn (pn:[B0 y]ₙ) (en:[x=y]ₙ): [B0 x]ₙ:= fun k => pn (fun p => en (fun e => k (eq_rect_r (fun x => B0 x) p e))). End Equality. Set Printing Universes. Section types. Universes z i j k. (** By this we actually mean j = i + 1 and k = j + 1. *) Constraint i < j. Constraint j < k. (** For A:□ᵢ a type, the general scheme is as follows: [A]₀ = (〚A〛₀,〚A〛₁) : Σ(A:□ᵢ).A→Prop *) (** ** Translation of □ᵢ *) (** ◪ᵢ := Σ(A:□ᵢ).(A → Prop) : □ᵢ₊₁ *) Definition typeTrad@{i}:= { A:Type@{i} & A -> Prop }. Notation "◪" := typeTrad. (** [□ᵢ]₀ : ◪ᵢ₊₁ := (◪ᵢ,〚◪ᵢ〛₁ ) = (◪ᵢ,λ(A:◪ᵢ).Π(R:◪ᵢ→Prop).Π(_:Π(A₀:◪ᵢ).R A₀).R A) *) Definition typeZero@{i} : typeTrad@{j}. exists typeTrad@{i}. exact (T@{j} (typeTrad@{i})). Defined. (** [□ᵢ]₁ : 〚◪ᵢ₊₁〛₁ [□ᵢ]₀ = Π(R:◪ᵢ₊₁→Prop).Π(_:Π(A₀:◪ᵢ₊₁).R A₀).R A) := λ(R:◪ᵢ₊₁→Prop).λ(k:Π(A₀:◪ᵢ₊₁).R A₀).k [□ᵢ]₀ *) Definition typeOne@{i} : T@{k} (typeTrad@{j}) typeZero@{i} := fun R k => k typeZero@{i}. (** ** Translation of Π(x:A).B *) Context (A : Type@{i}) (B : A -> Type@{i}). Definition Pi:Type@{i} := forall (x:A),B x. (** Translation of the dependent product: [Π(x:A).B]₀ : 〚□ᵢ〛₀ = [□ᵢ]₀.1 = ◪ᵢ := (Π(x:[A]₀).〚B〛, λf⇒ [Π(x:[A]₀).〚B〛]₁ f) *) Definition tradPi0 : typeZero@{i}.1. exists (forall (x:A),generous (B x)). exact (fun f => T (forall (x:A),generous (B x)) f). Defined. (** Translation of the dependent product: [Π(x:A).B]₁ : 〚□ᵢ〛₁ [Π(x:A).B]₀ := λRk. k [Π(x:A).B]₀ *) Definition tradPi1 : typeZero@{i}.2 tradPi0. simpl. intros R k. exact (k tradPi0). Defined. (** ** Translation of Σ(x:A).B *) Definition Sigma:Type@{i} := {x:A & B x}. (** Translation of the dependent product: [Σ(x:A).B]₀ : 〚□ᵢ〛₀ = [□ᵢ]₀.1 = ◪ᵢ := (Σ(x:[A]₀).〚B〛₀, λf⇒ [Σ(x:[A]₀).[B]₀]₁ f) *) Definition tradSigma0 : typeZero@{i}.1. exists (Sigma). exact (fun f => T (Sigma) f). Defined. (** Translation of the dependent product: [Σ(x:A).B]₁ : 〚□ᵢ〛₁ [Σ(x:A).B]₀ := λRk. k [Σ(x:A).B]₀ *) Definition tradSigma1 : typeZero@{i}.2 tradSigma0. simpl. intros R k. exact (k tradSigma0). Defined. (** ** Translation of bool *) Definition tradBool0 : typeTrad@{Set} := (bool;T@{z} (bool)). Definition tradBool1 : T typeTrad@{Set} tradBool0 := fun R k => k tradBool0. (** ** Translation of Prop *) (** [Prop]₀ : ◪₀ = Σ(A:□₀).(A → Prop) := (Σ(A:Prop).A→Prop, [Σ(A:Prop).A→Prop]₁) *) (* No constraint on z, in particular true for z=0. *) Definition tradProp0 : typeTrad@{z}. exists {A:Prop & A -> Prop }. exact (T@{z} ({A:Prop & A -> Prop })). Defined. (** [Prop]₁ : 〚◪₀〛₁ [Prop]₀ = Π(R:◪ᵢ₊₁→Prop).Π(_:Π(A₀:◪ᵢ₊₁).R A₀).R A) := λ(R:◪ᵢ₊₁→Prop).λ(k:Π(A₀:◪ᵢ₊₁).R A₀).k [□ᵢ]₀ *) Definition tradProp1 : T (typeTrad@{z}) tradProp0 := fun R k => k tradProp0. (** ** Translation of = *) Definition tradEquality0 (x:A0) : tradProp0.1 := (x=x;T (x=x)). Definition tradEquality1 (x:A0): tradProp0.2 (tradEquality0 x) := fun R k => k (tradEquality0 x). Section PiProp. Context (C0 : A0 -> Prop) (C1 : forall x:A0, T Prop (C0 x)). Definition PiProp : Prop := forall x, C0 x. (** Translation of the dependent product: [Π(x:A).C]₀ : 〚Prop〛₀ = [Prop]₀.1 = Prop := (Π(x:[A]₀).〚B〛, λf⇒ [Π(x:[A]₀).〚B〛]₁ f) *) Definition tradPiProp0 : tradProp0.1 := let PiP := forall x:A0, exists y:C0 x, forall (R:C0 x -> Prop), (forall z, R z) -> R y in (PiP; fun f : PiP => [PiP ]₁ f). Definition tradPiProp1 : tradProp0.2 tradPiProp0 := (fun R k=> k tradPiProp0). End PiProp. Section SigmaProp. Context (C0 : A0 -> Prop) (C1 : forall x:A0, T Prop (C0 x)). Definition SigmaProp : Prop := ex C0. Definition tradSigmaProp0 : tradProp0.1:= existT (fun A : Prop => forall _ : A, Prop) SigmaProp (fun f : SigmaProp => [SigmaProp]₁ f). Definition tradSigmaProp1 : tradProp0.2 tradSigmaProp0 := (fun R k=> k tradSigmaProp0). End SigmaProp. End types. Section Reduction. Section lam_letin. Context (t0 : forall x : A0, B0 x) (t1 : forall x : A0, [B0 x ]₁ (t0 x)) (u0 : A0) (u1 : [A0 ]₁ u0). Definition e0:=lam0 t0 t1. Definition e1:=lam1 t0 t1. Lemma lam_letin : app1 e0 u0 e1 u1 = letin1 t0 u0 t1 u1. Proof. reflexivity. Qed. End lam_letin. Section ifred. Context (T0 : bool -> Type) (t0 : T0 true) (t1: [T0 true ]₁ t0) (f0 : T0 false) (f1:[T0 false ]₁ f0). Lemma iftrue : ifthenelse1 T0 true0 true1 t0 t1 f0 f1 = t1. Proof. reflexivity. Qed. Lemma iffalse : ifthenelse1 T0 false0 false1 t0 t1 f0 f1 = f1. Proof. reflexivity. Qed. End ifred. Section projred. Context (t0 : A0) (u0 : B0 t0) (t1 : T A0 t0) (u1 : T (B0 t0) u0). Axiom param : forall A t0 (t1:T A t0) R k, t1 R k = k t0. Lemma fstred R k: fst1 (pair0 t0 u0) (pair1 t0 u0 t1 u1) R k= t1 R k. Proof. unfold fst1, pair0, pair1. simpl. repeat rewrite param. reflexivity. Qed. Lemma sndred R k: snd1 (pair0 t0 u0) (pair1 t0 u0 t1 u1) R k= u1 R k. Proof. unfold snd1, pair0, pair1. simpl. repeat rewrite param. reflexivity. Qed. End projred. End Reduction. End CPS.