defining my own LinearOrder

Stream: mathlib4

[Michael]

As part of my project to express introductory topology assignments in Lean, I need to make statements about the properties of various sets under orderings that I define. (Maybe I want to give an unusual ordering to $\mathbb{R}$, or any ordering to $$\mathBB{R}^2$$ - whatever.)

I'd like to supply this ordering as a relation, a function from type to type to Prop. And I'd like to be able to work with the existing functionality defined for the LinearOrder class.

I can't figure out how this is supposed to be done. The most promising thing I see in the documentation is LinearOrder.lift', but (a) this appears to involve defining your own type that extends LinearOrder, and (b) I was defeated in my attempt to do this by an apparent need to define decidableLE for the new type. I have not found/understood documentation on what it means for something to be a DecidableRel or how to provide one to my LinearOrder instance.

I think there's just enough information in Mathematics in Lean that I could define a type outside of Mathlib that benefited from the < infix operator, but in that case I'd have to reimplement all the various theorems manipulating inequalities, just for that type.

Questions:

(1) What is the expected method of working with a custom ordering on a set?

(2) If it really is to extend LinearOrder for every ordering, how is that done?

[Yaël Dillies]

Your message seems to be confusing types and their terms several times:

• "a function from type to type to Prop" read literally means Type → Type → Prop. This is not what you want. Instead you want CustomType → CustomType → Prop, where you've previously defined CustomType : Type.
• "this appears to involve defining your own type that extends LinearOrder". No, it doesn't. Instead it states that if you have an injective map CustomType → ExistingLinearOrder and an instance LinearOrder ExistingLinearOrder then you can build an instance of LinearOrder CustomType

[Yaël Dillies]

What you want to do is

• Define CustomType. If you are going to equip an existing type with an unusual ordering, you will need to create a "type synonym". There are several ways to do that. The one that requires the less subtleties is to do something like structure CustomType where toReal : ℝ (assuming you want to equip ℝ with an unusual ordering)
• Write the LinearOrder CustomType instance. Start with

instance : LinearOrder CustomType where
  le a b := _
  le_refl a := _
  le_trans a b c hab hbc := _
  le_total a b := _

and fix the errors

[Damiano Testa]

... beginning with the Yaël code action that missed an underscore.

[Michael]

"this appears to involve defining your own type that extends LinearOrder". No, it doesn't.

What you want to do is

• Define CustomType.
• Write the LinearOrder CustomType instance.

How have I avoided defining my own type that extends LinearOrder by (1) defining my own type, and then (2) deriving it from LinearOrder?

"a function from type to type to Prop" read literally means Type → Type → Prop. This is not what you want.

I know that's not what I want; that's why Prop was capitalized and "type" wasn't, though this time around I forgot to put backquotes on Prop. My first draft of the message got erased.

and fix the errors

I already tried this, and noted the error that stopped me: I don't know how to provide decidableLE. How do I do that? You just told me to do what I already reported I had done, while completely failing to mention the thing that I asked for help with.

[Yaël Dillies]

Ah okay. "defining my own type that extends LinearOrder" means

structure CustomType extends LinearOrder SomeExistingType where
  one_more_field : SomeSort

[Yaël Dillies]

"extending" means to literally use the extends keyword

[Yaël Dillies]

If you don't know how to fill in decidableEq, you can always use the axiom of choice in the form of docs#Classical.decRel :

instance : LinearOrder CustomType where
  le a b := _
  le_refl a := _
  le_trans a b c hab hbc := _
  le_total a b := _
  decidableEq := Classical.decRel _

[Yaël Dillies]

This is "cheating", but sometimes there's no way not to cheat (eg equality on ℝ is not algorithmically decidable)

[Michael]

Yaël Dillies said:

If you don't know how to fill in decidableEq, you can always use the axiom of choice in the form of docs#Classical.decRel :

I suspect that, for a case where I draw on the LinearOrder already associated with an underlying type, I should be able to use that LinearOrder's decidability fields to provide my own proof of decidability. I assume this would defer whether classical reasoning was required to the LinearOrder on the underlying type.

Is that right? How can I do that? I've tried defining a function that invokes underlying decidableEq / decidableLE fields, but just joining them together with logical connectives and returning that seems to be an error.

