Coerce value into trivial subtype

Stream: lean4

[Somo S.]

How do I "coerce" a value into a subtype wherever the predicated property is trivially provable?

So for example, assuming we can prove that "racecar" is a palindrome by simp, I would like to just declare it directly as a value of palindrome subtype like so:

def good:  MySubtype ( fun x =>  (String.reverse x)=x ) := "racecar"

instead of:

def bad:  Subtype ( fun x =>  (String.reverse x)=x ) := {val:="racecar", property:=(by simp)}

The best I have been able to do is just reduce it to (better but not ideal) terser notation like so:

-- "§"  symbol wraps the str up into the verbosity above
def meh:  MySubtype ( fun x =>  (String.reverse x)=x ) := §"racecar"

[Scott Morrison]

Would you be happy with := { val := "racecar" }? For that you can just use an auto_param.

structure P where
  v : ℕ
  p : True := by trivial

example : P := { v := 0 }

Unfortunately you can't write example : P := ⟨0⟩ here.

[Somo S.]

@Scott Morrison said:

Would you be happy with := { val := "racecar" }?

Unfortunately you can't write example : P := ⟨0⟩ here.

No I did explore both of those options. I would ideally like to reduce the extra boilerplate down to exactly 0 extra characters.

[Somo S.]

This type of thing already works with Fin. So with Fin you can simply just say:

example : Fin 5 := 2

instead of:

example : Fin 5 := Fin.mk 2 (by simp)
-- OR
example : Fin 5 := {val:=3, isLt:=by simp}

Is there any inspiration that can be drawn from the OfNat code that makes Fin work nicely in this way?

[Reid Barton]

It actually doesn't work quite that way --

example : Fin 5 := 7

[Somo S.]

@Reid Barton said:

It actually doesn't work quite that way --

Thanks I forgot about that it has a mod based definition. Ok so is there a way to make it work so that it passes when it can be trivially proven and otherwise it fails; all without defining any new notation?

[Kevin Buzzard]

Numerals are a special case but what's happening there is a coercion and, as Reid pointed out, no proof needs to be supplied, so it doesn't apply to your situation.

[Notification Bot]

A message was moved here from #lean4 > Coerce value into trivial subtype by Somo S..

[Somo S.]

Sorry ignore this thread in favor of https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Coerce.20value.20into.20trivial.20subtype

... I was only trying to rename the above

[Notification Bot]

Somo S. has marked this topic as resolved.

[Somo S.]

Somo S. said:

How do I "coerce" a value into a subtype wherever the predicated property is trivially provable?

So for example, assuming we can prove that "racecar" is a palindrome by simp, I would like to just declare it directly as a value of palindrome subtype like so:

def good:  MySubtype ( fun x =>  (String.reverse x)=x ) := "racecar"

instead of:

def bad:  Subtype ( fun x =>  (String.reverse x)=x ) := {val:="racecar", property:=(by simp)}

The best I have been able to do is just reduce it to (better but not ideal) terser notation like so:

-- "§"  symbol wraps the str up into the verbosity above
def meh:  MySubtype ( fun x =>  (String.reverse x)=x ) := §"racecar"

@@role:moderators I have lost the original post for this thread while attempting to merely edit the title to that of <https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Try.20to.20convert.20value.20into.20trivial.20subtype> .. for some reason it created a new topic instead of merely changing the title of this one.. Kindly assist in restoring my original post that contained the original question

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

I've glued the threads back together

[Scott Morrison]

Note this this was easier in lean3, where the ⟨0⟩ notation would have worked: in lean3 anonymous constructor notation made use of auto_param, although not of default values. In lean4, anonymous constructor notation uses neither.

See https://github.com/leanprover-community/mathlib4/issues/4998

[Mario Carneiro]

shouldn't that issue be on lean4 repo?

[Scott Morrison]

Well, I'm not sure that it's actually a bug report! In neither lean3 nor lean4 does anonymous constructor notation make use of default values. The change between lean3 and lean4 is just the auto_params have become a special case of default values. So it may well be "expected behaviour".

[Scott Morrison]

I made this issue mostly to illustrate what I was hoping we could start doing with porting notes --- have some place to link to that gives an explanation for classes of porting notes.