Working with fields

Stream: new members

[Leo Shine]

Hello,

I'm trying to write some lean code to work with general fields, and I want to show a goal like
x * b * 2⁻¹ * 2 = x * b
I know that 2 is not equal to zero (as a hypothesis), how do I pass this information into the simplifier or whatever so that it is able to use that fact to prove this seemingly trivial fact?

[Alex J. Best]

try field_simp [name_of_hypothesis] with the name of the hypothesis that 2 is not zero in your field

[Leo Shine]

Yes that's great thanks
Is there a way of making it work out things like 4 ≠ 0 based off 2 ≠ 0 automatically?

Also is there a way of getting good error messages when you accidentally write the 2 ≠ 0 hypothesis without saying this is about the particular field you are working over?

This isn't particularly helpful:

type mismatch
hnotorder2
has type
2 ≠ 0 : Prop
but is expected to have type
2 ≠ 0 : Prop

[Kevin Buzzard]

The best way to ask a question to this community is to give a #mwe . Also note #backticks . From what you say, the issue is that those are different 2s (one is probably a natural) but you can just hover over a 2 or a \ne to see the types of the terms involved.

[Kevin Buzzard]

As for proving 4!=0 I would rewrite 4 as 2*2 and then use exact?. If you want a more specific answer then please ask the question again but this time in the form "here is some compiling code with a sorry, can you suggest various ways of filling it in?"

[Leo Shine]

Thanks didnt realise you could get the details of the actual types of the numbers by hovering

I have managed to prove 4!=0, using mul_ne_zero, I guess I don't have a great grasp of which things Lean + tactics can do by default or whether I just have to prove things like 4!=0 given 2!=0 when they come up

[Kevin Buzzard]

Yeah. Step one is to figure out the difference between a theorem (which you typically rw or apply) and a tactic, and step 1' is to understand that there are only about 50 commonly used tactics and about 10^5 theorems. Step 2 is to get the hang of what the 50 or so tactics do, and this takes time: you just learn by doing, really. The norm_num tactic may or may not prove 4!=0 but that all depends on how you've told it 2!=0 (hence the importance of #mwe s). The ring tactic won't, because of $\Z/4\Z$. You might get somewhere with nlinarith but again it might depend on exactly how you've said that the characteristic isn't 2. etc etc.

[Miguel Marco]

I have been working precisely on a tactic for this kind of things. This is what I have so far:

import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Field.Basic
import Mathlib.Algebra.GroupWithZero.Units.Lemmas
import Mathlib.Algebra.Order.Field.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib
open Lean Meta Elab Tactic Parser Tactic


/-!
# `unify_denoms` tactic

Tactic to clear denominators in algebraic expressions, extends `field_simp`  using
rules that require denominators to be nonzero. The corresponding hypotheses are
added as new goals.
-/


/--
The `unify_denoms` tactic tries to unify denominators in expressions, adding the
necessary hypothesis aabout denominators being nonzero as new goals.
--/
syntax (name := unify_denoms) "unify_denoms" (location)? : tactic

macro_rules
| `(tactic | unify_denoms $[at $location]?) => `(tactic |(
  field_simp $[at $location]?
  repeat (first
    | (rw [← one_div]         $[at $location]?)
    | (rw [div_add_div]       $[at $location]?)
    | (rw [div_sub_div]       $[at $location]?)
    | (rw [add_div']          $[at $location]?)
    | (rw [div_add']          $[at $location]?)
    | (rw [div_sub']          $[at $location]?)
    | (rw [sub_div']          $[at $location]?)
    | (rw [mul_div_mul_right] $[at $location]?)
    | (rw [mul_div_mul_left]  $[at $location]?) )))

/--
The `unify_denoms'` tactic extends `unify_denoms` to work also on
(in)equalities.
--/
syntax (name := unify_denoms') "unify_denoms'" (location)?: tactic

macro_rules
| `(tactic | unify_denoms' $[at $location]?) => `(tactic |(
  unify_denoms $[at $location]?
  repeat (first
  | (rw [div_eq_div_iff] $[at $location]?)
  | (rw [div_le_div_iff] $[at $location]?)
  | (rw [div_lt_div_iff] $[at $location]?)
  | (rw [div_eq_iff]     $[at $location]?)
  | (rw [div_le_iff]     $[at $location]?)
  | (rw [div_lt_iff]     $[at $location]?)
  | (rw [eq_div_iff]     $[at $location]?)
  | (rw [le_div_iff]     $[at $location]?)
  | (rw [lt_div_iff]     $[at $location]?) )))

In your example, if you apply it like this:

example (X : Type) [Field X] (x b : X) : x * b * 2⁻¹ * 2 = x * b := by
  unify_denoms'

it will automatically solve the goal, at the price of leaving you with the task of proving a new goal consisting on 2 ≠ 0

[Miguel Marco]

To be more precise, what is needed in your example is just the rule div_eq_iff . So this works too:

example (X : Type) [Field X] (x b : X) : x * b * 2⁻¹ * 2 = x * b := by
  field_simp
  rw [div_eq_iff]

my tactic just tries a bunch of rules for similar cases.

[Eric Wieser]

Leo Shine said:

Yes that's great thanks
Is there a way of making it work out things like 4 ≠ 0 based off 2 ≠ 0 automatically?

The polyrith tactic can do this

[Kevin Buzzard]

Even though it's false for Z/4Z? Does polyrith behave differently with fields?

[Eric Wieser]

Whoops, I'm thinking of it solving 4 = 0 from 2 = 0

[Miguel Marco]

I guess cast_eq_zero_iff or charP_iff would be the relevant rules.