Coercions and liftings

Stream: new members

[Suryansh Shrivastava]

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

[Kevin Buzzard]

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]

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 :=
begin
  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),
end

[Suryansh Shrivastava]

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]

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]

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

[Suryansh Shrivastava]

or does lean generally decipher that for us?

[Kevin Buzzard]

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]

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]

It adds unnecessary things sometimes.

[Kevin Buzzard]

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.