Stream: Coq users

Topic: ✔ Recursive call failing on Acc


view this post on Zulip Mukesh Tiwari (Oct 08 2021 at 05:04):

Coq complains that my principal argument is "up / 256" instead of a subterm of "up", but that's the whole point of well founded induction, and I wonder what is wrong with my code below?

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)) :=
      match (N_le_gt_dec up 256) as upp return upp = _ -> _ with
      | left Hle => fun Hnp => _
      | right Hre => fun Hnp => _
      end eq_refl
    ) np (N.lt_wf 0 _ )).
    (* base case *)
    exact (List.cons (np_total up Hle) List.nil).

    (* Induction case: r := Nmod up 256 and t = N.div up 256 *)
    remember (N.modulo up 256) as r.
    remember (N.div up 256) as t.

    assert (Hacc: Acc  x y : N, 0 <= x < y) (t / 256)).
    eapply Acc_inv with (x := t). exact H.
    eapply N_eq_gt with (up := up); auto.
    (* total function *)
    pose proof (nmod_256 up) as Hup.
    assert (Hr : r < 256).
    rewrite <-Heqr in Hup.
    exact Hup.
    exact  (List.cons (np_total r Hr) (length_byte_list t Hacc)).
    Guarded.

Complete source code:

  Definition np_total (np : N) (H : np < 256) : byte.
  Proof.
    refine (match (np <? 256) as npp return _ = npp -> _ with
    | true => fun H => match (of_N np) as npw return _ = npw -> _  with
      | Some x => fun He => x
      | None => fun He => _  (* impossible *)
      end eq_refl
    | false => fun H => _
    end eq_refl).
    apply of_N_None_iff in He.
    abstract nia. (* abstract or transparent? *)
    apply N.ltb_ge in H.
    abstract nia.
  Defined.

  Lemma nmod_256 : forall np, np mod 256 < 256.
  Proof.
    intros ?. apply N.mod_lt. intro. inversion H.
  Qed.

  Lemma N_le_gt_dec : forall u v : N, {u < v} + {v <= u}.
  Proof.
  Admitted.

  Lemma N_eq_gt : forall up t : N, 256 <= up -> t = up / 256 -> 0 <= t / 256 < t.
  Proof.
    intros up t Hup Ht.
    split.
    apply N.le_0_l.
    apply N.div_lt_upper_bound.
    nia.
    (* I know that 1 <= t *)
    assert (Hot: 1 <= t).
    rewrite Ht.
    apply N.div_le_lower_bound. nia.
    simpl. exact Hup. nia.
  Qed.

  (* Let's go with List :) *)
  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)) :=
      match (N_le_gt_dec up 256) as upp return upp = _ -> _ with
      | left Hle => fun Hnp => _
      | right Hre => fun Hnp => _
      end eq_refl
    ) np (N.lt_wf 0 _ )).
    (* base case *)
    exact (List.cons (np_total up Hle) List.nil).

    (* Induction case: r := Nmod up 256 and t = N.div up 256 *)
    remember (N.modulo up 256) as r.
    remember (N.div up 256) as t.

    assert (Hacc: Acc  x y : N, 0 <= x < y) (t / 256)).
    eapply Acc_inv with (x := t). exact H.
    eapply N_eq_gt with (up := up); auto.
    (* total function *)
    pose proof (nmod_256 up) as Hup.
    assert (Hr : r < 256).
    rewrite <-Heqr in Hup.
    exact Hup.
    exact  (List.cons (np_total r Hr) (length_byte_list t Hacc)).
    Guarded.

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

First, you'll want an explicit struct annotation, to mark your fixpoint as structurally recursive on H, and then you should get the guardedness checker happy for that recursive argument.

view this post on Zulip Paolo Giarrusso (Oct 08 2021 at 06:03):

Well-founded recursion is essentially just a design pattern for using structural recursion: it does it on Acc. So I wonder about Acc_inv; but if it is transparent with the right definition, this should work.

view this post on Zulip Paolo Giarrusso (Oct 08 2021 at 06:04):

Oh yeah: https://github.com/coq/coq/blob/cf408497eef21ee76fb253d95dce20902bd5cb37/theories/Init/Wf.v

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

Style-wise, definitions are clearer in Gallina if they're transparent: you could move much more of your body into the refine, and Qed off the proofs using abstract (or Program and obligations, if Program does not mangle your code too much)

view this post on Zulip Mukesh Tiwari (Oct 08 2021 at 06:39):

Thanks @Paolo Giarrusso . Do you know a quick/clever way to turn r := up mod 256 into Hr : r = up mod 256? I generally do something like:

assert (r = up mod 256).
    subst r; reflexivity.

But I think there must be some better way to do this.

view this post on Zulip Mukesh Tiwari (Oct 08 2021 at 06:44):

Also, what is your feedback on this one?

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 (N_le_gt_dec up 256) as upp return upp = _ -> _ with
      | left Hle => fun Hnp => List.cons (np_total up Hle) List.nil
      | right Hre => 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 0 _ )).

    assert (Heqr: r = up mod 256).
    subst r. reflexivity.
    pose proof (nmod_256 up) as Hup.
    rewrite <-Heqr in Hup; exact Hup.


    assert (Hacc: Acc  x y : N, 0 <= x < y) (t / 256)).
    eapply Acc_inv with (x := t). exact H.
    eapply N_eq_gt with (up := up); auto.
    exact Hacc.
  Defined.

