Library MetaCoq.PCUIC.PCUICContextConversion

Inductive context_relation (P : context → context → context_decl → context_decl → Type)
          : ∀ (Γ Γ' : context), Type :=
| ctx_rel_nil : context_relation P nil nil
| ctx_rel_vass na na' T U Γ Γ' :
    context_relation P Γ Γ' →
    P Γ Γ' (vass na T) (vass na' U) →
    context_relation P (vass na T :: Γ) (vass na' U :: Γ')
| ctx_rel_def na na' t T u U Γ Γ' :
    context_relation P Γ Γ' →
    P Γ Γ' (vdef na t T) (vdef na' u U) →
    context_relation P (vdef na t T :: Γ) (vdef na' u U :: Γ').

Lemma context_relation_nth {P n Γ Γ' d} :
  context_relation P Γ Γ' → nth_error Γ n = Some d →
  { d' & ((nth_error Γ' n = Some d') ×
          let Γs := skipn (S n) Γ in
          let Γs' := skipn (S n) Γ' in
          context_relation P Γs Γs' ×
          P Γs Γs' d d')%type }.

Lemma context_relation_trans P :
  (∀ Γ Γ' Γ'' x y z,
      context_relation P Γ Γ' →
      context_relation P Γ' Γ'' →
      context_relation P Γ Γ'' →
      P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z) →
  Transitive (context_relation P).


Lemma weakening_cumul0 `{CF:checker_flags} Σ Γ Γ'' M N n :
  wf Σ.1 → n = #|Γ''| →
  Σ ;;; Γ |- M ≤ N →
  Σ ;;; Γ ,,, Γ'' |- lift0 n M ≤ lift0 n N.


Section ContextReduction.
  Context {cf : checker_flags}.
  Context (Σ : global_env).
  Context (wfΣ : wf Σ).


  Lemma red_ctx_skip i Γ Γ' :
    red1_red_ctxP Γ Γ' →
    red1_red_ctxP (skipn i Γ) (skipn i Γ').

  Lemma All2_local_env_over_red_refl {Γ Δ} :
    All2_local_env (on_decl (fun (Δ _ : context) (t u : term) ⇒ red Σ (Γ ,,, Δ) t u)) Δ Δ.

  Lemma All2_local_env_red_refl {Δ} :
    All2_local_env (on_decl (fun (Δ _ : context) (t u : term) ⇒ red Σ Δ t u)) Δ Δ.

  Lemma red1_red_ctxP_ass {Γ Γ' Δ} : assumption_context Δ →
    red1_red_ctxP Γ Γ' →
    red1_red_ctxP (Γ ,,, Δ) (Γ' ,,, Δ).

  Lemma red1_red_ctx_aux {Γ Γ' T U} :
    red1 Σ Γ T U →
    @red_ctx Σ Γ Γ' →
    red1_red_ctxP Γ Γ' →
    ∑ t, red Σ Γ' T t × red Σ Γ' U t.

  Lemma red_red_ctx' {Γ Γ' T U} :
    red Σ Γ T U →
    @red_ctx Σ Γ Γ' →
    red1_red_ctxP Γ Γ' →
    ∑ t, red Σ Γ' T t × red Σ Γ' U t.

  Lemma red_red_ctx_aux' {Γ Γ'} :
    @red_ctx Σ Γ Γ' → red1_red_ctxP Γ Γ'.

  Lemma red_red_ctx {Γ Γ' T U} :
    red Σ Γ T U →
    @red_ctx Σ Γ Γ' →
    ∑ t, red Σ Γ' T t × red Σ Γ' U t.

End ContextReduction.

Section ContextConversion.
  Context {cf : checker_flags}.
  Context (Σ : global_env_ext).
  Context (wfΣ : wf Σ).

  Inductive conv_decls (Γ Γ' : context) : ∀ (x y : context_decl), Type :=
  | conv_vass na na' T T' :
      
      Σ ;;; Γ |- T == T' →
      conv_decls Γ Γ' (vass na T) (vass na' T')

  | conv_vdef_type na na' b T T' :
      
      Σ ;;; Γ |- T == T' →
      conv_decls Γ Γ' (vdef na b T) (vdef na' b T')

  | conv_vdef_body na na' b b' T T' :
      
      
      Σ ;;; Γ |- b == b' →
      Σ ;;; Γ |- T == T' →
      conv_decls Γ Γ' (vdef na b T) (vdef na' b' T').

  Notation conv_context Γ Γ' := (context_relation conv_decls Γ Γ').

  Lemma conv_ctx_refl Γ : conv_context Γ Γ.

  Global Instance conv_ctx_refl' : Reflexive (context_relation conv_decls)
    := conv_ctx_refl.


  Lemma fill_le {Γ t t' u u'} :
    leq_term Σ t u → red Σ Γ t t' → red Σ Γ u u' →
    ∑ t'' u'', red Σ Γ t' t'' × red Σ Γ u' u'' × leq_term Σ t'' u''.

  Lemma fill_eq {Γ t t' u u'} :
    eq_term Σ t u → red Σ Γ t t' → red Σ Γ u u' →
    ∑ t'' u'', red Σ Γ t' t'' × red Σ Γ u' u'' × eq_term Σ t'' u''.

  Lemma cumul_red_ctx Γ Γ' T U :
    Σ ;;; Γ |- T ≤ U →
    red_ctx Σ Γ Γ' →
    Σ ;;; Γ' |- T ≤ U.

  Lemma cumul_red_ctx_inv Γ Γ' T U :
    Σ ;;; Γ |- T ≤ U →
    @red_ctx Σ Γ' Γ →
    Σ ;;; Γ' |- T ≤ U.

  Lemma conv_red_ctx {Γ Γ' T U} :
    Σ ;;; Γ |- T = U →
    @red_ctx Σ Γ Γ' →
    Σ ;;; Γ' |- T = U.

  Lemma conv_red_ctx_inv {Γ Γ' T U} :
    Σ ;;; Γ |- T = U →
    @red_ctx Σ Γ' Γ →
    Σ ;;; Γ' |- T = U.


  Lemma red_eq_context_upto_l {Re Γ Δ u v}
        `{RelationClasses.Reflexive _ Re} `{RelationClasses.Transitive _ Re} `{SubstUnivPreserving Re} :
    red Σ Γ u v →
    eq_context_upto Re Γ Δ →
    ∑ v',
    red Σ Δ u v' ×
    eq_term_upto_univ Re Re v v'.

  Definition eq_universe_leq_universe' φ u u'
    := eq_universe_leq_universe φ u u'.


  Lemma cumul_trans_red_leqterm {Γ t u v} :
    Σ ;;; Γ |- t ≤ u → Σ ;;; Γ |- u ≤ v →
    ∑ l o r, red Σ Γ t l ×
             red Σ Γ u o ×
             red Σ Γ v r ×
             leq_term Σ l o × leq_term Σ o r.



  Lemma conv_alt_eq_context_upto {Γ Δ T U} :
    eq_context_upto (eq_universe Σ) Γ Δ →
    Σ ;;; Γ |- T == U →
    Σ ;;; Δ |- T == U.

  Lemma cumul_eq_context_upto {Γ Δ T U} :
    eq_context_upto (eq_universe (global_ext_constraints Σ)) Γ Δ →
    Σ ;;; Γ |- T ≤ U →
    Σ ;;; Δ |- T ≤ U.

  Lemma conv_alt_red_ctx {Γ Γ' T U} :
    Σ ;;; Γ |- T == U →
    @red_ctx Σ Γ Γ' →
    Σ ;;; Γ' |- T == U.

  Lemma conv_alt_red_ctx_inv Γ Γ' T U :
    Σ ;;; Γ |- T == U →
    red_ctx Σ Γ' Γ →
    Σ ;;; Γ' |- T == U.

  Lemma conv_context_red_context Γ Γ' :
    conv_context Γ Γ' →
    ∑ Δ Δ', red_ctx Σ Γ Δ × red_ctx Σ Γ' Δ' × eq_context_upto (eq_universe Σ) Δ Δ'.

  Lemma conv_alt_conv_ctx Γ Γ' T U :
    Σ ;;; Γ |- T == U →
    conv_context Γ Γ' →
    Σ ;;; Γ' |- T == U.

  Lemma cumul_conv_ctx Γ Γ' T U :
    Σ ;;; Γ |- T ≤ U →
    conv_context Γ Γ' →
    Σ ;;; Γ' |- T ≤ U.

  Lemma conv_conv_ctx Γ Γ' T U :
    Σ ;;; Γ |- T = U →
    conv_context Γ Γ' →
    Σ ;;; Γ' |- T = U.

  Lemma conv_isWfArity_or_Type Γ Γ' T U :
    conv_context Γ' Γ →
    Σ ;;; Γ |- T = U →
    isWfArity_or_Type Σ Γ T →
    isWfArity_or_Type Σ Γ' U.
End ContextConversion.

Notation conv_context Σ Γ Γ' := (context_relation (conv_decls Σ) Γ Γ').



