# Zulip Chat Archive

## Stream: new members

### Topic: Define a finite set

#### Abhimanyu Pallavi Sudhir (Oct 14 2018 at 23:38):

How do I define a finite set only giving information of its cardinality? I'd like to define something like this:

definition S' : Type u | card : fintype.card S' = 2

(once again nonsense, but a sketch of what I want to define)

#### Bryan Gin-ge Chen (Oct 14 2018 at 23:38):

`finset.range`

?

#### Bryan Gin-ge Chen (Oct 14 2018 at 23:39):

oh you want a fintype, then try `fin`

#### Kevin Buzzard (Oct 15 2018 at 00:27):

Do you mean a finite type?

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 08:18):

You mean `def S' : Type := fin 2`

? That does seem to work.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 08:20):

Do you mean a finite type?

Oh, right, set only refers to subsets. I forgot.

#### Kenny Lau (Oct 15 2018 at 08:20):

I don’t think we understood this question

#### Kevin Buzzard (Oct 15 2018 at 13:35):

@Abhimanyu Pallavi Sudhir `fin 2`

is a type. There are exactly two distinct terms of that type. The terms are rather a mouthful to describe:

example : fin 2 := ⟨(0 : ℕ), dec_trivial⟩ example : fin 2 := ⟨(1 : ℕ), dec_trivial⟩

There's another type called `bool`

which also has exactly two terms. Type `#check bool`

and right-click on `bool`

and select "go to definition" to see it. The definition is completely different to `fin`

. The two terms of type `bool`

are `tt`

and `ff`

. These types `bool`

and `fin 2`

are not *equal*, but there is a map from `bool`

to `fin 2`

which is a bijection, and which you can define using the equation compiler (pattern matching).

Exercise 1: `def f : bool → fin 2`

. Define a function from `bool`

to `fin 2`

which you can prove (in maths, not in Lean) is a bijection.

Exercise 2: fill in the sorry.

import data.equiv.basic def X : equiv bool $ fin 2 := sorry

Exercise 3: find the library function which turns `X`

into a proof that `f`

is a bijection. Hint: which namespace do you think that function would be in?

open function example : bijective f := <FILL IN FUNCTION NAME> X

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:08):

@Abhimanyu Pallavi Sudhir

`fin 2`

is a type. There are exactly two distinct terms of that type. The terms are rather a mouthful to describe:example : fin 2 := ⟨(0 : ℕ), dec_trivial⟩ example : fin 2 := ⟨(1 : ℕ), dec_trivial⟩There's another type called

`bool`

which also has exactly two terms. Type`#check bool`

and right-click on`bool`

and select "go to definition" to see it. The definition is completely different to`fin`

. The two terms of type`bool`

are`tt`

and`ff`

. These types`bool`

and`fin 2`

are notequal, but there is a map from`bool`

to`fin 2`

which is a bijection, and which you can define using the equation compiler (pattern matching).Exercise 1:

`def f : bool → fin 2`

. Define a function from`bool`

to`fin 2`

which you can prove (in maths, not in Lean) is a bijection.Exercise 2: fill in the sorry.

import data.equiv.basic def X : equiv bool $ fin 2 := sorryExercise 3: find the library function which turns

`X`

into a proof that`f`

is a bijection. Hint: which namespace do you think that function would be in?open function example : bijective f := <FILL IN FUNCTION NAME> X

One more question: is there any way to use statements like "x is either the first element of fin 2 or the second element" directly without bijecting to bool?

#### Kenny Lau (Oct 15 2018 at 21:09):

by "use" do you mean "proof"?

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:09):

by "use" do you mean "proof"?

Either a proof or an existing lemma.

#### Kenny Lau (Oct 15 2018 at 21:09):

dec_trivial

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:11):

dec_trivial

Oh ok -- how would I actually denote "the first element of fin 2" and "the second element of fin 2" in such a statement? Just putting down the explicit form (like `⟨(0 : ℕ), dec_trivial⟩`

) gives errors.

#### Kenny Lau (Oct 15 2018 at 21:11):

