coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proving efficient decidability of a Prop?
- Date: Wed, 09 Jul 2014 23:34:47 +0200
On 09/07/2014 22:54, Andrew Kent wrote:
> My question is, was it silly of me to think that a big proof of decidability
> would be useful in helping prove particular instances? Is there some other
> "obviously better" approach I should have taken? Or an obviously better way
> to
> now prove instances of MyRel? Is this the kind of problem where one must
> utilize the refine tactic to get correct *and* efficient code? Or is it
> possible that I just wrote a particularly bad proof?
In general, function creating decidability proofs generate huge proof
terms, resulting in computational inefficiency. I tend to favour the
writing of such proofs on two steps :
1. A decision function : Definition decide : A -> B -> bool.
2. A specification : Definition decide_spec : forall (a : A) (b : B),
decide a b = true <-> MyRel a b.
This way, one can focus on the computational part of the decision
procedure. This may prove tricky to write though, depending on the
definition of MyRel.
PMP
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] Proving efficient decidability of a Prop?, Andrew Kent, 07/09/2014
- Re: [Coq-Club] Proving efficient decidability of a Prop?, Pierre-Marie Pédrot, 07/09/2014
- Re: [Coq-Club] Proving efficient decidability of a Prop?, Daniel Schepler, 07/10/2014
- Re: [Coq-Club] Proving efficient decidability of a Prop?, Andrew Kent, 07/10/2014
- Re: [Coq-Club] Proving efficient decidability of a Prop?, Cedric Auger, 07/10/2014
- Re: [Coq-Club] Proving efficient decidability of a Prop?, Andrew Kent, 07/10/2014
Archive powered by MHonArc 2.6.18.