The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Nadeem Abdul Hamid wrote:
> Now, however, if 'func1' depends on a proof of 'expr1', then the elim 
> tactic no longer succeeds, I guess because of the dependencies 
> introduced:
>
> Parameter elt : Set.
> Parameter expr1 : nat -> bool.
> Parameter func1 : forall i:nat, expr1 i = true -> option elt.
>
> Goal forall i,
> ((if (expr1 i) as b return (expr1 i = b -> bool)
> then fun X : expr1 i = true =>
> match (func1 i X) with
> | Some _ => true
> | _ => false
> end
> else fun _ => false) (refl_equal _) = true) ->
> elt.
> Proof.
> intros i.
> elim (expr1 i).
>
> Problem: "Abstracting over the term "expr1 i" leads to a term...
> which is ill-typed."

The usual trick works: identify subterms that are causing trouble and 
generalize over them.

intros i.
generalize (func1 i).
elim (expr1 i).