在coq中,该destruct策略有一个变体接受"连接析取引入模式",允许用户为引入的变量分配名称,即使在解包复杂的归纳类型时也是如此.
coq中的Ltac语言允许用户编写自定义策略.我想写(实际上,维持)一种策略,在将控制权交给之前做一些事情destruct.
我希望我的自定义策略允许(或要求,更容易)用户提供我的策略可以提供的介绍模式destruct.
Ltac语法实现了什么？
我是一个Coq新手,因此为了提高我对证据检查的理解,我正在尝试使用Ssreflect库.
我在终端上运行的Mac OS v 10.10.3(Yosemite)上安装了Ssreflect v 1.5.
但是,当我尝试使用以下方法将库加载到CoqIDE 8.4p15中时:
Require Import ssreflect.
我收到错误:
Cannot find library ssreflect in loadpath
我尝试过使用:
Add LoadPath "/opt/local/lib/coq/user-contrib/Ssreflect/".
其中SSRCOQ_LIB当前设置,但我收到错误:
The file /opt/local/lib/coq/user-contrib/Ssreflect/ssreflect.vo contains library Ssreflect.ssreflect and not library ssreflect
感谢在CoqIDE中加载ssreflect库的任何帮助.
我正在尝试使用Function来定义使用度量的递归定义,并且我收到错误:
Error: find_call_occs : Prod
我在底部发布了整个源代码,但我的功能是
Function kripke_sat (M : kripke) (s : U) (p : formula) {measure size p}: Prop :=
match p with
| Proposition p' => L M (s)(p')
| Not p' => ~ kripke_sat M s p'
| And p' p'' => kripke_sat M s p' /\ kripke_sat M s p''
| Or p' p'' => kripke_sat M s p' \/ kripke_sat M s p''
| Implies p' p'' => ~kripke_sat M s p' \/ kripke_sat …我目前正在尝试从我的程序验证引理生成Haskell代码,如下所示:
Lemma the_thing_is_ok : forall (e:Something), Matches e (calculate_value e).
在结束我的部分之后,我做:
Extraction Language Haskell.
Recursive Extraction the_thing_is_ok
它似乎并不是真的很高兴,因为它返回以下错误:
__ = Prelude.error "Logical or arity value used"
我有另一个Lemma似乎确实输出得很好,但我无法弄清楚究竟是什么问题.有关如何解决该错误的任何线索？
我想使用集合,为此尝试使用MSets库.但我需要将函数从一种类型的集合写入另一种类型的集合,并且它与Coq的模块系统交互不良.
这是我面临的一个问题的例子.我想要一套类型T和套T*T.我加入投影功能proj1和proj2从一组对,和功能的获得一组值add_l并add_r创建从一个值组对和一组值.
我实例化我的模块nat.我创建了一组nat并调用add_l,但Coq并不知道这一点SNat.t并且S.S1.t是相同的.在这里,我可以直接创建一组类型S.S1.t,但如果它必须与更复杂的环境进行交互将会更加困难.
有可能让Coq理解SNat.t并且S.S1.t是一样的吗？或者我的问题有另一种解决方案吗？
Require Import MSets.
Module DecidablePair (DT1:DecidableType) (DT2:DecidableType) <: DecidableType.
Definition t : Type := DT1.t * DT2.t.
Definition eq x y := DT1.eq (fst x) (fst y) /\ DT2.eq (snd x) (snd y).
Lemma eq_equiv : Equivalence eq.
Proof.
split.
- split; reflexivity.
- split; symmetry; apply H. …如何使用在给定库中验证的结果？例如,我想Lemma peano_ind从库中使用BinInt.我用CoqIDE写这个:
Require Import BinInt.
Check peano_ind.
并获得"在当前环境中找不到参考peano_ind".错误.我也无法apply在证明期间使用它.
但是,它应该在那里,因为Locate Library BinInt.我看到Coq可以找到文件BinInt.vo,当我打开文件BinInt.v时我可以看到Lemma peano_ind.
我在Debian 9.0 + CoqIDE 8.5pl2和Windows 10 + CoqIDE 8.6上都有这个问题.
所有这一切都是因为我想对整数进行归纳.对此的不同解决方案也很不错,但我仍然因为缺乏使用以前经过验证的结果的能力而感到沮丧.
我对术语有以下定义：
Inductive term : Type :=
| Var : variable -> term
| Func : function_symbol -> list term -> term.
一个函数，该函数pos_list获取术语列表并为每个子术语返回“位置”列表。例如，对于[Var "e"; Func "f" [Var "x"; Func "i" [Var "x"]]]我来说，应该知道[[1]; [2]; [2; 1]; [2; 2]; [2; 2; 1]]每个元素在子项的树层次结构中的位置。
Definition pos_list (args:list term) : list position :=
let fix pos_list_aux ts is head :=
let enumeration := enumerate ts in
let fix post_enumeration ts is head :=
match is with
| [] => [] …MSets似乎是使用OCaml样式的有限集的方法。可悲的是，我找不到示例用法。
如何定义一个空的MSet或单例的MSet？如何将两个MSets结合在一起？
我有以下 Coq 环境。
1 subgoals
m : nat
IHm : forall n : nat, n + n = m + m -> n = m
n : nat
H : S (n + S n) = S (m + S m)
ll := ll : forall k : nat, k + S k = S k + k
这样做，只改变rewrite ll in HLHS ，而不改变RHS 。 应该适用于 nat 类型的所有变量。这里有什么问题吗？S (n + S n)S (S n + n)S …
假设我们有这样的事情:
假设x是实数.证明如果存在实数y,使得(y + 1)/(y-2)= x,则x <> 1".
如果以一种显而易见的方式制定它:forall x : R, (exists y, ((y + 1) * / (y - 2)) = x) -> x <> 1一个人很快遇到问题.
我们假设存在y这样的情况((y + 1) * / (y - 2)) = x).我错误地认为这也应该暗示这一点y <> 2吗？有没有办法在Coq中恢复这些信息？
当然,如果y存在,那么它不是2.如何在Coq中恢复这些信息 - 我是否需要明确地假设它(也就是说,无法以某种方式通过存在实例化来恢复它？).
当然,destruct H as [y]只是给我们((y + 1) * / (y - 2)) = x)了y : R,但现在我们不知道y <> 2.