0 and 1

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:12):

0 and 1

Wait, don't I need to do x.val, y.val for that? or do just x and y also take the values 0 and 1? (where `x y : fin 2`

). I was under the impression that `.val`

indexes the elements as 0 and 1 but the elements themselves are left abstract.

#### Kenny Lau (Oct 15 2018 at 21:14):

example : ∀ x : fin 2, x = 0 ∨ x = 1 := dec_trivial

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:15):

Oh ok -- what's the point of `x.val`

, then?

#### Kenny Lau (Oct 15 2018 at 21:17):

that 0 is of type `fin 2`

#### Chris Hughes (Oct 15 2018 at 21:18):

for any n, `fin (succ n)`

has `0`

defined on it in the obvious way, and any other numeral `x`

is just `\< x % succ n, proof\>`

. `val`

is a function `fin n -> nat`

, so it's useful whenever you want to turn something of type `fin n`

into something of type `nat`

.

#### Kenny Lau (Oct 15 2018 at 21:18):

you can also write:

example : ∀ x : fin 2, x.val = 0 ∨ x.val = 1 := dec_trivial

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:18):

for any n,

`fin (succ n)`

has`0`

defined on it in the obvious way, and any other numeral`x`

is just`\< x % succ n, proof\>`

.`val`

is a function`fin n -> nat`

, so it's useful whenever you want to turn something of type`fin n`

into something of type`nat`

.

So it's like a coercion?

#### Chris Hughes (Oct 15 2018 at 21:19):

Yes.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:22):

Thanks. I was proving that if there are three elements in fin 2, two of them must be equal -- I was trying some insanely long (relative to the triviality of the statement) proof by contradiction, ordering the elements and showing that the largest of the three will be above fin.last. Now it's easy.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:25):

By the way, does dec_trivial behave differently in term mode and tactic mode? The statement `have H01 : ∀ s : fin 2, s = 0 ∨ s = 1 := dec_trivial`

works, but `have H01 : ∀ s : fin 2, s = 0 ∨ s = 1, exact dec_trivial,`

doesn't.

#### Kenny Lau (Oct 15 2018 at 21:27):

example : true := have H01 : ∀ s : fin 2, s = 0 ∨ s = 1, from dec_trivial, trivial example : true := begin have H01 : ∀ s : fin 2, s = 0 ∨ s = 1, exact dec_trivial, trivial end

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:30):

Weird, that doesn't work for my theorem. I'll post my code, one second.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:32):

Or maybe it does.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:33):

Ok yeah it does.

#### Chris Hughes (Oct 15 2018 at 21:33):

If you `intro s`

it won't work.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:48):

I found my problem -- I have `local attribute [instance] classical.prop_decidable`

in my code, which seems to interfere with `dec_trivial`

.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:48):

How do I define the scope of a local attribute so it applies only to the theorem it is intended for?

#### Kevin Buzzard (Oct 15 2018 at 21:49):

I found my problem -- I have

`local attribute [instance] classical.prop_decidable`

in my code, which seems to interfere with`dec_trivial`

.

Remember when I suggested that `local attribute [instance, priority 0] classical.prop_decidable`

was better? It's for this sort of reason.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:49):

You did? Whoops, I missed it.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:50):

Yep, that works. Thanks.

#### Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:50):

But in a general scenario, is `section`

the only way to define the scope of local things?

#### Kevin Buzzard (Oct 15 2018 at 21:57):

`example (a b c : bool) : a = b ∨ b = c ∨ c = a := by cases a;cases b;cases c;simp `

#### Kevin Buzzard (Oct 15 2018 at 21:58):

This trick wouldn't work with `fin 2`

though. Although maybe @Scott Morrison was recently talking about a tactic which enabled you to do cases on `fin n`

somehow...

#### Kevin Buzzard (Oct 15 2018 at 21:58):

To make the trick work with `fin 2`

you would have to define your own recursor.

#### Kenny Lau (Oct 15 2018 at 21:59):

