How do I print out the "normal form" of a Lean4 program?

Stream: lean4

[Daniel Donnelly]

I hear that under some formal systems proof equivalence is well-defined by normal form equality, so I was wondering if we can equate Lean4 programs in any way? Also is variable substitution permutations (of all "variable symbols" including type variables and possibly even constants & other symbols) plus normal form an even stronger equality?

[Marcus Rossel]

AFAIK, equality of proofs is given by Lean's underlying calculus (#leantt) - it defines a notion of "definitional equality" and states that all proofs of the same proposition are definitionally equal.
For programs, i.e. functions, Lean allows us to equate them by "function extensionalty", using the funext axiom. It states that two functions which agree on all inputs are equal.
Judging from your question, this is probably rather unsatisfactory for you though :sweat_smile: So if you want to go more in the direction of directly comparing terms, Lean's Expr type might be interesting for you.

[Henrik Böving]

There does exist the so called weak head normal form (or whnf in code) for the Expr type but its job is not to always show equality of all Expr terms (if they are equal that is), only for a select subset.

[Henrik Böving]

I would also not be surprised if writing such a program is in fact impossible since this would be equivalent to a solver for any = proposition right? Seems unlikely to me that a general program for this does exist and if it exists it probably runs in infeasible time.

[Mario Carneiro]

The #reduce function can be used to compute the normal form of any lean term. It is not impossible, but it definitely has galactic complexity bounds. The status of strong normalization in lean is a little unclear though. It is mostly true for CIC-like systems, but false for proofs in Prop because of proof irrelevance (there is a recent counterexample by Coquand and Abel); it is still open for VM-style evaluation where proofs are skipped but other data types are computed until normalization.

[Mario Carneiro]

It's not equivalent to solving = propositions, this is certainly undecidable. The normal forms of a + (b + c) and (a + b) + c are not the same, even though they are provably (propositionally) equal (where a,b,c : nat)