Module CS := ConstraintSet.
Module LS := LevelSet.



Section CheckerFlags.
Context {cf : checker_flags}.

Global Instance subst_instance_list {A} `(UnivSubst A) : UnivSubst (list A)
  := fun u ⇒ map (subst_instance u).

Global Instance subst_instance_def {A : Set} `(UnivSubst A) : UnivSubst (def A)
  := fun u ⇒ map_def (subst_instance u) (subst_instance u).

Global Instance subst_instance_prod {A B} `(UnivSubst A) `(UnivSubst B)
  : UnivSubst (A × B)
  := fun u ⇒ on_pair (subst_instance u) (subst_instance u).

Global Instance subst_instance_nat : UnivSubst nat
  := fun _ n ⇒ n.

Lemma subst_instance_instance_length u1 u2 :
  #|subst_instance_instance u2 u1| = #|u1|.

Lemma subst_instance_level_two u1 u2 l :
  subst_instance_level u1 (subst_instance_level u2 l)
  = subst_instance_level (subst_instance_instance u1 u2) l.

Lemma subst_instance_univ_two u1 u2 s :
  subst_instance_univ u1 (subst_instance_univ u2 s)
  = subst_instance_univ (subst_instance_instance u1 u2) s.

Lemma subst_instance_instance_two u1 u2 u :
  subst_instance_instance u1 (subst_instance_instance u2 u)
  = subst_instance_instance (subst_instance_instance u1 u2) u.

Lemma subst_instance_constr_two u1 u2 t :
  subst_instance_constr u1 (subst_instance_constr u2 t)
  = subst_instance_constr (subst_instance_instance u1 u2) t.

Lemma subst_instance_context_two u1 u2 Γ :
  subst_instance_context u1 (subst_instance_context u2 Γ)
  = subst_instance_context (subst_instance_instance u1 u2) Γ.

Lemma subst_instance_cstr_two u1 u2 c :
  subst_instance_cstr u1 (subst_instance_cstr u2 c)
  = subst_instance_cstr (subst_instance_instance u1 u2) c.

Lemma In_subst_instance_cstrs u c ctrs :
  CS.In c (subst_instance_cstrs u ctrs)
  ↔ ∃ c', c = subst_instance_cstr u c' ∧ CS.In c' ctrs.

Lemma In_subst_instance_cstrs' u c ctrs :
  CS.In c ctrs →
  CS.In (subst_instance_cstr u c) (subst_instance_cstrs u ctrs).

Lemma subst_instance_cstrs_two u1 u2 ctrs :
  CS.Equal
    (subst_instance_cstrs u1 (subst_instance_cstrs u2 ctrs))
    (subst_instance_cstrs (subst_instance_instance u1 u2) ctrs).

Lemma consistent_instance_no_prop lvs φ uctx u :
  consistent_instance lvs φ uctx u
  → forallb (fun x ⇒ negb (Level.is_prop x)) u.


Lemma consistent_instance_declared lvs φ uctx u :
  consistent_instance lvs φ uctx u
  → forallb (fun l ⇒ LS.mem l lvs) u.

Lemma monomorphic_level_notin_AUContext s φ :
  ¬ LS.In (Level.Level s) (AUContext.levels φ).

Global Instance satisfies_equal_sets v :
  Morphisms.Proper (Morphisms.respectful CS.Equal iff) (satisfies v).

Global Instance satisfies_subsets v :
  Morphisms.Proper (Morphisms.respectful CS.Subset (flip impl))
                   (satisfies v).


Lemma val0_subst_instance_level u l v
      (Hu : forallb (negb ∘ Level.is_prop) u)
  : val0 v (subst_instance_level u l) = val0 (subst_instance_valuation u v) l.

Lemma satisfies0_subst_instance_ctr u v c
      (Hu : forallb (negb ∘ Level.is_prop) u)
  : satisfies0 v (subst_instance_cstr u c)
    ↔ satisfies0 (subst_instance_valuation u v) c.

Lemma satisfies_subst_instance_ctr u v ctrs
      (Hu : forallb (negb ∘ Level.is_prop) u)
  : satisfies v (subst_instance_cstrs u ctrs)
    ↔ satisfies (subst_instance_valuation u v) ctrs.

