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.
```

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.

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: Jun 16 2024 at 03:41 UTC