COQ-将表达式分配给变量

Question

首先，我还不熟悉Coq Lingo，因此我将宽松地使用EG'expression'和``变量''之类的术语，但是它们可能不是正确的COQ术语。

我正在尝试证明定理的以下子缘。

1 goal
b : bag
v, b' : nat
b'' : natlist
B : b = b' :: b''
IHb'' : b = b'' -> count v (add v b'') = count v b'' + 1
______________________________________(1/1)
S match v =? b' with
  | true => S (count v b'')
  | false => count v b''
  end = match v =? b' with
        | true => S (count v b'')
        | false => count v b''
        end + 1

您可以忽略s和+ 1，我基本上正在寻找一种分配

match v =? b' with
  | true => S (count v b'')
  | false => count v b''
  end

给类型nat的 方法方程式的侧面。 我该怎么做？或者我需要进行销毁v和b'并分别证明所有情况吗？

Answer 1

这是两种可能性。可能会有更好的。

您可以使用 为一个术语命名。该术语的所有出现都被变量所取代。

set (x := match v =? b' with
          | true => S (count v b'')
          | false => count v b''
          end).

有时，您需要隐藏变量的定义，并且只能记住它是根据需要调用的平等。为此，使用 记住 。

您可以使用 上下文 匹配目标 ，并为该模式中的任何内容命名。

match goal with |- context [S ?_x = ?_x + 1] => set (x := _x) end.

如果这是您的真正目标，而不是简化的例子，那么这是一个简单的算术语句#COQ：tacn.lia“ rel =” nofollow noreferrer“> lia ，让Coq弄清楚。

Require Import Lia.

…
lia.

Answer 2

除了吉尔斯的建议外，您还可以使用代码> 为了实现这一目标，至少以两种方式说明了此处：

Require Import Arith ssreflect.

Variables v b' b'' : nat.
Variable count : nat -> nat -> nat.

Goal
 S match v =? b' with
   | true => S (count v b'')
   | false => count v b''
   end
 = match v =? b' with
   | true => S (count v b'')
   | false => count v b''
   end + 1.
Proof.
  set t := (X in S X = X + _).
  Undo.
  set t := match _ with true => _ | false => _ end.
Abort.

后者也可以与常规set ，但需要括号：

  set (t := match _ with true => _ | false => _ end).