@[ext]
structure DictPoint (α β : Type*) [LinearOrder α] [LinearOrder β]
    where
  mk' :: (point : α × β)

namespace DictPoint

def lt {α β : Type*} [LinearOrder α] [LinearOrder β]
  := λ (p₁ p₂ : DictPoint α β) ↦
    p₁.point.1 < p₂.point.1 ∨
    p₁.point.1 = p₂.point.1 ∧ p₁.point.2 < p₂.point.2

end DictPoint

instance {α β : Type*} [LinearOrder α] [LinearOrder β]
    : LinearOrder (DictPoint α β) where
  -- [...]
  decidableLE := -- this doesn't work
    λ p₁ p₂ {αₒ : LinearOrder α} {βₒ : LinearOrder β} ↦
      αₒ.decidableLT p₁.point.1 p₂.point.1 ∨
      αₒ.decidableEq p₁.point.1 p₂.point.1 ∧ αₒ.decidableLE p₁.point.2 p₂.point.2

My best guess here is that logical connectives don't work with the Decidable type, but who knows. Is there some documentation somewhere on what the various DecidableX things mean, what they are, and how to work with them?

[Michael]

(My hope is that the DictPoint.lt function can be directly associated with the < operator on that compositely-typed LinearOrder once it's successfully defined. I am not sure that's the case right now; if you see an obvious pitfall, please let me know.)

[Yaël Dillies]

The Decidable instance you're missing is docs#Prod.Lex.decidable

[Michael]

that was a little too cryptic for me to understand

[Yaël Dillies]

A Decidable p instance is an algorithm for deciding whether p is true or false. Given algorithms for deciding whether p₁.point.1 < p₂.point.1, p₁.point.1 = p₂.point.1, p₁.point.2 < p₂.point.2 are true or false, can you write an algorithm for deciding whether p₁.point.1 < p₂.point.1 ∨ p₁.point.1 = p₂.point.1 ∧ p₁.point.2 < p₂.point.2 is true or false?

[Yaël Dillies]

