SearchAbout

Coq modeで
C-c C-f
Find theorems containing:
とミニバッファに出るので、定理を探したい型とか名前の一部とか入れると検索してくれる。

---

Coqはまだ面白いけど、非形式証明になるとさっぱりお手上げ。
数学苦手。nとn'が同時に出てこられると混乱するんですが。

以下引用

証明: l についての帰納法で証明する。

    まず、 l = [] と仮定して
            length (snoc [] n) = S (length [])

    を示す。これは length と snoc の定義から直接導かれる。

    次に、 l = n'::l' かつ
            length (snoc l' n) = S (length l')

    と仮定して、
            length (snoc (n' :: l') n) = S (length (n' :: l'))

    を示す。 length と snoc の定義から次のように変形できる。
            S (length (snoc l' n)) = S (S (length l'))

    これは帰納法の仮定から明らかである。