Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Destructing dependent match

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Destructing dependent match


chronological Thread 
  • 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




Archive powered by MhonArc 2.6.16.

Top of Page