The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Why does the "rewrite H" fail in np_true?  I am trying to write a (dependent) type function, np_total, that takes a binary natural number N, a proof that it's  less than 256, and returns a byte.  It's fairly straightforward but the problem happens when I am trying to prove the correctness lemma,  np_true. Based on my understanding, so far, of Coq, I need to generalise the terms and therefore this (enriched/generalised) return type:  match (np <? 256) as b return ∀ mp, np = mp ->  (mp <? 256) = b -> _ with but the problem is no matter how I generalise (I have tried a few), I am not able to prove the lemma np_true.  I understand that I can write it as a Sigma type, which is fairly straightforward [1], but I am interested in knowing how to solve this problem.

Lemma np_true : forall np (H : np <? 256 = true) x, of_N np = Some x -> np_total np H = x.
Proof.
  intros. unfold np_total.
(* this rewrite fails *)
 Fail rewrite H.

Definition np_total (np : N):  (np <? 256 = true) ->  byte.
Proof.
  intros H.
  refine(match (np <? 256) as b return ∀ mp, np = mp ->
      (mp <? 256) = b -> _ with
   | true => fun mp Hmp Hmpt =>
      match of_N mp as npt return _ = npt -> _ with
      | Some x => fun _ => x
      | None => fun Hf => _  
      end eq_refl
   | false => fun mp Hmp Hmf => _
  end np eq_refl eq_refl).
  abstract(
  apply of_N_None_iff in Hf;
  apply N.ltb_lt in Hmpt; nia).
  abstract (subst; congruence).

Defined.

Best,

Mukesh

[1] https://gist.github.com/mukeshtiwari/99538fd3ce0715155797528bdeb3d3a9#file-sig-v-L1-L17