The Coq mailing list

[Ben Moseley <ben_moseley AT mac.com>]

Hi,

I am somewhat puzzled by some behaviour with binding variables within nested 
matches.

I am working with: Coq 8.2pl1 (November 2010)

If I define a basic type and term...

Unset Printing Matching.
Inductive MyType : Set := | Left | Right.
Definition term (t : option MyType) : bool :=
  match t with
    | Some x => (match x with
                   | Left  => true
                   | Right => true
                 end)
    | None => true
  end.

...and then try to prove the following...

Theorem termTrue : forall t, term t = true.
  intro t; unfold term;
  match goal with | [ |- context [match ?d with
                                    | Some _ => (match ?y with
                                                   | Left  => true
                                                   | Right => true
                                                 end)
                                    | None => true
                                  end] ] => destruct d; [|reflexivity]
  end.
  destruct m; reflexivity.
Qed.

... then the match fails.

If instead I replace the '?y' with '_', then it succeeds.

Is there some reason why I can't bind both '?d' and '?y' ?

--Ben