induction principle を自分で書く
昨日 (http://lkozima.hatenablog.com/entry/2013/07/19/225156) よくわからないとか言っていたのが冷静に考えたらできた。
なんかこういうのを考えていて,
Inductive mov : nat -> nat -> Prop := | mov_1 : forall m, mov (S m) m | mov_2 : forall m, mov (S (S m)) m | mov_3 : forall m, mov (S (S (S m))) m. Inductive losing : nat -> Prop := | Losing : forall n, (forall m, mov n m -> exists k, mov m k /\ losing k) -> losing n.
losing に対する induction principle はどういう形になるべきだろうかという話でした。
結論から書くと
Fixpoint losing_induction P (IH : forall n, (forall m, mov n m -> exists k, mov m k /\ losing k /\ P k) -> P n) n (H : losing n) : P n := match H with | Losing n f => IH n (fun m Hm => match f m Hm with | ex_intro k (conj p1 p2) => ex_intro _ k (conj p1 (conj p2 (losing_induction P IH k p2))) end) end.
でよいと思います。読みにくいですが。Check してみるとこうなってます。
losing_induction : forall P : nat -> Prop, (forall n : nat, (forall m : nat, mov n m -> exists k : nat, mov m k /\ losing k /\ P k) -> P n) -> forall n : nat, losing n -> P n
これを使って losing なら 4 の倍数であることも証明できました。証明の中身は lt_wf_ind を使う場合とほとんど同じになりましたが。
でもそれよりも,どうやってこの形を出したかのほうがおもしろいと思うのでその話をします。