Stream: Coq users

Topic: Coq function not reducing (Zwf_well_founded may be culprit)


view this post on Zulip Mukesh Tiwari (Sep 14 2021 at 02:55):

I have encoded the binary extended Euclidean algorithm, taken from the book Handbook of Applied Cryptography (https://cacr.uwaterloo.ca/hac/about/chap14.pdf#page=17). However, when I am trying to compute Eval compute in binary_gcd 2 3 2 3 1 1 0 0 1., all I am getting is a complicated Coq terms . Based on my understanding, I believe, it is because of Zwf_well_founded so my question is: how can I make/force the implementation to spit (reduced) values than (complicated) proof terms? (I assume one would be to not use Zwf_well_founded but what are other changes I need to incorporate).

  Require Import Coq.NArith.BinNat.
  Require Import Coq.Program.Wf.
  Require Import Coq.ZArith.Zwf.
  Local Open Scope positive_scope.

  Lemma poslt_wf : well_founded Pos.lt.
  Proof.
    unfold well_founded.
    assert (forall x a, x = Zpos a -> Acc Pos.lt a).
    intros x. induction (Zwf_well_founded 1 x);
    intros a Hxa. subst x.
    constructor; intros y Hy.
    apply H0 with y; trivial.
    split; auto with zarith.
    intros. apply H with a.
    exact eq_refl.
  Defined.

  Definition poseven (a : positive) : bool :=
    match a with
    | xO _ => true
    | _ => false
    end.

  Lemma poseven_div : forall p, true = poseven p -> Pos.div2 p < p.
  Proof.
    induction p; simpl; intro H; try (inversion H).
    nia.
  Qed.


  Program Fixpoint binary_gcd (x y : positive) (u v g : positive) (a b c d : Z)
    {measure (Pos.add u v) (Pos.lt)} : Z * Z * positive :=
      match poseven u, poseven v with
      | true, true => binary_gcd x y (Pos.div2 u) (Pos.div2 v) (Pos.mul 2 g) a b c d
      | true, false =>
        match Z.even a, Z.even b with
        | true, true =>  binary_gcd x y (Pos.div2 u) v g (Z.div a 2) (Z.div b 2) c d
        | _, _ =>  binary_gcd x y (Pos.div2 u) v g (Z.div (a + y) 2) (Z.div (b - x) 2) c d
        end
      | false, true =>
        match Z.even c, Z.even d with
        | true, true => binary_gcd x y u (Pos.div2 v) g a b (Z.div c 2) (Z.div d 2)
        | _, _ => binary_gcd x y u (Pos.div2 v) g a b (Z.div (c + y) 2) (Z.div (d - x) 2)
        end
      | false, false =>
          match u ?= v with
          | Lt => binary_gcd x y u (Pos.sub v u) g a b (Z.sub c a) (Z.sub d b)
          | Eq => (a, b, Pos.mul g v)
          | Gt => binary_gcd x y (Pos.sub u v) v g (Z.sub a c) (Z.sub b d) c d
          end
      end.
    Next Obligation.
      apply Pos.add_lt_mono.
      apply poseven_div; exact Heq_anonymous.
      apply poseven_div; exact Heq_anonymous0.
    Defined.
    Next Obligation.
      apply Pos.add_lt_mono_r.
      apply poseven_div; exact Heq_anonymous1.
    Defined.
    Next Obligation.
      apply Pos.add_lt_mono_r.
      apply poseven_div; exact Heq_anonymous1.
    Defined.
    Next Obligation.
      apply Pos.add_lt_mono_l.
      apply poseven_div; exact Heq_anonymous2.
    Defined.
    Next Obligation.
      apply Pos.add_lt_mono_l.
      apply poseven_div; exact Heq_anonymous2.
    Defined.
    Next Obligation.
      symmetry in Heq_anonymous.
      pose proof (proj1 (Pos.compare_lt_iff u v) Heq_anonymous).
      rewrite Pos.add_sub_assoc, Pos.add_comm, Pos.add_sub.
      apply Pos.lt_add_r. exact H.
    Defined.
    Next Obligation.
      symmetry in Heq_anonymous.
      pose proof (proj1 (Pos.compare_gt_iff u v) Heq_anonymous).
      nia.
    Defined.
    Next Obligation.
      apply measure_wf.
      apply poslt_wf.
    Defined.

 (* This one does not reduce  to any value *)
  Eval compute in binary_gcd 2 3 2 3 1 1 0 0 1.

view this post on Zulip Guillaume Melquiond (Sep 14 2021 at 06:26):

If you do not care to evaluate terms in Coq, you can just extract your function to OCaml or Haskell. Indeed, terms such as Zwf_well_vounded will be erased during extraction.

view this post on Zulip Guillaume Melquiond (Sep 14 2021 at 06:29):

But if you want to evaluate in Coq, I suggest to do an induction on the positive structure of your largest input. This means that your algorithm could give up before having computed the actual gcd. But then you can prove that this never happens. Since this proof is completely independent of your computation, the later will not block.


Last updated: Jan 29 2023 at 01:02 UTC