Equivalent of "Program Definition" in Coq

Stream: new members

[Youngju Song]

Let us say I have the following code:

def myfunc (xs ys: List Nat): IO (List Nat) := do
  assert!(xs.length = ys.length)
  let mut res := nil
  for i in [0:xs.length] do
    res := (xs[i]! + ys[i]!) :: res
  return res

and I want to replace xs[i]! with xs[i] by providing proper proofs, thereby reducing the possibility of runtime failure.
In Coq, I could try using "Program Definition" keyword, where you can leave the proofs as blanks _ and later provide the proof once the definition is over. Is there similar functionality in Lean4?

[nrs]

You may use the partial def keyword to ignore termination proofs and sorry to provide placeholders for proofs

[nrs]

If you meant tactics that create goals according to how many holes you have in your proof, you might be interested in refine

[Matt Diamond]

you can also add the proofs as have assumptions within the function... that will suffice for xs[i] to work

[Matt Diamond]

import Mathlib

def myfunc (xs ys: List Nat): IO (List Nat) := do
  assert!(xs.length = ys.length)
  let mut res := []
  for i in [0:xs.length] do
    have : i < xs.length := sorry
    have : i < ys.length := sorry
    res := (xs[i] + ys[i]) :: res
  return res

[Matt Diamond]

I'm intrigued by the use of assert! though... it would be cool if that added proof assumptions, but it doesn't appear to

[Matt Diamond]

if it did then you could do something neat like this:

import Mathlib

def myfunc (xs ys: List Nat): IO (List Nat) := do
  assert!(xs.length = ys.length)
  let mut res := []
  for i in List.finRange xs.length do
    have : i < ys.length := my_assert_proof ▸ (Fin.is_lt _)
    res := (xs[i] + ys[i]) :: res
  return res

[Matt Diamond]

also it goes without saying that you could define the function so that the caller has to pass in a proof of xs.length = ys.length

[Youngju Song]

