Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Injectivity of existT

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Injectivity of existT


Chronological Thread 
  • From: Cao Qinxiang <caoqinxiang AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Injectivity of existT
  • Date: Sat, 15 Feb 2020 12:38:44 +0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f171.google.com
  • Ironport-phdr: 9a23:tiJ5iRIPwAu+VEagGdmcpTZWNBhigK39O0sv0rFitYgRKP7xwZ3uMQTl6Ol3ixeRBMOHsq4C1LOd7PqocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLx/IA+0oAnMucUbg5VuIbstxxXUpXdFZ+tZyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbDSxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lCsKMSMy/WfKgcJyka1bugqsqBNxw4HWYI+bOvlwcL7Dc9wGXmdORNpdWjZbD4+gc4cCDewMNvtYoYnnoFsOqAOzCBe2C+Po1zRGnX723as10uQgCw7G2gMgFM8JvXvIttr1M74SUeGzzKjHzDXMdfVW2Tjm5YjHdxAuu/CMXbZqfcXNzkkvEhrIg1ONooLmJzOYzvoBv3Sf4uZ6Vu+ii3QrpxxwrzWt3Msgl4vEip8Tx1vZ7yt22pw1Kse9SENjYd6rDp9QtyaCOotzWMwiQmVotD89yr0HpJK3ZSYKxIklyhLCcfCHfI+I4hXsVOaVPzh0nm5qeLW6hxqq8EigzPPzVtWs3VpUsiZIlsPAu3MN2hDJ98SKS/lw8l281TuNygzf8uRELlo1larfJZ4h2Lkwlp8LvEvfBCD2n1z2jK6QdkQr++in8eLnYrr9q5+TMo97kAD+MqA0lsOjBuQ4NxACX3KH9uSkyL3j4Ur5Ta1Wgf0xi6nVqYzVJcAGpqGiGAJVyYYi6xOnDzi8ytgYnH8HLEhEeB2dlYTpNUvOc7jECqK0hE3pmzN2zdjHOKfgC9PDNCvtirDkKJ107AZlyQwjzNlZ6NoAAbgGOfP1Sk74stPwARowMgjyyOHiXoYunrgCUH6CV/fKeJjZtkWFs7p2f7u8IbQNsTO4EMALoub0hCZgy1AYdKitm5AQbSLgR6U0EwCieXPpx+w5PyIPtws6QvbtjQTbAzFWbne2Gak742NiUd/0PcL4XomoxYe58mK7E5lRPD4UD1mNFTLvdtzBVa5TMWSdJchuljFCXr+kGdcs

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



Archive powered by MHonArc 2.6.18.

Top of Page