(the answer lies within docs#And.decidable and docs#Or.decidable, but you might want to try writing the algorithm yourself as an exercise)

[Michael]

well, without looking at anything...

I can write such an algorithm in general, and it would look exactly like that. Ignoring the illegal identifiers, the description of that algorithm in C would be p₁.point.1 < p₂.point.1 || (p₁.point.1 == p₂.point.1 && p₁.point.2 < p₂.point.2).

If I want to do the whole thing in nothing but if-else, a lisp version might look something like this:

(defun (dle p1 p2 linear-order-1 linear-order-2)
  (if (funcall (get-dlt linear-order-1) (car p1) (car p2))
    't
    (if (funcall (get-deq linear-order-1) (car p1) (car p2))
      (if (funcall (get-dle linear-order-2) (cadr p1) (cadr p2))
        't
        nil)
      nil)))

I don't think I can make do with a single decidable comparison function, but a set of two like decidableLT and decidableEq or decidableLE and decidableNot (?) should do the job.

I'm a little bemused, I guess, by the description of Decidable, which says "Decidable p is a data-carrying class that supplies a proof that p is either true or false. " and goes on to note that it is equivalent to Prop. From what I've been able to glean, p itself is already a proof that p is either true or false - though formally it seems to be a proof that p is either True or False, not true or false - so this sounds like a data-carrying class with two fields that are guaranteed to be identical to each other.

What am I missing?

[Michael]

I guess decidable NAND would do the job, but that doesn't seem to be provided by default, and I don't want to deal with NAND anyway.

[Yaël Dillies]

Have you looked at the definition of docs#Decidable ?

[Yaël Dillies]

It is an inductive type with two constructors. If you want to write an algorithm, you need to start by pattern-matching on what constructor your Decidable (p₁.point.1 < p₂.point.1) is.

[Yaël Dillies]

Start with this:

def decidable_and {p q : Prop} : Decidable p → Decidable q → Decidable (p ∧ q) := sorry

[Michael]

if you're having fun instructing me, or you think this might be edifying for other people, here are the problems I'm encountering:

def decidable_and {p q : Prop} (dp : Decidable p) (dq : Decidable q)
    : Decidable p → Decidable q → Decidable (p ∧ q) :=
  match dp with
  | isFalse p => isFalse (p ∧ q) -- p has the wrong type
  | isTrue p =>
    match dq with
    | isFalse q => isFalse (p ∧ q)
    | isTrue q => isTrue (p ∧ q)

I know that's the wrong skeleton, but I started there because it made more sense to me.

def decidable_and {p q : Prop}
    : Decidable p → Decidable q → Decidable (p ∧ q) :=
  λ dp dq ↦
    match dp with
    | isFalse (hₚ : Not p) => isFalse (Not (p ∧ q)) -- argument `¬(p ∧ q)` has type `Prop : Type` but is expected to have type `¬(p ∧ q) : Prop`
    | isTrue h₁ =>
      match dq with
      | isFalse h₂ => isFalse (h₁ ∧ h₂) -- similar type error
      | isTrue h₂ => isTrue (h₁ ∧ h₂) -- similar type error

One problem seems to be that my variables have type "a particular Prop" when they should have type "the Prop type itself", I think. And/or the other way around. The other one has to do with Decidable p having the constructors isFalse (Not p) and isTrue p, which I hate. That suggests to me that all Decidable propositions are true, and leaves me unsure of how to correctly deconstruct a Decidable. But that second one is also the kind of thing I hope I could work out on my own.

If I'm wearing on you, I can go consult the docs for And.decidable and Or.decidable that you mentioned.

[Michael]

Changing the result type of my "intuitive" approach (the first one) from Decidable p → Decidable q → Decidable (p ∧ q) to Decidable (p ∧ q) struck me as probably wise, but didn't resolve anything.

[Yaël Dillies]

Do you know that

:= λ x ↦ match x with
| pat1
| pat2

is the same as

| pat1
| pat2

[Michael]

I didn't know that and the example leaves me unsure what to do with it now;

def decidable_and {p q : Prop}
  : Decidable p → Decidable q → Decidable (p ∧ q)
  | isFalse hₚ => λ _ ↦ isFalse ¬(p ∧ q)
  | isTrue hₚ =>
    | isFalse h₂ => isFalse ¬(p ∧ q)
    | isTrue h₂ => isTrue (p ∧ q)

produces an error saying there's space in front of the second level of | .

(The reason the subscripts are p and 2 is that, if I attempt to type \_q, I get a subscript a followed by an ordinary q. I have no idea what's responsible for that; it isn't my keyboard. This appears to be a matter of which Unicode subscript characters exist and which don't.)

[Timo Carlin-Burns]

That shorthand only works at the very beginning of a definition when used instead of :=.

[Timo Carlin-Burns]

You can go back to using match for the inner cases or you can turn the whole thing into cases at the beginning like this

def decidable_and {p q : Prop}
  : Decidable p → Decidable q → Decidable (p ∧ q)
  | isFalse hₚ, _ => isFalse sorry
  | isTrue hₚ, isFalse h₂ => isFalse sorry
  | isTrue hₚ, isTrue h₂ => isTrue sorry

[Timo Carlin-Burns]

Your problem besides the syntax is that you're providing propositions like p \and q to isTrue when it expects a proof of that proposition

[Michael]

From what I've been able to glean, p itself is already a proof that p is either true or false

TPIL puts a lot of emphasis on the idea that the proposition p is, by internal representation, a proof that p is true.

Why is that not true in this case?

[Michael]

Here's something else that doesn't work:

def decidable_and₂ {p q : Prop}
  : Decidable p → Decidable q → Decidable (p ∧ q)
  | isTrue h₁, isTrue h₂ => isTrue (h₁ ∧ h₂)
  -- [...]

Here our first argument has type Decidable p, and we match it against the pattern isTrue h₁. So we have a hypothesis h₁ : Prop that says "p is true".

This hypothesis is useless because it apparently has no logical value. The error Lean emits for this complains that And cannot work with h₁, because it's not a proposition and And can only work with propositions.

[Michael]

example : (p : Prop) → p := by
  intro h
  assumption -- doesn't work
  done

example (p : Prop) : p → p := by
  intro h
  assumption -- works fine

I assume this is the same difference. What is that difference?

[Michael]

(The first of those examples gets pretty-printed as ∀ (p : Prop), p, the claim that all propositions are true. I think it should be the claim that all propositions imply themselves; it says that the proposition p implies p.)

[Michael]

(However, as far as I recall it is actually the case that all propositions are true - the only values are True and False, and False has no introductions. No?)

[Kim Morrison]

You are confusing levels. False has no introductions, yet it is a Prop.

[Michael]

But, if a Prop exists, it isn't False.

[Michael]

This works:

def decidable_and₃ {p q : Prop}
  : Decidable p → Decidable q → Decidable (p ∧ q)
  | isFalse h₁, _ =>
    have hn : ¬(p ∧ q) := by
      intro hc
      exact h₁ hc.left
    isFalse hn
  | _, isFalse h₂ =>
    have hn : ¬(p ∧ q) := by
      intro hc
      exact h₂ hc.right
    isFalse hn
  | isTrue h₁, isTrue h₂ => isTrue (And.intro h₁ h₂)

but my approach to trying this solution was to think "how would I get the IDE into 'proving mode'?", which leaves something to be desired.

[Michael]

re: only one possible value of any Prop, am I misinterpreting this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Natural.20Number.20Game/near/418428611 ?

[Michael]

(and for completeness, a terser version of decidable_and:

def decidable_and₄ {p q : Prop}
    : Decidable p → Decidable q → Decidable (p ∧ q)
  | isFalse h₁, _ => isFalse (λ (c : p ∧ q) ↦ h₁ c.left)
  | _, isFalse h₂ => isFalse (λ (c : p ∧ q) ↦ h₂ c.right)
  | isTrue h₁, isTrue h₂ => isTrue (And.intro h₁ h₂)

Here the algorithm for deciding whether p ∧ q is true has morphed from "well, it's true if they're both true, and false otherwise" to "well, if either of them is false, that would contradict the premise that p ∧ q is true".)

[Kevin Buzzard]

Michael said:

But, if a Prop exists, it isn't False.

What does that even mean?

#check False -- no error!

It exists!

[Michael]

Kevin Buzzard said:

Michael said:

But, if a Prop exists, it isn't False.

What does that even mean?

Possibly a good question. Why are AA and ZZ necessarily equal to each other?

If the only way to create a value of type Prop is by introducing True, then all Props must be true.

[Yaël Dillies]

You're mistaking terms and their types. 0 = 1 and 1 = 1 are both propositions. Only one of them is true.

[Kevin Buzzard]

Given that 2+2=5 is clearly a Prop and it's clearly not true, there has to be something wrong with your thinking

[Kevin Buzzard]

When I'm introducing Props to my students I refer to them for a while as "true/false statements".

[Yaël Dillies]

Lean implements two axioms, which you might be confusing:

• Propositional extensionality: If two propositions are equivalent, then they are equal: (p ↔ q) → (p = q)
• Proof irrelevance: If h and h' are two proofs of the same proposition, then they are equal: h h' : p, h = h'

[Yaël Dillies]

Further, we have the law of excluded middle, which says that every proposition is equivalent to either True or False

[Kevin Buzzard]

In the world of sets, the analogous situation is: the empty set exists but it doesn't have any elements, so the elements of the empty set don't exist.

[Yaël Dillies]

So the full picture is:

• Prop has two terms: True and False (note this is only provable assuming LEM)
• False has no term
• True has one term

[Michael]

Yaël Dillies said:

Lean implements two axioms, which you might be confusing:

• Propositional extensionality: If two propositions are equivalent, then they are equal: (p ↔ q) → (p = q)
• Proof irrelevance: If h and h' are two proofs of the same proposition, then they are equal: h h' : p, h = h'

Am I confusing those two with each other, or one of them with something else?

[Yaël Dillies]

You tell me!

[Kevin Buzzard]

Historically people took a long time to recognise 0 as a number for the same reason -- it represents the idea that something doesn't exist, but it itself exists.

[Michael]

It seems clear to me that if h and h' are two proofs of the same proposition, then h ↔ h' holds, which would make it difficult to confuse propositional extensionality with proof irrelevance. But that could be an argument that I'm not confusing them with each other, or that I am. So that's about all I can say about it.

[Michael]

The followup comment seems likely to be that ↔ is meant for variables of type Prop : Type and proof irrelevance is meant for variables of type [XXX] : Prop.

[Michael]

Kevin Buzzard said:

Given that 2+2=5 is clearly a Prop and it's clearly not true, there has to be something wrong with your thinking

For this one, you're exhibiting a way to create Props other than by introducing True. It is a good point and it doesn't agree well with what I've been absorbing about Lean from the documentation and other recent questions. It raises my interest in why AA and ZZ are necessarily equal to each other.

[Yaël Dillies]

Michael said:

It seems clear to me that if h and h' are two proofs of the same proposition, then h ↔ h' holds, which would make it difficult to confuse propositional extensionality with proof irrelevance.

h ↔ h' doesn't make sense because h h' : p, not h h' : Prop

[Michael]

Hey, I anticipated the followup comment :tada:

Moving back up the Great Tree of Thread Topics, figuring out decidable_and hasn't gotten me very far in implementing decidableLE:

-- just for context
structure DictPoint (α β : Type*) [LinearOrder α] [LinearOrder β]
    where
  mk' :: (point : α × β)

namespace DictPoint

def mk := λ {α β : Type*} (a : α) (b : β) [LinearOrder α] [LinearOrder β]
  ↦ DictPoint.mk' (Prod.mk a b)

def lt {α β : Type*} [LinearOrder α] [LinearOrder β]
  := λ (p₁ p₂ : DictPoint α β) ↦
    p₁.point.1 < p₂.point.1 ∨
    p₁.point.1 = p₂.point.1 ∧ p₁.point.2 < p₂.point.2

end DictPoint

instance {α β : Type*} [LinearOrder α] [LinearOrder β]
    : LinearOrder (DictPoint α β) where
  -- [...]
  decidableLE :=
    λ (p₁ p₂ : DictPoint α β) {αₒ : LinearOrder α} {βₒ : LinearOrder β} ↦
      let high₁ := p₁.point.1
      match (αₒ.decidableLT p₁.point.1 p₂.point.1) with
      | isTrue hhlt => isTrue sorry
      | isFalse hhge => isFalse sorry -- wrong, placeholder

This produces a type error on let high₁ := p₁.point.1, which doesn't seem right. There are also type errors on the other X.point.1 accesses. And a general problem with working in the definition of decidableLE is that the infoview often shows nothing where I'm hoping for stuff to be present.

[Michael]

How can let [name] := [expression] have a type error?

[Kevin Buzzard]

Can you make a #mwe ? I have errors when I cut and paste your code

[Kevin Buzzard]

Just put sorry to make things work, don't create errors

[Michael]

import Mathlib.Data.Real.Basic

@[ext]
structure DictPoint (α β : Type*) [LinearOrder α] [LinearOrder β]
    where
  mk' :: (point : α × β)

namespace DictPoint

def mk := λ {α β : Type*} (a : α) (b : β) [LinearOrder α] [LinearOrder β]
  ↦ DictPoint.mk' (Prod.mk a b)

def lt {α β : Type*} [LinearOrder α] [LinearOrder β]
  := λ (p₁ p₂ : DictPoint α β) ↦
    p₁.point.1 < p₂.point.1 ∨
    p₁.point.1 = p₂.point.1 ∧ p₁.point.2 < p₂.point.2

end DictPoint

instance {α β : Type*} [LinearOrder α] [LinearOrder β]
    : LinearOrder (DictPoint α β) where
  le := λ p₁ p₂ ↦ (DictPoint.lt p₁ p₂) ∨ p₁ = p₂
  le_refl := by simp
  le_trans := by sorry
  le_antisymm := by sorry
  decidableLE :=
    λ (p₁ p₂ : DictPoint α β) {αₒ : LinearOrder α} {βₒ : LinearOrder β} ↦
      let high₁ := p₁.point.1
      match (αₒ.decidableLT p₁.point.1 p₂.point.1) with
      | isTrue hhlt => isTrue sorry
      | isFalse hhge => isFalse sorry -- wrong, placeholder

[Kevin Buzzard]

α: Type u_1
β: Type u_2
inst✝¹: LinearOrder α
inst✝: LinearOrder β
p₁p₂: DictPoint α β
αₒ: LinearOrder α
βₒ: LinearOrder β
⊢ ?m.2528 p₁ p₂

says "you have two unrelated linear order structures on alpha".

[Michael]

I'm not convinced that Decidable.isTrue sorry is correct syntax, but I'm having a hard time addressing that because of the other errors.

[Michael]

ughh

[Kevin Buzzard]

So a < b is ambiguous right now which is not a good sign

[Michael]

Really? Don't the two LinearOrders on alpha have to coincide with each other?

[Kevin Buzzard]

No, definitely not! Why should they?

[Michael]

Well, because they're automatically derived from context? Why are they defined at all?

[Kevin Buzzard]

The thing I posted is the exact state of Lean's brain at the point of the first error, and you can just read it, all the assumptions Lean knows are there. It says that alpha and beta are types, and you have two unrelated linear orders on each of them.

[Kevin Buzzard]

instance {α β : Type*} [LinearOrder α] [LinearOrder β]
    : LinearOrder (DictPoint α β) where
  le := λ p₁ p₂ ↦ (DictPoint.lt p₁ p₂) ∨ p₁ = p₂
  le_refl := by simp
  le_trans := by sorry
  le_antisymm := by sorry
  decidableLE := by
    sorry
  le_total := sorry

Now at the decidableLE goal the brain (i.e. the local context) is

α: Type u_1
β: Type u_2
inst✝¹: LinearOrder α
inst✝: LinearOrder β
⊢ DecidableRel fun x x_1 ↦ x ≤ x_1

which looks much better

[Michael]

The reason I have the named LinearOrders in decidableLE is that I want to call their decidableXX functions.

The reason I haven't lifted that naming out to the declaration that DictPoint instances are also LinearOrder instances is that I don't want to be calling [LinearOrder_name].le instead of using ≤ notation, in the other proofs.

[Kevin Buzzard]

1) You didn't name the linear orders, you made new ones
2) if you want to name linear orders then do it here

