■

オバマがシリア攻撃で議会に諮るということ自体が、すでにアメリカの威信が低下してることを示してんのかもしんない。
あのクリントンですら独断先行でスーダン爆撃を強行していたころに比べると。

アメリカが無い世界とある世界の比較が出来ない以上、アメリカが介入することは本当に良いことかどうか、ということは分からんのであるが。

今日のCoq

apply

applyのつかいどころが今一分かってない。

1 subgoal
  
  SCase := "m = S m'" : String.string
  Case := "n = S n'" : String.string
  n' : nat
  IHn' : forall m : nat, true = beq_nat n' m -> n' = m
  m' : nat
  H : true = beq_nat n' m'
  ============================
   S n' = S m'

において、

 Lemma eq_remove_S : forall n m,
 n = m -> S n = S m.

という補題がある。

 apply eq_remove_S.

で

1 subgoal
  
  SCase := "m = S m'" : String.string
  Case := "n = S n'" : String.string
  n' : nat
  IHn' : forall m : nat, true = beq_nat n' m -> n' = m
  m' : nat
  H : true = beq_nat n' m'
  ============================
   n' = m'

こうなる。
HogeならばHuga という定理Ｌが存在し、
事実はHuga
apply Ｌ
で
事実はHoge
でええんかいな。ええっぽいな。
……
説明が最悪だな。
apply LでHogeが証明できれば、いまの事実Hugeは、証明できる。と言うべきだ。

• • -

inversion

  eq : length (v' :: l') = S n'
  ============================
   length l' = n'

で

inversion eq.

すると、

  eq : length (v' :: l') = S n'
  H0 : length l' = n'
  ============================
   length l' = length l'

うーむ。魔法にしか見えん。

Theorem eq_add_S : forall (n m : nat),
     S n = S m ->
     n = m.
Proof.
  intros n m eq. inversion eq. reflexivity. Qed.

  H : S n = S m
  ============================
   n = m

inversion H.で

  H : S n = S m
  H1 : n = m
  ============================
   m = m

これと大差ないことは、理屈では分かるんだけど。

• • -

嫁はんの体調がよさげでなによりだ。