[Coq] How to define complex inductions

Coq の証明の書き方パターンを yoshihiro503 さんに教わったので、忘れないうちに。

自然数に関する定理を証明したい場合に、下記の様な補題が欲しかったとします。

Lemma nat2_ind : forall P:nat -> Prop, P 0 -> P 1 ->
  (forall n:nat, P n -> P (S n) -> P (S (S n))) ->
  (forall n:nat, P n).

教わったコードを元に自分なりに書いてみたのが下記の証明です。

  
  ============================
   forall P : nat -> Prop,
   P 0 ->
   P 1 ->
   (forall n : nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P n

nat2_ind < intros P H0 H1 IH.          
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ============================
   forall n : nat, P n

nat2_ind < refine (fix ll n : P n := _).     (* ここで refine を使って ll を定義するのがポイント *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  ============================
   P n

(* しかしここで apply ll しても駄目。llはIHの仮定のところで使う *)

nat2_ind < induction n.
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  ============================
   P 0

subgoal 2 is:
 P (S n)

nat2_ind < exact H0.  (* n=0 のケースは P 0 *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P n
  ============================
   P (S n)

nat2_ind < induction n.
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  IHn : P 0
  ============================
   P 1

subgoal 2 is:
 P (S (S n))

nat2_ind < exact H1.  (* n=1 のケース *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P (S (S n))

nat2_ind < apply IH.   (* IH を使う *)
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P n

subgoal 2 is:
 P (S n)

nat2_ind < apply ll.  (* IHの仮定のところにはll を使ってOK *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P (S n)

nat2_ind < apply IHn0.          
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P n

nat2_ind < apply ll.  (* もう一度 ll を使う *)
Proof completed.

nat2_ind < Qed.

そもそもの証明のゴールをrefineを使ってllとして定義して、証明の中でllを使っているので非常に不思議なのですが、変な所（例えばrefine直後に）でapply llしてProof CompleteしてもQedしたとたんにエラーになります。エラーが出ない様にH0,H1,IHを使えば、証明が正しい事になります。

なお、同じ定理を短く書くとkikxさんの証明ゴルフみたいになるようです。すごい。