Stream: Coq users

Topic: Convincing Coq accept my definition


view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 14:04):

Hi everyone, how can I convince Coq to accept my definition of nat_div. (I understand that I am relying on accessibility predicate for termination but my decreasing argument is u)

From Coq Require Import Arith Utf8 Psatz
  Peano.

Section Wf_div.

  Definition R := fun x y => x < y.

  Lemma R_acc : forall (a : nat), Acc R a.
  Proof.
    induction a as [|a IHa].
    +
      constructor.
      intros ? Ha.
      refine (match Ha with end).
    +
      constructor.
      intros y Ha.
      constructor.
      intros z Hc.
      pose proof (Acc_inv IHa) as Ih.
      eapply Ih.
      unfold R in Ha, Hc |- *.
      abstract nia.
  Qed.


  Lemma R_sub_acc : forall (a b : nat),
     Acc R (a - b).
  Proof.
    intros ? ?.
    eapply R_acc.
  Qed.



  Theorem nat_div : nat -> forall (b : nat),
    0 < b -> nat * nat.
  Proof.
    intros a b Ha.
    refine((
      fix nat_div u (acc : Acc R u) :=
      match (lt_eq_lt_dec a b) with
        | inleft Hb =>
          match Hb with
          | left Hc => (0, a)
          | right Hc => (1, 0)
          end
        | inright Hb =>
          match nat_div (a - b) _ with
          | (q, r) => (S q, r)
          end
        end) a (R_acc a)).
    eapply R_sub_acc;
    assumption.
    Guarded.

view this post on Zulip Gaëtan Gilbert (Feb 04 2023 at 14:23):

my decreasing argument is u

but the recursive call is unrelated to u

view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 14:46):

@Gaëtan Gilbert Yeah, you are right. Maybe I see your point but I don't how to resolve it. I guess something like this?

Theorem nat_div :  forall (b : nat),
    0 < b -> nat -> nat * nat.
  Proof.
    intros b Hb.
    refine(
      fix nat_div a (* (acc : Acc R a) {struct acc} *) := _).

But the challenge is this does not give me a nice induction principle. When I uncomment (acc : Acc R a), the type checker is not happy.

view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 14:51):

(deleted)

view this post on Zulip Pierre Castéran (Feb 04 2023 at 14:57):

What about :

Section Divisor.
Variable b : nat.
Hypothesis Hb : 0 < b.

Definition div : nat->  nat * nat.
  refine (well_founded_induction lt_wf (fun n => (nat * nat)%type) _ ).
  - intros x Recx; destruct (lt_eq_lt_dec x b).
    + destruct s.
      * exact (0, b).
      * exact (1, 0).
    + destruct (Recx (x-b)) as [q r].
     *  abstract lia.
     *  exact (S q, r)
Defined.

End Divisor.

Indeed, the structural argument about accessibility can be observed in Acc_rect, used in well_founded_induction_type.

view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 15:03):

Thanks @Pierre Castéran ! I already have a solution using well_founded_induction but I am trying to simulated the Equations solution posted on Coq mailing, but I am not able to see how to convince Coq about termination.

view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 15:18):

I managed to get one but it's certainly not as clean as the Equations solution.

  Theorem nat_div :  nat -> forall (b : nat),
    0 < b -> nat * nat.
  Proof.
    intro a.
    cut (Acc R a); revert a.
    +
      refine(fix nat_div a (acc : Acc R a) {struct acc} :=
        match acc with
        | Acc_intro _ f => fun b Ha =>
          match (lt_eq_lt_dec a b) with
          | inleft Hb =>
            match Hb with
            | left Hc => (0, a)
            | right Hc => (1, 0)
            end
          | inright Hb =>
            match nat_div (a - b) _ b Ha with
            | (q, r) => (S q, r)
            end
          end
        end).
      assert (Hc : R (a - b) a).
      unfold R. abstract nia.
      exact (f (a - b) Hc).
    +
      intros a.
      eapply R_acc.
  Defined.

view this post on Zulip Pierre Castéran (Feb 04 2023 at 15:25):

Yes. What is the main difference between using Equationsand well_founded_induction?
I already used Equationsto define a complex well_founded recursive function.
The resulting function was also an application of

FixWf :
  forall (A : Type) (R : relation A),
       WellFounded R ->
       forall P : A -> Type, (forall x : A, (forall y : A, R y x -> P y) -> P x) -> forall x : A, P x

Your solution looks OK, the main difference is that your fix ... match acc ... part is in your definition instead of the standard library :grinning:

view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 15:34):

Equations really feels like magic, a really pleasant system to work for dependent types. I don't know how it internally work so I have no idea about the difference between Equations and well_founded_induction.

