4.6 Commutativity of Addition in Guru

Commutativityの証明。

Include "../guru-lang/lib/plus.g".

Define ch4_th : Forall(n m:nat). { (plus n m) = (plus m n) } :=
  induction(n:nat)
    return Forall(m:nat). { (plus n m) = (plus m n) }
  with
    Z => foralli(m:nat).
         trans cong (plus * m) n_eq      % (plus n m) = (plus Z m)
         trans join (plus Z m) m         % (plus Z m) = m
         trans cong * symm [plusZ m]     % m = (plus m Z)
               cong (plus m *) symm n_eq % (plus m Z) = (plus m n)
    | S n' => foralli(m:nat).
         trans cong (plus * m) n_eq                 % (plus n m) = (plus (S n') m)
         trans join (plus (S n') m) (S (plus n' m)) % (plus (S n') m) = (S (plus n' m))
         trans cong (S *) [n_IH n' m]               % (S (plus n' m)) = (S (plus m n'))
         trans cong * symm [plusS m n']             % (S (plus m n')) = (plus m (S n'))
               cong (plus m *) symm n_eq            % (plus m (S n')) = (plus m n)
  end.

plusZとplusSは、plus.gに以下のように定義されている。

plusZ : Forall(n:nat). { (plus n Z) = n }
plusS : Forall(n m : nat). { (plus n (S m)) = (S (plus n m))}

これで既存のlemmaの使い方も分かった。

合わせてGuruのソースコードも眺めているのだが・・・。
Yeti(http://mth.github.com/yeti/)もそうだけど
この手の言語はパーサを手作りするのが慣習なのだろうか。
あと、JDK1.4に合わせて作ってる。

hypjoinのようなコマンドが追加できるように頑張ろう。