Lemma conv_context_sym {cf:checker_flags} Σ Γ Γ' :
  wf Σ.1 → conv_context Σ Γ Γ' → conv_context Σ Γ' Γ.

Lemma conv_context_trans {cf:checker_flags} Σ :
  wf Σ.1 → CRelationClasses.Transitive (fun Γ Γ' ⇒ conv_context Σ Γ Γ').


Lemma context_conversion {cf:checker_flags} : env_prop
                             (fun Σ Γ t T ⇒
                                ∀ Γ', conv_context Σ Γ Γ' → wf_local Σ Γ' → Σ ;;; Γ' |- t : T).

Lemma context_conversion' {cf:checker_flags} {Σ Γ t T Γ'} :
    wf Σ.1 →
    wf_local Σ Γ' →
    Σ ;;; Γ |- t : T →
    conv_context Σ Γ Γ' →
    Σ ;;; Γ' |- t : T.

Lemma eq_context_upto_conv_context {cf:checker_flags} (Σ : global_env_ext) Re :
  RelationClasses.subrelation Re (eq_universe Σ) →
  subrelation (eq_context_upto Re) (fun Γ Γ' ⇒ conv_context Σ Γ Γ').

Lemma eq_context_upto_univ_conv_context {cf:checker_flags} Σ Γ Δ :
    eq_context_upto (eq_universe (global_ext_constraints Σ)) Γ Δ →
    conv_context Σ Γ Δ.