如何根据 Coq 中的规范构建字节列表

Question

我正在尝试根据上下文中的规范构建字节列表（该规范是基于 nth_error 函数的结合定义的，这些函数确定索引处的字节值（或一系列索引中的字节值）。例如，请参阅以下目标和上下文。

a_len, b_len : nat
a : seq.seq byte
b : seq.seq byte
H : Datatypes.length a = a_len /\           (* the length of list I'd like to build *)
    Datatypes.length b = b_len /\           (* the length of another list concatenated at the end *)
    is_true (b_len + 4 <= a_len) /\         (* added after edit *)
    is_true (1 < b_len) /\                  (* added after edit *)
    nth_error a 0 = x00 /\                         (* the value of first byte is zero *)
    (forall i : nat,                               (* then we have a bunch of x01's *)
     is_true (0 < i) /\ is_true (i < a_len - b_len - 1) ->
     nth_error a i = Some x01) /\
    nth_error a (a_len - b_len - 1) = Some x00 /\  (* next byte is zero *)
    (forall j : nat,                               (* which ends with a list that is equal to b *)
     is_true (0 <= j) /\ is_true (j < b_len) ->
     nth_error a (a_len - b_len + j) = nth_error b j)
______________________________________(1/1)
a = [x00] ++ repeat x01 (a_len - b_len - 2) ++ [x00] ++ b

我尝试使用一些现有的引理，例如 nth_error_split，其定义为：

nth_error_split :
    forall [A : Type] (l : seq.seq A) (n : nat) [a : A],
    nth_error l n = Some a ->
    exists l1 l2 : seq.seq A,
      l = (l1 ++ (a :: l2)%SEQ)%list /\ Datatypes.length l1 = n

并像这样定义一些引理：

Lemma two_concats_equality1: 
    forall (lb1 lb1' lb2 lb2': list byte), 
           (lb1 ++ lb2) = (lb1' ++ lb2') /\ length lb1 = length lb1' -> lb1 = lb1' /\ lb2 = lb2'.

构建字节列表，a，从头开始使用 nth_error_split 并使用 two_concats_equality1 携带信息，并多次执行此操作直到结束。但还没有成功。我什至无法证明 two_concats_equality1 引理（暂时假设为真）。我卡在了字节重复的开头，nth_error a i = Some x01。

我想知道这是否是证明此目标的正确方法。如果没有，请告诉我你会怎么做。

如有任何意见，我们将不胜感激。

编辑：

正如@Yves 所指出的，我正在进行以下编辑：

更正上下文中的拼写错误。没有变量n，应该是a_len.
我在描述 a_len 和 b_len 的关系的规范中添加了两个约束，避免了提到的错误陈述。
在下面，您可以找到导入库的最小可重现示例。

From mathcomp Require Import all_ssreflect ssrnat.
From Coq Require Import Lia.
Require Import Init.Byte Coq.Lists.List.
Import ListNotations. 

Lemma build_from_spec : 
    forall (a_len b_len : nat) (a b : list byte),
    Datatypes.length a = a_len /\
    Datatypes.length b = b_len /\
    a_len >= b_len + 4 /\
    b_len >= 2 /\
    nth_error a 0 = Some x00 /\
    (forall i : nat, (0 < i) /\ (i < a_len - b_len - 1) ->
    nth_error a i = Some x01) /\
    nth_error a (a_len - b_len - 1) = Some x00 /\
    (forall j : nat, (0 <= j) /\ (j < b_len) ->
    nth_error a (a_len - b_len + j) = nth_error b j) 
    ->
    a = [x00] ++ repeat x01 (a_len - b_len - 2) ++ [x00] ++ b.
Proof.
Admitted.

Answer 1

问题被楼主编辑了，改了说法。此消息的底部是对原始问题的回答。

要解决这个问题，您需要一个（还）不存在于库中的定理，我将其包含在这里：

Lemma eq_from_nth_error {A : Type} (l1 l2 : list A) :
  (forall i, nth_error l1 i = nth_error l2 i) -> l1 = l2.
Proof.
elim: l1 l2 => [ | a l1 IH] [ | a' l2] //.
    by move=> abs; have := (abs 0).
  by move=> abs; have := (abs 0).
move=> cmp; congr (_ :: _).
  by have := (cmp 0) => /= [[]].
apply: IH=> i; exact (cmp i.+1).
Qed.

利用这个定理，您可以通过研究作为参数给 nth_error 的所有可能索引 i 来证明等式。所以，你介绍你的假设，然后你应用这个定理，你介绍 i，然后你看看 i:

的 5 种可能情况

如果i = 0,
如果0 < i < a_len - b_len - 1
如果i = a_len - b_len - 1
如果a_len - b_len - 1 < i < a_len
如果a_len <= i

在ssreflect风格中，这些case是通过写作来介绍的

have [/eqP i_is_0 | i_is_not_0] := boolP(i == 0).

have [i_lt_border | is_larger] := boolP(i < a_len - b_len - 1).

等等。您将能够完成证明。你让你的生活变得复杂，因为你的语句是使用算术语句的数学组件版本编写的：(i < a_len) 是一个 lia 无法识别的布尔表达式，因此你需要执行很多操作使事情正常进行的转换。这是一个示例问题。

Lemma arithmetic_difficulty i j : i + 3 < j - 2 -> i <= j.
Proof.
Fail lia.
rewrite -?(minusE, plusE).
move/ltP => i3j2.
apply/leP.
lia.
Qed.

所以你看，我需要使用重写定理minusE、plusE、ltP和leP来转换[=的“数学分量”定义28=、-、<和<=这些运算符的传统版本，在lia之前可以解决问题。通常情况下，lia应该改进一下，这样在以后的Coq版本中就不需要这种转换了（我用的是coq.8.12，这个技巧还是需要的）。

先前版本的声明是错误的，并提示我生成以下反例：

From mathcomp Require Import all_ssreflect.

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

Section some_context.

Definition byte := nat.
Variables x00 x01 : byte.

Lemma Dan_problem : (forall (a_len b_len : nat)
(a b : seq byte)
(H : Datatypes.length a = a_len /\
    Datatypes.length b = b_len /\
    List.nth_error a 0 = Some x00 /\
    (forall i : nat,
    is_true (0 < i) /\ is_true (i < a_len - b_len - 1) ->
      List.nth_error a i = Some x01) /\
    List.nth_error a (a_len - b_len - 1) = Some x00 /\
    (forall j : nat,
      is_true (0 <= j) /\ is_true (j < b_len) ->
      List.nth_error a (a_len - b_len + j) = List.nth_error b j)),
a = [:: x00] ++ List.repeat x01 (a_len - b_len - 2) ++ [:: x00] ++ b) ->
   False.
Proof.
intros abs.
assert (cnd1 : forall i,  0 < i /\ i < 1 - 0 -1 ->
  List.nth_error [:: x00] i = Some x01).
  by move=> i [igt0 ilt0].
assert (cnd2 : forall j : nat,
          0 <= j /\ j < 0 ->
         List.nth_error [:: x00] (1 - 0 + j) = List.nth_error [::] j).
  by move=> j [jge0 glt0].
generalize (abs 1 0 (x00::nil) nil (conj erefl
    (conj erefl (conj erefl (conj cnd1 (conj erefl cnd2)))))).
by rewrite /=.
Qed.

这个脚本混合了数学组件风格和香草 coq 风格，这是不好的味道。

如何根据 Coq 中的规范构建字节列表

How can I build a list of bytes from its specification in Coq

formal-verification

proof

coq

coq-tactic