notation for "type of x"

Stream: new members

[Alex Meiburg]

I have a term x of type Group g, and I'm making another term y also of type Group g. If I write my expression for y bare, like f x foo bar, then Lean can't infer all the types it needs and gets stuck. If I supply a cast like (f x foo bar : Group g), then Lean computes it fine.

Now, I could write ( ... : Group g) everywhere in my code. But this expression f x foo bar is kind of long and I'm using it lots of places, so I'm defining a notation for it, something like

notation:100 x " ∘[ " p " ] " y  => (composeAt x p y : Group g)

The above doesn't actually compile, because g isn't in scope. I can do set_option quotPrecheck false right before, and then this notation works, but only as long it's actually called g. Which is kind of gross, I'll admit.

I would like to be able to write something like

notation:100 x " ∘[ " p " ] " y  => (composeAt x p y : typeof(x))

and then my notation would do

x ∘[ foo ] bar
--->
(composeAt x foo bar : typeof(x))
--->
(composeAt x foo bar : Group g)

and work how I want. Is there any way to do this in Lean?

[Alex Meiburg]

(deleted)

[Matt Diamond]

is composeAt x p y : typeof(x) a simplification or the actual code you want to be able to write?

[Alex Meiburg]

The actual code I want to be able to write. I realize that typeof is not real syntax, so I'm wondering if there's anything else I could write of a similar form, to say "elaborate this expression into the same type as the term x you already have".

[Matt Diamond]

I'm curious what the type signature of composeAt is then... wouldn't the type signature make it clear that the type of the output of the function should be identical to the type of the first variable passed into it? I'm wondering how Lean gets confused here

[Mario Carneiro]

Alex Meiburg said:

I realize that typeof is not real syntax,

#check type_of% 1 -- Nat : Type

[Alex Meiburg]

oh nice! Thanks. :)

[N Gelwan]

But why can't you write a new function which binds its output type to the type of x?

[Alex Meiburg]

So, the type signature is Group g -> (some thing I defined) -> Group g -> Group g. So yes, you would expect it to be able to deduce it from the type of x.

The weird part is that I was using it in forms like composeAt 1 0 y, and I think it was somehow getting tripped up with what type to cast 1 into and then how to interpret the value of p, 0 (which had a dependent type on x). This fixed my problem:

notation:70 x:71 " ∘[ " p:70 " ] " y:70  => (composeAt x p y : typeof% x)

and now it all elaborates fine!

[Alex Meiburg]

(If this sounds suspicious, like, "Alex you're doing something wrong if this is the problem you're having", please let me know)

[Mario Carneiro]

an MWE would be helpful

[Alex Meiburg]

Okay, in the process of trying to make a mwe and running into more issues, I think I found the 'real' solution, which is that I should change the order of arguments in composeAt to be x y p. The type of p still depends on x, but now the elaborator hits y before p, so it goes back and knows the right type for x, and doesn't get stuck at p. My notation reorders the arguments to make sense anyway.

[Alex Meiburg]

If you want to see exactly what's going on, here's the code I've actually got. Trying to build up to operads

import Mathlib

variable (A : ℕ → Type*)

def Family :=
  Sigma A

class MultiComposable where
  compose {n m} : A n → Fin n → A m → A (n+m-1)

class ComposableOne where
  one : A 1

instance ComposableOne.toOne [ComposableOne A] : One (Family A) :=
  ⟨⟨_, one⟩⟩

namespace BadExample

def composeAt {A} [MultiComposable A] (x : Family A) (p : Fin x.fst) (y : Family A)
  : Family A :=
    ⟨_, MultiComposable.compose x.snd p y.snd⟩

scoped notation:70 x:71 " ∘[ " p:70 " ] " y:70  => composeAt x p y

class Operad extends MultiComposable A, ComposableOne A where
  id_left (a : Family A) : 1 ∘[0] a = a --error here
  --if I do some casting in my notation based on y, then this fails instead
  id_right (a : Family A) (p : Fin a.fst) : a ∘[p] 1 = a