Lemma not_var_global_levels Σ (hΣ : wf Σ) :
  LS.For_all (negb ∘ Level.is_var) (global_levels Σ).

Definition wf_ext_wk (Σ : global_env_ext)
  := wf Σ.1 × on_udecl_prop Σ.1 Σ.2.

Lemma not_var_global_ext_levels Σ φ (hΣ : wf_ext_wk (Σ, Monomorphic_ctx φ)) :
  LS.For_all (negb ∘ Level.is_var)
                   (global_ext_levels (Σ, Monomorphic_ctx φ)).

Lemma levels_global_constraint Σ (hΣ : wf Σ) c :
  CS.In c (global_constraints Σ)
  → LS.In c.1.1 (global_levels Σ)
    ∧ LS.In c.2 (global_levels Σ).

Lemma levels_global_ext_constraint Σ φ (hΣ : wf_ext_wk (Σ, φ)) c :
  CS.In c (global_ext_constraints (Σ, φ))
  → LS.In c.1.1 (global_ext_levels (Σ, φ))
    ∧ LS.In c.2 (global_ext_levels (Σ, φ)).

Definition is_monomorphic_cstr (c : univ_constraint)
  := negb (Level.is_var c.1.1) && negb (Level.is_var c.2).

Lemma monomorphic_global_constraint Σ (hΣ : wf Σ) c :
  CS.In c (global_constraints Σ)
  → is_monomorphic_cstr c.

Lemma monomorphic_global_constraint_ext Σ φ
      (hΣ : wf_ext_wk (Σ, Monomorphic_ctx φ)) c :
  CS.In c (global_ext_constraints (Σ, Monomorphic_ctx φ))
  → is_monomorphic_cstr c.


Lemma subst_instance_monom_cstr inst c :
  is_monomorphic_cstr c
  → subst_instance_cstr inst c = c.

Lemma satisfies_union v φ1 φ2 :
  satisfies v (CS.union φ1 φ2)
  ↔ (satisfies v φ1 ∧ satisfies v φ2).

Lemma equal_subst_instance_cstrs_mono u cstrs :
  CS.For_all is_monomorphic_cstr cstrs →
  CS.Equal (subst_instance_cstrs u cstrs) cstrs.

