le and ge not equivalent?

Stream: new members

[Calle Sönne]

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.

[Calle Sönne]

but the test lemma seems to imply they are different?

[Chris Hughes]

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

[Calle Sönne]

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

[Calle Sönne]

so I assume yes

[Patrick Massot]

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

[Chris Hughes]

Anyway, always use le

[Kevin Buzzard]

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