The Coq mailing list

[Andrew Hirsch <akhirsch AT cs.cornell.edu>]

Hey Coq-Club,

I've been working with dependent matches explicitly for the first time recently, and I ran into a problem. I'm not sure how to do anything with a dependent if, since anything I do seems to run into a ill-typed middle step. Here's a minimal working example:

  Parameter A B : Type.

  Parameter a : A.

  Parameter f : A -> bool.

  Parameter lhs : f a = true -> B.

  Parameter rhs : B.

  Axiom pf : f a = true.

  

  Theorem i_would_like_this_to_work : (if f a as b return f a = b -> B

                                       then lhs

                                       else fun _ => rhs) = lhs.

Notably, this gives me an error when I type Admitted, while my example from my real codebase doesn't. I'm not sure why. 

Here's what I've been getting, when I try to e.g. rewrite pf: 

Toplevel input, characters 0-10:

Error: Abstracting over the term "f a" leads to a term

"fun b : bool =>

 (if b as b0 return (b = b0 -> B) then lhs else fun _ : b = false => rhs) =

 lhs" which is ill-typed.

Any help I could get on this would be appreciated!

-Andrew