The Coq mailing list

["JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>]

Well, I confirm this is, in my perspective, worrying, even if this is 
justified. Consider this :

Variable States:Set.
Variable Progress:States->States->Prop.
Variable Is_Secure:States->Prop.

(* This is the security proof required, were x" the final state *)
Theorem system_secure:forall (x x'':nat), Is_Secure x->Progress x 
x''->Is_Secure x''.
Proof.
intros x x'' Hx Hprg; trivial.
Qed.
(* To do this proof, we have enriched the hint database about Progress x x" 
*)

(* Ancient version without hints about  Progress x x" *)
(* REMOVED =================
(* An axiom about security of x" w.r.t. the security of x *)
Axiom system_secure:forall (x x'':States), Is_Secure x->Progress x 
x''->Is_Secure x''.
(* Will have to check one day, may not be true for any x" *)
property about Progress x x" now proved ========= END OF REMOVED PART *)

Check system_secure.

   Regards, Eric

----- Original Message ----- 
From: "Chris Casinghino" <chris.casinghino AT gmail.com>
To: 
<coq-club AT pauillac.inria.fr>
Sent: Thursday, April 02, 2009 2:36 PM
Subject: [Coq-Club] Re: coq proof of fermat's last theorem


> I know it is partially documented [1], but are the coq developers
> aware that this "feature" can be exploited in this way?  All joking
> aside, it seems deceptive that this file compiles.