The Coq mailing list

[Jason Hickey <jyh AT cs.caltech.edu>]

Jean-Christophe Filliatre wrote:
> In  the Coq  architecture, the  correctness is  ensured at  the kernel
> level,  once  the  proof  is  completed.   To  be  more  precise,  the
> validation above will build the proof  term once the proof is done and
> this proof term will be type-checked by the kernel.

Thanks, that makes perfect sense.  We do a similar double-check in 
MetaPRL.  To follow the soundness argument one step further, a 
programmer can always write a bad tactic, even a bad validation. 
However, a proof_tree can always be checked.

   type proof_tree = {
     open_subgoals : int;
     goal : goal;
     ref : (rule * proof_tree list) option }

In a complete proof, there must be no open_subgoals, and no ref=None.  A 
proof_tree proves a goal if the goal has a type, and for each node in 
the tree the (goal, rule, subgoals) is a valid inference.  Furthermore, 
1) there are a small number of rules defined by the kernel, and 2) in 
each case, if the goal has a type then the subgoals have a type.

In the implementation of proof checking, what happens with terms in rule 
arguments?  For example, for the rule (Cut (direction, id, <term>)), I 
assume the proof checker must perform a typecheck on <term>.  Is this right?

Thanks,

Jason

--
Jason Hickey                  http://www.cs.caltech.edu/~jyh
Caltech Computer Science      Tel: 626-395-6568 FAX: 626-792-4257