instance {α β : Type*} [name1 : LinearOrder α] [name2 : LinearOrder β]

[Michael]

if I just name the LinearOrders at the top level (instance {α β : Type*} { something: LinearOrder α} {somethingelse : LinearOrder β, they'll still work the same way as the implicit ones?

[Michael]

sounds like it

[Michael]

Kevin Buzzard said:

The thing I posted is the exact state of Lean's brain at the point of the first error, and you can just read it, all the assumptions Lean knows are there. It says that alpha and beta are types, and you have two unrelated linear orders on each of them.

How did you call that message up? For me the infoview shows various instances of

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  αₒ
inferred
  inst✝¹

[Michael]

Kevin Buzzard said:

1) You didn't name the linear orders, you made new ones
2) if you want to name linear orders then do it here

instance {α β : Type*} [name1 : LinearOrder α] [name2 : LinearOrder β]

wait, followup question: your named LinearOrders are still notated in [] square brackets. My understanding was that the meaning of the [] is that you don't provide a name for the value, which is why in my code I have {}.

[Kevin Buzzard]

Screenshot-from-2024-03-01-11-19-55.png

My cursor is at the beginning of the first error (just before the p).

[Michael]

  decidableLE :=
    λ p₁ p₂ ↦
      let high₁ := p₁.point.1
      let high₂ := p₂.point.1
      match (αₒ.decidableLT high₁ high₂) with
      | isTrue hhlt =>
        have hd : this.le p₁ p₂ := by -- error, there is no le
          simp at hhlt
      sorry
      | isFalse hhge => isFalse sorry -- wrong, placeholder