view this post on Zulip Pierre Courtieu (Feb 04 2023 at 15:40):

I guess the two versions don't behave the same when it comes to reduction and/or extraction? Nothing fundamental but significant though.

view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 15:51):

Surprisingly, the extraction gives a OCaml code that is very similar to the one that Coq type checker rejects :)

let rec nat_div a b =
  match lt_eq_lt_dec a b with
  | Inleft hb ->
    (match hb with
     | Left -> Pair (O, a)
     | Right -> Pair ((S O), O))
  | Inright -> let Pair (q, r) = nat_div (sub a b) b in Pair ((S q), r)

view this post on Zulip Pierre Courtieu (Feb 04 2023 at 15:53):

Compare it to the one you get with well_founded_induction, and the one with Equations.

view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 16:11):

Equations extraction is very different, at least by just looking at the syntax, from the well_founded_one. Vanilla Coq extraction very idiomatic, at least for my taste.

Equations extraction.

Require Import Arith.
From Equations Require Import Equations.
Set Equations Transparent.



Definition pf {A} (a : A) : {b | a = b} :=
  exist _ a eq_refl.

Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).


Equations division (a b : nat) (p : 0 < b) : nat * nat by wf a lt :=
  division a b p with pf (a <? b) =>
      | true eqn: _ =>  (0, a)
      | false eqn: Ha =>
        match division (a - b) b p with
        | (q, r) => (S q, r)
        end.
  Next Obligation.
    eapply Nat.sub_lt.
    eapply Nat.ltb_ge in Ha;
    exact Ha.
    exact p.
  Defined.

Extraction division.

let division a a0 =
  let rec fix_F x =
    let a1 = let pr1,_ = x in pr1 in
    let b = let pr1,_ = let _,pr2 = x in pr2 in pr1 in
    (match pf (Nat.ltb a1 b) with
     | True -> Pair (O, a1)
     | False ->
       let Pair (q, r) = let y = (sub a1 b),(b,__) in fix_F y in
       Pair ((S q), r))
  in fix_F (a,(a0,__))

Well _founded_induction extraction

Section Wf_div.



  Lemma R_wf :
    well_founded lt.
  Proof.
    intro a.
    apply lt_wf.
  Qed.



  Theorem nat_div_wf : forall (a b : nat),
    0 < b -> nat * nat.
  Proof.
    intro a.
    induction (R_wf a) as [a Ha IHa];
    intros b Hb.
    destruct (lt_eq_lt_dec a b) as [[Hc | Hc] | Hc].
    +
      exact (0, a).
    +
      exact (1, 0).
    +
      assert (Hrel : (a - b) < a) by nia.
      destruct (IHa (a - b) Hrel b Hb) as (q, r).
      exact (S q, r).
  Defined.

End Wf_div.

Extraction nat_div_wf.

let rec nat_div_wf x b =
  let s = lt_eq_lt_dec x b in
  (match s with
   | Inleft a -> (match a with
                  | Left -> Pair (O, x)
                  | Right -> Pair ((S O), O))
   | Inright ->
     let p = let y = sub x b in nat_div_wf y b in
     let Pair (a, b0) = p in Pair ((S a), b0))

view this post on Zulip Notification Bot (Feb 04 2023 at 16:15):

Mukesh Tiwari has marked this topic as resolved.

view this post on Zulip Paolo Giarrusso (Feb 04 2023 at 16:24):

FWIW, all uses of lia/nia in Defined blocks should usually be wrapped by abstract; and if you're interested in extraction you probably want N not nat...

view this post on Zulip Mukesh Tiwari (Feb 04 2023 at 16:46):

@Paolo Giarrusso Do you know where can I find this theorem, Theorem N_lt_eq_lt_dec : forall (x y : N), {x < y} + {x = y} + {y < x}. in Coq library?

view this post on Zulip Paolo Giarrusso (Feb 04 2023 at 16:54):

@Mukesh Tiwari https://gitlab.mpi-sws.org/iris/stdpp/-/blob/e04271e24ab89bc735321375fb85ed7e1f9f80e7/stdpp/lexico.v#L99-107

view this post on Zulip Notification Bot (Feb 05 2023 at 09:50):

Dominique Larchey-Wendling has marked this topic as unresolved.

view this post on Zulip Dominique Larchey-Wendling (Feb 05 2023 at 09:50):

Hi @Mukesh Tiwari

Nowadays I usually use the following induction on _ _ as _ with measure _ tactic notation to do all the Acc fixpoint encoding for me in a uniform way. Best regards,

