The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

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