The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  Concerning the equality between two existT, you can find some useful  lemmas in libraries EqdepFacts and Eqdep_dep.

  EqdepFacts.eq_sigT_fst:
  forall (X : Type) (P : X -> Type) (x1 x2 : X) (H1 : P x1) (H2 : P x2),
  existT P x1 H1 = existT P x2 H2 -> x1 = x2

inj_pair2_eq_dec :
forall A : Type,
(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

Hope this helps

Pierre

---

De: "Jeremy Dawson" <Jeremy.Dawson AT anu.edu.au>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mardi 1 Octobre 2019 09:57:05
Objet: [Coq-Club] existT

Hi,

I have an inductive definition:

Inductive
in_dersrec (X : Type) (rules : rlsT X) (prems : X -> Type)
(concl : X) (d : derrec rules prems concl)
   : forall concls : list X, dersrec rules prems concls -> Type :=
     in_dersrec1 : forall (concls : list X) (ds : dersrec rules prems
concls),
                   in_dersrec d (dlCons d ds)
   | in_dersrec2 : forall (concl' : X) (d' : derrec rules prems concl')
                     (concls : list X) (ds : dersrec rules prems concls),
                   in_dersrec d ds -> in_dersrec d (dlCons d' ds)

When I have a goal with
X0 : in_dersrec d ds
among the assumptions,
inversion X0. gives new assumptions

   ds0 : dersrec rules prems concls
   H0, H2 : p :: concls = ps
   H3 : existT (fun x : list X => dersrec rules prems x)
          (p :: concls) (dlCons d ds0) =
        existT (fun x : list X => dersrec rules prems x) ps ds

What I would expect to get is also
dlCons d ds0 = ds

Whay do I get this strange assumption?

Furthermore, it seems that existT is a constructor for the inductive
definition of sigT.  That being so, why doesn't injection H3
give that the respective arguments of the two occurrences of existT are
equal?

thanks for any help

Jeremy