Zulip Chat Archive

Stream: new members

Topic: trivial ordering


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:09):

norm_num

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:10):

import tactic

example : 12345 < 67890 := by norm_num

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:10):

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

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:10):

:pray:

I knew there had to be a better way

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:10):

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

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:11):

Hahahaha, glad to be here at Lean 3

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:11):

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

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:11):

Ah gotcha

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:12):

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

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:12):

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

view this post on Zulip 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.

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:13):

I'm only looking to use it on small numbers

view this post on Zulip 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!"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:15):

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

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:15):

Reducing from PCP into a model of representing phonology

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:15):

Maybe that's what kids want these days.

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:15):

I'll pitch it to publishers

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:16):

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

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:16):

Get CS undergrads to play it.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:23):

Gotcha, very cool!

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:24):

so that makes sense

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 23:26):

import tactic

#print nat

#print num
#print pos_num

to see how it actually does it.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.)

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:54):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 09 2020 at 23:55):

the question is: valid with respect to what?

view this post on Zulip 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

view this post on Zulip 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--

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 09 2020 at 23:57):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 10 2020 at 00:02):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 10 2020 at 00:05):

What are they?

view this post on Zulip Mario Carneiro (Feb 10 2020 at 00:05):

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

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 10 2020 at 00:05):

Gotcha!

view this post on Zulip Mario Carneiro (Feb 10 2020 at 00:05):

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

view this post on Zulip Mario Carneiro (Feb 10 2020 at 00:05):

so you have a whole sequence of nested models of ZFC

view this post on Zulip Mario Carneiro (Feb 10 2020 at 00:06):

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

view this post on Zulip Mario Carneiro (Feb 10 2020 at 00:07):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 10 2020 at 00:09):

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

view this post on Zulip 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