Coq

プログラム全体を一つの関数とみなしたり、関係の命題として表したり、自分には超難しい。証明もくそ長くなってきて手に負えなくなりつつある。

そろそろ限界か。

見たことないタクティックの使い方もやたら出てくんですが。

• apply (H0 x) in H1.
  • apply withをH1仮説上で使用する方法？でいいの？
• assumption.
  • そのままで適用出来る仮定があれば適用してくれる。

まあしかし、未だにapply withの使いかたすらよくわかってない。