というわけで一通り証明が終わったようだ。
Include "../usr/guru-lang/lib/plus.g".
Include "../usr/guru-lang/lib/mult.g".
Include "../usr/guru-lang/lib/bool.g".
Define 3_8_1_1 := join (mult zero three) zero.
Classify 3_8_1_1.
Define 3_8_1_2 := join (lt zero three) tt.
Classify 3_8_1_2.
Define 3_8_1_3 := join (le one three) tt.
Classify 3_8_1_3.
Define 3_8_2 : Forall(x:nat). { (mult Z x) = Z } :=
foralli(x:nat).
join (mult Z x) Z.
Classify 3_8_2.
Define 3_8_3 : Forall(x:nat)(y:nat). { (lt Z (plus (S x) y)) = tt } :=
foralli(x:nat)(y:nat).
join (lt Z (plus (S x) y)) tt.
Classify 3_8_3.
Define 3_8_4 : Forall(x:bool). { (and ff x) = ff } :=
foralli(x:bool).
join (and ff x) ff.
Classify 3_8_4.
Define 3_8_5 : Forall(x:bool). { (and x x) = x } :=
foralli(x:bool).
case x with
ff => trans cong (and * *) x_eq
trans join (and ff ff) ff
symm x_eq
| tt => trans cong (and * *) x_eq
trans join (and tt tt) tt
symm x_eq
end.
Classify 3_8_5.
Define 3_8_6 : Forall(x:nat). { (le Z x) = tt } :=
foralli(x:nat).
case x with
default nat => hypjoin (le Z x) tt by x_eq end
end.
Inductive penta : type :=
MacBride : penta
| MacLean : penta
| Scharffer : penta
| Jessup : penta
| OldCapitol : penta.
Define clockwise :=
fun(p:penta).
match p with
MacBride => MacLean
| MacLean => Scharffer
| Scharffer => Jessup
| Jessup => OldCapitol
| OldCapitol => MacBride
end.
Define counter :=
fun(p:penta).
match p with
MacBride => OldCapitol
| MacLean => MacBride
| Scharffer => MacLean
| Jessup => Scharffer
| OldCapitol => Jessup
end.
Define theorem_penta : Forall(p:penta). { (clockwise (counter p)) = p } :=
foralli(p:penta).
case p with
default penta => hypjoin (clockwise (counter p)) p by p_eq end
end.3.8.6はhypjoin(85ページに記載がある)で簡略表記している。
同様の表記を愚直に書くとこの通り。
Define 3_8_6b : Forall(x:nat). { (le Z x) = tt } :=
foralli(x:nat).
case x with
Z => trans cong (le Z *) x_eq
join (le Z Z) tt
| S x' => trans cong (le Z *) x_eq
join (le Z (S x')) tt
end.
