coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Indexed Types Pattern Matching Problem

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: Roman Beslik <beroal AT ukr.net>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Indexed Types Pattern Matching Problem
Date: Tue, 23 Mar 2010 10:37:08 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type; b=DlXLbgSqkkgM+zlHezuOLB9ZUQzKyxUwLid8+G8UcMdvdqR8xoJHutU8W0oe5elZKB By/LUt+RpZ0KuZFOrA6ht8la4YA8U+RKbtJgVPdD9FSnDhHkhl4F8fbChhJDkUniORLu nM/U4mFxRbwICkNT1YeN/32S0CHEZCaDNPdv8=

> "inversion x0" does "pattern matching". I think that it fails because "subst
> b" stands before "inversion x0" (see another proof below). "inversion H.
> subst b." changes "x0" to something different. There are different variables
> "x0 : Interpret RT b" and "x1 : Interpret RT Rec" in the proof term.

I see the point. I think it is the same what Chlipala says with
"convoy pattern" in his book, Chapter 7.

Many thanks again for very useful advices.

Best regards,

Gyesik

[Coq-Club] Indexed Types Pattern Matching Problem, Gyesik Lee
- Re: [Coq-Club] Indexed Types Pattern Matching Problem, Roman Beslik
  - Re: [Coq-Club] Indexed Types Pattern Matching Problem, Gyesik Lee
    - Re: [Coq-Club] Indexed Types Pattern Matching Problem, Roman Beslik
      - Re: [Coq-Club] Indexed Types Pattern Matching Problem, Gyesik Lee
        
        Re: [Coq-Club] Indexed Types Pattern Matching Problem, Roman Beslik
        
        Message not available
        
        Re: [Coq-Club] Indexed Types Pattern Matching Problem, Roman Beslik
        Re: [Coq-Club] Indexed Types Pattern Matching Problem, Gyesik Lee
- Re: [Coq-Club] Indexed Types Pattern Matching Problem, Adam Chlipala