CODEWITHSUNDEEP
isabelle
Tom
Tom

Reputation: 6971

How can I recover the Pure lambda expression associated with a proof in Isabelle?

When constructing a proof in Isabelle/HOL we are actually constructing a lambda expression that has a type corresponding to the theory we are trying to proof.

Is there anyway to see the raw lambda expression that corresponds to a proved theorem?

Upvotes: 0

Views: 69

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8248

I get the feeling you're coming from the world of dependently-typed systems like Coq or Lean. Isabelle is an LCF-style prover, which works quite differently. No information on the proof steps is recorded for performance reasons – the soundness of the system is instead ensured by having a comparatively small and simple kernel that all other code must go through in order to produce theorems.

There is, however, an option to let the Isabelle kernel record ‘proof terms’, which are probably more or less what you are looking for. Look at the HOL-Proofs session in the Isabelle distribution and the following paper:

Proof terms for simply typed higher order logic (freely accessible version, slides)

However, this is a feature that is almost never used and the suffers from poor performance of anything except very small examples.

There are several reasons for this and I am not an expert, so take this with a grain of salt: my impression is that the reason is that 1. this feature has never been considered very important so far and is therefore not fully optimised, and 2. proofs in Isabelle tend to use lots of automation, and the proof terms resulting from such automatic procedures are often needlessly blown up and ugly.

Another issue might be (careful, I might be completely mistaken here) that systems like Coq and Lean have the concept of definitional equality and apply such equations implicitly without recording their application in the proof term at all. Isabelle/HOL, on the other hand, has no such thing (all equalities are the same) and one must therefore be recorded explicitly.

However, there has recently been some new interest in this matter and people are actively working on improving the performance and usability of Isabelle's proof terms. So hopefully the situation will be a bit better in a few years!

Upvotes: 2

Related Questions