8.7.5 Proof checking
| Page 359 of 800||
The Logiweb proof checker verifies the proofs on a page as follows:
- Finding the proofs on the page
- The checker scans the codex for proofs. The codex contains definitions. A definition is a proof if it defines the proof aspect of a domestic construct. A construct is domestic if it is defined on the page itself. Non-domestic proofs are ignores so stating a proof on one page of a lemma from some other page has no effect.
- Tactic expansion
- Definitions are macro expanded before they reach the codex so the proof checker does not need to care about macro expansion. Instead, the proof checker does tactic expansion. It does so by doing normal evaluation (based on the value aspect) of the right hand side of each proof and then applying the result to the proof and to the cache of the page. The output of that is supposed to be a proof expressed in the Logiweb sequent calculus. If this process throws an exception, the proof is considered to be in error.
- Sequent evaluation
- The output from tactic expansion is sequent evaluated. For each proof this leads to a sequent of form where is a set of premisses, is a set of side conditions, and is a result which holds if the given premisses and side conditions hold. If sequent evaluation throws an exception, the proof is considered to be in error.
- Side condition check
- The proof checker checks that . If not, the proof is considered to be in error.
- Result check
- As mentioned, a proof is a definition. The left hand side of the definition is the lemma which the proof is supposed to prove. The proof checker looks up the statement aspect of the lemma and compares that aspect to . If they differ or if the statement aspect is undefined, the proof is considered to be in error.
- Premise checking
- For each premise in , the proof checker verifies that the premise is a lemma which has been proved elsewhere. If the lemma belongs to the same page then the proof checker verifies that the lemmas do not use each other in a circular fashion. If the lemma belongs to some other page then the proof checker performs two checks. First, it looks up the diagnose hook of that other page to see that the other page is correct. Second, it looks up the claim aspect of the other page to see that the other page has been verified by the same proof checker.
Copyright © 2010
| Page 359 of 800||