Zulip Chat Archive

Stream: general

Topic: linarith and ordinal file


view this post on Zulip Sebastien Gouezel (Jul 19 2020 at 13:49):

I have tried to use linarith in the file set_theory/ordinal.lean, but it doesn't work. The minimal example is as follows. Import tactic.linarith at the top of the file. In the middle of the file (Line 996), there is

theorem zero_lt_one : (0 : ordinal) < 1 :=
lt_iff_le_and_ne.2 zero_le _, ne.symm $ ordinal.one_ne_zero

Now, try pasting a linarith lemma before this lemma. It works. After the lemma, it fails.

lemma works {a b : } (hab : a  b) (h : b < a) : false :=
begin
  linarith,
end

theorem zero_lt_one : (0 : ordinal) < 1 :=
lt_iff_le_and_ne.2 zero_le _, ne.symm $ ordinal.one_ne_zero

lemma fails {a b : } (hab : a  b) (h : b < a) : false :=
begin
  linarith,
end

So I guess linarith gets confused in some way by the ordinal lemma zero_lt_one.

view this post on Zulip Rob Lewis (Jul 19 2020 at 14:50):

(deleted)

view this post on Zulip Rob Lewis (Jul 19 2020 at 14:56):

#3455

view this post on Zulip Sebastien Gouezel (Jul 19 2020 at 15:09):

Thanks!


Last updated: May 11 2021 at 21:10 UTC