coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: coq proof of fermat's last theorem

From: St�phane Glondu <steph AT glondu.net>
To: "JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>
Cc: Chris Casinghino <chris.casinghino AT gmail.com>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Re: coq proof of fermat's last theorem
Date: Fri, 03 Apr 2009 13:43:25 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

JAEGER, Eric (SGDN) a �crit :
> Well, I confirm this is, in my perspective, worrying, even if this is
> justified. Consider this :
> [...]
> Check system_secure.

Coq < Print Assumptions system_secure.
Axioms:
system_secure : forall x x'' : States,
Is_Secure x -> Progress x x'' -> Is_Secure x''

The checker (coqchk, new in 8.2) can also help spotting stray axioms.

Cheers,

--
St�phane

Re: [Coq-Club] coq proof of fermat's last theorem, (continued)
- Re: [Coq-Club] coq proof of fermat's last theorem, Edsko de Vries
- [Coq-Club] Re: coq proof of fermat's last theorem, Chris Casinghino
  - Re: [Coq-Club] Re: coq proof of fermat's last theorem, Guillaume Melquiond
    - Re: [Coq-Club] Re: coq proof of fermat's last theorem, Chris Casinghino
      - Re: [Coq-Club] Re: coq proof of fermat's last theorem, Guillaume Melquiond
        
        Re: [Coq-Club] Re: coq proof of fermat's last theorem, Ian Lynagh
        
        Re: [Coq-Club] Re: coq proof of fermat's last theorem, Hugo Herbelin
        
        Re: [Coq-Club] Re: coq proof of fermat's last theorem, Chris Casinghino
    - RE: [Coq-Club] Re: coq proof of fermat's last theorem, Georges Gonthier
  - Re: [Coq-Club] Re: coq proof of fermat's last theorem, JAEGER, Eric (SGDN)
    - Re: [Coq-Club] Re: coq proof of fermat's last theorem, St�phane Glondu