Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] existT


Chronological Thread 
  • From: Tom de Jong <tdejong.ac AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] existT
  • Date: Wed, 2 Oct 2019 14:12:01 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tdejong.ac AT gmail.com; spf=Pass smtp.mailfrom=tdejong.ac AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f42.google.com
  • Ironport-phdr: 9a23:y/QpkRIXJJR50duk1dmcpTZWNBhigK39O0sv0rFitYgRLPXxwZ3uMQTl6Ol3ixeRBMOHsqkC17Sd7fmocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTSwbal9IRi3ognct9QaipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPl8J+kqxbrhKiqRJxzYHbb4OaO+ZxcK7GYdMXRnBMUtpNWyFPAI6xaZYEAeobPeZfqonwv0UArRy7BQKxGezg1CJDiHvx3a083OQqDAbL3BA9EN0QsnTUq9P1NKgIXe+v0KbF1jrDb/ZM1jf87IjEaAwuofaJXb9pd8fa1EchFwTAjlqKqIzlOSuY1uULs2iB7upvT/iji2A9qwx3vzOhxd8sh5HXio4Jzl3I7yZ0zYYvKdGmVkJ3fMSoHZROuy2CKod7TcEvT3t1tCs5ybAKo4C3cDQWxJg92hLTd/6Kfo6V6Rz5TumROy13hHd9dbK/mRmy9U+gx/X5Vsau0VZKqjNJk9fWtnwQzhDT5MeKRuVn8keu3jaP0A/T6uVaLkwuiaXbLJshzqYxlpoVr0vDAjf7lFvqgKKSbEkp+eil5/75brn4u5OQLYB5hh/mPqQrgMO/AOA4MgYUX2ic/OSxzKHj8lDnT7VIif02lKbZvIrAKssHvaO5DApV3Zwi6xa7FTupzNMYnXwfIFJfZB2Hl5TpO03JIP3gEfi/hE2snC53yPDCI73uGY7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iNuNBRggdgew3uzPCdNn14pYV3jcLLWeNfbutlrA6u9nAe6Ka8dBpDrwKf8j6Ljnhlc2nFYcee+i2p5BOyPwJehvP0jMOSmkudwGC2pf5lNvHtyvs0WLVHtoX1j3Wqs94j8hD4f/VNXMQ4mshPqK2yLpR8QKNFADMUiFFDLTT6vBQ+0FMXvALcpokzhCXr+kGdd4iEOe8TTiwr8iFdL6vy0VsZW5iYpw7uzX0A4orHl6U57b3GaKQGV52GgPQm1u0Q==

> Actually, under some conditions existT is injective. It is the case if
> the underlying type has decidable equality. See proof below. IIRC
> a proof of this nowadays is also in the standard library, but I do not
> seem to be able to find it that quickly.
https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html

Best,

Tom

On 02/10/2019 1:47 pm, Chris Dams wrote:
Hello all,

Actually, under some conditions existT is injective. It is the case if
the underlying type has decidable equality. See proof below. IIRC
a proof of this nowadays is also in the standard library, but I do not
seem to be able to find it that quickly.

Good luck,
Chris

Definition sigT_get_proof:
   forall T: Type,
   forall eq_dec_T: forall t t': T, {t = t'} + {~ t = t'},
   forall P: T -> Type,
   forall t: T,
   P t ->
   sigT P ->
   P t.
intros T eq_dec_T P t H1 H2.
destruct H2 as [t' H2].
destruct (eq_dec_T t t') as [H3|H3].
rewrite H3.
exact H2.
exact H1.
Defined.

Theorem sigT_get_proof_existT_same:
   forall T: Type,
   forall eq_dec_T: forall t t': T, {t = t'} + {~ t = t'},
   forall P: T -> Type,
   forall t: T,
   forall H1 H2: P t,
   sigT_get_proof eq_dec_T t H1 (existT P t H2) = H2.
Proof.
intros T eq_dec_T P t H1 H2.
unfold sigT_get_proof.
destruct (eq_dec_T t t) as [H3|H3].
unfold eq_rect_r.
symmetry.
exact (eq_rect_eq_dec eq_dec_T (fun t: T => P t) H2 (sym_eq H3)).
tauto.
Qed.

Theorem existT_injective:
   forall T,
   (forall t1 t2: T, { t1 = t2 } + { t1 <> t2 }) ->
   forall P: T -> Type,
   forall t: T,
   forall pt1 pt2: P t,
   existT P t pt1 = existT P t pt2 ->
   pt1 = pt2.
Proof.
intros T T_dec P t pt1 pt2 H1.
pose (H2 := f_equal (sigT_get_proof T_dec t pt1) H1).
repeat rewrite sigT_get_proof_existT_same in H2.
assumption.
Qed.




Archive powered by MHonArc 2.6.18.

Top of Page