Define a finite set

Stream: new members

[Abhimanyu Pallavi Sudhir]

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]

finset.range ?

[Bryan Gin-ge Chen]

oh you want a fintype, then try fin

[Kevin Buzzard]

Do you mean a finite type?

[Abhimanyu Pallavi Sudhir]

You mean def S' : Type := fin 2? That does seem to work.

[Abhimanyu Pallavi Sudhir]

Do you mean a finite type?

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

[Kenny Lau]

I don’t think we understood this question

[Kevin Buzzard]

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

@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 booland 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

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]

by "use" do you mean "proof"?

[Abhimanyu Pallavi Sudhir]

by "use" do you mean "proof"?

Either a proof or an existing lemma.

[Kenny Lau]

dec_trivial

[Abhimanyu Pallavi Sudhir]

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]

0 and 1

[Abhimanyu Pallavi Sudhir]

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]

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

[Abhimanyu Pallavi Sudhir]

Oh ok -- what's the point of x.val, then?

[Kenny Lau]

that 0 is of type fin 2

[Chris Hughes]

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]

you can also write:

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

[Abhimanyu Pallavi Sudhir]

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]

Yes.

[Abhimanyu Pallavi Sudhir]

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]

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]

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]

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

[Abhimanyu Pallavi Sudhir]

Or maybe it does.

[Abhimanyu Pallavi Sudhir]

Ok yeah it does.

[Chris Hughes]

If you intro s it won't work.

[Abhimanyu Pallavi Sudhir]

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]

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

[Kevin Buzzard]

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]

You did? Whoops, I missed it.

[Abhimanyu Pallavi Sudhir]

Yep, that works. Thanks.

[Abhimanyu Pallavi Sudhir]

But in a general scenario, is section the only way to define the scope of local things?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

To make the trick work with fin 2 you would have to define your own recursor.

[Kenny Lau]

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]

How do you do it for fin 2?

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

yeah but it ain't merged

[Kevin Buzzard]

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]

aah it's the commas I guess

[Kevin Buzzard]

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]

@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 booland 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

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]

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

[Abhimanyu Pallavi Sudhir]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

So non-examples are things like nat and bool.

[Kevin Buzzard]

But an example would be something like and P Q.

[Abhimanyu Pallavi Sudhir]

Wait, can't and P Q be considered a pi type?

[Kenny Lau]

it's a sigma type

[Abhimanyu Pallavi Sudhir]

Since it's a function of two propositions?

[Kenny Lau]

and is a pi type

[Abhimanyu Pallavi Sudhir]

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

[Kevin Buzzard]

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]

I said and P Q is an inductive type, not and

[Abhimanyu Pallavi Sudhir]

Oh ok sure, that makes sense.

[Abhimanyu Pallavi Sudhir]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

function expected at
HP
term has type
P

[Kevin Buzzard]

You have to know how to supply them.

[Chris Hughes]

example (P Q : Prop) (HP : P) (HQ : Q) : and P Q := { left := HP, right := HQ} is the syntax I think.

[Kevin Buzzard]

right

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Reid Barton]

It doesn't have anything to do with the left and right tactics if that's what you mean

[Abhimanyu Pallavi Sudhir]

Oh right, that's for or goals.

[Reid Barton]

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]

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]

Ah, I see.

[Kevin Buzzard]

I figured out the fields by writing ... := {} and then looking at the errors.

[Abhimanyu Pallavi Sudhir]

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

[Kevin Buzzard]

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]

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]

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]

I figured out the fields by writing ... := {} and then looking at the errors.

This is so September 2018...

[Patrick Massot]

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]

I need to move with the times.

[Kevin Buzzard]

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]

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]

I think I once knew a good reason for this

[Chris Hughes]

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]

@Chris Hughes Can you give an example?

[Abhimanyu Pallavi Sudhir]

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]

That did define a function f.

[Johan Commelin]

It is the same as

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

[Chris Hughes]

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]

Here's your function defined using the equation compiler

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

[Abhimanyu Pallavi Sudhir]

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]

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]

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

[Chris Hughes]

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]

\forall is only for propositions.

[Chris Hughes]

It's only for types.

[Kevin Buzzard]

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

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]

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

[Kevin Buzzard]

  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]

we should all wait until fin_cases is merged

[Kevin Buzzard]

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]

@Kenny Lau I just dealt with n>=2 using contradiction. Abhi is yet to run into this issue I think.

[Abhimanyu Pallavi Sudhir]

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]

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

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]

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

[Abhimanyu Pallavi Sudhir]

I guess refl is more powerful than I thought.

[Abhimanyu Pallavi Sudhir]

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]

In fact it seems just doing cases x gives a statement that says x.val < 2.

[Kenny Lau]

import data.fintype

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

[Kenny Lau]

:P

[Abhimanyu Pallavi Sudhir]

What??

[Kevin Buzzard]

rofl what happened there?

[Mario Carneiro]

fintype.card bool = 2

[Mario Carneiro]

so bool ~= fin 2

[Kenny Lau]

trunc

[Kevin Buzzard]

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) equivs with fin n

[Kenny Lau]

still trunc

[Kevin Buzzard]

Aah, but Kenny's proof is noncomputable :O

[Mario Carneiro]

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

[Kenny Lau]

how?

[Kenny Lau]

wait, proof is irrelevant and can't be evaluated

[Mario Carneiro]

false on both counts

[Mario Carneiro]

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

[Mario Carneiro]

and it can be evaluated

[Mario Carneiro]

even if it was a proof

[Kenny Lau]

how can I do it then

[Mario Carneiro]

via #reduce

[Kenny Lau]

oh well then you can't make it a definition

[Kenny Lau]

could you show us the code?

[Mario Carneiro]

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]

...or get a deterministic timeout

[Abhimanyu Pallavi Sudhir]

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]

What's trunc.out? Someone catch me up.

[Kevin Buzzard]

it noncomputably removes the trunc.

[Kenny Lau]

For a type \a, trunc \a is the type \a quotient by the equivalence relation that relates everything

[Kevin Buzzard]

You can see the docstring for trunc by hovering over it. It's some weird CS thing.

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

By the way, exercise 3 is just equiv.bijective X (or at least this works).

[Abhimanyu Pallavi Sudhir]

Wait, could we also have used finset.card_eq_of_bijective to prove bijectivity then prove equiv from equiv.of_bijective?

[Abhimanyu Pallavi Sudhir]

Oh wait that's for finsets.

[Kevin Buzzard]

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]

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]

Although I didn't hit escape, just scrolled.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Oh this trunc thing -- Lean is not keen on choosing a bijection between bool and fin 2but 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 equivs is non-empty without producing an explicit element.

[Chris Hughes]

It's stronger than nonempty.

[Kevin Buzzard]

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

[Chris Hughes]

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]

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

[Chris Hughes]

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]

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

[Kenny Lau]

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]

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

[Kevin Buzzard]

Maybe I'm less concerned about computability than I think

[Abhimanyu Pallavi Sudhir]

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]

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