The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Actually, I only had weak decidable equality (x=y \/ x<>y) for some of 
the types.  But I proved a version of inj_pair2_eq_dec that works in 
that case:


Lemma inj_pair2_weak_eq_dec : forall A, (forall x y:A, x=y \/ x<>y) ->
                                   ( forall (P:A -> Type) (p:A) (x y:P 
p), existT P p x = existT P p y -> x = y ).
Proof.
  intros A eq_dec.
  apply eq_dep_eq__inj_pair2.
  apply eq_rect_eq__eq_dep_eq.
  apply Streicher_K__eq_rect_eq.
  apply UIP_refl__Streicher_K.
  cbv. intros.
  apply eq_proofs_unicity.
  apply eq_dec.
Qed.

-- Jonathan


On 05/30/2016 06:51 PM, Jonathan Leivent wrote:
> On 05/30/2016 06:45 PM, Daniel Schepler wrote:
> > On Mon, May 30, 2016 at 2:50 PM, Adam Chlipala <adamc AT csail.mit.edu> 
> > wrote:
> > > In general, it requires an axiom.  If you [Require Import Eqdep], 
> > > you get it
> > > as [inj_pair2].
> > >
> > >
> > > On 05/30/2016 05:48 PM, Jonathan Leivent wrote:
> > > > Is this provable?:
> > > >
> > > > Lemma existT_inj : forall T f x a b, @existT T f x a = @existT T f 
> > > > x b ->
> > > > a = b.
> > > >
> > > > I can't prove it with injectivity, or by f_equal with projT2.  If 
> > > > it is
> > > > provable, what's the secret ingredient?
> > And in a specific case, if you have a decision procedure for equality
> > to x, then existT_inj holds for that case.  (Ex: if T = nat; or if T =
> > option A, and x = None.)
>
> That's precisely what I need - as I do have decidable equality for the 
> type involved.  I see it now: Eqdep_dec.inj_pair2_eq_dec:
>
> Thanks!
>
> -- Jonathan