The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Sep 28, 2012 at 8:11 AM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> I wanted to manually perform a "discriminate", and I did something
> like :
>
> Lemma Z : true = false → False.
> refine (λ H, match H with eq_refl => True end).
> Defined.
>
> I am pretty sure it used not to work (I am on a 8.4 trunk version) on
> 8.3. So I was very surprised to see it working, and I feared a bug.
>
> Print Z.
>
> Hopefully returns something that I recognize to be correct. So now
> pattern matching on Coq seems more clever than in 8.3. So I was
> wondering from when such an improvement occured and if there was some
> other nice improvement in the same spirit (I did not find it in the
> Changelog…).

Interesting... it seems this also applies to a lot of the cases I have
in EqualityFreeInversion...

Inductive vector (X:Type) : nat -> Type :=
| vector_nil : vector X 0
| vector_cons : X -> forall {n:nat}, vector X n ->
     vector X (S n).

Definition vector_hd {X:Type} {n:nat} (v : vector X (S n)) : X :=
match v with
| vector_nil => tt
| vector_cons h _ _ => h
end.
Print vector_hd.

Definition vector_tl {X:Type} {n:nat} (v : vector X (S n)) :
  vector X n :=
match v with
| vector_nil => tt
| vector_cons _ _ t => t
end.

Definition vector_split {X:Type} {n:nat} (v : vector X (S n)) :
  { p : X * vector X n | let (h,t):=p in
                         v = vector_cons _ h t } :=
match v with
| vector_nil => tt
| vector_cons h _ t =>
  exist _ (h, t) eq_refl
end.

Also...
Lemma S_inj : forall m n:nat, S m = S n -> m = n.
Proof.
intros.
refine (match H with | eq_refl => _ end).
reflexivity.
Qed.

It still doesn't seem to apply as is to my canonical example which
seems to require three nested match/return expressions -- proving
injectivity of FinS:

Inductive Fin : nat -> Set :=
| FinO : forall {n}, Fin (S n)
| FinS : forall {n}, Fin n -> Fin (S n).

Lemma FinS_inj : forall {n:nat} (x y:Fin n),
  FinS x = FinS y -> x = y.
Proof.
intros.
(*
refine (match H with
        | eq_refl => eq_refl
        end).
internal type checking error! *)
refine (match H in (_ = FinS_y) return
  (match FinS_y as FinS_y' in (Fin Sn) return
     (match Sn return Type with
      | 0 => unit
      | S n => Fin n -> Prop
      end) with
   | FinO _ => fun _ => True
   | FinS _ y => fun x => x = y
   end x) with
| eq_refl => _
end).
reflexivity.
Qed.

(I've also, in the past, worked out a proof of
forall {n} (x y:Fin n) (P : FinS x = FinS y -> Prop), (forall e:x=y, P
(f_equal FinS e)) -> forall e':FinS x = FinS y, P e',
i.e. dependent inversion of an equality statement of the form FinS x =
FinS y to something of the form f_equal FinS (e : x = y).  In that
case, the nested return expressions get even more complex -- but it's
definitely possible to do it without JMeq or anything of that sort.)
-- 
Daniel Schepler