end BadExample

namespace GoodExample

--now we change the order of the arguments
def composeAt {A} [MultiComposable A] (x : Family A) (y : Family A) (p : Fin x.fst)
  : Family A :=
    ⟨_, MultiComposable.compose x.snd p y.snd⟩

scoped notation:70 x:71 " ∘[ " p:70 " ] " y:70  => composeAt x y p

class Operad extends MultiComposable A, ComposableOne A where
  id_left (a : Family A) : 1 ∘[0] a = a --works fine
  id_right (a : Family A) (p : Fin a.fst) : a ∘[p] 1 = a --works fine

[Matt Diamond]

FYI there's a typo in BadExample, you wrote ∘1[ instead of ∘[ when you declared the notation

I know it's not the actual issue here

[Alex Meiburg]

oops yeah, fixed

[Kevin Buzzard]

Another approach if you want two district Group structures on one type g is to make a type synonym def g' := g and put the second group structure on g' instead. You can define the bijection from g to g' using rfl and then typeclass interference will know what you mean by * because it will be able to look at the type.

[Alex Meiburg]

Ah, it wasn't really Group, it was some type I had defined (Family) -- but I figured that would distract from the question...

[Kevin Buzzard]

Is Family a structure or a class?

[Alex Meiburg]

It's

def Family (A : Nat → Type*) :=
  Sigma A

I'm modelling my code to a decent degree off of GradedMonoid (which is defined the same as Family, except that it takes an arbitrary (A : ι → Type*) and not just Nat)

[Kevin Buzzard]

Oh ok. The type synonym trick is a way to get two distinct instances of a class on the same type so is probably not relevant here.

[Alex Meiburg]

yeah, maybe Group was a poor choice for my stand-in then, whoops

[Alex Meiburg]

