Revision 1c783fb2a09f78c7d1bd2f27008221724fe204d0 authored by Martin Baillon on 08 July 2021, 22:02:58 UTC, committed by Martin Baillon on 08 July 2021, 22:02:58 UTC
1 parent 2a2e136
Translation.v
Set Primitive Projections.
Set Universe Polymorphism.
Require Import Dialogue.
Require Import Base.
Section AxiomTranslation.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Variables (X Y : Type).
Implicit Type (A B : Type).
(*In this section we present the Axiom translation,
which adds an oracle α : X -> Y in the context.
We use a Cwf-like presentation *)
(*In the axiom translation, the empty context is
translated as α : X -> Y. As such, there is no empty
context in the image of the translation, and all contexts
depend on α.*)
Definition ACtx := (X -> Y) -> Type.
(*A type is a function from contexts to Type*)
Definition ATy (Gamma : ACtx) : Type :=
forall α : X -> Y, Gamma α -> Type.
(*Type is translated as the constant function
that always returns Type*)
Definition AType {Gamma : ACtx} : ATy Gamma :=
fun α gamma => Type.
(*AEl is the axiom version of Tarsky's El function*)
Definition AEl (Gamma : ACtx) (A : ATy Gamma) :
Type :=
forall (α : X -> Y) (gamma : Gamma α), A α gamma.
(*Empty context*)
Definition ACtx_nil : ACtx := fun α => unit.
Notation "()" := (ACtx_nil).
(*Context extension*)
Definition ACtx_cons (Gamma : ACtx) (A : ATy Gamma) :
ACtx:=
fun (α : X -> Y) => tsig (fun (gamma : Gamma α) => A α gamma).
Notation "Γ · A" := (@ACtx_cons Γ A) (at level 50, left associativity).
Definition Actx_cons (Gamma : ACtx) (A : ATy Gamma) (α : X -> Y)
(gamma : Gamma α) (a : A α gamma) : (ACtx_cons A) α.
Proof.
exists gamma ; exact a.
Defined.
Notation "γ ·· x" := (@Actx_cons γ x) (at level 50, left associativity).
(*In what follows, we deal with the negative fragment
of type theory : Weakening, Pi-types, Substitution, etc*)
(*Lifting rule*)
Definition ALift
(Gamma : ACtx) (A : ATy Gamma) (B : ATy Gamma) :
ATy (ACtx_cons A) :=
fun α gamma => B α gamma.(fst).
Notation "⇑ A" := (@ALift _ _ A) (at level 10).
(*Weakening rule*)
Definition AWeaken {Γ : ACtx} {R S : ATy Γ} (r : AEl R) :
@AEl (ACtx_cons S) (@ALift _ S R).
Proof.
+ refine (fun α γr => r α γr.(fst)).
Defined.
Notation "↑ M" := (@AWeaken _ _ _ M) (at level 10).
(*Variable rule*)
Definition AVar (Gamma : ACtx)
(A : ATy Gamma) :
AEl (@ALift Gamma A A) :=
fun (α : X -> Y) (gamma : ACtx_cons A α) => gamma.(snd).
Notation "#" := (@AVar _ _) (at level 0).
(*Substitution*)
Definition ASub (Gamma : ACtx) (A : ATy Gamma)
(B : ATy (ACtx_cons A)) (a : AEl A) : ATy Gamma :=
fun α gamma => B α (exist (a α gamma)).
Notation "S {{ r }} " := (ASub S r) (at level 20, left associativity).
(*Pi-type*)
Definition APi (Gamma : ACtx) (A : ATy Gamma)
(B : ATy (ACtx_cons A)) : ATy Gamma :=
fun α gamma =>
forall a : A α gamma, B α (exist a).
Notation "∏" := (@APi).
Notation "A → B" := (@APi _ A (⇑ B)) (at level 99, right associativity, B at level 200).
(*Introduction for Pi*)
Definition ALam (Gamma : ACtx) (A : ATy Gamma)
(B : ATy (ACtx_cons A))(f : AEl B)
: AEl (APi B) :=
fun (α : X -> Y) (gamma : Gamma α) (a : A α gamma) => f α (exist a).
Notation "'λ'" := (@ALam).
(*Introduction of the non-dependent arrow*)
Definition ALamN {Γ : ACtx } {A : ATy Γ} {B : ATy Γ}
(f : @AEl (Γ · A) (⇑ B)) : @AEl Γ (A → B) :=
@ALam Γ A (⇑ B) f.
(*Elimination for Pi*)
Definition AApp {Γ : ACtx}
{A : ATy Γ} {B : ATy (@ACtx_cons Γ A)}
(f : @AEl Γ (APi B)) (x : @AEl Γ A) : @AEl Γ (ASub B x) :=
fun α γr => f α γr (x α γr).
Notation "t • u" := (@AApp _ _ _ t u) (at level 12, left associativity).
(*Elimination of the non-dependent arrow*)
Definition AAppN {Γ : ACtx } {A : ATy Γ} {B : ATy Γ}
(f : @AEl Γ (A → B))(x : @AEl Γ A) : @AEl Γ B :=
@AApp Γ A (⇑ B) f x.
Notation "t ◊ u" := (@AAppN _ _ _ t u) (at level 12, left associativity).
(*It is now time to define the translation
of various inductive types*)
(*The translation of booleans*)
Definition Abool {Gamma : ACtx} : ATy Gamma := fun α gamma => bool.
Definition Atrue (Gamma : ACtx) : AEl (@Abool Gamma) :=
fun α gamma => true.
Definition Afalse (Gamma : ACtx) : AEl (@Abool Gamma) :=
fun α gamma => false.
(* The Axiom translation builds a model of full-CIC as soon as X->Y
is not empty, but the global translation will be a model of BTT.
Thus, we only define the Axiom translation for BTT*)
(*Non-dependent eliminator for booleans*)
Definition Abool_rec (Γ : ACtx) :
@AEl Γ (∏ Γ AType ((@AVar _ AType) → (@AVar _ AType) → Abool → (@AVar _ AType))) :=
fun α ga P ptrue pfalse b => match b with
| true => ptrue
| false => pfalse
end.
(*Storage operator for booleans, in direct style*)
Definition Abool_stor {Γ : ACtx} :
AEl (Abool → (Abool → AType) → AType) :=
fun α ga b P => @Abool_rec Γ α ga ((bool -> Type) -> Type)
(fun k => k true)
(fun k => k false)
b P.
(*Restricted dependent-eliminator for booleans.*)
Definition Abool_rect (Γ : ACtx) :
AEl (∏ Γ (Abool → AType)
((@AApp _ Abool AType # (@Atrue _)) →
((@AApp _ Abool AType # (@Afalse _)) →
(∏ _ Abool (Abool_stor • # • (↑#)))))) :=
fun α gamma P ptrue pfalse b =>
match b with
| true => ptrue
| false => pfalse
end.
(*The translation of natural numbers*)
Definition Anat {Γ : ACtx} : ATy Γ := fun α gamma => nat.
Definition A0 {Γ : ACtx} : AEl (@Anat Γ) := fun α gamma => 0.
Definition ASucc {Γ : ACtx} :
AEl (∏ Γ (@Anat Γ) (@Anat (ACtx_cons (@Anat Γ)))) :=
fun _ _ n => S n.
(*Non-dependent eliminator for natural numbers*)
Definition Anat_rec (Γ : ACtx) :
@AEl Γ (∏ Γ AType
(@AVar _ AType →
(Anat → (@AVar _ AType) → (@AVar _ AType)) →
Anat →
(@AVar _ AType))).
Proof.
refine (fun α gamma P p0 pS => _).
refine (fix f n := match n with
| 0 => p0
| S k => pS k (f k)
end).
Defined.
(*Storage operator for natural numbers. In direct style it amounts to :
Definition Nat_stor (n : nat) (P : nat -> Type) : Type :=
@Nat_rec ((nat -> Type) -> Type)
(fun P => P 0)
(fun n P k => k (S n))
n P.*)
Definition Anat_stor{Γ : ACtx } :
@AEl Γ (Anat → (Anat → AType) → AType).
Proof.
pose (r := @AApp _ _ _ (@Anat_rec Γ) ((Anat → AType) → AType)).
let T := constr:(@AEl Γ (((Anat → AType) → AType) → (Anat → ((Anat → AType) → AType) → ((Anat → AType) → AType)) → Anat → ((Anat → AType) → AType))) in
unshelve refine (let r : T := r in _).
unshelve refine (AApp (AApp r _) _).
- refine (ALamN (@AAppN _ Anat _ _ _)).
+ now refine (@AVar _ _).
+ now refine (@A0 _).
- refine (@ALamN _ _ _ _).
refine (@ALamN (@ACtx_cons Γ Anat) (⇑ ((Anat → AType) → AType)) (⇑ ((Anat → AType) → AType)) _).
refine (@ALamN (Γ · Anat · (⇑ ((Anat → AType) → AType)))
(⇑(⇑(Anat → AType))) (⇑ (⇑ AType)) _).
refine (@AAppN _ Anat _ _ _).
+ now refine #.
+ now refine (@AAppN _ Anat _ (@ASucc _) (↑↑#)).
Defined.
(*Restricted dependent-eliminator for natural numbers.*)
Definition Anat_rect {Γ : ACtx} :
@AEl Γ (∏ _ (Anat → AType)
((@AApp _ _ AType # A0) →
(∏ _ Anat ((Anat_stor • # • (↑#)) →
(Anat_stor • (ASucc • #) • (↑#)))) →
∏ _ Anat (Anat_stor • # • (↑#)))).
Proof.
unshelve refine (fun α γ P p0 pS => _).
refine (fix g n := match n as n0 return
(fix f (n : nat) : (nat -> Type) -> Type :=
match n with
| 0 => fun a0 : nat -> Type => a0 0
| S k => fun a0 : nat -> Type => a0 (S k)
end) n0 P
with
| 0 => p0
| S k => pS k (g k)
end).
Defined.
(*Our definitions "computes", that is : Anat_rect P p0 pS 0 reduces to p0
and Anat_rect P p0 pS (S k) reduces to pS k (Anat_rect P p0 pS k) *)
Goal forall (Γ : ACtx)
(P : @AEl Γ (Anat → AType))
(T0 := (P • (@A0 _)))
(p0 : @AEl Γ T0)
(TS := (∏ _ Anat ((@AApp (Γ · Anat) _ AType
(@AApp (Γ · Anat) _ _ Anat_stor #) (↑P)) →
(@AApp (Γ · Anat) _ AType
(@AApp (Γ · Anat) _ _ Anat_stor
(@AApp (Γ · Anat) _ _ (@ASucc _) #)) (↑P)))))
(pS : @AEl Γ TS)
(TR := ∏ Γ Anat (Anat_stor • @AVar _ Anat • ↑ P))
,
@AApp Γ _ _ (@AAppN Γ _ _ (@AAppN Γ T0 (TS → TR) ((@Anat_rect Γ) • P) p0) pS) (@A0 _)
=
p0.
Proof. reflexivity. Qed.
Goal forall (Γ : ACtx)
(P : @AEl Γ (Anat → AType))
(T0 := (P • (@A0 _)))
(p0 : @AEl Γ T0)
(TS := (∏ _ Anat ((@AApp (Γ · Anat) _ AType
(@AApp (Γ · Anat) _ _ Anat_stor #) (↑P)) →
(@AApp (Γ · Anat) _ AType
(@AApp (Γ · Anat) _ _ Anat_stor
(@AApp (Γ · Anat) _ _ (@ASucc _) #)) (↑P)))))
(pS : @AEl Γ TS)
(TR := ∏ Γ Anat (Anat_stor • @AVar _ Anat • ↑ P))
(n : @AEl Γ Anat)
,
forall (α : X -> Y) (γr : Γ α),
(@AApp Γ _ _ (@AAppN Γ _ _ (@AAppN Γ T0 (TS → TR) ((@Anat_rect Γ) • P) p0) pS) (AApp (@ASucc _) n)) α γr
=
(@AAppN Γ (@AApp Γ (Anat → AType) _ (@AApp Γ _ _ Anat_stor n) P) (Anat_stor • ((@ASucc _) • n) • P) (AApp pS n) (@AApp Γ _ _ (@AAppN Γ _ _ (@AAppN Γ T0 (TS → TR) ((@Anat_rect Γ) • P) p0) pS) n)) α γr.
Proof. reflexivity. Qed.
(*Translation of equality*)
Inductive Eq {A : Type} (x : A) : A -> Type := Eq_refl : Eq x x.
Definition Aeq {Γ : ACtx} : AEl (∏ Γ AType (# → # → AType)) :=
fun _ _ => @Eq.
Definition Arefl {Γ : ACtx} :
AEl (∏ Γ AType
(∏ _ #
(Aeq • (↑#) ◊ # ◊ #))) :=
fun _ _ => @Eq_refl.
(*Non-dependent eliminator for equality*)
Definition Aeq_rec (Γ : ACtx) :
@AEl Γ (∏ Γ AType
(∏ _ #
(∏ (Γ · AType · (@AVar _ AType))
((↑#) → AType)
(((@AVar (Γ · AType · (@AVar _ AType))
((↑(@AVar _ AType)) → AType)) ◊ ↑#) →
(∏ (Γ · AType · (@AVar _ AType) · ((↑#) → AType))
(↑↑#)
((((Aeq • (↑↑↑(@AVar _ AType))) ◊ ↑↑#) ◊ #) →
((↑(@AVar (Γ · AType · (@AVar _ AType))
((↑(@AVar _ AType)) → AType))) ◊ #))))))) :=
fun α γ A x P px y e =>
match e as e0 in (Eq _ y0) return (P y0) with
| Eq_refl _ => px
end.
(*Storage operator for equality, in direct style*)
Definition Aeq_stor {Γ : ACtx} :
@AEl Γ (∏ Γ AType
(∏ _ #
(∏ _ (↑#)
((((Aeq • (↑↑(@AVar _ AType))) ◊ ↑#) ◊ #) →
(∏ _ (↑↑#)
((((Aeq • (↑↑↑(@AVar _ AType))) ◊ (↑↑#)) ◊ #) →
AType)) →
AType)))) :=
fun α γ A x y e P =>
@Aeq_rec Γ α γ A x (fun z => ((Eq x z -> Type) -> Type))
(fun k => k (Eq_refl x)) y e (P y).
(*Restricted dependent-eliminator for equality.
Unfortunately, due to unification problems, Coq
crashes before it can even compute the type of
Aeq_rect.
That is why we leave this in comment mode.
Definition Aeq_rect (Γ : ACtx) :
@AEl Γ (∏ Γ AType
(∏ _ #
(∏ _ (∏ _ (↑#) ((((Aeq • (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) →
AType))
(((@AApp (Γ · AType · (@AVar _ AType) · (∏ _ (↑#) ((((Aeq • (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) → AType)))
(↑↑#) ((((Aeq • (↑↑↑(@AVar _ AType))) ◊ (↑↑#)) ◊ #) → AType) # (↑#)) ◊
(@AApp (Γ · AType · (@AVar _ AType) · (∏ _ (↑#) ((((Aeq • (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) → AType))) (↑ (↑ #)) (Aeq • ↑ (↑ (↑ #)) ◊ # ◊ #) (Arefl • (↑↑#)) (↑#))) →
∏ (Γ · AType · (@AVar _ AType) · (∏ _ (↑#) ((((Aeq • (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) → AType)))
(↑↑#)
(∏ _ (((Aeq • (↑↑↑(@AVar _ AType))) ◊ (↑↑#)) ◊ #)
((@AApp _ (↑↑↑↑(@AVar _ AType)) _
(@AApp (Γ · AType · (@AVar _ AType) ·
(∏ _ (↑#) ((((@AApp _ AType ((# → # → AType)) Aeq (↑↑(@AVar _ AType))) ◊ (↑#)) ◊ #) → AType)) ·
(↑↑#) ·
(((Aeq • (↑↑↑(@AVar _ AType))) ◊ (↑↑#)) ◊ #))
(↑↑↑↑(@AVar _ AType)) _
(@AApp _ AType _
Aeq_stor (↑↑↑↑(@AVar _ AType)))
(↑↑↑#))
(↑#))
◊ # ◊ (↑↑#))))))).
*)
(*Translation of lists*)
Inductive list (A : Type) : Type :=
nil : list A | cons : A -> list A -> list A.
Arguments nil {A}.
Definition Alist {Γ : ACtx} : @AEl Γ (AType → AType) :=
fun α gamma a => list a.
Definition Anil {Γ : ACtx} :
AEl (∏ Γ AType (Alist • (@AVar _ AType))) := fun α ga A => @nil A.
Definition Acons {Γ : ACtx} :
AEl (∏ Γ AType
((@AVar _ AType) → (Alist • (@AVar _ AType)) → (Alist • (@AVar _ AType)))) :=
fun α gamma A a la => cons a la.
(*Non-dependent eliminator for lists*)
Definition Alist_rec (Γ : ACtx) :
@AEl Γ (∏ Γ AType
(∏ _ AType
(# →
(↑ # → Alist • ↑ # → # → #) →
Alist • ↑ # →
#))).
Proof.
unshelve refine (fun alpha gamma A P pnil pcons => _).
refine (fix f l {struct l} := match l with
| nil => pnil
| cons x q => pcons x q (f q)
end).
Defined.
(*Storage operator for lists, in direct style*)
Definition Alist_stor{Γ : ACtx } :
AEl (∏ Γ AType (Alist • # → (Alist • # → AType) → AType)) :=
fun (α : X -> Y) (_ : Γ α) (A : Type) =>
fix f (l : list A) : (list A -> Type) -> Type :=
match l with
| nil => fun a0 : list A -> Type => a0 nil
| cons x q =>
fun P : list A -> Type =>
f q (fun q' : list A => P (cons x q'))
end.
(*Restricted dependent-eliminator for lists.
Unification problems also appear here, albeit less
serious ones, which is why our definition type-checks,
in a couple of minutes time.*)
Definition Alist_rect {Γ : ACtx} :
@AEl Γ (∏ Γ AType
(∏ _ ((Alist • (@AVar _ AType)) → AType)
((@AAppN _ _ AType # (Anil • (↑(@AVar _ AType)))) →
(∏ _ (↑(@AVar _ AType))
(∏ (Γ · AType · ((Alist • (@AVar _ AType)) → AType) · (↑(@AVar _ AType)))
(Alist • (↑↑(@AVar _ AType)))
((((Alist_stor • (↑↑↑(@AVar _ AType)))
◊ (@AVar _ ((Alist • (↑↑(@AVar _ AType)))))
◊ (↑↑(@AVar _ ((Alist • (@AVar _ AType)) → AType))))) →
(((Alist_stor • (↑↑↑(@AVar _ AType)))
◊ ((Acons • (↑↑↑(@AVar _ AType))) ◊ (↑#) ◊ #)
◊ (↑↑(@AVar _ ((Alist • (@AVar _ AType)) → AType)))))))) →
∏ (Γ · AType · ((Alist • (@AVar _ AType)) → AType)) (Alist • ↑#)
((Alist_stor • (↑↑(@AVar _ AType))) ◊ # ◊ (↑#))))) :=
fun alpha gamma A P pnil pcons =>
fix f l := match l as l0 return
(fix g (l : list A) : (list A -> Type) -> Type :=
match l with
| nil => fun a0 : list A -> Type => a0 nil
| cons x q =>
fun P : list A -> Type =>
g q (fun q' : list A => P (cons x q'))
end) l0 P
with
| nil => pnil
| cons x q => pcons x q (f q)
end.
End AxiomTranslation.
Section BranchingTranslation.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Variables (X Y : Type).
(*In this section we present the Branching translation,
which interprets all types as algebras of the Dialogue monad.
Again, we use a Cwf-like presentation *)
(*Let us first formalize what is an algebra of the Dialogue monad.*)
Definition BranchingTYPE := {A : Type & (Y -> A) -> X -> A}.
(*In the Branching translation, contexts are translated pointwise.
As such, they are simply types.*)
Definition BCtx := Type.
(*A type is a function from contexts to BranchingType*)
Definition BTy (Gamma : BCtx) := Gamma -> BranchingTYPE.
(*Type is translated as the constant function that always return
BranchingTYPE. The proof of algebraicity is a dummy function.*)
Definition Bunit : BranchingTYPE :=
@exist Type (fun A => (Y -> A) -> X -> A) unit (fun _ _ => tt).
Definition BType {Gamma : BCtx} : BTy Gamma :=
fun _ => @exist Type (fun A => (Y -> A) -> X -> A)
BranchingTYPE (fun _ _ => Bunit).
(*BEl is the branching version of Tarsky's El function*)
Definition BEl {Gamma : BCtx} (A : BTy Gamma) : Type :=
forall (gamma : Gamma), (A gamma).(fst).
(*Empty context*)
Definition BCtx_nil : BCtx := unit.
Notation "()" := (BCtx_nil).
(*Context extension*)
Definition BCtx_cons (Gamma : BCtx) (A : BTy Gamma) :=
tsig (fun (gamma : Gamma) => (A gamma).(fst)).
Notation "Γ · A" := (@BCtx_cons Γ A) (at level 50, left associativity).
Definition Bctx_cons (Gamma : BCtx) (B : BTy Gamma)
(gamma : Gamma) (b : (B gamma).(fst)) : Gamma · B.
Proof.
exists gamma ; exact b.
Defined.
Notation "γ ·· x" := (@Actx_cons γ x) (at level 50, left associativity).
(*In what follows, we deal with the negative fragment
of type theory : Weakening, Pi-types, Substitution, etc*)
(*Lifting rule*)
Definition BLift {Gamma : BCtx} {A : BTy Gamma} (B : BTy Gamma) : BTy (Gamma · A) :=
fun gamma => B gamma.(fst).
Notation "⇑ A" := (@BLift _ _ A) (at level 10).
(*Weakening rule*)
Definition BWeaken {Γ : BCtx} {R S : BTy Γ} (r : BEl R) :
@BEl (Γ · S) (⇑ R).
Proof.
+ refine (fun γr => r γr.(fst)).
Defined.
Notation "↑ M" := (@BWeaken _ _ _ M) (at level 10).
(*Variable rule*)
Definition BVar {Gamma : BCtx}
(A : BTy Gamma) :
BEl (@BLift Gamma A A) :=
fun (gamma : (Gamma · A)) => gamma.(snd).
Notation "#" := (@BVar _ _) (at level 0).
(*Substitution*)
Definition BSub {Gamma : BCtx} (A : BTy Gamma) (B : BTy (Gamma · A)) (a : BEl A) : BTy Gamma :=
fun gamma => B ({|fst := gamma ; snd := a gamma |}).
Notation "S {{ r }} " := (@BSub _ _ S r) (at level 20, left associativity).
(*Pi-type*)
Definition BPi {Gamma : BCtx} {A : BTy Gamma} (B : BTy (Gamma · A)) : BTy Gamma.
Proof.
unshelve refine (fun gamma => exist _).
- exact (forall a : (A gamma).(fst),
(B {| fst := gamma; snd := a|}).(fst)).
- exact (fun f x a => (B {| fst := gamma; snd := a |}).(snd) (fun y => f y a) x).
Defined.
Notation "∏" := (@BPi).
Notation "A → B" := (@BPi _ A (⇑ B)) (at level 99, right associativity, B at level 200).
(*Introduction for Pi*)
Definition BLam {Gamma : BCtx} (A : BTy Gamma) (B : BTy (Gamma · A)) (f : BEl B)
: BEl (BPi B) :=
fun (gamma : Gamma) (a : (A gamma).(fst)) => f {| fst := gamma; snd := a |}.
Notation "'λ'" := (@ALam).
(*Introduction of the non-dependent arrow*)
Definition BLamN {Γ : BCtx } {A : BTy Γ} {B : BTy Γ}
(f : @BEl (Γ · A) (⇑ B)) : @BEl Γ (A → B) :=
@BLam Γ A (⇑ B) f.
(*Elimination for Pi*)
Definition BApp {Γ : BCtx} {A : BTy Γ} {B : BTy (Γ · A)}
(f : BEl (∏ Γ A B)) (x : BEl A) : @BEl _ (B {{ x }}) :=
fun gamma => f gamma (x gamma).
Notation "t • u" := (@BApp _ _ _ t u) (at level 12, left associativity).
(*Elimination of the non-dependent arrow*)
Definition BAppN {Γ : BCtx } {A : BTy Γ} {B : BTy Γ}
(f : @BEl Γ (A → B)) (x : @BEl Γ A) : @BEl Γ B :=
@BApp Γ A (⇑ B) f x.
Notation "t ◊ u" := (@BAppN _ _ _ t u) (at level 12, left associativity).
(*Internal Tarsky's El function*)
Definition BEL {Γ : BCtx } (A : @BEl Γ BType) : BTy Γ := A.
Notation "[ A ]" := (@BEL _ A).
(*It is now time to define the translation
of various inductive types*)
(*The translation of booleans*)
Inductive BranchingBool :=
| Btrue_aux : BranchingBool
| Bfalse_aux : BranchingBool
| Bêtabool : (Y -> BranchingBool) -> X -> BranchingBool.
Definition Bbool {Gamma : BCtx} : BTy Gamma :=
fun gamma => {| fst := BranchingBool; snd := Bêtabool |}.
Definition Btrue {Gamma : BCtx} : BEl (@Bbool Gamma) := (fun _ => Btrue_aux).
Definition Bfalse {Gamma : BCtx} : BEl (@Bbool Gamma) := (fun _ => Bfalse_aux ).
(*Non-dependent eliminator for booleans*)
Definition Bbool_rec {Γ : BCtx} :
@BEl Γ (∏ Γ BType ((@BVar _ BType) → (@BVar _ BType) → Bbool → (@BVar _ BType))).
Proof.
unshelve refine (fun ga P ptrue pfalse => _).
now refine (fix f b := match b with
| Btrue_aux => ptrue
| Bfalse_aux => pfalse
| Bêtabool g x => P.(snd) (fun y => f (g y)) x
end).
Defined.
(*Storage operator for booleans*)
Definition Bbool_stor {Gamma : BCtx} :
@BEl Gamma (Bbool → (Bbool → BType) → BType).
Proof.
exact (fun ga b P => @Bbool_rec Gamma ga
(@BPi Gamma (@BPi Gamma (@Bbool Gamma) (@BType _))
(@BType _) ga)
(fun k => k Btrue_aux)
(fun k => k Bfalse_aux) b P).
Defined.
(*Restricted dependent-eliminator for booleans.*)
Definition Bbool_rect (Γ : BCtx) :
@BEl Γ (∏ _ (Bbool → BType) (
(@BApp (Γ · (Bbool → BType)) Bbool BType # Btrue) →
(@BApp (Γ · (Bbool → BType)) Bbool BType # Bfalse) →
∏ _ Bbool (@BApp _ _ BType
(@BApp (Γ · (Bbool → BType) · Bbool) _ _ Bbool_stor #) (↑#)))) :=
fun ga P ptrue pfalse b =>
match b with
| Btrue_aux => ptrue
| Bfalse_aux => pfalse
| Bêtabool g x => tt
end.
(*The translation of natural numbers*)
Definition Bnat {Gamma : BCtx} : BTy Gamma :=
fun gamma => {| fst := BranchingNat X Y ; snd := @Bêtanat X Y |}.
Definition Bzero {Gamma : BCtx} : BEl (@Bnat Gamma) := fun gamma => @B0 X Y.
Definition BSucc {Gamma : BCtx} :
@BEl Gamma (Bnat → Bnat) :=
fun gamma => (@BS X Y).
(*Non-dependent eliminator for natural numbers*)
Definition Bnat_rec (Γ : BCtx) :
BEl (∏ Γ BType ([#] →
(Bnat → [#] → [#]) →
Bnat →
[#])).
Proof.
- unshelve refine (fun gamma P p0 pS => _).
exact (fix f n := match n with
| B0 _ _ => p0
| BS k => pS k (f k)
| Bêtanat g x => P.(snd) (fun y => f (g y)) x
end).
Defined.
(*Storage operator for natural numbers*)
Definition Bnat_stor {Γ : BCtx} :
@BEl Γ (Bnat → (Bnat → BType) → BType).
Proof.
pose (r := BApp (@Bnat_rec Γ) ((Bnat → BType) → BType)).
let T := constr:(@BEl Γ (((Bnat → BType) → BType) → (Bnat → ((Bnat → BType) → BType) → ((Bnat → BType) → BType)) → Bnat → ((Bnat → BType) → BType))) in
unshelve refine (let r : T := r in _).
unshelve refine (BAppN (BAppN r _) _).
- refine (BLamN (@BAppN _ Bnat _ _ _)).
+ now refine #.
+ now refine Bzero.
- refine (@BLamN _ _ _ _).
refine (@BLamN _ (⇑ ((Bnat → BType) → BType)) (⇑ ((Bnat → BType) → BType)) _).
refine (@BLamN _ (⇑(⇑(Bnat → BType))) (⇑ (⇑ BType)) _).
refine (@BAppN _ Bnat _ _ _).
+ now refine #.
+ now refine (@BAppN _ Bnat _ BSucc (↑↑#)).
Defined.
(*Restricted dependent-eliminator for natural numbers*)
Definition Bnat_rect {Γ : BCtx} :
BEl (∏ Γ (Bnat → BType) (
(@BApp (Γ · (Bnat → BType)) Bnat BType # Bzero) →
(∏ _ Bnat ((Bnat_stor • # • (↑#)) →
(Bnat_stor • (BSucc • #) • (↑#)))) →
∏ _ Bnat (Bnat_stor • # • (↑#)))).
Proof.
unshelve refine (fun γ P p0 pS => _).
exact (fix g n :=
match n with
| B0 _ _ => p0
| BS k => pS k (g k)
| Bêtanat _ _ => tt
end).
Defined.
(*The translation of equality*)
Inductive BranchingEq (A : BranchingTYPE) (a : A.(fst)) : A.(fst) -> Type :=
| Beq_refl : BranchingEq a a
| Bêtaeq : forall (b : A.(fst)), (Y -> BranchingEq a b) -> X -> BranchingEq a b.
Definition Beq {Gamma : BCtx}: BEl (∏ Gamma BType ([#] → [#] → BType)).
Proof.
unshelve refine (fun gamma A x y => exist _).
- exact (@BranchingEq A x y).
- exact (@Bêtaeq A x y).
Defined.
Definition Brefl {Γ : BCtx} :
BEl (∏ Γ BType
(∏ _ [#]
[Beq • (↑#) ◊ # ◊ #])) :=
fun _ => @Beq_refl.
(*Non-dependent eliminator for equality*)
Definition Beq_rec (Γ : BCtx) :
@BEl Γ (∏ Γ BType
(∏ _ [#]
(∏ (Γ · BType · (@BVar _ BType))
([↑#] → BType)
([(@BVar (Γ · BType · (@BVar _ BType))
((↑(@BVar _ BType)) → BType)) ◊ ↑#] →
(∏ (Γ · BType · (@BVar _ BType) · ([↑#] → BType))
(↑↑#)
([((Beq • (↑↑↑(@BVar _ BType))) ◊ ↑↑#) ◊ #] →
[(↑(@BVar (Γ · BType · (@BVar _ BType))
((↑(@BVar _ BType)) → BType))) ◊ #])))))):=
fun γ B x P px =>
fix g y e :=
match e as e0 in (BranchingEq _ y0) return (P y0).(fst) with
| Beq_refl _ => px
| @Bêtaeq _ _ b f x => (P b).(snd) (fun z => g b (f z)) x
end.
(*Storage operator for equality, in direct style*)
Definition Beq_stor {Γ : BCtx} :
@BEl Γ (∏ Γ BType
(∏ _ [#]
(∏ _ [↑#]
([((Beq • (↑↑(@BVar _ BType))) ◊ ↑#) ◊ #] →
(∏ _ [↑↑#]
([((Beq • (↑↑↑(@BVar _ BType))) ◊ (↑↑#)) ◊ #] →
BType)) →
BType)))) :=
fun γ B x y e P =>
match e in (BranchingEq _ b)
return ((BranchingEq x b -> BranchingTYPE) -> BranchingTYPE)
with
| Beq_refl _ => fun k : BranchingEq x x -> BranchingTYPE => k (Beq_refl x)
| @Bêtaeq _ _ _ _ _ => fun _ => Bunit
end (P y).
(*As for the axiom translation, unification problems forbid us
from writing the restricted dependent eliminator*)
(*The translation of lists*)
Inductive BranchingList {A : BranchingTYPE} : Type :=
| Bnil_aux : BranchingList
| Bcons_aux : A.(fst) -> BranchingList -> BranchingList
| Bêtalist : (Y -> BranchingList) -> X -> BranchingList.
Definition Blist {Gamma : BCtx} : @BEl Gamma (BType → BType) :=
fun _ A => {| fst := @BranchingList A ; snd := @Bêtalist A |}.
Definition Bnil {Γ : BCtx} : BEl (∏ Γ BType (Blist • #)) :=
fun _ B => @Bnil_aux B.
Definition Bcons {Γ : BCtx} :
BEl (∏ Γ BType ([#] → (Blist • #) → (Blist • #))) :=
fun gamma A x l => Bcons_aux x l.
(*Non-dependent eliminator for lists*)
Definition Blist_rec (Γ : BCtx) :
@BEl Γ (∏ Γ BType
(∏ _ BType
([#] →
([↑#] → Blist • ↑ # → [#] → [#]) →
Blist • ↑ # →
[#]))).
Proof.
unshelve refine (fun gamma B P pnil pcons => _).
refine (fix f l {struct l} := match l with
| Bnil_aux => pnil
| Bcons_aux x q => pcons x q (f q)
| Bêtalist g x => P.(snd) (fun y => f (g y)) x
end).
Defined.
(*Storage operator for lists*)
Definition Blist_stor{Γ : BCtx } :
BEl (∏ Γ BType (Blist • # → (Blist • # → BType) → BType)) :=
fun (_ : Γ) B =>
fix f (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
match l with
| Bnil_aux => fun P : @BranchingList B -> BranchingTYPE => P (Bnil_aux)
| Bcons_aux x q =>
fun P : @BranchingList B -> BranchingTYPE =>
f q (fun l' : @BranchingList B => P (Bcons_aux x l'))
| Bêtalist g x => fun P : @BranchingList B -> BranchingTYPE => Bunit
end.
(*Restricted dependent-eliminator for lists.*)
Definition Blist_rect {Γ : BCtx} :
@BEl Γ (∏ Γ BType
(∏ _ ((Blist • #) → BType)
((@BAppN _ _ BType # (Bnil • (↑#))) →
(∏ _ [↑(@BVar _ BType)]
(∏ (Γ · BType · ((Blist • #) → BType) · (↑#))
(Blist • (↑↑(@BVar _ BType)))
(([(Blist_stor • (↑↑↑(@BVar _ BType)))
◊ (@BVar _ ((Blist • (↑↑#))))
◊ (↑↑(@BVar _ ((Blist • #) → BType)))]) →
([(Blist_stor • (↑↑↑(@BVar _ BType)))
◊ ((Bcons • (↑↑↑(@BVar _ BType))) ◊ (↑#) ◊ #)
◊ (↑↑(@BVar _ ((Blist • #) → BType)))])))) →
∏ (Γ · BType · ((Blist • #) → BType)) (Blist • ↑#)
[(Blist_stor • (↑↑(@BVar _ BType))) ◊ # ◊ (↑#)]))) :=
fun _ B P pnil pcons =>
fix f l := match l as l0 return
((fix g (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
match l with
| Bnil_aux => fun P => P (Bnil_aux)
| Bcons_aux x q =>
fun P =>
g q (fun l' => P (Bcons_aux x l'))
| Bêtalist g x => fun P => Bunit
end) l0 P).(fst)
with
| Bnil_aux => pnil
| Bcons_aux x q => pcons x q (f q)
| Bêtalist _ _ => tt
end.
End BranchingTranslation.
Section Parametricity.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Variables (X Y : Type).
Definition ℙ := X -> Y.
Notation "'ACtx'" := (ACtx X Y).
Notation "'ACtx_nil'" := (@ACtx_nil X Y).
Notation "'BTy'" := (BTy X Y).
(*In this section we present the Algebraic Binary
Parametricity translation, which binds together
the two previous ones.
Again, we use a Cwf-like presentation *)
(*An algebraic binary parametric type is made of a binary predicate
Te, together with the proof that it is algebraic in respect to the
Branching translation*)
Set Printing Universes.
Definition ETy_aux (α : X -> Y) (A : Type) (B : BranchingTYPE X Y) :=
{Te : A -> fst B -> Type &
forall (a : A) (f : Y -> fst B) (x : X),
Te a (f (α x)) -> Te a (snd B f x)}.
(*Contexts are relations on contexts from the Axiom
translation and from the Branching translation.
As such, they start by α : ℙ.*)
Definition ECtx (Γa : ACtx) (Γb : BCtx) :=
forall (α : ℙ), Γa α -> Γb -> Type.
(*ETy is simply ETy_aux depending on contexts*)
Definition ETy (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(A : ATy Γa) (B : BTy Γb) :=
forall (α : ℙ) (γa : Γa α) (γb : Γb) (γe : Γe α γa γb),
ETy_aux α (A α γa) (B γb).
Definition EElt_aux {α : X -> Y} (A : Type) (B : BranchingTYPE X Y)
(R : ETy_aux α A B) (a : A) (b : B.(fst)) :=
R.(fst) a b.
(*EElt is the parametric version of Tarsky's El function*)
Definition EElt (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(ra : AEl Ra) (rb : BEl Rb) :=
forall (α : ℙ) (γa : Γa α) (γb : Γb) (γe : Γe α γa γb),
EElt_aux (Re α γa γb γe) (ra α γa) (rb γb).
(*As for the Branching translation, the translation of Type
is the constant function that always returns ETy_aux, and
we ensure algebraicity through a dummy function.*)
Definition Ue {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
ETy Γe (@AType _ _ _) (@BType _ _ _).
Proof.
unshelve refine (fun α γa γb γe => exist _).
+ refine (fun A B => @tsig (A -> B.(fst) -> Type) _).
exact (fun Te => forall (a : A) (f : Y -> B.(fst)) (x : X) (fe : Te a (f (α x))),
Te a ((B.(snd) f x))).
+ intros A f x fe.
unshelve refine (exist _).
* exact (fun _ _ => unit).
* exact (fun _ _ _ _ => tt).
Defined.
(*Empty context*)
Definition ECtx_nil : ECtx ACtx_nil (BCtx_nil) :=
fun _ _ _ => unit.
Definition Ectx_nil {α : ℙ} : @ECtx_nil α tt tt := tt.
Notation "()" := Ectx_nil.
(*Context extension*)
Definition ECtx_cons (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb) :
ECtx (ACtx_cons Ra) (BCtx_cons Rb).
Proof.
unshelve refine (fun α γa γb => _).
apply (@tsig (Γe α γa.(fst) γb.(fst))).
intro γe.
exact ((Re α _ _ γe).(fst) γa.(snd) γb.(snd)).
Defined.
Notation "Γe · Re" := (@ECtx_cons _ _ Γe _ _ Re) (at level 50, left associativity).
Definition ETy_inst (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(α : ℙ) (γa : Γa α) (γb : Γb) (γe : Γe α γa γb)
(ra : Ra α γa) (rb : (Rb γb).(fst)) :=
(Re α γa γb γe).(fst) ra rb.
Definition Ectx_cons (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(α : ℙ) (γa : Γa α) (γb : Γb) (γe : Γe α γa γb)
(ra : Ra α γa) (rb : (Rb γb).(fst)) (re : ETy_inst Re γe ra rb) :
(Γe · Re) (Actx_cons ra) (Bctx_cons rb) :=
{| fst := γe; snd := re |}.
Notation "γe ·· xe" := (@Ectx_cons _ _ _ _ _ _ _ _ _ γe _ _ xe) (at level 50, left associativity).
(*In what follows, we deal with the negative fragment
of type theory : Weakening, Pi-types, Substitution, etc*)
(*Lifting rule*)
Definition ELift (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(Sa : ATy Γa) (Sb : BTy Γb) (Se : ETy Γe Sa Sb)
: ETy (Γe · Re) (@ALift X Y _ Ra Sa) (@BLift X Y _ Rb Sb) :=
fun α γa γb γe => Se α γa.(fst) γb.(fst) γe.(fst).
Notation "⇑ A" := (@ELift _ _ _ _ _ _ _ _ A) (at level 10).
(*Weakening rule*)
Definition EWeaken (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(Sa : ATy Γa) (Sb : BTy Γb) (Se : ETy Γe Sa Sb)
(ra : AEl Ra) (rb : BEl Rb) (re : EElt Re ra rb) :
@EElt _ _ (Γe · Se) _ _ (⇑ Re) (AWeaken ra) (BWeaken rb) :=
fun α γa γb γe => re α _ _ γe.(fst).
Notation "↑ M" := (@EWeaken _ _ _ _ _ _ _ _ _ _ _ M) (at level 10).
(*Variable rule*)
Definition EVar (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb) :
@EElt _ _ (Γe · Re) _ _ (ELift Re) (@AVar X Y _ Ra) (@BVar X Y _ Rb) :=
fun α γa γb γe => γe.(snd).
Arguments EVar {Γa} {Γb} {Γe} {Ra} {Rb} _.
Notation "#" := (@EVar _ _ _ _ _ _) (at level 0).
(*Substitution*)
Definition ESub (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(Sa : ATy (ACtx_cons Ra)) (Sb : BTy (BCtx_cons Rb))
(Se : ETy (Γe · Re) Sa Sb)
(ra : AEl Ra) (rb : BEl Rb) (re : EElt Re ra rb) :
ETy Γe (ASub Sa ra) (BSub Sb rb) :=
fun α γa γb γe => Se _ _ _ (γe ·· (re α γa γb γe)).
Notation "S {{ r }} " := (@ESub _ _ _ _ _ _ _ _ S _ _ r) (at level 20, left associativity).
(*Pi-type*)
Definition EPi {Γa : ACtx} {Γb : BCtx} (Γe : ECtx Γa Γb)
{Ra : ATy Γa} {Rb : BTy Γb} (Re : ETy Γe Ra Rb)
{Sa : ATy (ACtx_cons Ra)} {Sb : BTy (BCtx_cons Rb)}
(Se : ETy (Γe · Re) Sa Sb) :
ETy Γe (APi Sa) (BPi Sb).
Proof.
unshelve refine (fun α γa γb γe => exist _).
+ exact (fun fa fb =>
forall (ra : Ra α γa) (rb : (Rb γb).(fst))
(re : ETy_inst Re γe ra rb),
(Se α _ _ (γe ·· re)).(fst) (fa ra) (fb rb)).
+ unshelve refine (fun _ _ _ fe ra rb re =>
(Se α _ _ (γe ·· re)).(snd) _ _ _ _).
exact (fe ra rb re).
Defined.
Notation "∏ A B" := (@EPi _ _ _ _ _ A _ _ B) (at level 100).
Notation "A → B" := (@EPi _ _ _ _ _ A _ _ (⇑ B))
(at level 99, right associativity, B at level 200).
(*Introduction for Pi*)
Definition ELam (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(Sa : ATy (ACtx_cons Ra)) (Sb : BTy (BCtx_cons Rb))
(Se : ETy (Γe · Re) Sa Sb)
(fa : AEl Sa) (fb : BEl Sb) (fe : EElt Se fa fb) :
EElt (EPi Se) (ALam fa) (BLam fb) :=
fun _ _ _ γe _ _ re => fe _ _ _ (γe ·· re).
Notation "'λ'" := ELam.
(*Introduction of the non-dependent arrow*)
Definition ELamN (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(Sa : ATy Γa) (Sb : BTy Γb) (Se : ETy Γe Sa Sb)
fa fb (fe : @EElt _ _ (Γe · Re) _ _ (⇑ Se) fa fb) :
EElt (Re → Se) (ALamN fa) (BLamN fb) :=
@ELam _ _ Γe _ _ Re _ _ (⇑ Se) _ _ fe.
(*Elimination for Pi*)
Definition EApp (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(Sa : ATy (ACtx_cons Ra)) (Sb : BTy (BCtx_cons Rb))
(Se : ETy (Γe · Re) Sa Sb)
(fa : AEl (APi Sa)) (fb : BEl (BPi Sb))
(fe : EElt (EPi Se) fa fb)
(ra : AEl Ra) (rb : BEl Rb) (re : EElt Re ra rb) :
EElt (Se {{re}}) (AApp fa ra) (BApp fb rb) :=
fun α γa γb γe => fe _ _ _ _ _ _ (re α γa γb γe).
Notation "t • u" := (EApp t u) (at level 12, left associativity).
(*Elimination of the non-dependent arrow*)
Definition EAppN (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : ATy Γa) (Rb : BTy Γb) (Re : ETy Γe Ra Rb)
(Sa : ATy Γa) (Sb : BTy Γb) (Se : ETy Γe Sa Sb)
fa fb (fe : EElt (Re → Se) fa fb)
ra rb (re : EElt Re ra rb) : EElt Se (AAppN fa ra) (BAppN fb rb) :=
@EApp _ _ Γe _ _ Re _ _ (⇑ Se) _ _ fe _ _ re.
Notation "t ◊ u" := (@EAppN _ _ _ _ _ _ _ _ _ _ _ t _ _ u) (at level 12, left associativity).
(*Internal Tarsky's El function*)
Definition EREL (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb)
(Ra : AEl (@AType X Y Γa)) (Rb : BEl (@BType X Y Γb))
(Re : EElt (@Ue _ _ Γe) Ra Rb) : ETy Γe Ra Rb :=
Re.
Notation "[ A ]" := (@EREL _ _ _ _ _ A).
(*The translation of booleans*)
Inductive EParabool (α : X -> Y) :
bool -> (BranchingBool X Y) -> Type :=
| EParatrue : EParabool α true (@Btrue_aux X Y)
| EParafalse : EParabool α false (@Bfalse_aux X Y)
| EParabêtabool : forall (bo : bool) (f : (Y -> BranchingBool X Y)) (x : X)
(rel : EParabool α bo (f (α x)) ),
EParabool α bo (Bêtabool f x).
Definition Ebool {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
ETy Γe (@Abool X Y Γa) (@Bbool X Y Γb) :=
(fun (α : ℙ) _ _ _ => {| fst := EParabool α; snd := @EParabêtabool α |}).
Definition Etrue {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (@Ebool _ _ Γe) (@Atrue X Y Γa) (@Btrue X Y Γb) :=
fun α _ _ _ => @EParatrue α.
Definition Efalse {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (@Ebool _ _ Γe) (@Afalse X Y Γa) (@Bfalse X Y Γb) :=
fun α _ _ _ => @EParafalse α.
(*Non-dependent eliminator for booleans*)
Definition Ebool_rec (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb) :
@EElt _ _ Γe _ _ (@EPi _ _ _ _ _ Ue _ _ ([EVar Ue] → [EVar Ue] → Ebool → [EVar Ue]))
(@Abool_rec X Y Γa) (@Bbool_rec X Y Γb).
Proof.
unshelve refine (fun α γa γb γe Pa Pb Pe pta ptb pte pfa pfb pfe => _).
exact (fix f _ _ b := match b with
| EParatrue _ => pte
| EParafalse _ => pfe
| EParabêtabool rel =>
Pe.(snd) _ _ _ (f _ _ rel)
end).
Defined.
(*Storage operator for booleans*)
Definition Ebool_stor {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
@EElt _ _ Γe _ _ (Ebool → (Ebool → Ue) → Ue) (@Abool_stor X Y Γa) (@Bbool_stor X Y Γb).
Proof.
pose (r := EApp (@Ebool_rec _ _ Γe) ((Ebool → Ue) → Ue)).
let T := constr:(@EElt _ _ Γe _ _ (((Ebool → Ue) → Ue) → ((Ebool → Ue) → Ue) → Ebool → ((Ebool → Ue) → Ue)) (AApp (@Abool_rec _ _ Γa) _) (BApp (@Bbool_rec _ _ Γb) _)) in
unshelve refine (let r : T := r in _).
unshelve refine (EAppN (EAppN r _) _).
+ refine (ELamN (@EAppN _ _ _ _ _ Ebool _ _ Ue (@AVar X Y _ _) (@BVar X Y _ _) # _ _ Etrue)).
+ refine (ELamN (@EAppN _ _ _ _ _ Ebool _ _ Ue (@AVar X Y _ _) (@BVar X Y _ _) # _ _ Efalse)).
Defined.
(*Restricted dependent eliminator for booleans*)
Definition Ebool_rect {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (EPi (Γe := Γe) (Re := (Ebool → Ue)) (
[@EApp _ _ (Γe · (Ebool → Ue)) _ _ Ebool _ _ Ue _ _ # _ _ Etrue] →
[@EApp _ _ (Γe · (Ebool → Ue)) _ _ Ebool _ _ Ue _ _ # _ _ Efalse] →
(@EPi _ _ _ _ _ Ebool _ _ [(Ebool_stor • #) • (↑#)])))
(@Abool_rect X Y Γa) (@Bbool_rect _ _ Γb) :=
fun α γa γb γe Pa Pb Pe pta ptb pte pfa pfb pfe ba bb be =>
match be as be0 in EParabool _ ba0 bb0
with
| EParatrue _ => pte
| EParafalse _ => pfe
| EParabêtabool rel => tt
end.
(*The translation of natural numbers*)
Inductive EParanat (α : X -> Y) : nat -> BranchingNat X Y -> Type :=
| EP0 : EParanat α 0 (@B0 X Y)
| EPS : forall (no : nat) (nt : BranchingNat X Y)
(ne : EParanat α no nt),
EParanat α (S no) (BS nt)
| EPbêta : forall (no : nat) (f : (Y -> BranchingNat X Y)) (x : X)
(rel : EParanat α no (f (α x)) ),
EParanat α no (Bêtanat f x).
Definition Enat {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb}:
ETy Γe (@Anat X Y Γa) (@Bnat X Y Γb).
Proof.
unshelve refine (fun α γa γb γe => exist _).
- exact (EParanat α).
- exact (@EPbêta α).
Defined.
Definition E0 {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (@Enat _ _ Γe) (@A0 X Y Γa) (@Bzero X Y Γb) :=
fun α _ _ _ => EP0 α.
Definition ES {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
@EElt _ _ Γe _ _ (Enat → Enat) (@ASucc X Y Γa) (@BSucc X Y Γb) :=
fun α _ _ _ _ _ ne => EPS ne.
(*Non-dependent eliminator for natural numbers*)
Definition Enat_rec (Γa : ACtx) (Γb : BCtx) (Γe : ECtx Γa Γb):
@EElt _ _ Γe _ _ (EPi (Re:= Ue) ([EVar Ue] → (Enat → [EVar Ue] → [EVar Ue]) → Enat → [EVar Ue]))
(@Anat_rec X Y Γa) (@Bnat_rec X Y Γb).
Proof.
cbv.
unshelve refine (fun α γa γb γe Pa Pb Pe p0a p0b p0e pSa pSb pSe => _).
refine (fix g na nb ne :=
match ne as n in EParanat _ mo mt return
fst Pe
((fix f (n : nat) : Pa :=
match n with
| 0 => p0a
| S k => pSa k (f k)
end) mo)
((fix f (n : BranchingNat X Y) : fst Pb :=
match n with
| B0 _ _ => p0b
| BS k => pSb k (f k)
| Bêtanat g x => snd Pb (fun y : Y => f (g y)) x
end) mt)
with
| EP0 _ => p0e
| @EPS _ ka kb ke => pSe _ _ ke _ _ (g ka kb ke)
| @EPbêta _ ka f x rel => Pe.(snd) _ _ _ (g ka (f (α x)) rel)
end).
Defined.
(*Storage operator for natural numbers*)
Definition Enat_stor {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb}:
@EElt _ _ Γe _ _ (Enat → (Enat → Ue) → Ue) (@Anat_stor X Y Γa) (@Bnat_stor X Y Γb).
Proof.
pose (r := EApp (@Enat_rec _ _ Γe) ((Enat → Ue) → Ue)).
let T := constr:(EElt (Γe := Γe) (((Enat → Ue) → Ue) → (Enat → ((Enat → Ue) → Ue) → ((Enat → Ue) → Ue)) → Enat → ((Enat → Ue) → Ue)) (AApp (@Anat_rec _ _ Γa) _) (BApp (@Bnat_rec _ _ Γb) _)) in
unshelve refine (let r : T := r in _).
unshelve refine (EAppN (EAppN r _) _).
- refine (ELamN (EAppN (Re := Enat) (Se := Ue) _ _)).
+ now refine #.
+ now refine E0.
- refine (@ELamN _ _ _ _ _ _ _ _ _ _ _ _).
refine (ELamN (Γe:= Γe · Enat) (Re:= (⇑((Enat → Ue) → Ue))) (Se:= (⇑ ((Enat → Ue) → Ue))) _).
refine (ELamN (Γe:= (Γe · Enat · (⇑ ((Enat → Ue) → Ue))))
(Re:= (⇑(⇑(Enat → Ue)))) (Se:= (⇑ (⇑ Ue))) _).
refine (EAppN (Re:= Enat) _ _).
+ now refine #.
+ now refine (EAppN (Re:= Enat) ES (↑↑(EVar Enat))).
Defined.
(*Restricted dependent eliminator for natural numbers*)
Definition Enat_rect {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb}:
EElt (EPi (Γe:= Γe) (Re:= Enat → Ue)
([EApp (Γe := (Γe · (Enat → Ue))) (Re:= Enat) (Se:= Ue) # E0] →
[EPi (Re:= Enat) ([EApp (Γe:= Γe · (Enat → Ue) · Enat) (Se:= Ue)
(EApp (Γe:= Γe · (Enat → Ue) · Enat) Enat_stor #) (↑#)] →
[EApp (Γe:= Γe · (Enat → Ue) · Enat) (Se:= Ue)
(EApp (Γe:= Γe · (Enat → Ue) · Enat) Enat_stor
(EApp (Γe:= Γe · (Enat → Ue) · Enat) ES #)) (↑#)])] →
EPi (Re:= Enat) [EApp (Γe:= Γe · (Enat → Ue) · Enat) (Se:= Ue)
(EApp (Γe:= Γe · (Enat → Ue) · Enat) Enat_stor #) (↑#)]))
(@Anat_rect X Y Γa) (@Bnat_rect X Y Γb).
Proof.
unshelve refine (fun α γa γb γe Pa Pb Pe p0a p0b p0e pSa pSb pSe => _).
now refine (fix g na nb ne :=
match ne as n in EParanat _ mo mt
with
| EP0 _ => p0e
| @EPS _ ka kb ke => pSe _ _ ke _ _ (g ka kb ke)
| @EPbêta _ ka f x rel => tt
end).
Defined.
(*The two following propositions are Propositions 19 and 20 in our paper *)
Proposition Specification_unicity {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
forall (na : AEl (@Anat X Y Γa)) (nb : BEl (@Bnat X Y Γb)) (α : X -> Y)
(γa : Γa α) (γb : Γb) (γe : Γe α γa γb),
EParanat α (na α γa) (nb γb) -> na α γa = BNdialogue (nb γb) α.
Proof.
intros na nb α γa γb γe ne.
induction ne ; trivial ; now apply eq_S.
Defined.
Proposition Generic_Parametricity :
forall (α : X -> Y) (nb : BranchingNat X Y),
EParanat α (BNdialogue nb α) nb.
Proof.
now refine (fix g α nb :=
match nb as n return
EParanat _ (BNdialogue n α) n
with
| B0 _ _ => EP0 α
| BS kb => EPS (g α kb)
| Bêtanat f x => EPbêta (g α (f (α x)))
end).
Defined.
(*The translation of equality*)
Inductive EParaeq {α : X -> Y} (A : Type) (B : BranchingTYPE X Y) (E : ETy_aux α A B)
(ta : A) (tb : B.(fst)) (te : EElt_aux E ta tb) :
forall (ua : A) (ub : B.(fst)) (ue : EElt_aux E ua ub),
(Eq ta ua) -> (BranchingEq tb ub) -> Type :=
| EParaeq_refl : EParaeq te te (Eq_refl ta) (Beq_refl tb)
| EParabêtaeq : forall (ua : A) (ub : B.(fst)) (ue : EElt_aux E ua ub)
(e : Eq ta ua)
(f : Y -> BranchingEq tb ub) (x : X)
(rel : EParaeq te ue e (f (α x))),
EParaeq te ue e (Bêtaeq f x).
Definition Eeq {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe := Γe) (EPi (Γe := Γe) (Re:= Ue) ((EVar Ue) → (EVar Ue) → Ue))
(@Aeq X Y Γa) (@Beq X Y Γb).
Proof.
unshelve refine (fun α γa γb γe Ra Rb Re ta tb te ua ub ue => exist _).
- exact (EParaeq te ue).
- exact (EParabêtaeq (te:= te) (ue:= ue)).
Defined.
Definition Eeq_refl {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (EPi (Γe := Γe) (Re:= Ue)
(EPi (Γe := Γe · Ue) (Re:= [EVar Ue])
[(EApp (Γe := Γe · Ue · [EVar Ue])
(Re := Ue)
(Se:= (EVar Ue) → (EVar Ue) → Ue) Eeq (↑#)) ◊ # ◊ #]))
(@Arefl _ _ Γa) (@Brefl _ _ Γb) :=
fun α γa γb γe Ra Rb Re ra rb re => EParaeq_refl re.
(*Non-dependent eliminator for equality*)
Definition Eeq_rec {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe:= Γe) (EPi (Γe:= Γe) (Re:= Ue)
(EPi (Re:= [EVar Ue])
(EPi (Γe:= Γe · Ue · (EVar Ue))
(Re:= [↑(EVar Ue)] → Ue)
([(EVar (Γe:= Γe · Ue · (EVar Ue))
([↑(EVar Ue)] → Ue)) ◊ ↑#] →
(EPi (Γe:= Γe · Ue · (EVar Ue) · ([↑(EVar Ue)] → Ue))
(Re:= [↑↑#])
([((Eeq • (↑↑↑(EVar Ue))) ◊ ↑↑#) ◊ #] →
[(↑(EVar (Γe:= Γe · Ue · (EVar Ue))
((↑(EVar Ue)) → Ue))) ◊ #]))))))
(@Aeq_rec _ _ Γa) (@Beq_rec _ _ Γb) :=
fun α γa γb γe Ra Rb Re xa xb xe Pa Pb Pe pa pb pe =>
fix g ya yb ye eqa eqb eqe :=
match eqe in (@EParaeq _ _ _ _ _ _ _ ya0 yb0 ye0 eqa0 eqb0)
return (Pe ya0 yb0 ye0).(fst)
(match eqa0 in (Eq _ ya0)
return (Pa ya0)
with
| Eq_refl _ => pa
end)
((fix g y e :=
match e in (BranchingEq _ yb0)
return (fst (Pb yb0))
with
| Beq_refl _ => pb
| @Bêtaeq _ _ _ _ b f x => snd (Pb b) (fun z : Y => g b (f z)) x
end) yb0 eqb0)
with
| EParaeq_refl _ => pe
| @EParabêtaeq _ _ _ _ _ _ _ za zb ze eqza f x rel =>
(Pe za zb ze).(snd) _ _ x (g za zb ze eqza (f (α x)) rel)
end.
(*Storage operator for equality, in direct style*)
Definition Eeq_stor {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe:= Γe)
(EPi (Γe:= Γe) (Re:= Ue)
(EPi (Re:= [EVar Ue])
(EPi (Re:= [↑(EVar Ue)])
([((Eeq • (↑↑(EVar Ue))) ◊ ↑#) ◊ #] →
(EPi (Γe:= Γe · Ue · [EVar Ue] · [↑(EVar Ue)])
(Re:= [↑↑(EVar Ue)])
([((Eeq • (↑↑↑(EVar Ue))) ◊ (↑↑#)) ◊ #] →
Ue)) →
Ue))))
(@Aeq_stor _ _ Γa) (@Beq_stor _ _ Γb).
Proof.
cbv.
refine (fun α γa γb γe Ra Rb Re xa xb xe ya yb ye eqa eqb eqe =>
match eqe in (@EParaeq _ _ _ _ _ _ _ ya0 yb0 ye0 eqa0 eqb0)
with
| EParaeq_refl _ =>
fun Pa Pb Pe => Pe xa xb xe (Eq_refl xa) (Beq_refl xb) (EParaeq_refl xe)
| @EParabêtaeq _ _ _ _ _ _ _ za zb ze eqza f x rel =>
fun Pa Pb Pe => {|fst := fun _ _ => unit ;
snd := fun _ _ _ _ => tt |}
end).
Defined.
(*As for the two previous translations, unification problems forbid us
from writing Eeq_rect*)
(*The translation of lists*)
Arguments nil {A}.
Notation "x :: l" := (cons x l).
Inductive EParalist {α : X -> Y} (A : Type) (B : BranchingTYPE X Y) (E : ETy_aux α A B)
: list A -> (@BranchingList X Y B) -> Type :=
| EParanil : EParalist E nil (@Bnil_aux X Y _)
| EParacons : forall (la : list A) (lb : @BranchingList X Y B)
(le : EParalist E la lb)
(a : A) (b : B.(fst))
(e : EElt_aux E a b),
EParalist E (a :: la) (Bcons_aux b lb)
| EParabêtalist : forall (la : list A)
(f : Y -> (@BranchingList X Y B))
(x : X)
(rel : EParalist E la (f (α x))),
EParalist E la (Bêtalist f x).
Definition Elist {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe := Γe) (Ue → Ue) (@Alist _ _ Γa) (@Blist _ _ Γb).
Proof.
unshelve refine (fun alpha γa γb γe Ra Rb Re => exist _).
+ exact (EParalist Re).
+ exact (EParabêtalist (E := Re)).
Defined.
Definition Enil {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe := Γe) (EPi (Re := Ue) (Elist • (EVar Ue))) (@Anil _ _ _) (@Bnil _ _ _) :=
fun α γa γb γe Ra Rb Re => EParanil _.
Definition Econs {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe := Γe) (EPi (Re := Ue) ((EVar Ue) → [EApp Elist (EVar Ue)] → [EApp Elist (EVar Ue)]))
(@Acons _ _ _) (@Bcons _ _ _) :=
fun α γa γb γe Ra Rb Re ra rb re la lb le => EParacons le re.
(*Non-dependent eliminator for lists*)
Definition Elist_rec {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb}:
EElt (Γe := Γe) (EPi (Re := Ue)
(EPi (Re := Ue)
([EVar Ue] →
([↑(EVar Ue)] → Elist • ↑ (EVar Ue) → [EVar Ue] → [EVar Ue]) →
Elist • ↑ (EVar Ue) →
[EVar Ue]))) (@Alist_rec _ _ _) (@Blist_rec _ _ _)
:=
fun α γa γb γe Ra Rb Re Pa Pb Pe pnila pnilb pnile pconsa pconsb pconse =>
fix f la lb le {struct le} :=
match le as le0 in EParalist _ la0 lb0
return
fst Pe
((fix f (l : list Ra) : Pa :=
match l with
| nil => pnila
| (x :: q) => pconsa x q (f q)
end) la0)
((fix f (l : BranchingList (Y:=Y)) : fst Pb :=
match l with
| @Bnil_aux _ _ => pnilb
| Bcons_aux x q => pconsb x q (f q)
| Bêtalist g x => snd Pb (fun y : Y => f (g y)) x
end) lb0)
with
| @EParanil _ _ _ _ => pnile
| @EParacons _ _ _ _ qa qb qe ra rb re =>
pconse ra rb re qa qb qe _ _ ((f qa qb qe))
| @EParabêtalist _ _ _ _ qa g x rel => Pe.(snd) _ _ _ (f qa (g (α x)) rel)
end.
(*Storage operator for lists, in direct style*)
Definition Elist_stor {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe := Γe) (EPi (Re := Ue) (Elist • (EVar Ue) → (Elist • (EVar Ue) → Ue) → Ue))
(@Alist_stor _ _ _) (@Blist_stor _ _ _).
Proof.
unshelve refine (fun α γa γb γe Ra Rb Re => _).
unshelve refine (fix f la lb le :=
match le as le0 in EParalist _ la0 lb0
with
| EParanil _ => fun _ _ Pe => (Pe nil (@Bnil_aux X Y _) (EParanil _))
| @EParacons _ _ _ _ qa qb qe ra rb re =>
fun Pa Pb Pe => f qa qb qe _ _ (fun la lb le => Pe _ _ (EParacons le re))
| @EParabêtalist _ _ _ _ qa g x rel =>
fun Pa Pb Pe => ((ELift Ue _ ).(snd) _ _ x _)
end).
- exact (fun y => @Blist_stor X Y _ _ _ (g y) Pb).
- exact (f _ _ rel Pa Pb Pe).
Defined.
(*Restricted dependent eliminator for lists*)
Definition Elist_rect {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe:= Γe) (EPi (Re:= Ue)
(EPi (Re:= (Elist • (EVar Ue)) → Ue)
((EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue))
(Re:= ⇑(Elist • ((EVar Ue)))) (Se:= Ue) # (Enil • (↑(EVar Ue)))) →
(EPi (Re:= [↑(EVar Ue)])
(EPi (Re:= Elist • (↑↑(EVar Ue)))
(([(EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue) · (↑#) · (Elist • (↑↑(EVar Ue))))
(Re:= (Elist • (↑ ↑ ↑(EVar Ue))))
(Se:= ((Elist • (↑ ↑ ↑(EVar Ue))) → Ue) → Ue)
(Elist_stor • (↑↑↑(EVar Ue)))
(EVar ((Elist • (↑↑(EVar Ue))))))
◊ (↑↑(EVar ((Elist • (EVar Ue)) → Ue)))]) →
([(EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue) · (↑#) · (Elist • (↑↑(EVar Ue))))
(Re:= (Elist • (↑ ↑ ↑(EVar Ue))))
(Se:= ((Elist • (↑ ↑ ↑(EVar Ue))) → Ue) → Ue)
(Elist_stor • (↑↑↑(EVar Ue)))
((EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue) · (↑#) · (Elist • (↑↑(EVar Ue))))
(Re:= ↑ ↑ ↑(EVar Ue))
(Se:= (Elist • (↑ ↑ ↑ (EVar Ue))) → (Elist • (↑ ↑ ↑ (EVar Ue))))
(Econs • (↑↑↑(EVar Ue))) (↑#)) ◊ #))
◊ (↑↑(EVar ((Elist • (EVar Ue)) → Ue)))])))) →
EPi (Re:= Elist • ↑(EVar Ue))
[(EAppN (Γe:= Γe · Ue · ((Elist • (EVar Ue)) → Ue) · (Elist • ↑(EVar Ue)))
(Re:= (Elist • (↑ ↑ (EVar Ue))))
(Se:= ((Elist • (↑ ↑(EVar Ue))) → Ue) → Ue)
(Elist_stor • (↑↑(EVar Ue))) #) ◊ (↑#)])))
(@Alist_rect X Y Γa) (@Blist_rect X Y Γb).
Proof.
vm_compute.intros α γa γb γe Ra Rb Re.
(*Restricted dependent-eliminator for lists.*)
Definition Elist_rect {Γa : ACtx} {Γb : BCtx} {Γe : ECtx Γa Γb} :
EElt (Γe := Γe) (EPi (Re := Ue)
(EPi (Re := ((Elist • #) → Ue))
((EAppN (Se := Ue) # (Enil • (↑#))) →
(EPi (Re := [↑(EVar Ue)])
(EPi (Γe := (Γe · Ue · ((Elist • #) → Ue) · (↑#)))
(Re := (Elist • (↑↑(EVar Ue))))
(([(EAppN
(@EApp _ _ _ _ _ Ue _ _
(Elist • (EVar Ue) → (Elist • (EVar Ue) → Ue) → Ue)
(@Alist_stor X Y _) (@Blist_stor _ _ _)
Elist_stor _ _ (↑↑↑(EVar Ue)))
(EVar ((Elist • (↑↑(EVar Ue))))))
◊ (↑↑(EVar ((Elist • #) → Ue)))]) →
([(Elist_stor • (↑↑↑(EVar Ue)))
◊ ((Econs • (↑↑↑(EVar Ue))) ◊ (↑#) ◊ #)
◊ (↑↑(@EVar _ ((Elist • #) → Ue)))])))) →
EPi (Γe := Γe · Ue · ((Elist • #) → Ue)) (Re := (Elist • ↑#))
[(Elist_stor • (↑↑(EVar Ue))) ◊ # ◊ (↑#)])))
(@Alist_rect X Y Γa) (@Blist_rect X Y Γb).
Proof.
unshelve refine (fun gamma B P pnil pcons => _).
refine (fix f l := match l as l0 return
((fix g (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
match l with
| Bnil_aux => fun P => P (Bnil_aux)
| Bcons_aux x q =>
fun P =>
g q (fun l' => P (Bcons_aux x l'))
| Bêtalist g x => fun P => Bunit
end) l0 P).(fst)
with
| Bnil_aux => pnil
| Bcons_aux x q => pcons x q (f q)
| Bêtalist _ _ => tt
end).*)
End Parametricity.
Section AvareXY.
Unset Implicit Arguments.
Variables X Y : Type.
Notation "'ℙ'" := (X -> Y).
Notation "'ACtx'" := (ACtx X Y).
Notation "'BTy'" := (BTy X Y).
Definition Ctx :=
triple (fun (A : ACtx) (B : BCtx) =>
forall (α : ℙ), A α -> B -> Type).
Definition Ctx_El (Γ : Ctx) (α : ℙ) :=
triple (fun (a : Γ.(q1) α) (b : Γ.(q2)) =>
Γ.(q3) α a b).
Notation " Γ ‡ α " := (Ctx_El Γ α) (at level 11).
Definition Ty (Γ : Ctx) : Type :=
triple (fun (A : ATy Γ.(q1)) (B : BTy Γ.(q2)) =>
forall (α : ℙ) (γ : Ctx_El Γ α),
tsig (fun (Te : A α (γ.(q1)) -> (B γ.(q2)).(fst) -> Type) =>
forall (a : A α (γ.(q1)))
(f : Y -> (B γ.(q2)).(fst))
(x : X) (fe : Te a (f (α x))), Te a ((B γ.(q2)).(snd) f x))).
Definition RElt (Γ : Ctx) (R : Ty Γ) : Type :=
triple (fun (a : AEl R.(q1)) (b : BEl R.(q2)) =>
forall (α : ℙ) (γ : Ctx_El Γ α),
(R.(q3) α γ).(fst) (a α γ.(q1)) (b γ.(q2))).
Definition Ty_inst {Γ : Ctx} {α : ℙ} (R : Ty Γ) (γ : Ctx_El Γ α) : Type
:=
triple (fun (a : R.(q1) α γ.(q1)) (b : (R.(q2) γ.(q2)).(fst)) =>
(R.(q3) α γ).(fst) a b).
Definition Inst {Γ : Ctx} {R : Ty Γ} {α : ℙ} (r : RElt _ R)
(γ : Ctx_El Γ α) : Ty_inst R γ.
Proof.
exists (r.(q1) α γ.(q1)) (r.(q2) γ.(q2)).
exact (r.(q3) α γ).
Defined.
Notation "r ® γ" := (Inst r γ) (at level 10, left associativity).
Definition Ctx_nil : Ctx.
Proof.
exists (@ACtx_nil X Y) (BCtx_nil).
apply (fun _ _ _ => unit).
Defined.
Definition ctx_nil {α : ℙ} : Ctx_nil ‡ α.
Proof.
exists tt tt.
exact: tt.
Defined.
Notation "()" := ctx_nil.
Definition Ctx_cons (Γ : Ctx) (R : Ty Γ) : Ctx.
Proof.
exists (ACtx_cons R.(q1)) (BCtx_cons R.(q2)).
intros α Acons Bcons.
apply (@tsig (Γ.(q3) α Acons.(fst) Bcons.(fst))).
intro γe.
exact ((R.(q3) α (exist3 γe)).(fst) Acons.(snd) Bcons.(snd)).
Defined.
Notation "Γ · A" := (Ctx_cons Γ A) (at level 50, left associativity).
Definition ctx_cons {Γ : Ctx} {R : Ty Γ} {α : ℙ}
(γ : Γ ‡ α) (x : Ty_inst R γ) :
(Γ · R) ‡ α.
Proof.
destruct x as [xa xb xe].
exists (Actx_cons xa) (Bctx_cons xb).
exists γ.(q3).
exact xe.
Defined.
Notation "γ ·· x" := (ctx_cons γ x) (at level 50, left associativity).
Definition Ctx_tl {Γ : Ctx} {R : Ty Γ} {α : ℙ}
(γ : Ctx_El (Γ · R) α) : Ctx_El Γ α.
Proof.
exists γ.(q1).(fst) γ.(q2).(fst).
exact (γ.(q3).(fst)).
Defined.
Notation "¿ g" := (Ctx_tl g) (at level 10).
Definition Lift {Γ : Ctx} {R1 : Ty Γ} (R2 : Ty Γ) : Ty (Γ · R1).
Proof.
unshelve refine (exist3 _).
+ refine (fun α γr => R2.(q1) α γr.(fst)).
+ refine (fun γd => R2.(q2) γd.(fst)).
+ unshelve refine (fun α γ => _).
exact (R2.(q3) α (¿ γ)).
Defined.
Notation "⇑ A" := (Lift A) (at level 10).
Definition Var {Γ : Ctx} (R : Ty Γ) : RElt (Γ · R) (⇑ R).
Proof.
unshelve refine (exist3 _).
+ refine (fun α γr => γr.(snd)).
+ refine (fun γd => γd.(snd)).
+ exact (fun α γ => γ.(q3).(snd)).
Defined.
Notation "#" := (Var _) (at level 0).
Definition Weaken {Γ : Ctx} {R S : Ty Γ} (r : RElt Γ R) :
RElt (Γ · S) (⇑ R).
Proof.
unshelve refine (exist3 _).
+ refine (fun α γr => r.(q1) α γr.(fst)).
+ refine (fun γd => r.(q2) γd.(fst)).
+ exact (fun α γ => r.(q3) α (¿ γ)).
Defined.
Notation "↑ M" := (Weaken M) (at level 10).
Definition Sub {Γ : Ctx} {R : Ty Γ} (S : Ty (Γ · R)) (r : RElt Γ R) :
Ty Γ.
Proof.
unshelve refine (exist3 _).
+ refine (fun α γr => S.(q1) α (@exist _ _ γr (r.(q1) α γr))).
+ refine (fun γd => S.(q2) (@exist _ _ γd (r.(q2) γd))).
+ exact (fun α γ =>
S.(q3) α (γ ·· (r ® γ))).
Defined.
Notation "S {{ r }} " := (Sub S r) (at level 20, left associativity).
Definition RPi {Γ : Ctx} (A : Ty Γ) (B : Ty (Γ · A)) : Ty Γ.
Proof.
unshelve refine (exist3 _).
- refine (fun α γr => forall (x : A.(q1) α γr), B.(q1) α (@exist _ _ γr x)).
- intro γd.
unshelve refine (exist _) ; simpl.
+ refine (forall (x : (A.(q2) γd).(fst)), (B.(q2) (@exist _ _ γd x)).(fst)).
+ refine (fun f x a => (B.(q2) (@exist _ _ γd a)).(snd) (fun y => f y a) x).
- simpl ; unshelve refine (fun α γ => _).
unshelve refine (exist _).
have aux :
+ exact (fun fr fd => forall a : Ty_inst A γ,
(B.(q3) α (γ ·· a)).(fst)
(fr a.(q1))
(fd a.(q2))).
(* + exact (fun fr fd => forall a : RElt Γ A,
(B.(q3) α (γ ·· (a ® γ))).(fst)
(fr (a ® γ).(q1))
(fd (a ® γ).(q2))).*)
+ unshelve refine (fun _ _ _ fe a => (B.(q3) α (γ ·· a)).(snd) _ _ _ _).
exact (fe a).
Defined.
Notation "∏" := (RPi).
Notation "A → B" := (RPi A (⇑ B)) (at level 99, right associativity, B at level 200).
Definition RLam {Γ : Ctx} {A : Ty Γ} (B : Ty (Γ · A)) (f : RElt (Γ · A) B)
: RElt Γ (RPi A B).
Proof.
unshelve refine (exist3 _).
+ refine (fun α γr xr => f.(q1) α (@exist _ _ γr xr)).
+ refine (fun γd xd => f.(q2) (@exist _ _ γd xd)).
+ exact (fun α γ x => f.(q3) α (γ ·· x)).
Defined.
Notation "'λ'" := RLam.
Definition RLamN {Γ : Ctx} {A : Ty Γ} {B : Ty Γ} (f : RElt (Γ · A) (⇑ B)) : RElt Γ (A → B) :=
@RLam Γ A (⇑ B) f.
Definition RApp {Γ : Ctx} {A : Ty Γ} {B : Ty (Γ · A)}
(f : RElt Γ (RPi A B)) (x : RElt Γ A) : RElt Γ (B {{ x }}).
Proof.
unshelve refine (exist3 _).
+ refine (fun α γr => f.(q1) α γr (x.(q1) α γr)).
+ refine (fun γd => f.(q2) γd (x.(q2) γd)).
+ exact (fun α γ =>
f.(q3) α γ (x ® γ)).
Defined.
Notation "t • u" := (RApp t u) (at level 12, left associativity).
Definition RAppN {Γ : Ctx} {A : Ty Γ} {B : Ty Γ} (f : RElt Γ (A → B))(x : RElt Γ A) : RElt Γ B :=
@RApp Γ A (⇑ B) f x.
Notation "t ◊ u" := (@RAppN _ _ _ t u) (at level 12, left associativity).
Definition U {Γ : Ctx} : Ty Γ.
Proof.
unshelve refine (exist3 _).
- refine (fun α γr => Type).
- unshelve refine (fun γd => exist _).
+ refine (BranchingTYPE X Y).
+ refine (fun _ _ => Bunit X Y).
- unshelve refine (fun (α : ℙ) (γ : Γ ‡ α) => exist _).
+ unshelve refine (fun A B => @tsig (A -> B.(fst) -> Type) _).
* exact (fun Te => forall (a : A) (f : Y -> B.(fst)) (x : X) (fe : Te a (f (α x))),
Te a ((B.(snd) f x))).
+ intros A f x fe.
unshelve refine (exist _).
* exact (fun _ _ => unit).
* simpl.
exact (fun _ _ _ _ => tt).
Defined.
Definition REL {Γ : Ctx} (A : RElt Γ U) : Ty Γ.
Proof.
exists (fun p γ => A.(q1) p γ) (fun γ => A.(q2) γ).
unshelve refine (fun (α : ℙ) (γ : Γ ‡ α) => exist _).
- exact (A.(q3) α γ).(fst).
- exact (A.(q3) α γ).(snd).
Defined.
Notation "[ A ]" := (REL A).
Definition RElt_inst {Γ : Ctx} {α : ℙ} {γ : Γ ‡ α}
(R : Ty_inst U γ) : Type :=
triple (fun (a : R.(q1)) (b : R.(q2).(fst)) =>
R.(q3).(fst) a b).
Definition RProp {Γ : Ctx} : Ty Γ.
Proof.
unshelve refine (exist3 _).
- refine (fun α γr => Prop).
- intro γd.
unshelve refine (exist _).
+ refine ({P : Prop & (Y -> P) -> X -> P}).
+ refine (fun _ _ => _).
refine (@exist _ _ True _).
refine (fun _ _ => I).
- unshelve refine (fun (α : ℙ) (γ : Γ ‡ α) => exist _).
+ exact (fun A B => tsig (fun (Te : A -> B.(fst) -> Type) =>
forall (a : A) (f : Y -> B.(fst) ) (x : X) (fe : Te a (f (α x))),
Te a ((B.(snd) f x)))).
+ simpl ; intros.
unshelve refine (exist _).
* exact (fun _ _ => True).
* simpl.
exact (fun _ _ _ _ => I).
Defined.
Definition REL_Prop {Γ : Ctx} (A : RElt Γ RProp) : Ty Γ.
Proof.
unshelve refine (exist3 _).
- unshelve refine (fun α γ => _).
exact (A.(q1) α γ).
- refine (fun γ => _).
refine (exist _).
apply (A.(q2) γ).(snd).
- unshelve refine (fun (α : ℙ) (γ : Γ ‡ α) => exist _).
+ exact (A.(q3) α γ).(fst).
+ exact (A.(q3) α γ).(snd).
Defined.
Inductive RParabool (α : X -> Y) :
bool -> (BranchingBool X Y) -> Type :=
| RParatrue : RParabool α true (@Btrue_aux X Y)
| RParafalse : RParabool α false (@Bfalse_aux X Y)
| RParabêtabool : forall (bo : bool) (f : (Y -> BranchingBool X Y)) (x : X)
(rel : RParabool α bo (f (α x)) ),
RParabool α bo (Bêtabool f x).
Definition Rbool {Γ : Ctx} : Ty Γ.
Proof.
exists (@Abool X Y Γ.(q1)) (@Bbool X Y Γ.(q2)).
exact (fun (α : ℙ) (γ : Γ ‡ α) => {| fst := RParabool α; snd := RParabêtabool α |}).
Defined.
Definition Rtrue {Γ : Ctx} : RElt Γ Rbool.
Proof.
exists (@Atrue X Y Γ.(q1)) (@Btrue X Y Γ.(q2)).
exact (fun α _ => RParatrue α).
Defined.
Definition Rfalse {Γ : Ctx} : RElt Γ Rbool.
Proof.
exists (@Afalse X Y Γ.(q1)) (@Bfalse X Y Γ.(q2)).
exact (fun α _ => RParafalse α).
Defined.
Definition Rbool_rec (Γ : Ctx) :
RElt Γ (∏ U ([Var U] → [Var U] → Rbool → [Var U])).
Proof.
exists (@Abool_rec X Y Γ.(q1)) (@Bbool_rec X Y Γ.(q2)).
simpl ; intros α g P ptrue pfalse b.
destruct b as [bo bb be].
revert be ; revert bb ; revert bo ; simpl.
unshelve refine (fix f _ _ b := match b with
| RParatrue _ => _
| RParafalse _ => _
| RParabêtabool _ _ _ _ rel =>
P.(q3).(snd) _ _ _ (f _ _ rel)
end).
- exact ptrue.(q3).
- exact pfalse.(q3).
Defined.
Definition Rbool_stor {Γ : Ctx} :
RElt Γ (Rbool → (Rbool → U) → U).
Proof.
pose (r := RApp (Rbool_rec Γ) ((Rbool → U) → U)).
let T := constr:(RElt Γ (((Rbool → U) → U) → ((Rbool → U) → U) → Rbool → ((Rbool → U) → U))) in
unshelve refine (let r : T := r in _).
unshelve refine (RAppN (RAppN r _) _).
+ refine (RLamN (@RAppN _ Rbool _ _ _)).
- refine #.
- refine Rtrue.
+ refine (RLamN (@RAppN _ Rbool _ _ _)).
- refine #.
- refine Rfalse.
Defined.
Definition Rbool_rect {Γ : Ctx} :
RElt Γ (∏ (Rbool → U) (
[@RApp (Γ · (Rbool → U)) Rbool U (Var (Rbool → U)) Rtrue] →
[@RApp (Γ · (Rbool → U)) Rbool U # Rfalse] →
∏ Rbool [@RApp _ _ U
(@RApp (Γ · (Rbool → U) · Rbool) _ _ Rbool_stor #) (↑#)])).
Proof.
unshelve refine (exist3 _).
- refine (fun α γ P ptrue pfalse b =>
match b with
| true => ptrue
| false => pfalse
end).
- unshelve refine (fun g P ptrue pfalse bb =>
match bb with
| Btrue_aux _ _ => ptrue
| Bfalse_aux _ _ => pfalse
| Bêtabool _ _ => tt
end).
- intros α γ P ptrue pfalse b.
destruct b as [bo bb be].
revert be ; revert bb ; revert bo.
unshelve refine (fun _ _ b => match b with
| RParatrue _ => _
| RParafalse _ => _
| RParabêtabool _ _ _ _ _ => tt
end).
+ now apply ptrue.
+ now apply pfalse.
Defined.
Inductive RParanat (α : X -> Y) : nat -> BranchingNat X Y -> Type :=
| RP0 : RParanat α 0 (B0 X Y)
| RPS : forall (no : nat) (nt : BranchingNat X Y)
(ne : RParanat α no nt),
RParanat α (S no) (BS nt)
| RPbêta : forall (no : nat) (f : (Y -> BranchingNat X Y)) (x : X)
(rel : RParanat α no (f (α x)) ),
RParanat α no (Bêtanat f x).
Definition Rnat {Γ : Ctx} : Ty Γ.
Proof.
unshelve refine (exist3 _).
- refine (fun (α : X -> Y) (γ : Γ.(q1) α) => nat ).
- refine (Bnat X Y).
- exact (fun α γ => exist (RPbêta α)).
Defined.
Definition R0 {Γ : Ctx} : RElt Γ Rnat.
Proof.
exists (fun _ _ => 0) (fun _ => B0 X Y).
now refine (fun α _ => RP0 α).
Defined.
Definition RS {Γ : Ctx} : RElt Γ (Rnat → Rnat).
Proof.
exists (fun _ _ => S) (fun _ => @BS X Y).
now refine (fun α _ n => RPS α n.(q1) n.(q2) n.(q3)).
Defined.
Lemma RParanat_equal {Γ : Ctx} (n : RElt Γ Rnat)
(α : X -> Y) (γ : Γ ‡ α) :
BNdialogue (n ® γ).(q2) α = (n ® γ).(q1).
Proof.
destruct n as [nt no ne] ; simpl.
elim: (ne α γ) =>
[ | β mt mo me | β f x mo rel] ; trivial ; simpl.
exact: eq_S.
Qed.
Definition Rnat_rec (Γ : Ctx) :
RElt Γ (∏ U ([Var U] → (Rnat → [Var U] → [Var U]) → Rnat → [Var U])).
Proof.
unshelve refine (exist3 _).
- simpl ; unshelve refine (fun α gamma P p0 pS => _).
refine (fix f n := match n with
| 0 => p0
| S k => pS k (f k)
end).
- simpl ; unshelve refine (fun gamma P p0 pS => _).
refine (fix f n := match n with
| B0 _ _ => p0
| BS k => pS k (f k)
| Bêtanat g x => P.(snd) (fun y => f (g y)) x
end).
- simpl.
unshelve refine (fun α gamma P p0 pS n => _).
cbv in P.
unshelve refine (let fix g no nt ne :=
match ne as n in RParanat _ mo mt return
fst (q3 P)
((fix f (n : nat) : q1 P :=
match n with
| 0 => q1 p0
| S k => q1 pS k (f k)
end) mo)
((fix f n : (q2 P).(fst) :=
match n with
| B0 _ _ => q2 p0
| BS k => q2 pS k (f k)
| Bêtanat g x => ((P.(q2)).(snd) (fun y => f (g y)) x)
end) mt)
with
| RP0 _ => p0.(q3)
| RPS _ ko kt ke => pS.(q3) (exist3 ke) (exist3 (g ko kt ke))
| RPbêta _ ko f x rel => P.(q3).(snd) _ _ _ (g ko (f (α x)) rel)
end
in g n.(q1) n.(q2) n.(q3)).
Defined.
Definition Rnat_stor {Γ : Ctx} :
RElt Γ (Rnat → (Rnat → U) → U).
Proof.
pose (r := RApp (Rnat_rec Γ) ((Rnat → U) → U)).
let T := constr:(RElt Γ (((Rnat → U) → U) → (Rnat → ((Rnat → U) → U) → ((Rnat → U) → U)) → Rnat → ((Rnat → U) → U))) in
unshelve refine (let r : T := r in _).
unshelve refine (RAppN (RAppN r _) _).
- refine (RLamN (@RAppN _ Rnat _ _ _)).
+ now refine #.
+ now refine R0.
- refine (@RLamN _ _ _ _).
refine (@RLamN (@Ctx_cons Γ Rnat) (⇑ ((Rnat → U) → U)) (⇑ ((Rnat → U) → U)) _).
refine (@RLamN (Γ · Rnat · (⇑ ((Rnat → U) → U)))
(⇑(⇑(Rnat → U))) (⇑ (⇑ U)) _).
refine (@RAppN _ (Rnat → U) _ _ _).
+ now refine (↑#).
+ apply RLamN.
refine (@RAppN _ Rnat _ _ _).
* now refine (↑#).
* now refine (@RAppN _ Rnat _ RS (↑↑↑(Var Rnat))).
Defined.
Definition Rnat_rect {Γ : Ctx} :
RElt Γ (∏ (Rnat → U) (
[@RApp (Γ · (Rnat → U)) Rnat U # R0] →
[∏ Rnat ([@RApp (Γ · (Rnat → U) · Rnat) _ U
(@RApp (Γ · (Rnat → U) · Rnat) _ _ Rnat_stor #) (↑#)] →
[@RApp (Γ · (Rnat → U) · Rnat) _ U
(@RApp (Γ · (Rnat → U) · Rnat) _ _ Rnat_stor
(@RApp (Γ · (Rnat → U) · Rnat) _ _ RS #)) (↑#)])] →
∏ Rnat [@RApp (Γ · (Rnat → U) · Rnat) _ U
(@RApp (Γ · (Rnat → U) · Rnat) _ _ Rnat_stor #) (↑#)])).
Proof.
unshelve refine (exist3 _).
- cbv.
unshelve refine (fun α γ P p0 pS => _).
refine (fix g n := match n with
| 0 => p0
| S k => pS k (g k)
end).
- cbv.
unshelve refine (fun γ P p0 pS => _).
simpl.
refine (fix g n :=
match n with
| B0 _ _ => p0
| BS k => pS k (g k)
| Bêtanat _ _ => tt
end).
- unshelve refine (fun α gamma P p0 pS n => _).
destruct n as [ho ht he].
revert he ; revert ho ; revert ht.
cbv in pS.
refine (fix g ht ho he :=
match he with
| RP0 _ => _
| RPS _ no nt ne => pS.(q3) (exist3 ne) (exist3 (g nt no ne))
| RPbêta _ _ _ _ _ => tt
end).
exact p0.(q3).
Defined.
Definition RApp_inst {Γ : Ctx} {α : ℙ} {γ : Γ ‡ α} {A : Ty Γ}
{B : Ty (Γ · A)} (f : Ty_inst (RPi A B) γ) (x : Ty_inst A γ) :
Ty_inst B (γ ·· x).
Proof.
unshelve refine (exist3 _).
- exact (f.(q1) x.(q1)).
- exact (f.(q2) x.(q2)).
- exact (f.(q3) x).
Defined.
Inductive Bsig (A : BranchingTYPE X Y)
(B : A.(fst) -> BranchingTYPE X Y) : Type :=
| Bex : forall (a : A.(fst)) (b : (B a).(fst)), Bsig A B
| Bêtasig : (Y -> Bsig A B) -> X -> Bsig A B.
Inductive RParasig {Γ : Ctx} {α : X -> Y} {γ : Γ ‡ α}
(A : Ty_inst U γ) (B : Ty_inst ((Var U) → U) (γ ·· A))
: tsig (B.(q1)) -> Bsig (A.(q2)) (B.(q2)) -> Type :=
| Paraex : forall (a : RElt_inst A) (b : RElt_inst (RApp_inst B a)),
RParasig A B (@exist _ _ a.(q1) b.(q1)) (Bex A.(q2) B.(q2) a.(q2) b.(q2))
| Parabêtasig : forall (ba : tsig B.(q1)) (f : Y -> Bsig A.(q2) B.(q2))
(x : X) (rel : RParasig A B ba (f (α x))),
RParasig A B ba (Bêtasig A.(q2) B.(q2) f x).
Definition Rsig {Γ : Ctx} : RElt Γ (∏ U (((Var U) → U) → U)).
Proof.
unshelve refine (exist3 _).
- cbv.
intros alpha gamma A B.
exact (tsig B).
- unshelve refine (fun gamma A B => exist _).
+ refine (Bsig A B).
+ exact (Bêtasig A B).
- unshelve refine (fun alpha gamma A B => exist _).
+ exact (RParasig A B).
+ exact (Parabêtasig A B).
Defined.
Arguments nil {A}.
Notation "x :: l" := (cons x l).
Definition Ty' (α : X -> Y) :=
triple
(fun (a : Type) (b : {A : Type & (Y -> A) -> X -> A}) =>
{Te : a -> fst b -> Type &
forall (a0 : a) (f : Y -> fst b) (x : X),
Te a0 (f (α x)) -> Te a0 (snd b f x)}).
Definition RElt' {α : X -> Y} (R : Ty' α) :=
triple (fun (a : q1 R) (b : fst (q2 R)) => fst (q3 R) a b).
Inductive RParalist {α : X -> Y} (A : Ty' α)
: list A.(q1) -> (@BranchingList X Y A.(q2)) -> Type :=
| RParanil : RParalist A nil (@Bnil_aux X Y _)
| RParacons : forall (la : list A.(q1)) (lb : @BranchingList X Y A.(q2))
(le : RParalist A la lb)
(x : RElt' A),
RParalist A (x.(q1) :: la) (Bcons_aux x.(q2) lb)
| RParabêtalist : forall (la : list A.(q1))
(f : Y -> (@BranchingList X Y A.(q2)))
(x : X)
(rel : RParalist A la (f (α x))),
RParalist A la (Bêtalist f x).
Definition Rlist {Γ : Ctx} : RElt Γ (U → U).
Proof.
unshelve refine (exist3 _).
- exact (fun alpha gamma A => list A).
- exact (@Blist X Y Γ.(q2)).
- unshelve refine (fun alpha gamma A => exist _).
+ exact (RParalist A).
+ exact (RParabêtalist A).
Defined.
Definition Rnil {Γ : Ctx} : RElt Γ (∏ U (Rlist • (Var U))).
Proof.
unshelve refine (exist3 _).
- exact (fun _ _ => @nil).
- exact (@Bnil X Y Γ.(q2)).
- exact (fun alpha gamma _ => RParanil _).
Defined.
Definition Rcons {Γ : Ctx} :
RElt Γ (∏ U ((Var U) → [RApp Rlist (Var U)] → [RApp Rlist (Var U)])).
Proof.
unshelve refine (exist3 _).
- exact (fun alpha gamma A a l => cons a l).
- exact (@Bcons X Y Γ.(q2)).
- now cbv ; refine (fun alpha gamma A a l => RParacons A l.(q1) l.(q2) l.(q3) a).
Defined.
(*Non-dependent eliminator for lists*)
Definition Rlist_rec (Γ : Ctx) :
@RElt Γ (∏ U
(∏ U
([Var U] →
([↑(Var U)] → Rlist • ↑ (Var U) → [Var U] → [Var U]) →
Rlist • ↑ (Var U) →
[Var U]))).
Proof.
unshelve refine (exist3 _).
- exact (@Alist_rec X Y Γ.(q1)).
- exact (@Blist_rec X Y Γ.(q2)).
- cbv.
unshelve refine (fun α gamma R P pnil pcons l => _).
refine (let fix f la lb le {struct le} :=
match le as le0 in RParalist _ la0 lb0
return
fst (q3 P)
((fix g (la : list (q1 R)) : q1 P :=
match la with
| nil => q1 pnil
| (x :: q) => q1 pcons x q (g q)
end) la0)
((fix g (lb : BranchingList (Y:=Y)) : fst (q2 P) :=
match lb with
| @Bnil_aux _ _ => q2 pnil
| Bcons_aux x q => q2 pcons x q (g q)
| Bêtalist h x => snd (q2 P) (fun y : Y => g (h y)) x
end) lb0)
with
| RParanil _ => pnil.(q3)
| RParacons _ qa qb qe x => pcons.(q3) x (exist3 qe) (exist3 (f qa qb qe))
| RParabêtalist _ qa g x rel => P.(q3).(snd) _ _ _ (f qa (g (α x)) rel)
end in f l.(q1) l.(q2) l.(q3)).
Defined.
Definition Runit {Γ : Ctx } : Ty Γ.
Proof.
unshelve refine (exist3 _).
- exact (fun _ _ => unit).
- exact (fun _ => @Bunit X Y).
- unshelve refine (fun _ _ => exist _).
+ exact (fun _ _ => unit).
+ exact (fun _ _ _ _ => tt).
Defined.
(*Storage operator for lists*)
Definition Rlist_stor{Γ : Ctx } :
RElt Γ (∏ U (Rlist • (Var U) → (Rlist • (Var U) → U) → U)).
Proof.
let T1 := constr: (∏ (@U (Γ · U · U)) ([(Var U)] →
([↑ (Var U)] → Rlist • (↑ (Var U)) → [(Var U)] → [(Var U)]) →
Rlist • (↑(Var U)) →
[(Var U)])) in
let T := constr: ((@Var (Γ · U) U ) → (([↑ (Var U)] → Rlist • ↑ (Var U) → [Var U] → [Var U]) → Rlist • ↑ (Var U) → [Var U])) in
pose (r := @RApp (Γ · U) U T (@RApp (Γ · U) U T1 ((@Rlist_rec _)) [@Var Γ U]) ((((@Rlist (Γ · U)) • (@Var Γ U)) → (@U (Γ · U))) → (@U (Γ · U)))).
let T := constr: (@RElt (Γ · U) ((((Rlist • (Var U)) → U) → U) → ([Var U] → (Rlist • (Var U)) → (((Rlist • (Var U)) → U) → U) → (((Rlist • (Var U)) → U) → U)) → (Rlist • (Var U)) → (((Rlist • (Var U)) → U) → U))) in
unshelve refine (let r : T := r in _).
unshelve refine (RLam _ _).
unshelve refine (RApp (RApp r _) _).
- unshelve refine (@RLam _ (Rlist • (Var U) → U) _ _).
unshelve refine (@RAppN _ (Rlist • ↑ (Var U)) (⇑ U) _ _).
+ now refine (@Var _ _).
+ now refine (Rnil • ↑(Var U)).
- refine (@RLamN _ _ _ _).
refine (@RLamN _ (⇑ (Rlist • (Var U)))
(⇑ (((Rlist • (Var U) → U) → U) → ((Rlist • (Var U) → U) → U))) _).
refine (@RLamN _ (⇑ ⇑ ((Rlist • (Var U) → U) → U)) (⇑ ⇑ ((Rlist • (Var U) → U) → U)) _).
refine (@RLamN _ (⇑ ⇑ ⇑ ((Rlist • (Var U) → U))) (⇑ ⇑ ⇑ U) _).
refine (@RApp _ ((Rlist • ↑ ↑ ↑ ↑ (Var U)) → U) (⇑ (⇑ (⇑ (⇑ U)))) _ _).
+ now refine (↑#).
+ apply RLamN.
refine (@RAppN _ (Rlist • ↑ ↑ ↑ ↑ ↑ (Var U)) _ _ _).
* now refine (↑#).
* refine (@RAppN _ (Rlist • ↑ ↑ ↑ ↑ ↑ (Var U)) _ _ _).
refine (@RAppN _ [↑ ↑ ↑ ↑ ↑ (Var U)] _ _ _).
refine (Rcons • (↑ ↑ ↑ ↑ ↑ (Var U))).
refine (↑ ↑ ↑ ↑ #).
exact #.
Defined.
(*Restricted dependent-eliminator for lists.*)
Definition Rlist_rect {Γ : Ctx} :
@RElt Γ (∏ U
(∏ ((Rlist • (Var U)) → U)
((@RAppN (Γ · U · ((Rlist • (Var U)) → U))
(⇑(Rlist • ((Var U)))) U # (Rnil • (↑(Var U)))) →
(∏ [↑(@Var _ U)]
(∏ (Rlist • (↑↑(@Var _ U)))
(([(@RAppN (Γ · U · ((Rlist • (Var U)) → U) · (↑#) · (Rlist • (↑↑(@Var _ U))))
((Rlist • (↑ ↑ ↑(Var U))))
(((Rlist • (↑ ↑ ↑(Var U))) → U) → U)
(Rlist_stor • (↑↑↑(@Var _ U)))
(@Var _ ((Rlist • (↑↑(Var U))))))
◊ (↑↑(@Var _ ((Rlist • (Var U)) → U)))]) →
([(@RAppN (Γ · U · ((Rlist • (Var U)) → U) · (↑#) · (Rlist • (↑↑(@Var _ U))))
((Rlist • (↑ ↑ ↑(Var U))))
(((Rlist • (↑ ↑ ↑(Var U))) → U) → U) (Rlist_stor • (↑↑↑(@Var _ U)))
((@RAppN (Γ · U · ((Rlist • (Var U)) → U) · (↑#) · (Rlist • (↑↑(@Var _ U))))
(↑ ↑ ↑(Var U))
((Rlist • (↑ ↑ ↑ (Var U))) → (Rlist • (↑ ↑ ↑ (Var U))))
(Rcons • (↑↑↑(@Var _ U))) (↑#)) ◊ #))
◊ (↑↑(@Var _ ((Rlist • (Var U)) → U)))])))) →
∏ (Rlist • ↑(Var U))
[(@RAppN (Γ · U · ((Rlist • (Var U)) → U) · (Rlist • ↑(Var U)))
((Rlist • (↑ ↑ (Var U))))
(((Rlist • (↑ ↑(Var U))) → U) → U)
(Rlist_stor • (↑↑(@Var _ U))) #) ◊ (↑#)]))).
Proof.
unshelve refine (exist3 _).
- exact (@Alist_rect X Y Γ.(q1)).
- exact (@Blist_rect X Y Γ.(q2)).
- refine (fun α gamma A P pnil pcons l => _).
lazy in l.
destruct l as [la lb le].
unfold Alist_rect ; unfold Blist_rect.
induction le.
+ exact pnil.(q3).
+ simpl in pcons.
vm_compute.
unshelve refine (pcons.(q3) x (exist3 le) _).
refine (let fix f la lb le :=
match le
with
| RParanil _ => _
| RParacons _ qa qb qe x => _
| RParabêtalist _ qa g x rel => _
end
in f la lb le).
+ exact (pnil.(q3)).
induction le.
+ exact pnil.(q3).
+ refine (pcons.(q3) x (exist3 le) _).
:=
fun _ B P pnil pcons =>
fix f l := match l as l0 return
((fix g (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
match l with
| Bnil_aux => fun P => P (Bnil_aux)
| Bcons_aux x q =>
fun P =>
g q (fun l' => P (Bcons_aux x l'))
| Bêtalist g x => fun P => Bunit
end) l0 P).(fst)
with
| Bnil_aux => pnil
| Bcons_aux x q => pcons x q (f q)
| Bêtalist _ _ => tt
end.
Proof.
unshelve refine (fun gamma B P pnil pcons => _).
refine (fix f l := match l as l0 return
((fix g (l : @BranchingList B) : (@BranchingList B -> BranchingTYPE) -> BranchingTYPE :=
match l with
| Bnil_aux => fun P => P (Bnil_aux)
| Bcons_aux x q =>
fun P =>
g q (fun l' => P (Bcons_aux x l'))
| Bêtalist g x => fun P => Bunit
end) l0 P).(fst)
with
| Bnil_aux => pnil
| Bcons_aux x q => pcons x q (f q)
| Bêtalist _ _ => tt
end).*)
Inductive Eq {A : Type} (x : A) : A -> Type := Eq_refl : Eq x x.
Inductive Beq (A : BranchingTYPE X Y) (a : A.(fst)) : A.(fst) -> Type :=
| Beq_refl : Beq A a a
| Bêtaeq : forall (b : A.(fst)), (Y -> Beq A a b) -> X -> Beq A a b.
Inductive RParaeq {Γ : Ctx} {α : X -> Y} {γ : Γ ‡ α} (A : Ty_inst U γ) (a : RElt_inst A) :
forall (b : RElt_inst A),
(Eq a.(q1) b.(q1)) -> (Beq A.(q2) a.(q2) b.(q2)) -> Type :=
| RParaeq_refl : RParaeq A a a (Eq_refl a.(q1)) (Beq_refl A.(q2) a.(q2))
| RParabêtaeq : forall (b : RElt_inst A) (e : Eq a.(q1) b.(q1))
(f : Y -> Beq A.(q2) a.(q2) b.(q2)) (x : X)
(rel : RParaeq A a b e (f (α x))),
RParaeq A a b e (Bêtaeq A.(q2) a.(q2) b.(q2) f x).
Definition Req {Γ : Ctx} : RElt Γ (∏ U ((Var U) → (Var U) → U)).
Proof.
unshelve refine (exist3 _).
- exact (fun alpha gamma => @Eq).
- unshelve refine (fun gamma A a b => exist _).
+ exact (Beq A a b).
+ exact (Bêtaeq A a b).
- unshelve refine (fun alpha gamma A a b => exist _).
+ exact (RParaeq A a b).
+ exact (RParabêtaeq A a b).
Defined.
Print Rcons.
(*
Inductive AEqFin {Γ : Ctx} {α : X -> Y} {γ : Γ ‡ α} :
(Ty_inst Rnat γ -> nat) -> Ty_inst [RApp Rlist Rnat] γ -> (Ty_inst Rnat γ -> nat) -> Type :=
| AEqnil : forall (f g : (Ty_inst Rnat γ -> nat)), AEqFin f (Rnil ® γ) g
| AEqcons : forall (f g : (Ty_inst Rnat γ -> nat))
(l : Ty_inst [RApp Rlist Rnat] γ)
(n : Ty_inst Rnat γ),
(f n = g n) -> (AEqFin f l g) -> (AEqFin f (Rcons n l) g).*)
Inductive AEqFin : (nat -> nat) -> list nat -> (nat -> nat) -> Type :=
AEqnil : forall alpha bêta : nat -> nat, AEqFin alpha nil bêta
| AEqcons : forall (alpha bêta : nat -> nat) (l : list nat) (x : nat),
Eq (alpha x) (bêta x) ->
AEqFin alpha l bêta -> AEqFin alpha (x :: l) bêta.
Definition Bnat' : BranchingTYPE X Y :=
{| fst := BranchingNat X Y ; snd := @Bêtanat X Y |}.
Print Bcons_aux.
Inductive BEqFin : (BranchingNat X Y -> BranchingNat X Y) ->
(@BranchingList X Y Bnat') ->
(BranchingNat X Y -> BranchingNat X Y) ->
Type :=
| BEqnil : forall (f g : BranchingNat X Y -> BranchingNat X Y),
BEqFin f (@Bnil_aux X Y Bnat') g
| BEqcons : forall (f g : BranchingNat X Y -> BranchingNat X Y)
(l : (@BranchingList X Y Bnat'))
(n : Bnat'.(fst)),
(Beq Bnat' (f n) (g n)) -> (BEqFin f l g) -> (BEqFin f (Bcons_aux n l) g)
| BêtaEqFin : forall (f g : BranchingNat X Y -> BranchingNat X Y)
(l : (@BranchingList X Y Bnat'))
(h : Y -> BEqFin f l g) (x : X),
BEqFin f l g.
Definition Rnil_nat {Γ : Ctx} : RElt Γ (([RApp Rlist Rnat])).
Proof.
unshelve refine (exist3 _).
- exact (fun _ _ => @nil nat).
- exact (fun _ => @Bnil_aux X Y _).
- exact (fun _ _ => RParanil _).
Defined.
Definition Rcons_nat {Γ : Ctx} : RElt Γ (Rnat → ([RApp Rlist Rnat] → [RApp Rlist Rnat])).
Proof.
unshelve refine (exist3 _).
- exact (fun _ _ => @cons nat).
- exact (fun _ => @Bcons_aux X Y _).
- exact (fun _ _ n l => RParacons _ _ _ l.(q3) _).
Defined.
Inductive RParaEqFin {Γ : Ctx} {α : X -> Y} {γ : Γ ‡ α} :
forall (f : Ty_inst [Rnat → Rnat] γ) (l : Ty_inst [RApp Rlist Rnat] γ)
(g : Ty_inst [Rnat → Rnat] γ),
AEqFin f.(q1) l.(q1) g.(q1) -> BEqFin f.(q2) l.(q2) g.(q2) -> Type :=
| RParaEqnil : forall (f g : Ty_inst [Rnat → Rnat] γ),
RParaEqFin f (Rnil_nat ® γ) g (AEqnil f.(q1) g.(q1)) (BEqnil f.(q2) g.(q2))
| RParaEqcons : forall (f g : Ty_inst [Rnat → Rnat] γ)
(l : Ty_inst [RApp Rlist Rnat] γ)
(n : Ty_inst Rnat γ)
(i : AEqFin f.(q1) l.(q1) g.(q1))
(j : BEqFin f.(q2) l.(q2) g.(q2))
(k : RElt_inst (@RApp_inst Γ α _ Rnat (⇑U)
(@RApp_inst Γ α γ Rnat ((Rnat → U))
((@RApp Γ U ((Var U) → (Var U) → U) Req Rnat) ® γ) (RApp_inst f n))
(RApp_inst g n))),
RParaEqFin f l g i j ->
RParaEqFin f (RApp_inst (RApp_inst (Rcons_nat ® γ) n) l) g
(AEqcons f.(q1) g.(q1) l.(q1) n.(q1) k.(q1) i)
(BEqcons f.(q2) g.(q2) l.(q2) n.(q2) k.(q2) j)
| RParabêtaEqFin : forall (f g : Ty_inst [Rnat → Rnat] γ)
(l : Ty_inst [RApp Rlist Rnat] γ)
(i : AEqFin f.(q1) l.(q1) g.(q1))
(h : Y -> BEqFin f.(q2) l.(q2) g.(q2)) (x : X)
(rel : RParaEqFin f l g i (h (α x))),
RParaEqFin f l g i (BêtaEqFin f.(q2) g.(q2) l.(q2) h x).
Definition REqFin {Γ : Ctx} :
RElt Γ ((Rnat → Rnat) →
[RApp Rlist Rnat] →
(Rnat → Rnat) → U).
Proof.
unshelve refine (exist3 _).
- exact (fun alpha gamma f l g => AEqFin f l g).
- unshelve refine (fun gamma f l g => exist _).
+ exact (BEqFin f l g).
+ exact (BêtaEqFin f g l).
- unshelve refine (fun alpha gamma f l g => exist _).
+ exact (RParaEqFin f l g).
+ exact (RParabêtaEqFin f g l).
Defined.
Definition Acontinuous (f : (nat -> nat) -> nat) (u : nat -> nat) :=
{l : list nat & forall v : nat -> nat, AEqFin u l v -> f u = f v}.
Definition Bcontinuous (f : ((Bnat').(fst) -> (Bnat').(fst)) -> (Bnat').(fst))
(u : (Bnat').(fst) -> (Bnat').(fst)) : BranchingTYPE X Y.
Proof.
unshelve refine (exist _).
unshelve refine (Bsig _ _).
- unshelve refine (exist _).
+ exact (@BranchingList X Y Bnat').
+ exact (@Bêtalist X Y _).
- unshelve refine (fun l => exist _).
+ refine (forall v : (BranchingNat X Y) -> (BranchingNat X Y), BEqFin u l v -> Beq _ (f u) (f v)).
+ exact (fun h e v rel => Bêtaeq _ (f u) (f v) (fun y => h y v rel) e).
- exact (Bêtasig _ _).
Defined.
(*Definition Rcontinuous {Γ : Ctx} :
RElt Γ (((Rnat → Rnat) → Rnat) →
(Rnat → Rnat) → U).
Proof.
(*unshelve refine (exist3 _).
- unshelve refine (fun alpha gamma f u => _).
refine ({l : list nat & forall v : nat -> nat, AEqFin u l v -> f u = f v}).
- unshelve refine (fun gamma f u => exist _).
+ unshelve refine (Bsig (@Blist X Y (@Bnat X Y)) _).
unshelve refine (fun l => exist _).
* refine (forall v : (BranchingNat X Y) -> (BranchingNat X Y), BEqFin u l v -> Beq _ (f u) (f v)).
* exact (fun h e v rel => Bêtaeq _ (f u) (f v) (fun y => h y v rel) e).
+ simpl.
unshelve refine (Bêtasig _ _).
- unshelve refine (fun alpha gamma f u => exist _).
+ simpl.
intros acont bcont.
refine ({l : BEl (@Blist X Y (@Bnat X Y)) & forall v : (BranchingNat X Y) -> (BranchingNat X Y), BEqFin u l v -> f u = f v}).
+ unshelve refine (fun h e => exist _).
* refine (Bêtalist (fun y => (h y).(fst)) e).
* intros v rel.
have aux := (BêtaEqFin u v (Bêtalist (fun y : Y => fst (h y)) e) _ e).
exact (BêtaEqFin u v (Bêtalist (fun y : Y => fst (h y)) e) _ e).*)
refine (RLamN _).
refine (@RLamN (@Ctx_cons Γ ((Rnat → Rnat) → Rnat)) (⇑ ((Rnat → Rnat))) (⇑ U) _).
refine (@RAppN _ ((@RApp (Γ · ((Rnat → Rnat) → Rnat) · ⇑ (Rnat → Rnat)) _ _ Rlist Rnat) → U) U _ _).
refine (@RApp _ _ _ Rsig (RApp Rlist Rnat)).
refine (@RLamN _ _ _ _).
unshelve refine (RPi (Rnat → Rnat) _).
unshelve refine (RPi _ _).
refine (@RAppN _ (Rnat → Rnat) U _ ((Var (Rnat → Rnat)))).
refine (@RAppN _ (⇑ ⇑(@RApp (Γ · ((Rnat → Rnat) → Rnat) · ⇑ (Rnat → Rnat)) _ _ Rlist Rnat)) ((Rnat → Rnat) → U) _ (↑ (Var (@RApp (Γ · ((Rnat → Rnat) → Rnat) · ⇑ (Rnat → Rnat)) _ _ Rlist Rnat)))).
refine (@RAppN _ (Rnat → Rnat) (⇑ (⇑ (Rlist • Rnat)) → (Rnat → Rnat) → U) _ (↑↑(Var (Rnat → Rnat)))).
refine (↑ ↑ REqFin).
refine (REL _).
refine (@RAppN _ Rnat U _ _).
refine (@RAppN _ Rnat (Rnat → U) _ _).
refine (RApp Req Rnat).
unshelve refine (@RAppN _ ((Rnat → Rnat)) Rnat _ _).
- refine (↑ ↑ ↑ ↑ (Var ((Rnat → Rnat) → Rnat))).
- refine (↑ ↑ ↑ (Var (Rnat → Rnat))).
- unshelve refine (@RAppN _ ((Rnat → Rnat)) Rnat _ _).
+ refine (↑ ↑ ↑ ↑ (Var ((Rnat → Rnat) → Rnat))).
+ refine (↑ (Var (Rnat → Rnat))).
Defined.
Definition inj1 {Γ : Ctx} (n : nat) : RElt Γ Rnat.
Proof.
induction n.
- exact R0.
- exact (RApp RS IHn).
Defined.
Definition inj2 {Γ : Ctx} (u : nat -> nat) : RElt Γ (Rnat → Rnat).
Proof.
unshelve refine (exist3 _).
- exact (fun _ _ => u).
- unshelve refine (fun gamma n => _).
refine (let fix f v n := match n with
| B0 _ _ => BNEta _ _ (v 0)
| BS m => f (fun k => v (S k)) m
| Bêtanat h x => Bêtanat (fun y => f v (h y)) x
end in f u n).
- unshelve refine (fun alpha gamma n => _).
simpl.
destruct n as [na nb ne].
revert u.
elim: ne.
+ intro u ; simpl.
induction (u 0).
* exact (RP0 alpha).
* simpl.
exact (RPS alpha _ _ IHn).
+ simpl.
intros ma mb me ihme u.
exact (ihme (fun k => u (S k))).
+ simpl ; intros ma h x rel ih u.
exact (RPbêta alpha _ _ _ (ih u)).
Defined.*)
End AvareXY.
Section Avarenat.
Notation " Γ ‡ α " := (Ctx_El nat nat Γ α) (at level 11).
Notation "r ® γ" := (Inst nat nat r γ) (at level 10, left associativity).
Notation "()" := (ctx_nil nat nat).
Notation "Γ · A" := (Ctx_cons nat nat Γ A) (at level 50, left associativity).
Notation "γ ·· x" := (ctx_cons nat nat γ x) (at level 50, left associativity).
Notation "¿ g" := (Ctx_tl nat nat g) (at level 10).
Notation "⇑ A" := (Lift nat nat A) (at level 10).
Notation "#" := (Var nat nat _) (at level 0).
Notation "↑ M" := (Weaken nat nat M) (at level 10).
Notation "S {{ r }} " := (Sub nat nat S r) (at level 20, left associativity).
Notation "∏" := (RPi nat nat).
Notation "A → B" := (RPi nat nat A (⇑ B)) (at level 99, right associativity, B at level 200).
Notation "'λ'" := (RLam nat nat).
Notation "t • u" := (RApp nat nat t u) (at level 12, left associativity).
Notation "'Ctx'" := (Ctx nat nat).
Notation "'RElt'" := (RElt nat nat).
Notation "'Rnat'" := (@Rnat nat nat).
Definition inj3 {Γ : Ctx} (f : (nat -> nat) -> nat) (alpha : nat -> nat) (γ : Γ ‡ alpha) :
(forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> f u = f v) ->
(Ty_inst nat nat ((Rnat → Rnat) → Rnat) γ).
Proof.
intro hyp.
unshelve refine (exist3 _).
- exact f.
- simpl ; unshelve refine (fun u => _).
refine (BNEta nat nat _).
exact ((f (fun n => BNdialogue (u (BNEta _ _ n)) alpha))).
- simpl.
intro v.
have aux : forall m : nat, RParanat nat nat alpha m (BNEta _ _ m).
+ induction m.
* exact (RP0 nat nat alpha).
* exact (RPS nat nat alpha m _ IHm).
+ have aux2 : f (q1 v) = f (fun n : nat => BNdialogue (q2 v (BNEta nat nat n)) alpha).
* refine (hyp (q1 v) (fun n : nat => BNdialogue (q2 v (BNEta nat nat n)) alpha) _).
destruct v as [va vb ve].
simpl.
cbv in ve.
intro n.
specialize ve with (exist3 (aux n)) ; simpl in ve.
elim: ve ; trivial ; simpl.
intros ma mb me ; exact: eq_S.
* rewrite - aux2.
exact (aux (f (q1 v))).
Defined.
(*Theorem cont_imp_cont (f : (nat -> nat) -> nat)
(ext : forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> f u = f v)
(cont : RElt (Ctx_nil nat nat) (∏ ((Rnat → Rnat) → Rnat)
(∏ (Rnat → Rnat) ((Rcontinuous nat nat • (↑(Var nat nat ((Rnat → Rnat) → Rnat)))) • (Var nat nat (Rnat → Rnat)))))) :
forall (alpha : nat -> nat), continuous f alpha.
Proof.
intro alpha.
have aux : {l : list nat & forall v : nat -> nat, AEqFin alpha l v -> Eq (f alpha) (f v)}.
exact (cont.(q1) alpha tt f alpha).
cbv in t.
exact t.
destruct cont as [conta contb conte].
cbv.
cbv in conta.
exact (conta alpha tt f alpha).*)
Definition RGeneric {Γ : Ctx} : RElt Γ (Rnat → Rnat).
Proof.
exists (fun α gamma => α) (fun gamma => Generic_aux 0).
intros α gamma n.
destruct n as [no nt ne] ; simpl.
unshelve refine (let aux : forall (k : nat),
RParanat _ _ α (α (k + no)) (Generic_aux k nt) := _ in _).
- revert ne ; revert no ; revert nt.
unshelve refine (fix f nt no ne k {struct ne}:= match ne with
| RP0 _ _ _ => RPbêta nat nat _ _ _ _ _
| RPS _ _ _ _ _ _ => _
| RPbêta _ _ _ _ _ _ _ => _
end).
+ rewrite - plus_n_O.
refine (let fix g n := match n as n0
return (RParanat nat nat α n0 (BNEta nat nat (n0)))
with
| 0 => (RP0 _ _ α)
| S k => RPS nat nat α k (BNEta nat nat k) (g k)
end
in g (α k)).
+ rewrite - plus_n_Sm ; rewrite - plus_Sn_m.
exact (f b n r (S k)).
+ simpl. apply RPbêta. now apply (f (b (α n0)) n r k) .
- exact: (aux 0).
Defined.
Print RParanat_equal.
Lemma NaturRadinPGeneric {Γ : Ctx} {α : nat -> nat} (n : RElt Γ Rnat)
(γ : Γ ‡ α):
BNdialogue ((RGeneric • n) ® γ).(q2) α = α (n ® γ).(q1).
Proof.
destruct n as [no nt ne] ; simpl.
have aux : forall (k : nat),
BNdialogue (Generic_aux k (nt (q2 γ))) α = α (k + (no α (q1 γ))).
- elim: (ne α γ) ; simpl.
+ intros k ; now rewrite NaturBNEtaDialogue ; rewrite - plus_n_O.
+ intros mt mo me ihme k.
rewrite - plus_n_Sm ; rewrite - plus_Sn_m.
exact: ihme.
+ intros f x mo me ihme k.
now specialize ihme with k.
- exact: aux.
Qed.
Theorem continuity (f : RElt (Ctx_nil nat nat) ((Rnat → Rnat) → Rnat)) (α : nat -> nat) :
continuous (fun p => f.(q1) p ().(q1) p) α.
Proof.
pose proof (@RParanat_equal nat nat (Ctx_nil nat nat) (f • RGeneric)) as Eq.
destruct (BNDialogue_Continuity (f.(q2) (@ctx_nil nat nat α).(q1) (Generic_aux 0)) α)
as [l ihl].
exists l ; intros β Finite_Eq.
simpl in Eq ; rewrite - (Eq α () ) ; rewrite - (Eq β () ).
exact: ihl.
Qed.
Arguments nil {A}.
Notation "x :: l" := (cons x l).
Fixpoint upton (n : nat) : list nat :=
match n with
| 0 => (0 :: nil)
| S k => (S k :: (upton k))
end.
(*Definition uptocontinuous (f : (nat -> nat) -> nat) (alpha : nat -> nat) :=
{n : nat & forall bêta : nat -> nat, EqFin alpha (upton n) bêta -> f alpha = f bêta}.
Lemma Inconsistency (P : forall (f : (nat -> nat) -> nat)
(ext : forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> f u = f v), forall (alpha : nat -> nat), uptocontinuous f alpha) :
False.
Proof.
pose M := P _ _ (fun _ => 0).
pose m := M (fun _ => 0) (fun _ _ _ => eq_refl).
Print f_equal.
pose aux : forall beta : nat -> nat,
(forall u v : nat -> nat,
(forall n : nat, u n = v n) -> beta (u m.(fst)) = beta (v m.(fst))) :=
fun bêta u v hyp => f_equal bêta (hyp m.(fst)).
- pose f := fun beta => M (fun alpha => beta (alpha m.(fst))) (aux _).
have aux2 :forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> (f u).(fst) = (f v).(fst).
+ intros u v hyp.
unfold f.
unfold aux.
unfold f.
unfold m.
unfold aux.
Lemma continuity2 (f : (nat -> nat) -> nat) (alpha : nat -> nat)
(ext : forall (u v : nat -> nat), (forall (n : nat), u n = v n) -> f u = f v) :
continuous f alpha.
Proof.
have p := (RApp_inst _ _ (inj3 f alpha () ext) (RGeneric ® (@ctx_nil nat nat alpha))).(q1) .
have hyp : forall alpha beta, (RApp_inst _ _ (inj3 f alpha () ext) (RGeneric ® (@ctx_nil nat nat alpha))).(q2) = (RApp_inst _ _ (inj3 f beta () ext) (RGeneric ® (@ctx_nil nat nat beta))).(q2).
cbn.
cbv.
< reflexivity.
have aux : BNdialogue p.(q2) alpha = p.(q1).
- destruct p as [pa pb pe] ; simpl.
elim: pe ; trivial.
exact (fun _ _ _ => eq_S _ _).
- About BNDialogue_Continuity.*)
End Avarenat.
Computing file changes ...
