Zulip Chat Archive

Stream: general

Topic: Basic questions


view this post on Zulip Charles Rezk (Oct 18 2018 at 00:27):

How would I go about proving things about functions between sets, especially finite sets? I see some machinery for sets (really, "subsets" of a given type), but nothing about functions between them. On the other hand, I can certainly have functions between types, but I don't see a convenient way to produce a particular "finite type".

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:30):

what do you want to do with them exactly?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:31):

for the most part you can just write functions between types

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:31):

which happen to be finite

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:32):

Let's say I want to construct a particular finite type, e.g., of size n. How do I do it?

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:33):

And how do I prove things about it?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:33):

fin n is a type of size n

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:34):

and functions out of fin n have various properties not shared by general types, for example list.of_fn turns a function out of fin n into a list of values

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:34):

Where is the code for fin?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:36):

init/data/fin I think

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:36):

it's imported by default

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:38):

I don't see "list" in there.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:38):

that definition is in data.list.basic

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:43):

How would I go about constructing a function out of a S:fin n ?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:49):

You can just define the function as a lambda...

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:49):

or you can use fin.cases

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:52):

Not sure how to construct anything other than identity function that way. Because I don't know what the "elements" of fin n are called.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:52):

0, 1, 2, ...

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:53):

Where in the code for fin does it say that I can do that?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:54):

has_one and has_add give you that for free

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:54):

init.fin.ops I think

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:57):

Nothing about looking at the code would suggest why that's the case

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:58):

The code that actually causes 2 to be parsed as bit0 1 is in the parser (C++ code), and bit0 is defined in init.core

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:58):

okay

view this post on Zulip Charles Rezk (Oct 18 2018 at 00:59):

I'd rather read the documentation than look at the code, but there doesn't seem to be any.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 00:59):

Every type that has a 0 and 1 and addition has all numerals

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:03):

So I can treat elements of a fin n as natural numbers, e.g., add them and such?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:03):

yes

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:03):

Here's the definition of fin in init/data/fin/basic.lean:

structure fin (n : nat) := (val : nat) (is_lt : val < n)

This says that fin takes as input n, which should be a nat (natural number). fin n is then a structure (a certain simple kind of inductive type) which contains a field called val (which takes values in nat) and a field called is_lt (which is a proof that val < n). So I would say that (val : nat) tells you that the elements of fin n can be written as natural numbers.

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:04):

I see.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:04):

when you write 10 : fin 3 you actually get 1 = 10 % 3

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:05):

Suppose I have an a:nat and an h:a<10. How do I construct an element of fin 10 from that?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:06):

\langle a, h\rangle

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:06):

Nothing more readable than than?

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:06):

than that?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:07):

There are several ways to write constructors for structures

view this post on Zulip Jeremy Avigad (Oct 18 2018 at 01:07):

@Mario Carneiro This is how I would do it:

def foo : fin 3 → nat
| ⟨0, _⟩   := 7
| ⟨1, _⟩   := 5
| ⟨2, _⟩   := 6
| ⟨n+3, h⟩ := absurd h (by simp)

Is there a better way?

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:07):

In VS code when you start typing \langle, you can hit tab and it will autocomplete into the left angle bracket unicode symbol

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:08):

What is "by simp" doing there?

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:08):

And you can always put in an explicit type ascription if you're worried that the ⟨⟩ syntax is too obscure.

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:09):

Assume I know nothing. What is an explicit type ascription?

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:09):

e.g. let f := (⟨a : nat ,h : a < 10⟩ : fin 10)

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:10):

A type ascription is this colon syntax; basically the stuff to the right of the colon is the type of the stuff to the left.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:10):

@Jeremy Avigad That's the nicest way to define functions out of fin n currently (and you can use dec_trivial in place of by simp), although if you want to prove properties about it fin.cases gives a slightly better reasoning

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:11):

I've been wondering whether we should have an explicit fin2 n type defined as an inductive type so that you get a nice recursion principle

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:11):

(This type actually exists in dioph.lean but is unused elsewhere)

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:13):

@Jeremy Avigad When I put in that code, it says "simplify tactic failed to simplify"

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:14):

@Jeremy Avigad When I put in that code it says "simply tactic failed to simplify"

view this post on Zulip Jeremy Avigad (Oct 18 2018 at 01:14):

Each element of fin 3 is something of the form fin.mk n h where n is a natural number and h : n < 3. We can abbreviate fin.mk n h as ⟨n, h⟩ because Lean can figure out the relevant constructor from the context.
The style of writing functions using definition by cases is described in Chapter 8 of Theorem Proving in Lean: https://leanprover.github.io/theorem_proving_in_lean/. In the last case, h is of the form n + 3 < n. We can rule out the case by showing that it is never true. by simp calls some built in automation to do that. As Mario points out, dec_trivial does something similar. It recognizes that there is a built-in procedure for evaluating inequalities, and uses that to determine that the negation of n + 3 < 3 is true.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:14):

@Charles Rezk does absurd h dec_trivial work in place of that code?

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:15):

Yes, replacing (by simp) with dec_trivial works.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:15):

you may need some simp lemmas from mathlib

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:15):

yes

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:15):

grrr

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:15):

do you not use mathlib?

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:16):

