How to rewrite given two dependent types are equal in Coq

Question

I'm working on a proof using bit vectors from the bbv library which look like word : nat -> Set. I'm trying to prove that the most significant bit is the same if you chop off some lower-order bits:

Require Import bbv.Word.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Arith.Plus.

Lemma drop_msb : forall (n : nat) (x : word (S (S n))),
  wmsb x false = wmsb (wtl x) false.

To prove this, the following lemma seems useful:

Check wmsb_split2.
(*
wmsb_split2 :
  forall sz (w: word (sz + 1)) b,
    wmsb w b = if weq (split2 _ 1 w) (natToWord _ 0) then false else true.
*)

Now, here's my attempt at the proof:

Proof.
  intros n x.
  assert (Snp : S (S n) = S n + 1). {
    rewrite <- Nat.add_1_l.
    apply plus_comm.
  }
  assert (xeq : word (S (S n)) = word ((S n) + 1)). {
    rewrite Snp.
    reflexivity.
  }
  rewrite wmsb_split2. (* Error: Found no subterm matching "wmsb ?M1864 ?M1865" in the current goal. *)

Here is the proof state.

  n : nat
  x : word (S (S n))
  Snp : S (S n) = S n + 1
  xeq : word (S (S n)) = word (S n + 1)
  ============================
  wmsb x false = wmsb (wtl x) false

I'm confused why wmsb_split2 can't be applied; I see wmsb _ _ right there in the conclusion! Do I need some form of the uniqueness of identity proofs given in EqDepFacts?

I also have the extra assertions there in case I need to rewrite x, but I can't do that either.

Li-yao Xia Li-yao Xia · Accepted Answer · 2020-01-29T14:29:27

There is a simpler proof by computation: because word is defined as a list of bits indexed by its length, if you know that the length is S (S n), then the first two constructors of the list are uniquely determined, and that fact is provided by the lemma destruct_word_S.

destruct_word_S :
  forall (sz : nat) (w : word (S sz)),
    exists (v : word sz) (b : bool), w = WS b v

In this case, that allows you to rewrite x : word (S (S n)) twice, into some term WS b0 (WS b1 x''), that enables both wmsb and wtl to compute.

To use destruct_word_S for rewriting, you have to destruct the two exists to expose the equality w = WS b v.

Lemma drop_msb : forall (n : nat) (x : word (S (S n))),
  wmsb x false = wmsb (wtl x) false.
Proof.
  intros.
  destruct (destruct_word_S x) as [x' [b0 Ex]].
  destruct (destruct_word_S x') as [x'' [b1 Ex']].
  rewrite Ex.
  rewrite Ex'. cbn.
  (* Goal: wmsb x'' b1 = wmsb x'' b1 *)
  reflexivity.
Qed.

I'm confused why wmsb_split2 can't be applied; I see wmsb _ _ right there in the conclusion!

The length of the word is an implicit argument to wmsb, and that's what doesn't unify here: the wmsb_split2 lemma uses @wmsb (sz + 1) and your goal uses @wmsb (S (S n)) on the left-hand side, and @wmsb (S n) on the right-hand side. But sz + 1 is not convertible to S (S n) (i.e., they can not normalize to the same term, for any instantiation of sz).

When dealing with indexed types, such as word, which is indexed by the length, equality behaves quite unintuitively.

I find that what works well in this context is inversion principles, like destruct_word_S, formulated in terms of homogeneous equality, i.e., =/eq, where both sides have the same type.

In contrast, heterogeneous equality spells trouble, and that's what you are getting into when you start thinking in terms of "a word (S sz) is also a word (sz + 1)", trying to equate things of different types.

Sadly I don't know of a good way of gaining the proper intuition here, other than the less than satisfactory path of learning about dependent type theory, to treat eq as "just another inductive type", being aware of all the ways it does not behave like a naive idea of "equality".

How to rewrite given two dependent types are equal in Coq

1 Answers