Default values for proof arguments in subtype's

Stream: general

[Ayhon]

I was wondering how to implement something like giving a default tactic to run to when instantiating a Subtype. My imagined syntax would be something like

abbrev A(n: Nat) := {x: Nat // 0 < x /\ x < n := by omega}

def foo(n: Nat)(x: A n): A n := A.mk (n - x)

In this case, the n - x would resolve the property by executing omega on its second argument.

I gave a try to implementing this as a macro (extending the already existing {$x // $p}), but ran into issues with how to model this. I imagine that as it is not something one is able to do currently, although I don't really understand how tactics as default arguments behave in Lean precisely, so perhaps there's a way to hack it together? Otherwise, I guess this is more of a feature request, or a thought experiment.

[Andrew Yang]

Is this good enough?

abbrev A (n: Nat) := {x : Nat // 0 < x ∧ x < n }
def A.mk {n : Nat} (k : Nat) (hk : 0 < k ∧ k < n := by omega) : A n := ⟨k, hk⟩
def foo (n : Nat) (x : A n) : A n := A.mk (n - x)

[Ayhon]

That would work, but admittedly I was thinking about it more as a "I could use this to specialize arguments passed to functions". I guess a more proper example would be something like this.

def foo(n: Nat)(x: {x: Nat // 0 < x /\ x < n := by omega}): Nat := sorry
example: Nat := foo 10 5

This is kind of the behaviour one has for Fin, which can be seen as Fin n = {x : Nat // x < n}, but since it has a specialized coe from Nat, then it works.

[Andrew Yang]

Do you need it to be a subtype or can you manage with foo (n : Nat) (x : Nat) (foo : 0 < x ∧ x < n := by omega)?

[Ayhon]

Hmm, it might be as simple as that. Let me test it a bit further for the purpose I had in mind

[Ayhon]

In a sense you're just currying the product. But then it doesn't work for return types. This might not be something I actually care about though

[Ayhon]

Hmm, it works quite well, but if I don't have the tactic script include something like assumption then I have to carry the conditions around in subsequent calls

[Ayhon]

That is, if I have something like

def fib(n: Nat)(x: Nat)(n_hypot: 0 < n /\ n < w := by decide) :=
  if x <= 1 then x else fib n (x-1) n_hypot + fib n (x-2) n_hypot

then I have to mention n_hypot again and again when doing the recursive calls.

Admittedly it's not a great example. Perhaps I can work out something better with Vector.

[Ayhon]

I think this example may make a bit more sense

def Int.relu(x: Int): if x < 0 then 0 else x
def Vector.relu(n: Nat)(arr: Vector Int n)(i: Nat)(n_hypot: n % 8 = 0 := by decide) :=
  if i_idx: i < n then
    arr.set i (arr[i].relu) i_idx
  else
    arr

One could also imagine that n_hypot is used to ensure that in the body of Vector.relu we can process elements in chunks of 8.

And by having n_hypot populated by decide, I could then call Vector.relu with n set to a number literal, and have decide check whether that literal is a multiple of 8 or not

[Ayhon]

Also, even if we discard the problems with recursivity, when decoupling the property from the type I need to put the argument at the end of the argument list. But if my function is returning another function, this breaks the currying. And one cannot have default values in implicit arguments (at least it keeps giving me errors).

That is, if I have something like

def foo(n: Nat)(n_hypot: 0 < n := by omega) := n.add
#eval foo 10 10 -- numerals are data in Lean, but the expected type is a proposition (0 < 10 : Prop)

[Ayhon]

Nah, I guess what I wanted to have is something like this

structure MyNat where
  val: Nat
  prop: val % 8 = 0 := by omega
instance: Coe MyNat Nat where coe := MyNat.val
instance: OfNat MyNat n where ofNat := MyNat.mk n

def Int.relu(x: Int): Int := if x < 0 then 0 else x
def Vector.relu(n: MyNat)(arr: Vector Int n)(i: Nat):=
  if i_idx: i < n then
    arr.set i (arr[i].relu) i_idx
  else
    arr

#eval #v[-1, -1, 1, 1, -1, -1, 1, -1].relu 8 0

The problem with this is that the OfNat instance doesn't work since I cannot defer the execution of the tactic in the default value of property until it is called with a specific value.

[Ayhon]

The only way I can conceive to achieve this is by using a macro when calling relu, which would execute the tactic and pass the proof term under the hood, similar to how GetElem works with the v[i] syntax (v[i] → GetElem.getElem v i (by get_elem_tactic), or something like that)