The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

I'm not sure that's helpful in your case, but

n <> 0

can also be formulated as

match n with 0 => False | S n => True end

which is irrelevant. The same should work for any equality of the form

n <> M

where M is a closed term. A bit different from Gabriel's idea, but not 
entirely different: you can maybe replace

n <> m

in general by

negb (eqb n m) = true

Since the latter is an equality on booleans it should also be irrelevant.

Best
Yannick

On 24/06/2020 08:51, Talia Ringer wrote:
> Thanks, that is very helpful! Part of the motivation for this was trying 
> to understand why I find it more difficult to reason about { n : nat | n 
> <> 0 } than I do about the inductive positives. It seems like it may be 
> easier to reason about a different refinement of nats. (This is not for 
> personal proving purposes, just academic curiosity.)
>
> On Tue, Jun 23, 2020, 10:31 PM Gabriel Scherer 
> <gabriel.scherer AT gmail.com <mailto:gabriel.scherer AT gmail.com>> wrote:
>
>     Pierre-Marie's typical example defines (A -> B) in the guest type
>     theory as (bool * (A -> B)) in the host theory, with a
>     type-preserving translation, and (=) in the guest as just (=) in the
>     host.  For any function you can get another distinct (but observably
>     equivalent in the guest) function by flipping the boolean. This also
>     applies if B is False.
>
>     On the other hand, you could define a "smaller" type of
>     inequivalence for a type (as an inductive presentation if you can,
>     for example) that has better properties. This comes up often in
>     cases where you need to reason on elements being equal, as the
>     definition of inequivalence as a function makes it hard to reason about.
>     For natural numbers for example, one definition of inequivalence
>     might be something like
>
>     Inductive different :=
>     | Bigger : forall (k : nat), m = n + S k -> different m n
>     | Smaller : forall (k : nat), m + S k = n -> different m n.
>
>     and this one should inherit contractibility from equality.
>
>     On Wed, Jun 24, 2020 at 6:12 AM Jason Gross <jasongross9 AT gmail.com
>     <mailto:jasongross9 AT gmail.com>> wrote:
>
>         As I understand it, with funext, you can prove irrelevance for
>         all proofs of x <> y of any type (because False is an hProp). 
>         However, without funext, you can't really prove anything about
>         equality of most function spaces (just like without K nor
>         univalence, you can't really prove anything about equality of
>         most types).  (I think there's actually a deeper relationship
>         here, probably along the same lines of how univalence implies
>         funext.  I don't understand it fully myself, but I believe Dan
>         Licata has a blog post on how knowing about equality in a
>         universe gives you things about equality of functions between
>         types in that universe.). In general, I think all you can say is
>         that if you can prove that `A -> B` is isomorphic to some
>         non-arrow-type `C` when you assume funext, then you can probably
>         embed `C` into `A -> B` even without funext.  So you can
>         lower-bound the number of distinct functions of a given type,
>         but you can't upper-bound it without funext in general. 
>         (Exception: you can upper-bound the number of functions from `A
>         -> B` when `A` is inhabited and `B` is not; the upper-bound is 0.)
>
>         I believe Pierre-Marie Pedrot has some models of type-theory (or
>         pointers to them) which contradict funext.  I'm not sure whether
>         or not any of them allow for multiple proofs of `A -> False`,
>         though I could believe that they might.
>
>         -Jason
>
>         On Tue, Jun 23, 2020, 22:25 Talia Ringer
>         <tringer AT cs.washington.edu <mailto:tringer AT cs.washington.edu>>
>         wrote:
>
>             Hi all,
>
>             I think this should be obvious, but I'm having trouble
>             thinking right now. I figure I'll ask in case somebody knows
>             the answer.
>
>             Suppose I have a type with decidable equality, like nat.
>             Then provably I have that all proofs of n = m for n m : nat
>             are equal to each other, without assuming UIP as an axiom.
>             That much I know.
>
>              From this, can I say anything about proofs of n <> m for n
>             m : nat without assuming functional extensionality? For
>             example, are all proofs of 0 <> 1 equal to each other? If
>             not, are they provably related in any interesting way?
>
>             Talia