用list_beq证明列表的相等性

Question

list_beq由Scheme Equality for list.生成。

我确信l = v如果list_beq A eq l v成立并想证明它。

但是，除非A和eq不是具体的，否则我们无法证明这一点。

所以，我想证明当A = nateq = Nat.eqb。

Require Import Coq.Lists.List.
Import ListNotations. 
From mathcomp Require Import ssreflect.
Scheme Equality for list.
Lemma list_eq (l v:list nat) : list_beq nat Nat.eqb l v = true -> l = v.
Proof.
case: l.
remember (list_beq nat Nat.eqb [] []).
destruct b;last first.
inversion Heqb.
destruct v => //.
intros.
destruct v => //.
rewrite /list_beq in H.
Abort.

我不知道该怎么做了。

请告诉我怎么做。

Answer 1

我认为使用Schemes的一个原因/好处是而不是必须自己进行归纳并查看所有案例。

如果你搜索由Scheme生成的list_beq，你会发现生成的引理internal_list_dec_bl，它可以帮助你推理关于list_eq_dec的荒谬案例。

Require Import List. Import ListNotations.
Scheme Equality for list.
Lemma list_eq (l v:list nat) : list_beq nat Nat.eqb l v = true -> l = v.
destruct(list_eq_dec _ PeanoNat.Nat.eqb) with l v as [H|H];
intros; try apply PeanoNat.Nat.eqb_eq in H. trivial. trivial. trivial.
exfalso.
apply H. apply internal_list_dec_bl with Nat.eqb.
apply PeanoNat.Nat.eqb_eq. apply H0.
Qed.

Answer 2

我已经自己证明了。

Require Import Coq.Lists.List  Coq.Bool.Bool.
Import ListNotations. 
Scheme Equality for list.
From mathcomp Require Import ssreflect.
Lemma list_eq (l v:list nat) : list_beq nat Nat.eqb l v = true -> l = v.
Proof.
- elim: l v.
remember (list_beq nat Nat.eqb [] []).
destruct b;last first.
inversion Heqb.
destruct v => //.
- intros.
destruct v => //.
rewrite /= in H0.
apply andb_true_iff in H0.
move: H0 => [left right].
f_equal.
apply PeanoNat.Nat.eqb_eq in left.
apply left.
apply H in right.
apply right.
Qed.