Zulip Chat Archive

Stream: new members

Topic: Define a finite set


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

view this post on Zulip Bryan Gin-ge Chen (Oct 14 2018 at 23:38):

finset.range ?

view this post on Zulip Bryan Gin-ge Chen (Oct 14 2018 at 23:39):

oh you want a fintype, then try fin

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 00:27):

Do you mean a finite type?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 08:18):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 08:20):

Do you mean a finite type?

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 08:20):

I don’t think we understood this question

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

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 21:09):

by "use" do you mean "proof"?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:09):

by "use" do you mean "proof"?

Either a proof or an existing lemma.

view this post on Zulip Kenny Lau (Oct 15 2018 at 21:09):

dec_trivial

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 21:11):

0 and 1

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 21:14):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:15):

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 21:17):

that 0 is of type fin 2

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 21:18):

you can also write:

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

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

view this post on Zulip Chris Hughes (Oct 15 2018 at 21:19):

Yes.

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

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:30):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:32):

Or maybe it does.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:33):

Ok yeah it does.

view this post on Zulip Chris Hughes (Oct 15 2018 at 21:33):

If you intro s it won't work.

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

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:49):

You did? Whoops, I missed it.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 21:50):

Yep, that works. Thanks.

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

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

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

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 21:58):

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

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

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 22:01):

How do you do it for fin 2?

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

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

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

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

view this post on Zulip Scott Morrison (Oct 15 2018 at 22:14):

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

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

view this post on Zulip Kenny Lau (Oct 15 2018 at 22:17):

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

yeah but it ain't merged

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

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 22:19):

aah it's the commas I guess

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:41):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:42):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:43):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:43):

So non-examples are things like nat and bool.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:44):

But an example would be something like and P Q.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:44):

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:45):

it's a sigma type

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:45):

Since it's a function of two propositions?

view this post on Zulip Kenny Lau (Oct 16 2018 at 16:45):

and is a pi type

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:46):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:46):

Oh ok sure, that makes sense.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:46):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:47):

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:48):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:48):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:48):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:49):

function expected at
HP
term has type
P

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:49):

You have to know how to supply them.

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:49):

right

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:50):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:50):

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:51):

Oh right, that's for or goals.

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 16:51):

Ah, I see.

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 16:51):

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

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

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 17:25):

I need to move with the times.

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 17:29):

I think I once knew a good reason for this

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 17:53):

@Chris Hughes Can you give an example?

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 17:57):

That did define a function f.

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

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

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

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

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 18:05):

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

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

view this post on Zulip Johan Commelin (Oct 16 2018 at 18:06):

\forall is only for propositions.

view this post on Zulip Chris Hughes (Oct 16 2018 at 18:07):

It's only for types.

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 19:57):

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

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 19:58):

we should all wait until fin_cases is merged

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 20:04):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:06):

I guess refl is more powerful than I thought.

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

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:09):

import data.fintype

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:09):

:P

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:10):

What??

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 20:10):

rofl what happened there?

view this post on Zulip Mario Carneiro (Oct 16 2018 at 20:11):

fintype.card bool = 2

view this post on Zulip Mario Carneiro (Oct 16 2018 at 20:11):

so bool ~= fin 2

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:12):

trunc

view this post on Zulip 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) equivs with fin n

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:12):

still trunc

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 20:12):

Aah, but Kenny's proof is noncomputable :O

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

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:13):

how?

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:13):

wait, proof is irrelevant and can't be evaluated

view this post on Zulip Mario Carneiro (Oct 16 2018 at 20:13):

false on both counts

view this post on Zulip Mario Carneiro (Oct 16 2018 at 20:13):

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

view this post on Zulip Mario Carneiro (Oct 16 2018 at 20:13):

and it can be evaluated

view this post on Zulip Mario Carneiro (Oct 16 2018 at 20:13):

even if it was a proof

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:13):

how can I do it then

view this post on Zulip Mario Carneiro (Oct 16 2018 at 20:14):

via #reduce

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:14):

oh well then you can't make it a definition

view this post on Zulip Kenny Lau (Oct 16 2018 at 20:14):

could you show us the code?

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 20:16):

...or get a deterministic timeout

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:18):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 20:19):

it noncomputably removes the trunc.

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:24):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:25):

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:27):

Oh wait that's for finsets.

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

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:36):

Although I didn't hit escape, just scrolled.

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 16 2018 at 20:38):

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 20:38):

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.

view this post on Zulip Chris Hughes (Oct 16 2018 at 21:02):

It's stronger than nonempty.

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

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

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

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

view this post on Zulip Chris Hughes (Oct 16 2018 at 21:42):

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

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

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

view this post on Zulip Kevin Buzzard (Oct 16 2018 at 21:47):

Maybe I'm less concerned about computability than I think

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

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