The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Here's a trick that can avoid the need to derive UIP_refl for a certain type:

Require Import Vector.

Lemma vectorS_decomp : forall {A:Type} {n:nat}
  (v : Vector.t A (S n)),
  exists (h:A) (t:Vector.t A n), Vector.cons _ h _ t = v.
Proof.
intros.
Require Import Program.
dependent destruction v.
eexists; eexists; reflexivity.
Qed.
Print Assumptions vectorS_decomp.

This shows JMeq_eq being used.  But if, instead, you write out:

Lemma vectorS_decomp' : forall {A:Type} {n:nat}
  (v : Vector.t A (S n)),
  exists (h:A) (t:Vector.t A n), Vector.cons _ h _ t = v.
Proof.
intros.
refine (match v as v' in (Vector.t _ Sn) return
  (match Sn return (Vector.t _ Sn -> Prop) with
   | 0 => fun _ => True
   | S n' => fun v'' =>
      exists (h:A) (t:Vector.t A n'), cons _ h _ t = v''
   end v') with
| Vector.nil => _
| Vector.cons h _ t => _
end); clear n v.
trivial.
eexists; eexists; reflexivity.
Qed.
Print Assumptions vectorS_decomp'.

then this doesn't use JMeq_eq.  Lots more examples of this kind of
thing at http://coq.inria.fr/cocorico/EqualityFreeInversion .

I've seen reports on this list that there's an "invert" tactic to be
incorporated in future Coq releases, which should handle doing this
kind of thing automatically.
-- 
Daniel Schepler


On Sun, Apr 20, 2014 at 8:00 AM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
 wrote:
> Is there a version of the dependent destruction tactic
> that does not use the JMeq_eq axiom?
>
> Section 10.5 of CPDT says that JMeq_eq is derivable
> from UIP_refl.
> Also, UIP_refl is derivable for types with decidable equality.
> http://coq.inria.fr/distrib/8.4/stdlib/Coq.Logic.Eqdep_dec.html
>
>
> A version of dependent destruction could either take the equality decider
> explicitly as input, or appeal to a designated hint database
> to get the required proofs of decidable equality.
>
> If someone has already written such a tactic and can share the code,
> I'd be grateful.
>
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/