当使用归纳时,我想假设n = 0和n = S n’来分离案例. Section x. Variable P : nat -> Prop. Axiom P0: P 0. Axiom PSn : forall n, P…

如何在HomCategory中使用类别中定义的符号？ Module Type Category. Parameter Object : Type. Parameter Arrow : Object -> Objec…

我试图写一个感应假设专门用于证明偶数的性质.我制定并证明了以下内容： Theorem ind_hyp_on_evens: forall (p : nat -> Prop), (p 0 -> (forall n…

我正在编写一种策略来查找与绑定列表中的键相关联的值.就像是： Require Import String List Program. Ltac assoc needle haystack := match haystac…

据我所知,Coq中的函数调用是不透明的. 有时,我需要使用展开来应用它,然后折叠以将函数定义/正文转回其名称.这通常很乏味.我的问题是,是否有更简单的方法来应用函数调用的特定实例？ 作为一个最小的例子,对于列表l,证明r…

我想知道简化策略在COQ中如何运作. 假设以下引理： Parameter n:nat. Lemma test: S n + 0 = S (n+0). 现在,简单.策略产生 S (n + 0) = S (n + 0) 我的…