Sure I use mathlib.

view this post on Zulip Scott Olson (Oct 18 2018 at 01:16):

@Jeremy Avigad I think you mean n + 3 < 3

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:16):

I probably haven't gotten to it. I'm still trying to figure out functions from finite sets.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:17):

gotten to what

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:17):

I don't know. I started trying to look at groups, then I went backwards because i didn't know how to do anything.

view this post on Zulip Jeremy Avigad (Oct 18 2018 at 01:19):

@Scott thanks, fixed. @Charles, you are right. If you add import filter.order to the top of the file it should work. As Mario points out, absurd h dec_trivial also works without importing anything.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:20):

it's in filter.order? That's embarrasing

view this post on Zulip Jeremy Avigad (Oct 18 2018 at 01:21):

It's probably in something more basic, I just happened to have filter.order open and that was sufficient.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:21):

also, I think you mean order.filter

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:27):

Using squeeze_simp, it's simp only [not_lt, zero_le, le_add_iff_nonneg_left], where not_lt is in algebra.order and the other two are in algebra.ordered_group.

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:30):

How would I write that without using any tactics?

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:36):

dec_trivial

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:36):

dec_trivial isn't a tactic, technically, though it's true that it is kind of opaque. I'll let someone more knowledgeable try to explain what precisely it's doing under the hood.

It looks like the term (not_lt.mpr $ (le_add_iff_nonneg_left 3).mpr $ zero_le n) also works, though I just reverse-engineered this from the squeeze_simp output above.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:37):

there are more efficient term proofs too

view this post on Zulip Mario Carneiro (Oct 18 2018 at 01:37):

but that's the one that simp finds

view this post on Zulip Jeremy Avigad (Oct 18 2018 at 01:43):

@Charles Writing out a fully detailed proof from basic lemmas is painful. Here is one way to do it:

example (n : nat) : ¬ (n + 3 < 3) :=
have h1 : 0 ≤ n, from nat.zero_le n,
have h2 : 0 + 3 ≤ n + 3, from nat.add_le_add_right h1 3,
have h3 : 3 ≤ n + 3, from h2,
show ¬ (n + 3 < 3), from not_lt_of_ge h3

But this is the sort of thing we really want automation to do: we should just say "this is obvious" and let Lean figure it out. The fact that we generally have to muck around to figure out what to do is a sign that interactive theorem proving is not yet ready for prime time. We are not yet where we want to be.
In fact, Scott Morrison has written an automated procedure called tidy that tries lots of "straightforward" things. In this case, it works:

import tactic.tidy

example (n : nat) : ¬ (n + 3 < 3) :=
by tidy

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:46):

I understand, but I'm trying to understand what is actually going on here.

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:47):

In this case, tidy just calls dec_trivial as you can see if you put in tidy { trace_result:=tt}.

view this post on Zulip Charles Rezk (Oct 18 2018 at 01:51):

It's not clear to me why I should have to have anything there: defining a function out of fin 3, I wouldn't expect to have to say anything abut its values on 3,4,5,...

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:53):

But an element of fin 3 is defined as a nat called val plus a proof that val is less than 3. So to define a function out of fin 3 you need to tell it what to do for every nat.

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 01:54):

For val=3,4,5,... that means that you have to show that the proof that val<3 can't exist.

view this post on Zulip Mario Carneiro (Oct 18 2018 at 02:09):

The fin.cases approach avoids this, although it can't use the equation compiler because it's not built in to lean.

def f : fin 3   :=
fin.cases 7 $
fin.cases 5 $
fin.cases 6 $
λ x, x.elim0
def f : fin 3   :=
fin.cases 7 $
fin.cases 5 $
λ _, 6

view this post on Zulip Mario Carneiro (Oct 18 2018 at 02:11):

the last one you can also do in the equation compiler version:

def foo : fin 3  nat
| 0, _⟩ := 7
| 1, _⟩ := 5
| ⟨_, _⟩ := 6

view this post on Zulip Johan Commelin (Oct 18 2018 at 04:20):

@Charles Rezk Have you seen the tutorials by Neil Strickland? They are amazing. I think they can help you get up to speed with Lean. Besides that, most of us has learned everything we know by just being very persistent in asking questions here.

view this post on Zulip Bryan Gin-ge Chen (Oct 18 2018 at 04:43):

I would recommend slowly working through "Theorem Proving in Lean" as well. The lean-focused chapters of Logic & Proof were also quite useful to me.

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 05:26):

@Charles Rezk The thing about fin 3 is that it's a theorem that it has three elements. If you make your own type which has three elements "by definition" then you could do this:

inductive threetype : Type
| zero : threetype
| one : threetype
| two : threetype

open threetype

definition f : threetype  
| zero := 59
| one := 65537
| two := 341

You can think of the n + 3 > 3 story as just supplying the proof that there aren't any more elements of fin 3.

view this post on Zulip Kevin Buzzard (Oct 18 2018 at 07:04):

dec_trivial isn't a tactic, technically, though it's true that it is kind of opaque. I'll let someone more knowledgeable try to explain what precisely it's doing under the hood.

The writers of TPIL probably fit the bill:

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#decidable-propositions


Last updated: May 13 2021 at 05:21 UTC