Here, this.le doesn't refer to anything. Also invalid are le p₁ p₂ and p₁ ≤ p₂. I was able to use expressions of the form p₁ ≤ p₂ in the definition of le_trans, and they use the definition of le provided above them. What's different in decidableLE?

[Kevin Buzzard]

What is αₒ? Can you post all the code that you changed since the last time you posted a MWE?

[Michael]

It's the linear order on alpha; other than naming the linear orders at the top level, that is all the code I've changed. But here's the mwe form again, with a line in le_trans to show correct synthesis of the ability to use the notation there:

import Mathlib.Data.Real.Basic

@[ext]
structure DictPoint (α β : Type*) [LinearOrder α] [LinearOrder β]
    where
  mk' :: (point : α × β)

namespace DictPoint

def mk := λ {α β : Type*} (a : α) (b : β) [LinearOrder α] [LinearOrder β]
  ↦ DictPoint.mk' (Prod.mk a b)

def lt {α β : Type*} [LinearOrder α] [LinearOrder β]
  := λ (p₁ p₂ : DictPoint α β) ↦
    p₁.point.1 < p₂.point.1 ∨
    p₁.point.1 = p₂.point.1 ∧ p₁.point.2 < p₂.point.2

end DictPoint

instance {α β : Type*} {αₒ : LinearOrder α} {βₒ : LinearOrder β}
    : LinearOrder (DictPoint α β) where
  le := λ p₁ p₂ ↦ (DictPoint.lt p₁ p₂) ∨ p₁ = p₂
  le_refl := by simp
  le_trans := by
    intro a b c
    sorry
  le_antisymm := by sorry
  le_total := by sorry
  decidableLE :=
    λ p₁ p₂ ↦
      let high₁ := p₁.point.1
      let high₂ := p₂.point.1
      match (αₒ.decidableLT high₁ high₂) with
      | isTrue hhlt =>
        have hd : p₁ ≤ p₂ := by
          simp at hhlt
      sorry
      | isFalse hhge => isFalse sorry -- wrong, placeholder

