coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Destructing dependent match
- Date: Thu, 16 Dec 2010 12:27:20 +0100
Le jeudi 16 décembre 2010 à 11:38 +0100, Guillaume Melquiond a écrit :
> Goal forall x, P (
> (if f x as b return (f x = b -> A) then fun H => A1 x H else fun _ => A2)
> (refl_equal (f x))).
> intros x.
> (*case (f x).*)
I finally managed to get the proof term right:
exact ((if f x as b' return (forall H0: f x = b', P
((if b' as b return f x = b -> A then fun H : f x = true => A1 x H
else fun _ => A2) H0)
) then fun H => H1 x H else fun _ => H2) (refl_equal (f x))).
But Matthieu's and Stephane's solutions look a lot more usable in
practice. Thanks.
Best regards,
Guillaume
- [Coq-Club] Destructing dependent match, Guillaume Melquiond
- Re: [Coq-Club] Destructing dependent match, Matthieu Sozeau
- Re: [Coq-Club] Destructing dependent match,
Stéphane Lescuyer
- Re: [Coq-Club] Destructing dependent match, Stéphane Lescuyer
- Re: [Coq-Club] Destructing dependent match, Guillaume Melquiond
- Re: [Coq-Club] Destructing dependent match, AUGER Cedric
Archive powered by MhonArc 2.6.16.