SysF_PTS.lambda2

(* (c) 2017, Jonas Kaiser, based on major contributions from Tobias Tebbi *)

Singel sorted PTS Lambda2

We define a de Bruijn presentation of the Pure Type System Lambda 2 and develop its theory. The definitions are those from our 2017 CPP paper. We also present the auxiliary type system P found in that article.

Require Import List Program.Equality.
From Autosubst Require Export Autosubst.

Require Import Decidable lib.

Set Implicit Arguments.

Syntax

Sorts/Universes
Inductive level := Prp | Typ.

Terms
Inductive termL : Type :=
| VarL (x : var)
| ProdL (a : termL) (b : {bind termL})
| AppL (a b : termL)
| LamL (a : termL) (b : {bind termL})
| SortL (u : level).

Decidable Equality on the Term Syntax
Instance decide_eq_level (u v : level) : Dec (u = v). derive. Defined.
Instance decide_eq_termL (a b : termL) : Dec (a = b). derive. Defined.

Autosubst machinery
Instance Ids_termL : Ids termL. derive. Defined.
Instance Rename_termL : Rename termL. derive. Defined.
Instance Subst_termL : Subst termL. derive. Defined.
Instance SubstLemmas_termL : SubstLemmas termL. derive. Qed.

Boolean decision test for Prp inside an Option
Definition eqPrp s := (if decide (s = Some(SortL Prp)) then true else false).

Some facts about sorts/levels and substitutions

Lemma sortL_ren u xi a : SortL u = a.[ren xi] -> a = SortL u.
Proof. intros E. destruct a; try discriminate E. asimpl in *. congruence. Qed.

Lemma sortL_p1 u : SortL u = (SortL u).[ren (+1)].
Proof. reflexivity. Qed.

Lemma sortL_add_subst {u} sigma : SortL u = (SortL u).[sigma].
Proof. reflexivity. Qed.

Lemma sortP_neq_ren xi a u : a.[ren xi] <> SortL u -> a <> SortL u.
Proof. destruct a; try discriminate. now asimpl. Qed.

Lemma sortP_eqPrp_f a : a <> SortL Prp -> eqPrp (Some a) = false.
Proof. intros H. destruct a; trivial. destruct u; trivial. congruence. Qed.

Lemma atnd_eqPrp_t Gamma x :
  atnd Gamma x (SortL Prp) -> eqPrp (get Gamma x) = true.
Proof.
  intros H. apply atnd_getD in H. rewrite getD_get in H.
  simpl in *. ca. ainv. atom_ren. rewrite H1. reflexivity.
Qed.

Lemma atnd_notPrp_eqPrp_f Gamma x a :
  atnd Gamma x a -> a <> (SortL Prp) -> eqPrp (get Gamma x) = false.
Proof.
  intros H. apply atnd_getD in H. rewrite getD_get in H.
  simpl in *. unfold eqPrp. ca. ainv. congruence.
Qed.

Lemma eqPrp_ren a xi : eqPrp (Some a.[ren xi]) = eqPrp (Some a).
Proof. destruct a; reflexivity. Qed.

Lemma eqPrp_t_subst_t a sigma : eqPrp (Some a) = true -> eqPrp (Some a.[sigma]) = true.
Proof. intros E. destruct a; trivial; discriminate. Qed.

System L - the usual PTS typing rules (without conversion)

Typing Judgement
Inductive typingL (Gamma : list termL) : termL -> termL -> Prop :=
| typingL_ax :
    typingL Gamma (SortL Prp) (SortL Typ)
| typingL_var x a u :
    atnd Gamma x a -> typingL Gamma a (SortL u) ->
    typingL Gamma (VarL x) a
| typingL_prod a b u :
    typingL Gamma a (SortL u) -> typingL (a :: Gamma) b (SortL Prp) ->
    typingL Gamma (ProdL a b) (SortL Prp)