[Jon Eugster]

I haven't thought at all about how your proof goes, but would you need to define the LE and LT instances for your DictPoint? Here is an example that at least compiles without error:

import Mathlib.Data.Real.Basic

@[ext]
structure DictPoint (α β : Type*) [LinearOrder α] [LinearOrder β]
    where
  mk' :: (point : α × β)

namespace DictPoint

def mk := λ {α β : Type*} (a : α) (b : β) [LinearOrder α] [LinearOrder β]
  ↦ DictPoint.mk' (Prod.mk a b)


def lt {α β : Type*} [LinearOrder α] [LinearOrder β]
  := λ (p₁ p₂ : DictPoint α β) ↦
    p₁.point.1 < p₂.point.1 ∨
    p₁.point.1 = p₂.point.1 ∧ p₁.point.2 < p₂.point.2

instance {α β : Type*} [LinearOrder α] [LinearOrder β] : LT <| DictPoint α β where
  lt := lt

def le {α β : Type*} [LinearOrder α] [LinearOrder β] := fun (p q : DictPoint α β) => p < q ∨ p = q

-- Add LE instance
instance {α β : Type*} [LinearOrder α] [LinearOrder β] : LE <| DictPoint α β where
  le := fun p q => p < q ∨ p = q

end DictPoint

