LogRel.GenericTyping: the generic interface of typing used to build the logical relation.

From Coq Require Import CRelationClasses ssrbool.
From LogRel.AutoSubst Require Import core unscoped Ast Extra.
From LogRel Require Import Utils BasicAst Computation Notations Closed Context NormalForms NormalEq Weakening UntypedReduction.

Section RedDefinitions.

  Context `{ta : tag}
    `{!WfContext ta} `{!WfType ta} `{!Typing ta}
    `{!ConvType ta} `{!ConvTerm ta} `{!ConvNeuConv ta}
    `{!RedType ta} `{!RedTerm ta}.

  Record TypeRedWhnf (Γ : context) (A B : term) : Type :=
    {
      tyred_whnf_red :> [ Γ |- A ⤳* B ] ;
      tyred_whnf_whnf :> whnf B
    }.

  Record TermRedWhnf (Γ : context) (A t u : term) : Type :=
    {
      tmred_whnf_red :> [ Γ |- t ⤳* u : A ] ;
      tmred_whnf_whnf :> whnf u
    }.

  Record TypeConvWf (Γ : context) (A B : term) : Type :=
    {
      tyc_wf_l : [Γ |- A] ;
      tyc_wf_r : [Γ |- B] ;
      tyc_wf_conv :> [Γ |- A ≅ B]
    }.

  Record TermConvWf (Γ : context) (A t u : term) : Type :=
    {
      tmc_wf_l : [Γ |- t : A] ;
      tmc_wf_r : [Γ |- u : A] ;
      tmc_wf_conv :> [Γ |- t ≅ u : A]
    }.

  Record TypeRedWf (Γ : context) (A B : term) : Type := {
    tyr_wf_r : [Γ |- B];
    tyr_wf_red :> [Γ |- A ⤳* B]
  }.

  Record TermRedWf (Γ : context) (A t u : term) : Type := {
    tmr_wf_r : [Γ |- u : A];
    tmr_wf_red :> [Γ |- t ⤳* u : A]
  }.

  Inductive WellSubst (Γ : context) : context -> (nat -> term) -> Type :=
    | well_sempty (σ : nat -> term) : [Γ |-s σ : ε ]
    | well_scons (σ : nat -> term) (Δ : context) A :
      [Γ |-s ↑ >> σ : Δ] -> [Γ |- σ var_zero : A[↑ >> σ]] ->
      [Γ |-s σ : Δ,, A]
  where "[ Γ '|-s' σ : Δ ]" := (WellSubst Γ Δ σ).

  Inductive ConvSubst (Γ : context) : context -> (nat -> term) -> (nat -> term) -> Type :=
  | conv_sempty (σ τ : nat -> term) : [Γ |-s σ ≅ τ : ε ]
  | conv_scons (σ τ : nat -> term) (Δ : context) A :
    [Γ |-s ↑ >> σ ≅ ↑ >> τ : Δ] -> [Γ |- σ var_zero ≅ τ var_zero: A[↑ >> σ]] ->
    [Γ |-s σ ≅ τ : Δ,, A]
  where "[ Γ '|-s' σ ≅ τ : Δ ]" := (ConvSubst Γ Δ σ τ).

  Inductive ConvCtx : context -> context -> Type :=
  | conv_cempty : [ |- ε ≅ ε]
  | conv_ccons Γ A Δ B : [ |- Γ ≅ Δ ] -> [Γ |- A ≅ B] -> [ |- Γ,, A ≅ Δ,, B]
  where "[ |- Γ ≅ Δ ]" := (ConvCtx Γ Δ).

  Lemma well_subst_ext Γ Δ (σ σ' : nat -> term) :
    σ =1 σ' ->
    [Γ |-s σ : Δ] ->
    [Γ |-s σ' : Δ].
  Proof.
    intros Heq.
    induction 1 in σ', Heq |- *.
    all: constructor.
    - eapply IHWellSubst.
      now rewrite Heq.
    - rewrite <- Heq.
      now replace A[↑ >> σ'] with A[↑ >> σ]
        by (now rewrite Heq).
  Qed.

  Record well_typed Γ t :=
  {
    well_typed_type : term ;
    well_typed_typed : [Γ |- t : well_typed_type]
  }.

  Record well_formed Γ t :=
  {
    well_formed_class : class ;
    well_formed_typed :
    match well_formed_class with
    | istype => [Γ |- t]
    | isterm A => [Γ |- t : A]
    end
  }.

  Inductive isWfFun (Γ : context) (A B : term) : term -> Set :=
    LamWfFun : forall A' t : term,
      [Γ |- A'] -> [Γ |- A ≅ A'] -> [Γ,, A |- t : B] -> [Γ,, A' |- t : B] -> isWfFun Γ A B (tLambda A' t)
  | NeWfFun : forall f : term, [Γ |- f ~ f : tProd A B] -> isWfFun Γ A B f.

  Inductive isWfPair (Γ : context) (A B : term) : term -> Set :=
    PairWfPair : forall A' B' a b : term,
      [Γ |- A'] -> [Γ |- A ≅ A'] ->
      [Γ,, A' |- B] ->
      [Γ,, A' |- B'] ->
      [Γ,, A |- B'] ->
      [Γ,, A |- B ≅ B'] ->
      [Γ,, A' |- B ≅ B'] ->
      [Γ |- a : A] ->
      [Γ |- a ≅ a : A] ->
      [Γ |- B[a..]] ->
      [Γ |- B'[a..]] ->
      [Γ |- B[a..] ≅ B'[a..]] ->
      [Γ |- b : B[a..]] ->
      [Γ |- b ≅ b : B[a..]] ->
      isWfPair Γ A B (tPair A' B' a b)
  | NeWfPair : forall n : term, [Γ |- n ~ n : tSig A B] -> isWfPair Γ A B n.

  Record EvalStep Γ t u k v := {
    evstep_eval : ∑ k', murec (eval true (tApp (erase t) (qNat u))) k' = Some (k, qNat v);
    evstep_nil : (forall k', k' < k -> [ Γ |- qRun t u k' ≅ tZero : tNat ]);
    evstep_val : [ Γ |- qRun t u k ≅ tSucc (qNat v) : tNat ];
  }.

End RedDefinitions.

Notation "[ Γ |- A ↘ B ]" := (TypeRedWhnf Γ A B) (only parsing) : typing_scope.
Notation "[ Γ |-[ ta ] A ↘ B ]" := (TypeRedWhnf (ta := ta) Γ A B) : typing_scope.
Notation "[ Γ |- t ↘ u : A ]" := (TermRedWhnf Γ A t u) (only parsing ): typing_scope.
Notation "[ Γ |-[ ta ] t ↘ u : A ]" := (TermRedWhnf (ta := ta) Γ A t u) : typing_scope.
Notation "[ Γ |- A :≅: B ]" := (TypeConvWf Γ A B) (only parsing) : typing_scope.
Notation "[ Γ |-[ ta ] A :≅: B ]" := (TypeConvWf (ta := ta) Γ A B) : typing_scope.
Notation "[ Γ |- t :≅: u : A ]" := (TermConvWf Γ A t u) (only parsing) : typing_scope.
Notation "[ Γ |-[ ta ] t :≅: u : A ]" := (TermConvWf (ta := ta) Γ A t u) : typing_scope.
Notation "[ Γ |- A :⤳*: B ]" := (TypeRedWf Γ A B) (only parsing) : typing_scope.
Notation "[ Γ |-[ ta ] A :⤳*: B ]" := (TypeRedWf (ta := ta) Γ A B) : typing_scope.
Notation "[ Γ |- t :⤳*: u : A ]" := (TermRedWf Γ A t u) (only parsing) : typing_scope.
Notation "[ Γ |-[ ta ] t :⤳*: u : A ]" := (TermRedWf (ta := ta) Γ A t u) : typing_scope.
Notation "[ Γ '|-s' σ : A ]" := (WellSubst Γ A σ) (only parsing) : typing_scope.
Notation "[ Γ |-[ ta ']s' σ : A ]" := (WellSubst (ta := ta) Γ A σ) : typing_scope.
Notation "[ Γ '|-s' σ ≅ τ : A ]" := (ConvSubst Γ A σ τ) (only parsing) : typing_scope.
Notation "[ Γ |-[ ta ']s' σ ≅ τ : A ]" := (ConvSubst (ta := ta) Γ A σ τ) : typing_scope.
Notation "[ |- Γ ≅ Δ ]" := (ConvCtx Γ Δ) (only parsing) : typing_scope.
Notation "[ |-[ ta ] Γ ≅ Δ ]" := (ConvCtx (ta := ta) Γ Δ) : typing_scope.

#[export] Hint Resolve
  Build_TypeRedWhnf Build_TermRedWhnf Build_TypeConvWf
  Build_TermConvWf Build_TypeRedWf Build_TermRedWf
  well_sempty well_scons conv_sempty conv_scons
  tyr_wf_r tyr_wf_red tmr_wf_r tmr_wf_red
  : gen_typing.

(* [export] Hint Extern 1 => match goal with | H : [ _ |- _ ▹h _ ] |- _ => destruct H | H : [ _ |- _ ↘ _ ] |- _ => destruct H | H : [ _ |- _ ↘ _ : _ ] |- _ => destruct H | H : [ _ |- _ :≅: _ ] |- _ => destruct H | H : [ _ |- _ :≅: _ : _] |- _ => destruct H | H : [ _ |- _ :⤳*: _ ] |- _ => destruct H | H : [ _ |- _ :⤳*: _ : _ ] |- _ => destruct H end : gen_typing. *)

Section GenericTyping.

  Context `{ta : tag}
    `{!WfContext ta} `{!WfType ta} `{!Typing ta} `{!ConvType ta} `{!ConvTerm ta} `{!ConvNeuConv ta}
    `{!RedType ta} `{!RedTerm ta}.

  Class WfContextProperties :=
  {
    wfc_nil : [|- ε ] ;
    wfc_cons {Γ} {A} : [|- Γ] -> [Γ |- A] -> [|- Γ,,A];
    wfc_wft {Γ A} : [Γ |- A] -> [|- Γ];
    wfc_ty {Γ A t} : [Γ |- t : A] -> [|- Γ];
    wfc_convty {Γ A B} : [Γ |- A ≅ B] -> [|- Γ];
    wfc_convtm {Γ A t u} : [Γ |- t ≅ u : A] -> [|- Γ];
    wfc_redty {Γ A B} : [Γ |- A ⤳* B] -> [|- Γ];
    wfc_redtm {Γ A t u} : [Γ |- t ⤳* u : A] -> [|- Γ];
  }.

  Class WfTypeProperties :=
  {
    wft_wk {Γ Δ A} (ρ : Δ ≤ Γ) :
      [|- Δ ] -> [Γ |- A] -> [Δ |- A⟨ρ⟩] ;
    wft_U {Γ} :
      [ |- Γ ] ->
      [ Γ |- U ] ;
    wft_prod {Γ} {A B} :
      [ Γ |- A ] ->
      [Γ ,, A |- B ] ->
      [ Γ |- tProd A B ] ;
    wft_sig {Γ} {A B} :
      [ Γ |- A ] ->
      [Γ ,, A |- B ] ->
      [ Γ |- tSig A B ] ;
    wft_Id {Γ} {A x y} :
      [Γ |- A] ->
      [Γ |- x : A] ->
      [Γ |- y : A] ->
      [Γ |- tId A x y] ;
    wft_term {Γ} {A} :
      [ Γ |- A : U ] ->
      [ Γ |- A ] ;
  }.

  Class TypingProperties :=
  {
    ty_wk {Γ Δ t A} (ρ : Δ ≤ Γ) :
      [|- Δ ] -> [Γ |- t : A] -> [Δ |- t⟨ρ⟩ : A⟨ρ⟩] ;
    ty_var {Γ} {n decl} :
      [ |- Γ ] ->
      in_ctx Γ n decl ->
      [ Γ |- tRel n : decl ] ;
    ty_prod {Γ} {A B} :
        [ Γ |- A : U] ->
        [Γ ,, A |- B : U ] ->
        [ Γ |- tProd A B : U ] ;
    ty_lam {Γ} {A B t} :
        [ Γ |- A ] ->
        [ Γ ,, A |- t : B ] ->
        [ Γ |- tLambda A t : tProd A B] ;
    ty_app {Γ} {f a A B} :
        [ Γ |- f : tProd A B ] ->
        [ Γ |- a : A ] ->
        [ Γ |- tApp f a : B[a ..] ] ;
    ty_nat {Γ} :
        [|-Γ] ->
        [Γ |- tNat : U] ;
    ty_zero {Γ} :
        [|-Γ] ->
        [Γ |- tZero : tNat] ;
    ty_succ {Γ n} :
        [Γ |- n : tNat] ->
        [Γ |- tSucc n : tNat] ;
    ty_natElim {Γ P hz hs n} :
      [Γ ,, tNat |- P ] ->
      [Γ |- hz : P[tZero..]] ->
      [Γ |- hs : elimSuccHypTy P] ->
      [Γ |- n : tNat] ->
      [Γ |- tNatElim P hz hs n : P[n..]] ;
    ty_empty {Γ} :
        [|-Γ] ->
        [Γ |- tEmpty : U] ;
    ty_emptyElim {Γ P e} :
      [Γ ,, tEmpty |- P ] ->
      [Γ |- e : tEmpty] ->
      [Γ |- tEmptyElim P e : P[e..]] ;
    ty_sig {Γ} {A B} :
        [ Γ |- A : U] ->
        [Γ ,, A |- B : U ] ->
        [ Γ |- tSig A B : U ] ;
    ty_pair {Γ} {A B a b} :
        [ Γ |- A ] ->
        [Γ ,, A |- B ] ->
        [Γ |- a : A] ->
        [Γ |- b : B[a..]] ->
        [Γ |- tPair A B a b : tSig A B] ;
    ty_fst {Γ A B p} :
        [Γ |- p : tSig A B] ->
        [Γ |- tFst p : A] ;
    ty_snd {Γ A B p} :
        [Γ |- p : tSig A B] ->
        [Γ |- tSnd p : B[(tFst p)..]] ;
    ty_Id {Γ} {A x y} :
      [Γ |- A : U] ->
      [Γ |- x : A] ->
      [Γ |- y : A] ->
      [Γ |- tId A x y : U] ;
    ty_refl {Γ A x} :
      [Γ |- A] ->
      [Γ |- x : A] ->
      [Γ |- tRefl A x : tId A x x] ;
    ty_IdElim {Γ A x P hr y e} :
      [Γ |- A] ->
      [Γ |- x : A] ->
      [Γ ,, A ,, tId A⟨@wk1 Γ A⟩ x⟨@wk1 Γ A⟩ (tRel 0) |- P] ->
      [Γ |- hr : P[tRefl A x .: x..]] ->
      [Γ |- y : A] ->
      [Γ |- e : tId A x y] ->
      [Γ |- tIdElim A x P hr y e : P[e .: y..]];
    ty_quote {Γ} {t} :
      [ Γ |- t ≅ t : arr tNat tNat ] ->
      [ Γ |- tQuote t : tNat ];
    ty_step {Γ} {t u} :
      [ Γ |- t ≅ t : arr tNat tNat ] ->
      [ Γ |- u ≅ u : tNat ] ->
      [ Γ |- run : arr tNat (arr tNat tPNat) ] ->
      [ Γ |- tStep t u : tNat ];
    ty_reflect {Γ} {t t' u u'} :
      [ Γ |- t ≅ t' : arr tNat tNat ] ->
      [ Γ |- u ≅ u' : tNat ] ->
      [ Γ |- run : arr tNat (arr tNat tPNat) ] ->
      [ Γ |- tReflect t u : tTotal t' u' ];
    ty_exp {Γ t A A'} : [Γ |- t : A'] -> [Γ |- A ⤳* A'] -> [Γ |- t : A] ;
    ty_conv {Γ t A A'} : [Γ |- t : A'] -> [Γ |- A' ≅ A] -> [Γ |- t : A] ;
  }.

  Class ConvTypeProperties :=
  {
    convty_term {Γ A B} : [Γ |- A ≅ B : U] -> [Γ |- A ≅ B] ;
    convty_equiv {Γ} :> PER (conv_type Γ) ;
    convty_wk {Γ Δ A B} (ρ : Δ ≤ Γ) :
      [|- Δ ] -> [Γ |- A ≅ B] -> [Δ |- A⟨ρ⟩ ≅ B⟨ρ⟩] ;
    convty_exp {Γ A A' B B'} :
      [Γ |- A ⤳* A'] -> [Γ |- B ⤳* B'] ->
      [Γ |- A' ≅ B'] -> [Γ |- A ≅ B] ;
    convty_uni {Γ} :
      [|- Γ] -> [Γ |- U ≅ U] ;
    convty_prod {Γ A A' B B'} :
      [Γ |- A] ->
      [Γ |- A ≅ A'] -> [Γ,, A |- B ≅ B'] ->
      [Γ |- tProd A B ≅ tProd A' B'] ;
    convty_sig {Γ A A' B B'} :
      [Γ |- A] ->
      [Γ |- A ≅ A'] -> [Γ,, A |- B ≅ B'] ->
      [Γ |- tSig A B ≅ tSig A' B'] ;
    convty_Id {Γ A A' x x' y y'} :
      (* Γ |- A -> ?  *)
      [Γ |- A ≅ A'] ->
      [Γ |- x ≅ x' : A] ->
      [Γ |- y ≅ y' : A] ->
      [Γ |- tId A x y ≅ tId A' x' y' ] ;
  }.

  Class ConvTermProperties :=
  {
    convtm_equiv {Γ A} :> PER (conv_term Γ A) ;
    convtm_conv {Γ t u A A'} : [Γ |- t ≅ u : A] -> [Γ |- A ≅ A'] -> [Γ |- t ≅ u : A'] ;
    convtm_wk {Γ Δ t u A} (ρ : Δ ≤ Γ) :
      [|- Δ ] -> [Γ |- t ≅ u : A] -> [Δ |- t⟨ρ⟩ ≅ u⟨ρ⟩ : A⟨ρ⟩] ;
    convtm_exp {Γ A t t' u u'} :
      [Γ |- t ⤳* t' : A] -> [Γ |- u ⤳* u' : A] ->
      [Γ |- A] -> [Γ |- t' : A] -> [Γ |- u' : A] ->
      [Γ |- A ≅ A] -> [Γ |- t' ≅ u' : A] -> [Γ |- t ≅ u : A] ;
    convtm_convneu {Γ n n' A} :
      [Γ |- n ~ n' : A] -> [Γ |- n ≅ n' : A] ;
    convtm_prod {Γ A A' B B'} :
      [Γ |- A : U] ->
      [Γ |- A ≅ A' : U] -> [Γ,, A |- B ≅ B' : U] ->
      [Γ |- tProd A B ≅ tProd A' B' : U] ;
    convtm_sig {Γ A A' B B'} :
      [Γ |- A : U] ->
      [Γ |- A ≅ A' : U] -> [Γ,, A |- B ≅ B' : U] ->
      [Γ |- tSig A B ≅ tSig A' B' : U] ;
    convtm_lam {Γ A B t t'} :
      [Γ |- A] ->
      [Γ |- A ≅ A] ->
      [Γ,, A |- t ≅ t' : B] ->
      [Γ |- tLambda A t ≅ tLambda A t' : tProd A B];
    convtm_eta {Γ f g A B} :
      [ Γ |- A ] ->
      [ Γ,, A |- B ] ->
      [ Γ |- f : tProd A B ] ->
      isWfFun Γ A B f ->
      [ Γ |- g : tProd A B ] ->
      isWfFun Γ A B g ->
      [ Γ ,, A |- eta_expand f ≅ eta_expand g : B ] ->
      [ Γ |- f ≅ g : tProd A B ] ;
    convtm_nat {Γ} :
      [|-Γ] -> [Γ |- tNat ≅ tNat : U] ;
    convtm_zero {Γ} :
      [|-Γ] -> [Γ |- tZero ≅ tZero : tNat] ;
    convtm_succ {Γ} {n n'} :
        [Γ |- n ≅ n' : tNat] ->
        [Γ |- tSucc n ≅ tSucc n' : tNat] ;
    convtm_eta_sig {Γ p p' A B} :
      [Γ |- A] ->
      [Γ ,, A |- B] ->
      [Γ |- p : tSig A B] ->
      isWfPair Γ A B p ->
      [Γ |- p' : tSig A B] ->
      isWfPair Γ A B p' ->
      [Γ |- tFst p ≅ tFst p' : A] ->
      [Γ |- tSnd p ≅ tSnd p' : B[(tFst p)..]] ->
      [Γ |- p ≅ p' : tSig A B] ;
    convtm_empty {Γ} :
      [|-Γ] -> [Γ |- tEmpty ≅ tEmpty : U] ;
    convtm_Id {Γ A A' x x' y y'} :
      (* Γ |- A -> ?  *)
      [Γ |- A ≅ A' : U] ->
      [Γ |- x ≅ x' : A] ->
      [Γ |- y ≅ y' : A] ->
      [Γ |- tId A x y ≅ tId A' x' y' : U ] ;
    convtm_refl {Γ A A' x x'} :
      [Γ |- A ≅ A'] ->
      [Γ |- x ≅ x' : A] ->
      [Γ |- tRefl A x ≅ tRefl A' x' : tId A x x] ;
  }.

  Class ConvNeuProperties :=
  {
    convneu_equiv {Γ A} :> PER (conv_neu_conv Γ A) ;
    convneu_conv {Γ t u A A'} : [Γ |- t ~ u : A] -> [Γ |- A ≅ A'] -> [Γ |- t ~ u : A'] ;
    convneu_wk {Γ Δ t u A} (ρ : Δ ≤ Γ) :
      [|- Δ ] -> [Γ |- t ~ u : A] -> [Δ |- t⟨ρ⟩ ~ u⟨ρ⟩ : A⟨ρ⟩] ;
    convneu_whne {Γ A t u} : [Γ |- t ~ u : A] -> whne t;
    convneu_var {Γ n A} :
      [Γ |- tRel n : A] -> [Γ |- tRel n ~ tRel n : A] ;
    convneu_app {Γ f g t u A B} :
      [ Γ |- f ~ g : tProd A B ] ->
      [ Γ |- t ≅ u : A ] ->
      [ Γ |- tApp f t ~ tApp g u : B[t..] ] ;
    convneu_natElim {Γ P P' hz hz' hs hs' n n'} :
        [Γ ,, tNat |- P ≅ P'] ->
        [Γ |- hz ≅ hz' : P[tZero..]] ->
        [Γ |- hs ≅ hs' : elimSuccHypTy P] ->
        [Γ |- n ~ n' : tNat] ->
        [Γ |- tNatElim P hz hs n ~ tNatElim P' hz' hs' n' : P[n..]] ;
    convneu_emptyElim {Γ P P' e e'} :
        [Γ ,, tEmpty |- P ≅ P'] ->
        [Γ |- e ~ e' : tEmpty] ->
        [Γ |- tEmptyElim P e ~ tEmptyElim P' e' : P[e..]] ;
    convneu_fst {Γ A B p p'} :
      [Γ |- p ~ p' : tSig A B] ->
      [Γ |- tFst p ~ tFst p' : A] ;
    convneu_snd {Γ A B p p'} :
      [Γ |- p ~ p' : tSig A B] ->
      [Γ |- tSnd p ~ tSnd p' : B[(tFst p)..]] ;
    convneu_IdElim {Γ A A' x x' P P' hr hr' y y' e e'} :
      (* Parameters well formed: required by declarative instance *)
      [Γ |- A] ->
      [Γ |- x : A] ->
      [Γ |- A ≅ A'] ->
      [Γ |- x ≅ x' : A] ->
      [Γ ,, A ,, tId A⟨@wk1 Γ A⟩ x⟨@wk1 Γ A⟩ (tRel 0) |- P ≅ P'] ->
      [Γ |- hr ≅ hr' : P[tRefl A x .: x..]] ->
      [Γ |- y ≅ y' : A] ->
      [Γ |- e ~ e' : tId A x y] ->
      [Γ |- tIdElim A x P hr y e ~ tIdElim A' x' P' hr' y' e' : P[e .: y..]];
    convneu_quote {Γ n n'} :
        [Γ |- n ≅ n' : arr tNat tNat] ->
        dnf n -> dnf n' ->
        ~ closed0 n -> ~ closed0 n' ->
        [Γ |- tQuote n ~ tQuote n' : tNat];
    convneu_step {Γ t t' t₀ u u' u₀} :
      [Γ |- t ≅ t' : arr tNat tNat] ->
      [Γ |- u ≅ u' : tNat] ->
      [Γ |- t ≅ t₀ : arr tNat tNat] ->
      [Γ |- u ≅ u₀ : tNat] ->
      [Γ |- run : arr tNat (arr tNat tPNat)] ->
      dnf t -> dnf t' -> dnf u -> dnf u' ->
      (~ is_closedn 0 t) + (~ is_closedn 0 u) -> (~ is_closedn 0 t') + (~ is_closedn 0 u') ->
      [Γ |- tStep t u ~ tStep t' u' : tNat];
    convneu_reflect {Γ t t' t₀ u u' u₀} :
      [Γ |- t ≅ t' : arr tNat tNat] ->
      [Γ |- u ≅ u' : tNat] ->
      [Γ |- t ≅ t₀ : arr tNat tNat] ->
      [Γ |- u ≅ u₀ : tNat] ->
      [Γ |- run : arr tNat (arr tNat tPNat)] ->
      dnf t -> dnf t' -> dnf u -> dnf u' ->
      (~ is_closedn 0 t) + (~ is_closedn 0 u) -> (~ is_closedn 0 t') + (~ is_closedn 0 u') ->
      [Γ |- tReflect t u ~ tReflect t' u' : tTotal t₀ u₀];
  }.

  Class RedTypeProperties :=
  {
    redty_wk {Γ Δ A B} (ρ : Δ ≤ Γ) :
      [|- Δ ] -> [Γ |- A ⤳* B] -> [Δ |- A⟨ρ⟩ ⤳* B⟨ρ⟩] ;
    redty_sound {Γ A B} : [Γ |- A ⤳* B] -> [A ⤳* B] ;
    redty_ty_src {Γ A B} : [Γ |- A ⤳* B] -> [Γ |- A] ;
    redty_term {Γ A B} :
      [ Γ |- A ⤳* B : U] -> [Γ |- A ⤳* B ] ;
    redty_refl {Γ A} :
      [ Γ |- A] ->
      [Γ |- A ⤳* A] ;
    redty_trans {Γ} :>
      Transitive (red_ty Γ) ;
  }.

  Class RedTermProperties :=
  {
    redtm_wk {Γ Δ t u A} (ρ : Δ ≤ Γ) :
      [|- Δ ] -> [Γ |- t ⤳* u : A] -> [Δ |- t⟨ρ⟩ ⤳* u⟨ρ⟩ : A⟨ρ⟩] ;
    redtm_sound {Γ A t u} : [Γ |- t ⤳* u : A] -> [t ⤳* u] ;
    redtm_ty_src {Γ A t u} : [Γ |- t ⤳* u : A] -> [Γ |- t : A] ;
    redtm_beta {Γ A B t u} :
      [ Γ |- A ] ->
      [ Γ ,, A |- t : B ] ->
      [ Γ |- u : A ] ->
      [ Γ |- tApp (tLambda A t) u ⤳* t[u..] : B[u..] ] ;
    redtm_natElimZero {Γ P hz hs} :
        [Γ ,, tNat |- P ] ->
        [Γ |- hz : P[tZero..]] ->
        [Γ |- hs : elimSuccHypTy P] ->
        [Γ |- tNatElim P hz hs tZero ⤳* hz : P[tZero..]] ;
    redtm_natElimSucc {Γ P hz hs n} :
        [Γ ,, tNat |- P ] ->
        [Γ |- hz : P[tZero..]] ->
        [Γ |- hs : elimSuccHypTy P] ->
        [Γ |- n : tNat] ->
        [Γ |- tNatElim P hz hs (tSucc n) ⤳* tApp (tApp hs n) (tNatElim P hz hs n) : P[(tSucc n)..]] ;
    redtm_app {Γ A B f f' t} :
      [ Γ |- f ⤳* f' : tProd A B ] ->
      [ Γ |- t : A ] ->
      [ Γ |- tApp f t ⤳* tApp f' t : B[t..] ];
    redtm_natelim {Γ P hz hs n n'} :
      [ Γ,, tNat |- P ] ->
      [ Γ |- hz : P[tZero..] ] ->
      [ Γ |- hs : elimSuccHypTy P ] ->
      [ Γ |- n ⤳* n' : tNat ] ->
      [ Γ |- tNatElim P hz hs n ⤳* tNatElim P hz hs n' : P[n..] ];
    redtm_emptyelim {Γ P n n'} :
      [ Γ,, tEmpty |- P ] ->
      [ Γ |- n ⤳* n' : tEmpty ] ->
      [ Γ |- tEmptyElim P n ⤳* tEmptyElim P n' : P[n..] ];
    redtm_fst_beta {Γ A B a b} :
      [Γ |- A] ->
      [Γ ,, A |- B] ->
      [Γ |- a : A] ->
      [Γ |- b : B[a..]] ->
      [Γ |- tFst (tPair A B a b) ⤳* a : A] ;
    redtm_fst {Γ A B p p'} :
      [Γ |- p ⤳* p' : tSig A B] ->
      [Γ |- tFst p ⤳* tFst p' : A] ;
    redtm_snd_beta {Γ A B a b} :
      [Γ |- A] ->
      [Γ ,, A |- B] ->
      [Γ |- a : A] ->
      [Γ |- b : B[a..]] ->
      [Γ |- tSnd (tPair A B a b) ⤳* b : B[(tFst (tPair A B a b))..]] ;
    redtm_snd {Γ A B p p'} :
      [Γ |- p ⤳* p' : tSig A B] ->
      [Γ |- tSnd p ⤳* tSnd p' : B[(tFst p)..]] ;
    redtm_idElimRefl {Γ A x P hr y A' z} :
      [Γ |- A] ->
      [Γ |- x : A] ->
      [Γ ,, A ,, tId A⟨@wk1 Γ A⟩ x⟨@wk1 Γ A⟩ (tRel 0) |- P] ->
      [Γ |- hr : P[tRefl A x .: x..]] ->
      [Γ |- y : A] ->
      [Γ |- A'] ->
      [Γ |- z : A] ->
      [Γ |- A ≅ A'] ->
      [Γ |- x ≅ y : A] ->
      [Γ |- x ≅ z : A] ->
      [Γ |- tIdElim A x P hr y (tRefl A' z) ⤳* hr : P[tRefl A' z .: y..]];
    redtm_idElim {Γ A x P hr y e e'} :
      [Γ |- A] ->
      [Γ |- x : A] ->
      [Γ ,, A ,, tId A⟨@wk1 Γ A⟩ x⟨@wk1 Γ A⟩ (tRel 0) |- P] ->
      [Γ |- hr : P[tRefl A x .: x..]] ->
      [Γ |- y : A] ->
      [Γ |- e ⤳* e' : tId A x y] ->
      [Γ |- tIdElim A x P hr y e ⤳* tIdElim A x P hr y e' : P[e .: y..]];
    redtm_evalquote {Γ t} :
      [Γ |- t ≅ t : arr tNat tNat] -> dnf t -> closed0 t ->
      [Γ |- tQuote t ⤳* qNat (quote (erase t)) : tNat];
    redtm_quote {Γ t t'} :
      [Γ |- t ≅ t' : arr tNat tNat] ->
      [ t ⇶* t' ] ->
      [Γ |- tQuote t ⤳* tQuote t' : tNat ];
    redtm_evalstep {Γ t u k n} :
      [Γ |- t ≅ t : arr tNat tNat] ->
      [Γ |- run : arr tNat (arr tNat tPNat)] ->
      dnf t -> closed0 t ->
      EvalStep Γ t u k n ->
      [Γ |- tStep t (qNat u) ⤳* qNat k : tNat ];
    redtm_step {Γ t t' u u'} :
      [Γ |- t ≅ t' : arr tNat tNat] ->
      [Γ |- u ≅ u' : tNat] ->
      [Γ |- run : arr tNat (arr tNat tPNat)] ->
      [ t ⇶* t' ] ->
      [ u ⇶* u' ] ->
      dnf t' -> dnf u' ->
      [Γ |- tStep t u ⤳* tStep t' u' : tNat ];
    redtm_evalreflect {Γ t t₀ u k n} :
      [Γ |- t ≅ t₀ : arr tNat tNat] ->
      [Γ |- run : arr tNat (arr tNat tPNat)] ->
      dnf t₀ -> closed0 t₀ ->
      EvalStep Γ t₀ u k n ->
      [Γ |- tReflect t₀ (qNat u) ⤳* qEvalTm k n : tTotal t (qNat u) ];
    redtm_reflect {Γ t t' u u'} :
      [Γ |- t ≅ t' : arr tNat tNat] ->
      [Γ |- u ≅ u' : tNat] ->
      [Γ |- run : arr tNat (arr tNat tPNat)] ->
      [ t ⇶* t' ] ->
      [ u ⇶* u' ] ->
      dnf t' -> dnf u' ->
      [Γ |- tReflect t u ⤳* tReflect t' u' : tTotal t u ];
    redtm_conv {Γ t u A A'} :
      [Γ |- t ⤳* u : A] ->
      [Γ |- A ≅ A'] ->
      [Γ |- t ⤳* u : A'] ;
    redtm_refl {Γ A t } :
      [ Γ |- t : A] ->
      [Γ |- t ⤳* t : A] ;
    redtm_trans {Γ A} :>
      Transitive (red_tm Γ A) ;
  }.

End GenericTyping.