Library MetaCoq.PCUIC.PCUICAstUtils

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_name na ++ "," ++
                            string_of_term b ++ "," ++ string_of_term t ++ ")"
  | tLambda na b t ⇒ "Lambda(" ++ string_of_name na ++ "," ++ string_of_term b
                                ++ "," ++ string_of_term t ++ ")"
  | tLetIn na b t' t ⇒ "LetIn(" ++ string_of_name 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(" ++ 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 (ind, i) t p brs ⇒
    "Case(" ++ string_of_inductive ind ++ "," ++ string_of_nat i ++ "," ++ string_of_term t ++ ","
            ++ string_of_term p ++ "," ++ string_of_list (fun b ⇒ string_of_term (snd b)) brs ++ ")"
  | tProj (ind, i, k) c ⇒
    "Proj(" ++ string_of_inductive ind ++ "," ++ string_of_nat i ++ "," ++ string_of_nat k ++ ","
            ++ 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.

Definition mkLambda_or_LetIn d t :=
  match d.(decl_body) with
  | None ⇒ tLambda d.(decl_name) d.(decl_type) t
  | Some b ⇒ tLetIn d.(decl_name) b d.(decl_type) t
  end.

Definition it_mkLambda_or_LetIn (l : context) (t : term) :=
  List.fold_left (fun acc d ⇒ mkLambda_or_LetIn d acc) l t.

Definition mkProd_or_LetIn d t :=
  match d.(decl_body) with
  | None ⇒ tProd d.(decl_name) d.(decl_type) t
  | Some b ⇒ tLetIn d.(decl_name) b d.(decl_type) t
  end.

Definition it_mkProd_or_LetIn (l : context) (t : term) :=
  List.fold_left (fun acc d ⇒ mkProd_or_LetIn d acc) l t.

Definition map_decl f (d : context_decl) :=
  {| decl_name := d.(decl_name);
     decl_body := option_map f d.(decl_body);
     decl_type := f d.(decl_type) |}.

Lemma map_decl_type f decl : f (decl_type decl) = decl_type (map_decl f decl).

Lemma map_decl_body f decl : option_map f (decl_body decl) = decl_body (map_decl f decl).

Lemma option_map_decl_body_map_decl f x :
  option_map decl_body (option_map (map_decl f) x) =
  option_map (option_map f) (option_map decl_body x).

Lemma option_map_decl_type_map_decl f x :
  option_map decl_type (option_map (map_decl f) x) =
  option_map f (option_map decl_type x).

Definition map_context f c :=
  List.map (map_decl f) c.

Definition map_constant_body f decl :=
  {| cst_type := f decl.(cst_type);
     cst_body := option_map f decl.(cst_body);
     cst_universes := decl.(cst_universes) |}.

Lemma map_cst_type f decl : f (cst_type decl) = cst_type (map_constant_body f decl).

Lemma map_cst_body f decl : option_map f (cst_body decl) = cst_body (map_constant_body f decl).

Definition map_def {A B : Set} (tyf bodyf : A → B) (d : def A) :=
  {| dname := d.(dname); dtype := tyf d.(dtype); dbody := bodyf d.(dbody); rarg := d.(rarg) |}.

Lemma map_dtype {A B : Set} (f : A → B) (g : A → B) (d : def A) :
  f (dtype d) = dtype (map_def f g d).

Lemma map_dbody {A B : Set} (f : A → B) (g : A → B) (d : def A) :
  g (dbody d) = dbody (map_def f g d).

Definition app_context (Γ Γ' : context) : context := (Γ' ++ Γ)%list.
Notation " Γ ,,, Γ' " := (app_context Γ Γ') (at level 25, Γ' at next level, left associativity) : pcuic.

Lemma app_context_assoc Γ Γ' Γ'' : Γ ,,, (Γ' ,,, Γ'') = Γ ,,, Γ' ,,, Γ''.

