Workaround for `{}` annotation in structures

Stream: lean4

[François G. Dorais]

The {} annotation has been disabled in inductive, structures and classes. I see how to work around it for inductive definitions, but I don't know how to easily work around it for structures and classes.

class Is42 (n : Nat) where
  is42 {} : n = 42

used to give Is42.is42 : ∀ (n : Nat) [self : Is42 n], n = 42.

The only way I found to reproduce the old behavior is to manually define the inductive:

class inductive Is42 (n : Nat) : Prop
| mk : n = 42 → Is42 n

def Is42.is42 (n : Nat) : [self : Is42 n] → n = 42
| mk h => h

Is there an easier way to do this?

[Leonardo de Moura]

@François G. Dorais We removed the feature because it was rarely used. All occurrences in the main repo were legacy (i.e., they are not necessary with the Lean 4 elaborator), and as far as we can tell this feature is not used in Mathlib 4. Haskell also seems to do well without having a similar feature. When removing this feature, we observed that every single existing instance looks now better without it. We are assuming that in most cases the n can be inferred from the expected type. In the rare cases where the expected type is not available, named arguments seem to be a reasonable alternative. Example:

#check Is42.is42 (n := 42)

If there are many instances where you have to use named arguments, an abbreviation is also a good solution.

abbrev Is42.is42' (n : Nat) [Is42 n] : n = 42 :=
  is42

BTW, you don't have to use class inductive. Here is the full example

class Is42 (n : Nat) where
  is42 : n = 42

instance : Is42 42 := ⟨rfl⟩

#check Is42.is42 (n := 42)

#check (Is42.is42 : 42 = 42)

abbrev Is42.is42' (n : Nat) [Is42 n] : n = 42 :=
  is42

#check Is42.is42' 42

I realize this is an artificial example to explain the problem you hit. If this comment is not useful, could you please point us to your actual development? We assumed the impact of this change would be minimal (or zero), if we are mistaken, it would be useful to see the actual use-cases where the removed feature is useful.

[François G. Dorais]

Thanks for the quick reply Leo!

I only had a couple of uses for this feature. I was never a big fan of it, so I'm not mourning the loss. I was asking in case I could reproduce the exact behavior using a macro or something.

The abbrev solution works in most cases but there is one thing that I miss. The {} annotation was smart about outParam. For example, I used generic classes for common identities as follows:

class OpRightInv (op : α → α → α) (inv : outParam (α → α)) (id : outParam α) : Prop where
  op_right_inv {} (x) : op x (inv x) = id
export OpRightInv (op_right_inv)

This automatically gives the desired signature:

op_right_inv : ∀ {α : Sort _} (op : α → α → α) {inv : α → α} {id : α} [self : OpRightInv op inv id] (x : α), op x (inv x) = id

This is really cool because I originally thought {} would also make inv and id explicit (as it does without outParam). Before I realized this, I wasn't using the {} annotation and would always specify (op:=...) since this type class needs at least this hook to trigger in most use cases. I was really happy when I noticed {} was smart about outParam. Ironically, this was just a few days before {} was dropped :disappointed:

Now, since {} was dropped, I use the abbrev trick as follows:

class OpRightInv (op : α → α → α) (inv : outParam (α → α)) (id : outParam α) : Prop where
  protected op_right_inv (x) : op x (inv x) = id
abbrev op_right_inv {α} (op : α → α → α) {inv : α → α} {id : α} [self : OpRightInv op inv id] := self.op_right_inv

This works in the same way but I have to calculate the signature by hand. This is admittedly not hard to do but {} as definitely more convenient. I'll eventually make a macro to automate this but this works fine for now.

[Sebastian Ullrich]

A little shorter:

abbrev op_right_inv {α} (op) := @OpRightInv.op_right_inv (α := α) (op := op)

[François G. Dorais]

Thanks Sebastian!

I was thinking about how to make this into a macro, but I'm still pretty clumsy at macro writing. What's the idiomatic way to handle binders? Ideally, I would like a macro that expands something like

identity op_right_inv (op : α → α → α) {inv : α → α} {id : α} (x) : op x (inv x) = id

into

