ring not respecting arbitrary

Stream: new members

[Yakov Pechersky]

Is it expected that ring will think that separate arbitrary _ values are equal?

import tactic.ring

example : ∃ (a b c : ℚ), 2 * a + (b + 2 * c) = 0 :=
begin
  let a : ℚ := arbitrary _,
  let b : ℚ := arbitrary _,
  let c : ℚ := arbitrary _,
  use [a, b, c],
  ring, -- 5 * a = 0
  sorry
end

[Eric Wieser]

is src#arbitrary irreducible? Edit: yes

[Eric Wieser]

I think by definition any terms constructed with the same function application must be equal to each other

[Yakov Pechersky]

Then I am not sure what arbitrary is supposed to do.

[Eric Wieser]

Well, it prevented you from replacing a with zero at least

[Kevin Buzzard]

Right --here a=b right? This is nothing to do with ring

[Eric Wieser]

Yes

[Eric Wieser]

I guess you could make a tactic that emits new definitions each time you invoke it?

[Eric Wieser]

And then you'd have things that are still defeq under the irreducible veil, but are no longer syntactically equal to each other

[Eric Wieser]

Or even:

@[irreducible] def arbitrary' (n : name) (α : Type*) [inhabited α] : α := default α

example : ∃ (a b c : ℚ), 2 * a + (b + 2 * c) = 0 :=
begin
  let a : ℚ := arbitrary' `a _,
  let b : ℚ := arbitrary' `b _,
  let c : ℚ := arbitrary' `c _,
  use [a, b, c],
  ring, -- 2 * a + (b + 2 * c) = 0
  sorry
end

[Yakov Pechersky]

import tactic.ring

example : true :=
begin
  let a : ℚ := sorry,
  let b : ℚ := sorry,
  suffices : a = b, by trivial,
  refl
end

example : true :=
begin
  let a : ℚ := sorry,
  let b : ℚ := arbitrary _,
  suffices : a = b, by trivial,
  refl -- this fails
end

[Kevin Buzzard]

That'll teach you to sorry data

[Yakov Pechersky]

Then you'll be even more horrified at this:

@[irreducible] def arbitrary' (n : name) (α : Type*) [inhabited α] : α := default α

-- 1.1.17
-- (a) Find infinitely many matrices `B` such that `BA = I₂` when
-- `A = ![![2, 3], ![1, 2], ![2, 5]]`
-- (b) Prove that there is no matrix `C` such that `AC =  I₃`
example (A : matrix (fin 3) (fin 2) ℚ) (hA : A = ![![2, 3], ![1, 2], ![2, 5]]) :
  (∃ (B : matrix (fin 2) (fin 3) ℚ) , B.mul A = 1) ∧
  ∀ (C : matrix (fin 2) (fin 3) ℚ), A.mul C ≠ 1 :=
begin
  split,
  { let c : ℚ := arbitrary' `c _,
    set b : ℚ := - 4 * c - 3 with hb,
    set a : ℚ := - (2 * b + 5 * c) / 3 with ha,
    let d : ℚ := arbitrary' `d _,
    set f : ℚ := d + 1 with hf,
    set e : ℚ := - 2 * (d + f) with he,
    set B : matrix (fin 2) (fin 3) ℚ := ![![a, b, c], ![d, e, f]] with hB,
    use B,
    rw [hA],
    ext i j,
    fin_cases i;
    fin_cases j;
    simp [ha, hb, he, hf];
    ring },
  { sorry }
end

[Eric Wieser]

What's the punchline, for those of us on mobile?

[Yakov Pechersky]

That I'm doing symbolic calculations on explicit matrices using mathlib

[Eric Wieser]

Are you trying to use arbitrary' as a crutch for "infinitely many"?

[Eric Wieser]

I guess the statement would be something like ∃ (s : set $ matrix (fin 2) (fin 3) ℚ) (hs : s.infinite), ∀ B ∈ s, B.mul A = 1)

[Eric Wieser]

And then you use set.range f where f is a function from prod ℚ ℚ to a matrix

[Eric Wieser]

For your example though, I don't think you need arbirary' `name at all - using have c : ℚ := arbitrary _, instead of let does the job

[Damiano Testa]

You could also introduce variables in the statement and prove the following:

def B (R : Type*) [ring R] : R → matrix (fin 2) (fin 3) R :=
  λ d, ![![1, 1, -1], ![d, - 4 * d - 2, d + 1]]

lemma Binj (R : Type*) [ring R] : function.injective (B R) :=
  λ a b ab, (matrix.ext_iff.mpr ab) 1 0

-- 1.1.17
-- (a) Find infinitely many matrices `B` such that `BA = I₂` when
-- `A = ![![2, 3], ![1, 2], ![2, 5]]`
-- (b) Prove that there is no matrix `C` such that `AC =  I₃`
example (d : ℚ) (A : matrix (fin 3) (fin 2) ℚ) (hA : A = ![![2, 3], ![1, 2], ![2, 5]]) :
  (B ℚ d).mul A = 1 ∧ ∀ (C : matrix (fin 2) (fin 3) ℚ), A.mul C ≠ 1 :=
begin
  split,
  { ext i j,
    fin_cases i;
    fin_cases j;
    simp [hA, B];
    ring },
  { sorry }
end

at this point, all that you are missing is that ℚ is infinite.

[Eric Wieser]

Should docs#infinite have more instances?

[Eric Wieser]

For instance, instances for prod, sum, sigma, and pi would all be good starts

[Mario Carneiro]

It seems like there will be a lot of proof search in those instances

[Eric Wieser]

Is it morally any different to instance searches for fintype?

[Mario Carneiro]

Yes, because fintype is a conjunctive property in most cases, which means that you can prove or disprove in linear time wrt the type expression

[Eric Wieser]

Ah right, we end up with a similar problem to docs#pi.nontrivial

[Eric Wieser]

Although we could probably solve it in the same way?

[Damiano Testa]

In this specific case, you could either use the natural numbers, instead of \Q, in the matrix B, or use char_zero, right?

[Yakov Pechersky]

Probably, but I didn't want to deal with nat division

[Damiano Testa]

Ah, actually, I meant to say that replacing \Q by ℤ worked:

example (d : ℤ) (A : matrix (fin 3) (fin 2) ℤ) (hA : A = ![![2, 3], ![1, 2], ![2, 5]]) :
  (B ℤ d).mul A = 1 :=
begin
  ext i j,
  fin_cases i;
  fin_cases j;
  simp [hA, B];
  ring,
end