Library MetaCoq.PCUIC.PCUICInduction
Deriving a compact induction principle for terms
Lemma term_forall_list_ind :
∀ 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)) →
(∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tProd n t t0)) →
(∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tLambda n t t0)) →
(∀ (n : name) (t : term),
P t → ∀ t0 : term, P t0 → ∀ t1 : term, P t1 → P (tLetIn n t t0 t1)) →
(∀ t u : term, P t → P u → P (tApp t u)) →
(∀ (s : String.string) (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)) →
(∀ (p : inductive × nat) (t : term),
P t → ∀ t0 : term, P t0 → ∀ l : list (nat × term),
tCaseBrsProp P l → P (tCase p 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.
Inductive ForallT {A} (P : A → Type) : list A → Type :=
| ForallT_nil : ForallT P []
| ForallT_cons : ∀ (x : A) (l : list A), P x → ForallT P l → ForallT P (x :: l).
Definition tCaseBrsType {A} (P : A → Type) (l : list (nat × A)) :=
ForallT (fun x ⇒ P (snd x)) l.
Definition tFixType {A : Set} (P P' : A → Type) (m : mfixpoint A) :=
ForallT (fun x : def A ⇒ P x.(dtype) × P' x.(dbody))%type m.
Lemma term_forall_list_rec :
∀ P : term → Type,
(∀ n : nat, P (tRel n)) →
(∀ i : ident, P (tVar i)) →
(∀ (n : nat) (l : list term), ForallT P l → P (tEvar n l)) →
(∀ s, P (tSort s)) →
(∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tProd n t t0)) →
(∀ (n : name) (t : term), P t → ∀ t0 : term, P t0 → P (tLambda n t t0)) →
(∀ (n : name) (t : term),
P t → ∀ t0 : term, P t0 → ∀ t1 : term, P t1 → P (tLetIn n t t0 t1)) →
(∀ t u : term, P t → P u → P (tApp t u)) →
(∀ (s : String.string) (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)) →
(∀ (p : inductive × nat) (t : term),
P t → ∀ t0 : term, P t0 → ∀ l : list (nat × term),
tCaseBrsType P l → P (tCase p t t0 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.