The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

I am not sure whether it is related. But sometimes we do not really need existT's injectivity, although we seem to need it. Here is a typical example: if a family of relations RA are all transitive, then their union is transitive.

Inductive sigT_relation {I: Type} {A: I -> Type} (RA: forall i, relation (A i)): relation (sigT A) :=

  | sigT_relation_intro i a b: RA i a b -> sigT_relation RA (existT _ i a) (existT _ i b).

Instance sigT_relation_transitive {I: Type} {A: I -> Type} (RA: forall i, relation (A i))

  {_: forall i, Transitive (RA i)}: Transitive (sigT_relation RA).

When I tried to prove it for the first time, I thought I have to use existT's injectivity. But it can be axiom-free:

Require Import Relation_Definitions.

Require Import RelationClasses.

Lemma path_sigT {I: Type} {A: I -> Type} (x y : sigT A) (H : x = y) :

  { p : projT1 x = projT1 y & eq_rect _ A (projT2 x) _ p = projT2 y }.

Proof.

  exists (f_equal _ H).

  destruct H; reflexivity.

Qed.

Inductive sigT_relation {I: Type} {A: I -> Type} (RA: forall i, relation (A i)): relation (sigT A) :=

  | sigT_relation_intro i a b: RA i a b -> sigT_relation RA (existT _ i a) (existT _ i b).

Lemma path_sigT_relation {I: Type} {A: I -> Type} (RA: forall i, relation (A i))

  (x y : sigT A) (H: sigT_relation RA x y):

  { p : projT1 x = projT1 y & RA _ (eq_rect _ A (projT2 x) _ p) (projT2 y) }.

Proof.

  inversion H.

  simpl in *.

  exists eq_refl.

  simpl.

  auto.

Qed.

Instance sigT_relation_transitive {I: Type} {A: I -> Type} (RA: forall i, relation (A i))

  {_: forall i, Transitive (RA i)}: Transitive (sigT_relation RA).

Proof.

  intros; hnf; intros.

  inversion H0; inversion H1; subst.

  apply path_sigT in H6.

  destruct H6.

  simpl in *.

  subst.

  econstructor.

  eapply H; eassumption.

Qed.

Print Assumptions sigT_relation_transitive.

Hope it helps!

Qinxiang Cao

Shanghai Jiao Tong University, John Hopcroft Center

Room 1110-2, SJTUSE Building

800 Dongchuan Road, Shanghai, China, 200240

On Sat, Feb 15, 2020 at 4:44 AM Chris Dams <chris.dams.nl AT gmail.com> wrote:

Besides what Adam Chlipala writes there also is inj_pair2_eq_dec en Eqdep_dec

which does not need any axiom but which needs the assumption that equality on

T is decidable.

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