# Zulip Chat Archive

## 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.

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

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

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

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

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

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