coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Deriving False from bool : Prop?
Date: Wed, 27 Jan 2016 10:26:55 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=arnaud.spiwack AT gmail.com; spf=Pass smtp.mailfrom=arnaud.spiwack AT gmail.com; spf=None smtp.helo=postmaster AT mail-lb0-f181.google.com
Ironport-phdr: 9a23:fSutshL1nwrHuEfyZ9mcpTZWNBhigK39O0sv0rFitYgUIvzxwZ3uMQTl6Ol3ixeRBMOAu60C07Cd6/qocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0ILvjavqodX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjfV7Y9RDjq1L9qVxbji29TPiUh8X7egc9YiKNL5gqmow1jzoXUZoCMKfc4cLmLLoBSfnZIQssED38JOYi7dYZaSrNZZes=

It's consistent. Set with --impredicative-set is like that.

On 27 January 2016 at 08:44, Jason Gross <jasongross9 AT gmail.com> wrote:

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