| typingL_app a b c d d' :
    typingL Gamma a (ProdL c d) -> typingL Gamma b c -> d' = d.[b/] ->
    typingL Gamma (AppL a b) d'
| typingL_lam a b c u :
    typingL Gamma a (SortL u) ->
    typingL (a :: Gamma) c (SortL Prp) ->
    typingL (a :: Gamma) b c ->
    typingL Gamma (LamL a b) (ProdL a c).

Well formed contexts
Inductive wfL : list termL -> Prop :=
| wfL_empty : wfL nil
| wfL_ext Gamma a u : typingL Gamma a (SortL u) -> wfL Gamma -> wfL (a :: Gamma).

REMARK: we try to avoid assuming well-formedness of contexts as much as possible, as it is viral. For the beta and id CMs of L, they appear to be essential though ... Note that in System P, the assumption can mostly be avoided (apart from internalisation)
Theory of L

Lemma typingL_prp_prp_contra Gamma : typingL Gamma (SortL Prp) (SortL Prp) -> False.
Proof. intros H. ainv. Qed.

(* Note: it is crucial that we only relate context lookups, not variable typings, here,
   as L is otherwise "too" recursive. That is, cr_typingL_up would not be provable, due to the sort condition. *)
Definition cr_typingL (xi : var -> var) Gamma Delta := forall x a, atnd Gamma x a -> atnd Delta (xi x) a.[ren xi].

Lemma cr_typingL_up a xi Gamma Delta : cr_typingL xi Gamma Delta -> cr_typingL (upren xi) (a :: Gamma) (a.[ren xi] :: Delta).
Proof.
  intros CR [|n] b Ln.
  - ainv. asimpl. constructor. autosubst.
  - ainv. asimpl. econstructor; eauto. autosubst.
Qed.

