coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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_decwhich does not need any axiom but which needs the assumption that equality onT 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
- [Coq-Club] Injectivity of existT, John Li, 02/14/2020
- Re: [Coq-Club] Injectivity of existT, Adam Chlipala, 02/14/2020
- Re: [Coq-Club] Injectivity of existT, Chris Dams, 02/14/2020
- Re: [Coq-Club] Injectivity of existT, Cao Qinxiang, 02/15/2020
Archive powered by MHonArc 2.6.18.