The Coq mailing list

[Guillaume Allais <guillaume.allais AT ens-lyon.org>]

I expect you could get uniqueness of proofs of `m <> n` if you
were willing to use `False` defined in `SProp` rather than `Prop`
(I don't have a version of Coq with `SProp` installed so cannot
check myself but we had a similar discussion on the agda-stdlib
a little while ago).

As for the general case, I suspect you ought to be able to *compute*
the inductive description of proofs of `m <> n` for inductive types
by using a zipper-like construction essentially representing a path
exploring the two trees in lock-step and pointing to the first
mismatch it can find.

For a binary tree you would have something of the sort
(using a left-to-right DFS):

Inductive BTree : Type
  := Leaf
   | Node : BTree -> BTree -> BTree.

Inductive Neq : BTree -> BTree -> Set
  (* Constructor mismatch *)
  := LeafNode  : forall l r, Neq Leaf (Node l r)
   | NodeLeaf  : forall l r, Neq (Node l r) Leaf
  (* (Equal) clowns to the Left, Jokers to the right *)
   | NodeLeft  : forall l1 l2 r1 r2, Neq l1 l2 -> Neq (Node l1 r1) (Node l2 
r2)
   | NodeRight : forall l r1 r2, Neq r1 r2 -> Neq (Node l r1) (Node l r2)
   .

You can easily prove

Neq_is_neq : forall t1 t2, Neq t1 t2 -> t1 <> t2.
eq_or_Neq : forall t1 t2, (t1 = t2) + Neq t1 t2.

Proving

Neq_pi : forall t1 t2 (p q : Neq t1 t2), p = q.

is not too bad using the coq-equations plugin. I have put everything up
here in case someone is interested:
https://github.com/gallais/potpourri/blob/master/coq/poc/Neq.v

Of course once you start storing data inside the tree, you'll need
hypotheses about the uniqueness of the proofs of (in)equatility for
this value type to prove uniqueness of the proofs relating the trees.

Cheers,

On 24/06/2020 10:37, Thorsten Altenkirch wrote:
> Coming to this discussion a bit late but here we have an inductive 
> characterisation of inequality that is m <> n <-> m<n \/ n<m. You can prove 
> UIP for the right hand side but not for the left because without funext you 
> can prove nothing non-trivial about functions.
> 
> Thorsten
> 
> From: <coq-club-request AT inria.fr> on behalf of Xavier Leroy 
> <xavier.leroy AT college-de-france.fr>
> Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
> Date: Wednesday, 24 June 2020 at 08:07
> To: "coq-club AT inria.fr" <coq-club AT inria.fr>
> Subject: Re: [Coq-Club] Silly question about decidable equality and 
> inequality
> 
> On Wed, Jun 24, 2020 at 8:52 AM Talia Ringer 
> <tringer AT cs.washington.edu<mailto:tringer AT cs.washington.edu>> 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.
> 
> Right.  There are many other ways to write this subset type that behave 
> well w.r.t. equality:
> 
> { n : nat | Nat.eqb n 0 = false }
> { n : nat | 0 < n }         (* I believe that Nat.le and Nat.lt have unique 
> proofs *)
> { n : nat | match n with O => False | S _ => True end }
> 
> etc.
> 
> - Xavier Leroy
> 
> 
> 
> (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
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
>