Require Import Arith Extraction Wellfounded Lia Utf8.

Section measure2_rect.

  Variable (X Y : Type) (m : X  Y  nat) (P : X  Y  Type)
           (HP : x y, (∀ x' y', m x' y' < m x y  P x' y')  P x y).

  Let m' '(x,y) := m x y.
  Let Rwf : well_founded  p q, m' p < m' q).
  Proof. apply wf_inverse_image, lt_wf. Qed.

  Definition measure2_rect x y : P x y.
  Proof.
    generalize (Rwf (x,y)); revert x y.
    refine (fix loop x y a {struct a} :=
      HP x y  x' y' _, loop x' y' _)).
    now apply Acc_inv with (1 := a).
  Qed.

End measure2_rect.

Extraction Inline measure2_rect.

Tactic Notation "induction" "on" hyp(x) hyp(y) "as" ident(IH) "with" "measure" uconstr(f) :=
  pattern x, y; revert x y; apply measure2_rect with (m := λ x y, f); intros x y IH.

Definition nat_div_specif n b '(q,r) := (n = q*b+r) /\ r < b.

Definition nat_div_pwc (n b : nat) : 0 < b  { c | nat_div_specif n b c }.
Proof.
  induction on n b as loop with measure (n-b); intros Hb.
  refine (match (lt_eq_lt_dec n b) with
    | inleft Hnb =>
      match Hnb with
      | left Hnb  => exist _ (0,n) _
      | right Hnb => exist _ (1,0) _
      end
    | inright Hnb =>
      let (c,Hc) := loop (n-b) b _ _ in
      match c as c' return nat_div_specif _ _ c' -> _ with
      | (q,r) => fun Hc =>  exist _ (S q,r) _
      end Hc
    end); red; try destruct Hc; try lia.
Defined.

Definition nat_div n b Hb := proj1_sig (nat_div_pwc n b Hb).

Fact nat_div_spec n b Hb :
  let (q,r) := nat_div n b Hb
  in  n = q * b + r /\ r < b.
Proof.
  unfold nat_div.
  destruct (nat_div_pwc n b Hb) as ([] & []); simpl; lia.
Qed.

Extraction Inline nat_div_pwc.
Recursive Extraction nat_div.

view this post on Zulip Dominique Larchey-Wendling (Feb 05 2023 at 09:52):

As a side question: don't you have difficulties to compute with your nat_div in Coq. Sometimes, the Qed from the lemmas of the Arith lib block the evaluation of such functions.

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 10:07):

Don't you need Rwf and measure2_rect to be Defined to compute with nat_div, @Dominique Larchey-Wendling ?

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 10:20):

Alternatively, the well-foundedness proofs can sometimes be kept opaque, if you use Acc_intro_generator; I've learned about this from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/well_founded.v#L11

view this post on Zulip Dominique Larchey-Wendling (Feb 05 2023 at 10:30):

I have not tested this particular one but I now prefer to write fully specified functions and get the fixpoint equations out of the spec, if ever needed. However, when properly specified, the equations may not be needed at all. But I did experiment such problems with evaluating well-founded fixpoints in the past.

Moreover I remember being told about this remark of generating Acc based fuel (by @Matthieu Sozeau on coq-club if my memory is correct), to be able to evaluate such Acc based fixpoints but thanks for the link that formalizes that cleanly.

view this post on Zulip Paolo Giarrusso (Feb 05 2023 at 10:36):

Ah, you've just reminded me: none of above versions come with unfolding lemmas — except the one from Equations, and I guess your point is to make unfolding unnecessary via the spec

view this post on Zulip Mukesh Tiwari (Feb 05 2023 at 11:01):

Dominique Larchey-Wendling said:

As a side question: don't you have difficulties to compute with your nat_div in Coq. Sometimes, the Qed from the lemmas of the Arith lib block the evaluation of such functions.

