The Coq mailing list

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

Hi everyone,

I have been looking at the type system in Coq, wondering what properties 
it ensures for proofs.  Thinking as an adversary, I borrowed some code 
from the Coq kernel.  Note, I didn't insert this into the kernel, I just 
load this code from coqtop.

    let internal_cut_rev_no_check id t gl =
      refiner (Prim (Cut (false, id, t))) gl

    let hack_tactic c gl =
       let id = next_name_away_with_default "H" Anonymous 
(pf_ids_of_hyps gl) in
          internal_cut_rev_no_check id c gl;;

    TACTIC EXTEND Hack
    | ["Hack" constr(c) ] -> [hack_tactic c]
    END

Next we try a proof.

   Coq < Declare ML Module "hack".
   Coq < Variables A : Prop.
   Coq < Goal A.
   Unnamed_thm < hack O.
   2 subgoals

   H : 0
   ============================
   A

   subgoal 2 is:
   0

This seems suprising to me.  Even though the second subgoal is 
unprovable, both subgoals are ill-formed.  Is this expected?  Is it 
accurate to say that proofs are valid only if one uses the "approved" 
functions from the kernel, and one does not use the refiner directly?

Perhaps the Coq semantics ensure that proofs using ill-typed terms are 
always invalid.

Peeking inside, we see the following.

proof_type.mli:
    and tactic = goal sigma -> (goal list sigma * validation)

    and validation = (proof_tree list -> proof_tree)

These are completely sensible types.  However, is it necessary to make 
them public/non-abstract?

I'm not criticizing, I just wonder if I missed something.  We use 
similar definitions in MetaPRL, but the tactic and validation types are 
abstract outside the kernel.  This helps ensure that correctness depends 
only on the kernel/refiner, not on user code (modulo correctness of 
OCaml, which is wonderful and reliable).

Jason

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