Zulip Chat Archive

Stream: new members

Topic: Working with fields

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


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?

This isn't particularly helpful:

type mismatch
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/4Z\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
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

| `(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
syntax (name := unify_denoms') "unify_denoms'" (location)?: tactic

| `(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

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