The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sat, Mar 16, 2013 at 5:31 PM, Leonardo Rodriguez
<leonardomatiasrodriguez AT gmail.com>
 wrote:
> Hello,
>
> Consider the following types:
>
> Inductive T : Type :=
>   a : T.
>
> Inductive H : T -> Type :=
>   b : H a.
>
> I have proved this trivial lemma:
>
> Lemma provable :
>   forall x : T, x = a.
> Proof.
>   intro x.
>   destruct x.
>   auto.
> Qed.
>
> But I couldn't prove this one:
>
> Lemma unprovable :
>   forall q : H a, q = b.
> Proof.
>   intro q.
> Abort.
>
> Could anyone explain me why? Has to do with proof irrelevance?
>
> Thank you in advance.

Here's another proof that's a bit closer to the wire than Adam's proof:

Lemma unprovable :
  forall q : H a, q = b.
Proof.
assert (forall (a':T) (q':H a'),
  match a' as a'' return (H a'' -> Prop) with
  | a => fun q'' => q'' = b
  end q').
destruct q'.
reflexivity.

exact (H0 a).
Qed.

And if you unfold the resulting proof term a bit, you get:

Definition unprovable' : forall q : H a, q = b :=
fun q:H a =>
  match q as q' in (H a') return
    (match a' as a'' return (H a'' -> Prop) with
     | a => fun q'' => q'' = b
     end q') with
  | b => eq_refl
  end.

(Shameless plug: This wasn't too hard to come up with by following the
principles of the EqualityFreeInversion page on the wiki.)
-- 
Daniel Schepler