trivial ordering

Stream: new members

[Cerek Hillen (he) (W2'20)]

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)]

Or rather the inverse of le_of_succ_le_succ, succ_le_succ I think?

[Kevin Buzzard]

norm_num

[Kevin Buzzard]

import tactic

example : 12345 < 67890 := by norm_num

[Kevin Buzzard]

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

[Cerek Hillen (he) (W2'20)]

:pray:

I knew there had to be a better way

[Kevin Buzzard]

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

[Cerek Hillen (he) (W2'20)]

Hahahaha, glad to be here at Lean 3

[Kevin Buzzard]

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

[Cerek Hillen (he) (W2'20)]

Ah gotcha

[Cerek Hillen (he) (W2'20)]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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)]

I'm only looking to use it on small numbers

[Kevin Buzzard]

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)]

  -- 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]

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]

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

[Cerek Hillen (he) (W2'20)]

Reducing from PCP into a model of representing phonology

[Kevin Buzzard]

Maybe that's what kids want these days.

[Cerek Hillen (he) (W2'20)]

I'll pitch it to publishers

[Cerek Hillen (he) (W2'20)]

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

[Kevin Buzzard]

Get CS undergrads to play it.

[Kevin Buzzard]

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]

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)]

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)]

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)]

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

[Kevin Buzzard]

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]

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)]

Gotcha, very cool!

[Kevin Buzzard]

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)]

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)]

so that makes sense

[Kevin Buzzard]

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)]

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]

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]

import tactic

#print nat

#print num
#print pos_num

to see how it actually does it.

[Cerek Hillen (he) (W2'20)]

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]

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]

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)]

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

[Cerek Hillen (he) (W2'20)]

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

[Mario Carneiro]

the question is: valid with respect to what?

[Mario Carneiro]

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)]

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)]

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

[Cerek Hillen (he) (W2'20)]

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]

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]

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

[Cerek Hillen (he) (W2'20)]

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

[Mario Carneiro]

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)]

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

[Cerek Hillen (he) (W2'20)]

What are they?

[Mario Carneiro]

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

[Cerek Hillen (he) (W2'20)]

Gotcha!

[Mario Carneiro]

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

[Mario Carneiro]

so you have a whole sequence of nested models of ZFC

[Mario Carneiro]

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

[Mario Carneiro]

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

[Cerek Hillen (he) (W2'20)]

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

[Mario Carneiro]

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

[Cerek Hillen (he) (W2'20)]

found it, will review later