一日目

とりあえず、使ってみないと分からんよな〜という話なんだが、Sparkleってマニュアルとかないのかよ。Cleanコミュニティのやる気のなさは異常(まあ単に人が少ないというだけなんだろうが)。細かくメモっとかないと自分で使い方を忘れそうlol

0.Sparkleが組み込まれたClean処理系を取ってくる
1.Examples/IO Proofs Example/ioproofs.prjをCleanで開く
2.(必要ならProject>Bring Up To Dateして)Project>Theorem Prover Projectを開く
3.Sparkleが起動したら、Section Centreウィンドウのload sectionをクリック。適当にlistsとかを選択
4.Section Centreに出てくるのは、証明済みの定理一覧っぽい
適当に、lists(54)→++_x_Nilとか選ぶと、「forall xs. xs++[] = xs」の証明が載ってる。基本的には帰納法だけ。まあ、Coqっぽいかなー。Coqとかもう忘れたよ！

てことで、使い方を知るために、Theorems>New Theoremを開く。適当に、定理名入れて、"Enter initial proposition for new Theorem:"の欄に"ls++[]=ls"と入れて、Create Theoremボタンを押す。Theorems>Prove topmost theoremを選択。で、以下は、List of tacticsウィンドウから、tacticをポチポチ選びながら証明を進めるらしい

1.まず、lsに関する帰納法。Inductionを選択してデフォルトのままOKを押す

2."⊥++[]=[]"を証明しろと言われる。これはDefinedness(って何?)を選べばよい

3.次は,[]++[]=[]を証明。Reduce tacticsを選択して、デフォルトのままOK。証明図が[]=[]に簡約されるので、Reflexiveを選択(つうか、Trivialじゃないのかよ)

4.次は、帰納法のステップ
forall l:a.forall ls:[a].ls++[]=ls -> [l:ls]++[]=[l:ls]
の証明。Introduce押して、そのままOK

5.l:a , ls:[a] , IH:ls++[]=lsという仮定から[l:ls]++[]=[l:ls]を証明するように言われる。Reduce、Injectiveをデフォルトのまますすめる。Reduceはいいとして、Injectiveが微妙に謎

6.さっきの仮定から、l=l and ls++[]=lsを導くように言われる。l=lとls++[]=lsをそれぞれ示せばいい。l=lはさっきと同様、Reflexiveで、ls++[]=lsは帰納法の仮定。具体的には、Split、reflexive、exact tacticを順に選択。以上で終わり

まあ、おおまかな使い方は分かった。Coqを使ったことあれば、大体一緒かな〜。Cleanはnon-strictなんで、しばしばボトムの扱いに注意しないといけない。

感想
・徹底したGUIウザイ
・コピペすらできない