The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

You need to first remove (or more precisely abstract) the part which
fails to typecheck when (f x) is generalized:

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.
 set (Z := A1 x) in *; clearbody Z.
 destruct (f x).
 ...

Notice how after the second line, the type of the first branch and its
relation with (f x) is in the hypothesis, which allows the subsequent
destruct to work.

Cheers,

Stéphane


On Thu, Dec 16, 2010 at 11:38 AM, Guillaume Melquiond
<guillaume.melquiond AT inria.fr>
 wrote:
> Hi,
>
> I'm having some trouble handling matchs when they have a dependent
> return type. Below is a simplified example. I would like to perform a
> case analysis on (f x) in order to simplify the goal. Ideally, that
> would produce two goals, one of them being:
>
> x: nat
> H: f x = true
> =============
> P (A1 x H)
>
> Standard tactics aren't helpful. I also tried writing a complete proof
> term, but I didn't succeed. Does anyone know of a tactic doing this kind
> of job or a way to write the proof term?
>
>
> Variable f : nat -> bool.
> Inductive A :=
>  | A1 : forall x, f x = true -> A
>  | A2 : A.
>
> Variable P : A -> Prop.
> Hypothesis H1: forall x (H: f x = true), P (A1 x H).
> Hypothesis H2: P A2.
>
> 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).*)
>
>
> Best regards,
>
> Guillaume
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06