Lemma typingL_ren Gamma a b : typingL Gamma a b -> forall Delta xi, cr_typingL xi Gamma Delta -> typingL Delta a.[ren xi] b.[ren xi].
Proof.
  intros H; induction H; intros Delta xi CR.
  - constructor.
  - econstructor; eauto.
  - econstructor; eauto. apply cr_typingL_up with (a:= a) in CR.
    specialize (IHtypingL2 _ _ CR). asimpl in IHtypingL2. now asimpl.
  - econstructor; eauto. subst. autosubst.
  - pose proof (@cr_typingL_up a _ _ _ CR) as CR'. econstructor; eauto.
    + specialize (IHtypingL2 _ _ CR'). asimpl in IHtypingL2. now asimpl.
    + specialize (IHtypingL3 _ _ CR'). asimpl in IHtypingL3. now asimpl.
Qed.

Lemma cr_typingL_shift Gamma a : cr_typingL (+1) Gamma (a :: Gamma).
Proof. intros n b L. econstructor; eauto. Qed.

Theorem typingL_weaken Gamma a b c : typingL Gamma a b -> typingL (c :: Gamma) a.[ren (+1)] b.[ren (+1)].
Proof. intros H. eapply typingL_ren; eauto using cr_typingL_shift. Qed.

Lemma wfL_atnd_ok Gamma n a : wfL Gamma -> atnd Gamma n a -> exists u, typingL Gamma a (SortL u).
Proof.
  intros W; revert n a. induction W; intros n b Ln.
  - inversion Ln.
  - destruct n; inversion Ln; subst.
    + exists u. rewrite (sortL_add_subst (ren (+1))). now apply typingL_weaken.
    + specialize (IHW _ _ H3). destruct IHW as [u' T].
      exists u'. rewrite (sortL_add_subst (ren (+1))). now apply typingL_weaken.
Qed.

(* This is the L-native CM definition which will cause the proliferation of well-formedness assumptions.
   We later us the L-P-Equivalence to obtain strengthening for PTS "types", which allows us to get away
   without well-formedness. *)
Definition cm_typingL_nat (sigma : var -> termL) Gamma Delta := forall x a, atnd Gamma x a -> typingL Delta (sigma x) a.[sigma].

(* We really need the side condition here, to handle the well-formedness assumption of the var rule! *)
Lemma cm_typingL_nat_up a u sigma Gamma Delta : cm_typingL_nat sigma Gamma Delta -> typingL Delta a.[sigma] (SortL u) -> cm_typingL_nat (up sigma) (a :: Gamma) (a.[sigma] :: Delta).
Proof.
  intros CM H [|n] b Ln.
  - ainv. asimpl. apply typingL_var with (u:=u).
    + constructor. autosubst.
    + rewrite (sortL_add_subst (ren (+1))). replace a.[sigma >> ren (+1)] with a.[sigma].[ren (+1)] by autosubst.
      now apply typingL_weaken.
  - ainv. asimpl. replace B.[sigma >> ren (+1)] with B.[sigma].[ren (+1)] by autosubst.
    now apply typingL_weaken, CM.
Qed.

Lemma typingL_subst_nat Gamma a b : typingL Gamma a b -> forall Delta sigma, cm_typingL_nat sigma Gamma Delta -> typingL Delta a.[sigma] b.[sigma].
Proof.
  intros H; induction H; intros Delta sigma CM.
  - constructor.
  - now apply CM.
  - econstructor; eauto. rewrite (sortL_add_subst (up sigma)).
    apply IHtypingL2. eapply cm_typingL_nat_up; eauto.
  - econstructor; eauto. subst. autosubst.
  - econstructor; eauto.
    + rewrite (sortL_add_subst (up sigma)). eapply IHtypingL2; eauto using cm_typingL_nat_up.
    + eapply IHtypingL3; eauto using cm_typingL_nat_up.
Qed.

Lemma cm_typingL_nat_id Gamma : wfL Gamma -> cm_typingL_nat ids Gamma Gamma.
Proof. intros W n b L. asimpl. destruct (wfL_atnd_ok W L) as [u T]. econstructor; eauto. Qed.

Lemma cm_typingL_nat_beta Gamma c d : wfL Gamma -> typingL Gamma c d -> cm_typingL_nat (c .: ids) (d :: Gamma) Gamma.
Proof.
  intros W T [|n] b L; ainv; asimpl.
  - trivial.
  - destruct (wfL_atnd_ok W H2) as [u T']. econstructor; eauto.
Qed.

Theorem typingL_beta_nat Gamma a b c d:
  wfL Gamma -> typingL Gamma c d -> typingL (d :: Gamma) a b -> typingL Gamma a.[c/] b.[c/].
Proof. intros W T H. eapply typingL_subst_nat; eauto using cm_typingL_nat_beta. Qed.

Theorem typingL_propagation_nat Gamma a b : wfL Gamma -> typingL Gamma a b -> b = SortL Typ \/ exists u, typingL Gamma b (SortL u).
Proof.
  intros W H; induction H; try (now left); right.
  - exists u; trivial.
  - exists Typ; constructor.
  - exists Prp. subst. destruct (IHtypingL1 W) as [E|[u TProd]]; [discriminate E|]. ainv.
    apply (typingL_beta_nat W H0) in H5. autosubst.
  - exists Prp. econstructor; eauto.
Qed.

Theorem typingL_typ_degenerate_nat Gamma a : wfL Gamma -> typingL Gamma a (SortL Typ) -> a = (SortL Prp).
Proof.
  intros W H. depind H; trivial.
  - ainv.
  - apply (typingL_propagation_nat W) in H. destruct H as [EX| [u TProd]]; [discriminate EX|]. ainv.
Qed.

System P - the auxilary type system

Type Formation Judgement
Inductive istyP Gamma : termL -> Prop :=
| istyP_var x :
    atnd Gamma x (SortL Prp) ->
    istyP Gamma (VarL x)
| istyP_prod1 a :
    istyP ((SortL Prp) :: Gamma) a ->
    istyP Gamma (ProdL (SortL Prp) a)
| istyP_prod2 a b :
    istyP Gamma a -> istyP (a :: Gamma) b ->
    istyP Gamma (ProdL a b).

Typing Judgement
Inductive typingP Gamma : termL -> termL -> Prop :=
| typingP_var x a :
    atnd Gamma x a -> istyP Gamma a ->
    typingP Gamma (VarL x) a
| typingP_app1 a b c d d' :
    typingP Gamma a (ProdL c d) -> typingP Gamma b c -> d' = d.[b/] ->
    typingP Gamma (AppL a b) d'
| typingP_lam1 a b c :
    istyP Gamma a -> typingP (a :: Gamma) b c ->
    typingP Gamma (LamL a b) (ProdL a c)
| typingP_app2 a b b' c :
    typingP Gamma a (ProdL (SortL Prp) b) -> istyP Gamma c -> b' = b.[c/] ->
    typingP Gamma (AppL a c) b'
| typingP_lam2 a b :
    typingP ((SortL Prp) :: Gamma) a b ->
    typingP Gamma (LamL (SortL Prp) a) (ProdL (SortL Prp) b).

Theory of P
Lemma istyP_notSort Gamma u : ~ istyP Gamma (SortL u).
Proof. intros H. ainv. Qed.

Lemma istyP_neqPrp Gamma a : istyP Gamma a -> a <> SortL Prp.
Proof. destruct 1; congruence. Qed.

Lemma atnd_type_eqPrp_f Gamma x a :
  atnd Gamma x a -> istyP Gamma a -> eqPrp (get Gamma x) = false.
Proof. intros H1 H2. eapply atnd_notPrp_eqPrp_f; eauto using istyP_neqPrp. Qed.

Definition cr_istyP (rho xi : var -> var) Gamma Delta := forall x, istyP Gamma (VarL (rho x)) -> istyP Delta (VarL (xi x)).

Lemma cr_cr_istyP xi Gamma Delta : cr xi Gamma Delta -> cr_istyP id xi Gamma Delta.
Proof. intros CR n H. ainv. apply CR in H1. constructor. now asimpl in *. Qed.

Lemma cr_istyP_id Gamma : cr_istyP id id Gamma Gamma.
Proof. intros n. auto. Qed.

Lemma cr_istyP_up a rho xi Gamma Delta : cr_istyP rho xi Gamma Delta -> cr_istyP (upren rho) (upren xi) (a.[ren rho] :: Gamma) (a.[ren xi] :: Delta).
Proof.
  intros CR [|n] L; ainv; asimpl in *.
  - apply sortL_ren in H1. subst. constructor. now econstructor.
  - apply sortL_ren in H1. rewrite H1 in H3.
    cut (istyP Gamma (VarL (rho n))); [intros J| now constructor]. aspec. ainv.
    constructor. rewrite sortL_p1. econstructor; eauto.
Qed.

Corollary cr_istyP_up_id a xi Gamma Delta : cr_istyP id xi Gamma Delta -> cr_istyP id (upren xi) (a:: Gamma) (a.[ren xi] :: Delta).
Proof.
  replace id with (upren id) at 2 by autosubst. replace a with (a.[ren id]) at 1 by autosubst.
  apply cr_istyP_up.
Qed.

Lemma istyP_ren Gamma a rho :
  istyP Gamma a.[ren rho] -> forall Delta xi, cr_istyP rho xi Gamma Delta -> istyP Delta a.[ren xi].
Proof.
  intros H. depind H; intros Delta xi CR; destruct a; ainv.
  - apply CR; auto using istyP.
  - apply sortL_ren in H2; subst. asimpl. constructor.
    apply IHistyP with (rho0 := upren rho); try autosubst.
    rewrite (sortL_add_subst (ren rho)) at 1. rewrite (sortL_add_subst (ren xi)) at 2.
    now apply cr_istyP_up.
  - constructor; eauto. asimpl.
    apply IHistyP2 with (rho0 := upren rho); try autosubst; auto using cr_istyP_up.
Qed.

Lemma cr_istyP_shift Gamma a : cr_istyP id (+1) Gamma (a :: Gamma).
Proof. intros n H. ainv. constructor. rewrite sortL_p1. econstructor; eauto. Qed.

Lemma cr_istyP_ushift Gamma a : cr_istyP (+1) id (a :: Gamma) Gamma.
Proof. intros n H. ainv. apply sortL_ren in H1. subst. now constructor. Qed.

Theorem istyP_weaken Gamma a b : istyP Gamma a -> istyP (b :: Gamma) a.[ren (+1)].
Proof. intros H. eapply istyP_ren; eauto using cr_istyP_shift. now asimpl. Qed.

Theorem istyP_strengthen Gamma a b: istyP (b :: Gamma) a.[ren (+1)] -> istyP Gamma a.
Proof. intros H. eapply istyP_ren in H; eauto using cr_istyP_ushift. now asimpl in *. Qed.

Definition cm_istyP sigma Gamma Delta := forall x, istyP Gamma (VarL x) -> istyP Delta (sigma x).

Lemma cr_cm_istyP xi Gamma Delta : cr_istyP id xi Gamma Delta -> cm_istyP (ren xi) Gamma Delta.
Proof. intros CR x H. asimpl. eapply CR. trivial. Qed.

Lemma cm_istyP_up a sigma Gamma Delta :
  cm_istyP sigma Gamma Delta -> cm_istyP (up sigma) (a :: Gamma) (a.[sigma] :: Delta).
Proof.
  intros c [|]; ainv; atom_ren.
  - econstructor. now constructor.
  - asimpl. apply istyP_weaken. auto using istyP.
Qed.

Lemma cm_istyP_beta_type Gamma a :
  istyP Gamma a -> cm_istyP (a .: ids) ((SortL Prp) :: Gamma) Gamma.
Proof. intros H [|x] L; simpl in *; ainv; atom_ren. now constructor. Qed.

Lemma cm_istyP_beta_term Gamma a b :
  typingP Gamma a b -> istyP Gamma b -> cm_istyP (a .: ids) (b :: Gamma) Gamma.
Proof. intros H1 H2 [|x] L; simpl in *; ainv; atom_ren. now constructor. Qed.

Lemma istyP_subst a sigma Gamma Delta :
  istyP Gamma a -> cm_istyP sigma Gamma Delta -> istyP Delta a.[sigma].
Proof.
  intros H. revert sigma Delta; induction H; intros.
  - eauto using istyP.
  - constructor. eauto using (@cm_istyP_up (SortL Prp)).
  - constructor; eauto. eauto using cm_istyP_up.
Qed.

Definition cr_typingP xi Gamma Delta := forall x a, typingP Gamma (VarL x) a -> typingP Delta (VarL (xi x)) a.[ren xi].

Lemma cr_typingP_up a xi Gamma Delta :
  cr_istyP id xi Gamma Delta -> cr_typingP xi Gamma Delta -> cr_typingP (upren xi) (a :: Gamma) (a.[ren xi] :: Delta).
Proof.
  intros CR1 CR2 [|n] L; ainv; asimpl in *.
  - constructor.
    + econstructor. autosubst.
    + replace (a.[ren (xi >>> (+1))]) with (a.[ren xi].[ren (+1)]) by autosubst.
      apply istyP_strengthen in H2. apply istyP_weaken.
      eapply istyP_ren; eauto. now asimpl.
  - apply istyP_strengthen in H2.
    cut (typingP Gamma (VarL n) B); [intros J| now constructor]. aspec. ainv.
    replace (B.[ren (xi >>> (+1))]) with (B.[ren xi].[ren (+1)]) by autosubst.
    constructor; eauto using istyP_weaken. econstructor; eauto.
Qed.

Lemma typingP_ren Gamma a b :
  typingP Gamma a b -> forall Delta xi, cr_istyP id xi Gamma Delta -> cr_typingP xi Gamma Delta -> typingP Delta a.[ren xi] b.[ren xi].
Proof.
  intros H; induction H; intros Delta xi CR1 CR2; asimpl.
  - apply CR2. now constructor.
  - eapply typingP_app1; eauto. subst. autosubst.
  - constructor.
    + eapply istyP_ren; eauto. autosubst.
    + eapply IHtypingP; eauto using cr_typingP_up, cr_istyP_up_id.
  - eapply typingP_app2; eauto.
    + eapply istyP_ren; eauto. now asimpl.
    + subst. autosubst.
  - eapply typingP_lam2. rewrite (sortL_add_subst (ren xi)).
    eapply IHtypingP; eauto using cr_typingP_up, cr_istyP_up_id.
Qed.

Lemma cr_typingP_shift Gamma a : cr_typingP (+1) Gamma (a :: Gamma).
Proof.
  intros n b H. ainv. constructor.
  - econstructor; eauto.
  - now apply istyP_weaken.
Qed.

Lemma typingP_weaken Gamma a b c : typingP Gamma a b -> typingP (c :: Gamma) a.[ren (+1)] b.[ren (+1)].
Proof. intros H. eapply typingP_ren; eauto using cr_istyP_shift, cr_typingP_shift. Qed.

Definition cm_typingP sigma (Gamma Delta : list termL) :=
  forall x a, typingP Gamma (VarL x) a -> typingP Delta (sigma x) a.[sigma].

Lemma cm_typingP_up a sigma Gamma Delta :
  cm_istyP sigma Gamma Delta ->
  cm_typingP sigma Gamma Delta ->
  cm_typingP (up sigma) (a :: Gamma) (a.[sigma] :: Delta).
Proof.
  intros CM1 CM2 [|n] b H; ainv; asimpl.
  - constructor.
    + constructor; autosubst.
    + replace (a.[sigma >> ren (+1)]) with (a.[sigma].[ren (+1)]) by autosubst.
      apply istyP_weaken. eapply istyP_subst; eauto using istyP_strengthen.
  - replace (B.[sigma >> ren (+1)]) with (B.[sigma].[ren (+1)]) by autosubst.
    apply typingP_weaken, CM2. constructor; eauto using istyP_strengthen.
Qed.

Lemma typingP_subst Gamma a b:
  typingP Gamma a b ->
  forall Delta sigma,
    cm_istyP sigma Gamma Delta ->
    cm_typingP sigma Gamma Delta ->
    typingP Delta a.[sigma] b.[sigma].
Proof.
  intros H; induction H; intros Delta sigma CM1 CM2.
  - apply CM2. now constructor.
  - subst. econstructor; eauto; autosubst.
  - asimpl. constructor; eauto using istyP_subst, cm_istyP_up, cm_typingP_up.
  - subst. econstructor 4; eauto using istyP_subst. autosubst.
  - asimpl. constructor 5.
    replace (SortL Prp) with ((SortL Prp).[sigma]) by autosubst.
    eauto using cm_istyP_up, cm_typingP_up.
Qed.

Lemma cm_typingP_beta_term Gamma a b :
  typingP Gamma a b -> istyP Gamma b -> cm_typingP (a .: ids) (b :: Gamma) Gamma.
Proof.
  intros H J [|n] c K; ainv; asimpl; trivial.
  constructor; eauto using istyP_strengthen.
Qed.

Lemma cm_typingP_beta_type Gamma a :
  istyP Gamma a -> cm_typingP (a .: ids) (SortL Prp :: Gamma) Gamma.
Proof.
  intros H [|n] c K; ainv; asimpl.
  constructor; eauto using istyP_strengthen.
Qed.

Theorem typingP_beta_term Gamma a b c d:
  istyP Gamma d -> typingP Gamma c d -> typingP (d :: Gamma) a b -> typingP Gamma a.[c/] b.[c/].
Proof.
  intros. eapply typingP_subst; eauto using cm_istyP_beta_term, cm_typingP_beta_term.
Qed.

Theorem typingP_beta_type Gamma a b c:
  istyP Gamma c -> typingP ((SortL Prp) :: Gamma) a b -> typingP Gamma a.[c/] b.[c/].
Proof.
  intros. eapply typingP_subst; eauto using cm_istyP_beta_type, cm_typingP_beta_type.
Qed.

(* Propagation for P *)
Lemma typingP_istyP Gamma a b : typingP Gamma a b -> istyP Gamma b.
Proof.
  intros H. induction H.
  - trivial.
  - subst. inversion IHtypingP1; subst; ainv. eauto using istyP_subst, cm_istyP_beta_term.
  - econstructor; eauto.
  - subst. inv IHtypingP; try now asimpl. eauto using istyP_subst, cm_istyP_beta_type.
  - constructor; eauto.
Qed.

Definition gentypingP Gamma a b :=
  match b with
  | (SortL Typ) => a = (SortL Prp)
  | (SortL Prp) => istyP Gamma a
  | _ => typingP Gamma a b
  end.

Lemma gentypingP_typingP Gamma a b :
  istyP Gamma b -> (gentypingP Gamma a b <-> typingP Gamma a b).
Proof.
  unfold gentypingP.
  split; intros; destruct b; intuition; now destruct (istyP_notSort $?).
Qed.

Equivalence of L and P
Lemma typingL_typingP Gamma a b : typingL Gamma a b -> gentypingP Gamma a b.
Proof.
  induction 1; simpl in *; trivial.
  - destruct u; subst; try now constructor.
    rewrite gentypingP_typingP by assumption. now constructor.
  - destruct u; subst; now constructor.
  - pose proof (typingP_istyP $?) as I. inv I.
    + simpl in *. rewrite gentypingP_typingP;
        eauto using typingP, istyP_subst, cm_istyP_beta_type.
    + rewrite gentypingP_typingP in *;
        eauto using typingP, istyP_subst, cm_istyP_beta_term.
  - rewrite gentypingP_typingP in * by assumption.
    destruct u; subst; eauto using typingP, istyP.
Qed.

Lemma istyP_typingL Gamma a : istyP Gamma a -> typingL Gamma a (SortL Prp).
Proof. induction 1; eauto using typingL. Qed.

Lemma typingP_typingL Gamma a b : typingP Gamma a b -> typingL Gamma a b.
Proof. induction 1; eauto using istyP_typingL, typingP_istyP, typingL. Qed.

Theorem typingPL_equiv Gamma a b :
  typingP Gamma a b <-> (typingL Gamma a b /\ typingL Gamma b (SortL Prp)).
Proof.
  split.
  - eauto using typingP_typingL, typingP_istyP, istyP_typingL.
  - intros [H1 H2]. apply typingL_typingP in H1. apply typingL_typingP in H2.
    simpl in H2. now rewrite gentypingP_typingP in H1.
Qed.

Better theory for L, exploiting LP Equivalence.

Lemma typingL_sort_strengthen Gamma a b u : typingL (a :: Gamma) b.[ren (+1)] (SortL u) -> typingL Gamma b (SortL u).
Proof.
  intros H. apply typingL_typingP in H. destruct u; simpl in H.
  - apply istyP_strengthen in H. now apply istyP_typingL.
  - symmetry in H. apply sortL_ren in H. subst. constructor.
Qed.

Definition cm_typingL (sigma : var -> termL) Gamma Delta := forall x a, typingL Gamma (VarL x) a -> typingL Delta (sigma x) a.[sigma].

Lemma cm_typingL_up a u sigma Gamma Delta : cm_typingL sigma Gamma Delta -> typingL Delta a.[sigma] (SortL u) -> cm_typingL (up sigma) (a :: Gamma) (a.[sigma] :: Delta).
Proof.
  intros CM H [|n] b Ln.
  - ainv. asimpl. apply typingL_var with (u:=u).
    + constructor. autosubst.
    + rewrite (sortL_add_subst (ren (+1))). replace a.[sigma >> ren (+1)] with a.[sigma].[ren (+1)] by autosubst.
      now apply typingL_weaken.
  - ainv. asimpl. replace B.[sigma >> ren (+1)] with B.[sigma].[ren (+1)] by autosubst.
    apply typingL_weaken, CM. apply typingL_sort_strengthen in H2. econstructor; eauto.
Qed.

Lemma typingL_subst Gamma a b : typingL Gamma a b -> forall Delta sigma, cm_typingL sigma Gamma Delta -> typingL Delta a.[sigma] b.[sigma].
Proof.
  intros H; induction H; intros Delta sigma CM.
  - constructor.
  - apply CM. econstructor; eauto.
  - econstructor; eauto. rewrite (sortL_add_subst (up sigma)).
    apply IHtypingL2. eapply cm_typingL_up; eauto.
  - econstructor; eauto. subst. autosubst.
  - econstructor; eauto.
    + rewrite (sortL_add_subst (up sigma)). eapply IHtypingL2; eauto using cm_typingL_up.
    + eapply IHtypingL3; eauto using cm_typingL_up.
Qed.

Lemma cm_typingL_id Gamma : cm_typingL ids Gamma Gamma.
Proof. intros n b L. now asimpl. Qed.

Lemma cm_typingL_beta Gamma c d : typingL Gamma c d -> cm_typingL (c .: ids) (d :: Gamma) Gamma.
Proof.
  intros T [|n] b L; ainv; asimpl.
  - trivial.
  - apply typingL_sort_strengthen in H1. econstructor; eauto.
Qed.

Theorem typingL_beta Gamma a b c d:
  typingL Gamma c d -> typingL (d :: Gamma) a b -> typingL Gamma a.[c/] b.[c/].
Proof. intros T H. eapply typingL_subst; eauto using cm_typingL_beta. Qed.

Theorem typingL_propagation Gamma a b : typingL Gamma a b -> b = SortL Typ \/ exists u, typingL Gamma b (SortL u).
Proof.
  intros H; induction H; try (now left); right.
  - exists u; trivial.
  - exists Typ; constructor.
  - exists Prp. subst. destruct IHtypingL1 as [E|[u TProd]]; [discriminate E|]. ainv.
    apply (typingL_beta H0) in H5. autosubst.
  - exists Prp. econstructor; eauto.
Qed.

Theorem typingL_typ_degenerate Gamma a : typingL Gamma a (SortL Typ) -> a = (SortL Prp).
Proof.
  intros H. depind H; trivial.
  - ainv.
  - apply typingL_propagation in H. destruct H as [EX| [u TProd]]; [discriminate EX|].
    inversion TProd; subst. eapply (typingL_beta H0) in H5. rewrite <- H1 in H5. inversion H5.
Qed.

Internalising contexts


Fixpoint internL (Gamma : list termL) (a b : termL) : (termL * termL) :=
  match Gamma with
  | nil => (a,b)
  | c :: Delta => internL Delta (LamL c a) (ProdL c b)
  end.

well formed contexts for the auxiliary type system P
Inductive wfP : list termL -> Prop :=
| wfP_empty : wfP nil
| wfP_ext_prp Gamma : wfP Gamma -> wfP (SortL Prp :: Gamma)
| wfP_ext_ty Gamma a : istyP Gamma a -> wfP Gamma -> wfP (a :: Gamma).

Lemma internLP_correct Gamma a b c d: wfP Gamma -> internL Gamma a b = (c,d) -> (typingP Gamma a b <-> typingP nil c d).
Proof.
  intros H. revert a b c d. induction H; intros; simpl in *.
  - inversion H; firstorder.
  - apply IHwfP in H0. eapply iff_trans; eauto. split.
    + intros. eapply typingP_lam2; eauto.
    + intros. now inversion H1.
  - apply IHwfP in H1. eapply iff_trans; eauto. split.
    + intros. eapply typingP_lam1; eauto.
    + intros. now inversion H2.
Qed.