example (a b c : bool) : a = b ∨ b = c ∨ c = a := (dec_trivial : ∀ a b c, a = b ∨ b = c ∨ c = a) a b c

#### Kevin Buzzard (Oct 15 2018 at 22:01):

How do you do it for `fin 2`

?

#### Kevin Buzzard (Oct 15 2018 at 22:02):

I am surprised your code works -- I would have guessed that `dec_trivial`

would have complained that it did not know the type of anything before you fed `a b c`

to it

#### Kenny Lau (Oct 15 2018 at 22:02):

example (a b c : bool) : a = b ∨ b = c ∨ c = a := match a, b, c with | ff, ff, _ := or.inl rfl | tt, tt, _ := or.inl rfl | ff, _, ff := or.inr (or.inr rfl) | tt, _, tt := or.inr (or.inr rfl) | _, ff, ff := or.inr (or.inl rfl) | _, tt, tt := or.inr (or.inl rfl) end

#### Kenny Lau (Oct 15 2018 at 22:02):

How do you do it for

`fin 2`

?

example (a b c : fin 2) : a = b ∨ b = c ∨ c = a := (dec_trivial : ∀ a b c, a = b ∨ b = c ∨ c = a) a b c

#### Mario Carneiro (Oct 15 2018 at 22:08):

I am surprised your code works -- I would have guessed that dec_trivial would have complained that it did not know the type of anything before you fed a b c to it

That's what the type ascription is for

#### Scott Morrison (Oct 15 2018 at 22:14):

The tactic Kevin mentioned above is in the PR #352.

#### Kevin Buzzard (Oct 15 2018 at 22:16):

I am surprised your code works -- I would have guessed that dec_trivial would have complained that it did not know the type of anything before you fed a b c to it

That's what the type ascription is for

Lean can't work out the types of `a b c`

when it has to check that `dec_trivial`

is a term of that type, in my model of how it works. It must decide to wait a bit longer and hope it gets lucky.

#### Kenny Lau (Oct 15 2018 at 22:17):

The tactic Kevin mentioned above is in the PR #352.

yeah but it ain't merged

#### Kevin Buzzard (Oct 15 2018 at 22:19):

Interestingly, this fails:

example : ∀ a b c : bool, a = b ∨ b = c ∨ c = a | ff, ff, _ := or.inl rfl | tt, tt, _ := or.inl rfl | ff, _, ff := or.inr (or.inr rfl) | tt, _, tt := or.inr (or.inr rfl) | _, ff, ff := or.inr (or.inl rfl) | _, tt, tt := or.inr (or.inl rfl)

#### Kevin Buzzard (Oct 15 2018 at 22:19):

aah it's the commas I guess

#### Kevin Buzzard (Oct 15 2018 at 22:20):

example : ∀ a b c : bool, a = b ∨ b = c ∨ c = a | ff ff _ := or.inl rfl | tt tt _ := or.inl rfl | ff _ ff := or.inr (or.inr rfl) | tt _ tt := or.inr (or.inr rfl) | _ ff ff := or.inr (or.inl rfl) | _ tt tt := or.inr (or.inl rfl)

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:36):

@Abhimanyu Pallavi Sudhir

`fin 2`

is a type. There are exactly two distinct terms of that type. The terms are rather a mouthful to describe:example : fin 2 := ⟨(0 : ℕ), dec_trivial⟩ example : fin 2 := ⟨(1 : ℕ), dec_trivial⟩There's another type called

`bool`

which also has exactly two terms. Type`#check bool`

and right-click on`bool`

and select "go to definition" to see it. The definition is completely different to`fin`

. The two terms of type`bool`

are`tt`

and`ff`

. These types`bool`

and`fin 2`

are notequal, but there is a map from`bool`

to`fin 2`

which is a bijection, and which you can define using the equation compiler (pattern matching).Exercise 1:

`def f : bool → fin 2`

. Define a function from`bool`

to`fin 2`

which you can prove (in maths, not in Lean) is a bijection.Exercise 2: fill in the sorry.

import data.equiv.basic def X : equiv bool $ fin 2 := sorryExercise 3: find the library function which turns

