From Coq Require Import ssreflect Morphisms.
From MetaCoq.Template Require Export utils Universes BasicAst Environment Reflect.
From MetaCoq.Template Require EnvironmentTyping.
From MetaCoq.PCUIC Require Export PCUICPrimitive.
From Equations Require Import Equations.

Declare Scope pcuic.
Delimit Scope pcuic with pcuic.
Open Scope pcuic.

Ltac pcuicfo_gen tac :=
  simpl in *; intuition (simpl; intuition tac).

Tactic Notation "pcuicfo" := pcuicfo_gen auto.
Tactic Notation "pcuicfo" tactic(tac) := pcuicfo_gen tac.

Class HasLen (A : Type) (x y : nat) := len : A → x = y.

Notation length_of t := ltac:(let lemma := constr:(PCUICAst.len t) in exact lemma) (only parsing).

Record predicate {term} := mk_predicate {
  pparams : list term;
  puinst : Instance.t;
  pcontext : list (context_decl term);
    
  preturn : term; }.
Derive NoConfusion for predicate.
Arguments predicate : clear implicits.
Arguments mk_predicate {_}.

Section map_predicate.
  Context {term term' : Type}.
  Context (uf : Instance.t → Instance.t).
  Context (paramf preturnf : term → term').
  Context (pcontextf : list (context_decl term) → list (context_decl term')).

  Definition map_predicate (p : predicate term) :=
    {| pparams := map paramf p.(pparams);
        puinst := uf p.(puinst);
        pcontext := pcontextf p.(pcontext);
        preturn := preturnf p.(preturn) |}.

  Lemma map_pparams (p : predicate term) :
    map paramf (pparams p) = pparams (map_predicate p).
  Proof using Type. reflexivity. Qed.

  Lemma map_preturn (p : predicate term) :
    preturnf (preturn p) = preturn (map_predicate p).
  Proof using Type. reflexivity. Qed.

  Lemma map_pcontext (p : predicate term) :
    pcontextf (pcontext p) = pcontext (map_predicate p).
  Proof using Type. reflexivity. Qed.

  Lemma map_puinst (p : predicate term) :
    uf (puinst p) = puinst (map_predicate p).
  Proof using Type. reflexivity. Qed.

End map_predicate.

Definition shiftf {A B} (f : nat → A → B) k := (fun k' ⇒ f (k' + k)).

Section map_predicate_k.
  Context {term : Type}.
  Context (uf : Instance.t → Instance.t).
  Context (f : nat → term → term).

  Definition map_predicate_k k (p : predicate term) :=
    {| pparams := map (f k) p.(pparams);
        puinst := uf p.(puinst);
        pcontext := p.(pcontext);
        preturn := f (#|p.(pcontext)| + k) p.(preturn) |}.

  Lemma map_k_pparams k (p : predicate term) :
    map (f k) (pparams p) = pparams (map_predicate_k k p).
  Proof using Type. reflexivity. Qed.

  Lemma map_k_preturn k (p : predicate term) :
    f (#|p.(pcontext)| + k) (preturn p) = preturn (map_predicate_k k p).
  Proof using Type. reflexivity. Qed.

  Lemma map_k_pcontext k (p : predicate term) :
    (pcontext p) = pcontext (map_predicate_k k p).
  Proof using Type. reflexivity. Qed.

  Lemma map_k_puinst k (p : predicate term) :
    uf (puinst p) = puinst (map_predicate_k k p).
  Proof using Type. reflexivity. Qed.

  Definition test_predicate (instp : Instance.t → bool) (p : term → bool)
    (pred : predicate term) :=
    instp pred.(puinst) && forallb p pred.(pparams) &&
    test_context p pred.(pcontext) && p pred.(preturn).

  Definition test_predicate_k (instp : Instance.t → bool)
    (p : nat → term → bool) k (pred : predicate term) :=
    instp pred.(puinst) && forallb (p k) pred.(pparams) &&
    test_context_k p #|pred.(pparams)| pred.(pcontext) &&
    p (#|pred.(pcontext)| + k) pred.(preturn).

  Definition test_predicate_ku (instp : nat → Instance.t → bool)
    (p : nat → term → bool) k (pred : predicate term) :=
    instp k pred.(puinst) && forallb (p k) pred.(pparams) &&
    test_context (p #|pred.(puinst)|) pred.(pcontext) &&
    p k pred.(preturn).

End map_predicate_k.

Section Branch.
  Context {term : Type}.
  Record branch := mk_branch {
    bcontext : list (context_decl term);
    
    bbody : term; }.
  Derive NoConfusion for branch.

  Definition string_of_branch (f : term → string) (b : branch) :=
  "([" ^ String.concat "," (map (string_of_name ∘ binder_name ∘ decl_name) (bcontext b)) ^ "], "
  ^ f (bbody b) ^ ")".

  Definition pretty_string_of_branch (f : term → string) (b : branch) :=
    String.concat " " (map (string_of_name ∘ binder_name ∘ decl_name) (bcontext b)) ^ " => " ^ f (bbody b).

  Definition test_branch (pctx : term → bool) (p : term → bool) (b : branch) :=
    test_context pctx b.(bcontext) && p b.(bbody).

  Definition test_branch_k (pred : predicate term) (p : nat → term → bool) k (b : branch) :=
    test_context_k p #|pred.(pparams)| b.(bcontext) && p (#|b.(bcontext)| + k) b.(bbody).

End Branch.
Arguments branch : clear implicits.

Section map_branch.
  Context {term term' : Type}.
  Context (f : term → term').
  Context (g : list (BasicAst.context_decl term) → list (BasicAst.context_decl term')).

  Definition map_branch (b : branch term) :=
  {| bcontext := g b.(bcontext);
      bbody := f b.(bbody) |}.

  Lemma map_bbody (b : branch term) :
    f (bbody b) = bbody (map_branch b).
  Proof using Type. reflexivity. Qed.

  Lemma map_bcontext (b : branch term) :
    g (bcontext b) = bcontext (map_branch b).
  Proof using Type. reflexivity. Qed.
End map_branch.

Definition map_branches {term B} (f : term → B) h l := List.map (map_branch f h) l.

Section map_branch_k.
  Context {term term' : Type}.
  Context (f : nat → term → term').
  Context (g : list (BasicAst.context_decl term) → list (BasicAst.context_decl term')).
  Definition map_branch_k k (b : branch term) :=
  {| bcontext := g b.(bcontext);
     bbody := f (#|b.(bcontext)| + k) b.(bbody) |}.

  Lemma map_k_bbody k (b : branch term) :
    f (#|b.(bcontext)| + k) (bbody b) = bbody (map_branch_k k b).
  Proof using Type. reflexivity. Qed.

  Lemma map_k_bcontext k (b : branch term) :
    g (bcontext b) = bcontext (map_branch_k k b).
  Proof using Type. reflexivity. Qed.
End map_branch_k.

Notation map_branches_k f h k brs :=
  (List.map (map_branch_k f h k) brs).

Notation test_branches_k p test k brs :=
  (List.forallb (test_branch_k p test k) brs).

Inductive term :=
| tRel (n : nat)
| tVar (i : ident)
| tEvar (n : nat) (l : list term)
| tSort (u : Universe.t)
| tProd (na : aname) (A B : term)
| tLambda (na : aname) (A t : term)
| tLetIn (na : aname) (b B t : term)
| tApp (u v : term)
| tConst (k : kername) (ui : Instance.t)
| tInd (ind : inductive) (ui : Instance.t)
| tConstruct (ind : inductive) (n : nat) (ui : Instance.t)
| tCase (indn : case_info) (p : predicate term) (c : term) (brs : list (branch term))
| tProj (p : projection) (c : term)
| tFix (mfix : mfixpoint term) (idx : nat)
| tCoFix (mfix : mfixpoint term) (idx : nat).

Derive NoConfusion for term.

Notation prim_val := (prim_val term).

Fixpoint mkApps t us :=
  match us with
  | nil ⇒ t
  | u :: us ⇒ mkApps (tApp t u) us
  end.

Definition isApp t :=
  match t with
  | tApp _ _ ⇒ true
  | _ ⇒ false
  end.

Definition isLambda t :=
  match t with
  | tLambda _ _ _ ⇒ true
  | _ ⇒ false
  end.

Lemma isLambda_inv t : isLambda t → ∃ na ty bod, t = tLambda na ty bod.
Proof. destruct t ⇒ //; eauto. Qed.

Record parameter_entry := {
  parameter_entry_type : term;
  parameter_entry_universes : universes_decl }.

Record definition_entry := {
  definition_entry_type : term;
  definition_entry_body : term;
  definition_entry_universes : universes_decl;
  definition_entry_opaque : bool }.

Inductive constant_entry :=
| ParameterEntry (p : parameter_entry)
| DefinitionEntry (def : definition_entry).

Derive NoConfusion for parameter_entry definition_entry constant_entry.

Inductive local_entry :=
| LocalDef : term → local_entry
| LocalAssum : term → local_entry.

Record one_inductive_entry := {
  mind_entry_typename : ident;
  mind_entry_arity : term;
  mind_entry_template : bool;
  mind_entry_consnames : list ident;
  mind_entry_lc : list term }.

Record mutual_inductive_entry := {
  mind_entry_record : option (option ident);
  
  mind_entry_finite : recursivity_kind;
  mind_entry_params : list (ident × local_entry);
  mind_entry_inds : list one_inductive_entry;
  mind_entry_universes : universes_decl;
  mind_entry_private : option bool
   }.

Derive NoConfusion for local_entry one_inductive_entry mutual_inductive_entry.

Fixpoint lift n k t : term :=
  match t with
  | tRel i ⇒ tRel (if Nat.leb k i then (n + i) else i)
  | tEvar ev args ⇒ tEvar ev (List.map (lift n k) args)
  | tLambda na T M ⇒ tLambda na (lift n k T) (lift n (S k) M)
  | tApp u v ⇒ tApp (lift n k u) (lift n k v)
  | tProd na A B ⇒ tProd na (lift n k A) (lift n (S k) B)
  | tLetIn na b t b' ⇒ tLetIn na (lift n k b) (lift n k t) (lift n (S k) b')
  | tCase ind p c brs ⇒
    let p' := map_predicate_k id (lift n) k p in
    let brs' := map_branches_k (lift n) id k brs in
    tCase ind p' (lift n k c) brs'
  | tProj p c ⇒ tProj p (lift n k c)
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (lift n k) (lift n k')) mfix in
    tFix mfix' idx
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (lift n k) (lift n k')) mfix in
    tCoFix mfix' idx
  | x ⇒ x
  end.

Notation lift0 n := (lift n 0).

Fixpoint subst s k u :=
  match u with
  | tRel n ⇒
    if Nat.leb k n then
      match nth_error s (n - k) with
      | Some b ⇒ lift0 k b
      | None ⇒ tRel (n - List.length s)
      end
    else tRel n
  | tEvar ev args ⇒ tEvar ev (List.map (subst s k) args)
  | tLambda na T M ⇒ tLambda na (subst s k T) (subst s (S k) M)
  | tApp u v ⇒ tApp (subst s k u) (subst s k v)
  | tProd na A B ⇒ tProd na (subst s k A) (subst s (S k) B)
  | tLetIn na b ty b' ⇒ tLetIn na (subst s k b) (subst s k ty) (subst s (S k) b')
  | tCase ind p c brs ⇒
    let p' := map_predicate_k id (subst s) k p in
    let brs' := map_branches_k (subst s) id k brs in
    tCase ind p' (subst s k c) brs'
  | tProj p c ⇒ tProj p (subst s k c)
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (subst s k) (subst s k')) mfix in
    tFix mfix' idx
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    let mfix' := List.map (map_def (subst s k) (subst s k')) mfix in
    tCoFix mfix' idx
  | x ⇒ x
  end.

Notation subst0 t := (subst t 0).
Definition subst1 t k u := subst [t] k u.
Notation subst10 t := (subst1 t 0).
Notation "M { j := N }" := (subst1 N j M) (at level 10, right associativity).

Fixpoint closedn k (t : term) : bool :=
  match t with
  | tRel i ⇒ Nat.ltb i k
  | tEvar ev args ⇒ List.forallb (closedn k) args
  | tLambda _ T M | tProd _ T M ⇒ closedn k T && closedn (S k) M
  | tApp u v ⇒ closedn k u && closedn k v
  | tLetIn na b t b' ⇒ closedn k b && closedn k t && closedn (S k) b'
  | tCase ind p c brs ⇒
    let p' := test_predicate_k (fun _ ⇒ true) closedn k p in
    let brs' := test_branches_k p closedn k brs in
    p' && closedn k c && brs'
  | tProj p c ⇒ closedn k c
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    List.forallb (test_def (closedn k) (closedn k')) mfix
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    List.forallb (test_def (closedn k) (closedn k')) mfix
  | _ ⇒ true
  end.

Section fix_test.

Variable test : term → bool.

Fixpoint test_context_nlict (bcontext : list (context_decl term)) :=
  match bcontext with
  | nil ⇒ true
  | d :: bcontext ⇒ test_context_nlict bcontext &&
                     test (decl_type d) && match decl_body d with Some _ ⇒ false | None ⇒ true end
  end.

End fix_test.

Definition test_branch_nlict test b :=
  test_context_nlict test (bcontext b) && test (bbody b).

Definition test_branches_nlict test brs :=
  forallb (test_branch_nlict test) brs.

Fixpoint nlict (t : term) : bool :=
  match t with
  | tEvar ev args ⇒ List.forallb nlict args
  | tLambda _ T M | tProd _ T M ⇒ nlict T && nlict M
  | tApp u v ⇒ nlict u && nlict v
  | tLetIn na b t b' ⇒ nlict b && nlict t && nlict b'
  | tCase ind p c brs ⇒
    let p' := test_predicate_k (fun _ ⇒ true) (fun _ ⇒ nlict) 0 p in
    let brs' := test_branches_nlict nlict brs in
    p' && nlict c && brs'
  | tProj p c ⇒ nlict c
  | tFix mfix idx ⇒
    List.forallb (test_def nlict nlict) mfix
  | tCoFix mfix idx ⇒
    List.forallb (test_def nlict nlict) mfix
  | _ ⇒ true
  end.

Notation closed t := (closedn 0 t).
Notation closed_decl n := (test_decl (closedn n)).
Notation closedn_ctx := (test_context_k closedn).
Notation closed_ctx := (closedn_ctx 0).

Fixpoint noccur_between k n (t : term) : bool :=
  match t with
  | tRel i ⇒ Nat.ltb i k || Nat.leb (k + n) i
  | tEvar ev args ⇒ List.forallb (noccur_between k n) args
  | tLambda _ T M | tProd _ T M ⇒ noccur_between k n T && noccur_between (S k) n M
  | tApp u v ⇒ noccur_between k n u && noccur_between k n v
  | tLetIn na b t b' ⇒ noccur_between k n b && noccur_between k n t && noccur_between (S k) n b'
  | tCase ind p c brs ⇒
    let p' := test_predicate_k (fun _ ⇒ true) (fun k' ⇒ noccur_between k' n) k p in
    let brs' := test_branches_k p (fun k ⇒ noccur_between k n) k brs in
    p' && noccur_between k n c && brs'
  | tProj p c ⇒ noccur_between k n c
  | tFix mfix idx ⇒
    let k' := List.length mfix + k in
    List.forallb (test_def (noccur_between k n) (noccur_between k' n)) mfix
  | tCoFix mfix idx ⇒
    let k' := List.length mfix + k in
    List.forallb (test_def (noccur_between k n) (noccur_between k' n)) mfix
  | _ ⇒ true
  end.

#[global]
Instance subst_instance_constr : UnivSubst term :=
  fix subst_instance_constr u c {struct c} : term :=
  match c with
  | tRel _ | tVar _ ⇒ c
  | tEvar ev args ⇒ tEvar ev (List.map (subst_instance_constr u) args)
  | tSort s ⇒ tSort (subst_instance_univ u s)
  | tConst c u' ⇒ tConst c (subst_instance_instance u u')
  | tInd i u' ⇒ tInd i (subst_instance_instance u u')
  | tConstruct ind k u' ⇒ tConstruct ind k (subst_instance_instance u u')
  | tLambda na T M ⇒ tLambda na (subst_instance_constr u T) (subst_instance_constr u M)
  | tApp f v ⇒ tApp (subst_instance_constr u f) (subst_instance_constr u v)
  | tProd na A B ⇒ tProd na (subst_instance_constr u A) (subst_instance_constr u B)
  | tLetIn na b ty b' ⇒ tLetIn na (subst_instance_constr u b) (subst_instance_constr u ty)
                                (subst_instance_constr u b')
  | tCase ind p c brs ⇒
    let p' := map_predicate (subst_instance_instance u) (subst_instance_constr u) (subst_instance_constr u) id p in
    let brs' := List.map (map_branch (subst_instance_constr u) id) brs in
    tCase ind p' (subst_instance_constr u c) brs'
  | tProj p c ⇒ tProj p (subst_instance_constr u c)
  | tFix mfix idx ⇒
    let mfix' := List.map (map_def (subst_instance_constr u) (subst_instance_constr u)) mfix in
    tFix mfix' idx
  | tCoFix mfix idx ⇒
    let mfix' := List.map (map_def (subst_instance_constr u) (subst_instance_constr u)) mfix in
    tCoFix mfix' idx
  
  end.

Fixpoint closedu (k : nat) (t : term) : bool :=
  match t with
  | tSort univ ⇒ closedu_universe k univ
  | tInd _ u ⇒ closedu_instance k u
  | tConstruct _ _ u ⇒ closedu_instance k u
  | tConst _ u ⇒ closedu_instance k u
  | tRel i ⇒ true
  | tEvar ev args ⇒ forallb (closedu k) args
  | tLambda _ T M | tProd _ T M ⇒ closedu k T && closedu k M
  | tApp u v ⇒ closedu k u && closedu k v
  | tLetIn na b t b' ⇒ closedu k b && closedu k t && closedu k b'
  | tCase ind p c brs ⇒
    let p' := test_predicate_ku closedu_instance closedu k p in
    let brs' := forallb (test_branch (closedu #|p.(puinst)|) (closedu k)) brs in
    p' && closedu k c && brs'
  | tProj p c ⇒ closedu k c
  | tFix mfix idx ⇒
    forallb (test_def (closedu k) (closedu k)) mfix
  | tCoFix mfix idx ⇒
    forallb (test_def (closedu k) (closedu k)) mfix
  | _ ⇒ true
  end.

Module PCUICTerm <: Term.

  Definition term := term.

  Definition tRel := tRel.
  Definition tSort := tSort.
  Definition tProd := tProd.
  Definition tLambda := tLambda.
  Definition tLetIn := tLetIn.
  Definition tInd := tInd.
  Definition tProj := tProj.
  Definition mkApps := mkApps.

  Definition lift := lift.
  Definition subst := subst.
  Definition closedn := closedn.
  Definition noccur_between := noccur_between.
  Definition subst_instance_constr := subst_instance.
End PCUICTerm.

Module PCUICEnvironment := Environment PCUICTerm.
Export PCUICEnvironment.

Fixpoint destArity Γ (t : term) :=
  match t with
  | tProd na t b ⇒ destArity (Γ ,, vass na t) b
  | tLetIn na b b_ty b' ⇒ destArity (Γ ,, vdef na b b_ty) b'
  | tSort s ⇒ Some (Γ, s)
  | _ ⇒ None
  end.

Definition inds ind u (l : list one_inductive_body) :=
  let fix aux n :=
      match n with
      | 0 ⇒ []
      | S n ⇒ tInd (mkInd ind n) u :: aux n
      end
  in aux (List.length l).

Module PCUICTermUtils <: TermUtils PCUICTerm PCUICEnvironment.

Definition destArity := destArity.
Definition inds := inds.

End PCUICTermUtils.

Ltac unf_term := unfold PCUICTerm.term in *; unfold PCUICTerm.tRel in *;
                 unfold PCUICTerm.tSort in *; unfold PCUICTerm.tProd in *;
                 unfold PCUICTerm.tLambda in *; unfold PCUICTerm.tLetIn in *;
                 unfold PCUICTerm.tInd in *; unfold PCUICTerm.tProj in *;
                 unfold PCUICTerm.lift in *; unfold PCUICTerm.subst in *;
                 unfold PCUICTerm.closedn in *; unfold PCUICTerm.noccur_between in *;
                 unfold PCUICTerm.subst_instance_constr in *;
                 unfold PCUICTermUtils.destArity in *; unfold PCUICTermUtils.inds in ×.

Lemma context_assumptions_mapi_context f (ctx : context) :
  context_assumptions (mapi_context f ctx) = context_assumptions ctx.
Proof.
  now rewrite mapi_context_fold; len.
Qed.
#[global]
Hint Rewrite context_assumptions_mapi_context : len.

Module PCUICEnvTyping := EnvironmentTyping.EnvTyping PCUICTerm PCUICEnvironment PCUICTermUtils.

Module PCUICConversion := EnvironmentTyping.Conversion PCUICTerm PCUICEnvironment PCUICTermUtils PCUICEnvTyping.

Global Instance context_reflect`(ReflectEq term) :
  ReflectEq (list (BasicAst.context_decl term)) := _.

Local Ltac finish :=
  let h := fresh "h" in
  right ;
  match goal with
  | e : ?t ≠ ?u |- _ ⇒
    intro h ; apply e ; now inversion h
  end.

Local Ltac fcase c :=
  let e := fresh "e" in
  case c ; intro e ; [ subst ; try (left ; reflexivity) | finish ].

Definition string_of_predicate {term} (f : term → string) (p : predicate term) :=
  "(" ^ "(" ^ String.concat "," (map f (pparams p)) ^ ")"
  ^ "," ^ string_of_universe_instance (puinst p)
  ^ ",(" ^ String.concat "," (map (string_of_name ∘ binder_name ∘ decl_name) (pcontext p)) ^ ")"
  ^ "," ^ f (preturn p) ^ ")".

Definition eqb_predicate_gen (eqb_univ_instance : Instance.t → Instance.t → bool)
  (eqdecl : context_decl → context_decl → bool)
  (eqterm : term → term → bool) (p p' : predicate term) :=
  forallb2 eqterm p.(pparams) p'.(pparams) &&
  eqb_univ_instance p.(puinst) p'.(puinst) &&
  forallb2 eqdecl p.(pcontext) p'.(pcontext) &&
  eqterm p.(preturn) p'.(preturn).

Definition eqb_predicate (eqterm : term → term → bool) (p p' : predicate term) :=
  eqb_predicate_gen eqb (eqb_context_decl eqterm) eqterm p p'.

#[global]
Hint Rewrite map_map_compose @compose_map_def map_length : map.

#[global]
Hint Rewrite @forallb_map : map.

Lemma map_predicate_map_predicate
      {term term' term''}
      (finst finst' : Instance.t → Instance.t)
      (f g : term' → term'')
      (f' g' : term → term')
      (h : list (BasicAst.context_decl term') → list (BasicAst.context_decl term''))
      (h' : list (BasicAst.context_decl term) → list (BasicAst.context_decl term'))
      (p : predicate term) :
  map_predicate finst f g h (map_predicate finst' f' g' h' p) =
  map_predicate (finst ∘ finst') (f ∘ f') (g ∘ g') (h ∘ h') p.
Proof.
  unfold map_predicate. destruct p; cbn.
  f_equal.
  apply map_map.
Qed.

Lemma map_predicate_id x : map_predicate (@id _) (@id term) (@id term) (@id _) x = id x.
Proof.
  unfold map_predicate; destruct x; cbn; unfold id.
  f_equal. apply map_id.
Qed.
#[global]
Hint Rewrite @map_predicate_id : map.

Definition tCasePredProp_k
            (P : nat → term → Type)
            k (p : predicate term) :=
  All (P k) p.(pparams) × onctx_k P #|p.(pparams)| p.(pcontext) ×
  P (#|p.(pcontext)| + k) p.(preturn).

Definition tCasePredProp {term}
            (Pparams Preturn : term → Type)
            (p : predicate term) :=
  All Pparams p.(pparams) ×
  onctx Pparams p.(pcontext) ×
  Preturn p.(preturn).

Lemma map_predicate_eq_spec {A B} (finst finst' : Instance.t → Instance.t)
  (f f' g g' : A → B) h h' (p : predicate A) :
  finst (puinst p) = finst' (puinst p) →
  map f (pparams p) = map g (pparams p) →
  h =1 h' →
  f' (preturn p) = g' (preturn p) →
  map_predicate finst f f' h p = map_predicate finst' g g' h' p.
Proof.
  intros. unfold map_predicate; f_equal; auto.
Qed.
#[global] Hint Resolve map_predicate_eq_spec : all.

Lemma map_predicate_k_eq_spec {A} (finst finst' : Instance.t → Instance.t)
  (f g : nat → A → A) k k' (p : predicate A) :
  finst (puinst p) = finst' (puinst p) →
  map (f k) (pparams p) = map (g k') (pparams p) →
  shiftf f k #|pcontext p| (preturn p) = shiftf g k' #|pcontext p| (preturn p) →
  map_predicate_k finst f k p = map_predicate_k finst' g k' p.
Proof.
  intros. unfold map_predicate_k; f_equal; auto.
Qed.
#[global] Hint Resolve map_predicate_k_eq_spec : all.

Lemma map_decl_id_spec P f d :
  ondecl P d →
  (∀ x : term, P x → f x = x) →
  map_decl f d = d.
Proof.
  intros Hc Hf.
  destruct Hc.
  unfold map_decl; destruct d; cbn in ×. f_equal; eauto.
  destruct decl_body; simpl; eauto. f_equal.
  eauto.
Qed.

Lemma map_decl_id_spec_cond P p f d :
  ondecl P d →
  test_decl p d →
  (∀ x : term, P x → p x → f x = x) →
  map_decl f d = d.
Proof.
  intros [].
  unfold map_decl; destruct d; cbn in ×.
  unfold test_decl; simpl.
  intros [pty pbody]%andb_and. intros Hx.
  f_equal; eauto.
  destruct decl_body; simpl; eauto. f_equal.
  eauto.
Qed.

Lemma map_context_id_spec P f ctx :
  onctx P ctx →
  (∀ x : term, P x → f x = x) →
  map_context f ctx = ctx.
Proof.
  intros Hc Hf. induction Hc; simpl; auto.
  rewrite IHHc. f_equal; eapply map_decl_id_spec; eauto.
Qed.
#[global] Hint Resolve map_context_id_spec : all.

Lemma map_context_id_spec_cond P p f ctx :
  onctx P ctx →
  test_context p ctx →
  (∀ x : term, P x → p x → f x = x) →
  map_context f ctx = ctx.
Proof.
  intros Hc Hc' Hf. induction Hc in Hc' |- *; simpl; auto.
  revert Hc'; simpl; intros [hx hl]%andb_and.
  rewrite IHHc; auto. f_equal. eapply map_decl_id_spec_cond; eauto.
Qed.
#[global] Hint Resolve map_context_id_spec_cond : all.

Lemma map_predicate_id_spec {A} finst (f f' : A → A) h (p : predicate A) :
  finst (puinst p) = puinst p →
  map f (pparams p) = pparams p →
  h (pcontext p) = pcontext p →
  f' (preturn p) = preturn p →
  map_predicate finst f f' h p = p.
Proof.
  unfold map_predicate.
  intros → → → ->; destruct p; auto.
Qed.
#[global] Hint Resolve map_predicate_id_spec : all.

Lemma map_predicate_k_id_spec {A} finst (f : nat → A → A) k (p : predicate A) :
  finst (puinst p) = puinst p →
  map (f k) (pparams p) = pparams p →
  shiftf f k #|p.(pcontext)| (preturn p) = preturn p →
  map_predicate_k finst f k p = p.
Proof.
  unfold map_predicate_k, shiftf.
  intros → → ->; destruct p; auto.
Qed.
#[global] Hint Resolve map_predicate_k_id_spec : all.

#[global]
Instance map_predicate_proper {term} :
  Proper (`=1` ==> `=1` ==> `=1` ==> Logic.eq ==> Logic.eq)%signature (@map_predicate term term id).
Proof.
  intros eqf0 eqf1 eqf.
  intros eqf'0 eqf'1 eqf' h h' eqh'.
  intros x y →.
  apply map_predicate_eq_spec; auto.
  now apply map_ext ⇒ x.
Qed.

#[global]
Instance map_predicate_proper' {term} f : Proper (`=1` ==> `=1` ==> Logic.eq ==> Logic.eq)
  (@map_predicate term term id f).
Proof.
  intros eqf0 eqf1 eqf h h' eqh'.
  intros x y →.
  apply map_predicate_eq_spec; auto.
Qed.

Lemma shiftf0 {A B} (f : nat → A → B) : shiftf f 0 =2 f.
Proof. intros x. unfold shiftf. now rewrite Nat.add_0_r. Qed.

#[global]
Hint Rewrite @shiftf0 : map.

Lemma map_predicate_k_map_predicate_k
  (finst finst' : Instance.t → Instance.t)
  (f f' : nat → term → term)
  k k' (p : predicate term) :
  map_predicate_k finst f k (map_predicate_k finst' f' k' p) =
  map_predicate_k (finst ∘ finst') (fun i ⇒ f (i + k) ∘ f' (i + k')) 0 p.
Proof.
  unfold map_predicate, map_predicate_k. destruct p; cbn.
  f_equal.
  now rewrite map_map.
  now len.
Qed.
#[global]
Hint Rewrite map_predicate_k_map_predicate_k : map.

Lemma map_predicate_map_predicate_k
  (finst finst' : Instance.t → Instance.t)
  (f : term → term) (f' : nat → term → term)
  k (p : predicate term) :
  map_predicate finst f f id (map_predicate_k finst' f' k p) =
  map_predicate_k (finst ∘ finst') (fun k ⇒ f ∘ f' k) k p.
Proof.
  unfold map_predicate, map_predicate_k. destruct p; cbn.
  f_equal.
  apply map_map.
Qed.
#[global]
Hint Rewrite map_predicate_map_predicate_k : map.

Lemma map_predicate_k_map_predicate
  (finst finst' : Instance.t → Instance.t)
  (f' : term → term) (f : nat → term → term)
  k (p : predicate term) :
  map_predicate_k finst f k (map_predicate finst' f' f' id p) =
  map_predicate_k (finst ∘ finst') (fun k ⇒ (f k) ∘ f') k p.
Proof.
  unfold map_predicate, map_predicate_k. destruct p; cbn.
  f_equal; len; auto.
  × apply map_map.
Qed.
#[global]
Hint Rewrite map_predicate_k_map_predicate : map.

Lemma map_branch_map_branch
      {term term' term''}
      (f : term' → term'')
      (f' : term → term')
      h h'
      (b : branch term) :
  map_branch f h (map_branch f' h' b) =
  map_branch (f ∘ f') (h ∘ h') b.
Proof.
  unfold map_branch; destruct b; cbn.
  f_equal.
Qed.
#[global]
Hint Rewrite @map_branch_map_branch : map.

Lemma map_branch_k_map_branch_k (f f' : nat → term → term) h h' k k' (b : branch term) :
  #|h' b.(bcontext)| = #|b.(bcontext)| →
  map_branch_k f h k (map_branch_k f' h' k' b) =
  map_branch_k (fun i ⇒ f (i + k) ∘ f' (i + k')) (h ∘ h') 0 b.
Proof.
  unfold map_branch, map_branch_k; destruct b; cbn. len.
  intros →.
  f_equal.
Qed.

Lemma map_branch_k_map_branch_k_id (f f' : nat → term → term) k k' (b : branch term) :
  map_branch_k f id k (map_branch_k f' id k' b) =
  map_branch_k (fun i ⇒ f (i + k) ∘ f' (i + k')) id 0 b.
Proof.
  unfold map_branch, map_branch_k; destruct b; cbn. len.
  f_equal.
Qed.
#[global]
Hint Rewrite map_branch_k_map_branch_k_id : map.

Lemma map_branch_map_branch_k
      (f : term → term)
      (f' : nat → term → term) k
      (b : branch term) :
  map_branch f id (map_branch_k f' id k b) =
  map_branch_k (fun k ⇒ f ∘ (f' k)) id k b.
Proof.
  unfold map_branch, map_branch_k; destruct b; cbn.
  f_equal.
Qed.

#[global]
Hint Rewrite map_branch_map_branch_k : map.
Lemma map_branch_k_map_branch
      (f' : term → term)
      (f : nat → term → term) k
      (b : branch term) :
  map_branch_k f id k (map_branch f' id b) =
  map_branch_k (fun k ⇒ f k ∘ f') id k b.
Proof.
  unfold map_branch, map_branch_k; destruct b; cbn. len.
  f_equal.
Qed.

#[global]
Hint Rewrite map_branch_k_map_branch : map.

Lemma map_branch_id x : map_branch (@id term) id x = id x.
Proof.
  unfold map_branch, id; destruct x; cbn.
  f_equal.
Qed.
#[global]
Hint Rewrite @map_branch_id : map.

Lemma map_decl_eq_spec {A B} {P : A → Type} {d} {f g : A → B} :
  ondecl P d →
  (∀ x, P x → f x = g x) →
  map_decl f d = map_decl g d.
Proof.
  destruct d; cbn; intros [Pty Pbod] Hfg.
  unfold map_decl; cbn in *; f_equal.
  × destruct decl_body; cbn in *; eauto. f_equal.
    eauto.
  × eauto.
Qed.

Lemma map_context_eq_spec {A B} P (f g : A → B) ctx :
  onctx P ctx →
  (∀ x, P x → f x = g x) →
  map_context f ctx = map_context g ctx.
Proof.
  intros onc Hfg.
  induction onc; simpl; auto.
  rewrite IHonc. f_equal.
  eapply map_decl_eq_spec; eauto.
Qed.

Lemma map_branch_eq_spec {A B} (f g : A → B) h h' (x : branch A) :
  f (bbody x) = g (bbody x) →
  h =1 h' →
  map_branch f h x = map_branch g h' x.
Proof.
  intros. unfold map_branch; f_equal; auto.
Qed.
#[global] Hint Resolve map_branch_eq_spec : all.

Lemma map_branch_k_eq_spec {A B} (f g : nat → A → B) h h' k k' (x : branch A) :
  shiftf f k #|x.(bcontext)| (bbody x) = shiftf g k' #|x.(bcontext)| (bbody x) →
  h =1 h' →
  map_branch_k f h k x = map_branch_k g h' k' x.
Proof.
  intros. unfold map_branch_k; f_equal; auto.
Qed.
#[global] Hint Resolve map_branch_eq_spec : all.

#[global]
Instance map_branch_proper {term} : Proper (`=1` ==> `=1` ==> Logic.eq ==> Logic.eq)
  (@map_branch term term).
Proof.
  intros eqf0 eqf1 eqf h h' eqh'.
  intros x y →.
  apply map_branch_eq_spec; auto.
Qed.

Lemma id_id {A} : @id A =1 id.
Proof. now intros x. Qed.
#[global] Hint Resolve id_id : core.

Lemma map_branch_id_spec (f : term → term) (x : branch term) :
  f (bbody x) = (bbody x) →
  map_branch f id x = x.
Proof.
  intros. rewrite (map_branch_eq_spec _ id id id); auto.
  now rewrite map_branch_id.
Qed.
#[global] Hint Resolve map_branch_id_spec : all.

Lemma map_branch_k_id_spec (f : nat → term → term) h k (x : branch term) :
  h (bcontext x) = bcontext x →
  shiftf f k #|x.(bcontext)| (bbody x) = (bbody x) →
  map_branch_k f h k x = x.
Proof.
  intros. unfold map_branch_k.
  destruct x; simpl in *; f_equal; eauto.
Qed.
#[global] Hint Resolve map_branch_k_id_spec : all.

Lemma map_branches_map_branches
      {term term' term''}
      (f : term' → term'')
      (f' : term → term')
      h h'
      (l : list (branch term)) :
  map (fun b ⇒ map_branch f h (map_branch f' h' b)) l =
  map (map_branch (f ∘ f') (h ∘ h')) l.
Proof.
  eapply map_ext ⇒ b. apply map_branch_map_branch.
Qed.

Definition tCaseBrsProp {A} (P : A → Type) (l : list (branch A)) :=
  All (fun x ⇒ onctx P (bcontext x) × P (bbody x)) l.

Definition tCaseBrsProp_k (P : nat → term → Type) (p : predicate term) k (l : list (branch term)) :=
  All (fun x ⇒ onctx_k P (#|p.(pparams)|) (bcontext x) × P (#|x.(bcontext)| + k) (bbody x)) l.

Lemma map_branches_k_map_branches_k
      {term term' term''}
      (f : nat → term' → term'')
      (g : term → term')
      (f' : nat → term → term')
      h h' k
      (l : list (branch term)) :
  (∀ ctx, #|h' ctx| = #|ctx|) →
  map (fun b ⇒ map_branch (f #|bcontext (map_branch g h' b)|) h (map_branch (f' k) h' b)) l =
  map (fun b ⇒ map_branch (f #|bcontext b|) h (map_branch (f' k) h' b)) l.
Proof.
  intros Hh.
  eapply map_ext ⇒ b. rewrite map_branch_map_branch.
  rewrite map_branch_map_branch.
  simpl; autorewrite with len. now rewrite Hh.
Qed.

Lemma case_brs_map_spec {A B} {P : A → Type} {l} {f g : A → B}
  {h h' : list (BasicAst.context_decl A) → list (BasicAst.context_decl B)} :
  tCaseBrsProp P l → (∀ x, P x → f x = g x) → h =1 h' →
  map_branches f h l = map_branches g h' l.
Proof.
  intros. red in X.
  eapply All_map_eq. eapply All_impl; eauto. simpl; intros.
  destruct X0.
  apply map_branch_eq_spec; eauto.
Qed.

Lemma map_decl_eqP_spec {A B} {P : A → Type} {p : A → bool}
   {d} {f g : A → B} :
  ondecl P d →
  test_decl p d →
  (∀ x, P x → p x → f x = g x) →
  map_decl f d = map_decl g d.
Proof.
  destruct d; cbn; intros [Pty Pbod] [pty pbody]%andb_and Hfg.
  unfold map_decl; cbn in *; f_equal.
  × destruct decl_body; cbn in *; eauto. f_equal.
    eauto.
  × eauto.
Qed.

Lemma map_context_eqP_spec {A B} {P : A → Type} {p : A → bool}
   {ctx} {f g : A → B} :
  All (ondecl P) ctx →
  test_context p ctx →
  (∀ x, P x → p x → f x = g x) →
  map_context f ctx = map_context g ctx.
Proof.
  intros Ha Hctx Hfg. induction Ha; simpl; auto.
  revert Hctx; simpl; intros [Hx Hl]%andb_and.
  rewrite IHHa; f_equal; auto.
  eapply map_decl_eqP_spec; eauto.
Qed.

Lemma mapi_context_eqP_spec {A B} {P : A → Type} {ctx} {f g : nat → A → B} :
  All (ondecl P) ctx →
  (∀ k x, P x → f k x = g k x) →
  mapi_context f ctx = mapi_context g ctx.
Proof.
  intros Ha Hfg. induction Ha; simpl; auto.
  rewrite IHHa; f_equal.
  destruct p as [Hty Hbody].
  unfold map_decl; destruct x ; cbn in *; f_equal.
  × destruct decl_body; cbn in *; auto.
    f_equal. eauto.
  × eauto.
Qed.

Lemma mapi_context_eqP_id_spec {A} {P : A → Type} {ctx} {f : nat → A → A} :
  All (ondecl P) ctx →
  (∀ k x, P x → f k x = x) →
  mapi_context f ctx = ctx.
Proof.
  intros Ha Hfg. induction Ha; simpl; auto.
  rewrite IHHa; f_equal.
  destruct p as [Hty Hbody].
  unfold map_decl; destruct x ; cbn in *; f_equal.
  × destruct decl_body; cbn in *; auto.
    f_equal. eauto.
  × eauto.
Qed.

Lemma mapi_context_eqP_test_id_spec {A} {P : A → Type} (p : nat → A → bool)
  k {ctx} {f : nat → A → A} :
  All (ondecl P) ctx →
  test_context_k p k ctx →
  (∀ k (x : A), P x → p k x → f k x = x) →
  mapi_context (shiftf f k) ctx = ctx.
Proof.
  intros Ha ht Hfg. revert ht.
  induction Ha; simpl; auto.
  intros [hl [hty hbod]%andb_and]%andb_and.
  rewrite IHHa; auto; f_equal.
  destruct p0 as [Hty Hbody].
  unfold map_decl; destruct x ; cbn in *; f_equal; eauto.
  destruct decl_body; cbn in *; auto.
  f_equal. unfold shiftf. eapply Hfg; auto.
Qed.

Lemma test_context_k_eqP_id_spec {A} {P : A → Type} (p q : nat → A → bool) k k' {ctx} :
  All (ondecl P) ctx →
  test_context_k p k ctx →
  (∀ i (x : A), P x → p (i + k) x → q (i + k') x) →
  test_context_k q k' ctx.
Proof.
  intros Ha ht Hfg. revert ht.
  induction Ha; simpl; auto.
  intros [hl [hty hbod]%andb_and]%andb_and.
  rewrite IHHa; simpl; auto.
  destruct p0 as [Hty Hbody].
  unfold test_decl; destruct x ; cbn in *; eauto.
  destruct decl_body; cbn in *; auto.
  rewrite !Hfg; auto.
Qed.

Lemma test_context_k_eqP_eq_spec {A} {P : A → Type} (p q : nat → A → bool) k k' {ctx} :
  All (ondecl P) ctx →
  (∀ i (x : A), P x → p (i + k) x = q (i + k') x) →
  test_context_k p k ctx = test_context_k q k' ctx.
Proof.
  intros Ha Hfg.
  induction Ha; simpl; auto.
  rewrite IHHa; auto; f_equal.
  destruct p0 as [Hty Hbody].
  unfold test_decl; destruct x ; cbn in *; f_equal; eauto.
  destruct decl_body; cbn in *; auto;
  rewrite !Hfg; auto.
Qed.

Lemma test_context_k_eq_spec (p q : nat → term → bool) k k' {ctx} :
  (p =2 q) →
  k = k' →
  test_context_k p k ctx = test_context_k q k' ctx.
Proof.
  intros Hfg <-.
  induction ctx as [|[na [b|] ty] ctx]; simpl; auto; now rewrite IHctx Hfg.
Qed.

Lemma test_context_k_eq (p : nat → term → bool) n ctx :
  test_context_k p n ctx = alli (fun k d ⇒ test_decl (p (n + k)) d) 0 (List.rev ctx).
Proof.
  induction ctx; simpl; auto.
  rewrite IHctx alli_app /= andb_comm andb_true_r andb_comm. f_equal.
  len. now rewrite Nat.add_comm.
Qed.

#[global]
Instance test_context_k_Proper : Proper (`=2` ==> Logic.eq ==> `=1`) (@test_context_k term).
Proof.
  intros f g Hfg k k' <- ctx.
  now apply test_context_k_eq_spec.
Qed.

#[global]
Instance test_predicate_k_Proper : Proper (`=1` ==> `=2` ==> Logic.eq ==> `=1`) (@test_predicate_k term).
Proof.
  intros hi hi' eqhi f g Hfg k k' <- ctx.
  unfold test_predicate_k. rewrite eqhi.
  now setoid_rewrite Hfg.
Qed.

#[global]
Instance test_predicate_ku_Proper : Proper (`=2` ==> `=2` ==> Logic.eq ==> `=1`) (@test_predicate_ku term).
Proof.
  intros hi hi' eqhi f g Hfg k k' <- ctx.
  unfold test_predicate_ku. rewrite eqhi.
  now setoid_rewrite Hfg.
Qed.

#[global]
Instance test_branch_k_Proper p : Proper (`=2` ==> Logic.eq ==> `=1`) (@test_branch_k term p).
Proof.
  intros f g Hfg k k' <- ctx.
  unfold test_branch_k.
  now setoid_rewrite Hfg.
Qed.

Lemma case_brs_map_spec_cond {A B} {P : A → Type} pctx p {l} {f g : A → B} {h h'}:
  tCaseBrsProp P l →
  forallb (test_branch pctx p) l →
  (∀ x, P x → p x → f x = g x) →
  
  h =1 h' →
  map_branches f h l = map_branches g h' l.
Proof.
  intros. red in X.
  eapply forallb_All in H.
  eapply All_map_eq.
  eapply All_prod in X; tea. clear H.
  eapply All_impl; eauto. simpl; intros br [[]%andb_and []].
  apply map_branch_eq_spec; eauto.
Qed.

Lemma case_brs_map_k_spec {A B} {P : A → Type} {k l} {f g : nat → A → B} {h h'} :
  tCaseBrsProp P l →
  (∀ k x, P x → f k x = g k x) →
  h =1 h' →
  map_branches_k f h k l = map_branches_k g h' k l.
Proof.
  intros. red in X.
  eapply All_map_eq. eapply All_impl; eauto. simpl; intros.
  apply map_branch_k_eq_spec; eauto.
  unfold shiftf. now apply H.
Qed.

Lemma case_brs_forallb_map_spec {A B} {P : A → Type} {pctx p : A → bool}
      {l} {f g : A → B} {h h'} :
  tCaseBrsProp P l →
  forallb (test_branch pctx p) l →
  (∀ x, P x → p x → f x = g x) →
  h =1 h' →
  map (map_branch f h) l = map (map_branch g h') l.
Proof.
  intros.
  eapply All_map_eq. red in X. apply forallb_All in H.
  eapply All_impl. eapply All_prod. exact X. exact H. simpl.
  intros [bctx bbod] [Hbr hb]. cbn in ×.
  unfold map_branch; cbn. f_equal.
  - apply H1.
  - eapply H0; eauto. apply Hbr.
    now move/andb_and: hb ⇒ [].
Qed.

Lemma test_context_map (p : term → bool) f (ctx : context) :
  test_context p (map_context f ctx) = test_context (p ∘ f) ctx.
Proof.
  induction ctx; simpl; auto.
  rewrite IHctx. f_equal.
  now rewrite test_decl_map_decl.
Qed.
#[global]
Hint Rewrite test_context_map : map.

Lemma onctx_test P (p q : term → bool) ctx :
  onctx P ctx →
  test_context p ctx →
  (∀ t, P t → p t → q t) →
  test_context q ctx.
Proof.
  intros Hc tc HP. revert tc.
  induction Hc; simpl; auto.
  destruct p0.
  intros [pl [pbod pty]%andb_and]%andb_and.
  rewrite (IHHc pl); simpl.
  unfold test_decl.
  rewrite (HP _ p0 pty) andb_true_r; simpl.
  destruct (decl_body x); simpl in *; eauto.
Qed.