The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Le 16 déc. 2010 à 11:38, Guillaume Melquiond a écrit :

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

Hi Guillaume,

  there is one way to do it by transforming the case into a non-dependent one:

Require Import Sumbool.

Lemma if_bool_to_sumbool {B} (a : bool) 
  (b1 : forall p : a = true, B)
  (b2 : forall p : a = false, B)
  : 
  (if a as a' return a = a' -> B then b1 else b2) (refl_equal a) =
  (match sumbool_of_bool a with
     | left p => b1 p
     | right p => b2 p
   end).
Proof. destruct a; auto. Qed.

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. rewrite if_bool_to_sumbool.
case (sumbool_of_bool (f x)); intros.
apply H1. apply H2.
Qed.

-- Matthieu