coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Deriving False from bool : Prop?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Deriving False from bool : Prop?
Date: Wed, 27 Jan 2016 07:44:08 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f175.google.com
Ironport-phdr: 9a23:sYyu6BFO3mmhO4NWUm63Ap1GYnF86YWxBRYc798ds5kLTJ75o8WwAkXT6L1XgUPTWs2DsrQf27WQ6/mrADVeqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0o8SYOlwWzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OShh78ry8BLHUAGn530GU2xQnAAeUCbf6xSvfJ7qtS2ymfB6wzLSac//VrcyVi6l9Lw6YBDtgSYDcTU+9TeE2YRLkKtHrUf59FREyInObdTNOQ==

Is it possible to derive [False] from the assumption that you have [T : Prop] with [a b : T] and [a <> b]? (On the flip side, is it possible to show that it's consistent to assume this?)

Thanks,

Jason

[Coq-Club] Deriving False from bool : Prop?, Jason Gross, 01/27/2016
- Re: [Coq-Club] Deriving False from bool : Prop?, Arnaud Spiwack, 01/27/2016
  - Re: [Coq-Club] Deriving False from bool : Prop?, roux cody, 01/27/2016
    - Re: [Coq-Club] Deriving False from bool : Prop?, Eddy Westbrook, 01/27/2016
      - Re: [Coq-Club] Deriving False from bool : Prop?, Thorsten Altenkirch, 01/27/2016
        
        Re: [Coq-Club] Deriving False from bool : Prop?, Eddy Westbrook, 01/27/2016
        
        Re: [Coq-Club] Deriving False from bool : Prop?, roux cody, 01/27/2016
        
        Re: [Coq-Club] Deriving False from bool : Prop?, Thorsten Altenkirch, 01/28/2016
        Re: [Coq-Club] Deriving False from bool : Prop?, Bob Atkey, 01/28/2016