(* Distributed under the terms of the MIT license. *)
From MetaRocq.Utils Require Import utils.
From MetaRocq.Common Require Import Environment.
From MetaRocq.Template Require Import Ast AstUtils.

Lemma term_forall_list_ind :
  ∀ P : term → Prop,
    (∀ n : nat, P (tRel n)) →
    (∀ i : ident, P (tVar i)) →
    (∀ (n : nat) (l : list term), Forall P l → P (tEvar n l)) →
    (∀ s, P (tSort s)) →
    (∀ t : term, P t → ∀ (c : cast_kind) (t0 : term), P t0 → P (tCast t c t0)) →
    (∀ (n : aname) (t : term), P t → ∀ t0 : term, P t0 → P (tProd n t t0)) →
    (∀ (n : aname) (t : term), P t → ∀ t0 : term, P t0 → P (tLambda n t t0)) →
    (∀ (n : aname) (t : term),
        P t → ∀ t0 : term, P t0 → ∀ t1 : term, P t1 → P (tLetIn n t t0 t1)) →
    (∀ t : term, P t → ∀ l : list term, Forall P l → P (tApp t l)) →
    (∀ s (u : list Level.t), P (tConst s u)) →
    (∀ (i : inductive) (u : list Level.t), P (tInd i u)) →
    (∀ (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u)) →
    (∀ (ci : case_info) (t : predicate term),
        tCasePredProp P P t → ∀ t0 : term, P t0 → ∀ l : list (branch term),
        tCaseBrsProp P l → P (tCase ci t t0 l)) →
    (∀ (s : projection) (t : term), P t → P (tProj s t)) →
    (∀ (m : mfixpoint term) (n : nat), tFixProp P P m → P (tFix m n)) →
    (∀ (m : mfixpoint term) (n : nat), tFixProp P P m → P (tCoFix m n)) →
    (∀ i, P (tInt i)) →
    (∀ f, P (tFloat f)) →
    (∀ s, P (tString s)) →
    (∀ u arr def ty, Forall P arr → P def → P ty → P (tArray u arr def ty)) →
    ∀ t : term, P t.
Proof.
  intros until t. revert t.
  fix auxt 1.
  move auxt at top.
  destruct t;
    match goal with
      H : _ |- _ ⇒ apply H; auto
    end;
    try solve [match goal with
      |- _ P ?arg ⇒
      revert arg; fix aux_arg 1; intro arg;
        destruct arg; constructor; [|apply aux_arg];
          try split; apply auxt
    end].
  destruct type_info; split; cbn; [|now auto].
  revert pparams; fix aux_pparams 1.
  intros []; constructor; [apply auxt|apply aux_pparams].
Defined.

Lemma term_forall_list_rect :
  ∀ P : term → Type,
    (∀ n : nat, P (tRel n)) →
    (∀ i : ident, P (tVar i)) →
    (∀ (n : nat) (l : list term), All P l → P (tEvar n l)) →
    (∀ s, P (tSort s)) →
    (∀ t : term, P t → ∀ (c : cast_kind) (t0 : term), P t0 → P (tCast t c t0)) →
    (∀ (n : aname) (t : term), P t → ∀ t0 : term, P t0 → P (tProd n t t0)) →
    (∀ (n : aname) (t : term), P t → ∀ t0 : term, P t0 → P (tLambda n t t0)) →
    (∀ (n : aname) (t : term),
        P t → ∀ t0 : term, P t0 → ∀ t1 : term, P t1 → P (tLetIn n t t0 t1)) →
    (∀ t : term, P t → ∀ l : list term, All P l → P (tApp t l)) →
    (∀ s (u : list Level.t), P (tConst s u)) →
    (∀ (i : inductive) (u : list Level.t), P (tInd i u)) →
    (∀ (i : inductive) (n : nat) (u : list Level.t), P (tConstruct i n u)) →
    (∀ (ci : case_info) (p0 : predicate term),
        tCasePredProp P P p0 → ∀ t : term, P t → ∀ l : list (branch term),
        tCaseBrsType P l → P (tCase ci p0 t l)) →
    (∀ (s : projection) (t : term), P t → P (tProj s t)) →
    (∀ (m : mfixpoint term) (n : nat), tFixType P P m → P (tFix m n)) →
    (∀ (m : mfixpoint term) (n : nat), tFixType P P m → P (tCoFix m n)) →
    (∀ i, P (tInt i)) →
    (∀ f, P (tFloat f)) →
    (∀ s, P (tString s)) →
    (∀ u arr def ty, All P arr → P def → P ty → P (tArray u arr def ty)) →
    ∀ t : term, P t.
Proof.
  intros until t. revert t.
  fix auxt 1.
  move auxt at top.
  destruct t;
    match goal with
      H : _ |- _ ⇒ apply H; auto
    end;
    try solve [match goal with
      |- _ P ?arg ⇒
      revert arg; fix aux_arg 1; intro arg;
        destruct arg; constructor; [|apply aux_arg];
          try split; apply auxt
    end].
  destruct type_info; split; cbn; [|now auto].
  revert pparams; fix aux_pparams 1.
  intros []; constructor; [apply auxt|apply aux_pparams].
Defined.