Coq：在分离逻辑基础中比较 Int 和 Nat

如何解决Coq：在分离逻辑基础中比较 Int 和 Nat

经历了 Separation Logic Foundations 后，我被困在 Repr.v 中的 trile_mlength 练习中。我认为我目前的问题是我不知道如何在 Coq 中处理 ints 和 nats。

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

解决方法

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

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

使用simpl后，可以使用length_cons将强制下推到plus_nat_eq_plus_int下，然后+结束。这条线应该满足目标。

Z.add_comm