CPDT の第 3 章では、Coq で負の帰納型が禁止されている理由について簡単に説明しています。もし私たちが持っていたら
Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.
次に、関数を簡単に定義できます
Definition uhoh (t : term) : term :=
match t with
| Abs f => f t
| _ => t
end.
そのため、用語uhoh (Abs uhoh)は非終了になり、「すべての定理を証明できる」ようになります。
非終了の部分は理解できますが、それで何かを証明する方法がわかりません。上記で定義したFalse使用法をどのように証明しますか?term