Zulip Chat Archive

Stream: new members

Topic: is less than transitive


view this post on Zulip Patrick Thomas (Oct 18 2020 at 19:05):

I seem to be stuck. Does this lemma actually hold? Am I missing an axiom? Did I define something wrong?

namespace hidden

class total_order (T : Type*) :=
(le : T  T  Prop)
(asymm :  x y : T, le x y  le y x  x = y)
(trans :  x y z : T, le x y  le y z  le x z)
(conn :  x y : T, le x y  le y x)


open total_order


-- s < t
def lt {T : Type*} [total_order T] (s t : T) : Prop := le s t  ¬ s = t


lemma lt_trans {T : Type*} [total_order T] {x y z : T} : lt x y  lt y z  lt x z :=
assume a1 : lt x y  lt y z,
have s1 : le x y := and.left (and.left a1),
have s2 : ¬ x = y := and.right (and.left a1),
have s3 : le y z := and.left (and.right a1),
have s4 : ¬ y = z := and.right (and.right a1),
have s5 : le x z := trans x y z (and.intro s1 s3),
sorry

end hidden

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:11):

The lemma is true

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:12):

And you don't need lt y z; it suffices to have le y z

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:12):

Once you know le x z, you need x ≠ z.

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:12):

By definition this is x = z → false

view this post on Zulip Patrick Thomas (Oct 18 2020 at 19:12):

That is where I am stuck.

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:13):

So, you can assume hxz : x = z

view this post on Zulip Yury G. Kudryashov (Oct 18 2020 at 19:13):

If you rewrite on this equality in s3, then you'll be able to apply asymm

view this post on Zulip Patrick Thomas (Oct 18 2020 at 19:14):

Ah! Thank you!


Last updated: May 08 2021 at 09:11 UTC