Avoiding type annotation

Stream: mathlib4

[Utensil Song]

Is there a way in Lean to avoid type annotation or express it before the : like explicitly choosing an instance for Mul in the following #mwe ? ( 3 examples are shown to demonstrate the spiritually same use case)

import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
import Mathlib.Tactic

variable {R : Type _}

variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]

variable {Q : QuadraticForm R M}

variable (u v w : CliffordAlgebra Q)

local instance hasCoeCliffordAlgebraRing : Coe R (CliffordAlgebra Q) := ⟨algebraMap R (CliffordAlgebra Q)⟩
local instance hasCoeCliffordAlgebraModule : Coe M (CliffordAlgebra Q) := ⟨CliffordAlgebra.ι Q⟩

/-!
  https://arxiv.org/abs/1205.5935

  Axiom 3. G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
-/
example (u v: M) : ∃ w : M, w = (u + v : CliffordAlgebra Q) := by
  use (u + v)
  rw [map_add]

example (r : R) (u : M) : (r * u : CliffordAlgebra Q) = u * r := by rw [@Algebra.commutes]

example (r : R) (u : M) : ∃ w : M, w = (r * u : CliffordAlgebra Q) := by
  use (r • u)
  rw [map_smul, Algebra.smul_def, Algebra.commutes]

P.S. I also don't know if using coe is the idiomatic way to try to write it in Lean as close as in math, but it works for other cases with the help from local notations and definitions.

[Eric Wieser]

If you want more symmetry, you could write:

notation:50 A " =[" T:50 "] " B:50 => @Eq T A B

example (u v: M) : ∃ w : M, w =[CliffordAlgebra Q] u + v := by
  use (u + v)
  rw [map_add]

[Eric Wieser]

Another option is

local macro_rules | `($a * $b) => `(HMul.hMul ($a : CliffordAlgebra Q) ($b : CliffordAlgebra Q))

though this is likely to become annoying quickly

[Utensil Song]

Annotating the eq seems clear and noiseless. The macro rules version is something I would wish to avoid too.

[Utensil Song]

local notation "Cl" => CliffordAlgebra Q
local notation:50 A "=" B:50 ":" T:50 => @Eq T A B

example (u v: M) : ∃ w : M, w = u + v : Cl := by
  use (u + v)
  rw [map_add]

seems more natural to me. Any idea why abbrev Cl := CliffordAlgebra Q doesn't work in place of local notation?

type mismatch
  u + v
has type
  M : outParam (Type u_2)
but is expected to have type
  Cl : Type (max ?u.218013 ?u.218012)

where

/-
Cl.{u_2, u_1} {R : Type u_1} {M : Type u_2} [inst✝ : CommRing R] [inst✝¹ : AddCommGroup M] [inst✝² : Module R M]
  {Q : QuadraticForm R M} : Type (max u_2 u_1)
-/
#check Cl

[Utensil Song]

Another caveat is that annotating only eq doesn't remove the need of local notation in

local notation x "²" => (x : Cl)^2

theorem ι_sq_scalar (m : M) : m² = Q m : Cl := by
  rw [pow_two, CliffordAlgebra.ι_sq_scalar]
  done

without the type annotation in local notation:

local notation x "²" => x^2

/-
failed to synthesize instance
  HPow M ?m.302609 Cl
-/
theorem ι_sq_scalar (m : M) : m² = Q m : Cl := by
  rw [pow_two, CliffordAlgebra.ι_sq_scalar]
  done

[Utensil Song]

It's not yet clear to me whether lean4#2854 (context: :thread: ) helps.

[Utensil Song]

A new case, #mwe:

import Mathlib.LinearAlgebra.CliffordAlgebra.Star

set_option autoImplicit false

variable {R : Type*} [CommRing R]

variable {M : Type*} [AddCommGroup M] [Module R M]

variable {Q : QuadraticForm R M}

open CliffordAlgebra

/-
failed to synthesize instance
  HMul (CliffordAlgebra Q) (CliffordAlgebra Q)ˣ (CliffordAlgebra Q)
-/
theorem units_involute_act_eq_conjAct {x : (CliffordAlgebra Q)ˣ} (y : M) : CliffordAlgebra.involute x * ι Q y * x⁻¹ = ConjAct.toConjAct x • ι Q y := by sorry

/-
  Instead, I have to write it with ↑ and type annotation
-/
theorem units_involute_act_eq_conjAct' {x : (CliffordAlgebra Q)ˣ} (y : M) : CliffordAlgebra.involute x * ι Q y * (↑x⁻¹ : CliffordAlgebra Q) = ConjAct.toConjAct x • ι Q y := by sorry

[Utensil Song]

When type class search fails to synth a HMul a b a, it seems reasonable for it to try coercion to synth an Mul a a a. Don't know if it's possible to be encoded in Lean.

[Eric Wieser]

I think something weirder is going on here:

import Mathlib.LinearAlgebra.CliffordAlgebra.Star

variable {R : Type*} [CommRing R]
variable {M : Type*} [AddCommGroup M] [Module R M]
variable {Q : QuadraticForm R M}

open CliffordAlgebra

-- ok
example {x : (CliffordAlgebra Q)ˣ} (y : M) : involute (Q := Q) x * ι Q y * x⁻¹ = ConjAct.toConjAct x • ι Q y := by sorry

-- fails
example {x : (CliffordAlgebra Q)ˣ} (y : M) : involute (Q := _) x * ι Q y * x⁻¹ = ConjAct.toConjAct x • ι Q y := by sorry

[Eric Wieser]

It seems that the actual problem is that Lean can't work out the type of involute x until it's looked at the *

[Eric Wieser]

I think this is due to a conflict between the default elaboration rules, which work from the outside in, and the special rules for * (binop%), which work from the inside out. If you disable those special rules then this works:

-- restore the lean3 behavior
macro_rules | `($x * $y) => `(@HMul.hMul _ _ _ instHMul $x $y)

-- ok
example {x : (CliffordAlgebra Q)ˣ} (y : M) :
  involute x * ι Q y * ↑x⁻¹ = ConjAct.toConjAct x • ι Q y := by sorry

[Utensil Song]

Interesting that it can be fixed by annotating the other Mul

[Utensil Song]

Eric Wieser said:

I think this is due to a conflict between the default elaboration rules, which work from the outside in, and the special rules for * (binop%), which work from the inside out. If you disable those special rules then this works:

-- restore the lean3 behavior
macro_rules | `($x * $y) => `(@HMul.hMul _ _ _ instHMul $x $y)

-- ok
example {x : (CliffordAlgebra Q)ˣ} (y : M) :
  involute x * ι Q y * ↑x⁻¹ = ConjAct.toConjAct x • ι Q y := by sorry

More context seems to be in lean4#1915.

[Utensil Song]

Or a few other PRs on binop, are they fixing something same underneath case by case?

[Eric Wieser]

I don't think there are any planned core changes incoming here

[Kyle Miller]

Here's a couple places where there's documentation about how the expression tree elaborator works:

• https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Extra.lean#L82 is the file with the elaborator
• the "manual-level explanation" in RFC lean4#2854

[Kyle Miller]

Outside-in vs inside-out isn't completely accurate. It elaborates each leaf in a full arithmetic expression without an expected type, then it computes a type that everything can be coerced to, and then it inserts coercions where needed.

A difference one can observe is that coercions don't get sunk into the leaves in expression trees -- they're stuck right at a leaf -- where if there were no such elaborator then coercions can get sunk arbitrarily deep based on expected types.

[Kyle Miller]

Indeed, I just looked at the first example and I see involute ↑x * (ι Q) y * ↑x⁻¹ = ConjAct.toConjAct x • (ι Q) y. It needs to sink a coercion into the argument to involute.

I obliquely mentioned this in the "future possibilities" section of the RFC. If there were a way for involute to participate in this elaboration algorithm and say that the input and output should have the same type, then the expression tree elaborator could help get this to elaborate successfully

[Eric Wieser]

Doesn't this mean that in practice almost every function ends up having to participate in the new elaboration?

[Eric Wieser]

It needs to sink a coercion into the argument to involute.

I guess the problem is that even

variable {x : (CliffordAlgebra Q)ˣ}
#check involute x

doesn't elaborate

[Kyle Miller]

I don't think so, just expressions that are algebraic operators of some sort, in the sense that you want all the "primary" arguments to all of them to have the same type.

[Kyle Miller]

Eric Wieser said:

I guess the problem is that even ...doesn't elaborate

Maybe involute needs its own elaborator to try to compute its Q and insert a coercion if needed?

[Eric Wieser]

I think this is a more general problem with coercion from Units

[Eric Wieser]

We have this problem for matrices elsewhere too

[Eric Wieser]

(the fact that involute is a morphism seems to be a distraction; it seems to fail as a plain function too)

[Utensil Song]

Eric Wieser said:

I think this is a more general problem with coercion from Units

Can a general elab be defined for Units, regardless of what the function is?

[Utensil Song]

Kyle Miller said:

Outside-in vs inside-out isn't completely accurate. It elaborates each leaf in a full arithmetic expression without an expected type, then it computes a type that everything can be coerced to, and then it inserts coercions where needed.

A difference one can observe is that coercions don't get sunk into the leaves in expression trees -- they're stuck right at a leaf -- where if there were no such elaborator then coercions can get sunk arbitrarily deep based on expected types.

The arbitrary deep issue seems to be manageable by a max depth analogous to max hearbeat. And it's quite small in practice, less than 5.

[Kyle Miller]

