The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

The error message is actually pretty decent in this case:

    The term "np_total_subproof0" of type
     "∀ np : N,
        (np <? 256) = true → ∀ mp : N, np = mp → (mp <? 256) = false → byte"
    cannot be applied to the terms
     "np" : "N"
     "H1" : "b0 = true"
     "mp" : "N"
     "Hmp" : "np = mp"
     "Hmf" : "(mp <? 256) = false"
    The 2nd term has type "b0 = true" which should be coercible to
     "(np <? 256) = true".

What this means is that your np_total_subproof0 wants an np of type N and a 
proof that n <? 256 is true.  When you try to rewrite (same problem if you 
try to destruct (n <? 256), btw), you abstract over the value of (n <? 256), 
turning it into an arbitrary boolean b0; as a result, the argument that gets 
passed to np_total_subproof0 has the wrong type.

You can see the same issue with `set` and `clearbody`: as long as you can't 
do `set (np <? 256) as b0; clearbody b0`, the rewrite won't work. Same with 
`pattern (np <? 256)`.

The usual trick for these issues is to generalize things to have 
less-dependent types.  Here's the completed proof, concretely:

    Require Import NArith Byte Utf8 Lia.
    Open Scope N_scope.

    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.
      (* Following the error messages: *)
      generalize (np_total_subproof0 np H) as sp0.
      generalize (@eq_refl bool (np <? 256)).
      (* But don't generalize too much *)
      set (np <? 256) as b in *; unfold b at 1.
      Fail Fail clearbody b. (* Phew *)
      rewrite H; subst b. (* Phew *)

      (* Now the actual proof: *)
      intros.
      Fail rewrite H0. (* Same problem *)
      generalize (np_total_subproof np np eq_refl e) as sp.
      rewrite H0.
      intros.
      reflexivity.
    Qed.

Clément.



On 10/15/21 8:37 PM, mukesh tiwari wrote:
> 
> 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
>  
> <https://gist.github.com/mukeshtiwari/99538fd3ce0715155797528bdeb3d3a9#file-sig-v-L1-L17>