class OpRightInv (op : α → α → α) (inv : outParam (α → α)) (id : outParam α) : Prop where
  protected op_right_inv (x) : op x (inv x) = id
abbrev op_right_inv (op : α → α → α) {inv : α → α} {id : α} [self : OpRightInv op inv id] := self.op_right_inv

[François G. Dorais]

I'm starting to think a macro is not the right idea for this.

[François G. Dorais]

@Leonardo de Moura: I've found another pattern where I used {}. These are classes that attempt to extract a normal form for objects that aren't of inductive type. My primary uses for these is to synthesize homomorphisms from a free algebra into a real-world algebra.

For illustration, here is a simple but complete example. Here the free algebra is a List monoid and the real-world algebra is Prop with And and True. (This is the version with {} for the new version, delete that annotation and replace all_eq x with all_eq (p:=x) where necessary.)

protected theorem And.assoc (p q r : Prop) : ((p ∧ q) ∧ r) = (p ∧ (q ∧ r)) :=
  propext ⟨λ| ⟨⟨hp,hq⟩,hr⟩ => ⟨hp,⟨hq,hr⟩⟩, λ| ⟨hp,⟨hq,hr⟩⟩ => ⟨⟨hp,hq⟩,hr⟩⟩

def All : List Prop → Prop
| [] => True
| p::ps => p ∧ All ps

protected theorem All.nil : All [] = True := by simp [All]

protected theorem All.single (p : Prop) : All [p] = p := by simp [All]

protected theorem All.append : (ps qs : List Prop) → All (ps ++ qs) = (All ps ∧ All qs)
| [], qs => by simp [All]
| p::ps, qs => by simp [All, And.assoc, All.append ps qs]

class AssocAnds (p : Prop) where
  list : List Prop
  all_eq {} : All list = p

namespace AssocAnds

@[simp] instance (prio:=low) (p : Prop) : AssocAnds p where
  list := [p]
  all_eq := All.single p

@[simp] instance : AssocAnds True where
  list := []
  all_eq := All.nil

@[simp] instance (p q : Prop) [AssocAnds p] [AssocAnds q] : LiftAnds (p ∧ q) where
  list := list p ++ list q
  all_eq := by rw [All.append, all_eq p, all_eq q]

end AssocAnds

This example is not that useful since we can use simp only [And.assoc] to similar effect. Not quite though, since simp works bottom-up whereas AssocAnds works top-down and stops as soon as it hits a snag. Of course, there are more sophisticated examples of this pattern where simp isn't a viable alternative.

In any case, the point is that AssocAnds.all_eq is not very useful with the parameter p as implicit. This was fixed by the {} annotation, now I must use (p:=...) in the majority use cases (e.g. all backwards rewrites). Adding an abbrev works too but {} was really the most convenient thing to have.

Bottom line, the {} annotation was actually useful for fields in classes and structures (but not necessarily for other uses). I would really appreciate bringing it back for this use or providing an equivalent alternative. This is pretty low priority for me, so no rush! (I also won't be heartbroken if you decide not to bring this feature back.)

[Leonardo de Moura]

For the new version, delete that annotation and replace all_eq x with all_eq (p:=x) where necessary.)

It works for me without any annotation. That is, I did not have to write (p := x). BTW, this was also our experience in other cases.

In any case, the point is that AssocAnds.all_eq is not very useful with the parameter p as implicit.

Do you have other examples where the parameter (p := x) is needed? I could remove all instances from your example.

Here is your example without extra annotations.

protected theorem And.assoc (p q r : Prop) : ((p ∧ q) ∧ r) = (p ∧ (q ∧ r)) :=
  propext ⟨λ| ⟨⟨hp,hq⟩,hr⟩ => ⟨hp,⟨hq,hr⟩⟩, λ| ⟨hp,⟨hq,hr⟩⟩ => ⟨⟨hp,hq⟩,hr⟩⟩

def All : List Prop → Prop
| [] => True
| p::ps => p ∧ All ps

protected theorem All.nil : All [] = True := by simp [All]

protected theorem All.single (p : Prop) : All [p] = p := by simp [All]

protected theorem All.append : (ps qs : List Prop) → All (ps ++ qs) = (All ps ∧ All qs)
| [], qs => by simp [All]
| p::ps, qs => by simp [All, And.assoc, All.append ps qs]

