error with (zmod p)

Stream: new members

[Lucas Allen]

Hello, I've been doing some stuff relating to computing things with polynomials. For this I defined a class poly and algorithms for adding, multiplying, dividing, gcd, etc. Now I want to do some stuff with zmop p (where p is prime), and I'm getting the error,

type mismatch at application
  poly_gcd f
term
  f
has type
  poly (zmod p)
but is expected to have type
  poly ?m_1"

when I try to do division or gcd. I think the problem might be that division and gcd want zmod p to be a field. All the operations which want zmod p to be a ring work. Unfortunately, I don't know how to get Lean to figure out that zmod p is a field. When I try,

import tactic
import data.zmod.basic
import Poly

open zmod
open tactic

#check zmod.field
instance xxx (p : ℕ) [fact (prime p)] : field (zmod p) := infer_instance
instance ttt : field (zmod 7) := infer_instance

I get the error "failed to synthesize type class instance for ⊢ field (zmod 7)". How can I get this to work?

[Johan Commelin]

https://github.com/leanprover-community/mathlib/blob/master/src/data/zmod/basic.lean#L787

[Johan Commelin]

I have no idea why this is failing for you....

[Mario Carneiro]

It says right there - you need an instance of fact (prime 7) to satisfy the instance

[Lucas Allen]

Ok, instance ttt [fact (prime 7)] : field (zmod 7) := infer_instance works, but why doesn't instance xxx (p : ℕ) [fact (prime p)] : field (zmod p) := infer_instance work?

[Markus Himmel]

prime is not the same as nat.prime

[Lucas Allen]

Also, I still get the error,

type mismatch at application
  poly_div_quot_rem p
term
  p
has type
  poly (zmod 7)
but is expected to have type
  poly ?m_1"

when attempting division or gcd.

[Lucas Allen]

(deleted)

[Lucas Allen]

Markus Himmel said:

prime is not the same as nat.prime

oh.

[Lucas Allen]

instance xxx (p : ℕ) [fact (nat.prime p)] : field (zmod p) := infer_instance works. But I still get the error.

[Markus Himmel]

Would you mind posting the code that generates the error?

[Lucas Allen]

So #eval poly_gcd p q gives the error, and poly_gcd is

def poly_gcd_aux {α : Type} [field α] [decidable_eq α] [inhabited α] :
  ℕ → poly α → poly α → poly α
| 0     P Q := P
| (n+1) P Q := if Q = 0 then P else poly_gcd_aux n Q (P %ₚ Q)

def poly_gcd {α : Type} [field α] [decidable_eq α] [inhabited α] (P Q : poly α) :
  poly α := poly_gcd_aux (deg P) P Q

I'm not sure where to stop posting code. Should I just post the whole file?

[Lucas Allen]

And

def p : poly (zmod 7) := ⟨[1,2,3]⟩
def q : poly (zmod 7) := ⟨[1,1]⟩

Also, poly_gcd isn't finished yet, the higher degree poly goes first, so don't judge me too harshly.

[Markus Himmel]

Does #eval poly_gcd p q give you the error about poly_div_quot_rem you posted earlier or a different error?

[Lucas Allen]

Yeah, same thing

type mismatch at application
  poly_gcd p
term
  p
has type
  poly (zmod 7)
but is expected to have type
  poly ?m_1

[Lucas Allen]

I thought it was something to do with defining poly_div_quot_rem and poly_gcd using [field \a] instead of [ring \a], since the operations with [ring \a] work and the operations with [field \a] don't.

[Lucas Allen]

I'll just post all the code...

[Lucas Allen]

Here's the Poly file

import tactic
import algebra.ring.basic

/--
Let's make polynomials lists!
so [1,2,3] represents the polynomial
1 + 2x + 3x²
-/
class poly (α : Type) [ring α] :=
(cofs : list α)

lemma poly_eq_iff {α : Type} [ring α] [decidable_eq α] (P Q : poly α) : P = Q ↔ P.cofs = Q.cofs :=
begin
  split,
  { intro,
    tactic.unfreeze_local_instances,
    cases P, cases Q,
    exact congr_arg _ a, },
  { intro,
    tactic.unfreeze_local_instances,
    cases P, cases Q,
    exact congr_arg poly.mk a, }
end

def poly_eq {α : Type} [ring α] [decidable_eq α] (P Q : poly α) : Prop := P.cofs = Q.cofs
def poly_eq_bool {α : Type} [ring α] [decidable_eq α] (P Q : poly α) : bool := P.cofs = Q.cofs

