Zulip Chat Archive

Stream: new members

Topic: Coercions and liftings

Suryansh Shrivastava (Mar 25 2023 at 21:23):

I am getting stuck on lifting and coercions in lean3, is there a source to learn more about them?

Kevin Buzzard (Mar 25 2023 at 21:37):

You wait until you try Lean 4.

Are you specifically interested in the ins and outs of has_lift_t and all that jazz (something I'm completely ignorant about, save for knowing that it's all changed in Lean 4 so there's no point learning about it anyway) or do you just want to know how to prove a goal involving integers when you have the corresponding hypothesis involving naturals?

Suryansh Shrivastava (Mar 26 2023 at 04:53):

Like when I was going through the definition of trece in finite fields, I didn't understand what the function of this symbol was:-⇑
The main theorem that I am looking at now is this :-

lemma trace_to_zmod_nondegenerate (F : Type*) [field F] [finite F] {a : F}
 (ha : a  0) :  b : F, algebra.trace (zmod (ring_char F)) F (a * b)  0 :=
  haveI : fact (ring_char F).prime := char_p.char_is_prime F _⟩,
  have htr := trace_form_nondegenerate (zmod (ring_char F)) F a,
  simp_rw [algebra.trace_form_apply] at htr,
  by_contra' hf,
  exact ha (htr hf),

Suryansh Shrivastava (Mar 26 2023 at 04:54):

but in the documentation, the same statement is given as :-

theorem finite_field.trace_to_zmod_nondegenerate (F : Type u_1) [field F] [finite F] {a : F} (ha : a  0) :
 (b : F), (algebra.trace (zmod (ring_char F)) F) (a * b)  0

Kevin Buzzard (Mar 26 2023 at 10:43):

It's the coercion from a function-like-thing (eg a group homomorphism, which is a function plus some axioms) to the underlying function

Suryansh Shrivastava (Mar 26 2023 at 13:34):

Okay, that makes sense, but we don't need to specify the coercion in our code?

Suryansh Shrivastava (Mar 26 2023 at 13:37):

or does lean generally decipher that for us?

Kevin Buzzard (Mar 26 2023 at 13:37):

Lean inserts it automatically if you write f x where f is a term which is not literally a function but you are attempting to evaluate it at x. The moment Lean sees you putting a term next to another term in a kind of "I'm trying to apply a function to an input" way, if f is not a function then the typeclass inference system will look for a coercion to a function. It's just like if you have a : nat but then write f a where f is a function expecting a real number -- this time it will coerce a from a natural to a real and you'l see f \u a where \u` is a little up-arrow this time representing a coercion from a term to another term.

Sky Wilshaw (Mar 26 2023 at 13:37):

Unfortunately, this process of elaboration isn't easily reversible. To generate the documentation, the elaborated code is "delaborated" back into human-readable stuff, but the delaborator isn't perfect!

Sky Wilshaw (Mar 26 2023 at 13:38):

It adds unnecessary things sometimes.

Kevin Buzzard (Mar 26 2023 at 13:38):

If the system finds a coercion to a function, it will apply the coercion and insert the relevant arrow; if it doesn't, you'll get an error of the form "I expected a function and got something else".

Yes, coercions are a good example where round-tripping is bad in Lean 3. If you cut and paste from the prettyprinter output and it doesn't compile because of an error under a coercion, just delete it; that usually does the trick.

Last updated: Dec 20 2023 at 11:08 UTC