Syntactically separate goals from code

Stream: new members

[MrQubo]

Is it possible in lean to syntactically separate proof obligations from the code?

As an example, with the proof obligation here I know of two ways I could write that proof:

inductive T
| t1 : T
| t2 : Array Nat → T

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => arr[0]'(by admit)

or

inductive T
| t1 : T
| t2 : Array Nat → T

def foo : T → Nat
| T.t1 => 0
| T.t2 arr =>
  have h : 0 < arr.size := by admit
  arr[0]'h

But in both cases the proof is written inline together with the code. Is it possible to somehow separate it? E.g. something like that?

inductive T
| t1 : T
| t2 : Array Nat → T

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => arr[0]'proof1
  where
    proof1 := by admit

Or even better, without having to give a name to the proof.

Also, the question is not tied to array access only, I would want something like that for any Prop autoParam.

[Mauricio Collares]

It's a bit subjective. Do you think the following is a solution?

inductive T
| t1 : T
| t2 : Array Nat → T

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => by
  refine arr[0]'?_
  · sorry

[Bjørn Kjos-Hanssen]

How about this...

import Mathlib

lemma prove {arr : Array Nat} : 0 < arr.size := by admit

inductive T
| t1 : T
| t2 : Array Nat → T

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => arr[0]'prove

[MrQubo]

@Mauricio Collares Not really. You could imagine there's more code after arr[0], or one more constructor and case T.t3.

[Aaron Liu]

inductive T
| t1 : T
| t2 : Array Nat → T

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => arr[0]'prove
  where
    prove {arr : Array Nat} : 0 < arr.size := by admit

[Mauricio Collares]

MrQubo said:

Mauricio Collares Not really. You could imagine there's more code after arr[0], or one more constructor and case T.t3.

Can you give an example? I'm not sure I'll be able to help, but I think it will help others understand the constraints. With one more constructor, you could do something like

inductive T
| t1 : T
| t2 : Array Nat → T
| t3 : Array Nat → T

def foo : T → Nat := by
  refine fun x =>
    match x with
    | T.t1 => 0
    | T.t2 arr => arr[0]'?_
    | T.t3 arr => arr[1]'?_
  · sorry
  · sorry

[MrQubo]

Mauricio Collares said:

MrQubo said:

Mauricio Collares Not really. You could imagine there's more code after arr[0], or one more constructor and case T.t3.

Can you give an example? I'm not sure I'll be able to help, but I think it will help others understand the constraints

Yes, sorry, here's an example:

inductive T
| t1 : T
| t2 : Array Nat → T
| t3 : T

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => arr[0]'(by admit) + arr[1]'(by admit)
| T.t3 => 0

I would want something like:

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => arr[0]'?_ + arr[1]'?_
| T.t3 => 0
  . by admit
  . by admit

As to why I want it. My goal is to make the functions easier to read. Usually I wouldn't care about proofs if I want to read the function to understand what it does.

[MrQubo]

Ah, yes, I can refine the whole body of a function, that looks promising!

[Kyle Miller]

I imagine one day there will be some real syntax for this. I understand Coq has such a feature.

Imagine a proofs clause, something like

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => arr[0]'?pf1 + arr[1]'?pf2
| T.t3 => 0
proofs
  case pf1 => sorry
  case pf2 => sorry

[MrQubo]

Kyle Miller said:

I imagine one day there will be some real syntax for this. I understand Coq has such a feature.

Imagine a proofs clause, something like

def foo : T → Nat
| T.t1 => 0
| T.t2 arr => arr[0]'?pf1 + arr[1]'?pf2
| T.t3 => 0
proofs
  case pf1 => sorry
  case pf2 => sorry

I implemented this with a macro:

import Lean

section

open Lean

macro d:Parser.Command.declaration "\nproofs\n" proofs:Parser.Tactic.tacticSeqIndentGt : command => do
  let proofs : TSyntax ``Parser.Tactic.tacticSeq := ⟨proofs⟩
  let d := d.raw
  let decl := d[1]
  -- TODO: abbrev, opaque, example
  if decl.isOfKind ``Parser.Command.definition then
    -- "def " >> declId >> optDeclSig >> declVal >> optDefDeriving
    let mut declVal : Syntax := decl[3]
    if declVal.isOfKind ``Parser.Command.declValSimple then
      -- leading_parser " :=\n" >> termParser >> Termination.suffix >> optional Term.whereDecls
      let term ← Elab.Term.expandWhereDeclsOpt declVal[3] declVal[1]
      let term : TSyntax `term := ⟨term⟩
      let term ← `(by refine $term; ($proofs))
      declVal := declVal.setArg 1 term
      declVal := declVal.setArg 3 mkNullNode
    else if declVal.isOfKind ``Parser.Command.declValEqns then
      -- leading_parser Term.matchAltsWhereDecls
      let declValEqns := declVal[0]
      -- leading_parser matchAlts >> Termination.suffix >> optional whereDecls
      let term ← Elab.Term.expandMatchAltsWhereDecls declValEqns
      let term : TSyntax `term := ⟨term⟩
      let term ← `(by refine $term; ($proofs))
      let terminationSuffix := declValEqns[1]
      declVal := mkNode ``Parser.Command.declValSimple #[mkAtom ":=", term, terminationSuffix, mkNullNode]
    else
      Macro.throwUnsupported
    let decl := decl.setArg 3 declVal
    let d := d.setArg 1 decl
    return ⟨d⟩
  else
   Macro.throwUnsupported

end

inductive T
| t1 : T
| t2 : (arr : Array Nat) → arr.size > 1  → T
| t3 : T

def foo : T → Nat
| T.t1 => 0
| T.t2 arr _ => arr[0]'?pf1 + arr[1]'?pf2
| T.t3 => 0
proofs
  case pf1 => omega
  case pf2 => omega

[Tomaz Mascarenhas]

Kyle Miller said:

I understand Coq has such a feature.

Indeed, in Coq there is a Program Definition constructor which defers all proof obligations to after you've defined your function, which I think is exactly what is being asked here: https://coq.inria.fr/doc/v8.9/refman/addendum/program.html#program-definition

[MrQubo]

Tomaz Gomes said:

Indeed, in Coq there is a Program Definition constructor which defers all proof obligations to after you've defined your function, which I think is exactly what is being asked here: https://coq.inria.fr/doc/v8.9/refman/addendum/program.html#program-definition

I don't know Coq too much, but indeed, I think that's what I'm asking about.
To apply it to Lean specifically, I think that every unsolved autoParam should generate a proof obligation automatically. And maybe even every implicit param.