Proving that ℕ is a preorder

Stream: new members

[Lars Ericson]

I'm trying to fill out a proof that ℕ is a preorder, using as much of ℕ as I can:

import algebra.group_with_zero.defs
import data.nat.basic
import init.meta.tactic

lemma nat_le_trans (a b c : ℕ ) : a ≤ b → b ≤ c → a ≤ c := nat.le_trans
#check nat.le_trans -- ?M_1 ≤ ?M_2 → ?M_2 ≤ ?M_3 → ?M_1 ≤ ?M_3
#check nat_le_trans -- nat_le_trans : ∀ (a b c : ℕ), a ≤ b → b ≤ c → a ≤ c

#check nat.lt_iff_le_not_le -- ?M_1 < ?M_2 ↔ ?M_1 ≤ ?M_2 ∧ ¬?M_2 ≤ ?M_1

lemma nat_lt_iff_le_not_le (α : Type *) (a b : α), a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac := sorry

instance : preorder ℕ := {
  le := (≤),
  le_refl := nat.le_refl,
  le_trans := nat_le_trans,
  lt_iff_le_not_le := nat_lt_iff_le_not_le,
}

There are a few issues:

1. I have to sugar nat.le_trans because it is not exactly in the form called for by

class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(lt := λ a b, a ≤ b ∧ ¬ b ≤ a)
(lt_iff_le_not_le : ∀ a b : α, a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac)

2. I don't know what . order_laws_tac does in a definition. I don't know where in TPIL to find the . notation for propositions. I don't understand the definition of

meta def order_laws_tac := whnf_target >> intros >> to_expr ``(iff.refl _) >>= exact

meta def whnf_target : tactic unit :=
target >>= whnf >>= change

meta occurs once in section 5.5 of TPIL and in the Lean reference manual it says "see chapter 7" which is basically a blank page. The meta language looks like a macro language.

The web page is not helpful because it states the axiom as

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

which clearly conveys that (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac" is a proposition that gets macro-expanded somehow. But order_laws_tac appears to be a recipe for proving a proposition, it is not the statement of a proposition, so I am stuck.

3. Even with the sorrys and what looks otherwise like correct form, the above doesn't work It breaks at

lemma nat_lt_iff_le_not_le (α : Type *) (a b : α), a < b ↔ (a ≤ b ∧ ¬ b ≤ a) . order_laws_tac := sorry

As always I would greatly appreciate some help on showing that ℕ is a preorder.

[Johan Commelin]

Have you tried removing the . order_laws_tac from that lemma statement?

[Johan Commelin]

Basically, you've already correctly inferred the answer to most of your questions.

[Johan Commelin]

. is a way to provide a recipe to automatically fill in the answer.

[Johan Commelin]

So you can just leave out the lt_iff_le_not_le field completely, and move on.

[Lars Ericson]

DONE

import data.nat.basic

lemma nat_le_trans (a b c : ℕ ) : a ≤ b → b ≤ c → a ≤ c := nat.le_trans

instance : preorder ℕ := {
  le := (≤),
  le_refl := nat.le_refl,
  le_trans := nat_le_trans,
}

PR for preorder?

[Johan Commelin]

Nope?

[Johan Commelin]

Sorry, why do you think this is not yet in mathlib?

[Johan Commelin]

I'm honestly confused.

[Bryan Gin-ge Chen]

import tactic
#check (by apply_instance: preorder ℕ)
/-
directed_order.to_preorder : preorder ℕ
-/

[Lars Ericson]

What is the recommended way to express the following? It says that, for any fixed n, fin n is a partial order, in 4 different ways:

import data.nat.basic

instance fin_n_partial_order (n: ℕ) : partial_order (fin n) :=
  subtype.partial_order (λ (i : ℕ), i < n)

lemma fin_n_partial_order1 (n: ℕ) : partial_order (fin n) :=
  subtype.partial_order (λ (i : ℕ), i < n)

def fin_n_partial_order2 (n: ℕ) : partial_order (fin n) :=
  subtype.partial_order (λ (i : ℕ), i < n)

example : (∀ n : ℕ , partial_order (fin n)) :=
begin
  intro h,
  exact subtype.partial_order (λ (i : ℕ), i < _),
end

[Bryan Gin-ge Chen]

There's already a partial_order instance on fin n for all n, so we would ordinarily just rely on type class inference to get this.

import tactic
#check (by apply_instance : ∀ n, partial_order (fin n))
/-
λ (n : ℕ), semilattice_inf.to_partial_order (fin n) : Π (n : ℕ), partial_order (fin n)
-/

[Lars Ericson]

Thanks, I didn't know I could put a quantifier in apply_instance, that's good to know.

[Eric Wieser]

Even if you couldn't, you could just use \lam _, by apply_instance

[Eric Wieser]

If you're trying to find an instance for something, my process is usually along the lines of:

• Assume you already have it (ie, just use mul_add and assume a distrib instance will be found)
• Use by apply_instance with #check or have : distrib T := just to double check the problem isn't something else (if that succeeds, it is)
• Try to find the file you'd expect to find the instance in, to work out what assumption you're missing
• Ask zulip to help with the above, or tell you that it doesn't exist