distinct

Stream: Is there code for X?

[Adam Topaz]

Suppose I have a type $\alpha$ and three terms $x,y,z : \alpha$. What's the idiomatic way to say that $x,y,z$ are distinct?

[Adam Topaz]

My inclination is to be tricky with matrices:

import data.matrix.notation

def distinct {α : Type*} (x y z : α) := function.injective ![x,y,z]

[Kevin Buzzard]

This came up on the discord and whatever the idiomatic way is, it was generally agreed that the most helpful way was just x \ne y \and y \ne z \and z \ne x. A more fun question: if alpha is linearly ordered and your goal is S_3-invariant, how do you now prove WLOG x<y<z?

[Adam Topaz]

Okay, but now what if I have 5 elements?

[Adam Topaz]

I don't want to write too many things

[Eric Wieser]

Possibly [x,y,z].pairwise (≠)

[Eric Wieser]

Which should still give you helpful induction principles

[Adam Topaz]

I would still like a smaller proof, but this isn't too bad:

import data.matrix.notation

example {α : Type*} {a b c d e f g : α} (cond : function.injective ![a,b,c,d,e,f,g]) : c ≠ g :=
cond.ne $ show (2 : fin 7) ≠ 6, by dec_trivial

[Kevin Buzzard]

Do you ever really have 5 elements in practice?

[Adam Topaz]

https://en.wikipedia.org/wiki/Complete_quadrangle

[Adam Topaz]

I can get by with 3, but I might need 5 in the future :)

[Adam Topaz]

I don't think I'll ever need 6 though.

[Adam Topaz]

This all started with the following lemma which I'm working on for some stuff with projective geometry:

lemma exists_unique_rep_of_colinear {x y z : proj K V} {v : V} :
  x.is_rep v → colinear x y z → (function.injective ![x,y,z]) →
  ∃! (w : V), y.is_rep w ∧ z.is_rep (v + w) := sorry

[Adam Topaz]

(in some sense, this is the key lemma that makes the fundamental theorem of projective geometry actually work.)