Library MetaCoq.PCUIC.PCUICSafeLemmata

Notation "( x ; y )" := (existT _ x y).


Definition nodelta_flags := RedFlags.mk true true true false true true.

Inductive dlexprod {A} {B : A → Type}
          (leA : A → A → Prop) (leB : ∀ x, B x → B x → Prop)
  : sigT B → sigT B → Prop :=
| left_lex :
    ∀ x x' y y',
      leA x x' →
      dlexprod leA leB (x;y) (x';y')

| right_lex :
    ∀ x y y',
      leB x y y' →
      dlexprod leA leB (x;y) (x;y').


Definition lexprod := Subterm.lexprod.

Inductive dlexmod {A} {B : A → Type}
    (leA : A → A → Prop)
    (eA : A → A → Prop)
    (coe : ∀ x x', eA x x' → B x → B x')
    (leB : ∀ x, B x → B x → Prop)
  : sigT B → sigT B → Prop :=
| left_dlexmod :
    ∀ x x' y y',
      leA x x' →
      dlexmod leA eA coe leB (x;y) (x';y')

| right_dlexmod :
    ∀ x x' y y' (e : eA x x'),
      leB x' (coe _ _ e y) y' →
      dlexmod leA eA coe leB (x;y) (x';y').

Notation "x ⊩ R1 ⨶ R2" :=
  (dlexprod R1 (fun x ⇒ R2)) (at level 20, right associativity).
Notation "R1 ⊗ R2" :=
  (lexprod R1 R2) (at level 20, right associativity).

Notation "x ⊨ e \ R1 'by' coe ⨷ R2" :=
  (dlexmod R1 e coe (fun x ⇒ R2)) (at level 20, right associativity).

Lemma acc_dlexprod :
  ∀ A B leA leB,
    (∀ x, well_founded (leB x)) →
    ∀ x,
      Acc leA x →
      ∀ y,
        Acc (leB x) y →
        Acc (@dlexprod A B leA leB) (x;y).

Lemma dlexprod_Acc :
  ∀ A B leA leB,
    (∀ x, well_founded (leB x)) →
    ∀ x y,
      Acc leA x →
      Acc (@dlexprod A B leA leB) (x;y).

Lemma dlexprod_trans :
  ∀ A B RA RB,
    transitive RA →
    (∀ x, transitive (RB x)) →
    transitive (@dlexprod A B RA RB).


Lemma acc_dlexmod :
  ∀ A B (leA : A → A → Prop) (eA : A → A → Prop)
        (coe : ∀ x x', eA x x' → B x → B x')
        (leB : ∀ x : A, B x → B x → Prop)
        (sym : ∀ x y, eA x y → eA y x)
        (trans : ∀ x y z, eA x y → eA y z → eA x z),
    (∀ x, well_founded (leB x)) →
    (∀ x x' y, eA x x' → leA y x' → leA y x) →
    (∀ x, ∃ e : eA x x, ∀ y, coe _ _ e y = y) →
    (∀ x x' y e, coe x x' (sym _ _ e) (coe _ _ e y) = y) →
    (∀ x0 x1 x2 e1 e2 y,
      coe _ _ (trans x0 x1 x2 e1 e2) y =
      coe _ _ e2 (coe _ _ e1 y)
    ) →
    (∀ x x' e y y',
      leB _ y (coe x x' e y') →
      leB _ (coe _ _ (sym _ _ e) y) y'
    ) →
    ∀ x,
      Acc leA x →
      ∀ y,
        Acc (leB x) y →
        ∀ x' (e : eA x x'),
          Acc (@dlexmod A B leA eA coe leB) (x'; coe _ _ e y).

Lemma dlexmod_Acc :
  ∀ A B (leA : A → A → Prop) (eA : A → A → Prop)
    (coe : ∀ x x', eA x x' → B x → B x')
    (leB : ∀ x : A, B x → B x → Prop)
    (sym : ∀ x y, eA x y → eA y x)
    (trans : ∀ x y z, eA x y → eA y z → eA x z),
    (∀ x, well_founded (leB x)) →
    (∀ x x' y, eA x x' → leA y x' → leA y x) →
    (∀ x, ∃ e : eA x x, ∀ y, coe _ _ e y = y) →
    (∀ x x' y e, coe x x' (sym _ _ e) (coe _ _ e y) = y) →
    (∀ x0 x1 x2 e1 e2 y,
      coe _ _ (trans x0 x1 x2 e1 e2) y =
      coe _ _ e2 (coe _ _ e1 y)
    ) →
    (∀ x x' e y y',
      leB _ y (coe x x' e y') →
      leB _ (coe _ _ (sym _ _ e) y) y'
    ) →
    ∀ x y,
      Acc leA x →
      Acc (@dlexmod A B leA eA coe leB) (x ; y).

Section Lemmata.
  Context {cf : checker_flags}.
  Context (flags : RedFlags.t).

  Lemma eq_term_zipc_inv :
    ∀ φ u v π,
      eq_term φ (zipc u π) (zipc v π) →
      eq_term φ u v.

  Lemma eq_term_zipx_inv :
    ∀ φ Γ u v π,
      eq_term φ (zipx Γ u π) (zipx Γ v π) →
      eq_term φ u v.

  Lemma eq_term_upto_univ_zipc :
    ∀ Re u v π,
      RelationClasses.Reflexive Re →
      eq_term_upto_univ Re Re u v →
      eq_term_upto_univ Re Re (zipc u π) (zipc v π).

  Lemma eq_term_zipc :
    ∀ (Σ : global_env_ext) u v π,
      eq_term (global_ext_constraints Σ) u v →
      eq_term (global_ext_constraints Σ) (zipc u π) (zipc v π).

  Lemma eq_term_upto_univ_zipp :
    ∀ Re u v π,
      RelationClasses.Reflexive Re →
      eq_term_upto_univ Re Re u v →
      eq_term_upto_univ Re Re (zipp u π) (zipp v π).

  Lemma eq_term_zipp :
    ∀ (Σ : global_env_ext) u v π,
      eq_term (global_ext_constraints Σ) u v →
      eq_term (global_ext_constraints Σ) (zipp u π) (zipp v π).

  Lemma eq_term_upto_univ_zipx :
    ∀ Re Γ u v π,
      RelationClasses.Reflexive Re →
      eq_term_upto_univ Re Re u v →
      eq_term_upto_univ Re Re (zipx Γ u π) (zipx Γ v π).

  Lemma eq_term_zipx :
    ∀ φ Γ u v π,
      eq_term φ u v →
      eq_term φ (zipx Γ u π) (zipx Γ v π).

  Inductive cored Σ Γ: term → term → Prop :=
  | cored1 : ∀ u v, red1 Σ Γ u v → cored Σ Γ v u
  | cored_trans : ∀ u v w, cored Σ Γ v u → red1 Σ Γ v w → cored Σ Γ w u.



  Lemma lookup_env_ConstantDecl_inv :
    ∀ Σ k k' ty bo uni,
      Some (ConstantDecl k' {| cst_type := ty ; cst_body := bo; cst_universes := uni |})
      = lookup_env Σ k →
      k = k'.

  Lemma fresh_global_nl :
    ∀ Σ k,
      fresh_global k Σ →
      fresh_global k (map nl_global_decl Σ).


  Context (Σ : global_env_ext).

  Inductive welltyped Σ Γ t : Prop :=
  | iswelltyped A : Σ ;;; Γ |- t : A → welltyped Σ Γ t.


  Definition wellformed Σ Γ t :=
    welltyped Σ Γ t ∨ ∥ isWfArity typing Σ Γ t ∥.


  Lemma wellformed_irr :
    ∀ {Σ Γ t} (h1 h2 : wellformed Σ Γ t), h1 = h2.

  Context (hΣ : ∥ wf Σ ∥).

  Lemma welltyped_alpha Γ u v :
      welltyped Σ Γ u →
      eq_term_upto_univ eq eq u v →
      welltyped Σ Γ v.

  Lemma wellformed_alpha Γ u v :
      wellformed Σ Γ u →
      eq_term_upto_univ eq eq u v →
      wellformed Σ Γ v.

  Lemma wellformed_nlctx Γ u :
      wellformed Σ Γ u →
      wellformed Σ (nlctx Γ) u.

  Lemma red_cored_or_eq :
    ∀ Γ u v,
      red Σ Γ u v →
      cored Σ Γ v u ∨ u = v.

  Lemma cored_it_mkLambda_or_LetIn :
    ∀ Γ Δ u v,
      cored Σ (Γ ,,, Δ) u v →
      cored Σ Γ (it_mkLambda_or_LetIn Δ u)
               (it_mkLambda_or_LetIn Δ v).

  Lemma cored_welltyped :
    ∀ {Γ u v},
      welltyped Σ Γ u →
      cored (fst Σ) Γ v u →
      welltyped Σ Γ v.

  Lemma cored_trans' :
    ∀ {Γ u v w},
      cored Σ Γ u v →
      cored Σ Γ v w →
      cored Σ Γ u w.

  Lemma cored_red_trans :
    ∀ Γ u v w,
      red Σ Γ u v →
      red1 Σ Γ v w →
      cored Σ Γ w u.

  Lemma cored_case :
    ∀ Γ ind p c c' brs,
      cored Σ Γ c c' →
      cored Σ Γ (tCase ind p c brs) (tCase ind p c' brs).

  Lemma welltyped_context :
    ∀ Γ t,
      welltyped Σ Γ (zip t) →
      welltyped Σ (Γ ,,, stack_context (snd t)) (fst t).

  Lemma wellformed_context :
    ∀ Γ t,
      wellformed Σ Γ (zip t) →
      wellformed Σ (Γ ,,, stack_context (snd t)) (fst t).

  Lemma cored_red :
    ∀ Γ u v,
      cored Σ Γ v u →
      ∥ red Σ Γ u v ∥.

  Lemma cored_context :
    ∀ Γ t u π,
      cored Σ (Γ ,,, stack_context π) t u →
      cored Σ Γ (zip (t, π)) (zip (u, π)).

  Lemma cored_zipx :
    ∀ Γ u v π,
      cored Σ (Γ ,,, stack_context π) u v →
      cored Σ [] (zipx Γ u π) (zipx Γ v π).

  Lemma red_zipx :
    ∀ Γ u v π,
      red Σ (Γ ,,, stack_context π) u v →
      red Σ [] (zipx Γ u π) (zipx Γ v π).

  Lemma cumul_zippx :
    ∀ Γ u v ρ,
      Σ ;;; (Γ ,,, stack_context ρ) |- u ≤ v →
      Σ ;;; Γ |- zippx u ρ ≤ zippx v ρ.

  Lemma conv_LetIn_bo :
    ∀ Γ na ty t u u',
      Σ ;;; Γ ,, vdef na ty t |- u == u' →
      Σ ;;; Γ |- tLetIn na ty t u == tLetIn na ty t u'.

  Lemma conv_alt_it_mkLambda_or_LetIn :
    ∀ Δ Γ u v,
      Σ ;;; (Δ ,,, Γ) |- u == v →
      Σ ;;; Δ |- it_mkLambda_or_LetIn Γ u == it_mkLambda_or_LetIn Γ v.

  Lemma conv_alt_it_mkProd_or_LetIn :
    ∀ Δ Γ B B',
      Σ ;;; (Δ ,,, Γ) |- B == B' →
      Σ ;;; Δ |- it_mkProd_or_LetIn Γ B == it_mkProd_or_LetIn Γ B'.

  Lemma conv_zipp :
    ∀ Γ u v ρ,
      Σ ;;; Γ |- u == v →
      Σ ;;; Γ |- zipp u ρ == zipp v ρ.

  Lemma cumul_zipp :
    ∀ Γ u v π,
      Σ ;;; Γ |- u ≤ v →
      Σ ;;; Γ |- zipp u π ≤ zipp v π.

  Lemma conv_zipp' :
    ∀ leq Γ u v π,
      conv leq Σ Γ u v →
      conv leq Σ Γ (zipp u π) (zipp v π).

  Lemma conv_alt_zippx :
    ∀ Γ u v ρ,
      Σ ;;; (Γ ,,, stack_context ρ) |- u == v →
      Σ ;;; Γ |- zippx u ρ == zippx v ρ.

  Lemma conv_zippx :
    ∀ Γ u v ρ,
      Σ ;;; Γ ,,, stack_context ρ |- u == v →
      Σ ;;; Γ |- zippx u ρ == zippx v ρ.

  Lemma conv_zippx' :
    ∀ Γ leq u v ρ,
      conv leq Σ (Γ ,,, stack_context ρ) u v →
      conv leq Σ Γ (zippx u ρ) (zippx v ρ).

  Lemma cored_nl :
    ∀ Γ u v,
      cored Σ Γ u v →
      cored Σ (nlctx Γ) (nl u) (nl v).


  Lemma wf_fun :
    ∀ A (R : A → A → Prop) B (f : B → A),
      well_founded R →
      well_founded (fun x y ⇒ R (f x) (f y)).

  Lemma Acc_fun :
    ∀ A (R : A → A → Prop) B (f : B → A) x,
      Acc R (f x) →
      Acc (fun x y ⇒ R (f x) (f y)) x.

  Lemma welltyped_it_mkLambda_or_LetIn :
    ∀ Γ Δ t,
      welltyped Σ Γ (it_mkLambda_or_LetIn Δ t) →
      welltyped Σ (Γ ,,, Δ) t.

  Lemma it_mkLambda_or_LetIn_welltyped :
    ∀ Γ Δ t,
      welltyped Σ (Γ ,,, Δ) t →
      welltyped Σ Γ (it_mkLambda_or_LetIn Δ t).

  Lemma welltyped_it_mkLambda_or_LetIn_iff :
    ∀ Γ Δ t,
      welltyped Σ Γ (it_mkLambda_or_LetIn Δ t) ↔
      welltyped Σ (Γ ,,, Δ) t.

  Lemma isWfArity_it_mkLambda_or_LetIn :
    ∀ Γ Δ T,
      isWfArity typing Σ Γ (it_mkLambda_or_LetIn Δ T) →
      isWfArity typing Σ (Γ ,,, Δ) T.

  Lemma wellformed_it_mkLambda_or_LetIn :
    ∀ Γ Δ t,
      wellformed Σ Γ (it_mkLambda_or_LetIn Δ t) →
      wellformed Σ (Γ ,,, Δ) t.

  Lemma wellformed_zipp :
    ∀ Γ t ρ,
      wellformed Σ Γ (zipp t ρ) →
      wellformed Σ Γ t.

  Lemma it_mkLambda_or_LetIn_wellformed :
    ∀ Γ Δ t,
      wellformed Σ (Γ ,,, Δ) t →
      wellformed Σ Γ (it_mkLambda_or_LetIn Δ t).

  Lemma zipx_wellformed :
    ∀ {Γ t π},
      wellformed Σ Γ (zipc t π) →
      wellformed Σ [] (zipx Γ t π).

  Lemma wellformed_zipx :
    ∀ {Γ t π},
      wellformed Σ [] (zipx Γ t π) →
      wellformed Σ Γ (zipc t π).

  Lemma wellformed_zipc_stack_context Γ t π ρ args
    : decompose_stack π = (args, ρ)
      → wellformed Σ Γ (zipc t π)
      → wellformed Σ (Γ ,,, stack_context π) (zipc t (appstack args ε)).

  Lemma wellformed_zipc_zippx :
    ∀ Γ t π,
      wellformed Σ Γ (zipc t π) →
      wellformed Σ Γ (zippx t π).

  Lemma lookup_env_const_name :
    ∀ {c c' d},
      lookup_env Σ c' = Some (ConstantDecl c d) →
      c' = c.

  Lemma red_const :
    ∀ {Γ n c u cty cb cu},
      Some (ConstantDecl n {| cst_type := cty ; cst_body := Some cb ; cst_universes := cu |})
      = lookup_env Σ c →
      red (fst Σ) Γ (tConst c u) (subst_instance_constr u cb).

  Lemma cored_const :
    ∀ {Γ n c u cty cb cu},
      Some (ConstantDecl n {| cst_type := cty ; cst_body := Some cb ; cst_universes := cu |})
      = lookup_env Σ c →
      cored (fst Σ) Γ (subst_instance_constr u cb) (tConst c u).


  Lemma app_reds_r :
    ∀ Γ u v1 v2,
      red Σ Γ v1 v2 →
      red Σ Γ (tApp u v1) (tApp u v2).

  Lemma app_cored_r :
    ∀ Γ u v1 v2,
      cored Σ Γ v1 v2 →
      cored Σ Γ (tApp u v1) (tApp u v2).

  Fixpoint isAppProd (t : term) : bool :=
    match t with
    | tApp t l ⇒ isAppProd t
    | tProd na A B ⇒ true
    | _ ⇒ false
    end.

  Fixpoint isProd t :=
    match t with
    | tProd na A B ⇒ true
    | _ ⇒ false
    end.

  Lemma isAppProd_mkApps :
    ∀ t l, isAppProd (mkApps t l) = isAppProd t.

  Lemma isProdmkApps :
    ∀ t l,
      isProd (mkApps t l) →
      l = [].

  Lemma isSortmkApps :
    ∀ t l,
      isSort (mkApps t l) →
      l = [].

  Lemma isAppProd_isProd :
    ∀ Γ t,
      isAppProd t →
      welltyped Σ Γ t →
      isProd t.

  Lemma mkApps_Prod_nil :
    ∀ Γ na A B l,
      welltyped Σ Γ (mkApps (tProd na A B) l) →
      l = [].

  Lemma mkApps_Prod_nil' :
    ∀ Γ na A B l,
      wellformed Σ Γ (mkApps (tProd na A B) l) →
      l = [].

  Lemma decompose_stack_noStackApp :
    ∀ π l ρ,
      decompose_stack π = (l,ρ) →
      isStackApp ρ = false.

  Lemma stack_context_decompose :
    ∀ π,
      stack_context (snd (decompose_stack π)) = stack_context π.

  Lemma it_mkLambda_or_LetIn_inj :
    ∀ Γ u v,
      it_mkLambda_or_LetIn Γ u =
      it_mkLambda_or_LetIn Γ v →
      u = v.

  Lemma nleq_term_zipc :
    ∀ u v π,
      nleq_term u v →
      nleq_term (zipc u π) (zipc v π).

  Lemma nleq_term_zipx :
    ∀ Γ u v π,
      nleq_term u v →
      nleq_term (zipx Γ u π) (zipx Γ v π).


  Fixpoint let_free_context (Γ : context) :=
    match Γ with
    | [] ⇒ true
    | {| decl_name := na ; decl_body := Some b ; decl_type := B |} :: Γ ⇒ false
    | {| decl_name := na ; decl_body := None ; decl_type := B |} :: Γ ⇒
      let_free_context Γ
    end.

  Lemma let_free_stack_context :
    ∀ π,
      let_free_context (stack_context π).

  Lemma cored_red_cored :
    ∀ Γ u v w,
      cored Σ Γ w v →
      red Σ Γ u v →
      cored Σ Γ w u.

  Lemma red_neq_cored :
    ∀ Γ u v,
      red Σ Γ u v →
      u ≠ v →
      cored Σ Γ v u.

  Lemma red_welltyped :
    ∀ {Γ u v},
      welltyped Σ Γ u →
      ∥ red (fst Σ) Γ u v ∥ →
      welltyped Σ Γ v.

  Lemma red_cored_cored :
    ∀ Γ u v w,
      red Σ Γ v w →
      cored Σ Γ v u →
      cored Σ Γ w u.

  Lemma subject_conversion :
    ∀ Γ u v A B,
      Σ ;;; Γ |- u : A →
      Σ ;;; Γ |- v : B →
      Σ ;;; Γ |- u == v →
      ∑ C,
        Σ ;;; Γ |- u : C ×
        Σ ;;; Γ |- v : C.

  Lemma welltyped_zipc_replace :
    ∀ Γ u v π,
      welltyped Σ Γ (zipc v π) →
      welltyped Σ (Γ ,,, stack_context π) u →
      Σ ;;; Γ ,,, stack_context π |- u == v →
      welltyped Σ Γ (zipc u π).

  Lemma wellformed_zipc_replace :
    ∀ Γ u v π,
      wellformed Σ Γ (zipc v π) →
      wellformed Σ (Γ ,,, stack_context π) u →
      Σ ;;; Γ ,,, stack_context π |- u == v →
      wellformed Σ Γ (zipc u π).


  Lemma Construct_Ind_ind_eq :
    ∀ {Γ n i args u i' args' u'},
      Σ ;;; Γ |- mkApps (tConstruct i n u) args : mkApps (tInd i' u') args' →
      i = i'.

  Lemma Proj_red_cond :
    ∀ Γ i pars narg i' c u l,
      wellformed Σ Γ (tProj (i, pars, narg) (mkApps (tConstruct i' c u) l)) →
      nth_error l (pars + narg) ≠ None.

  Lemma Case_Construct_ind_eq :
    ∀ {Γ ind ind' npar pred i u brs args},
      wellformed Σ Γ (tCase (ind, npar) pred (mkApps (tConstruct ind' i u) args) brs) →
      ind = ind'.

  Lemma Proj_Constuct_ind_eq :
    ∀ Γ i i' pars narg c u l,
      wellformed Σ Γ (tProj (i, pars, narg) (mkApps (tConstruct i' c u) l)) →
      i = i'.

  Lemma cored_zipc :
    ∀ Γ t u π,
      cored Σ (Γ ,,, stack_context π) t u →
      cored Σ Γ (zipc t π) (zipc u π).

  Lemma red_zipc :
    ∀ Γ t u π,
      red Σ (Γ ,,, stack_context π) t u →
      red Σ Γ (zipc t π) (zipc u π).

  Lemma wellformed_zipc_zipp :
    ∀ Γ t π,
      wellformed Σ Γ (zipc t π) →
      wellformed Σ (Γ ,,, stack_context π) (zipp t π).

  Lemma conv_context_convp :
    ∀ Γ Γ' leq u v,
      conv leq Σ Γ u v →
      conv_context Σ Γ Γ' →
      conv leq Σ Γ' u v.

End Lemmata.

Lemma strengthening `{cf : checker_flags} :
  ∀ {Σ Γ Γ' Γ'' t T},
    wf Σ.1 →
    Σ ;;; Γ ,,, Γ'' ,,, lift_context #|Γ''| 0 Γ'
    |- lift #|Γ''| #|Γ'| t : lift #|Γ''| #|Γ'| T →
    Σ;;; Γ ,,, Γ' |- t : T.


Lemma map_option_out_mapi :
  ∀ {A B} (l : list A) (l' : list B) f P,
    map_option_out (mapi f l) = Some l' →
    Alli (fun i x ⇒ on_Some_or_None P (f i x)) 0 l →
    All P l'.

Lemma Alli_id :
  ∀ {A} {P : nat → A → Type} (l : list A) (n : nat),
    (∀ n x, P n x) → Alli P n l.

Lemma map_option_out_All {A} P (l : list (option A)) l' :
  (All (on_some P) l) →
  map_option_out l = Some l' →
  All P l'.

Lemma All_mapi {A B} P f l k :
  Alli (fun i x ⇒ P (f i x)) k l → All P (@mapi_rec A B f l k).

Lemma type_Case_valid_btys {cf:checker_flags} Σ Γ ind u npar p args :
    ∀ mdecl idecl (isdecl : declared_inductive Σ.1 mdecl ind idecl),
    mdecl.(ind_npars) = npar →
    let pars := List.firstn npar args in
    ∀ pty, Σ ;;; Γ |- p : pty →
    ∀ indctx pctx ps btys, types_of_case ind mdecl idecl pars u p pty
                           = Some (indctx, pctx, ps, btys) →
    
    
    
    
    All (fun x ⇒ Σ ;;; Γ |- snd x : tSort ps) btys.

Lemma type_Case' {cf:checker_flags} Σ Γ ind u npar p c brs args :
    ∀ mdecl idecl (isdecl : declared_inductive Σ.1 mdecl ind idecl),
    mdecl.(ind_npars) = npar →
    let pars := List.firstn npar args in
    ∀ pty, Σ ;;; Γ |- p : pty →
    ∀ indctx pctx ps btys, types_of_case ind mdecl idecl pars u p pty
                           = Some (indctx, pctx, ps, btys) →
    check_correct_arity (global_ext_constraints Σ) idecl ind u indctx pars pctx →
    existsb (leb_sort_family (universe_family ps)) idecl.(ind_kelim) →
    Σ ;;; Γ |- c : mkApps (tInd ind u) args →
    All2 (fun x y ⇒ (fst x = fst y) × (Σ ;;; Γ |- snd x : snd y)) brs btys →
    Σ ;;; Γ |- tCase (ind, npar) p c brs : mkApps p (List.skipn npar args ++ [c]).

Lemma destArity_spec_Some ctx T ctx' s :
  destArity ctx T = Some (ctx', s)
  → it_mkProd_or_LetIn ctx T = it_mkProd_or_LetIn ctx' (tSort s).