naming hypotheses when using do-notation

Stream: lean4

[Jonathan Protzenko]

I looked into the documentation (doc/do.md) but I didn't find anything... still using fact as my running example, consider the two styles below:

def checked_sub (n: Nat) (m: Nat): Option Nat :=
  if n >= m then
    some (n - m)
  else
    none

def fact3 (x: Nat): Option Nat :=
  if x = 0 then
    return 1
  else
    do
      let y <- checked_sub x 1
      fact3 y
termination_by fact3 x => x
decreasing_by
  simp_wf
  sorry

def fact4 (x: Nat): Option Nat :=
  if x = 0 then
    return 1
  else
    match h:checked_sub x 1 with
    | some y =>
      fact4 y
    | none =>
      none
termination_by fact4 x => x
decreasing_by
  simp_wf
  sorry

I am now in a monad (this is obviously a simplified version of what I'm trying to achieve)... the recursion is not really relevant to this example

for fact4, I have a hypothesis h: checked_sub x 1 = some y in my context (after simp_wf), but for fact3, I don't have that crucial bit of information in my context

is there any way to bind the hypothesis when using do <- notation?

[Sebastian Ullrich]

Hi Jonathan! I don't see how this could work for an arbitrary monad. But for specific cases like Option we can transfer the hypothesis inside a subtype.

def Option.attach : (o : Option α) → Option { x : α // o = some x }
  | .some x => .some ⟨x, rfl⟩
  | .none   => .none

...      let ⟨y, hy⟩ <- checked_sub x 1 |>.attach

[Jonathan Protzenko]

hey Sebastian! ok, this is nice -- I had gone that route (@Son Ho's suggestion) but eventually realized that the refinement prevented the operator from satisfying the signature of the Bind typeclass... but your solution is nice and compact... maybe I could even define a custom operator (<--) that combines both in one go, but I don't know yet how to do that... thanks!

[Sebastian Ullrich]

Oh yes, you can do something like

macro "let" h:ident " : " e:term " <-- " f:term : doElem =>
  `(doElem| let ⟨$e, $h⟩ ← Option.attach $f)

...       let hy : y <-- checked_sub x 1

and then optionally abstract attach into a typeclass

[Jonathan Protzenko]

ah that's excellent, thanks so much Sebastian!

[Jonathan Protzenko]

actually I'm reviving this thread... I finally got around to using this in real code, but then I have an universes issue:

def checked_sub (n: USize) (m: USize): Option USize :=
  sorry

def Option.attach : (o : Option α) → Option { x : α // o = some x }
| .some x => .some ⟨x, rfl⟩
| .none   => .none

def termination (T : Type) (key : USize) (v: T) :=
  (key, v)

def foo (T: Type) (k: USize) (v: T) : Option USize :=
  if h: k = 0 then
    .some 0
  else do
    let k <- checked_sub k (USize.ofNatCore 1 (by
      match USize.size, usize_size_eq with
      | _, Or.inl rfl => decide
      | _, Or.inr rfl => decide))
    let ⟨ k, h ⟩ <- foo T k v |> Option.attach
    .some k
termination_by foo T k v => termination T k v
decreasing_by sorry

here, the termination measure is rejected, on the basis that:

type mismatch
  termination T k v
has type
  USize × T : Type
but is expected to have type
  ?β : Sort ?u.9354

bear in mind that this code is auto-generated, so the termination measure always, by default, contains a tuple of all the arguments

[Jonathan Protzenko]

this is of course a minimal repro, the actual use-case is more involved, but this is the gist of the issue

[Jonathan Protzenko]

if I get rid of the option.attach and the h, then all goes well

[Jonathan Protzenko]

so I don't understand why this particular usage gives rise to a universe problem

[Mario Carneiro]

that is a strange error message, since the type should unify with that target type

[Mario Carneiro]

the only thing I can think is that one of those metavariables is not assignable at the current mvar depth, or is not allowed to reference those local variables or something along those lines

[Mario Carneiro]

or else the error message is just lying

[Mario Carneiro]

do you have an MWE not using intlit?

[Jonathan Protzenko]

oh sorry yes of course

[Jonathan Protzenko]

I thought it was self-contained

[Mario Carneiro]

sorry seems to work to reproduce

[Jonathan Protzenko]

ok glad to know you were able to reproduce

[Mario Carneiro]

using (k, v) directly causes a similar error message:

termination_by foo T k v => (k, v)

application type mismatch
  (k, v)
argument
  v
has type
  T : Type
but is expected to have type
  ?m.864 : Type ?u.859

which makes me think that it is indeed an issue of the metavariable not being allowed to reference T

[Mario Carneiro]

This probably warrants a bug report, but you can likely work around it by using termination_by' instead

[Mario Carneiro]

although, in this example how do you intend to prove termination? T is an arbitrary type, you don't have a well founded instance on it

[Mario Carneiro]

For this particular example, I guess you don't want v to participate in the well founded measure

[Jonathan Protzenko]

this is just to demonstrate the issue, in this example, I could conceivably show that the first argument of the pair is always decreasing, I guess

[Jonathan Protzenko]

thanks, I'll file an issue on the bug tracker

[Mario Carneiro]

I mean that in general, it doesn't make sense to have v in there because T is a generic argument. You would have to change the type of the function foo to add a well founded measure

[Jonathan Protzenko]

do you mean that if v appears in the termination_by, then there is no hope of proving termination, even though the first argument is decreasing?

[Mario Carneiro]

I mean that there is no hope of making the termination hint typecheck, because even after you get past the current error message there is a secondary goal (solved by typeclass inference) to find an instance of WellFoundedRelation for the type of the expression you gave (here USize x T)

[Mario Carneiro]

and that will definitely fail because there is no instance of WellFoundedRelation T in the context

[Mario Carneiro]

furthermore, if you fix this issue by not including variables with generic types in the tuple, then the current issue will also go away

[Mario Carneiro]

An alternative way to solve that issue would be to change the type of foo to

def foo (T: Type) [WellFoundedRelation T] (k: USize) (v: T) : Option USize :=

at which point arguably it should work to use (k, v) as the termination hint, and this is what I regard as the bug in this case

[Mario Carneiro]

Lean is supposed to be doing some preprocessing to determine the arguments that don't change in the recursion (here both T and v would be eligible) and excluding them from the termination context, so that the goal becomes T, v |- WellFounded USize instead of |- WellFoundedRelation ((T : Type) ×' (_ : USize) ×' T) (which is more awkward to work with). Specifically, I believe termination_by is trying to use invImage (fun (T, k, v) => <your hint>) _ as the termination relation, and this is a problem because the type of <your hint> cannot depend on T,k,v here since docs4#invImage requires a non-dependent function

[Mario Carneiro]

If you use termination_by' you can take the construction of the termination relation into your own hands, which will likely lead to more stable behavior compared to termination_by's heuristics

[Mario Carneiro]

BTW, if your termination hint is just the tuple of everything I think you can leave it off, since that's the default

[Jonathan Protzenko]

thanks, in my case I do expect and anticipate that the user will refine the termination measure -- the termination definition is in a separate file that is not auto-generated and that the user will have to provide... Aeneas currently generates a "template" where the default termination measure is a tuple of all the arguments, and the termination proof is just sorry -- the user takes that template as a base, then replaces the definitions

[Jonathan Protzenko]

so it's just a confusing error message for the default measure that in any case would not have worked anyhow

[Mario Carneiro]

Note that lean's actual default does not suffer from this issue, if you use decreasing_by sorry alone you can see in the input tactic states some references to

invImage (fun a => PSigma.casesOn a fun T snd => PSigma.casesOn snd fun x snd => sizeOf x) instWellFoundedRelation

which is to say, lean is using the equivalent of termination_by T k v => sizeOf k

[Jonathan Protzenko]

I made progress, but I'm still getting errors... thanks for your patience as I try to work this out

def Option.attach {α: Type} (o : Option α): Option { x : α // o = .some x } :=
  match o with
  | .some x => .some ⟨x, rfl⟩
  | .none => .none

def f
  (T : Type) (ls : List T) :
  (Option (List T))
  :=
  match ls with
  | .cons _ tl =>
      do
        have h: List.length tl < List.length ls := by sorry
        let ⟨ tl0, h ⟩ <- f T tl |> Option.attach
        .none
  | .nil =>
    .none
termination_by f ls => List.length ls

here, notice that I have gotten rid of all of the decreases_by business, and I'm merely trying to get the termination proof to work out in the style you suggested (with a have right before the recursive call)

I thought this would work, but I'm getting:

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
tl: List T✝
h: List.length tl < List.length ls✝
ls: List T
⊢ List.length ls < Nat.succ (List.length tl)

if I replace ⟨ tl0, h ⟩ with x, then this succeeds...

[Jonathan Protzenko]

the other thing I'm noticing as I look back at this: I'm not even sure how the proof is supposed to succeed... this goal is really confusing

[James Gallicchio]

It's also fixed if you move the recursive call outside the do notation :joy: this seems to be one of those places where do notation destroys all evidence of where values come from

[James Gallicchio]

let me see if i can make a simple MWE to show why...

[James Gallicchio]

oh dear, I am quite confused. somewhat simpler MWE:

-- this works
def g (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      let res := g T tl
      res |> Option.attach |>.bind fun ⟨x,h⟩ => x
  | [] => .none

-- this does not
def g' (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      g' T tl |> Option.attach |>.bind fun ⟨x,h⟩ => x
  | [] => .none

[James Gallicchio]

maybe one of the elaboration experts can give some insight here ???

[James Gallicchio]

I suspect it has something to do with the fact that g' T tl appears in the type of Option.attach res, which breaks (?) the structural induction??

[Jonathan Protzenko]

nice repro, thanks!

[James Gallicchio]

ooh, even more strange:

-- works
def g' (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      let res := Option.attach (g' T tl)
      res.bind fun x => x.val
  | [] => .none

-- doesn't
def g'' (T : Type) (ls : List T) : (Option (List T)) :=
  match ls with
  | _::tl =>
      let res := Option.attach (g'' T tl)
      res.bind fun ⟨x,h⟩ => x
  | [] => .none

[Jonathan Protzenko]

this matches what I observed earlier, which it is the unpacking of the subtype via the \langle, \rangle that causes the error

[James Gallicchio]

I had thought it was unrelated :D I was wrong

[Jonathan Protzenko]

so I'm wondering if having very dependently-typed hypotheses in the context is somehow leading to a poor unification choice (e.g. with variables that later on would escape their scope), and thus ultimately to a failure

[Mario Carneiro]

This is a bug for sure. I assume it has something to do with the fact that match generates a matcher function which generalizes over a bunch of things in the context, and it might be picking g'' itself as one of the things to generalize, meaning that the call to fun ⟨x,h⟩ => x (which macro expands to fun x => match x with | ⟨x,h⟩ => x) turns into something like fun x => g''._match g'' T tl res x and now g'' is being passed unapplied to a helper function and this is no longer structurally recursive

[Jonathan Protzenko]

thanks, I filed a bug https://github.com/leanprover/lean4/issues/2102

[Jonathan Protzenko]

So far, with everyone's help, I have a workaround for all of the issues above (notably, introducing extra let-bindings to defeat issue #2102)... but I am now hitting performance problems (which surfaced via errors referring to "heartbeats", as I mentioned in another thread). Here's a succinct description of the issue: if my definition uses the <- monadic bind operator, it is type-checked instantly and the interactive mode returns to me in a snap, but if I use the <-- (see above, the one that pipes the result through Result.attach), I need to multiply max heartbeats by 10 and the definition type-checks in a little under 3 minutes. This is a closed term, so in theory, it should be able to reduce in a call-by-value, efficient fashion, but clearly, it's not happening here.

I could not reproduce the issue with Option, so unfortunately the repro involves cloning the Aeneas repo...

Here's what I tried:

• I traced Compiler.simp to see what was happening with reduction, and I did see that with my special <-- operator, there were a lot of packing / unpackings of Subtype
• interestingly, the elaboration seems to "figure out" that with <-, some monadic let-bindings had no dependency upon a lot of earlier variables, and thus could be hoisted, this did not seem to happen with the <-- version
• I tried to reproduce with Option.bind, to no avail, so I looked up the definition of Option.bind, and I noticed that it was marked as @[inline], so I marked my own Result.attach and Result.bind as @[inline]
• with the fix above, I was able to see that eventually, the <- version (fast) and the <-- version (slow) reduce to the same term (size: 132), but I don't seem to have access to the intermediary states of reduction (the output is trimmed to the most recent few messages)

in case anyone has the good will and time to take a look, the repro is here: https://github.com/AeneasVerif/aeneas/blob/8a986a9c61e62ad3cc1955a71e3c14de00411f60/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean#L558-L632, the repository should be clone-able easily, and it suffices to open this file in an editor to witness the issue (or run lake build on the command-line)

[Jonathan Protzenko]

my closed term is not huge, so I'm wondering if the presence of hypotheses triggers a bad complexity somewhere... but I don't have enough expertise to figure out what it might be