The Coq mailing list

[nnovak <nnovak AT gc.cuny.edu>]

Hello,

Recently I've been playing with export of theories from Coq to XML.
And encountered this problem:

It seems that when a "simpl" tactic is used in a proof, after we
ask to show us the proof ("Show Proof") the work of this tactic is not
visible in the outputted proof, moreover it is also not in the
exported proof ("Show XML Proof").

I suspect it is not possible to verify efficiently that proofs
produced by "Show Proof"/"Show XML Proof" are correct ones.
I could try to apply "simpl" everytime when a certain step of the
proof can't be applied immediately but I'm not sure that this is the
right way to do. Also since "simpl" allows for parameters there is no
way to guess them.

Here is a more detailed description if what I was doing:

Lemma and a proof of the lemma (taken from Tutorial):

         Lemma plus_n_0: forall n:nat, n = n+O.
           intro.
           elim n.
           simpl.
           auto.
           simpl.
           auto.

         Show XML Proof.

         Show Proof.
         Qed.

1. Second simpl does the following:
 it makes the transition from S n = (S n) + 0   to  S n = S (n+0)
2. This transition is not seen in the proof of the lemma (shown by
command "Show Proof".
   here is the output of this command:
        LOC:
        Subgoals
        Proof: fun n : nat =>
            nat_ind (fun n0 : nat => n0 = n0 + 0) (refl_equal 0)
            (fun (n0 : nat) (H : n0 = n0 + 0) => f_equal S H) n

And it is also not in the proof extracted by the command "Show XML
Proof".

Best regards,
Natalia Novak