instance {α β : Type*} [α₀ : LinearOrder α] [LinearOrder β] : LinearOrder (DictPoint α β) where
  le_refl := sorry
  le_trans := sorry
  le_antisymm := sorry
  le_total := sorry
  decidableLE a b := show Decidable (a ≤ b) from
    match α₀.decidableLT a.point.1 b.point.1 with
    | isTrue (h : a.point.1 < b.point.1) => sorry
    | isFalse (h : ¬ (a.point.1 < b.point.1)) => sorry

[Michael]

I have been worrying about defining LE and LT on DictPoint. It appears to me that, within the body of the instance declaration, LE is defined and LT isn't, which I find weird.

In this particular instance, LE seems to be defined while I'm defining le_trans, but not while I'm defining decidableLE, which I find much weirder.

[Michael]

My understanding was that the LinearOrder on a DictPoint type defines the LE and LT notation for the type...?

[Kevin Buzzard]

But not in time for you to use them. This is why Jon's approach is better

[Michael]

But not in time for you to use them.

How come one of them is usable in my le_trans?

[Michael]

Also, I tend to object to the fact that saying "when alpha and beta have LinearOrders, there is a LinearOrder on the DictPoint type as follows: to decide whether p_1 < p_2, find the LinearOrders on alpha and beta, and then..." creates an error complaining that the implicit LinearOrder on alpha when I'm defining the LinearOrder on a DictPoint might be different from the implicit LinearOrder on alpha when I'm defining the implementation of that LinearOrder's decidableLE method...

...but then defining an independent LE.le for the type I'm about to define a LinearOrder on is not just not a conflict with the LE.le provided by the LinearOrder, it's required.

[Yaël Dillies]

Kevin Buzzard said:

But not in time for you to use them. This is why Jon's approach is better

I'm actually not sure what you mean here, Kevin

[Kevin Buzzard]

