标签: coq

假设我有一个假设和上下文中的H : forall ( x : X ), P x变量。x : X我想进行通用实例化并获得新的假设H' : P x。最无痛的方法是什么？显然apply H in x不起作用。assert ( P x )其次是apply Hdos，但是如果很复杂的话可能会变得非常混乱P。

有一个类似的问题似乎有些相关。但不确定它是否可以应用在这里。

所以我有两个假设，一个是h : A -> B，另一个是h2 : A。我怎样才能h3 : B出现在我的假设中？

我想证明一些简单的事情，例如对于每个自然数 n，都存在一个自然数 k 使得：

(2*n + 1)^2 = 8*k + 1

这样的证明是如何进行的呢？我想把它分成 n 是奇数或偶数的情况，但我不知道在 Coq 中如何做到这一点。另外，Coq 中是否有内置的幂（指数）运算符？

我知道排除中间在构造逻辑中是不可能的。然而，当我尝试在 Coq 中展示它时，我陷入了困境。

Theorem em: forall P : Prop, ~P \/ P -> False.

我的做法是：

intros P H.
unfold not in H.
intuition.

系统说如下：

2 subgoals
P : Prop
H0 : P -> False
______________________________________(1/2)
False
______________________________________(2/2)
False

我应该如何进行？谢谢

I'm writing a fixpoint that requires an integer to be incremented "towards" zero at every iteration. This is too complicated for Coq to recognize as a decreasing argument automatically and I'm trying prove that my fixpoint will terminate.

I have been copying (what I believe is) an example of a well-foundedness proof for a step function on Z from the standard library. (Here)

Require Import ZArith.Zwf.

Section wf_proof_wf_inc.
  Variable c : Z.
  Let Z_increment (z:Z) := (z + ((Z.sgn c) …

如何在（纯）构造演算中定义递归函数？我在那里没有看到任何固定点组合器。

我试图直接从字段的公理证明简单的字段属性。在对 Coq 的原生字段支持（就像这个）进行了一些实验之后，我决定最好简单地写下 10 条公理并使其自包含。当我需要使用rewrite我自己的==操作员时，我遇到了一个困难，这自然是行不通的。我意识到我必须添加一些==自反的、对称的和可传递的公理，但我想知道这是否就够了？或者也许有更简单的方法来使用rewrite用户定义==？这是我的 Coq 代码：

Variable (F:Type).
Variable (zero:F).
Variable (one :F).
Variable (add: F -> F -> F).
Variable (mul: F -> F -> F).
Variable (opposite: F -> F).
Variable (inverse : F -> F).
Variable (eq: F -> F -> Prop).

Axiom add_assoc: forall (a b c : F), (eq (add (add a b) c) (add a (add b c))).
Axiom mul_assoc: forall …

对于我通过 Coq 编写群论的项目，显然 3 个元素的关联性是给定的，但是我正在努力证明它适用于长度为 n 的字符串。也就是说， (x1 * ... * xn) 总是相同的，无论有多少括号，或者有多少位置。相关的组代码是

Structure group :=
{
  e : G;
  Op : G -> G -> G;
  Inv : G -> G;

  Associativity : forall (x y z : G), Op x (Op y z) = Op (Op x y) z;
  LeftInverse : forall (x : G), Op (Inv x) x = e;
  LeftIdentity : forall (x : G), Op e x = x;
}.

这不是我有问题的证据本身，而是如何对其进行编码。我可以看到至少我需要一个进一步的函数来允许我对字符串进行操作而不仅仅是元素，但我不知道如何开始。任何指针？

我正在按照这些说明使用 opam 安装 coq并收到错误消息

`No solution for coq: The following dependencies couldn't be met:
          - coq ? ocaml < 4.10
              base of this switch (use '--unlock-base' to force)

我继续使用以下命令切换到 ocaml 4.05.0

opam switch create with-coq 4.05.0

并且可以成功安装 Coq，但我更愿意使用 ocaml 的更新版本。这是 Coq 和 oCaml 之间的实际不兼容，还是我做错了什么？

对于添加的上下文，我现在使用 opam 2.0.6、ocaml 版本 4.05.0 和 Coq 版本 8.11.0。我的操作系统是 macOS。之前，唯一的区别是我尝试使用 ocaml 4.10.0。

谢谢！

我有一个由两部分组成的问题。目标：我想定义给定类别内部的类别概念。

1. 我想出了以下简单的代码，但是会产生一个莫名其妙的错误消息，即：

文件“./Category.v”，第 5 行，第 4-5 个字符：语法错误：在 [record_fields] 之后出现“}”（在 [constructor_list_or_record_decl] 中）。

Record Category :=
{   Ob : Type;
    Hom : Ob -> Ob -> Type;
    _o_ : forall {a b c}, Hom b c -> Hom a b -> Hom a c;
    1 : forall {x}, Hom x x;
    Assoc : forall a b c d (f : Hom c d) (g : Hom b c) (h : Hom a b),
    f o (g o h) = (f o g) …