我已经定义了列表的归纳定义(称为listkind
),以便我可以通过归纳listkind
而不是列表来轻松证明特定定理。
Inductive listkind {X}: list X -> Prop :=
| l_nil : listkind []
| l_one : forall a:X, listkind [a]
| l_app : forall l, listkind l -> forall a b, listkind ([a]++l++[b]).
(有了这个性质,为了证明关于列表的事情,我必须证明列表是 []、[a] 或 [a]++l++[b] 的情况,而不是列表是 [] 或a::l。在我的特定定理中,这些情况更适合,并使证明更简单。)
但是,为了能够在我的证明中使用 listkind,我必须证明
Lemma all_lists_are_listkind: (forall {X} (l:list X), listkind l).
尝试了各种方法后,我发现自己卡在了这一点上。我非常感谢看到如何执行这样的证明,最好使用最少的 coq 魔法。