`X`

into a proof that`f`

is a bijection. Hint: which namespace do you think that function would be in?open function example : bijective f := <FILL IN FUNCTION NAME> X

Exercise 1 is easy, it's just

def f : bool → fin 2 := begin intro x, cases x, exact 0, exact 1, end

But I have no clue as to how to even start exercise 2. Is there a library command that helps you prove the isomorphism?

#### Kevin Buzzard (Oct 16 2018 at 16:41):

Do you know how to build terms whose type is a structure using `{`

`}`

?

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:42):

No, I'm not even sure what a structure is.

#### Kevin Buzzard (Oct 16 2018 at 16:43):

A structure is just an inductive type which only has one constructor.

#### Kevin Buzzard (Oct 16 2018 at 16:43):

So non-examples are things like `nat`

and `bool`

.

#### Kevin Buzzard (Oct 16 2018 at 16:44):

But an example would be something like `and P Q`

.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:44):

Wait, can't `and P Q`

be considered a pi type?

#### Kenny Lau (Oct 16 2018 at 16:45):

it's a sigma type

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:45):

Since it's a function of two propositions?

#### Kenny Lau (Oct 16 2018 at 16:45):

`and`

is a pi type

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:45):

Ok, sure, then how is it an inductive type? ("A structure is just an inductive type...")

#### Kevin Buzzard (Oct 16 2018 at 16:45):

There's only one way you can build a term of type `and P Q`

-- you have to supply a proof of `P`

and a proof of `Q`

. So this gives us the possibility of having a second piece of notation for defining terms of type `and P Q`

where we say we're making something of type `and P Q`

and then just supply the proofs of `P`

and `Q`

#### Kevin Buzzard (Oct 16 2018 at 16:46):

I said `and P Q`

is an inductive type, not `and`

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:46):

Oh ok sure, that makes sense.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:46):

But I'm still not sure what that has to do with inductive types.

#### Kevin Buzzard (Oct 16 2018 at 16:47):

`example (P Q : Prop) : and P Q := {}`

#### Kevin Buzzard (Oct 16 2018 at 16:47):

If you type that, you get a red underline under the squiggly bracket -- this can't work currently, because we didn't supply proofs of P and Q. But the `{}`

notation is clue to a new way of defining a term of type `and P Q`

#### Kevin Buzzard (Oct 16 2018 at 16:48):

And the error is interesting -- Lean complains that some fields are missing.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:48):

I tried supplying the proofs, still doesn't work.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:48):

`example (P Q : Prop) (HP : P) (HQ : Q) : and P Q := {HP HQ}`

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:49):

function expected at

HP

term has type

P

#### Kevin Buzzard (Oct 16 2018 at 16:49):

You have to know how to supply them.

#### Chris Hughes (Oct 16 2018 at 16:49):

`example (P Q : Prop) (HP : P) (HQ : Q) : and P Q := { left := HP, right := HQ}`

is the syntax I think.

#### Kevin Buzzard (Oct 16 2018 at 16:49):

right

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:50):

Oh ok, so it's just standard left and right in term mode.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:50):

(But I don't know how to do exercise 2 in tactic mode either.)

#### Reid Barton (Oct 16 2018 at 16:50):

It doesn't have anything to do with the `left`

and `right`

tactics if that's what you mean

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:51):

Oh right, that's for `or`

goals.

#### Reid Barton (Oct 16 2018 at 16:51):

It's just that the fields of the structure `and P Q`

happen to also be named `left`

and `right`

(I guess? I never knew this)

#### Kevin Buzzard (Oct 16 2018 at 16:51):

So you can start work on Q2 by doing this:

def X : equiv bool $ fin 2 := { to_fun := f, inv_fun := sorry, left_inv := begin sorry end, right_inv := begin sorry end }

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:51):

Ah, I see.

#### Kevin Buzzard (Oct 16 2018 at 16:51):

I figured out the fields by writing `... := {}`

and then looking at the errors.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:52):

I knew the fields from the definition, but I didn't know how to supply them.

