小编use*_*393的帖子

这是一个递归函数all_zero,用于检查自然数列表中的所有成员是否为零:

Require Import Lists.List.
Require Import Basics.

Fixpoint all_zero ( l : list nat ) : bool :=
  match l with
  | nil => true
  | n :: l' => andb ( beq_nat n 0 ) ( all_zero l' )
  end.

现在,假设我有以下目标

true = all_zero (n :: l')

我想用这个unfold策略将其转化为

true = andb ( beq_nat n 0 ) ( all_zero l' )

不幸的是,我不能用一个简单的方法来做,unfold all_zero因为战术会急切地找到并替换所有的实例all_zero,包括一次展开形式的实例,它变成一团糟.有没有办法避免这种情况并只展开一次递归函数？

我知道我可以通过证明临时等价来获得相同的结果assert (...) as X,但效率很低.我想知道是否有一种简单的方法可以做到这一点unfold.

这是我对回文的归纳定义:

Inductive pal { X : Type } : list X -> Prop :=
  | pal0 : pal []
  | pal1 : forall ( x : X ), pal [x]
  | pal2 : forall ( x : X ) ( l : list X ), pal l -> pal ( x :: l ++ [x] ).

我想从Software Foundations中证明这个定理:

Theorem rev_eq_pal : forall ( X : Type ) ( l : list X ),
  l = rev l -> …

CPDT的第三章简要讨论了为什么在Coq中禁止负归纳类型.如果我们有

Inductive term : Set :=
| App : term -> term -> term
| Abs : (term -> term) -> term.

然后我们可以轻松定义一个函数

Definition uhoh (t : term) : term :=
  match t with
    | Abs f => f t
    | _ => t
  end.

因此该术语uhoh (Abs uhoh)将是非终止的,"我们将能够证明每个定理".

我理解非终止部分,但我不知道如何用它来证明任何东西.如何False使用term上面定义的证明？

这是pc我在数学定理中使用的归纳类型.

Inductive pc ( n : nat ) : Type :=
  | pcs : forall ( m : nat ), m < n -> pc n
  | pcm : pc n -> pc n -> pc n.

另一种归纳类型pc_tree,它基本上是一个包含一个或多个pcs 的二叉树.pcts是包含单个叶节点的构造pc,并且pctm是一个包含多个内部节点构造pc秒.

Inductive pc_tree : Type :=
  | pcts : forall ( n : nat ), pc n -> pc_tree
  | pctm : pc_tree -> pc_tree -> pc_tree.

并且是一个归纳定义的命题 …

我试图在Prolog中编码基本的逻辑推理,我想定义一些自定义运算符来简化表示法.如果我能|-为⊢ 打字,那将会很方便.所以我试过了

:- op(1150, xfy, [ '|-' ]).
gamma |- a.
Gamma |- or(A,_) :- Gamma |- A.
Gamma |- or(_,A) :- Gamma |- A.

但是当我尝试查询时gamma |- or(a,X),我收到错误消息

ERROR: '<meta-call>'/1: Undefined procedure: gamma/0

而不是true我期望的.

问题似乎是定义的运算符包括垂直条形字符.如果我将知识库修改为

:- op(1150, xfy, [ imp ]).
gamma imp a.
Gamma imp or(A,_) :- Gamma imp A.
Gamma imp or(_,A) :- Gamma imp A.

然后Prolog在回答查询时没有问题gamma imp or(a,X).垂直条是保留字符,我不允许在定义中使用吗？或者有什么方法可以解决这个问题？

据我所知,在Vim中定义特定于文件类型的行为的推荐方法是使用.vimfiles和filetype pluginoption..html例如,要添加文件设置,我会添加filetype plugin on我的.vimrc并添加设置~/.vim/ftplugin/html.vim.

然而,我能找到的这种方法的所有例子都是关于流行的现有文件类型,如.html或.sql.相同的修复程序是否适用于自定义文件类型？假设我想使用带扩展名的新文件类型.newft.如果我~/.vim/ftplugin/newft.vim使用这种新类型和加载的设置创建somefile.newft,Vim会自动检测其类型和加载newft.vim吗？

我问这个是因为这正是我正在做的事情,到目前为止它还没有奏效.我想知道这是一个错误还是Vim的预期行为.

在大多数编程语言中，'c'是一个字符，"c"也是一个长度为 1 的字符串。但是 Coq（根据其标准 ascii 和字符串库）使用"c"这两者作为表示法，这需要不断使用 来Open Scope明确所指的是哪一个。如何避免这种情况并以通常的方式用单引号指定字符？如果有一个解决方案仅部分覆盖标准库，更改表示法但回收其余部分，那就太好了。

假设R某种类型存在否定关系A.

Variable A : Type.
Variable R : A -> A -> A -> A -> A -> A -> A -> A -> A -> A -> Prop.

X并且Y是略微不同的命题,它们都断言R持有超过10个类型的术语A.

Inductive X : Prop :=
| X_intro : forall a0 a1 a2 a3 a4 a5 a6 a7 a8 a9, 
R a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 -> X. 

Record Y : Prop :=
{ a0 …

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

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