The Coq mailing list

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

Oh, and just a precision, if you need something that depends on the
value of Z, in that case the hypothesis H1, make sure you assert it in
the context before clearing Z's body.

Stéphane

2010/12/16 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
>



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