Library MetaCoq.PCUIC.PCUICCasesContexts

From Coq Require Import Utf8 ssreflect ssrbool.
From MetaCoq.Template Require Import config utils.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICInduction
     PCUICLiftSubst PCUICEquality PCUICSigmaCalculus.

Require Import Equations.Type.Relation_Properties.
Require Import Equations.Prop.DepElim.
From Equations Require Import Equations.

Local Set SimplIsCbn.

Implicit Types (cf : checker_flags) (Σ : global_env_ext).

Lemma map2_set_binder_name_alpha_eq (nas : list aname) (Δ Δ' : PCUICEnvironment.context) :
  All2 (fun x y ⇒ x = (decl_name y)) nas Δ' →
  eq_context_upto_names Δ Δ' →
  (map2 set_binder_name nas Δ) = Δ'.
Proof.
  intros hl. induction 1 in nas, hl |- *; cbn; auto.
  destruct nas; cbn; auto.
  destruct nas; cbn; auto; depelim hl.
  f_equal; auto. destruct r; subst; cbn; auto.
Qed.
Notation eq_names := (All2 (fun x y ⇒ x = (decl_name y))).

Lemma eq_names_subst_context nas Γ s k :
  eq_names nas Γ →
  eq_names nas (subst_context s k Γ).
Proof.
  induction 1.
  × rewrite subst_context_nil. constructor.
  × rewrite subst_context_snoc. constructor; auto.
Qed.

Lemma eq_names_subst_instance nas Γ u :
  eq_names nas Γ →
  eq_names nas (subst_instance u Γ).
Proof.
  induction 1.
  × constructor.
  × rewrite /subst_instance /=. constructor; auto.
Qed.

Lemma alpha_eq_subst_instance Δ Δ' i :
  eq_context_upto_names Δ Δ' →
  eq_context_upto_names Δ@[i] Δ'@[i].
Proof.
  induction 1.
  × constructor.
  × cbn. constructor; auto. destruct r; constructor; auto.
    all:cbn; subst; reflexivity.
Qed.

Lemma alpha_eq_context_assumptions Δ Δ' :
  eq_context_upto_names Δ Δ' →
  context_assumptions Δ = context_assumptions Δ'.
Proof.
  induction 1; simpl; auto; try lia.
  destruct r; simpl; auto; lia.
Qed.

Lemma alpha_eq_extended_subst Δ Δ' k :
  eq_context_upto_names Δ Δ' →
  extended_subst Δ k = extended_subst Δ' k.
Proof.
  induction 1 in k |- *; simpl; auto.
  destruct r; subst; simpl; auto. f_equal. apply IHX.
  rewrite IHX (alpha_eq_context_assumptions l l') //.
Qed.

Lemma alpha_eq_smash_context Δ Δ' :
  eq_context_upto_names Δ Δ' →
  eq_context_upto_names (smash_context [] Δ) (smash_context [] Δ').
Proof.
  induction 1.
  × constructor.
  × destruct x; depelim r; simpl; auto.
    rewrite !(smash_context_acc _ [_]).
    eapply All2_app; auto; repeat constructor; subst; simpl; auto.
    rewrite (All2_length X) -(alpha_eq_extended_subst l l' 0) // (alpha_eq_context_assumptions l l') //.
Qed.

Lemma alpha_eq_lift_context n k Δ Δ' :
  eq_context_upto_names Δ Δ' →
  eq_context_upto_names (lift_context n k Δ) (lift_context n k Δ').
Proof.
  induction 1.
  × constructor.
  × rewrite !lift_context_snoc; destruct x; depelim r; simpl; subst; auto;
    constructor; auto; repeat constructor; subst; simpl; auto;
    now rewrite (All2_length X).
Qed.

Lemma alpha_eq_subst_context s k Δ Δ' :
  eq_context_upto_names Δ Δ' →
  eq_context_upto_names (subst_context s k Δ) (subst_context s k Δ').
Proof.
  induction 1.
  × constructor.
  × rewrite !subst_context_snoc; destruct x; depelim r; simpl; subst; auto;
    constructor; auto; repeat constructor; subst; simpl; auto;
    now rewrite (All2_length X).
Qed.

Lemma inst_case_predicate_context_eq {mdecl idecl ind p} :
  eq_context_upto_names p.(pcontext) (ind_predicate_context ind mdecl idecl) →
  case_predicate_context ind mdecl idecl p =
  inst_case_predicate_context p.
Proof.
  intros a.
  eapply map2_set_binder_name_alpha_eq.
  { eapply eq_names_subst_context, eq_names_subst_instance.
    eapply All2_map_left. eapply All2_refl. reflexivity. }
  { apply alpha_eq_subst_context, alpha_eq_subst_instance.
    now symmetry. }
Qed.

Definition ind_binder ind idecl p :=
  let indty :=
    mkApps (tInd ind p.(puinst))
            (map (lift0 #|ind_indices idecl|) p.(pparams) ++ to_extended_list (ind_indices idecl)) in
  {| decl_name := {|
               binder_name := nNamed (ind_name idecl);
               binder_relevance := ind_relevance idecl |};
  decl_body := None;
  decl_type := indty |}.

Definition case_predicate_context' ind mdecl idecl p :=
    ind_binder ind idecl p :: subst_context (List.rev p.(pparams)) 0
    (subst_instance p.(puinst)
       (expand_lets_ctx (ind_params mdecl) (ind_indices idecl))).

Lemma eq_binder_annots_eq nas Γ :
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) nas Γ →
  eq_context_upto_names (map2 set_binder_name nas Γ) Γ.
Proof.
  induction 1; simpl; constructor; auto.
  destruct x, y as [na [b|] ty]; simpl; constructor; auto.
Qed.

Definition pre_case_branch_context (ind : inductive) (mdecl : mutual_inductive_body)
  (params : list term) (puinst : Instance.t) (cdecl : constructor_body) :=
  subst_context (List.rev params) 0
  (expand_lets_ctx (subst_instance puinst (ind_params mdecl))
         (subst_context (inds (inductive_mind ind) puinst (ind_bodies mdecl))
        #|ind_params mdecl|
        (subst_instance puinst (cstr_args cdecl)))).

Lemma pre_case_branch_context_length_args {ind mdecl params puinst cdecl} :
  #|pre_case_branch_context ind mdecl params puinst cdecl| = #|cstr_args cdecl|.
Proof.
  now rewrite /pre_case_branch_context; len.
Qed.

Lemma All2_eq_binder_subst_context (l : list (binder_annot name)) s k Γ :
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) l Γ →
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) l (subst_context s k Γ).
Proof.
  induction 1; rewrite ?subst_context_snoc //; constructor; auto.
Qed.

Lemma All2_eq_binder_subst_instance (l : list (binder_annot name)) u (Γ : context) :
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) l Γ →
  All2 (fun x y ⇒ eq_binder_annot x y.(decl_name)) l (subst_instance u Γ).
Proof.
  induction 1; rewrite ?subst_context_snoc //; constructor; auto.
Qed.

Lemma inst_case_branch_context_eq {ind mdecl cdecl p br} :
  eq_context_upto_names br.(bcontext) (cstr_branch_context ind mdecl cdecl) →
  case_branch_context ind mdecl p (forget_types br.(bcontext)) cdecl = inst_case_branch_context p br.
Proof.
  intros.
  rewrite /case_branch_context /case_branch_context_gen.
  rewrite /inst_case_branch_context /inst_case_context.
  eapply map2_set_binder_name_alpha_eq.
  eapply eq_names_subst_context, eq_names_subst_instance.
  eapply All2_map_left. eapply All2_refl. reflexivity.
  rewrite /pre_case_branch_context_gen /inst_case_context.
  eapply alpha_eq_subst_context, alpha_eq_subst_instance.
  now symmetry.
Qed.