## Stream: new members

### Topic: Working with fields

#### Leo Shine (Oct 28 2023 at 20:30):

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 (Oct 28 2023 at 20:49):

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

#### Leo Shine (Oct 28 2023 at 20:59):

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?

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

#### Kevin Buzzard (Oct 28 2023 at 21:13):

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 (Oct 28 2023 at 21:15):

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 (Oct 28 2023 at 21:18):

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 (Oct 28 2023 at 22:03):

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 (Oct 28 2023 at 22:06):

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
-/

/--
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 (Oct 28 2023 at 22:11):

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 (Oct 28 2023 at 22:41):

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 (Oct 28 2023 at 22:46):

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

#### Eric Wieser (Oct 28 2023 at 23:07):

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

#### Miguel Marco (Oct 28 2023 at 23:26):

I guess cast_eq_zero_iff or charP_iff would be the relevant rules.

Last updated: Dec 20 2023 at 11:08 UTC