The issue here isn't about arbitrary depth, it's that the expression tree elaborator is only aware of terms that appear (recursively) as operands to binop% notations, etc. The algorithm would not work at all if it were extended to visit all operands to all functions to a certain depth.

[Utensil Song]

I see...

[Kyle Miller]

There's no single process that is responsible for sinking coercions arbitrarily deep into expressions in the main elaborator. It's a combination of the fact that when elaborating there's an expected type, and when function applications are elaborated Lean can insert coercions to the functions arguments when there's a type mismatch.

[Kyle Miller]

For example, in

#check (id (5 : Nat) : Int)
/- id ↑5 : ℤ -/

[Kyle Miller]

The expression tree evaluator does try to play nicely with this, at least in one direction (when it's inside another expression, rather than when other expressions are within it):

#check (id ((5 : Nat) + (6 : Nat)) : Int)
/-
id (↑5 + ↑6) : ℤ
-/

This by the way is an example of why it's not accurate to say that it's "inside-out". It's using the expected type "outside-in" and pushes coercions to the leaves.

[Utensil Song]

Just read the elab code, now it makes much more sense. It seems that operator side has done what it can, the cause might be how involute is defined.

[Eric Wieser]

I think involute is a distraction here: here's a much more minimal #mwe:

import Mathlib.Data.ZMod.Basic

def foo {n} (z : Fin n) : ℤ := z + 1

variables (zu : (Fin 2)ˣ)
#check foo zu  -- fails
#check foo ↑zu  -- fails
#check foo (zu : Fin 2)  -- ok

[Eric Wieser]

The ingredients seem to just be using Units on a parameterized type

[Kyle Miller]

What does the coercion for units? I wonder if this is one of these things where we have to exeriment with CoeHead, etc.

[Eric Wieser]

I believe it's a CoeOut docs#Units.instCoeHeadUnits

[Utensil Song]

I don't understand what I'm doing, but defining any of these instances doesn't help @Eric Wieser 's MWE:

variable {n : Nat} [Monoid (Fin n)] (z :  (Fin n)ˣ)

instance : CoeHead (Fin n)ˣ (Fin n) :=
  ⟨Units.val⟩

instance : CoeTail (Fin n)ˣ (Fin n) :=
  ⟨Units.val⟩

instance : Coe (Fin n)ˣ (Fin n) where
  coe := Units.val

instance : CoeDep (Fin n)ˣ z (Fin n) where
  coe := Units.val z

Related.

[Utensil Song]

Checking with set_option trace.Meta.synthInstance true, CoeDep did help, making the :explosion: happen in fewer steps.

[Wrenna Robson]

Oh yes, I noticed this recently in my work with units. Honestly in some ways the fact it's a coercion at all is a bit of a trap because it is hard to make it work. I don't know what defines the coercion.

[Wrenna Robson]

I wonder if it's related somehow to the fact that a unit contains two pieces of data? I mean it shouldn't be, it's hardly unique in that. But it's the only aspect that seems weirder than anything else.

[Utensil Song]

In #9111, the directly ported lipschitz looks like this:

def lipschitz (Q : QuadraticForm R M) :=
  Subgroup.closure (Coe.coe ⁻¹' Set.range (ι Q) : Set (CliffordAlgebra Q)ˣ)
#align lipschitz lipschitz

which fails with

failed to synthesize instance
  Coe (CliffordAlgebra Q)ˣ (CliffordAlgebra Q)

Of course, it works if Coe.coe is changed to CoeHead.coe but I was ignorant about it and used Units.val in its place. I think it makes it even more clear about what the preimage is. And even knowing that CoeHead.coe works, I'm still reluctant to change it back. I hope that's OK.

Posting this here as this topic has more context, and I still wonder why the synthesization failed.

[Utensil Song]

Eric Wieser said:

I think this is due to a conflict between the default elaboration rules, which work from the outside in, and the special rules for * (binop%), which work from the inside out. If you disable those special rules then this works:

-- restore the lean3 behavior
macro_rules | `($x * $y) => `(@HMul.hMul _ _ _ instHMul $x $y)

-- ok
example {x : (CliffordAlgebra Q)ˣ} (y : M) :
  involute x * ι Q y * ↑x⁻¹ = ConjAct.toConjAct x • ι Q y := by sorry

Also in #9111, I've used this solution, but for a serious PR, I think I need to remove this macro_rules but as this errors for all occurrences and alike (>5) of involute ↑x * ι Q y * ↑x⁻¹ in the file, should I use involute (Q := Q) instead? It seems less poluting and better than type annotating ↑x⁻¹. (UPDATE: this commit has done this.)

[Eric Wieser]

In Lean4 you should pretty much never write Coe.coe, but (↑)

[Utensil Song]

(↑) ⁻¹' definitely works in this case!

[Utensil Song]

with the extra benefit that hover/cm+click on it gives Units.val : (CliffordAlgebra Q)ˣ → CliffordAlgebra Q :astonished: