标签: coq

我已经困惑了几个小时,我无法弄清楚如何证明

forall n:nat, ~n<n

在Coq.我真的需要你的帮助.有什么建议？

liftM2 {A B R : Set} {m} {x : Monad m} (f : A -> B -> R) (ma : m A) (mb : m B) : (m R)

有没有减少这种类型的技巧？我有一个多余x的.

Monad是一个类型类: (Set -> Set) -> Type

我正在学习Coq.我陷入了一个非常愚蠢的问题(没有动力,真的很傻).我想构建一个从2,+ oo]到映射x到x-3的整数集的函数.这应该很简单...... 我知道,任何语言都很简单.但不是在Coq.首先,我写(我解释了很多细节,以便有人可以解释我在Coq的行为中不理解的东西)

Definition f : forall n : nat, n > 2 -> nat.

我得到了一个子目标

  ============================
   forall n : nat, n > 2 -> nat

这意味着Coq想要一个从n> 2的证明到整数集的映射.精细.所以我想告诉它n = 3 + p对于某个整数p,然后返回整数p.我写 :

intros n H.

我得到了上下文/子目标

  n : nat
  H : n > 2
  ============================
   nat

然后我想我已经证明n = 3 + p对于某个整数p by

cut(exists p, 3 + p = n).

我得到了上下文/子目标

  n : nat
  H : n > 2
  ============================
   (exists p : nat, 3 + p = …

我试图get使用子集类型为列表执行安全功能.我用程序试了这个定义

Program Fixpoint get A (l : list A) (n : {x : nat | x < length l} ) : A :=
  match (n, l) with
  | (O, x :: l') => x
  | (S n', x :: l') => get l' n'
  | _ => _
  end.

问题是它得到以下错误

Found a constructor of inductive type nat while a constructor of sig is expected.

为什么coq不允许我在包含子集类型的对中进行模式匹配？

同一个Linux命令在一个环境中成功,而在另一个环境中失败:

$ coqtop -lv test.v -I Lib

我得到的失败是Debian延伸和Coq v8.5

$ uname -a
Linux front 4.8.0-1-amd64 #1 SMP Debian 4.8.7-1 (2016-11-13) x86_64 GNU/Linux

$ coqtop -v
The Coq Proof Assistant, version 8.5 (June 2016)
compiled on Jun 9 2016 12:4:46 with OCaml 4.02.3

我得到的错误信息是:

Welcome to Coq 8.5 (June 2016)
Require Import libtest.
Error during initialization:
File "/home/user/dev/coq/test.v", line 1, characters 15-22:
Error: Unable to locate library libtest.

与同一源相关的相同命令成功的环境是:

$ uname -a 
Linux back 3.16.0-4-amd64 #1 SMP Debian 3.16.36-1+deb8u2 (2016-10-19)x86_64 GNU/... …

是否有一种策略可以使用而不是replace在下面的示例中来简化此表达式？

Require Import Vector.

Goal forall (n b:nat) (x:t nat n), (map (fun a => plus b a) x) = x.
Proof.
  intros n b x.
  replace (fun a => plus b a) with (plus b) by auto.
  ...

考虑以下修复点:

Require Import Coq.Lists.List.
Import ListNotations.

Inductive my_type: Type:=
| Left: my_type
| Right: my_type
.

Fixpoint decrease (which: my_type) (left right: list my_type) : list my_type :=
match which with
| Left =>
  match left with
  | [] => []
  | a::tl => decrease a tl right
  end
| Right =>
  match right with
  | [] => []
  | a::tl => decrease a left tl
  end
end.

Coq拒绝以下修复点,因为它无法猜测减少的修复点(有时候left列表会失去它的头部,有时候它就是那个right).

这个答案表明,人们可以通过使用Program Fixpoint和指定一个来解决这个问题{measure …

Include M1M说另一个模块内部的确切语义是什么？与Import M1在模块M内部进行操作有何不同？更准确地说，以下命令的语义是什么：

Module Type M := M1 <+ M2 <+ M3.

我想写一个带有可选变量名的策略.最初的战术看起来像这样:

Require Import Classical.

Ltac save := 
  let H := fresh in
  apply NNPP;
  intro H;
  apply H.

我想让用户有机会选择他想要的名字,并使用它:save a例如.

我用这个解决方案编写了一个变体:

Require Import Classical.

Inductive ltac_No_arg : Set :=
  | ltac_no_arg : ltac_No_arg.

Ltac savetactic h := 
  match type of h with
    | ltac_No_arg => let H := fresh in
      apply NNPP;
      intro H;
      apply H
    | _ => apply NNPP;
      intro h;
      apply h
  end.

Tactic Notation "save" := savetactic ltac_no_arg.
Tactic Notation …

对于该类型：

Record Version := mkVersion { 
  major  : nat; 
  minor  : nat; 
  branch : {b:nat| b > 0 /\ b <= 9};
  hotfix : {h:nat| h > 0 /\ h < 8} 
}.

我正在尝试举一个例子：

Example ex1 := mkVersion 3 2 (exist _ 5) (exist _ 5).

它失败了：

术语“存在？P 5”的类型为“？P 5-> {x：nat |？P x}”，而术语为“ {b：nat | b> 0 / \ b <= 9}”。 。

我想念什么？