Stream: Coq users

Topic: ✔ Rewrite fails (Incorrect elimination of "N.ltb_lt up 256")


view this post on Zulip Mukesh Tiwari (Oct 09 2021 at 03:32):

Edit: The lemma below is incorrect and therefore not provable :). This N.to_nat (N.div np 256 + 1) should be
N.to_nat (log256 np + 1), but it contains some useful information; hence I am not deleting this thread.

I am trying to rewrite an assumption into the goal, but getting this error:

Reason is: Incorrect elimination of "N.ltb_lt up 256" in the inductive type
        "and": ill-formed elimination predicate.


  Theorem length_correctness : forall np : N, List.length (length_byte_list np) = N.to_nat (N.div np 256 + 1).
  Proof.
    intro np.
    induction (N.lt_wf 0 np) as [up Hacc IHup].
    refine(match (up <? 256) as upp return _ = upp -> _ with
    | true => fun Hnp => _
    | false =>  fun Hnp => _
    end eq_refl).
    + apply N.ltb_lt in Hnp.
      assert (Hup : up/256 = 0).
      rewrite N.div_small;
      [reflexivity | exact Hnp].
      rewrite Hup.
      unfold length_byte_list.
      simpl. apply N.ltb_lt in Hnp.
      (* rewrite Hnp is not working
         which is ill-typed.
        Reason is: Incorrect elimination of "N.ltb_lt up 256" in the inductive type
        "and": ill-formed elimination predicate. *)
      admit.

Based on my (limited) understanding, it might be the case that this rewrite is creating some inconsistent state and therefore now allowing the rewrite, so my question is: how can I solve this? Complete source code [1]

[1] https://gist.github.com/mukeshtiwari/eb3376d4eb568628205d5b3469b85785

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 04:30):

(0) Instead of a dependently typed "refine (match...)", what about destruct (up <? 256) eqn:?

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 04:36):

(1) Can you poat the complete goal at the point of the error?

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 04:39):

(2) I haven't seen this specific type error, but if rewrite is producing an ill-typed state because of dependent types, often one needs to actually understand the details of the type error, and change the state to fix it.

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 04:41):

That might sound tautological, but this is one of the few scenario where one needs to typecheck a tactic output on their own to fix it!

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 04:42):

(in fact, when using lots of dependent types, some prefer writing proof terms directly, so that it's easier to reason about them; see Agda)

view this post on Zulip Mukesh Tiwari (Oct 09 2021 at 08:37):

(0) I changed it to destruct (up <? 256) eqn:? but the error is same.
(1) I posted the error message on gist [1].

[1] https://gist.github.com/mukeshtiwari/82d56ffdce8e9707cb2c9baf610608b6

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 08:56):

This goal is too unwieldy for this to be solvable in general (but ways out exist); my advice about using abstract to hide obligations was exactly to avoid having proof obligations inside your Defined terms.

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 09:01):

however, I suspect I spotted the _first_ problem, tho I’m not sure if the usual workarounds would scale here

view this post on Zulip Mukesh Tiwari (Oct 09 2021 at 09:07):

Now wrapping some terms into abstract changed the error:

which is ill-typed.
Reason is: Illegal application:
The term "length_byte_list_subproof" of type
 "∀ up : N, (up <? 256) = true → up < 256"
cannot be applied to the terms
 "up" : "N"
 "Hnp0" : "b = true"
The 2nd term has type "b = true" which should be coercible to
 "(up <? 256) = true".

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 09:07):

Here’s an extract of the first error:

Abstracting over the term "up <? 256" leads to a term
λ b : bool,
  length
    ((if b as upp return (b = upp  list byte)
      then
       λ Hnp0 : b = true,
         (np_total up (match N.ltb_lt up 256 with
                       | conj H _ => H
                       end Hnp0) :: Datatypes.nil)%list

which is ill-typed.

here, we cannot apply N.ltb_lt up 256 (or its first half) to Hnp0 : b = true — even if we could apply it to Hnp0 : up <? 256 = true.

So, rewriting up <? 256 in all occurrences is not possible directly.

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 09:09):

your error is also of a similar kind

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 09:12):

one basic idea is to (1) avoid rewriting in those positions where that causes a type error (2) trying to make that easier to scale.

Here, probably you can generalize over the proof term ((match N.ltb_lt up 256 with | conj H _ => H end Hnp0), or length_byte_list_subproof up Hnp0) — it often doesn’t matter which exact proof you have that up < 256.

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 09:12):

alternatively, you can list the occurrences where to rewrite.

view this post on Zulip Paolo Giarrusso (Oct 09 2021 at 09:13):

Neither one scales so well with goal size, but abstract might help already a bit.

view this post on Zulip Mukesh Tiwari (Oct 09 2021 at 09:17):

Thansk @Paolo Giarrusso I don't know how to abstract the third bullet. I might look more into tomorrow (going for dinner). Enjoy your day!

Definition length_byte_list (np : N) : list byte.
  Proof.


    refine ((fix length_byte_list up (H: Acc (fun x y =>  (* 0 <= *) x < y) (N.div up 256)) {struct H} :=
      match (up <? 256) as upp return _ = upp -> _ with
      | true => fun Hnp => List.cons (np_total up _) List.nil
      | false => fun Hnp =>
        let r := N.modulo up 256 in
        let t := N.div up 256 in
        List.cons (np_total r _) (length_byte_list t _)
      end eq_refl
    ) np (N_Lt_wf _)).  (* ((@Acc_intro_generator _ (fun x y => 0 <= x < y) 100 (N.lt_wf 0)) (N.div np 256))). *)
    + abstract (apply N.ltb_lt in Hnp; exact Hnp).
    + abstract (apply (nmod_256 up)).
    + apply Acc_inv with (x := t). subst t; exact H.
      apply N.ltb_ge in Hnp;
      eapply N_eq_gt with (up := up); auto.
      Show Proof.
  Defined.

view this post on Zulip Mukesh Tiwari (Oct 09 2021 at 23:04):

(deleted)

view this post on Zulip Notification Bot (Oct 10 2021 at 06:48):

Mukesh Tiwari has marked this topic as resolved.


Last updated: Feb 06 2023 at 12:04 UTC