coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity of inductive type implies False

From: Cristóbal Camarero Coterillo <nakacristo AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] injectivity of inductive type implies False
Date: Tue, 28 Feb 2017 18:08:50 +0000
Accept-language: es-ES, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nakacristo AT hotmail.com; spf=Pass smtp.mailfrom=nakacristo AT hotmail.com; spf=None smtp.helo=postmaster AT COL004-OMC1S10.hotmail.com
Ironport-phdr: 9a23:ZnRLDRbY/BjTF6Nvfg0rTRb/LSx+4OfEezUN459isYplN5qZr8y5bnLW6fgltlLVR4KTs6sC0LuL9fqwEjVZud6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCzbL52LBi6txvdu8oZjYd/N6o91gbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrRyhuRJx3pLUbo+WOvVicazQZskVSXZdUstLSyBNHp6wYo0SBOQBJ+ZYqIz9qkMQoBukBAmsH//v0jxTiXDs2a01y/osHhvD3AM6BdIBrm7UrNLtO6oMVuC10LfHzS/Cb/NS3Tf975XDfxcnof6WXrJ/a9beyVMuFwPeklWQrpfoPzOS1uQRtmiU9etgVea1h2E7rAFxpyGiy8ExgYfKnoIY0lHJ+CVjzIs1JdC0UkB2bNG+HJdOqy2WL4p7T8M4T2xouCs20LMLtJGhcCUJzpks2gTRZOadc4eS5xLuTOaRLil8hHJiYL+ymQ+8/068xuHgWcS4yU9EoC1bn9XRq34BygDf5tKHSvt64keh3CyA1wHX6u1ePU80kq/bJ4Ygwr42iJUTrVzOEy72lUnsjKKbdl8o9+an5uj9fLnquoeQN4puhQH/NqQulNa/AeM9MgUWWWiU4+e826f/8k3jQbVKleE2kq7CvZDaIsQbuqu5DBVU0oYn8RqwEzCm0NEAkXkdMF1FYA6Hj5TuO1zWPP/4Cu6/j02wnzdv2vDJJabsAo7NL3jGiLfuZ6xx609ayAopzNBQ/YhYCr8bIKG7Zkik/tffF1oyNxG+6+fhEtR0kI0EEyrbCaiAdajWrFWg5+Q1IuDKapVD6xjnLP1wzOTvlmOik1YZSoKg2JINZWq/Kd9hP0iDYH7ohZ9VF24JtwEkTff2j3WCViJWbne2Gak742doW8qdEY7fS9X10/S61yChE8gOaw==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Thank you Guillaume and Gil.

It felt natural to ask for injection. It is interesting to see that in Agda they made the same mistake.

Can it be assumed for simple types? As for example nat<>Z or list nat <> list Z. Maybe even list A=list B -> A=B.

Or more interestingly, if we define the type array by
Inductive array (A:Type):nat->Type:=
|nil : array A 0
|cons : forall n:nat, A -> array A n -> array A (S n).

then can be assumed that array m A=array n B implies m=n and A=B? or at least array m A=array n A -> m=n?

Best regards,

--Cristóbal Camarero

Re: [Coq-Club] injectivity of inductive type implies False, Cristóbal Camarero Coterillo, 02/28/2017
- Re: [Coq-Club] injectivity of inductive type implies False, Abhishek Anand, 03/01/2017
- <Possible follow-up(s)>
- Re: [Coq-Club] injectivity of inductive type implies False, Cristóbal Camarero Coterillo, 03/02/2017
  - Re: [Coq-Club] injectivity of inductive type implies False, Thorsten Altenkirch, 03/03/2017
    - Re: [Coq-Club] injectivity of inductive type implies False, Marco Servetto, 03/03/2017
      - Re: [Coq-Club] injectivity of inductive type implies False, Greg Morrisett, 03/03/2017
        
        Re: [Coq-Club] injectivity of inductive type implies False, Thorsten Altenkirch, 03/17/2017
        
        Re: [Coq-Club] injectivity of inductive type implies False, Marco Servetto, 03/20/2017