class AssocAnds (p : Prop) where
  list : List Prop
  all_eq : All list = p

namespace AssocAnds

@[simp] instance (prio:=low) (p : Prop) : AssocAnds p where
  list := [p]
  all_eq := All.single p

@[simp] instance : AssocAnds True where
  list := []
  all_eq := All.nil

@[simp] instance (p q : Prop) [AssocAnds p] [AssocAnds q] : AssocAnds (p ∧ q) where
  list := list p ++ list q
  all_eq := by rw [All.append, all_eq, all_eq]

-- Same `instance` with `simp`
@[simp] instance (p q : Prop) [AssocAnds p] [AssocAnds q] : AssocAnds (p ∧ q) where
  list := list p ++ list q
  all_eq := by simp [All.append, all_eq]

end AssocAnds

[François G. Dorais]

You're right! I gutted too much and should have left some sample uses of the class...

The issue is with backwards rewrites rw [←all_eq p]. These don't work without the parameter. These are the most common when using these classes since we usually have the real world term p and we want to lift to the free algebra, which is list in this case. The free algebra is usually some inductive type or similar, so there's more tools to work with there than with the plain term p.

[Leonardo de Moura]

Could you please paste here this use case?

[François G. Dorais]

To avoid more errors gutting stuff, I've moved two full examples from a private to a public repo on github:

• Semigroup.reflect:

theorem reflect {α} (s : SemigroupSig α) [Semigroup s] (xs : List α) {a b : α} [Reflect s a xs] [Reflect s b xs] : Reflect.expr s a (xs:=xs) = Reflect.expr s b (xs:=xs) → a = b := by
  intro h
  rw [← Reflect.eval_eq (s:=s) (x:=a) (xs:=xs), ← Reflect.eval_eq (s:=s) (x:=b) (xs:=xs), h]

• Monoid.reflect:

theorem reflect {α} (s : MonoidSig α) [Monoid s] (xs : List α) {a b : α} [Reflect s a xs] [Reflect s b xs] : Reflect.expr s a (xs:=xs) = Reflect.expr s b (xs:=xs) → a = b := by
  intro h
  rw [←Reflect.eval_eq (s:=s) (x:=a) (xs:=xs), ←Reflect.eval_eq (s:=s) (x:=b) (xs:=xs), h]

[François G. Dorais]

In both cases, the original implementation used {} at both Reflect.expr and Reflect.eval_eq.

[Leonardo de Moura]

@François G. Dorais Thanks for sharing the example. I didn't install it on my machine yet, but I browsed the sources.
I think they do not make a compelling case for adding {} back. Even if we do it, every example you had would still require the ←. It feels natural to manually define an abbreviation eq_eval in this case that uses the explicit binder annotations and flips the equation. Then, you will be able to write

theorem reflect {α} (s : SemigroupSig α) [Semigroup s] (xs : List α) {a b : α} [Reflect s a xs] [Reflect s b xs] : Reflect.expr s a (xs:=xs) = Reflect.expr s b (xs:=xs) → a = b := by
  intro h
  rw [eq_eval s  a xs, eq_eval s b xs, h]

[François G. Dorais]

OK. I can live with that. The issue with Reflect.expr is a bit more nagging. But it only ever needs just the (xs:=...) so I won't do a wrapper for that one.

[Henrik Böving]

I got another question regarding this. I implemented the slim check port for mathlib4 and it contains a typeclass:

class SampleableExt (α : Sort u) where
  proxy {} : Type v
  [proxyRepr : Repr proxy]
  [shrink : Shrinkable proxy]
  sample {} : Gen proxy
  interp : proxy → α

where I now have to remove the {} in order to get my type fixed, howver both fields dont allow the lean compiler to infer the alpha parameter over which the type class is actually declared so where I could previously write:

        let n ← sample Nat
        pure $ Char.ofNat n

I now have to write

        let n ← sample
        pure $ Char.ofNat n

which the lean compiler cannot infer:

application type mismatch
  Char.ofNat n
argument
  n
has type
  proxy ?m.9290 : Type
but is expected to have type
  ℕ : Type

What's the recommended way to address this use case? Have a manual wrapper as well?