Coq：在分离逻辑基础中比较一个 Int 和一个 Nat答案

【问题标题】：Coq: Comparing an Int to a Nat in Separation Logic FoundationsCoq：在分离逻辑基础中比较一个 Int 和一个 Nat
【发布时间】：2021-09-15 09:13:25
【问题描述】：

通过Separation Logic Foundations，我被困在Repr.v 中的triple_mlength 练习上。我认为我目前的问题是我不知道如何在 Coq 中处理 int 和 nat。

Lemma triple_mlength: forall (L: list val) (p:loc),
triple (mlength p)
       (MList L p)
       (fun r => \[r = val_int (length L)] \* (MList L p))

Check (fun L => val_int (length L)) 不会抛出错误，这意味着 length 可以是 int。但是，长度是不透明的，我无法展开它。

我目前的背景和目标：

x : val
p : loc
C : p <> null
x0 : loc
H : p <> null
xs : list val
IH : forall y : list val,
     list_sub y (x :: xs) ->
     forall p, triple (mlength p) 
                      (MList y p) 
                      (fun r:val => \[r = length y] \* MList y p)
______________________________________________________________
length xs + 1 = length (x :: xs)

取消设置目标转换为的打印符号：

eq (Z.add (length xs) (Zpos xH)) (length (cons x xs))

我认为试图将 (1:Z) 添加到 (length xs: nat)，然后将其与 (length (cons x xs) : nat) 进行比较

类型：

Inductive nat : Set := O : nat
                     | S : nat -> nat

Inductive Z : Set := Z0 : int 
                   | Zpos : positive -> int 
                   | Zneg : positive -> int

list: forall A, list A -> nat

length: forall A, list A -> nat

val_int: int -> val

Coq 版本是 8.12.2

【问题讨论】：

标签： coq proof theorem-proving

【解决方案1】：

在将length xs : nat 和length (x :: xs) : nat 转换为ints 的范围内有一个强制nat_to_Z : nat -> int。这与符号机制是分开的，因此当您只要求 Coq 显示符号时您看不到它。但是，它就在那里，您需要在证明中处理它。有一堆引理证明nat 操作和Z/int 操作之间的等价性。

加载您的文件并查看了一下（Search 是您的朋友！），看来您无法简化 length (x :: xs) = S (length xs) 的原因是因为有一个引理 length_cons 给出了 length (x :: xs) = (1 + length xs)%nat。我想这本书的作者出于某种原因认为这将是一个好主意，所以他们禁用了通常的简化。请注意，“通常”length 是透明的，simpl 可以实现这一目标。

使用length_cons 后，您可以使用plus_nat_eq_plus_int 将强制向下推到+ 下，然后Z.add_comm 完成。这条线应该满足目标。

now rewrite length_cons, plus_nat_eq_plus_int, Z.add_comm.

【讨论】：