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のようなコマンドが追加できるように頑張ろう。