getting from #eval to a proof.

Stream: lean4

[Kind Bubble]

Suppose that after a good amount of work, I come up with a type T. Now that I've done all of my conceptual work, I can have it evaluated by Lean:

#eval T

Suppose that this gives me 6 in the output. Now that I know that T = 6, what is the name of the proof

p : T = 6

i.e. I used Lean to calculate something on its own... surely I can now access some proof p : T = 6 by some means or another?

[Kind Bubble]

Maybe there is some kind of simplify T and a proof p : T = simplify T?

Mostly I need this "simplify" to work well with arithmetic and inductive types.

[Henrik Böving]

The question doesn't exactly make sense to me, you are evaluating a type, types cannot be evaluated, they are...well types.

[Alex J. Best]

Its not always true that if Lean can #eval something then there is a clear way to prove it. Sometimes rfl will work as the proof, but this is not guarenteed.

[Kevin Buzzard]

Yeah 6 is not a type, I think you mean a term

[Mario Carneiro]

The native_decide tactic will allow you to prove equalities if #eval can evaluate them to true. It is discouraged though because it significantly increases the scope of the things you have to trust

[Mario Carneiro]

opaque T : Nat := 6

#eval T -- 6

example : T = 6 := rfl -- fail :(
example : T = 6 := by decide -- fail :(
example : T = 6 := by native_decide -- ok :)

[Jason Rute]

I’m surprised this works.

def fib : Nat -> Nat
| 0 => 0
| 1 => 1
| n+2 => fib n + fib (n+1)

#eval fib 30  -- 832040
theorem fib30 : fib 30 = 832040 := rfl

[Jason Rute]

@Kind Bubble I get the sense that you have an application in mind that would require both lean to compute things and generate proofs of its computations. While this is likely theoretically possible in some sense in Lean (as Lean is implemented in Lean) it is not the most natural thing to do. So it might be good to give the #xy of what you are trying to do.