Refine type

Stream: lean4

[eduardo]

I'm trying to encode refinement types through evidence, like NonEmptyString; I've found an older conversation with an example, but simp is not solving the goal.

https://leanprover-community.github.io/archive/stream/270676-lean4/topic/newtype.html

The closest result I've reached is this one.

structure NonEmptyString where
  value : String
  ev : value.length > 0
deriving Repr

def mkNonEmptyString (s : String) (ev : s.length > 0) : NonEmptyString :=
  { value := s, ev := ev }

def eg : NonEmptyString :=
  mkNonEmptyString "hello" (by decide)

Is it possible to pin a tactic into mkNonEmptyString and avoid applying it manually in the callers?

[Chris Bailey]

Indeed it is.

def mkNonEmptyString (s : String) (ev : s.length > 0 := by decide) : NonEmptyString :=
  { value := s, ev := ev }

def eg : NonEmptyString :=
  mkNonEmptyString "hello"

[eduardo]

Thank you, Chris!

[eduardo]

Can I take this opportunity to ask you what the semantic difference is between defining the evidence in the signature instead of within the function? I saw some examples, but they don't work (at least for this tactic).

def mkNonEmptyString (s : String) : NonEmptyString :=
 let ev : s.length > 0 := by decide
 { value := s, ev := ev }

[Eric Wieser]

def mkNonEmptyString (s : String) : NonEmptyString := amounts to claiming that all strings are non-empty, which is obviously false!

[Eric Wieser]

(ev : s.length > 0 := by decide) is a hint to the caller; it's a regular argument, but if the caller omits it asmkNonEmptyString "hello" then it is elaborated as mkNonEmptyString "hello" (by decide)

[eduardo]

Thank you, Eric!

[Chris Bailey]

If it helps, that syntax (a : A := ..) is generic syntax for an optional argument, it just happens to work with proofs (and proofs via tactic):

def foo (a : Nat) (b : Nat := 0) : Nat := a + b

#eval foo 10     -- 10
#eval foo 10 5   -- 15

[Markus Schmaus]

You can also provide a default when defining structure, and you don't need to define an extra mkNoneEmptyString, since NonEmptyString.mk already exists. With this your example becomes:

structure NonEmptyString where
  value : String
  ev : value.length > 0 := by decide
deriving Repr

def eg : NonEmptyString :=
  NonEmptyString.mk "hello"

[eduardo]

Hmm, it seems https://leanprover-community.github.io/archive/stream/270676-lean4/topic/newtype.html is correct except for the tactic; it wasn't clear to me if we were allowed to have default tactics at the structure declaration level. The compiler generates the mk I was looking for. Thank you, Marcus!