coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Properties on mutual definitions

From: Taral <taralx AT gmail.com>
To: Thomas Th�m <thomas.thuem AT st.ovgu.de>
Cc: Adam Chlipala <adamc AT hcoop.net>, Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Properties on mutual definitions
Date: Wed, 9 Dec 2009 13:32:20 -0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=x/5oxWZf5Pz+VoJIPWU3s/GiPa8pgTr4dcO9Rqet/C0pMTQAhyDKTECCWU1MI+q7os pgvM9q+wAjyGyk0MPj0Ae8AApIpRFvgsnEvo5/j4/dozu2WEz8Tr0vtBV5vPWlpFfNL0 AvK+Kv/NiCUfEiG9m4wIx6JaQA1w5ZA9twmEo=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Dec 9, 2009 at 7:36 AM, Thomas Th�m
<thomas.thuem AT st.ovgu.de>
wrote:
> You are right. How do I solve it?

I think the key thing here is that the proof you were using was an
existence proof. That has to be strengthened before it can be easily
proved. What you need is this:

(forall a : exp, f a a) /\ (forall l : list exp, g l l).

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

[Coq-Club] Properties on mutual definitions, Thomas Th�m
- Re: [Coq-Club] Properties on mutual definitions, Adam Chlipala
  - Re: [Coq-Club] Properties on mutual definitions, Thomas Th�m
  - Message not available
    - Re: [Coq-Club] Properties on mutual definitions, Taral
- Re: [Coq-Club] Properties on mutual definitions, AUGER
  - Re: [Coq-Club] Properties on mutual definitions, muad
    - Re: [Coq-Club] Properties on mutual definitions, Adam Chlipala
      - [Coq-Club] Properties on mutual definitions, Thomas Th�m
        
        Re: [Coq-Club] Properties on mutual definitions, Adam Chlipala
        
        Re: [Coq-Club] Properties on mutual definitions, AUGER
        
        [Coq-Club] Properties on mutual definitions, Thomas Thüm