Software Foundations

仕事がつまらんので逃避中。

https://www.cis.upenn.edu/~bcpierce/sf/current/
読み始めて三年の月日が経とうというのに、まだ半分もいかない。
ちょっと読んでは分からんので中断し、忘れているので最初からやりなおしとかやってりゃ進まないのは当たり前。

というわけで三回目の挑戦中。
前半は大分書き変わってて、初版と比べて、だいぶ分かりやすくなった。と思う。(beautiful n とか、やはりいらない子だった。)
自分にとって、三回目だというのもあるかもしれないが。

前回、前々回と挫折したImp.vを今回初めて読了。数学力も数学学習歴ともに皆無のおっさんにはつらくて楽しい本だわいな。

Imp.vの中の問題やってる間、

forall X (l a:list X),  l = a ++ l -> a = [].

こんなの命題の証明があれば便利かな？とか思い証明しようとして、

Lemma app_any_is_nil : forall X (l a:list X),
  l = a ++ l -> a = [].
Proof.
(* lの帰納法で
  intros. induction l. apply app_nil_r in H. rewrite H. reflexivity.
  あれ？
*)
(* aの帰納法で。*)
  intros X l a. generalize dependent l.
induction a as [|xa a']. intros. reflexivity. intros. destruct l. inversion H. inversion H. Abort.

え？何で出来ひんの？。
まあ別に本編では結局いらなかったので放置してたけど、

さっき

Goal forall n a:nat,
       n = a + n -> a = 0.
Proof.
  intros. induction n.
  - rewrite  plus_0_r in H. rewrite H. reflexivity.
  - rewrite <- plus_n_Sm in H. inversion H. apply IHn in H1. apply H1.
Qed.

こんな感じで、リストじゃなくて自然数だったらすぐ証明出来るよなあ。とか考えてたら、lengthから証明すりゃいいのか。と思いついた。

Lemma app_any_is_nil : forall X (l a:list X),
  l = a ++ l -> a = [].
Proof.
  intros.
  assert(length l = length (a++l)).  apply f_equal. assumption.
  rewrite app_length in H0.
  assert(length a = 0).
  induction (length l).
  - rewrite plus_0_r in H0. rewrite H0. reflexivity.
  - rewrite <- plus_n_Sm in H0. inversion H0. apply IHn in H2. assumption.
  (* length a = 0 -> a = [] の証明 *)
  - destruct a.
   + reflexivity.
   + inversion H1.
Qed.

冷静に考えると小学生並のことしかやってないな。
でも、楽しいし、解けたら嬉しいのでよいことにする。一人初等数学。