Zulip Chat Archive

Stream: new members

Topic: le and ge not equivalent?


view this post on Zulip Calle Sönne (Feb 22 2019 at 21:07):

Code:

lemma test (L : ) (h : L  0) (h₁ : 0  L): L < 0 :=
begin
rw le_iff_eq_or_lt at h₁,
rw le_iff_eq_or_lt at h,
end

Tactic state:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_3 ≤ ?m_4
state:
L : ℝ,
h : L ≥ 0,
h₁ : 0 = L ∨ 0 < L
⊢ L < 0

why is this happening? In my code where this originally happened I had just proved L ≥ 0 in a have statement, switching it to 0 ≤ L gave no errors as if they were the same.

view this post on Zulip Calle Sönne (Feb 22 2019 at 21:08):

but the test lemma seems to imply they are different?

view this post on Zulip Chris Hughes (Feb 22 2019 at 21:08):

rw requires syntactic equality, whereas have only requires definitional equality. For rw to work they have to look the same more or less.

view this post on Zulip Calle Sönne (Feb 22 2019 at 21:11):

Does simp also require syntactic equality? I switched rw into simp in code above, and it also gives an error.

view this post on Zulip Calle Sönne (Feb 22 2019 at 21:11):

so I assume yes

view this post on Zulip Patrick Massot (Feb 22 2019 at 21:15):

It would be easier to help if you could provide a true lemma that you'd like to prove

view this post on Zulip Chris Hughes (Feb 22 2019 at 21:19):

Anyway, always use le

view this post on Zulip Kevin Buzzard (Feb 22 2019 at 22:17):

Yes, rewrites are a great example of where definitional equality isn't good enough. I see this a lot in my code now, I don't know why. I have to use show to change my goal to something definitionally equal and then the rw works


Last updated: May 13 2021 at 16:25 UTC