#### Kevin Buzzard (Oct 16 2018 at 16:53):

If you replace `inv_fun := sorry`

with `inv_fun := _`

and look at the error, you'll see that `inv_fun`

is supposed to be the inverse map from `fin 2`

back to `bool`

. So you could define that outside, like you did with `f`

#### Kevin Buzzard (Oct 16 2018 at 16:53):

The two remaining fields are the proofs that the compositions in both directions are the identity. Of course both proofs are "just unravel everything" but I think it's quite good fun trying to work out how to do this.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 17:05):

Ok, I'm defining `f_inv`

, and I've gotten up to having `Hx01 : x = 0 ∨ x = 1`

:

def f_inv : fin 2 → bool := begin intro x, have H01 : ∀ s : fin 2, s = 0 ∨ s = 1, exact dec_trivial, have Hx01 : x = 0 ∨ x = 1, exact H01 x, sorry, end

But for some reason I can't do `cases Hx01`

. I get `induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop`

What's going on?

#### Patrick Massot (Oct 16 2018 at 17:07):

I figured out the fields by writing

`... := {}`

and then looking at the errors.

This is so September 2018...

#### Patrick Massot (Oct 16 2018 at 17:07):

Nowadays we type `{!}`

and click on the light bulb (or Ctrl-.) and choose the relevant option from the menu (I don't have Lean to check right now)

#### Kevin Buzzard (Oct 16 2018 at 17:25):

I need to move with the times.

#### Kevin Buzzard (Oct 16 2018 at 17:26):

Abhi -- it's not a good idea to use tactics to define data. You can use tactics for the proof, but for the data you are better off using something like the equation compiler

#### Kevin Buzzard (Oct 16 2018 at 17:29):

But to answer your question about what's going on, the `cases`

command runs the recursor for the type, and if you look at the definition of `or.rec`

you'll see that it's only set up to spit out proofs, not data

#### Kevin Buzzard (Oct 16 2018 at 17:29):

I think I once knew a good reason for this

#### Chris Hughes (Oct 16 2018 at 17:31):

The iota reduction rule for `or`

would cause contradictions when both sides of the `or`

were true if `or`

could produce data.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 17:53):

@Chris Hughes Can you give an example?

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 17:56):

Abhi -- it's not a good idea to use tactics to define data. You can use tactics for the proof, but for the data you are better off using something like the equation compiler

I'm not sure how to. I mean, I tried to use the equation compiler to produce a definition for `f`

, but all I could do is:

def f (b : bool): fin 2 := if b = tt then 0 else 1

Which is only the value of `f`

, not a function itself.

#### Johan Commelin (Oct 16 2018 at 17:57):

That did define a function `f`

.

#### Johan Commelin (Oct 16 2018 at 17:57):

It is the same as

def f : bool → fin 2 := \lam b, if b = tt then 0 else 1

#### Chris Hughes (Oct 16 2018 at 17:59):

`def f (h : 1 = 1 ∨ 0 = 0) : ℕ := or.cases_on h (λ h, 0) (λ h, 1)`

. The iota reduction rule says `f (or.inl rfl) = 0`

and that `f (or.inr rfl) = 1)`

, but since by proof irrelevance `or.inl rfl = or.inr rfl`

, this would imply `0 = 1`

, hence `or`

cannot eliminate into data.

#### Chris Hughes (Oct 16 2018 at 18:00):

Here's your function defined using the equation compiler

def f : bool → fin 2 | tt := 0 | ff := 1

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 18:02):

`def f (h : 1 = 1 ∨ 0 = 0) : ℕ := or.cases_on h (λ h, 0) (λ h, 1)`

. The iota reduction rule says`f (or.inl rfl) = 0`

and that`f (or.inr rfl) = 1)`

, but since by proof irrelevance`or.inl rfl = or.inr rfl`

, this would imply`0 = 1`

, hence`or`

cannot eliminate into data.

Huh -- I thought `0 = 0`

and `1 = 1`

would just be treated as propositions (and indeed they are equivalent).

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 18:04):

It is the same as

