## Stream: new members

### Topic: trivial ordering

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:05):

Hey, quick question. I was wondering if there was a canonical way to show that i < j for two naturals i and j where their value is known.

I know I can repeatedly apply nat.le_of_succ_le_succ and then use nat.zero_le, but that feels very cumbersome for proving something that's trivially true

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:06):

Or rather the inverse of le_of_succ_le_succ, succ_le_succ I think?

#### Kevin Buzzard (Feb 09 2020 at 23:09):

norm_num

#### Kevin Buzzard (Feb 09 2020 at 23:10):

import tactic

example : 12345 < 67890 := by norm_num


#### Kevin Buzzard (Feb 09 2020 at 23:10):

NB it only works if i is actually less than j.

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:10):

:pray:

I knew there had to be a better way

#### Kevin Buzzard (Feb 09 2020 at 23:10):

When I asked that question a couple of years ago, there wasn't ;-)

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:11):

Hahahaha, glad to be here at Lean 3

#### Kevin Buzzard (Feb 09 2020 at 23:11):

I had Lean 3, it was just that import tactic imported far fewer tactics.

Ah gotcha

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:12):

Also I finished Natural Number Game recently, I really like what you and Mohammed put together

#### Kevin Buzzard (Feb 09 2020 at 23:12):

Mathlib is a misnomer. It contains a whole bunch of other useful things too.

#### Kevin Buzzard (Feb 09 2020 at 23:12):

I'm sorry NNG looks so amateurish. We're both mathematicians ;-)

#### Kevin Buzzard (Feb 09 2020 at 23:13):

example : 5 < 23 := dec_trivial

The problem with that is it doesn't scale, because it does exactly what you were suggesting to do, so with 5-digit numbers things get a bit horrible.

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:13):

I'm only looking to use it on small numbers

#### Kevin Buzzard (Feb 09 2020 at 23:14):

dec_trivial is a cool tactic. It says "If this statement is decidable in the sense of logic, then decide it!"

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:14):

  -- We define a score to be a vector of natural numbers of length n. Each value
-- score_i corresponds to the number of violations that occurred in the ith
-- constraint.
def score (n : ℕ) := vector ℕ n

-- We define an ordering on scores such that s₁ ≤ s₂ iff they are equal up to
-- some index i, wherein s₁[i] ≤ s₂[i].
def score_le {n : ℕ} (s1 : score n) (s2 : score n) : Prop :=
∃ (i : ℕ) (h : i < n),
nth s1 ⟨i, h⟩ ≤ nth s2 ⟨i, h⟩ ∧
∀ (j : ℕ) (h' : j < i),
nth s1 ⟨j, lt.trans h' h⟩ = nth s2 ⟨j, lt.trans h' h⟩


so long as score vectors stay small at least

#### Kevin Buzzard (Feb 09 2020 at 23:14):

And there's a proof that i<j is decidable, and indeed you sketched the proof above. So dec_trivial runs through that proof.

#### Kevin Buzzard (Feb 09 2020 at 23:15):

score! Are you making a game? Lean pong would be cool.

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:15):

Reducing from PCP into a model of representing phonology

#### Kevin Buzzard (Feb 09 2020 at 23:15):

Maybe that's what kids want these days.

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:15):

I'll pitch it to publishers

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:16):

"It's a game where you do computability theory proofs"

#### Kevin Buzzard (Feb 09 2020 at 23:16):

Get CS undergrads to play it.

#### Kevin Buzzard (Feb 09 2020 at 23:17):

norm_num does the more sensible thing of converting everything to binary and then working with it using more sensible (but still formally verified) algorithms.

#### Kevin Buzzard (Feb 09 2020 at 23:19):

When I asked the question you asked, there was tactic.norm_num but not tactic.interactive.norm_num, which meant that the guts were there but you couldn't use it in tactic mode. Within about a week Mario Carneiro had got it working in tactic mode and I could then do all the inequalities I wanted. There have been countless cases like this, where someone needs something technical, mentions it on the chat, and then someone else knocks it up. The whole thing is quite an amazing project.

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:20):

Yeah, I've actually been getting in trying to contribute to Lean. I'm about to start work so I'll probably hold off until I become more situated therein but don't be surprised if you find my name on some commits :slight_smile:

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:21):

Also I don't know enough to ask the question right, but I'll try my best: is the norm_num / dec_trivial contrast at all related to the provably correct Lean kernel(?) I've heard about?

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:21):

or since norm_num is formally verified is it still considered to be a provably correct member of that kernel

#### Kevin Buzzard (Feb 09 2020 at 23:22):

dec_trivial is just using the stupidest algorithm. norm_num is doing a whole lot more work -- but it is still formally verified.

#### Kevin Buzzard (Feb 09 2020 at 23:22):

You would be able to tell if it were not formally verified -- the kernel would not let the proof go through.

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:23):

Gotcha, very cool!

#### Kevin Buzzard (Feb 09 2020 at 23:24):

So it's doing basic integer arithmetic but with a more optimised representation (Lean's definition of a natural is just some unwieldy linked list, so the first trick is to move to the num class which is naturals but stored in binary)

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:24):