@nrs @Matt Diamond Thank you for the reply!
What Matt wrote is close to what I want. Coq's "Program Definition" does that for the user. It would be ideal if something like the following works, which uses xs[i]'h notation for providing the proof h, but it is left as a blank in the definition time and gets resolved separately (so that it doesn't corrupt the readability of the definition) in the Next Obligation block below.

def myfunc (xs ys: List Nat): IO (List Nat) := do
  assert!(xs.length = ys.length)
  let mut res := []
  for i in [0:xs.length] do
    res := (xs[i]'_ + ys[i]'_) :: res
  return res
Next Obligation.
-- proof obligation for the first occurrence of `_`.
Qed.
Next Obligation.
-- proof obligation for the second occurrence of `_`.
Qed.

Btw, what is the ▸ notation? Is it the same as |> ?

[Matt Diamond]

▸ is a macro built on top of Eq.rec and Eq.symm... it's just a shorthand for rewriting based on an equality

[Matt Diamond]

so in my example I was saying that if we had a proof of xs.length = ys.length we could use it to rewrite i < xs.length to i < ys.length

[nrs]

If the obligations are of significant size, it is in my experience idiomatic in Lean to create new theorem or lemma declarations that specifically provide these proofs (or that provide the statement of the proofs followed by := sorry). If the proof obligations are small, you may explicitly write metavariables ?myVar, ?foo in place of the holes, and this will make them appear as new goals. The refine tactic is a small variation of this workflow where all the holes can be placed in a single function, or you can use Matt's suggested have keywords. suffices is also worth looking into for managing these workflows

[Youngju Song]

@Matt Diamond Thank you for the explanation!

[Youngju Song]

@nrs Thank you for the reply! I am not sure I fully follow your explanation though. (1) Does "sorry" allow one to provide the proof latter? What would be the syntax for doing this? (2) I tried to use metavariables as you suggested, but not sure how to make it work - it gives me a syntax error (4.15.0-rc1). Would you mind providing a minimal code snippet that I can copy-paste and play with?

[nrs]

def myfunc (xs ys: List Nat): IO (List Nat) := do
  assert!(xs.length = ys.length)
  let mut res := .nil
  for i in [0:xs.length] do
    res := (xs[i]'sorry + ys[i]'sorry) :: res
  return res

def myfunc' (xs ys: List Nat): IO (List Nat) := do
  assert!(xs.length = ys.length)
  let mut res := .nil
  for i in [0:xs.length] do
    res := (xs[i]'(p i) + ys[i]'(q i)) :: res
  return res
where
  p x := sorry
  q x := sorry

[nrs]

I had not considered: the metavariables syntax, andrefine and suffices are only available in tactics mode! (which must begin with a tactic block starting with the termby)

[Kyle Miller]

@Youngju Song Re (1), no sorry does not allow you to provide the proof later.

[Eric Wieser]

Youngju Song said:

I tried to use metavariables as you suggested, but not sure how to make it work

def myfunc'' (xs ys: List Nat): IO (List Nat) := by
  refine do
    assert!(xs.length = ys.length)
    let mut res := .nil
    for i in [0:xs.length] do
      res := (xs[i]'?_ + ys[i]'?_) :: res
    return res
  · sorry
  · sorry

[Kyle Miller]

There's currently no "program definition"-style system, but it seems like it should be possible to make a prototype for something that would effectively do what Eric just wrote, but with some potentially nicer syntax and properties. (Using by and refine like this changes the way in which the function elaborates in some subtle ways, and it should be possible to avoid this.)

[Kyle Miller]

I could imagine something like

def myfunc (xs ys: List Nat): IO (List Nat) := do
  assert!(xs.length = ys.length)
  let mut res := nil
  for i in [0:xs.length] do
    res := (xs[i]'?h1 + ys[i]'?h2) :: res
  return res
obligations
  case h1 => -- ... proof ...
  case h2 => -- ... proof ...

There is already a procedure to collect metavariables from a definition for error reporting purposes, but this obligations block could be a way to capture them.

[Matt Diamond]

any thoughts on assert! introducing assumptions? or is that a bad idea?

[Matt Diamond]

just asking if it would be theoretically desirable (I know it doesn't work that way right now)

[nrs]

we'd probably want that as an explicitly passed proof, since panic in Lean doesn't crash the program but produces a value

[Kyle Miller]

At least for now you can use an if/else to collect assumptions. I can't comment on having assert! be able to introduce hypotheses.

[Joachim Breitner]

Funnily, assert! does introduce assumptions for termination checking (because it’s using ite, and when handling recursion, ite is turned into dite):
#lean4 > assert! in recursive functions @ 💬

[Marcus Rossel]

(deleted)

[Youngju Song]

Thank you all for the advices!!
What @nrs and @Eric Wieser suggested seems to work well for my small examples.
@Kyle Miller what you suggested looks interesting. (1) Is there some feature request channel for Lean developers? (2) Do you think it could be implemented in the user side (without modifying Lean itself) with reasonable effort? If that is the case, maybe I can also give it a shot with advices from experts in the community.

[Kyle Miller]

@Youngju Song I got a prototype working:

syntax "program " term " by " Parser.Tactic.tacticSeqIndentGt : term

macro_rules
  | `(program $t by%$byTk $seq:tacticSeq) =>
    -- these %$_ annotations are a bid to get errors to appear in sensible places
    withRef (mkNullNode #[byTk, seq]) `(by%$byTk refine%$t $t; ( $seq ))

def myfunc (xs ys : List Nat) : IO (List Nat) := program do
  if hl : xs.length = ys.length then
    let mut res := []
    for h : i in [0:xs.length] do
      res := (xs[i]'?h1 + ys[i]'?h2) :: res
    return res
  else
    panic! "lengths not equal"
by
  case h1 => exact h.2
  case h2 => rw [← hl]; exact h.2

[Kyle Miller]

(The assert! wasn't adding any hypothesis to the context that h1 or h2 could capture, so I changed it to an if manually.)

[Kyle Miller]

(@Joachim Breitner What do you think about an obligations_by clause for definitions?)

[Joachim Breitner]

Plausible, but I'm not immediately convinced it's worth the extra language surface complexity. Maybe some program verification projects would benefit? Maybe your prototype is goin enough for those users to scratch that itch and demonstrate the usefulness of this idiom?

Also does this need to be attached to definitions, or could it be a term syntax, similar to where and like your prototype, so that it can be used locally as well, and everywhere where terms are expected, rather than just in definitions?

[Mario Carneiro]

note that program above is a term syntax

[Mario Carneiro]

I feel like a design here should also allow doing things like coq-procrastination

[Mario Carneiro]

in particular, you should be able to generate a metavariable inside a block scope and solve it outside that scope, provided there are enough opt-in markers

[Youngju Song]

@Kyle Miller Wow, that looks much more elegant than what I thought, thank you for doing this! I am playing with it and so far it seems to work. I will report here if I find an issue.

[Frédéric Dupuis]

Regarding assert! being able to introduce the hypothesis being asserted, the following works pretty well:

def checkThat (p : Prop) [Decidable p] : Option (PLift p) :=
  if h : p then some ⟨h⟩ else none

def myfunc (xs ys: List Nat): IO (List Nat) := do
  let some ⟨hlength⟩ := checkThat (xs.length = ys.length) | panic! "different lengths"
  let mut res := []
  for i in List.finRange xs.length do
    res := (xs[i] + ys[i]) :: res
  return res