Library MetaCoq.PCUIC.utils.PCUICAstUtils

From MetaCoq.Template Require Import utils uGraph Reflect.
From MetaCoq.PCUIC Require Import PCUICAst PCUICSize.

Require Import ssreflect.
From Equations Require Import Equations.
Set Equations Transparent.

Lemma eqb_annot_reflect {A} na na' : reflect (@eq_binder_annot A A na na') (eqb_binder_annot na na').
Proof.
  unfold eqb_binder_annot, eq_binder_annot.
  destruct Classes.eq_dec; constructor; auto.
Qed.

Definition string_of_aname (b : binder_annot name) :=
  string_of_name b.(binder_name).

Fixpoint string_of_term (t : term) :=
  match t with
  | tRel n ⇒ "Rel(" ^ string_of_nat n ^ ")"
  | tVar n ⇒ "Var(" ^ n ^ ")"
  | tEvar ev args ⇒ "Evar(" ^ string_of_nat ev ^ "," ^ string_of_list string_of_term args ^ ")"
  | tSort s ⇒ "Sort(" ^ string_of_sort s ^ ")"
  | tProd na b t ⇒ "Prod(" ^ string_of_aname na ^ "," ^
                            string_of_term b ^ "," ^ string_of_term t ^ ")"
  | tLambda na b t ⇒ "Lambda(" ^ string_of_aname na ^ "," ^ string_of_term b
                                ^ "," ^ string_of_term t ^ ")"
  | tLetIn na b t' t ⇒ "LetIn(" ^ string_of_aname na ^ "," ^ string_of_term b
                                 ^ "," ^ string_of_term t' ^ "," ^ string_of_term t ^ ")"
  | tApp f l ⇒ "App(" ^ string_of_term f ^ "," ^ string_of_term l ^ ")"
  | tConst c u ⇒ "Const(" ^ string_of_kername c ^ "," ^ string_of_universe_instance u ^ ")"
  | tInd i u ⇒ "Ind(" ^ string_of_inductive i ^ "," ^ string_of_universe_instance u ^ ")"
  | tConstruct i n u ⇒ "Construct(" ^ string_of_inductive i ^ "," ^ string_of_nat n ^ ","
                                    ^ string_of_universe_instance u ^ ")"
  | tCase ci p t brs
    "Case(" ^ string_of_case_info ci ^ "," ^ string_of_term t ^ ","
            ^ string_of_predicate string_of_term p ^ "," ^ string_of_list (string_of_branch string_of_term) brs ^ ")"
  | tProj p c
    "Proj(" ^ string_of_inductive p.(proj_ind) ^ "," ^ string_of_nat p.(proj_npars) ^ "," ^ string_of_nat p.(proj_arg) ^ ","
            ^ string_of_term c ^ ")"
  | tFix l n ⇒ "Fix(" ^ (string_of_list (string_of_def string_of_term) l) ^ "," ^ string_of_nat n ^ ")"
  | tCoFix l n ⇒ "CoFix(" ^ (string_of_list (string_of_def string_of_term) l) ^ "," ^ string_of_nat n ^ ")"
  
  end.

Ltac change_Sk :=
  repeat match goal with
    | |- context [S (?x + ?y)] ⇒ progress change (S (x + y)) with (S x + y)
    | |- context [#|?l| + (?x + ?y)] ⇒ progress replace (#|l| + (x + y)) with ((#|l| + x) + y) by now rewrite Nat.add_assoc
  end.

Ltac solve_all_one :=
  try lazymatch goal with
  | H: tCasePredProp _ _ _ |- _destruct H as [? [? ?]]
end;
  unfold tCaseBrsProp, tFixProp in *;
  autorewrite with map;
  rtoProp;
  try (
    apply map_predicate_eq_spec ||
    apply map_predicate_k_eq_spec ||
    apply map_predicate_id_spec ||
    apply map_predicate_k_id_spec ||
    apply map_branch_k_eq_spec ||
    apply map_branch_k_id_spec ||
    apply map_def_eq_spec ||
    apply map_def_id_spec ||
    apply map_branch_eq_spec ||
    apply map_branch_id_spec ||
    (eapply All_forallb_eq_forallb; [eassumption|]) ||
    (eapply mapi_context_eqP_test_id_spec; [eassumption|eassumption|]) ||
    (eapply mapi_context_eqP_spec; [eassumption|]) ||
    (eapply mapi_context_eqP_id_spec; [eassumption|]) ||
    (eapply onctx_test; [eassumption|eassumption|]) ||
    (eapply test_context_k_eqP_id_spec; [eassumption|eassumption|]) ||
    (eapply test_context_k_eqP_eq_spec; [eassumption|]) ||
    (eapply map_context_eq_spec; [eassumption|]));
  repeat toAll; try All_map; try close_Forall;
  change_Sk; auto with all;
  intuition eauto 4 with all.

Ltac solve_all := repeat (progress solve_all_one).
#[global] Hint Extern 10 ⇒ rewrite !map_branch_map_branch : all.
#[global] Hint Extern 10 ⇒ rewrite !map_predicate_map_predicate : all.

Lemma lookup_env_nil c s : lookup_global [] c = Some s False.
Proof.
  induction c; simpl; auto ⇒ //.
Qed.

Lemma lookup_env_cons {kn d Σ kn' d'} : lookup_global ((kn, d) :: Σ) kn' = Some d'
  (kn = kn' d = d') (kn kn' lookup_global Σ kn' = Some d').
Proof.
  simpl.
  epose proof (ReflectEq.eqb_spec (A:=kername) kn' kn). simpl in H.
  elim: H. intros → [= <-]; intuition auto.
  intros diff look. intuition auto.
Qed.

Lemma lookup_env_cons_fresh {kn d Σ kn'} :
  kn kn'
  lookup_global ((kn, d) :: Σ) kn' = lookup_global Σ kn'.
Proof.
  simpl.
  epose proof (ReflectEq.eqb_spec (A:=kername) kn' kn). simpl in H.
  elim: H. intros → ⇒ //. auto.
Qed.

Fixpoint decompose_app_rec (t : term) l :=
  match t with
  | tApp f adecompose_app_rec f (a :: l)
  | _(t, l)
  end.

Definition decompose_app t := decompose_app_rec t [].

Lemma mkApps_tApp f a l : mkApps (tApp f a) l = mkApps f (a :: l).
Proof. reflexivity. Qed.

Lemma tApp_mkApps f a : tApp f a = mkApps f [a].
Proof. reflexivity. Qed.

Definition mkApps_decompose_app_rec t l :
  mkApps t l = mkApps (fst (decompose_app_rec t l)) (snd (decompose_app_rec t l)).
Proof.
  revert l; induction t; try reflexivity.
  intro l; cbn in ×.
  transitivity (mkApps t1 ((t2 ::l))). reflexivity.
  now rewrite IHt1.
Qed.

Definition mkApps_decompose_app t :
  t = mkApps (fst (decompose_app t)) (snd (decompose_app t))
  := mkApps_decompose_app_rec t [].

Lemma decompose_app_rec_mkApps f l l' : decompose_app_rec (mkApps f l) l' =
                                    decompose_app_rec f (l ++ l').
Proof.
  induction l in f, l' |- *; simpl; auto; rewrite IHl ?app_nil_r; auto.
Qed.

Require Import ssrbool.

Lemma decompose_app_mkApps f l :
  ~~ isApp f decompose_app (mkApps f l) = (f, l).
Proof.
  intros Hf. rewrite /decompose_app decompose_app_rec_mkApps. rewrite app_nil_r.
  destruct f; simpl in *; (discriminate || reflexivity).
Qed.

Lemma mkApps_app f l l' : mkApps f (l ++ l') = mkApps (mkApps f l) l'.
Proof.
  induction l in f, l' |- *; destruct l'; simpl; rewrite ?app_nil_r; auto.
  rewrite IHl //.
Qed.

Lemma mkApps_tApp_inj fn args t u :
  ~~ isApp fn
  mkApps fn args = tApp t u
  t = mkApps fn (removelast args) u = last args t.
Proof.
  intros napp eqapp.
  destruct args using rev_case ⇒ //.
  simpl in eqapp. subst fn ⇒ //.
  rewrite mkApps_app in eqapp. noconf eqapp.
  now rewrite removelast_app // last_app // /= app_nil_r.
Qed.

Lemma removelast_length {A} (args : list A) : #|removelast args| = Nat.pred #|args|.
Proof.
  induction args ⇒ //. destruct args ⇒ //.
  now rewrite (removelast_app [_]) // app_length IHargs /=.
Qed.

Lemma nth_error_removelast {A} {args : list A} {n arg} :
  nth_error (removelast args) n = Some arg
  nth_error args n = Some arg.
Proof.
  intros h. rewrite nth_error_removelast //.
  apply nth_error_Some_length in h.
  now rewrite removelast_length in h.
Qed.

Lemma mkApps_discr f args t :
  args []
  mkApps f args = t
  ~~ isApp t False.
Proof.
  intros.
  destruct args using rev_case ⇒ //.
  rewrite mkApps_app in H0. destruct t ⇒ //.
Qed.

Fixpoint decompose_prod (t : term) : (list aname) × (list term) × term :=
  match t with
  | tProd n A Blet (nAs, B) := decompose_prod B in
                  let (ns, As) := nAs in
                  (n :: ns, A :: As, B)
  | _([], [], t)
  end.

Fixpoint remove_arity (n : nat) (t : term) : term :=
  match n with
  | Ot
  | S nmatch t with
          | tProd _ _ Bremove_arity n B
          | _t
          end
  end.

Definition isConstruct_app t :=
  match fst (decompose_app t) with
  | tConstruct _ _ _true
  | _false
  end.

Definition mind_body_to_entry (decl : mutual_inductive_body)
  : mutual_inductive_entry.
Proof.
  refine {| mind_entry_record := None;
            mind_entry_finite := Finite;
            mind_entry_params := _;
            mind_entry_inds := _;
            mind_entry_universes := decl.(ind_universes);
            mind_entry_private := None |}.
  - refine (match List.hd_error decl.(ind_bodies) with
            | Some i0_
            | Nonenil
            end).
    pose (typ := decompose_prod i0.(ind_type)).
    destruct typ as [[names types] _].
    apply (List.firstn decl.(ind_npars)) in names.
    apply (List.firstn decl.(ind_npars)) in types.
    refine (List.combine _ _).
    exact (List.map string_of_aname names).
    exact (List.map LocalAssum types).
  - refine (List.map _ decl.(ind_bodies)).
    intros [].
    refine {| mind_entry_typename := ind_name0;
              mind_entry_arity := remove_arity decl.(ind_npars) ind_type0;
              mind_entry_template := false;
              mind_entry_consnames := _;
              mind_entry_lc := _;
            |}.
    refine (List.map (fun xcstr_name x) ind_ctors0).
    refine (List.map (fun xremove_arity decl.(ind_npars)
                                                (cstr_type x)) ind_ctors0).
Defined.

Fixpoint decompose_prod_assum (Γ : context) (t : term) : context × term :=
  match t with
  | tProd n A Bdecompose_prod_assum (Γ ,, vass n A) B
  | tLetIn na b bty b'decompose_prod_assum (Γ ,, vdef na b bty) b'
  | _(Γ, t)
  end.

Lemma decompose_prod_assum_ctx ctx t : decompose_prod_assum ctx t =
  let (ctx', t') := decompose_prod_assum [] t in
  (ctx ,,, ctx', t').
Proof.
  induction t in ctx |- *; simpl; auto.
  - simpl. rewrite IHt2.
    rewrite (IHt2 ([] ,, vass _ _)).
    destruct (decompose_prod_assum [] t2). simpl.
    unfold snoc. now rewrite app_context_assoc.
  - simpl. rewrite IHt3.
    rewrite (IHt3 ([] ,, vdef _ _ _)).
    destruct (decompose_prod_assum [] t3). simpl.
    unfold snoc. now rewrite app_context_assoc.
Qed.

Fixpoint decompose_prod_n_assum (Γ : context) n (t : term) : option (context × term) :=
  match n with
  | 0 ⇒ Some (Γ, t)
  | S n
    match t with
    | tProd na A Bdecompose_prod_n_assum (Γ ,, vass na A) n B
    | tLetIn na b bty b'decompose_prod_n_assum (Γ ,, vdef na b bty) n b'
    | _None
    end
  end.

Lemma it_mkLambda_or_LetIn_app l l' t :
  it_mkLambda_or_LetIn (l ++ l') t = it_mkLambda_or_LetIn l' (it_mkLambda_or_LetIn l t).
Proof. induction l in l', t |- *; simpl; auto. Qed.

Lemma decompose_prod_n_assum_it_mkProd ctx ctx' ty :
  decompose_prod_n_assum ctx #|ctx'| (it_mkProd_or_LetIn ctx' ty) = Some (ctx' ++ ctx, ty).
Proof.
  revert ctx ty. induction ctx' using rev_ind; move⇒ // ctx ty.
  rewrite app_length /= it_mkProd_or_LetIn_app /=.
  destruct x as [na [body|] ty'] ⇒ /=;
  now rewrite !Nat.add_1_r /= IHctx' -app_assoc.
Qed.

Definition is_ind_app_head t :=
  let (f, l) := decompose_app t in
  match f with
  | tInd _ _true
  | _false
  end.

Lemma is_ind_app_head_mkApps ind u l : is_ind_app_head (mkApps (tInd ind u) l).
Proof.
  unfold is_ind_app_head.
  unfold decompose_app. rewrite decompose_app_rec_mkApps. now simpl; trivial.
Qed.

Lemma decompose_prod_assum_it_mkProd ctx ctx' ty :
  is_ind_app_head ty
  decompose_prod_assum ctx (it_mkProd_or_LetIn ctx' ty) = (ctx' ++ ctx, ty).
Proof.
  revert ctx ty. induction ctx' using rev_ind; move⇒ // ctx ty /=.
  destruct ty; unfold is_ind_app_head; simpl; try (congruence || reflexivity).
  moveHty. rewrite it_mkProd_or_LetIn_app /=.
  case: x ⇒ [na [body|] ty'] /=; by rewrite IHctx' // /snoc -app_assoc.
Qed.

Lemma reln_length Γ Γ' n : #|reln Γ n Γ'| = #|Γ| + context_assumptions Γ'.
Proof.
  induction Γ' in n, Γ |- *; simpl; auto.
  destruct a as [? [b|] ?]; simpl; auto.
  rewrite Nat.add_1_r. simpl. rewrite IHΓ' ⇒ /= //.
Qed.

Lemma to_extended_list_k_length Γ n : #|to_extended_list_k Γ n| = context_assumptions Γ.
Proof.
  now rewrite /to_extended_list_k reln_length.
Qed.

Lemma reln_list_lift_above l p Γ :
  Forall (fun x n, x = tRel n p n n < p + length Γ) l
  Forall (fun x n, x = tRel n p n n < p + length Γ) (reln l p Γ).
Proof.
  generalize (Nat.le_refl p).
  generalize p at 1 3 5.
  induction Γ in p, l |- ×. simpl. auto.
  intros. destruct a. destruct decl_body. simpl.
  assert(p0 S p) by lia.
  specialize (IHΓ l (S p) p0 H1). rewrite <- Nat.add_succ_comm, Nat.add_1_r.
  simpl in ×. rewrite <- Nat.add_succ_comm in H0. eauto.
  simpl in ×.
  specialize (IHΓ (tRel p :: l) (S p) p0 ltac:(lia)). rewrite <- Nat.add_succ_comm, Nat.add_1_r.
  eapply IHΓ. simpl in ×. rewrite <- Nat.add_succ_comm in H0. auto.
  simpl in ×.
  constructor. p. intuition lia. auto.
Qed.

Lemma to_extended_list_k_spec Γ k :
  Forall (fun x n, x = tRel n k n n < k + length Γ) (to_extended_list_k Γ k).
Proof.
  pose (reln_list_lift_above [] k Γ).
  unfold to_extended_list_k.
  forward f. constructor. apply f.
Qed.

Lemma to_extended_list_lift_above Γ :
  Forall (fun x n, x = tRel n n < length Γ) (to_extended_list Γ).
Proof.
  pose (reln_list_lift_above [] 0 Γ).
  unfold to_extended_list.
  forward f. constructor. eapply Forall_impl; eauto. intros.
  destruct H; eexists; intuition eauto.
Qed.

Fixpoint reln_alt p (Γ : context) :=
  match Γ with
  | [][]
  | {| decl_body := Some _ |} :: Γreln_alt (p + 1) Γ
  | {| decl_body := None |} :: ΓtRel p :: reln_alt (p + 1) Γ
  end.

Lemma reln_alt_eq l Γ k : reln l k Γ = List.rev (reln_alt k Γ) ++ l.
Proof.
  induction Γ in l, k |- *; simpl; auto.
  destruct a as [na [body|] ty]; simpl.
  now rewrite IHΓ.
  now rewrite IHΓ -app_assoc.
Qed.

Lemma to_extended_list_k_cons d Γ k :
  to_extended_list_k (d :: Γ) k =
  match d.(decl_body) with
  | Noneto_extended_list_k Γ (S k) ++ [tRel k]
  | Some bto_extended_list_k Γ (S k)
  end.
Proof.
  rewrite /to_extended_list_k reln_alt_eq. simpl.
  destruct d as [na [body|] ty]. simpl.
  now rewrite reln_alt_eq Nat.add_1_r.
  simpl. rewrite reln_alt_eq.
  now rewrite -app_assoc !app_nil_r Nat.add_1_r.
Qed.

Ltac merge_All :=
  unfold tFixProp, tCaseBrsProp in *;
  repeat toAll.

#[global]
Hint Rewrite @map_def_id @map_id : map.

Ltac close_All :=
  match goal with
  | H : Forall _ _ |- Forall _ _apply (Forall_impl H); clear H; simpl
  | H : All _ _ |- All _ _apply (All_impl H); clear H; simpl
  | H : OnOne2 _ _ _ |- OnOne2 _ _ _apply (OnOne2_impl H); clear H; simpl
  | H : All2 _ _ _ |- All2 _ _ _apply (All2_impl H); clear H; simpl
  | H : Forall2 _ _ _ |- Forall2 _ _ _apply (Forall2_impl H); clear H; simpl
  | H : All _ _ |- All2 _ _ _
    apply (All_All2 H); clear H; simpl
  | H : All2 _ _ _ |- All _ _
    (apply (All2_All_left H) || apply (All2_All_right H)); clear H; simpl
  end.

Lemma mkApps_inj :
   u v l,
    mkApps u l = mkApps v l
    u = v.
Proof.
  intros u v l eq.
  revert u v eq.
  induction l ; intros u v eq.
  - cbn in eq. assumption.
  - cbn in eq. apply IHl in eq.
    inversion eq. reflexivity.
Qed.

Lemma isApp_mkApps :
   u l,
    isApp u
    isApp (mkApps u l).
Proof.
  intros u l h.
  induction l in u, h |- ×.
  - cbn. assumption.
  - cbn. apply IHl. reflexivity.
Qed.

Lemma decompose_app_rec_notApp :
   t l u l',
    decompose_app_rec t l = (u, l')
    isApp u = false.
Proof.
  intros t l u l' e.
  induction t in l, u, l', e |- ×.
  all: try (cbn in e ; inversion e ; reflexivity).
  cbn in e. eapply IHt1. eassumption.
Qed.

Lemma decompose_app_notApp :
   t u l,
    decompose_app t = (u, l)
    isApp u = false.
Proof.
  intros t u l e.
  eapply decompose_app_rec_notApp. eassumption.
Qed.

Lemma decompose_app_rec_inv {t l' f l} :
  decompose_app_rec t l' = (f, l)
  mkApps t l' = mkApps f l.
Proof.
  induction t in f, l', l |- *; try intros [= <- <-]; try reflexivity.
  simpl. apply/IHt1.
Qed.

Lemma decompose_app_inv {t f l} :
  decompose_app t = (f, l) t = mkApps f l.
Proof. by apply/decompose_app_rec_inv. Qed.

Lemma decompose_app_nonnil t f l :
  isApp t
  decompose_app t = (f, l) l [].
Proof.
  intros isApp.
  destruct t; simpl ⇒ //.
  intros da.
  pose proof (decompose_app_notApp _ _ _ da).
  apply decompose_app_inv in da.
  destruct l using rev_ind.
  unfold decompose_app ⇒ /=.
  destruct f ⇒ //.
  destruct l ⇒ //.
Qed.

Fixpoint nApp t :=
  match t with
  | tApp u _S (nApp u)
  | _ ⇒ 0
  end.

Lemma isApp_false_nApp :
   u,
    isApp u = false
    nApp u = 0.
Proof.
  intros u h.
  destruct u.
  all: try reflexivity.
  discriminate.
Qed.

Lemma nApp_mkApps :
   t l,
    nApp (mkApps t l) = nApp t + #|l|.
Proof.
  intros t l.
  induction l in t |- ×.
  - simpl. lia.
  - simpl. rewrite IHl. cbn. lia.
Qed.

Lemma decompose_app_eq_mkApps :
   t u l l',
    decompose_app t = (mkApps u l', l)
    l' = [].
Proof.
  intros t u l l' e.
  apply decompose_app_notApp in e.
  apply isApp_false_nApp in e.
  rewrite nApp_mkApps in e.
  destruct l' ; cbn in e ; try lia.
  reflexivity.
Qed.

Lemma mkApps_nApp_inj :
   u u' l l',
    nApp u = nApp u'
    mkApps u l = mkApps u' l'
    u = u' l = l'.
Proof.
  intros u u' l l' h e.
  induction l in u, u', l', h, e |- ×.
  - cbn in e. subst.
    destruct l' ; auto.
    exfalso.
    rewrite nApp_mkApps in h. cbn in h. lia.
  - destruct l'.
    + cbn in e. subst. exfalso.
      rewrite nApp_mkApps in h. cbn in h. lia.
    + cbn in e. apply IHl in e.
      × destruct e as [e1 e2].
        inversion e1. subst. auto.
      × cbn. f_equal. auto.
Qed.

Lemma mkApps_notApp_inj :
   u u' l l',
    isApp u = false
    isApp u' = false
    mkApps u l = mkApps u' l'
    u = u' l = l'.
Proof.
  intros u u' l l' h h' e.
  eapply mkApps_nApp_inj.
  - rewrite → 2!isApp_false_nApp by assumption. reflexivity.
  - assumption.
Qed.

Definition head x := (decompose_app x).1.
Definition arguments x := (decompose_app x).2.

Lemma head_arguments x : mkApps (head x) (arguments x) = x.
Proof.
  unfold head, arguments, decompose_app.
  remember (decompose_app_rec x []).
  destruct p as [f l].
  symmetry in Heqp.
  eapply decompose_app_rec_inv in Heqp.
  now simpl in ×.
Qed.

Lemma fst_decompose_app_rec t l : fst (decompose_app_rec t l) = fst (decompose_app t).
Proof.
  induction t in l |- *; simpl; auto. rewrite IHt1.
  unfold decompose_app. simpl. now rewrite (IHt1 [t2]).
Qed.

Lemma decompose_app_rec_head t l f : fst (decompose_app_rec t l) = f
  negb (isApp f).
Proof.
  induction t; unfold isApp; simpl; try intros [= <-]; auto.
  intros. apply IHt1. now rewrite !fst_decompose_app_rec.
Qed.

Lemma head_nApp x : negb (isApp (head x)).
Proof.
  unfold head.
  eapply decompose_app_rec_head. reflexivity.
Qed.

Lemma head_tapp t1 t2 : head (tApp t1 t2) = head t1.
Proof. rewrite /head /decompose_app /= fst_decompose_app_rec //. Qed.

Lemma mkApps_Fix_spec mfix idx args t : mkApps (tFix mfix idx) args = t
                                        match decompose_app t with
                                        | (tFix mfix idx, args')args' = args
                                        | _False
                                        end.
Proof.
  intros H; apply (f_equal decompose_app) in H.
  rewrite decompose_app_mkApps in H. reflexivity.
  destruct t; noconf H. rewrite <- H. reflexivity.
  simpl. reflexivity.
Qed.

Lemma decompose_app_rec_tFix mfix idx args t l :
  decompose_app_rec t l = (tFix mfix idx, args) mkApps t l = mkApps (tFix mfix idx) args.
Proof.
  unfold decompose_app.
  revert l args.
  induction t; intros args l' H; noconf H. simpl in H.
  now specialize (IHt1 _ _ H).
  reflexivity.
Qed.

Lemma decompose_app_tFix mfix idx args t :
  decompose_app t = (tFix mfix idx, args) t = mkApps (tFix mfix idx) args.
Proof. apply decompose_app_rec_tFix. Qed.

Lemma mkApps_eq_head {x l} : mkApps x l = x l = [].
Proof.
  assert (WF : WellFounded (precompose lt PCUICSize.size))
    by apply wf_precompose, lt_wf.
  induction l. simpl. constructor.
  apply apply_noCycle_right. simpl. red. rewrite size_mkApps. simpl. lia.
Qed.

Lemma mkApps_eq_inv {x y l} : x = mkApps y l size y size x.
Proof.
  assert (WF : WellFounded (precompose lt size))
    by apply wf_precompose, lt_wf.
  induction l in x, y |- ×. simpl. intros → ; constructor.
  simpl. intros. specialize (IHl _ _ H). simpl in IHl. lia.
Qed.

Lemma mkApps_eq_left x y l : mkApps x l = mkApps y l x = y.
Proof.
  induction l in x, y |- *; simpl. auto.
  intros. simpl in ×. specialize (IHl _ _ H). now noconf IHl.
Qed.

Lemma decompose_app_eq_right t l l' : decompose_app_rec t l = decompose_app_rec t l' l = l'.
Proof.
  induction t in l, l' |- *; simpl; intros [=]; auto.
  specialize (IHt1 _ _ H0). now noconf IHt1.
Qed.

Lemma mkApps_eq_right t l l' : mkApps t l = mkApps t l' l = l'.
Proof.
  intros. eapply (f_equal decompose_app) in H. unfold decompose_app in H.
  rewrite !decompose_app_rec_mkApps in H. apply decompose_app_eq_right in H.
  now rewrite !app_nil_r in H.
Qed.

Lemma atom_decompose_app t l : ~~ isApp t decompose_app_rec t l = pair t l.
Proof. destruct t; simpl; congruence. Qed.

Lemma mkApps_eq_inj {t t' l l'} :
  mkApps t l = mkApps t' l'
  ~~ isApp t ~~ isApp t' t = t' l = l'.
Proof.
  intros Happ Ht Ht'. eapply (f_equal decompose_app) in Happ. unfold decompose_app in Happ.
  rewrite !decompose_app_rec_mkApps in Happ. rewrite !atom_decompose_app in Happ; auto.
  rewrite !app_nil_r in Happ. intuition congruence.
Qed.

Ltac solve_discr' :=
  match goal with
    H : mkApps _ _ = mkApps ?f ?l |- _
    eapply mkApps_eq_inj in H as [? ?]; [|easy|easy]; subst; try intuition congruence
  | H : ?t = mkApps ?f ?l |- _
    change t with (mkApps t []) in H ;
    eapply mkApps_eq_inj in H as [? ?]; [|easy|easy]; subst; try intuition congruence
  | H : mkApps ?f ?l = ?t |- _
    change t with (mkApps t []) in H ;
    eapply mkApps_eq_inj in H as [? ?]; [|easy|easy]; subst; try intuition congruence
  end.

Lemma mkApps_eq_decompose_app {t t' l l'} :
  mkApps t l = mkApps t' l'
  decompose_app_rec t l = decompose_app_rec t' l'.
Proof.
  induction l in t, t', l' |- *; simpl.
  - intros →. rewrite !decompose_app_rec_mkApps.
    now rewrite app_nil_r.
  - intros H. apply (IHl _ _ _ H).
Qed.

Lemma mkApps_eq_decompose {f args t} :
  mkApps f args = t
  ~~ isApp f
  fst (decompose_app t) = f.
Proof.
  intros H Happ; apply (f_equal decompose_app) in H.
  rewrite decompose_app_mkApps in H. auto. rewrite <- H. reflexivity.
Qed.

Ltac finish_discr :=
  repeat match goal with
         | [ H : ?x = ?x |- _ ] ⇒ clear H
         | [ H : mkApps _ _ = mkApps _ _ |- _ ] ⇒
           let H0 := fresh in let H1 := fresh in
                              specialize (mkApps_eq_inj H eq_refl eq_refl) as [H0 H1];
                              clear H;
                              try (congruence || (noconf H0; noconf H1))
         | [ H : mkApps _ _ = _ |- _ ] ⇒ apply mkApps_eq_head in H
         end.

Ltac prepare_discr :=
  repeat match goal with
         | [ H : mkApps ?f ?l = tApp ?y ?r |- _ ] ⇒ change (mkApps f l = mkApps y [r]) in H
         | [ H : tApp ?f ?l = mkApps ?y ?r |- _ ] ⇒ change (mkApps f [l] = mkApps y r) in H
         | [ H : mkApps ?x ?l = ?y |- _ ] ⇒
           match y with
           | mkApps _ _fail 1
           | _change (mkApps x l = mkApps y []) in H
           end
         | [ H : ?x = mkApps ?y ?l |- _ ] ⇒
           match x with
           | mkApps _ _fail 1
           | _change (mkApps x [] = mkApps y l) in H
           end
         end.

Inductive mkApps_spec : term list term term list term term Type :=
| mkApps_intro f l n :
    ~~ isApp f
    mkApps_spec f l (mkApps f (firstn n l)) (skipn n l) (mkApps f l).

Lemma decompose_app_rec_eq f l :
  ~~ isApp f
  decompose_app_rec f l = (f, l).
Proof.
  destruct f; simpl; try discriminate; congruence.
Qed.

Lemma decompose_app_rec_inv' f l hd args :
  decompose_app_rec f l = (hd, args)
   n, ~~ isApp hd l = skipn n args f = mkApps hd (firstn n args).
Proof.
  destruct (isApp f) eqn:Heq.
  revert l args hd.
  induction f; try discriminate. intros.
  simpl in H.
  destruct (isApp f1) eqn:Hf1.
  2:{ rewrite decompose_app_rec_eq in H ⇒ //. now apply negbT.
      revert Hf1.
      inv H. 1. simpl. intuition auto. now eapply negbT. }
  destruct (IHf1 eq_refl _ _ _ H).
  clear IHf1.
   (S x); intuition auto. eapply (f_equal (skipn 1)) in H2.
  rewrite [l]H2. now rewrite skipn_skipn Nat.add_1_r.
  rewrite -Nat.add_1_r firstn_add H3 -H2.
  now rewrite -[tApp _ _](mkApps_app hd _ [f2]).
  rewrite decompose_app_rec_eq; auto. now apply negbT.
  move⇒ [] H →. subst f. 0. intuition auto.
  now apply negbT.
Qed.

Lemma mkApps_elim_rec t l l' :
  let app' := decompose_app_rec (mkApps t l) l' in
  mkApps_spec app'.1 app'.2 t (l ++ l') (mkApps t (l ++ l')).
Proof.
  destruct app' as [hd args] eqn:Heq.
  subst app'.
  rewrite decompose_app_rec_mkApps in Heq.
  have H := decompose_app_rec_inv' _ _ _ _ Heq.
  destruct H. simpl. destruct a as [isapp [Hl' Hl]].
  subst t.
  have H' := mkApps_intro hd args x. rewrite Hl'.
  rewrite -mkApps_app. now rewrite firstn_skipn.
Qed.

Lemma mkApps_elim t l :
  let app' := decompose_app (mkApps t l) in
  mkApps_spec app'.1 app'.2 t l (mkApps t l).
Proof.
  have H := @mkApps_elim_rec t l [].
  now rewrite app_nil_r in H.
Qed.

Lemma nisApp_mkApps {t l} : ~~ isApp (mkApps t l) ~~ isApp t l = [].
Proof.
  induction l in t |- *; simpl; auto.
  intros. destruct (IHl _ H). discriminate.
Qed.

Lemma mkApps_nisApp {t t' l} : mkApps t l = t' ~~ isApp t' t = t' l = [].
Proof.
  induction l in t |- *; simpl; auto.
  intros. destruct (IHl _ H). auto. subst. simpl in H0. discriminate.
Qed.

Lemma tApp_mkApps_inj f a f' l :
  tApp f a = mkApps f' l l []
  f = mkApps f' (removelast l) (a = last l a).
Proof.
  induction l in f' |- *; simpl; intros H. noconf H. intros Hf. congruence.
  intros . destruct l; simpl in ×. now noconf H.
  specialize (IHl _ H). forward IHl by congruence.
  apply IHl.
Qed.

Definition application_atom t :=
  match t with
  | tVar _
  | tSort _
  | tInd _ _
  | tConstruct _ _ _
  | tLambda _ _ _true
  | _false
  end.

Lemma application_atom_mkApps {t l} : application_atom (mkApps t l) application_atom t l = [].
Proof.
  induction l in t |- *; simpl; auto.
  intros. destruct (IHl _ H). discriminate.
Qed.

Ltac solve_discr :=
  (try (progress (prepare_discr; finish_discr; cbn [mkApps] in × )));
  (try (match goal with
        | [ H : is_true (application_atom _) |- _ ] ⇒ discriminate
        | [ H : is_true (application_atom (mkApps _ _)) |- _ ] ⇒
          destruct (application_atom_mkApps H); subst; try discriminate
        end)).

Use a coercion for this common projection of the global context.
Definition fst_ctx : global_env_ext global_env := fst.
Coercion fst_ctx : global_env_ext >-> global_env.

Definition empty_ext (Σ : global_env) : global_env_ext
  := (Σ, Monomorphic_ctx).

Lemma destArity_app_aux {Γ Γ' t}
  : destArity (Γ ,,, Γ') t = option_map (fun '(ctx, s)(Γ ,,, ctx, s))
                                        (destArity Γ' t).
Proof.
  revert Γ'.
  induction t; cbn; intro Γ'; try reflexivity.
  - rewrite <- app_context_cons. now eapply IHt2.
  - rewrite <- app_context_cons. now eapply IHt3.
Qed.

Lemma destArity_app {Γ t}
  : destArity Γ t = option_map (fun '(ctx, s)(Γ ,,, ctx, s))
                               (destArity [] t).
Proof.
  exact (@destArity_app_aux Γ [] t).
Qed.

Lemma destArity_app_Some {Γ t ctx s}
  : destArity Γ t = Some (ctx, s)
     ctx', destArity [] t = Some (ctx', s) ctx = Γ ,,, ctx'.
Proof.
  intros H. rewrite destArity_app in H.
  destruct (destArity [] t) as [[ctx' s']|]; cbn in ×.
   ctx'. inversion H. now subst.
  discriminate H.
Qed.

Lemma destArity_it_mkProd_or_LetIn ctx ctx' t :
  destArity ctx (it_mkProd_or_LetIn ctx' t) =
  destArity (ctx ,,, ctx') t.
Proof.
  induction ctx' in ctx, t |- *; simpl; auto.
  rewrite IHctx'. destruct a as [na [b|] ty]; reflexivity.
Qed.

Lemma mkApps_nonempty f l :
  l [] mkApps f l = tApp (mkApps f (removelast l)) (last l f).
Proof.
  destruct l using rev_ind. intros; congruence.
  intros. rewrite mkApps_app. simpl. f_equal.
  rewrite removelast_app. congruence. simpl. now rewrite app_nil_r.
  rewrite last_app. congruence.
  reflexivity.
Qed.

Lemma destArity_tFix {mfix idx args} :
  destArity [] (mkApps (tFix mfix idx) args) = None.
Proof.
  induction args. reflexivity.
  rewrite mkApps_nonempty.
  intros e; discriminate e.
  reflexivity.
Qed.

Lemma destArity_tApp {t u l} :
  destArity [] (mkApps (tApp t u) l) = None.
Proof.
  induction l. reflexivity.
  rewrite mkApps_nonempty.
  intros e; discriminate e.
  reflexivity.
Qed.

Lemma destArity_tInd {t u l} :
  destArity [] (mkApps (tInd t u) l) = None.
Proof.
  induction l. reflexivity.
  rewrite mkApps_nonempty.
  intros e; discriminate e.
  reflexivity.
Qed.

Lemma destArity_mkApps_None ctx t l :
  destArity ctx t = None destArity ctx (mkApps t l) = None.
Proof.
  induction l in t |- ×. trivial.
  intros H. cbn. apply IHl. reflexivity.
Qed.

Lemma destArity_mkApps_Ind ctx ind u l :
  destArity ctx (mkApps (tInd ind u) l) = None.
Proof.
  apply destArity_mkApps_None. reflexivity.
Qed.


Section MapInP.
  Context {A B : Type}.
  Context {P : A Type}.
  Context (f : (x : A), P x B).

  Equations map_InP (l : list A) (H : x, In x l P x) : list B :=
  map_InP nil _ := nil;
  map_InP (cons x xs) H := cons (f x (H x (or_introl eq_refl))) (map_InP xs (fun x inxH x _)).
End MapInP.

Lemma map_InP_spec {A B : Type} {P : A Type} (f : A B) (l : list A) (H : x, In x l P x) :
  map_InP (fun (x : A) (_ : P x) ⇒ f x) l H = List.map f l.
Proof.
  remember (fun (x : A) (_ : P x) ⇒ f x) as g.
  funelim (map_InP g l H) ⇒ //; simpl. f_equal.
  now rewrite H0.
Qed.

Lemma nth_error_map_InP {A B : Type} {P : A Type} (f : x : A, P x B) (l : list A) (H : x, In x l P x) n x :
  nth_error (map_InP f l H) n = Some x
   a, (nth_error l n = Some a) ×
   p : P a, x = f a p.
Proof.
  induction l in n, H |- ×. simpl. rewrite nth_error_nil ⇒ //.
  destruct n; simpl; intros [=].
  subst x.
  eexists; intuition eauto.
  eapply IHl. eapply H1.
Qed.

Lemma map_InP_length {A B : Type} {P : A Type} (f : x : A, P x B) (l : list A) (H : x, In x l P x) :
  #|map_InP f l H| = #|l|.
Proof.
  induction l; simpl; auto.
Qed.
#[global]
Hint Rewrite @map_InP_length : len.

Views

Definition isSort T :=
  match T with
  | tSort utrue
  | _false
  end.

Inductive view_sort : term Type :=
| view_sort_sort s : view_sort (tSort s)
| view_sort_other t : ¬ isSort t view_sort t.

Equations view_sortc (t : term) : view_sort t :=
  view_sortc (tSort s) := view_sort_sort s;
  view_sortc t := view_sort_other t _.

Definition isProd t :=
  match t with
  | tProd na A Btrue
  | _false
  end.

Inductive view_prod : term Type :=
| view_prod_prod na A b : view_prod (tProd na A b)
| view_prod_other t : ¬ isProd t view_prod t.

Equations view_prodc (t : term) : view_prod t :=
  view_prodc (tProd na A b) := view_prod_prod na A b;
  view_prodc t := view_prod_other t _.

Definition isInd (t : term) : bool :=
  match t with
  | tInd _ _true
  | _false
  end.

Inductive view_ind : term Type :=
| view_ind_tInd ind u : view_ind (tInd ind u)
| view_ind_other t : negb (isInd t) view_ind t.

Equations view_indc (t : term) : view_ind t :=
  view_indc (tInd ind u) ⇒ view_ind_tInd ind u;
  view_indc tview_ind_other t _.

Inductive view_prod_sort : term Type :=
| view_prod_sort_prod na A B : view_prod_sort (tProd na A B)
| view_prod_sort_sort u : view_prod_sort (tSort u)
| view_prod_sort_other t :
    ¬isProd t
    ¬isSort t
    view_prod_sort t.

Equations view_prod_sortc (t : term) : view_prod_sort t := {
  | tProd na A Bview_prod_sort_prod na A B;
  | tSort uview_prod_sort_sort u;
  | tview_prod_sort_other t _ _
  }.

Lemma nth_error_ass_subst_context s k Γ :
  ( n d, nth_error Γ n = Some d decl_body d = None)
   n d, nth_error (subst_context s k Γ) n = Some d decl_body d = None.
Proof.
  induction Γ as [|[? [] ?] ?] in |- *; simpl; auto;
  intros; destruct n; simpl in *; rewrite ?subst_context_snoc in H0; simpl in H0.
  - noconf H0; simpl.
    specialize (H 0 _ eq_refl). simpl in H; discriminate.
  - specialize (H 0 _ eq_refl). simpl in H; discriminate.
  - noconf H0; simpl. auto.
  - eapply IHΓ; intros; eauto.
    now specialize (H (S n0) d0 H1).
Qed.

Lemma nth_error_smash_context Γ Δ :
  ( n d, nth_error Δ n = Some d decl_body d = None)
   n d, nth_error (smash_context Δ Γ) n = Some d decl_body d = None.
Proof.
  induction Γ as [|[? [] ?] ?] in Δ |- *; simpl; auto.
  - intros. eapply (IHΓ (subst_context [t] 0 Δ)); tea.
    now apply nth_error_ass_subst_context.
  - intros. eapply IHΓ. 2:eauto.
    intros.
    pose proof (nth_error_Some_length H1). autorewrite with len in H2. simpl in H2.
    destruct (eq_dec n0 #|Δ|).
    × subst.
      rewrite nth_error_app_ge in H1; try lia.
      rewrite Nat.sub_diag /= in H1. noconf H1.
      reflexivity.
    × rewrite nth_error_app_lt in H1; try lia. eauto.
Qed.

Lemma context_assumptions_smash_context Δ Γ :
  context_assumptions (smash_context Δ Γ) =
  context_assumptions Δ + context_assumptions Γ.
Proof.
  induction Γ as [|[? [] ?] ?] in Δ |- *; simpl; auto;
  rewrite IHΓ.
  - now rewrite context_assumptions_fold.
  - rewrite context_assumptions_app /=. lia.
Qed.

Lemma context_assumptions_expand_lets_ctx Γ Δ :
  context_assumptions (expand_lets_ctx Γ Δ) = context_assumptions Δ.
Proof. now rewrite /expand_lets_ctx /expand_lets_k_ctx; len. Qed.
#[global]
Hint Rewrite context_assumptions_expand_lets_ctx : len.