我在Linux(Ubuntu 17.04)中成功安装了Coq 8.6和CoqIDE.但是,我不知道为了将SSReflect和MathComp添加到此安装中而继续.我检查过的所有参考资料似乎都让我很困惑.有没有人有一个直接和简单的食谱？我确实安装了opam.
我正在阅读ssreflect教程,内容如下:
下面,我们通过将命题陈述翻译成布尔对应物来证明...,这很容易用暴力证明.这种证明技术称为反射.Ssreflect的设计允许和ssreflect的精神建议广泛使用这种技术.
这(反射)是否意味着ssreflect假设排除中间(forall A:Prop, A \/ ~A)？
它看起来就是这种情况,因为所有布尔值都满足EM如果是这样,这将是遵循ssreflect样式的一个很大的假设.
另外,我不太了解下面的"本地"或"小规模"部分:
由于它通常在本地用于有效处理样张的小部分(而不是在整个校样结构中使用),这称为小规模反射,因此名称为ssreflect.
小部件与整体打样结构的含义是什么？这是否意味着我们可以在本地假设EM有时没有伤害并且一般不使用EM,或者这里的本地是否意味着其他东西？
另外,我在Coq方面经验不足,并且不太清楚"布尔对应物"上的这种"蛮力"风格(主要基于case我目前读到的分析)是否比香草Coq方式更有效.对我来说,蛮力不是很直观,在你看到结果之前不容易猜到.
有什么具体的例子来说明这里的效率吗？
我正在尝试处理ssreflect中的规范结构.我从这里获取了 2段代码.
我将为bool和选项类型带来件.
Section BoolFinType.
Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by case. Qed.
Definition bool_finMixin := Eval hnf in FinMixin bool_enumP.
Canonical bool_finType := Eval hnf in FinType bool bool_finMixin.
Lemma card_bool : #|{: bool}| = 2. Proof. by rewrite cardT enumT unlock. Qed.
End BoolFinType.
Section OptionFinType.
Variable T : finType.
Notation some := (@Some _) (only parsing).
Local Notation enumF T := (Finite.enum T).
Definition option_enum := None :: map some (enumF T).
Lemma …我想在 Coq/SSReflect 中创建一个归纳定义的枚举类型，例如
Inductive E: Type := A | B | C.
因为finType它显然是有限类型。我有三个解决方案来做到这一点，但所有的解决方案都比我预期的要复杂，而且永远不会令人满意。
在第一个解决方案中，我为eqType、choiceType和实现了 mixin countType。finType
Require Import all_ssreflect.
Inductive E := A | B | C.
Definition E_to_ord (e:E) : 'I_3.
by apply Ordinal with (match e with A => 0 | B => 1 | C => 2 end); case e.
Defined.
Definition E_of_ord (i:'I_3) : E.
by case i=>m ltm3; apply(match m with 0 => A | 1 => …什么是重写的最佳方式\sum_(i...) (F i - G i)是(\sum_(i...) F i - \sum_(i...) G i)与序数bigop，假设下溢得到妥善管理？
更准确地说，关于这些下溢，我对以下引理感兴趣：
Lemma big_split_subn (n : nat) (P : 'I_n -> bool) (F G : 'I_n -> nat) :
(forall i : 'I_n, P i -> G i <= F i) ->
\sum_(i < n | P i) (F i - G i) = \sum_(i < n | P i) F i - \sum_(i < n | P i) G i.
似乎big_split …
在我看来,ssreflect当我们进行依赖模式匹配时,隐式构造函数字段会变成显式字段,并且设置各种隐式选项不会影响此行为.
使用Coq 8.6可以使用以下代码:
Require Import Coq.Unicode.Utf8.
Set Implicit Arguments.
Set Contextual Implicit.
Inductive Vec (A : Type) : nat ? Type :=
nil : Vec A 0
| cons : ? {n}, A ? Vec A n ? Vec A (S n).
Fixpoint append {A n m}(xs : Vec A n)(ys : Vec A m) : Vec A (n + m) :=
match xs with
nil => ys
| cons x xs => cons x (append xs ys) …例如，coq 在其标准库中有一个 Classical 包，其中包含经典逻辑中的引理，例如与 forall 相关并存在的引理（https://coq.inria.fr/library/Coq.Logic.Classical_Pred_Type.html）。
我的问题是 mathcomp 或 ssreflect 本身是否有任何类似的支持。到目前为止，我发现的只是https://github.com/coq/stdlib2/blob/master/src/bool.v#L548 中的一些定义和引理
谢谢
我在Coq中使用MathComp库进行反射时遇到了一些非常简单的证明.
假设我想证明这个引理:
From mathcomp Require Import ssreflect ssrbool ssrnat.
Lemma example m n: n.+1 < m -> n < m.
Proof.
have predn_ltn_k k: (0 < k.-1) -> (0 < k).
by case: k.
rewrite -subn_gt0 subnS => submn_pred_gt0.
by rewrite -subn_gt0; apply predn_ltn_k.
Qed.
对于这样一个简单的任务,这种方法对我来说似乎有些"非正统".有更好/更简单的方法吗？