instance {α : Type} [ring α] [decidable_eq α] [inhabited α] : has_equiv (poly α) := ⟨poly_eq⟩

instance {α : Type} [ring α] [decidable_eq α] [inhabited α] : decidable_eq (poly α) :=
begin
  intros a b,
  rw poly_eq_iff,
  cases a, cases b,
  haveI j : decidable (a = b) := infer_instance,
  exact j,
end

/-- `X` is the polynomial variable (aka indeterminant). Lifted from polynomial.basic in mathlib-/
def X {α : Type} [ring α] [has_one α] [has_zero α] : poly α :=
begin
  apply poly.mk,
  exact [0,1],
end

def list_remove_leading_zeros {α : Type} [ring α] [has_zero α] [decidable_eq α] : list α → list α
| []     := [0]
| (h::t) := if h = 0 then list_remove_leading_zeros t else h::t

def remove_leading_zeros {α : Type} [ring α] [has_zero α] [decidable_eq α] (P : poly α) : poly α :=
begin
  apply poly.mk,
  exact (list_remove_leading_zeros P.cofs.reverse).reverse,
end

def deg {α : Type} [ring α] [decidable_eq α] (P : poly α) : ℕ :=
  (list_remove_leading_zeros P.cofs.reverse).length - 1

/--The zero polynomial-/
instance {α : Type} [ring α] [has_zero α] : has_zero (poly α) :=
begin
  apply has_zero.mk,
  apply poly.mk,
  exact [0],
end

/--The one polynomial-/
instance {α : Type} [ring α] [has_one α] : has_one (poly α) :=
begin
  apply has_one.mk,
  apply poly.mk,
  exact [1],
end

/-- Representation of polynomials -/
def list_to_string {α : Type} [ring α] [has_repr α] [decidable_eq α] : list α → string
| []     := ""
| [h]    := repr h
| (h::t) := if h = 0
            then list_to_string t
            else (repr h ++ "X^" ++ (repr t.length) ++ " + ") ++ (list_to_string t)

instance {α : Type} [ring α] [has_repr α] [decidable_eq α] : has_repr (poly α) :=
⟨λ p, list_to_string p.cofs.reverse⟩

/--returns the leading cof-/
def list_lead {α : Type} [ring α] [inhabited α] (a : list α) : α := a.reverse.head

def lead {α : Type} [ring α] [inhabited α] (P : poly α) : α := list_lead P.cofs

/--return the negative Poly-/
def list_poly_neg {α : Type} [ring α] : list α → list α
| []     := []
| (h::t) := (-h) :: list_poly_neg t

def poly_neg {α : Type} [ring α] (P : poly α) : poly α :=
begin
  apply poly.mk,
  exact list_poly_neg P.cofs,
end

instance {α : Type} [ring α] : has_neg (poly α) := ⟨poly_neg⟩

/--adds two Polys together-/
def list_poly_add {α : Type} [ring α] : list α → list α → list α
| []     Q      := Q
| P      []     := P
| (h::t) (u::v) := (h + u) :: (list_poly_add t v)

def poly_add {α : Type} [ring α] [decidable_eq α] (P Q : poly α) : poly α :=
begin
  apply remove_leading_zeros,
  apply poly.mk,
  exact (list_poly_add P.cofs Q.cofs),
end

instance {α : Type} [ring α] [decidable_eq α] : has_add (poly α) := ⟨poly_add⟩
instance {α : Type} [ring α] [decidable_eq α] : has_sub (poly α) :=
begin
  apply has_sub.mk,
  intros P Q,
  exact P + -Q,
end

/--Scalar multiplication-/
def list_poly_scalar_mul {α : Type} [ring α] (t : α) (P : list α) : list α :=
P.map (λ c, t * c)

def poly_scalar_mul {α : Type} [ring α] [decidable_eq α] (t : α) (P : poly α) : poly α :=
begin
  apply remove_leading_zeros,
  apply poly.mk,
  exact (list_poly_scalar_mul t P.cofs),
end

/--The derivative-/
def list_poly_deriv {α : Type} [ring α] : list α → list α
| []     := []
| [a]    := []
| (h::t) := (h * (t.length)) :: list_poly_deriv t

def poly_deriv {α : Type} [ring α] (P : poly α) : poly α :=
begin
  apply poly.mk,
  exact (list_poly_deriv P.cofs.reverse).reverse,
end

/--polynomial modulo some number-/
def list_poly_mod {α : Type} [ring α] [has_mod α] (n : α) : list α → list α
| []     := []
| (h::t) := (h % n) :: list_poly_mod t

def poly_mod {α : Type} [ring α] [decidable_eq α] [has_mod α] (n : α) (P : poly α) : poly α :=
begin
  apply remove_leading_zeros,
  apply poly.mk,
  exact list_poly_mod n P.cofs,
end

infix ` •ₚ `:88 := poly_scalar_mul
prefix ` dₚ `:80 := poly_deriv

/--Polynomial multiplication-/
def list_poly_mul {α : Type} [ring α] (P Q : list α) : list α :=
begin
  induction P,
  { use ([]), },
  { have Qxp : list α, from list_poly_scalar_mul P_hd Q,
    exact list_poly_add (0::P_ih) Qxp },
end

def poly_mul {α : Type} [ring α] [decidable_eq α] (P Q : poly α) : poly α :=
begin
  apply remove_leading_zeros,
  apply poly.mk,
  exact (list_poly_mul P.cofs.reverse Q.cofs.reverse).reverse,
end

instance {α : Type} [ring α] [decidable_eq α] : has_mul (poly α) := ⟨poly_mul⟩

-- instance {α : Type} [ring α] : ring (poly α) :=
-- begin
--   apply ring.mk,
--   repeat {sorry},
-- end

/--Polynomial division-/
--Note: Polynomial division works only for polynomials over a field.

def list_Xn {α : Type} [ring α] [has_one α] [has_zero α] : ℕ → list α
| 0     := [1]
| (n+1) := 0 :: list_Xn n

def Xn {α : Type} [ring α] [has_one α] [has_zero α] (n : ℕ) : poly α := poly.mk (list_Xn n)

def list_poly_div {α : Type} [field α] [decidable_eq α] [inhabited α] (Q : poly α) :
  ℕ → poly α → poly α → poly α × poly α
| 0     q r := (q,r)
| (n+1) q r := if deg r < deg Q then (q,r)
               else do let rol := lead r / lead Q,
                       list_poly_div n (q + (rol •ₚ Xn (deg r - deg Q))) (r - (rol •ₚ Q * Xn (deg r - deg Q)))

def poly_div_quot_rem {α : Type} [field α] [decidable_eq α] [inhabited α] (P Q : poly α) : poly α × poly α :=
list_poly_div Q (deg P - deg Q + 1) 0 P

def poly_quot {α : Type} [field α] [decidable_eq α] [inhabited α] (P Q : poly α) : poly α :=
(poly_div_quot_rem P Q).1

def poly_rem {α : Type} [field α] [decidable_eq α] [inhabited α] (P Q : poly α) : poly α :=
(poly_div_quot_rem P Q).2

infix ` /ₚ `:87 := poly_quot
infix ` %ₚ `:88 := poly_rem

/--Polynomial GCD-/
--Note: this computes the gcd of polynomials over a field.
def poly_gcd_aux {α : Type} [field α] [decidable_eq α] [inhabited α] :
  ℕ → poly α → poly α → poly α
| 0     P Q := P
| (n+1) P Q := if Q = 0 then P else poly_gcd_aux n Q (P %ₚ Q)

def poly_gcd {α : Type} [field α] [decidable_eq α] [inhabited α] (P Q : poly α) :
  poly α := poly_gcd_aux (deg P) P Q

And here's an MWE with the error

import tactic
import data.zmod.basic
import Poly

open zmod
open tactic

#check zmod.field
instance xxx (p : ℕ) [fact (nat.prime p)] : field (zmod p) := infer_instance
instance ttt [fact (nat.prime 7)] : field (zmod 7) := infer_instance

def p : poly (zmod 7) := ⟨[1,2,3]⟩
def q : poly (zmod 7) := ⟨[1,1]⟩

#eval poly_add p q  --works
#eval poly_neg p    --works
#eval poly_deriv p  --works
#eval poly_mul p q  --works
#eval poly_div_quot_rem p q --FAILS!
#eval poly_gcd p q  --FAILS!

[Kevin Buzzard]

Do you need to put fact (nat.prime 7) into the type class inference system? It won't be there automatically

[Kevin Buzzard]

ie instance : fact (nat.prime 7) := by unfold fact; norm_num?

[Lucas Allen]

Yes! that fixed it. Thanks.