coq 中 case 策略的语法

Question

有人可以向我解释一下下面的 coq 策略是做什么的吗？ case x : fun H => [|[]] // _. 我如何使用 destruct 重写它？

更好的是，任何人都可以指出我在 coq 文档中解释上述语法的地方吗？

Answer 1

最初发布中给出的示例无法解析，因此这里尝试生成类似的

case

命令，但没有语法错误。

case :

是

ssreflect

习语的一部分。

case 

name

:

value

.

与

destruct 

value

eqn:

name 的作用大致相同。这

=>

是关于在每种情况下制作介绍模式。

在这里，我将解释以下行的行为：

case name : x H => [|[]] // _.

这对

x

进行了析构（我们期望

x

属于具有两个构造函数的类型，第二个构造函数具有一个本身为归纳类型的参数；如果

x

属于类型

nat

这将工作）。

现在有一个微妙之处，即

H

出现在

x

和

=>

之间。这意味着

H

假设将恢复到以下结论： 执行

case

命令之前的目标。

revert H; destruct x as [ | [ | temporary_name]] eqn:name; try easy; intros _" 

这里的

try easy

代表 ssreflect 习惯用法中使用的

\\

。

intros _

在这里代表 ssreflect 行末尾的

_

：它在剩余情况下删除了

H

的相应实例，可能是因为这包含了无用的事实。

这个解释并不完全匹配，因为

case ... : ...

不执行任何操作 修改目标，而

destruct

修改任何发生

x

的假设。

这是一个会话示例，其中两种策略的行为相同：

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section sandbox.

Variable P : nat -> Prop.


Lemma toto (x : nat) (H : x == 1) : P x.
Proof.
revert H; destruct x as [| [| temporary]] eqn: name; try easy; intros _.
Abort.

Lemma titi (x : nat) (H : x == 1) : P x.
Proof.
case name : x H => [|[]] // _.
Abort.