Yeah, I had but when I changed R_acc (see the very top post) closed with Qed to Defined, it worked. Also, I found out that lt_wf has been closed with Defined so I used it (https://github.com/coq/coq/blob/master/theories/Arith/Wf_nat.v). But I see your point because in the past, I have had hard time evaluating the functions defined using well_founded_ind. I think something has changed in evaluation mechanism of Coq but I can only speculate.

Section Wf_div.


  Theorem nat_div :  nat -> forall (b : nat),
    0 < b -> nat * nat.
  Proof.
    intro a.
    cut (Acc lt a);
    [revert a |].
    +
      refine(fix nat_div a (acc : Acc lt a) {struct acc} :
        forall b : nat, 0 < b -> nat * nat :=
        match acc with
        | Acc_intro _ f => fun b Ha =>
          match (lt_eq_lt_dec a b) with
          | inleft Hb =>
            match Hb with
            | left Hc => (0, a)
            | right Hc => (1, 0)
            end
          | inright Hb =>
            match nat_div (a - b) _ b Ha with
            | (q, r) => (S q, r)
            end
          end
        end).
      assert (Hc : (a - b) < a).
      abstract nia.
      exact (f (a - b) Hc).
    +
      eapply lt_wf.
  Defined.

End Wf_div.

Lemma pf : 0 < 2.
Proof.
  auto.
Defined.

Eval compute in nat_div 400 2 pf.

= (200, 0)
     : nat * nat

view this post on Zulip Karl Palmskog (Feb 05 2023 at 11:06):

Paolo Giarrusso said:

Alternatively, the well-foundedness proofs can sometimes be kept opaque, if you use Acc_intro_generator; I've learned about this from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/well_founded.v#L11

This is something we should highlight to the community better. Maybe one good way is as a Proof Assistant Stack Exchange question? Apparently the original source is https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00013.html

view this post on Zulip Mukesh Tiwari (Feb 05 2023 at 12:12):

@Karl Palmskog It would also be a good idea to maintain a tutorial/wiki, possibly within the Coq GitHub repo, for this kind of Coq tricks.

view this post on Zulip Karl Palmskog (Feb 05 2023 at 12:13):

I suggest making PR to something like: https://github.com/tchajed/coq-tricks

view this post on Zulip Karl Palmskog (Feb 05 2023 at 12:13):

I list some of the tutorial/tricks resources at https://github.com/coq-community/awesome-coq#tutorials-and-hints

view this post on Zulip Karl Palmskog (Feb 05 2023 at 12:14):

the main reason for getting something into Proof Assistant SE is that search engines adore them

view this post on Zulip Mukesh Tiwari (Feb 06 2023 at 10:35):

Interestingly, I already have two examples [1, 2] of computing with Opaque Acc proofs. I just need to write some explanation about it and push them to https://github.com/tchajed/coq-tricks.

[1] https://github.com/mukeshtiwari/Coq-automation/blob/master/Opaque.v#L62
[2] https://github.com/mukeshtiwari/Coq-automation/blob/master/Gcd_guarded.v#L64

view this post on Zulip Mukesh Tiwari (Feb 06 2023 at 11:29):

Just an observation: it seems that using this method (unfolding Acc once and use f to construct less than lt proof), we can compute with well founded functions without any guard (Edit: Acc_intro_generator). I tried to write my byte list following the same pattern and it works.

From Coq Require Import Arith Utf8 Psatz
  Peano NArith Strings.Byte NArith.

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

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

Definition length_byte_list_without_guard : N -> list byte.
  Proof.
    intro np.
    cut (Acc lt (N.to_nat np));
    [revert np |].
    +
      refine(fix length_byte_list_without_guard np (acc : Acc lt (N.to_nat np))
        {struct acc} :=
      match acc with
      | Acc_intro _ f =>
        match (np <? 256) as npp
          return _ = npp -> _
        with
        | true => fun Ha => List.cons (np_total np Ha) List.nil
        | false => fun Ha =>
            let r := N.modulo np 256 in
            let t := N.div np 256 in
            List.cons (np_total r _) (length_byte_list_without_guard t _)
        end eq_refl
      end).
      ++
        apply N.ltb_lt, (nmod_256 np).
      ++
        apply N.ltb_ge in Ha.
        assert (Hc : (N.to_nat t < N.to_nat np)%nat).
        unfold t. rewrite N2Nat.inj_div.
        eapply Nat.div_lt; try abstract nia.
        exact (f (N.to_nat t) Hc).
    +
      apply lt_wf.
  Defined.


Eval compute in length_byte_list_without_guard 3723.
= ("139"%byte :: "014"%byte :: nil)%list
     : list byte

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 12:22):

As long as the Acc argument reduces enough times the computation will go through; using guard + opaque well-foundedness is a bit hacky, but it can perform better if the well-foundedness proof is slow

view this post on Zulip Matthieu Sozeau (Feb 06 2023 at 14:34):

It's a bit incorrect to say "without guarded recursion", the definition is still guarded on the Acc proof. As lt_wf is transparent though, you can compute with it fine.

view this post on Zulip Paolo Giarrusso (Feb 06 2023 at 15:00):

I think "without guard" stood for "without Gonthier's hack for opaque well-foundedness proofs", since the actual listings kind-of rename stdlib's Acc_intro_generator to guard; I agree the description is confusing and stdlib's name is better.


Last updated: Jun 24 2024 at 14:01 UTC