coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: roconnor AT theorem.ca
- To: Adam Chlipala <adamc AT cs.berkeley.edu>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Dependently-typed binary operators
- Date: Tue, 13 Sep 2005 02:35:14 -0400 (EDT)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Tue, 13 Sep 2005
roconnor AT theorem.ca
wrote:
> Think about what the two goals will be after the destruct. Write out what
> they are. Then you will realize it will be neccesary to
>
> unfold band32.
Actually now that I think about it, it is not clear from the resulting
goals that it is neccesary to unfold band32. Furthermore you probably
don't want to do destruct; destruct will generalize away the 32 and
consider both constructors.
You don't want to do this. You know your vector is of lenght 32, so you
know there is only one possible constructor. What you want instead is
dependent inverison. The solution to your 2nd order woes is seems to be
to generalize anything related to your term.
In this case you will need to do
generalize e2
clear e2
unfold band32
dependent inverion e1
Of course the next thing you will want to do is
dependent inversion e2.
But how you are going to do that is beyond my skills. I'd be tempted to
do the whole proof via (vector (bool*bool) 32). Perhaps others know
better solutions.
Welcome to the nightmare that is programming with dependent types. ;-)
--
Russell O'Connor <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''
- [Coq-Club] Dependently-typed binary operators, Adam Chlipala
- Re: [Coq-Club] Dependently-typed binary operators,
roconnor
- Re: [Coq-Club] Dependently-typed binary operators, roconnor
- Re: [Coq-Club] Dependently-typed binary operators, Pierre Casteran
- Re: [Coq-Club] Dependently-typed binary operators,
Conor McBride
- Re: [Coq-Club] Dependently-typed binary operators,
roconnor
- Re: [Coq-Club] Dependently-typed binary operators, Conor McBride
- Re: [Coq-Club] Dependently-typed binary operators,
roconnor
- Re: [Coq-Club] Dependently-typed binary operators, roconnor
- Re: [Coq-Club] Dependently-typed binary operators, Frederic Blanqui
- Re: [Coq-Club] Dependently-typed binary operators,
roconnor
Archive powered by MhonArc 2.6.16.