如何根据Coq - 编程之家

如何解决如何根据Coq

我正在尝试根据我在上下文中使用的规范构建字节列表（该规范基于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.

解决方法

该问题由原始海报编辑，更改了声明。此消息的底部是原始问题的答案。

要解决此问题，您需要一个（尚未）存在于库中的定理，并且该定理包括在这里：

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.

利用该定理，您可以通过研究作为参数i给出的所有可能的索引nth_error来证明相等性。因此，您介绍了假设，然后应用了该定理，并介绍了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风格中，这些情况是通过书写来介绍的

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 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来转换{{1}的“数学组件”定义}，+，-和<转换为这些运算符的传统版本，然后<=才能解决问题。通常，lia应该得到改进，以便在更高版本的Coq中将不需要这种转换（我正在使用coq.8.12，并且仍然需要这种技巧）。

该语句的先前版本为false，并提示我生成以下反示例：

lia

此脚本混合了数学组件样式和香草coq样式，这是不好的味道。