The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

Hello all,
I have a Coq problem:

Consider the following situation (a simplified abstraction of a  
program that I am working on), the development for which goes through  
fine:

    Parameter elt : Set.
    Parameter expr1 : nat -> bool.
    Parameter func1 : forall i:nat, option elt.

    Goal
     forall i,
      ((if (expr1 i) as b return (expr1 i = b -> bool)
        then fun X : expr1 i = true =>
          match (func1 i) with
            | Some _ => true
            | _ => false
          end
        else fun _ => false) (refl_equal _) = true) ->
      elt.
    Proof.
      intros i.
      elim (expr1 i); try (intros Habs; discriminate Habs).
      elim (func1 i); try (intros Habs; discriminate Habs).
      intros e _; exact e.
    Defined.

Basically, reasoning that if the big, complicated expression reduced  
to 'true' then it must have been the case that func1 produced some  
element, and that is exactly what is needed.


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."

      (* note: func1 is opaque because this goal is actually happening
         in the body of a fixpoint defined using 'Program', and func1  
is
         the recursive call, so it is not possible to unfold it to  
get rid of
         the dependency on X through reduction/simplification of  
'(func1 i X)'.*)


Is there any way to solve the problem in the second instance?

Thanks in advance for any help/suggestions.

--- nadeem