Lemma app_context_cons Γ Γ' A : Γ ,,, (Γ' ,, A) = (Γ ,,, Γ') ,, A.

Lemma app_context_length Γ Γ' : #|Γ ,,, Γ'| = #|Γ'| + #|Γ|.

Lemma nth_error_app_context_ge v Γ Γ' : #|Γ'| ≤ v → nth_error (Γ ,,, Γ') v = nth_error Γ (v - #|Γ'|).

Lemma nth_error_app_context_lt v Γ Γ' : v < #|Γ'| → nth_error (Γ ,,, Γ') v = nth_error Γ' v.

Lemma app_context_nil_l Γ : [] ,,, Γ = Γ.

Lemma map_app_context f Γ Γ' : map f (Γ ,,, Γ') = map f Γ ,,, map f Γ'.

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

Definition decompose_app t := 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').


Lemma decompose_app_mkApps f l :
  ~~ isApp f → decompose_app (mkApps f l) = (f, l).

Lemma mkApps_nested f l l' : mkApps (mkApps f l) l' = mkApps f (l ++ l').

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

Definition get_ident (n : name) : string :=
  match n with
  | nAnon ⇒ "XX"
  | nNamed i ⇒ i
  end.

Fixpoint remove_arity (n : nat) (t : term) : term :=
  match n with
  | O ⇒ t
  | S n ⇒ match t with
          | tProd _ _ B ⇒ remove_arity n B
          | _ ⇒ t
          end
  end.

Definition isConstruct_app t :=
  match fst (decompose_app t) with
  | tConstruct _ _ _ ⇒ true
  | _ ⇒ false
  end.

Fixpoint lookup_mind_decl (id : ident) (decls : global_env)
 := match decls with
    | nil ⇒ None
    | InductiveDecl kn d :: tl ⇒
      if string_compare kn id is Eq then Some d else lookup_mind_decl id tl
    | _ :: tl ⇒ lookup_mind_decl id tl
    end.

Definition mind_body_to_entry (decl : mutual_inductive_body)
  : mutual_inductive_entry.

Definition arities_context (l : list one_inductive_body) :=
  rev_map (fun ind ⇒ vass (nNamed ind.(ind_name)) ind.(ind_type)) l.

Lemma arities_context_length l : #|arities_context l| = #|l|.

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

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 B ⇒ decompose_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_mkProd_or_LetIn_app l l' t :
  it_mkProd_or_LetIn (l ++ l') t = it_mkProd_or_LetIn l' (it_mkProd_or_LetIn l t).

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).

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).

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).

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).

Fixpoint reln (l : list term) (p : nat) (Γ0 : list context_decl) {struct Γ0} : list term :=
  match Γ0 with
  | [] ⇒ l
  | {| decl_body := Some _ |} :: hyps ⇒ reln l (p + 1) hyps
  | {| decl_body := None |} :: hyps ⇒ reln (tRel p :: l) (p + 1) hyps
  end.

Definition to_extended_list_k Γ k := reln [] k Γ.
Definition to_extended_list Γ := to_extended_list_k Γ 0.

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 Γ).

Lemma to_extended_list_k_spec Γ k :
  Forall (fun x ⇒ ∃ n, x = tRel n ∧ k ≤ n ∧ n < k + length Γ) (to_extended_list_k Γ k).

Lemma to_extended_list_lift_above Γ :
  Forall (fun x ⇒ ∃ n, x = tRel n ∧ n < length Γ) (to_extended_list Γ).

Fixpoint reln_alt p Γ :=
  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.

Lemma to_extended_list_k_cons d Γ k :
  to_extended_list_k (d :: Γ) k =
  match d.(decl_body) with
  | None ⇒ to_extended_list_k Γ (S k) ++ [tRel k]
  | Some b ⇒ to_extended_list_k Γ (S k)
  end.

Fixpoint context_assumptions (Γ : context) :=
  match Γ with
  | [] ⇒ 0
  | d :: Γ ⇒
    match d.(decl_body) with
    | Some _ ⇒ context_assumptions Γ
    | None ⇒ S (context_assumptions Γ)
    end
  end.

Definition map_one_inductive_body npars arities f (n : nat) m :=
  match m with
  | Build_one_inductive_body ind_name ind_type ind_kelim ind_ctors ind_projs ⇒
    Build_one_inductive_body ind_name
                             (f 0 ind_type)
                             ind_kelim
                             (map (on_pi2 (f arities)) ind_ctors)
                             (map (on_snd (f (S npars))) ind_projs)
  end.

Definition fold_context f (Γ : context) : context :=
  List.rev (mapi (fun k' decl ⇒ map_decl (f k') decl) (List.rev Γ)).

Lemma fold_context_alt f Γ :
  fold_context f Γ =
  mapi (fun k' d ⇒ map_decl (f (Nat.pred (length Γ) - k')) d) Γ.

Lemma fold_context_length f Γ : length (fold_context f Γ) = length Γ.