view this post on Zulip Paolo Giarrusso (Oct 08 2021 at 06:51):

proof bullets would help reading, but instead of introducing Heqr, could you just use unfold r; exact Hup? Or even exact Hup since that unfold is redundant (unfolds aren’t needed by eapply, they’re only needed to help rewrite)

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

Awesome!

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

@Paolo Giarrusso Do you know a way to turn Opaque definitions to Transparent? I am talking about N.lt_wf [1]. One way is to copy paste the definition and end it with Defined but I am wondering is there any other way?

About N.lt_wf.
N.lt_wf is not universe polymorphic
Arguments N.lt_wf _%N_scope
N.lt_wf is opaque
Expands to: Constant Coq.NArith.BinNat.N.lt_wf

[1] https://github.com/coq/coq/blob/61e0d9fd6ac124e45576878f6eda842eb09e4b4b/theories/Numbers/NatInt/NZOrder.v#L633

view this post on Zulip Gaëtan Gilbert (Oct 08 2021 at 08:58):

qed cannot be undone

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

Thanks @Gaëtan Gilbert . I manage to prove it (a transparent definition) but I am curious what would break if someone changes the Qed in [1] to Defined in Coq code base?

Section Wf_proof.

  Let f (a : N) := N.to_nat a.

  Definition zwf (x y : N) := (f x < f y)%nat.

  Lemma zwf_well_founded : well_founded zwf.
  Proof.
    exact (well_founded_ltof _ f).
  Defined.

 Lemma N_acc (x : N) : forall a, a < x -> Acc N.lt a.
  Proof.
    induction (zwf_well_founded x) as [z Hz IHz].
    intros ? Hxa.
    constructor; intros y Hy.
    eapply IHz with (y := a).
    unfold zwf. unfold f.
    nia. nia.
  Defined.

  Lemma N_lt_wf : well_founded N.lt.
  Proof.
    red; intros ?.
    constructor; intros y Hy.
    eapply N_acc with (x := a).
    exact Hy.
  Defined.


  Lemma N_Lt_wf : forall up, Acc (fun x y => x < y) up.
  Proof.
    intros up.
    pose proof (N_lt_wf up).
    exact H.
  Defined.

End Wf_proof.

[1] https://github.com/coq/coq/blob/61e0d9fd6ac124e45576878f6eda842eb09e4b4b/theories/Numbers/NatInt/NZOrder.v#L633

view this post on Zulip Gaëtan Gilbert (Oct 08 2021 at 09:54):

probably nothing would break
deciding what to make qed is pretty adhoc so there may not be any real reason for these lemmas to be opaque

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2021 at 09:57):

Note that making wf proofs Defined is (arguably) discouraged by quite a few people.

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2021 at 09:57):

They recommend instead Qed wf proofs + what is known (?) as Krebbers' trick

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

@Pierre-Marie Pédrot That trick [1] goes at least 12 years back :).

[1} https://coq-club.inria.narkive.com/gO2dnKc4/well-founded-recursion-stuck-on-opaque-proofs

view this post on Zulip Pierre-Marie Pédrot (Oct 08 2021 at 11:28):

Yeah, it's true that I distinctly remember Thomas Braibant discussing about this technique some time when I was still at the ENS Lyon, so somewhere between 2009 and 2010... But as the message says, it was already considered folklore so the proper attribution might be lost to the mist of the dawn of ages...

view this post on Zulip Guillaume Melquiond (Oct 08 2021 at 11:46):

This trick certainly predates Krebber. For instance, Gonthier was already explaining it in 2007: https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00013.html

view this post on Zulip Karl Palmskog (Oct 08 2021 at 14:20):

ah, could someone please document this trick/idiom on the Discourse? Otherwise, I fear we will have to keep digging up these old Coq-Club threads...

It's also a good fit for a self-answered question on StackOverflow.

view this post on Zulip Paolo Giarrusso (Oct 08 2021 at 22:32):

Paolo Giarrusso Do you know a way to turn Opaque definitions to Transparent? I am talking about N.lt_wf [1]. One way is to copy paste the definition and end it with Defined but I am wondering is there any other way?

Others have answered the main question; I'll add that Qed and Opaque are different things, for non-obvious soundness reasons (!)

view this post on Zulip Mukesh Tiwari (Oct 08 2021 at 23:00):

Paolo Giarrusso said:

Others have answered the main question; I'll add that Qed and Opaque are different things, for non-obvious soundness reasons (!)

Sounds interesting and premise for a new question @Paolo Giarrusso .

view this post on Zulip Notification Bot (Oct 09 2021 at 00:14):

Mukesh Tiwari has marked this topic as resolved.

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

Karl Palmskog said:

ah, could someone please document this trick/idiom on the Discourse? Otherwise, I fear we will have to keep digging up these old Coq-Club threads...

It's also a good fit for a self-answered question on StackOverflow.

Karl, I am happy to do that but in which section of Discourse should I post this trick?

view this post on Zulip Karl Palmskog (Oct 09 2021 at 09:44):

I think "Using Coq" fits well (https://coq.discourse.group/c/using-coq/5)


Last updated: Jan 31 2023 at 14:03 UTC