The Coq mailing list

[Li-Yang Tan <lytan AT artsci.wustl.edu>]

Hi All,

I am having trouble proving a seemingly intuitive fact about dependent
records:

Lemma projS2_eq :
  forall (A : Set)(P : A -> Set)(x : A) (p1 p2 : P x),
  existS P x p1 = existS P x p2 -> p1 = p2.

Presently, I have added it as an axiom but it would be nice if I could
avoid that.  Is this injectivity property independent of the type
theory?  A preliminary read of Cornes' and Terrasse's paper "Automatic
Inversion of Inductive Predicates in Coq" seems to suggest that this is
indeed the case, the reason being that it is equivalent to Streicher's
Axiom.

A full running example of the context in which I need this axiom/lemma
is given below.  Any help or suggestions would be greatly appreciated.

Thanks in advance,
Li-Yang Tan


Inductive q0_type : Set :=
  I : q0_type | O : q0_type | Fun : q0_type -> q0_type -> q0_type.

Inductive Var : q0_type -> Set :=
  V_ : forall t, nat -> Var t.
Inductive Const : q0_type -> Set :=
  Iota_ : Const (Fun I (Fun O I))
| Q_ : forall t, Const (Fun (Fun O t) t).
Inductive Trm : q0_type -> Set :=
  _v : forall t, Var t -> Trm t
| _c : forall t, Const t -> Trm t
| Lambda : forall s t, Var s -> Trm t -> Trm (Fun t s)
| Apply : forall s t, Trm (Fun s t) -> Trm t -> Trm s.

Implicit Arguments _v.
Implicit Arguments _c.
Implicit Arguments Lambda.
Implicit Arguments Apply.

Inductive Pos : Set :=
  empty : Pos
| P0 : Pos -> Pos
| P1 : Pos -> Pos.

Inductive subtrm : forall a b, Trm a -> Trm b -> Pos -> Prop :=
  subtrm_empty : forall a A, subtrm a a A A empty
| subtrm_apply0 : forall a b t M N T p,
                             subtrm t (Fun a b) T M p ->
                             subtrm _ _ T (Apply M N) (P0 p)
| subtrm_apply1 : forall a b t M N T p,
                             subtrm t b T N p ->
                             subtrm _ a T (Apply M N) (P1 p)
| subtrm_lambda0 : forall a b t x M T p,
                             subtrm t a T (_v x) p ->
                             subtrm t (Fun b a) T (Lambda x M) (P0 p)
| subtrm_lambda1 : forall a b t x M T p,
                             subtrm t b T M p ->
                             subtrm t (Fun b a) T (Lambda x M) (P1 p).
Implicit Arguments subtrm.

Lemma foo :
  forall a b t, forall M : Trm (Fun a b), forall N : Trm b,
  forall T : Trm t, forall p,
    subtrm T (Apply M N) (P0 p) -> subtrm T M p.
Proof.
  intros.
  inversion H.
  inversion H0; simpl.
  subst b0.
  assert (M0 = M).
  Focus 2.
  subst M0; assumption.
  (* Here, I need to prove M0 = M from H5 *)
Admitted.