Lemma subst_instance_cstrs_union u φ φ' :
  CS.Equal (subst_instance_cstrs u (CS.union φ φ'))
           (CS.union (subst_instance_cstrs u φ) (subst_instance_cstrs u φ')).


Definition sub_context_set (φ φ' : ContextSet.t)
  := LS.Subset φ.1 φ'.1 ∧ CS.Subset φ.2 φ'.2.

Definition global_ext_context_set Σ : ContextSet.t
  := (global_ext_levels Σ, global_ext_constraints Σ).

Global Instance sub_context_set_trans : RelationClasses.Transitive sub_context_set.

Lemma consistent_ext_trans_polymorphic_case_aux {Σ φ1 φ2 φ' udecl inst inst'} :
  wf_ext_wk (Σ, Polymorphic_ctx (φ1, φ2)) →
  valid_constraints0 (global_ext_constraints (Σ, Polymorphic_ctx (φ1, φ2)))
                     (subst_instance_cstrs inst udecl) →
  valid_constraints0 (global_ext_constraints (Σ, φ'))
                     (subst_instance_cstrs inst' φ2) →
  forallb (fun x : Level.t ⇒ negb (Level.is_prop x)) inst' →
  valid_constraints0 (global_ext_constraints (Σ, φ'))
                     (subst_instance_cstrs
                        (subst_instance_instance inst' inst) udecl).

Lemma consistent_ext_trans_polymorphic_cases Σ φ φ' udecl inst inst' :
  wf_ext_wk (Σ, φ) →
  sub_context_set (monomorphic_udecl φ) (global_ext_context_set (Σ, φ')) →
  consistent_instance_ext (Σ, φ) (Polymorphic_ctx udecl) inst →
  consistent_instance_ext (Σ, φ') φ inst' →
  consistent_instance_ext (Σ, φ') (Polymorphic_ctx udecl)
                          (subst_instance_instance inst' inst).

Lemma consistent_ext_trans Σ φ φ' udecl inst inst' :
  wf_ext_wk (Σ, φ) →
  sub_context_set (monomorphic_udecl φ) (global_ext_context_set (Σ, φ')) →
  consistent_instance_ext (Σ, φ) udecl inst →
  consistent_instance_ext (Σ, φ') φ inst' →
  consistent_instance_ext (Σ, φ') udecl (subst_instance_instance inst' inst).


Lemma consistent_instance_valid_constraints Σ φ u univs :
  wf_ext_wk (Σ, φ) →
  CS.Subset (monomorphic_constraints φ)
                       (global_ext_constraints (Σ, univs)) →
  consistent_instance_ext (Σ, univs) φ u →
  valid_constraints (global_ext_constraints (Σ, univs))
                    (subst_instance_cstrs u (global_ext_constraints (Σ, φ))).


Class SubstUnivPreserved {A} `{UnivSubst A} (R : constraints → crelation A)
  := Build_SubstUnivPreserved :
       ∀ φ φ' (u : universe_instance),
         forallb (fun x ⇒ negb (Level.is_prop x)) u →
         valid_constraints φ' (subst_instance_cstrs u φ) →
         subrelation (R φ)
                     (precompose (R φ') (subst_instance u)).

Lemma satisfies_subst_instance φ φ' u :
  check_univs = true →
  forallb (fun x ⇒ negb (Level.is_prop x)) u →
  valid_constraints φ' (subst_instance_cstrs u φ) →
  ∀ v, satisfies v φ' →
       satisfies (subst_instance_valuation u v) φ.

Global Instance leq_universe_subst_instance : SubstUnivPreserved leq_universe.

Global Instance eq_universe_subst_instance : SubstUnivPreserved eq_universe.

Lemma precompose_subst_instance_instance Rle u i i' :
  precompose (R_universe_instance Rle) (subst_instance_instance u) i i'
  <~> R_universe_instance (precompose Rle (subst_instance_univ u)) i i'.

Definition precompose_subst_instance_instance__1 Rle u i i'
  := equiv _ _ (precompose_subst_instance_instance Rle u i i').

Definition precompose_subst_instance_instance__2 Rle u i i'
  := equiv_inv _ _ (precompose_subst_instance_instance Rle u i i').

Global Instance eq_term_upto_univ_subst_instance
         (Re Rle : constraints → universe → universe → Prop)
      {he: SubstUnivPreserved Re} {hle: SubstUnivPreserved Rle}
  : SubstUnivPreserved (fun φ ⇒ eq_term_upto_univ (Re φ) (Rle φ)).

Lemma leq_term_subst_instance : SubstUnivPreserved leq_term.

Lemma eq_term_subst_instance : SubstUnivPreserved eq_term.

Lemma subst_instance_univ_super l u
      (Hu : forallb (negb ∘ Level.is_prop) u)
  : subst_instance_univ u (Universe.super l)
    = Universe.super (subst_instance_level u l).

Lemma subst_instance_univ_make l u :
  subst_instance_univ u (Universe.make l)
  = Universe.make (subst_instance_level u l).

Lemma LevelIn_subst_instance Σ l u univs :
  LS.In l (global_ext_levels Σ) →
  LS.Subset (monomorphic_levels Σ.2) (global_ext_levels (Σ.1, univs)) →
  consistent_instance_ext (Σ.1, univs) Σ.2 u →
  LS.In (subst_instance_level u l) (global_ext_levels (Σ.1, univs)).

Lemma is_prop_subst_instance_univ u l
      (Hu : forallb (negb ∘ Level.is_prop) u)
  : Universe.is_prop (subst_instance_univ u l) = Universe.is_prop l.

Lemma is_small_subst_instance_univ u l
  : Universe.is_small l → Universe.is_small (subst_instance_univ u l).

Lemma sup_subst_instance_univ u s1 s2 :
  subst_instance_univ u (Universe.sup s1 s2)
  = Universe.sup (subst_instance_univ u s1) (subst_instance_univ u s2).

Lemma product_subst_instance u s1 s2
      (Hu : forallb (negb ∘ Level.is_prop) u)
 : subst_instance_univ u (Universe.sort_of_product s1 s2)
   = Universe.sort_of_product (subst_instance_univ u s1) (subst_instance_univ u s2).

Lemma iota_red_subst_instance pars c args brs u :
  subst_instance_constr u (iota_red pars c args brs)
  = iota_red pars c (subst_instance u args) (subst_instance u brs).

Lemma fix_subst_subst_instance u mfix :
  map (subst_instance_constr u) (fix_subst mfix)
  = fix_subst (subst_instance u mfix).

Lemma cofix_subst_subst_instance u mfix :
  map (subst_instance_constr u) (cofix_subst mfix)
  = cofix_subst (subst_instance u mfix).

Lemma isConstruct_app_subst_instance u t :
  isConstruct_app (subst_instance_constr u t) = isConstruct_app t.

Lemma fix_context_subst_instance u mfix :
  subst_instance_context u (fix_context mfix)
  = fix_context (subst_instance u mfix).

Lemma subst_instance_context_app u L1 L2 :
  subst_instance_context u (L1,,,L2)
  = subst_instance_context u L1 ,,, subst_instance_context u L2.

Lemma red1_subst_instance Σ Γ u s t :
  red1 Σ Γ s t →
  red1 Σ (subst_instance_context u Γ)
       (subst_instance_constr u s) (subst_instance_constr u t).

Lemma cumul_subst_instance (Σ : global_env_ext) Γ u A B univs :
  forallb (fun x ⇒ negb (Level.is_prop x)) u →
  valid_constraints (global_ext_constraints (Σ.1, univs))
                    (subst_instance_cstrs u Σ) →
  Σ ;;; Γ |- A ≤ B →
  (Σ.1,univs) ;;; subst_instance_context u Γ
                   |- subst_instance_constr u A ≤ subst_instance_constr u B.

Global Instance eq_decl_subst_instance : SubstUnivPreserved eq_decl.

Global Instance eq_context_subst_instance : SubstUnivPreserved eq_context.

Lemma subst_instance_destArity Γ A u :
  destArity (subst_instance_context u Γ) (subst_instance_constr u A)
  = match destArity Γ A with
    | Some (ctx, s) ⇒ Some (subst_instance_context u ctx, subst_instance_univ u s)
    | None ⇒ None
    end.

Lemma option_map_two {A B C} (f : A → B) (g : B → C) x
  : option_map g (option_map f x) = option_map (g ∘ f) x.

Lemma option_map_ext {A B} (f g : A → B) (H : ∀ x, f x = g x)
  : ∀ z, option_map f z = option_map g z.

Lemma subst_instance_instantiate_params_subst u0 params pars s ty :
  option_map (on_pair (map (subst_instance_constr u0)) (subst_instance_constr u0))
             (instantiate_params_subst params pars s ty)
  = instantiate_params_subst (subst_instance_context u0 params)
                             (map (subst_instance_constr u0) pars)
                             (map (subst_instance_constr u0) s)
                             (subst_instance_constr u0 ty).

Lemma subst_instance_instantiate_params u0 params pars ty :
  option_map (subst_instance_constr u0)
             (instantiate_params params pars ty)
  = instantiate_params (subst_instance_context u0 params)
                       (map (subst_instance_constr u0) pars)
                       (subst_instance_constr u0 ty).

Lemma subst_instance_inds u0 ind u bodies :
  subst_instance u0 (inds ind u bodies)
  = inds ind (subst_instance u0 u) bodies.

Lemma subst_instance_decompose_prod_assum u Γ t :
  subst_instance u (decompose_prod_assum Γ t)
  = decompose_prod_assum (subst_instance_context u Γ) (subst_instance_constr u t).

Lemma subst_instance_decompose_app_rec u Γ t
  : subst_instance u (decompose_app_rec t Γ)
    = decompose_app_rec (subst_instance u t) (subst_instance u Γ).

Lemma subst_instance_to_extended_list u l
  : map (subst_instance_constr u) (to_extended_list l)
    = to_extended_list (subst_instance_context u l).

Lemma subst_instance_build_branches_type u0 ind mdecl idecl pars u p :
  map (option_map (on_snd (subst_instance_constr u0)))
      (build_branches_type ind mdecl idecl pars u p)
  = build_branches_type ind mdecl idecl (map (subst_instance_constr u0) pars)
                        (subst_instance_instance u0 u) (subst_instance_constr u0 p).

Axiom fix_guard_subst_instance :
  ∀ mfix u,
    fix_guard mfix →
    fix_guard (map (map_def (subst_instance_constr u) (subst_instance_constr u))
                   mfix).

Lemma All_local_env_over_subst_instance Σ Γ (wfΓ : wf_local Σ Γ) :
  All_local_env_over typing
                     (fun Σ0 Γ0 (_ : wf_local Σ0 Γ0) t T (_ : Σ0;;; Γ0 |- t : T) ⇒
       ∀ u univs, wf_ext_wk Σ0 →
                  sub_context_set (monomorphic_udecl Σ0.2)
                                  (global_ext_context_set (Σ0.1, univs)) →
                  consistent_instance_ext (Σ0.1, univs) Σ0.2 u →
                  (Σ0.1, univs) ;;; subst_instance_context u Γ0
                  |- subst_instance_constr u t : subst_instance_constr u T)
                     Σ Γ wfΓ →
  ∀ u univs,
    wf_ext_wk Σ →
    sub_context_set (monomorphic_udecl Σ.2)
                    (global_ext_context_set (Σ.1, univs)) →
    consistent_instance_ext (Σ.1, univs) Σ.2 u →
    wf_local (Σ.1, univs) (subst_instance_context u Γ).


Lemma typing_subst_instance :
  env_prop (fun Σ Γ t T ⇒ ∀ u univs,
                wf_ext_wk Σ →
                sub_context_set (monomorphic_udecl Σ.2)
                                (global_ext_context_set (Σ.1, univs)) →
                consistent_instance_ext (Σ.1, univs) Σ.2 u →
                (Σ.1,univs) ;;; subst_instance_context u Γ
                |- subst_instance_constr u t : subst_instance_constr u T).

Lemma typing_subst_instance' Σ φ Γ t T u univs :
  wf_ext_wk (Σ, univs) →
  (Σ, univs) ;;; Γ |- t : T →
  sub_context_set (monomorphic_udecl univs) (global_ext_context_set (Σ, φ)) →
  consistent_instance_ext (Σ, φ) univs u →
  (Σ, φ) ;;; subst_instance_context u Γ
            |- subst_instance_constr u t : subst_instance_constr u T.

Definition global_context_set Σ : ContextSet.t
  := (global_levels Σ, global_constraints Σ).

Lemma global_context_set_sub_ext Σ φ :
  sub_context_set (global_context_set Σ) (global_ext_context_set (Σ, φ)).

Lemma weaken_lookup_on_global_env'' Σ c decl :
  wf Σ →
  lookup_env Σ c = Some decl →
  sub_context_set (monomorphic_udecl (universes_decl_of_decl decl))
                  (global_context_set Σ).

Lemma typing_subst_instance'' Σ φ Γ t T u univs :
  wf_ext_wk (Σ, univs) →
  (Σ, univs) ;;; Γ |- t : T →
  sub_context_set (monomorphic_udecl univs) (global_context_set Σ) →
  consistent_instance_ext (Σ, φ) univs u →
  (Σ, φ) ;;; subst_instance_context u Γ
            |- subst_instance_constr u t : subst_instance_constr u T.

Lemma typing_subst_instance_decl Σ Γ t T c decl u :
  wf Σ.1 →
  lookup_env Σ.1 c = Some decl →
  (Σ.1, universes_decl_of_decl decl) ;;; Γ |- t : T →
  consistent_instance_ext Σ (universes_decl_of_decl decl) u →
  Σ ;;; subst_instance_context u Γ
            |- subst_instance_constr u t : subst_instance_constr u T.

End CheckerFlags.