import Mathlib.Tactic

example (X : Type) : PartialOrder X where
  le x y := True
  le_refl := by
    intro a
    have foo : a ≤ a := by sorry -- failed to synthesize instance LE X
  le_trans := sorry
  le_antisymm := sorry

[Kevin Buzzard]

But making the LE instance first avoids this.

[Michael]

The le_refl example bothered me, because by my standard LE is also available there!

Turns out, LE in the goal is fine, and it uses the relation defined by the LinearOrder. (Note that the goal when providing a proof of le_refl is a ≤ a, and it simplifies just fine.) But using LE outside the goal, during your proof, is wrong and meaningless.

Why the difference?

[Michael]

It's also possible to introduce a proof that a ≤ b from a protasis in the goal (le_trans defines a goal of this type), and that is given the expected meaning, even though it's no longer in the goal. But you can't define your own propositions that way?

[Jon Eugster]

This might be slightly inaccurate, but there are two different things happening regarding the ≤ symbol.

1) In the infoview, you have a term like @LE.le X (@LE.mk X fun (x y : X) => True) a a which gets "delaborated" (aka. displayed) as a ≤ a. (you can see this by setting set_option pp.all true above your proof).

2) When you want to write ≤ yourself in code, this needs to be parsed, and that happens by using this macro from core:

macro_rules | `($x ≤ $y)  => `(binrel% LE.le $x $y)

Lean needs to find an instance of LE X to do so. But instance inference cannot find this adhoc instance (@LE.mk X fun (x y : X) => True), which is created through the le field (and some others) in your structure. I guess because that one is never added (or rather, not added yet), but that's where I'm not super sure...

You can still do what Kevin does, just without using the notation:

import Mathlib.Tactic

example (X : Type) : PartialOrder X where
  le x y := True
  le_refl := by
    intro a
    have foo : (LE.mk fun (x y : X) => True).le a a := by dsimp
    -- in the infoview you see: `foo : a ≤ a`
    exact foo
  le_trans := sorry
  le_antisymm := sorry

[Luigi Massacci]

Somewhat unrelated to linear orders, but hijacking the initial discussion on Prop-s:

Yaël Dillies said:

So the full picture is:

• Prop has two terms: True and False (note this is only provable assuming LEM)
• False has no term
• True has one term

@Michael, try making sense of this if you want to have some fun:

example : ¬(∃ P : Prop, ¬(True ↔ P) ∧ ¬(False ↔ P)) :=
  fun ⟨_, npt, npf⟩ ↦ npf ⟨fun f ↦ f.elim, fun p ↦ npt ⟨fun _ ↦ p, fun _ ↦ trivial⟩⟩

Or even worse if you like propositional extensionality:

example : ¬(∃ P : Prop, True ≠ P ∧ False ≠ P) :=
  fun ⟨_ , npt, npf⟩ ↦ npf <| propext ⟨fun f ↦ f.elim, fun p ↦ npt <| propext ⟨fun _ ↦ p, fun _ ↦ trivial⟩⟩

note that LEM was not used anywhere at all (as you can see from the lack of imports)

[Mario Carneiro]

LEM was not used anywhere at all (as you can see from the lack of imports)

You don't need an import to use classical logic, Classical.em is defined in the Init package which is available by default

[Mario Carneiro]

you don't even need to use Classical in your code directly; things like by_contra, by_cases and split will automatically use classical logic, and are available without imports

[Luigi Massacci]

Ahhh, I should have remebered the discussion about LEM in split and deduced the rest, thank you for the clarification. Having said that, @Michael you can still verify I’m not lying with #print axioms (assuming @Mario Carneiro won’t come out and show that even that can be bypassed in some way…)

[Mario Carneiro]

(it can, but the code that does generally looks decidedly adversarial / malicious. You won't run into it using lean/mathlib normally.)

[Mario Carneiro]

import Lean

open Lean in
elab "#print axioms " n:ident : command => do
  logInfo m!"'{n}' does not depend on any axioms... jk lol"

theorem totally_intuitionistic {p} : p ∨ ¬p := Classical.em p

#print axioms totally_intuitionistic
-- 'totally_intuitionistic' does not depend on any axioms... jk lol

[Mario Carneiro]

See also #general > PSA about trusting Lean proofs