The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 16 Dec 2010 12:27:20 +0100,
Guillaume Melquiond 
<guillaume.melquiond AT inria.fr>
 a écrit :

I come late, and my solution is not better than Stephane's one, but it
seems to be an alternative and is near of what you did (but without
using the exact tactic):

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))).
 Proof.
 intros x.
 (*case (f x).*)
 generalize (eq_refl (f x)).
 set (p := f x) at 2 3.
 generalize p; subst p.
 intros [].
  exact (H1 x).
 intros _; apply H2.
Qed.

> 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
>