Stream: Coq users

Topic: Inverse of an integer modulo prime.

Mukesh Tiwari (Dec 18 2020 at 04:45):

Do we have inverse function in standard library [1] (I can not find any in Znumbertheory)? I tried to write one using the euclid implementation given in the library, but it is opaque; hence no normalisation.

  Print Euclid. (*
  Inductive Euclid (a b : Z) : Set :=
    Euclid_intro : forall u v d : Z, u * a + v * b = d -> Zis_gcd a b d -> Euclid a b *)

  Definition inverse (m t : Z) : Z :=
    match euclid m t with
    | Euclid_intro _ _ u v d Huv Hgcd => u
    end.

  Theorem tinv : inverse 2 3 = 2.
  Proof.
    unfold inverse.
    simpl euclid. (* Nothing happens *)

[1] https://coq.inria.fr/library/Coq.ZArith.Znumtheory.html

Michael Soegtrop (Dec 18 2020 at 10:13):

There is a Fixpoint pos_div_eucl (a:positive)(b:N) : N * N for positive binary integers.

Christian Doczkal (Dec 18 2020 at 11:22):

edivn : nat -> nat -> (nat * nat) from mathcomp.ssreflect.div also computes.

Last updated: Oct 08 2024 at 16:02 UTC