Dependent types are getting me down. :( I don't know how to show that things are equal when the starting types are different... and I get messages like this that I can't understand:

case h.h
A: ℕ → Type u_1
v: Type
a: (k : ℕ) × ((Fin k → v) → v)
asnd: (Fin a.fst → v) → v
vs: Fin (1 + a.fst - 1) → v
k2: Fin a.fst
| { val := ↑k2, isLt := (_ : ↑k2 < 1 + a.fst - 1) }
Messages (1)
Operad.lean:190:10
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  { val := ↑?a, isLt := ?h }
case h.h
A: ℕ → Type u_1
v: Type
a: (k : ℕ) × ((Fin k → v) → v)
asnd: (Fin a.fst → v) → v
vs: Fin (1 + a.fst - 1) → v
k2: Fin a.fst
| { val := ↑k2, isLt := (_ : ↑k2 < 1 + a.fst - 1) }

So here the goal (in conv mode) was

{ val := ↑k2, isLt := (_ : ↑k2 < 1 + a.fst - 1) }

and I did rw [Fin.eta] but it says it can't find that... urgh....

[Riccardo Brasca]

Equality is a relation defined on two terms with the same type, so in general you should not do that.

[Riccardo Brasca]

We have a more general notion, but it's probably a good idea to avoid it

[Alex Meiburg]

I'm aware there's HEq but I have a very bad idea of how to use it

[Alex Meiburg]

I mean, it seems worth being able to say that (x : Fin (n+m)) = (y : Fin (m+n)) and stuff like that. And I'm not sure how I'm "supposed" to handle things like that

[Riccardo Brasca]

This is really a limit case. Sometimes you can rw [add_comm] (maybe simp_rw) at x, where x : Fin (n+m). The clean way of doing this is to use docs#finCongr

[Riccardo Brasca]

It gives you a bijection Fin m ≃ Fin n if n = m that you should use to pass from Fin m to Fin n

[Alex Meiburg]

How do things like GradedMonoid handle it...? I mean, I have a mul : A i -> A j -> A (i+j), which means that I can't express commutativity as mul (x : A i) (y : A j) = mul y x, because one side is an A (i+j) and the other is A (j+i). I see that clearly they do express things like commutativity, but I'm struggling to understand how. It looks like they just render some kind of forgetful thing that turns mul into a "union" multiply over the whole thing, with no dependent information...?

[Kyle Miller]

One solution is to define mul i j k : A i -> A j -> A k that's zero unless k = i + j. Chain complexes do something similar.

[Kyle Miller]

I suppose a tradeoff is that k isn't inferred from i and j.

[Mario Carneiro]

can you use default arguments for that?

[Riccardo Brasca]

The trick is that if A : ι → Type u, than GradedMonoid A (that is defined as Sigma A) has a "normal" multiplication

[Riccardo Brasca]

And we require this one to be commutative

[Riccardo Brasca]

So we have a class docs#GradedMonoid.GMul and an instance saying that Mul (GradedMonoid A) if [GradedMonoid.GMul A]. The definition of the multiplication is

fun x y : GradedMonoid A => ⟨_, GMul.mul x.snd y.snd⟩

[Riccardo Brasca]

In particular, the equality for the commutativity is just x * y = y * x, where now x, y, x*y and y*x have all type GradedMonoid A. The equality x * y = y * x is an equality in a Sigma type, so it is the same as requiring that both components are equal. The equality of the first component says what you want, and the other one is automatically true since ι is a commutative monoid.

[Eric Wieser]

(I think you mean the equality of the second component says what you want?)

[Eric Wieser]

Alex Meiburg said:

If you want to see exactly what's going on, here's the code I've actually got.

Adding instance [ComposableOne A] : NeZero ((1 : Family A).1) := ⟨one_ne_zero⟩ fixes this

[Riccardo Brasca]

Eric Wieser said:

(I think you mean the equality of the second component says what you want?)

Yes, of course

[N Gelwan]

Here's a question I had that ended up on the grading topic recently, if you're interested: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Identities.20to.20Equivalences.20in.20Graded.20Structures/near/410059564.

[Alex Meiburg]

Alright, I'm trying to muddle my way through HEq. I understand that a painful part of HEq it (HEq f g) (HEq x y) doesn't imply (HEq (f x) (g y)). Are either of these true, at least? Are they named in Mathlib, or if not, is there a tactic that applies them for me?

lemma heq_funext {f : α₁ → β} {g : α₂ → β} (h : ∀x y, (hxy : HEq x y) → f x = g y) : HEq f g := by
  sorry

lemma heq_congr {f : α₁ → β} {g : α₂ → β} (h₁ : HEq f g) (h₂ : HEq x y) : f x = g y := by
  sorry

[Riccardo Brasca]

I am not completely sure, but we have docs#Function.hfunext, that suggests your first lemma is not true.

[Riccardo Brasca]

And the second one seems to me exactly the fact that HEq f g and HEq x y implies HEq (f x) (f y) (just use heq_iff_eq), that does not hold.

[Mario Carneiro]

the second one is true

lemma heq_congr {f : α₁ → β} {g : α₂ → β} (h₁ : HEq f g) (h₂ : HEq x y) : f x = g y := by
  cases h₂
  cases h₁
  rfl

[Riccardo Brasca]

OK, I could have waited 10 more seconds :D

[Riccardo Brasca]

Ah, of course, the difference is that we have the same β both for f and g.

[Mario Carneiro]

heq_funext looks even more strongly false, you should be able to disprove it if you take α₁ and α₂ to be provably different types

[Riccardo Brasca]

@Alex Meiburg you can of course doing whatever you prefer, but there are reasons why we suggest to avoid HEq. The design choices we made in mathlib can look not very natural (for example the current design of graded monoid), but we thought carefully about it, and it's probably not a good idea for a beginner to try to reinvent the wheel.

Having said that, I completely understand that trying to do it by yourself is funny and interesting!

[Mario Carneiro]

import Mathlib.Logic.Equiv.Basic

axiom heq_funext {α₁ α₂ β} {f : α₁ → β} {g : α₂ → β} (h : ∀x y, (hxy : HEq x y) → f x = g y) : HEq f g

example : False := by
  have := @heq_funext False True Bool (fun _ => true) (fun _ => true) (fun.)
  have : (False → Bool) ≃ (True → Bool) := type_eq_of_heq this ▸ .refl _
  cases congrFun (this.symm.subsingleton.allEq (fun _ => false) (fun _ => true)) ⟨⟩

[Eric Rodriguez]

Riccardo Brasca said:

Alex Meiburg you can of course doing whatever you prefer, but there are reasons why we suggest to avoid HEq. The design choices we made in mathlib can look not very natural (for example the current design of graded monoid), but we thought carefully about it, and it's probably not a good idea for a beginner to try to reinvent the wheel.

Having said that, I completely understand that trying to do it by yourself is funny and interesting!

I think HEq is unfairly maligned; it definitely can have its uses. Also, Eric W's indexed eq was an interesting experiment that still has time to go somewhere

[Alex Meiburg]

Ah, that's a shame about the funext. Yes, I would like to avoid HEq, but I really don't see any way to define operads without Sigma types: the basic composition operation in operads is dependently typed. And then, whenever I want Sigma.ext, HEq gets in there.

[Riccardo Brasca]

I don't know anything about operads, but I suggest you ask exactly what you need and I am sure someone will help.

[Riccardo Brasca]

Avoiding #xy

[Mario Carneiro]

I think HEq is unfairly maligned; it definitely can have its uses.

I think the correct tool that you usually want to use in place of HEq is called a "pathover" in HoTT, and represents an equality dependent on another equality.

inductive Pathover (P : α → Sort u) (x : α) (a : P x) : ∀ (y : α), x = y → P y → Prop
  | rfl : Pathover P x a x rfl a

The trouble with HEq is that it is equivalent to the specific combination ∃ h : α = β, Pathover id α x β h y:

example {x : α} {y : β} : HEq x y ↔ ∃ h : α = β, Pathover id α x β h y := by
  constructor
  · rintro ⟨⟩; exact ⟨_, ⟨⟩⟩
  · rintro ⟨⟨⟩, ⟨⟩⟩; exact .rfl

and so it bakes a type equality into the definition (i.e. we set the α in Pathover to Type u), which is less introspectable than if the type was, say, an inductive type and P was a nontrivial function, since then we can do inversion on that equality. (The other awkward thing about HEq is the fact that it erases the proof h : α = β by quantifying over it, although in lean this is not much of an issue because of proof irrelevance. In actual HoTT without proof irrelevance you can't do this because you might need to remember that your pathover is over a particular equality and forgetting it and reintroducing a new one can produce nontrivial loops.)

You might ask why mathlib doesn't have pathovers given all of this. One reason is that "just avoid the whole area" is surprisingly effective advice, and another reason is that one pathover is not enough, you might need 2-pathovers as well:

inductive Pathover2 (P : α → Sort u) (Q : ∀ a, P a → Sort v) (x : α) (a : P x) (q : Q x a) :
    ∀ (y : α) (h : x = y) (b : P y), Pathover P x a y h b → Q y b → Prop
  | rfl : Pathover2 P Q x a q x rfl a .rfl q

The more generalizable way of getting these equalities is by using equalities in sigma types instead.

[Mario Carneiro]

There is a counterpoint to this though, which is that pathovers are equivalent to HEq because of proof irrelevance:

example (h : x = y) : Pathover P x a y h b ↔ HEq a b := by
  constructor
  · rintro ⟨⟩; exact .rfl
  · cases h; rintro ⟨⟩; exact .rfl

So you can kind of pretend that a HEq is really a pathover and ignore the type equality it bakes in. This only works in the presence of the equality x = y though (which is also a prerequisite for stating a pathover), you should not attempt to do "inversion" on a HEq to get type equalities out of it because that's where all the undesirable properties come from. Just think of this as the "second half" of a sigma type equality: (⟨x, a⟩ : Σ x : α, P x) = ⟨y, b⟩ <-> ∃ h : x = y, ???, where the equality h : x = y is already in context and hence the type equality expressed by the HEq a b is already provable from other things in the context.

[Kyle Miller]

(Re "inversion", the congr! tactic tries to help you with this by giving you all the relevant preceding Eq/HEq goals as additional hypotheses. This isn't strictly necessary though, since you can re-prove these in later goals as needed.)

[Kyle Miller]

Here's a list of ways I know for handling these equality problems. HEq is one of them, but it's at the end of the list because there's usually a better option. Sometimes HEq pops up in the middle of a proof, and it's fine, but you don't necessarily want to make a whole theory using it.

variable {α : Type*} {β : α → Type*}

section

/-! # Use a cast function and equality

Pros:
- Sticks with equality
- Uses a function that rewrites just type indices so it's possible to write
  lemmas saying how the cast function interacts with other functions
- Lemmas can extract this equality directly from the term when rewriting
Cons:
- Asymmetric
- Need to set up `cast_rfl`, `cast_cast`, etc. lemmas
-/

def castα {x₁ x₂ : α} (y : β x₁) (h : x₁ = x₂) : β x₂ := h ▸ y

variable (x₁ x₂ : α) (h : x₁ = x₂) (y₁ : β x₁) (y₂ : β x₂)

#check castα y₁ h = y₂

end

section

/-! # Use a custom equality type

Pros:
- Unlike `HEq`, remembers the index equality
- Symmetric
Cons:
- Is a "global" notion
- There's no `rw`/`simp` for rewriting with your equality type
- Need to prove rfl, symm, trans
-/

inductive Eqα : {x₁ x₂ : α} → β x₁ → β x₂ → Prop
  | rfl {x : α} (y : β x) : Eqα y y

example (x₁ x₂ : α) (y₁ : β x₁) (y₂ : β x₂) (h : Eqα y₁ y₂) : x₁ = x₂ := by
  cases h
  rfl

end

section

/-! # Use equality of sigma types

Pros:
- Unlike `HEq`, remembers the index equality.
- Avoids making a custom relation, and uses built-in types
- Sticks with equality, so `rw`/`simp` is possible
Cons:
- Is a "global" notion in that the equality is on this auxiliary sigma type
-/

abbrev mk {x : α} (y : β x) : Σ x : α, β x := ⟨x, y⟩

example (x₁ x₂ : α) (y₁ : β x₁) (y₂ : β x₂) (h : mk y₁ = mk y₂) : x₁ = x₂ :=
  congr_arg Sigma.fst h

end

section

/-! # Use HEq

Pros:
- It's a built-in relation with some tactic support.
- So long as you still keep the index equality in context, it's equivalent to the others.
- You can "rewrite" with it using `congr(...)` quotations (a mathlib syntax)
Cons:
- There is nothing tying the index equality to the HEq, so it can get lost.
- You can't `rw`/`simp` with it.
-/

example (x₁ x₂ : α) (y₁ : β x₁) (y₂ : β x₂) (h : HEq y₁ y₂) : x₁ = x₂ := by
  sorry -- Impossible

end

[Alex Meiburg]

Ah! I think congr! solves my problems nicely! I can now prove several things I couldn't previously. I should probably learn how it works, I mean, but congr generates HEq's where congr! seems better at simplifying it and getting me Eq's instead. :) I'm doing the "Sigma" approach mentioned at https://github.com/eric-wieser/lean-graded-rings/blob/cf463b1b9317e16499a51b20037ad8319311bd21/src/cicm2022/examples/graded_semigroup.lean#L42?decl=h%20:%20i+j=k.g_semigroup, but the "h : i+j=k" approach looks nice too..