Easy equations modulo N

Stream: new members

[Eloi]

Hi, I have this state:

N : ℕ
AB : special_linear_group (fin 2) ℤ
A₁ : ⇑A 1 0 ≡ 0 [ZMOD ↑N]
A₂ : ⇑A 0 0 ≡ 1 [ZMOD ↑N]
A₃ : ⇑A 0 1 ≡ 0 [ZMOD ↑N]
B₁ : ⇑B 1 0 ≡ 0 [ZMOD ↑N]
B₂ : ⇑B 0 0 ≡ 1 [ZMOD ↑N]
B₃ : ⇑B 0 1 ≡ 0 [ZMOD ↑N]
⊢ ⇑A 1 0 * ⇑B 0 0 + ⇑A 1 1 * ⇑B 1 0 ≡ 0 [ZMOD ↑N]

This should be easy, like a bunch of rw and simp or ring. What am I missing?

A minimal example:

import data.matrix.basic
import data.int.modeq


variables {A B: matrix (fin 2) (fin 2) ℤ}
        {N: nat}

lemma lem (A₁ : A 1 0 ≡ 0 [ZMOD ↑N])
    (A₂ : A 0 0 ≡ 1 [ZMOD ↑N])
    (A₃ : A 0 1 ≡ 0 [ZMOD ↑N])
    (B₁ : B 1 0 ≡ 0 [ZMOD ↑N])
    (B₂ : B 0 0 ≡ 1 [ZMOD ↑N])
    (B₃ : B 0 1 ≡ 0 [ZMOD ↑N]):  A 1 0 * B 0 0 + A 1 1 * B 1 0 ≡ 0 [ZMOD ↑N]:=

begin
    sorry,

end

Thanks!

[Kenny Lau]

import data.matrix.basic
import data.int.modeq

variables {A B: matrix (fin 2) (fin 2) ℤ} {N: nat}

lemma lem (A₁ : A 1 0 ≡ 0 [ZMOD ↑N])
  (A₂ : A 0 0 ≡ 1 [ZMOD ↑N])
  (A₃ : A 0 1 ≡ 0 [ZMOD ↑N])
  (B₁ : B 1 0 ≡ 0 [ZMOD ↑N])
  (B₂ : B 0 0 ≡ 1 [ZMOD ↑N])
  (B₃ : B 0 1 ≡ 0 [ZMOD ↑N]):
  A 1 0 * B 0 0 + A 1 1 * B 1 0 ≡ 0 [ZMOD ↑N] :=
begin
  have := (A₁.modeq_mul B₂).modeq_add (B₁.modeq_mul_left (A 1 1)),
  rw [zero_mul, mul_zero, add_zero] at this,
  exact this
end

lemma lem' (A₁ : A 1 0 ≡ 0 [ZMOD ↑N])
  (A₂ : A 0 0 ≡ 1 [ZMOD ↑N])
  (A₃ : A 0 1 ≡ 0 [ZMOD ↑N])
  (B₁ : B 1 0 ≡ 0 [ZMOD ↑N])
  (B₂ : B 0 0 ≡ 1 [ZMOD ↑N])
  (B₃ : B 0 1 ≡ 0 [ZMOD ↑N]):
  A 1 0 * B 0 0 + A 1 1 * B 1 0 ≡ 0 [ZMOD ↑N] :=
by simpa only [zero_mul, mul_zero, add_zero] using (A₁.modeq_mul B₂).modeq_add (B₁.modeq_mul_left (A 1 1))

[Kevin Buzzard]

lemma lem (A₁ : A 1 0 ≡ 0 [ZMOD ↑N])
    (A₂ : A 0 0 ≡ 1 [ZMOD ↑N])
    (A₃ : A 0 1 ≡ 0 [ZMOD ↑N])
    (B₁ : B 1 0 ≡ 0 [ZMOD ↑N])
    (B₂ : B 0 0 ≡ 1 [ZMOD ↑N])
    (B₃ : B 0 1 ≡ 0 [ZMOD ↑N]):  A 1 0 * B 0 0 + A 1 1 * B 1 0 ≡ 0 [ZMOD ↑N]:=

begin
  rw (show (0 : ℤ) = 0 * B 0 0 + A 1 1 * 0, by ring),
  apply int.modeq.modeq_add;
  apply int.modeq.modeq_mul;
  try {assumption};
  refl
end

[Eloi]

Thanks!

I'm puzzeled by the weird thing that try{assumtion} does, and why exact A₁, doesn't work there?

[Kevin Buzzard]

I am doing semicolon magic

[Kevin Buzzard]

Change the semicolon to a comma and you'll see that actually I have four goals at the try {assumption} point. The semicolon means "do the next tactic on all the goals created by the last tactic"

[Eloi]

Oh I see it now, thanks!

[Jalex Stark]

assumption' is an alias for any_goals { assumption }