累積帰納法の一般化

coq

TopProver で行われたCoqコンテストに参加して、モチベが上がったため、coqのライブラリを整備することに。
とりあえず便利なので累積帰納法を整備した。
自然数に関する累積帰納法だけだと不便なことがあるので、より一般化し、任意の型 X の f による nat への写像に関する累積帰納法を扱えるようにした。

これによって

  • l : list X の 長さ に関する帰納法
  • l : list nat の 合計 に関する帰納法
  • l : list nat の 長さ + 合計 に関する帰納法 (これ便利)
  • (n, m) : nat * nat の n + m に関する帰納法

などが簡単にでき、超便利。

(*
  Lib for induction

 累積帰納法(cov_induction)
  usage:
    apply (cov_induction (fun n => ...)).

 一般化累積帰納法(mapped_cov_induction)
  example:
    apply (cov_induction (fun l => length l) (fun l => ...)).
*)

Require Import Le Omega.

Theorem cov_induction: forall P: nat -> Prop, (forall n: nat, ((forall (m: nat), m < n -> P m) -> P n)) -> (forall n: nat, P n).
Proof.
  assert(Lem: forall P: nat -> Prop, (forall n: nat, ((forall (m: nat), m < n -> P m) -> P n)) -> (forall n m: nat, n < m -> P n)). {
    intros P IH n m. generalize dependent n.
    induction m.
    - intros n H. inversion H.
    - intros n H. inversion H.
    -- apply IH. apply IHm.
    -- apply IHm. apply H1.
  }
  - intros P H1 n.
    apply Lem with (m := S n).
  -- apply H1.
  -- apply le_n_S. apply le_refl.
Qed.

Theorem mapped_cov_induction:
  forall {X} (f: X -> nat) (P: X -> Prop), (forall x: X, (forall y: X, f y < f x -> P y) -> P x) -> forall z, P z.
Proof.
  intros X f P.
  generalize (cov_induction (fun n => forall (x: X), n = f x -> P x)); intro Ind.
  intros Asm1 z. apply Ind with (n := f z).
  - intros n IH x H.
    apply Asm1.
    intros y H4.
    apply IH with (m := f y); omega.
  - reflexivity.
Qed.

(* endlib: induction *)