Library MetaCoq.Template.Induction

From MetaCoq Require Import utils Ast AstUtils Environment.

Deriving a compact induction principle for terms

Allows to get the right induction principle on lists of terms appearing in the term syntax (in evar, applications, branches of cases and (co-)fixpoints.
Custom induction principle on syntax, dealing with the various lists appearing in terms.

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