def f : bool → fin 2 := \lam b, if b = tt then 0 else 1

Thanks -- why doesn't `∀ b : bool`

work in place of `λ b`

?

#### Kenny Lau (Oct 16 2018 at 18:05):

`(λ b, proof) : (∀ b : bool, p b)`

#### Chris Hughes (Oct 16 2018 at 18:06):

They are treated as propositions. That's why it's not possible to eliminate into data. If both sides of the `or`

are true it breaks proof irrelevance, but without this iota reduction rule you can't compute with it.

#### Johan Commelin (Oct 16 2018 at 18:06):

`\forall`

is only for propositions.

#### Chris Hughes (Oct 16 2018 at 18:07):

It's only for types.

#### Kevin Buzzard (Oct 16 2018 at 19:01):

@Abhimanyu Pallavi Sudhir here are some comments on things you said whilst I was going home.

If `X`

is an inductive type then it could well have been defined in something like the following way:

inductive X | c1 : X | c2 : X

and then you can define functions `X->Y`

using the equation compiler like this (I `open X`

because `c1`

is really called `X.c1`

etc)

open X def f : X → ℕ | c1 := 4 | c2 := 6

Note that the `|`

symbols are being used in two different ways here -- first to define an inductive type, and secondly to define a function from the type. The equation compiler is quite powerful. It's trickier to get it to define the map from `fin 2`

, but it's possible. The equation compiler is very smart.

You asked about `\forall b`

instead of `lam b`

-- one is the type, and one is the term. You use Pi to make Pi types (and forall is a special case of Pi, as are function types), and lam to make terms of type Pi. This is what Kenny's post was demonstrating. It took me some time to get my head around all this but it's easy really -- somehow I never read anything which explained it all in simple terms (which was what I needed this time last year). There are propositions called things like `P`

and proofs called things like `H`

or `HP`

. Similarly there are function types (Pi types) called things like `X -> Y`

and then there are actual functions (the terms) called things like `lam x, x + 1`

.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 19:55):

Thanks. This works for exercise 2 (`left_inv`

only -- presumably the same thing works for `right_inv`

) :

import data.equiv.basic import tactic.norm_num --set_option pp.notation false def f : bool → fin 2 | tt := 1 | ff := 0 def f_inv : fin 2 → bool := λ k, if k = 1 then tt else ff def X : equiv bool (fin 2) := { to_fun := f, inv_fun := f_inv, left_inv := begin rw function.left_inverse, intro x, cases x, have Hfff : f ff = 0, rw f, rw Hfff, rw f_inv, exact dec_trivial, have Hftt : f tt = 1, rw f, rw Hftt, rw f_inv, exact dec_trivial, end, right_inv := begin sorry end } example : function.bijective f := sorry --<FILL IN FUNCTION NAME> X #check function.bijective_iff_has_inverse

Although `dec_trivial`

did the job for me, I'm curious to know what exactly is the algorithm being tried by Lean at that point (in Lean notation, it's obvious mathematically), i.e. what could I replace `dec_trivial`

with?

#### Kevin Buzzard (Oct 16 2018 at 19:57):

`right_inv`

might be harder, the way you've set it up.

#### Kevin Buzzard (Oct 16 2018 at 19:58):

left_inv := begin intro x, cases x, have Hfff : f ff = 0, rw f, rw Hfff, rw f_inv,refl, have Hftt : f tt = 1, rw f, rw Hftt, rw f_inv, refl, end,

#### Kenny Lau (Oct 16 2018 at 19:58):

we should all wait until `fin_cases`

is merged

#### Kevin Buzzard (Oct 16 2018 at 19:59):

Your `rw`

doesn't seem to do anything. Because your goal is definitionally equal to what the rw changed it into, you can just skip it. And both of your algorithms are `rfl`

-- the left hand side equals the right hand side by definition.

#### Kevin Buzzard (Oct 16 2018 at 20:00):

@Kenny Lau I just dealt with `n>=2`

using contradiction. Abhi is yet to run into this issue I think.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:03):

Does `fin_cases`

