Data.Real.CauSeq (mathlib4#1124)

Stream: mathlib4

[Eric Wieser]

It looks like this PR has run into a misport between docs#is_absolute_value.abv_add and docs4#IsAbsoluteValue abv_add; the former takes abv as an explicit argument, but the port takes it as an implicit argument

[Eric Wieser]

I think this is caused by the []s in

class is_absolute_value {S} [ordered_semiring S]
  {R} [semiring R] (f : R → S) : Prop :=
(abv_nonneg [] : ∀ x, 0 ≤ f x)
(abv_eq_zero [] : ∀ {x}, f x = 0 ↔ x = 0)
(abv_add [] : ∀ x y, f (x + y) ≤ f x + f y)
(abv_mul [] : ∀ x y, f (x * y) = f x * f y)

has the Lean4 equivalent of these been discussed elsewhere?

[Eric Rodriguez]

people have just been priming and making separate methods

[Eric Rodriguez]

the feature is obviously got a weird syntax in lean3 but removing it in lean4 isn't the way either I don't think

[Eric Rodriguez]

see docs4#Countable

[Yaël Dillies]

Yeah, I liked this feature, so it's a bit sad to see it gone without replacement.

[Eric Wieser]

At any rate, it sounds like the interim solution is to add the primed lemmas; or better yet, for mathport to generate them

[Reid Barton]

I think this specific [] mode was a feature added in the community lean version (a practice which always seemed a bit dubious to me, with the port on the horizon).

[Moritz Doll]

I've made a PR to have the function argument explicit: mathlib4#1398
I think the [] feature is nice (the syntax is unintuitive IMO), but it seems to be not used a lot in mathlib and I haven't heard of it before porting IsAbsoluteValue. In general it would be nice to have Lean 4 features to remove all of the boilerplate-y foo' fields. For the coercion this should be taken care of by elaboration of coercions (though I am not completely sure of it, since we have the FunLike weirdness).

[Moritz Doll]

Sorry for the delay, I needed a few days to recover from the vacation.

[Eric Wieser]

In the porting meeting call I suggested that maybe we don't even need a replacement for [], and better heuristics for argument explicitness (i.e. do the right thing automatically) would suffice.

[Eric Wieser]

Either way, your PR is definitely the best short -term solution!