The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Does this lemma do approximately what you want?

Goal forall (b : bool) (P : bool -> Type) (t : true = b -> P true) (f : false = b -> P false) (H : true = b),

       (if b as b' return b' = b -> P b'

        then t

        else f) eq_refl

       = match H in (_ = b') return P b' with

           | eq_refl => t H

         end.

Proof.

  destruct H; reflexivity.

Defined.

On Tue, Dec 9, 2014 at 1:15 AM, Andrew Hirsch <akhirsch AT cs.cornell.edu> wrote:

Revert and dependent destruction do not work for me, since my actual example has much more complicated expressions. Here's the actual example, I can give more context if needed:

(if authority_message π a φ as b

     return (authority_message π a φ = b -> {Γ ⊢ ψ} + {True})

    then fun Heqb : authority_message π a φ = true => in_left

    else fun _ : authority_message π a φ = false => in_right) eq_refl

authority_message takes three types, the second of which (a in this case) is a proof about the first (pi). I also know that in this particular case, it's true. I'd like to get the fact that the answer is in_left.

-Andrew

On Tue, Dec 9, 2014 at 12:55 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

This should error on the theorem statement, because lhs does not have type [f a = f a -> B], which is the type of your left hand side.  It does not give you an error in 8.4 because of bug 3792, which has been fixed in trunk.

The error message you are getting from [rewrite] is a result of the fact that your new left hand side would have type [true = true -> B], while your new right hand side would have type [f a = true], because [rewrite] will not change the type of [lhs].  To fix this, you'll have to [revert lhs].  Then [rewrite pf] should work.  However, it's quite possible that this is not the issue you're having in your actual example;  for instance, the issue might be that the equivalent of [revert lhs] would itself cause a type error.

-Jason

On Tue, Dec 9, 2014 at 12:37 AM, Andrew Hirsch <akhirsch AT cs.cornell.edu> wrote:

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