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: Oct 13 2024 at 01:02 UTC