order_laws_tac error with partial_order

Stream: new members

[Fingy Soupy]

Hello, I'm attempting to construct an instance of partial_order for a type however I've run into an error I cannot make sense of when I construct the lt_iff_le_not_le field

type mismatch at field 'lt_iff_le_not_le'
  lt_iff_le_not_le
has type
  ∀ {a b : I}, a < b ↔ a ≤ b ∧ ¬b ≤ a
but is expected to have type
  auto_param (∀ (a b : I), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)

From the definition of preorder, I see that this field has a . after it:

(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)

After looking at the mathlib documentation, I learned that order_laws_tac is a tactic, however, I'm not sure what using a . and then a tactic does.
The documentation for order_laws_tac mentions the refl tactic but I constructed a linear_order for another type very similarly and did not run into this issue.

My full code up until this error is here:
https://gist.github.com/sjkillen/c815cd47e434b55befb8a1665b614b0f

Although I don't expect anyone to read through that mess and I hope that there's something that will either help me understand this error or to write a minimal example.

[Yaël Dillies]

This means that a < b is defined as a ≤ b ∧ ¬ b ≤ a by default and you must have defined it another way. . order_laws_tac is a way to automatically prove ∀ {a b}, a < b ↔ a ≤ b ∧ ¬b ≤ a when the default < is used (this is basically ust trying refl).

[Yaël Dillies]

You should either not define a custom < or prove that your custom < really respects a < b ↔ a ≤ b ∧ ¬b ≤ a.

[Yaël Dillies]

Oh sorry, rereading this, the problem is somewhere else. You simply didn't include the lt field in I.partial_order, so it defaulted to a ≤ b ∧ ¬ b ≤ a, meaning that your proof of a < b ↔ a ≤ b ∧ ¬ b ≤ a doesn't apply anymore because it's talking about a (definitionally different but propositionally equal) <. The fix is to simply include it:

instance : partial_order I :=
{ le := le,
  lt := lt,
  le_refl := le_refl,
  le_trans := @le_trans,
  le_antisymm := @le_antisymm,
  lt_iff_le_not_le := @lt_iff_le_not_le }

[Fingy Soupy]

Ah, that works thank you! :) and thank you for explaining order_laws_tac

[Fingy Soupy]

(deleted)