actually allow just doing cases on `fin n`

? Does it break it up into the full `n`

cases even if `n`

is a thousand?

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:03):

@Kenny Lau I just dealt with

`n>=2`

using contradiction. Abhi is yet to run into this issue I think.

Wait, which issue?

#### Kevin Buzzard (Oct 16 2018 at 20:04):

His definition of `f_inv`

is "k=1" and "all other cases" so he'll have to deal with k>=2 at some point.

#### Kevin Buzzard (Oct 16 2018 at 20:04):

left_inv := begin intro x, cases x;refl end,

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:06):

I guess `refl`

is more powerful than I thought.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:08):

His definition of

`f_inv`

is "k=1" and "all other cases" so he'll have to deal with k>=2 at some point.

I can just use exfalso and prove a contradiction using `2 > fin.last`

.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:09):

In fact it seems just doing `cases x`

gives a statement that says `x.val < 2`

.

#### Kenny Lau (Oct 16 2018 at 20:09):

import data.fintype noncomputable def X : equiv bool (fin 2) := trunc.out (fintype.equiv_fin bool)

#### Kenny Lau (Oct 16 2018 at 20:09):

:P

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:10):

What??

#### Kevin Buzzard (Oct 16 2018 at 20:10):

rofl what happened there?

#### Mario Carneiro (Oct 16 2018 at 20:11):

`fintype.card bool = 2`

#### Mario Carneiro (Oct 16 2018 at 20:11):

so `bool ~= fin 2`

#### Kenny Lau (Oct 16 2018 at 20:12):

trunc

#### Kevin Buzzard (Oct 16 2018 at 20:12):

Oh, that's exactly what Abhi was asking if he could do earlier. `fintype.equiv_fin`

is the general proof that a type which is known to have finitely many elements (say `n`

) `equiv`

s with `fin n`

#### Kenny Lau (Oct 16 2018 at 20:12):

still trunc

#### Kevin Buzzard (Oct 16 2018 at 20:12):

Aah, but Kenny's proof is noncomputable :O

#### Mario Carneiro (Oct 16 2018 at 20:13):

the funny part is it's not really, if you evaluate the proof you can eliminate the trunc

#### Kenny Lau (Oct 16 2018 at 20:13):

how?

#### Kenny Lau (Oct 16 2018 at 20:13):

wait, proof is irrelevant and can't be evaluated

#### Mario Carneiro (Oct 16 2018 at 20:13):

false on both counts

#### Mario Carneiro (Oct 16 2018 at 20:13):

it's not a proof, it's a trunc

#### Mario Carneiro (Oct 16 2018 at 20:13):

and it can be evaluated

#### Mario Carneiro (Oct 16 2018 at 20:13):

even if it was a proof

#### Kenny Lau (Oct 16 2018 at 20:13):

how can I do it then

#### Mario Carneiro (Oct 16 2018 at 20:14):

via `#reduce`

#### Kenny Lau (Oct 16 2018 at 20:14):

oh well then you can't make it a definition

#### Kenny Lau (Oct 16 2018 at 20:14):

could you show us the code?

#### Mario Carneiro (Oct 16 2018 at 20:14):

If you `#reduce`

the proof that `trunc (bool ~= fin 2)`

you will get something that starts `trunc.mk`

... then you throw that away and keep the rest

#### Kevin Buzzard (Oct 16 2018 at 20:16):

...or get a deterministic timeout

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:17):

def X : equiv bool (fin 2) := { to_fun := f, inv_fun := f_inv, left_inv := begin --rw function.left_inverse, intro x, cases x, have Hfff : f ff = 0, rw f, rw Hfff, rw f_inv, refl, have Hftt : f tt = 1, rw f, rw Hftt, rw f_inv, refl, end, right_inv := begin intro x, have H01 : ∀ s : fin 2, s = 0 ∨ s = 1, exact dec_trivial, have x01 : x = 0 ∨ x = 1, exact H01 x, cases x01 with x0 x1, --case x0 rw x0, have Hfarc0 : f_inv 0 = ff, refl, rw Hfarc0, refl, --case x1 rw x1, exact dec_trivial, end }

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:18):