I vaguely remember a proof in my Formal Language Theory about how an n-ary representation with n > 1 is exponentially more efficient than unary

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:24):

so that makes sense

#### Kevin Buzzard (Feb 09 2020 at 23:24):

It uses something which might be called reflection to construct a theorem about nums which is provably equivalent to the theorem about nats, and then proves the theorem about nums using formally verified but fast algorithms

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:25):

It uses something which might be called reflection to construct a theorem about nums which is provably equivalent to the theorem about nats, and then proves the theorem about nums using formally verified but fast algorithms

That's very cool

#### Kevin Buzzard (Feb 09 2020 at 23:25):

1,000,000 : nat is stored as succ (succ (succ (succ ... so it's horrible. But in num it's just essentially the binary string.

#### Kevin Buzzard (Feb 09 2020 at 23:26):

import tactic

#print nat

#print num
#print pos_num


to see how it actually does it.

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:35):

Hm. Looks like lean-mode is angry about import tactic. Time to try it in vscode and maybe spend my evening debugging elisp instead of writing proofs

#### Rob Lewis (Feb 09 2020 at 23:43):

I'm about to go to bed, but to avoid a misunderstanding: norm_num has nothing to do with the num type and isn't proof by reflection. It works on terms of type nat that have the structure of binary numerals. I'm happy to write more tomorrow if you're really curious (and I'm sure others could explain too).

#### Mario Carneiro (Feb 09 2020 at 23:53):

Also I don't know enough to ask the question right, but I'll try my best: is the norm_num / dec_trivial contrast at all related to the provably correct Lean kernel(?) I've heard about?

This is probably needless pedantry, but: the lean kernel is not provably correct, nor is it proven correct. It is rather the "source of truth" for all derivations done in lean, meaning that any tactics or terms that are created must pass through the kernel before being certified by it, so that as long as the kernel is correct and consistent then everything else is too. That's the "small trusted kernel" idea. (This does not mean that the kernel is bug-free, but we haven't found any soundness-critical issues in the history of lean AFAIK.)

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:54):

Definitely not needless pedantry, that's quite a big difference

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:55):

were it proven correct then all proofs validated by lean would necessarily be valid vs. their validity being motivated, right?

#### Mario Carneiro (Feb 09 2020 at 23:55):

the question is: valid with respect to what?

#### Mario Carneiro (Feb 09 2020 at 23:56):

Even if you prove the correctness of lean in some other formal prover, you are still trusting that prover as the source of truth. You can't eliminate this any more than you can do mathematics without any axioms

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:56):

Fair point. Are you getting after the fact that proofs in Lean are necessarily valid with respect to the Lean kernel? And discrepancies between the kernel and--

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:57):

yeah I suppose that encapsulates it better than I could :slight_smile:

#### Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:57):

And even in constructing a proof outside of a formal prover, it's a motivation towards its correctness because of space for error?

#### Mario Carneiro (Feb 09 2020 at 23:59):

You can also do a "paper proof" of correctness/consistency, and in fact I have done so for lean (see https://github.com/digama0/lean-type-theory/releases/tag/v1.0). But that doesn't cover implementation correctness, only soundness of the underlying type theory

#### Mario Carneiro (Feb 09 2020 at 23:59):

And it is still subject to general issues with paper proofs, namely gaps in mathematical presentation and human error

#### Cerek Hillen (he) (W2'20) (Feb 10 2020 at 00:02):

I'll take a look at the proof. And that all makes sense

#### Mario Carneiro (Feb 10 2020 at 00:03):

The proof shows that lean is consistent relative to ZFC with omega inaccessible cardinals (which are needed for the universe hierarchy)

#### Cerek Hillen (he) (W2'20) (Feb 10 2020 at 00:04):

I don't have a great mathematical maturity--I'm familiar with ZFC, but not with omega inaccessible carindals

What are they?

#### Mario Carneiro (Feb 10 2020 at 00:05):

That's omega many (i.e. indexed by natural numbers) inaccessible cardinals, in an increasing sequence

Gotcha!

#### Mario Carneiro (Feb 10 2020 at 00:05):

an inaccessible cardinal is basically a set which is large enough to model ZFC

#### Mario Carneiro (Feb 10 2020 at 00:05):

so you have a whole sequence of nested models of ZFC

#### Mario Carneiro (Feb 10 2020 at 00:06):

It's a pretty weak condition as far as large cardinal assumptions go

#### Mario Carneiro (Feb 10 2020 at 00:07):

But ZFC itself doesn't cut it because lean can prove ZFC is consistent

#### Cerek Hillen (he) (W2'20) (Feb 10 2020 at 00:08):

Ah interesting, I wasn't aware that you could prove ZFC's consistency in Lean. That's very cool

#### Mario Carneiro (Feb 10 2020 at 00:09):

See the file set_theory.zfc in mathlib, which explicitly constructs a model

#### Cerek Hillen (he) (W2'20) (Feb 10 2020 at 00:09):

found it, will review later

Last updated: May 13 2021 at 17:42 UTC