The Coq mailing list

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

As a side note: in this particular case, picking a simpler definition of 
np_total helps a lot:

    From Coq Require Import NArith Strings.Byte Utf8 Lia.
    Open Scope N_scope.

    Definition np_total (np : N):  (np <? 256 = true) ->  byte.
    Proof.
      intros H.
      pose proof of_N_None_iff np.
      destruct (of_N np) as [b | ].
      - exact b.
      - exfalso;
          abstract (apply N.ltb_lt in H;
                    intuition lia).
    Defined.

    Lemma np_true : forall np (H : np <? 256 = true) x,
      of_N np = Some x -> np_total np H = x.
    Proof.
      unfold np_total; intros * Heq.
      generalize (of_N_None_iff np).
      rewrite Heq; intros.
      reflexivity.
    Qed.

On 10/15/21 11:03 PM, mukesh tiwari wrote:
> Thanks Clémen! Very helpful. Finally, I get the idea.
> 
> Best,
> Mukesh
> 
> On Sat, Oct 16, 2021 at 1:00 PM Clément Pit-Claudel <cpitclaudel AT gmail.com 
> <mailto:cpitclaudel AT gmail.com>> wrote:
> 
>     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>
>  
> <https://gist.github.com/mukeshtiwari/99538fd3ce0715155797528bdeb3d3a9#file-sig-v-L1-L17
>  
> <https://gist.github.com/mukeshtiwari/99538fd3ce0715155797528bdeb3d3a9#file-sig-v-L1-L17>>
>