What's `trunc.out`

? Someone catch me up.

#### Kevin Buzzard (Oct 16 2018 at 20:19):

it noncomputably removes the trunc.

#### Kenny Lau (Oct 16 2018 at 20:20):

For a type `\a`

, `trunc \a`

is the type `\a`

quotient by the equivalence relation that relates everything

#### Kevin Buzzard (Oct 16 2018 at 20:20):

You can see the docstring for `trunc`

by hovering over it. It's some weird CS thing.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:24):

Ok, I'll need to read up a bit on that.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:25):

By the way, exercise 3 is just `equiv.bijective X`

(or at least this works).

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:27):

Wait, could we also have used `finset.card_eq_of_bijective`

to prove bijectivity then prove `equiv`

from `equiv.of_bijective`

?

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:27):

Oh wait that's for `finset`

s.

#### Kevin Buzzard (Oct 16 2018 at 20:31):

By the way, exercise 3 is just

`equiv.bijective X`

(or at least this works).

Great! How did you find it? I found it by writing `bijective`

and hitting ctrl-space and escape a few times.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:35):

Great! How did you find it? I found it by writing

`bijective`

and hitting ctrl-space and escape a few times.

Yep, same.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:36):

Although I didn't hit escape, just scrolled.

#### Kevin Buzzard (Oct 16 2018 at 20:36):

Sometimes in VS Code the first time I try ctrl-space I don't get all the options, so I instinctively cancel and try again before I start scrolling.

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:38):

Yeah, I think sometimes it limits itself to a specific namespace or something.

#### Kevin Buzzard (Oct 16 2018 at 20:38):

Oh this `trunc`

thing -- Lean is not keen on choosing a bijection between `bool`

and `fin 2`

but if you put an equivalence relation on the type of all choices, and the relation was "it's always true", then Lean will give you an element of the quotient type and this is well-defined! So Kenny's construction only shows that the type of `equiv`

s is non-empty without producing an explicit element.

#### Chris Hughes (Oct 16 2018 at 21:02):

It's stronger than nonempty.

#### Kevin Buzzard (Oct 16 2018 at 21:07):

because it's data. But I am very hazy about what difference this makes, and even hazier about whether I care.

#### Chris Hughes (Oct 16 2018 at 21:22):

The definition of `equiv.fintype`

, the thing that says `A`

is finite implies `equiv A B`

is finite uses `equiv_fin`

and the lift condition is met because `fintype`

is a `subsingleton`

. This in turn means that determinant is computable.

#### Kevin Buzzard (Oct 16 2018 at 21:34):

They'll be pleased in M1M1 :-) I still have not got my head around how important computability is in my world.

#### Chris Hughes (Oct 16 2018 at 21:37):

I get the impression that it's nice to be able to easily prove `1+1=2`

etc., but I never use computability on naturals on numbers bigger than about 4, and the same with most other computable objects.

#### Chris Hughes (Oct 16 2018 at 21:42):

Also Lean computable rarely means efficiently computable, so it's kind of useless.

#### Kenny Lau (Oct 16 2018 at 21:44):

David Helm once said that one of the reasons he likes modular forms is that this is one of the unique opportunities in pure maths where you get to see numbers bigger than 4

#### Kevin Buzzard (Oct 16 2018 at 21:47):

I once wrote an entire paper and then looked through it to find the biggest number in it, and it was 2

#### Kevin Buzzard (Oct 16 2018 at 21:47):

Maybe I'm less concerned about computability than I think

#### Abhimanyu Pallavi Sudhir (Oct 16 2018 at 21:57):

I once wrote an entire paper and then looked through it to find the biggest number in it, and it was 2

I'm guessing reference and equation numbering don't count.

#### Kevin Buzzard (Oct 16 2018 at 22:12):

I'm not sure I numbered any equations but I almost certainly numbered theorems (did you notice that here they name them instead?) and no I didn't count those numbers :-)

Last updated: May 14 2021 at 04:22 UTC