Library MetaCoq.PCUIC.PCUICSize

Section ListSize.
  Context {A} (size : A → nat).

  Equations list_size (l : list A) : nat :=
  list_size nil := 0;
  list_size (cons a v) := S (size a + list_size v).

  Lemma list_size_app (l l' : list A) : list_size (l ++ l') = list_size l + list_size l'.

  Lemma list_size_rev (l : list A) : list_size (List.rev l) = list_size l.

End ListSize.

Section ListSizeMap.
  Context {A} (sizeA : A → nat).
  Context {B} (sizeB : B → nat).

  Lemma list_size_mapi_rec_eq (l : list A) (f : nat → A → B) k :
    (∀ i x, sizeB (f i x) = sizeA x) →
    list_size sizeB (mapi_rec f l k) = list_size sizeA l.

  Lemma list_size_mapi_eq (l : list A) (f : nat → A → B) :
    (∀ i x, sizeB (f i x) = sizeA x) →
    list_size sizeB (mapi f l) = list_size sizeA l.

  Lemma list_size_map_eq (l : list A) (f : A → B) :
    (∀ x, sizeA x = sizeB (f x)) →
    list_size sizeB (map f l) = list_size sizeA l.

  Lemma list_size_mapi_rec_le (l : list A) (f : nat → A → B) k :
    (∀ i x, sizeB (f i x) ≤ sizeA x) →
    list_size sizeB (mapi_rec f l k) ≤ list_size sizeA l.

  Lemma list_size_mapi_le (l : list A) (f : nat → A → B) :
    (∀ i x, sizeB (f i x) ≤ sizeA x) →
    list_size sizeB (mapi f l) ≤ list_size sizeA l.

  Lemma list_size_map_le (l : list A) (f : A → B) :
    (∀ x, sizeB (f x) ≤ sizeA x) →
    list_size sizeB (map f l) ≤ list_size sizeA l.

End ListSizeMap.

Lemma list_size_map_hom {A} (size : A → nat) (l : list A) (f : A → A) :
  (∀ x, size x = size (f x)) →
  list_size size (map f l) = list_size size l.

Definition def_size (size : term → nat) (x : def term) := size (dtype x) + size (dbody x).
Definition mfixpoint_size (size : term → nat) (l : mfixpoint term) :=
  list_size (def_size size) l.

Definition decl_size (size : term → nat) (x : context_decl) :=
  size (decl_type x) + option_default size (decl_body x) 0.

Definition context_size (size : term → nat) (l : context) :=
  list_size (decl_size size) l.

Fixpoint size t : nat :=
  match t with
  | tRel i ⇒ 1
  | tEvar ev args ⇒ S (list_size size args)
  | tLambda na T M ⇒ S (size T + size M)
  | tApp u v ⇒ S (size u + size v)
  | tProd na A B ⇒ S (size A + size B)
  | tLetIn na b t b' ⇒ S (size b + size t + size b')
  | tCase ind p c brs ⇒ S (size p + size c + list_size (fun x ⇒ size (snd x)) brs)
  | tProj p c ⇒ S (size c)
  | tFix mfix idx ⇒ S (mfixpoint_size size mfix)
  | tCoFix mfix idx ⇒ S (mfixpoint_size size mfix)
  | x ⇒ 1
  end.