The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Abhishek,

  There is a version avoiding the use of JMeq_eq using the dependent-pair equality encoding and looking for instances of an EqDec class that is part of the equations package (currently available only on my github, sorry), along with a generalize_eqs_sigma (iirc). The transformation to use sigmas instead of JMeq is fairly complicated though, and generates huge terms due to projections.
Best,
-- Matthieu

On Apr 20, 2014, at 17:49, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Thanks for that tip.

Somehow, my head hurts while writing down such matches manually, 

specially for more complicated proofs about  more complicated dependent data structures.

It feels like wasting a large fraction of my time and proof-script-space on steps that should intuitively be "trivial".

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Apr 20, 2014 at 11:20 AM, Daniel Schepler <dschepler AT gmail.com> wrote:

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/