CODEWITHSUNDEEP
coq
Daisuke Sugawara
Daisuke Sugawara

Reputation: 321

Prove equality of lists with list_beq

list_beq is generated by Scheme Equality for list..

I'm sure that l = v if list_beq A eq l v holds and want to prove it.

But, we can't proof that unless A and eq are not concrete.

So, I want to proof that when A = nat eq = 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.

I don't know how to do any more.

Please tell me how to do that.

Upvotes: 0

Views: 310

Answers (2)

larsr
larsr

Reputation: 5811

I think one reason for/benefit of using Schemes is to not have to do the induction and go through all the cases yourself.

If you search for list_beq that was generated by Scheme you find the generated lemma internal_list_dec_bl that can help you to reason about the absurd case you get when reasoning about 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.

Upvotes: 2

Daisuke Sugawara
Daisuke Sugawara

Reputation: 321

I have proved on my own.

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.

Upvotes: 1

Related Questions