Lemma fold_context_snoc0 f Γ d : fold_context f (d :: Γ) = fold_context f Γ ,, map_decl (f (length Γ)) d.

Lemma fold_context_app f Γ Δ :
  fold_context f (Δ ++ Γ) = fold_context (fun k ⇒ f (length Γ + k)) Δ ++ fold_context f Γ.

Lemma context_assumptions_fold Γ f : context_assumptions (fold_context f Γ) = context_assumptions Γ.

Lemma nth_error_fold_context (f : nat → term → term):
  ∀ (Γ' Γ'' : context) (v : nat),
    v < length Γ' → ∀ nth,
    nth_error Γ' v = Some nth →
    nth_error (fold_context f Γ') v = Some (map_decl (f (length Γ' - S v)) nth).

Lemma nth_error_fold_context_eq:
  ∀ (Γ' : context) (v : nat) f,
    nth_error (fold_context f Γ') v =
    option_map (map_decl (f (length Γ' - S v))) (nth_error Γ' v).

Lemma nth_error_ge {Γ Γ' v Γ''} f : length Γ' ≤ v →
  nth_error (Γ' ++ Γ) v =
  nth_error (fold_context (f 0) Γ' ++ Γ'' ++ Γ) (length Γ'' + v).

Lemma nth_error_lt {Γ Γ' Γ'' v} (f : nat → term → term) : v < length Γ' →
  nth_error (fold_context f Γ' ++ Γ'' ++ Γ) v =
  option_map (map_decl (f (length Γ' - S v))) (nth_error (Γ' ++ Γ) v).

Definition map_mutual_inductive_body f m :=
  match m with
  | Build_mutual_inductive_body finite ind_npars ind_pars ind_bodies ind_universes ⇒
    let arities := arities_context ind_bodies in
    let pars := fold_context f ind_pars in
    Build_mutual_inductive_body finite ind_npars pars
      (mapi (map_one_inductive_body (context_assumptions pars) (length arities) f) ind_bodies)
      ind_universes
  end.

Lemma ind_type_map f npars_ass arities n oib :
  ind_type (map_one_inductive_body npars_ass arities f n oib) = f 0 (ind_type oib).

Lemma ind_ctors_map f npars_ass arities n oib :
  ind_ctors (map_one_inductive_body npars_ass arities f n oib) =
  map (on_pi2 (f arities)) (ind_ctors oib).

Lemma ind_pars_map f m :
  ind_params (map_mutual_inductive_body f m) =
  fold_context f (ind_params m).

Lemma ind_projs_map f npars_ass arities n oib :
  ind_projs (map_one_inductive_body npars_ass arities f n oib) =
  map (on_snd (f (S npars_ass))) (ind_projs oib).

Definition test_def {A : Set} (tyf bodyf : A → bool) (d : def A) :=
  tyf d.(dtype) && bodyf d.(dbody).

Definition tCaseBrsProp {A} (P : A → Type) (l : list (nat × A)) :=
  All (fun x ⇒ P (snd x)) l.

Definition tFixProp {A : Set} (P P' : A → Type) (m : mfixpoint A) :=
  All (fun x : def A ⇒ P x.(dtype) × P' x.(dbody))%type m.


Lemma map_def_map_def {A B C : Set} (f f' : B → C) (g g' : A → B) (d : def A) :
  map_def f f' (map_def g g' d) = map_def (fun x ⇒ f (g x)) (fun x ⇒ f' (g' x)) d.

Lemma compose_map_def {A B C : Set} (f f' : B → C) (g g' : A → B) :
  compose (A:=def A) (map_def f f') (map_def g g') = map_def (compose f g) (compose f' g').

Lemma map_def_id {t : Set} x : map_def (@id t) (@id t) x = x.

Lemma map_def_spec {A B : Set} (P P' : A → Type) (f f' g g' : A → B) (x : def A) :
  P' x.(dbody) → P x.(dtype) → (∀ x, P x → f x = g x) →
  (∀ x, P' x → f' x = g' x) →
  map_def f f' x = map_def g g' x.

Lemma case_brs_map_spec {A B : Set} {P : A → Type} {l} {f g : A → B} :
  tCaseBrsProp P l → (∀ x, P x → f x = g x) →
  map (on_snd f) l = map (on_snd g) l.

Lemma tfix_map_spec {A B : Set} {P P' : A → Type} {l} {f f' g g' : A → B} :
  tFixProp P P' l → (∀ x, P x → f x = g x) →
  (∀ x, P' x → f' x = g' x) →
  map (map_def f f') l = map (map_def g g') l.

Lemma map_def_test_spec {A B : Set}
      (P P' : A → Type) (p p' : pred A) (f f' g g' : A → B) (x : def A) :
  P x.(dtype) → P' x.(dbody) → (∀ x, P x → p x → f x = g x) →
  (∀ x, P' x → p' x → f' x = g' x) →
  test_def p p' x →
  map_def f f' x = map_def g g' x.

Lemma case_brs_forallb_map_spec {A B : Set} {P : A → Type} {p : A → bool}
      {l} {f g : A → B} :
  tCaseBrsProp P l →
  forallb (test_snd p) l →
  (∀ x, P x → p x → f x = g x) →
  map (on_snd f) l = map (on_snd g) l.

Lemma tfix_forallb_map_spec {A B : Set} {P P' : A → Prop} {p p'} {l} {f f' g g' : A → B} :
  tFixProp P P' l →
  forallb (test_def p p') l →
  (∀ x, P x → p x → f x = g x) →
  (∀ x, P' x → p' x → f' x = g' x) →
  map (map_def f f') l = map (map_def g g') l.



Lemma mkApps_inj :
  ∀ u v l,
    mkApps u l = mkApps v l →
    u = v.

Lemma isApp_mkApps :
  ∀ u l,
    isApp u →
    isApp (mkApps u l).

Lemma decompose_app_rec_notApp :
  ∀ t l u l',
    decompose_app_rec t l = (u, l') →
    isApp u = false.

Lemma decompose_app_notApp :
  ∀ t u l,
    decompose_app t = (u, l) →
    isApp u = false.

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

Lemma isApp_false_nApp :
  ∀ u,
    isApp u = false →
    nApp u = 0.

Lemma nApp_mkApps :
  ∀ t l,
    nApp (mkApps t l) = nApp t + #|l|.

Lemma decompose_app_eq_mkApps :
  ∀ t u l l',
    decompose_app t = (mkApps u l', l) →
    l' = [].

Lemma mkApps_nApp_inj :
  ∀ u u' l l',
    nApp u = nApp u' →
    mkApps u l = mkApps u' l' →
    u = u' ∧ l = l'.

Lemma mkApps_notApp_inj :
  ∀ u u' l l',
    isApp u = false →
    isApp u' = false →
    mkApps u l = mkApps u' l' →
    u = u' ∧ l = l'.

Lemma decompose_app_rec_inv {t l' f l} :
  decompose_app_rec t l' = (f, l) →
  mkApps t l' = mkApps f l.

Lemma decompose_app_inv {t f l} :
  decompose_app t = (f, l) → t = mkApps f l.

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.

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.

Lemma decompose_app_tFix mfix idx args t :
  decompose_app t = (tFix mfix idx, args) → t = mkApps (tFix mfix idx) args.

Lemma mkApps_size x l : size (mkApps x l) = size x + list_size size l.
Lemma mkApps_eq_head {x l} : mkApps x l = x → l = [].

Lemma mkApps_eq_inv {x y l} : x = mkApps y l → size y ≤ size x.

Lemma mkApps_eq_left x y l : mkApps x l = mkApps y l → x = y.

Lemma decompose_app_eq_right t l l' : decompose_app_rec t l = decompose_app_rec t l' → l = l'.

Lemma mkApps_eq_right t l l' : mkApps t l = mkApps t l' → l = l'.


Lemma atom_decompose_app t l : ~~ isApp t → decompose_app_rec t l = pair t l.

Lemma mkApps_eq_inj {t t' l l'} :
  mkApps t l = mkApps t' l' →
  ~~ isApp t → ~~ isApp t' → t = t' ∧ l = l'.


Lemma mkApps_eq_decompose {f args t} :
  mkApps f args = t →
  ~~ isApp f →
  fst (decompose_app t) = f.



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).

Lemma firstn_add {A} x y (args : list A) : firstn (x + y) args = firstn x args ++ firstn y (skipn x args).

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).

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')).

Lemma mkApps_elim t l :
  let app' := decompose_app (mkApps t l) in
  mkApps_spec app'.1 app'.2 t l (mkApps t l).

Lemma nisApp_mkApps {t l} : ~~ isApp (mkApps t l) → ~~ isApp t ∧ l = [].

Lemma mkApps_nisApp {t t' l} : mkApps t l = t' → ~~ isApp t' → t = t' ∧ l = [].

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 = [].

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 ContextSet.empty).