## Stream: new members

### Topic: easy questions

#### Adrian Chu (Jun 26 2019 at 08:23):

theorem test (x : ℕ): ∃ a : ℕ, 2*a = 4 := sorry

theorem test2 (x : ℕ): ∃ b : ℕ, 3*b = 6 :=
begin
fapply exists.intro,
exact 3, sorry
end


in this stupid theorem, i want to replace 3 with the a given by test, how should i write?

#### Kenny Lau (Jun 26 2019 at 08:25):

you can't take out what you put in the proof of an existential statement

#### Adrian Chu (Jun 26 2019 at 08:27):

huh? but then how should we define a number x+1, in which the existence of x is guaranteed by some previous theorem A?

#### Kenny Lau (Jun 26 2019 at 08:28):

example (choice : Π (C : ℕ → Prop), (∃ n, C n) → ℕ)
(spec : ∀ (C : ℕ → Prop) (n : ℕ) (h : C n), choice C ⟨n, h⟩ = n) :
false :=

i see

#### Kevin Buzzard (Jun 27 2019 at 12:10):

Why does rfl fail?

#### Kevin Buzzard (Jun 27 2019 at 12:10):

def x: ℕ → ℕ := (λ i, i+1)
def y: ℕ → ℕ := (λ i, 1+i)
theorem test : x = y  := rfl -- type mismatch


#### Kenny Lau (Jun 27 2019 at 12:18):

the first one is i+1 and the second one is 1+i

oh thanks. Duh.

#### Kevin Buzzard (Jun 27 2019 at 12:26):

The colours played a trick on my brain somehow

#### Keeley Hoek (Jun 27 2019 at 12:35):

Whoever made the courier new typeface has caused at least billions of dollars of damage with how close i and 1 look

#### Adrian Chu (Jun 27 2019 at 14:08):

wouldn't 1 and l be deadlier?

#### Marc Huisinga (Jun 27 2019 at 14:36):

1ucki1y l is 1ess common in programming

#### Keeley Hoek (Jun 29 2019 at 06:34):

is it illegal to delcare a long literal in Java with a lower case l?

#### Keeley Hoek (Jun 29 2019 at 06:34):

If no, that's a good one

that's legal

#### Johan Commelin (Jun 29 2019 at 07:05):

There's an entire class of "off-by-l" errors

#### Gun Pinyo (Jul 21 2019 at 16:53):

Hi guys, I want to use the heterogeneous equality but cannot derive it to homogeneous equality. i.e. can we define the following?

    def foo (α β : Type) (p : α = β) (x : α) (y : β) :
x == y → (eq.rec_on p x : β) = y := sorry


#### Chris Hughes (Jul 21 2019 at 16:57):

def foo (α β : Type) (p : α = β) (x : α) (y : β) :
x == y → (eq.rec_on p x : β) = y := λ h, by cases h; refl


#### Chris Hughes (Jul 21 2019 at 17:01):

You don't need the assumption α = β, it's implied by x == y

#### Gun Pinyo (Jul 21 2019 at 17:01):

@Chris Hughes ah, thanks. but how about another way?

#### Gun Pinyo (Jul 21 2019 at 17:04):

wait, if we don't need p : α = β, then how can we express (eq.rec_on p x : β) = y?

#### Chris Hughes (Jul 21 2019 at 17:05):

You could write eq.rec_on (type_eq_of_heq (h : x == y)) x

#### Gun Pinyo (Jul 22 2019 at 10:34):

Hi, there. Can anyone tell me why the following example doesn't work?

example (α β : Type) (p : α = β) : unit → α = unit → β :=
begin rw p, reflexivity end


after rw p the goal is unit → β = unit → β but reflexivity doesn't work.

#### Chris Hughes (Jul 22 2019 at 10:35):

Brackets

example (α β : Type) (p : α = β) : (unit → α) = (unit → β) :=
begin rw p end


#### Gun Pinyo (Jul 22 2019 at 10:36):

@Chris Hughes wow, such a silly mistake. Thank you

#### Kenny Lau (Jul 22 2019 at 10:43):

example (α β : Type) (p : α = β) : unit → α = unit → β :=
begin intros _ h, rw [← p, h], exact () end


#### Gun Pinyo (Jul 22 2019 at 18:06):

Does lean have something like the following in standard library or mathlib?

def uip (α : Prop) (x y : α) : x = y := sorry


if not, how can we prove this?

#### Kenny Lau (Jul 22 2019 at 18:07):

rfl

#### Kenny Lau (Jul 22 2019 at 18:07):

this is called proof irrelevance and is built into Lean

#### Kenny Lau (Jul 22 2019 at 18:07):

it says that two proofs of the same proposition are definitionally equal

#### Gun Pinyo (Jul 22 2019 at 18:08):

@Kenny Lau , thank you :)

#### Gun Pinyo (Jul 25 2019 at 10:52):

I have a problem with unfolding tactic. Considering the following code

structure graph :=
(nodes  : Type)
(edges  : Type)
(srctrg : bool → edges → nodes)

def prism_graph (G : graph) : graph :=
{ nodes  := bool × G.nodes
, edges  := (bool × G.edges) ⊕ G.nodes
, srctrg := λ b e, match e with
| (sum.inl (b', e)) := (b, G.srctrg b' e)
| (sum.inr v)       := (b, v)
end
}

def cube_graph : ℕ → graph
| 0      := ⟨unit, unit, (λ _ _, ())⟩
| (n +1) := prism_graph (cube_graph n)

example (n : ℕ) (b : bool) (v : (cube_graph n).nodes) :
(graph.srctrg (cube_graph (n +1)) b (sum.inr v)) = (b, v) :=
begin
unfold cube_graph,
end


I don't understand why unfold cube_graph fails. Clearly, it should succeed with the goal become (graph.srctrg (prism_graph (cube_graph n)) b (sum.inr v)) = (b, v).

Ps. You might argue that I can close this tactic by refl but my point is to use unfold. The reason is that this is the simplified version of the actual problem that I am working and I can't just use refl.
Ps2. This is another question. If refl works, why simp doesn't. Isn't simp use refl at the end anyway?

#### Patrick Massot (Jul 25 2019 at 11:02):

You're expecting too much from unfold. What you want here is dsimp [cube_graph].

#### Patrick Massot (Jul 25 2019 at 11:03):

About your second question, maybe simp is actually doing some thing which turns your goal into a non-refl goal.

#### Chris Hughes (Jul 25 2019 at 11:03):

You can use dunfold. The reason simp doesn't work, is because graph.srctrg is a dependent function, so the expression after rewriting only typechecks because cube_graph (n + 1) = prism_graph (cube_graph n) is s definitional equality.

#### Gun Pinyo (Jul 25 2019 at 13:23):

@Patrick Massot @Chris Hughes Thank you for introducing dsimp and dunfold to me.

Another question, if I have two occurrences of the same
definition in a goal. (d)unfold once will affect the first
occurrence an not the second, if I want another way (i.e. affect the second
one and not the first one) what should I do?

#### Kevin Buzzard (Jul 25 2019 at 13:25):

Definitional unfolding is all defeq, so if your goal does not look like what you want it to look like, you can just write change <what you want the goal to look like> and if what you write is definitionally equal to what the goal is, the goal will change to what you write. Note that show is synonymous with change, although you can use change on hypotheses as well.

#### Kevin Buzzard (Jul 25 2019 at 13:26):

The other approach for zooming in on terms in goals is conv mode: https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

#### Kevin Buzzard (Jul 25 2019 at 13:27):

I don't know how much you know about definitional equality v all the other equalities, but here's something I wrote about definitional equality: https://xenaproject.wordpress.com/2019/05/21/equality-part-1-definitional-equality/

#### Chris Hughes (Jul 25 2019 at 13:28):

Patrick Massot Chris Hughes Thank you for introducing dsimp and dunfold to me.

Another question, if I have two occurrences of the same
definition in a goal. (d)unfold once will affect the first
occurrence an not the second, if I want another way (i.e. affect the second
one and not the first one) what should I do?

Do you have an example of this. Usually I think it unfolds all occurrences, so it might be not unfolding the second one for some other reason.

#### Kevin Buzzard (Jul 25 2019 at 13:31):

Another thing you might want to know is that if you type #print prefix cube_graph then you can see all the stuff that Lean generated for you when you made cube_graph. Things called cube_graph._equation.1 or something (I forget what they're exactly called) are the things which Lean tries to use when you run unfold -- that's what the tactic actually does. Similarly dsimp [cube_graph] tries to simplify using those "hidden" equation lemmas.

#### Gun Pinyo (Jul 25 2019 at 13:35):

@Kevin Buzzard Thank you for introducing change and conv. These what tactics that I have been looking for many days. It is also interesting to know that we can even unfold anonymous functions as well.

@Chris Hughes I have but it is in a long file and it can be the case that the second occurrence is not unfoldable at the moment so I miss understood the behaviour of (d)unfold .

#### Jesse Michael Han (Jul 25 2019 at 15:13):

@Gun Pinyo you should definitely read through the general mathlib tactic documentation

#### Gun Pinyo (Jul 27 2019 at 10:48):

If I am in the tactic mode with 2 goals. Is there any tactic that lets me prove the second goal before the first one?
The motivation behind this is when the second goal is a lot easier than the first one.

Ps. I have read through https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md but didn't find any.

#### Kevin Buzzard (Jul 27 2019 at 10:48):

swap

#### Kevin Buzzard (Jul 27 2019 at 10:48):

Once you've got it working, hover over the tactic to see the docstring.

#### Gun Pinyo (Jul 27 2019 at 10:52):

@Kevin Buzzard Thank you.
So there are more tactics that are not in mathlib. Where can I find the documentation of these built-in tactics?
At first, I thought every built-in tactic should be in https://leanprover.github.io/reference/tactics.html# but it is not the case for swap.

#### Kevin Buzzard (Jul 27 2019 at 10:54):

Maybe swap is in core Lean? You can just right click on it to check.

#### Kevin Buzzard (Jul 27 2019 at 10:54):

A great place for learning about core tactics is the book Theorem Proving In Lean.

#### Bryan Gin-ge Chen (Jul 27 2019 at 10:59):

It would be good to add swap and any other missing core tactics to that doc page. Maybe for now we should just add a comment to this issue https://github.com/leanprover-community/mathlib/issues/450

#### Gun Pinyo (Jul 27 2019 at 10:59):

@Kevin Buzzard I agree, that was what I did before starting my current project.
But again, it doesn't mention swap.

#### Gun Pinyo (Jul 27 2019 at 11:04):

Oh, btw, swap is defined in mathlib and not the builtin one. https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive.lean

#### Keeley Hoek (Jul 27 2019 at 13:48):

If I recall, core defines tactic.swap but does not expose to interactive?

#### Gun Pinyo (Aug 07 2019 at 14:01):

This might be a very stupid question but why can't we add univalence axiom to lean3? i.e. why axiom K of lean3 doesn't play well with the univalence axiom?

(deleted)

(deleted)

#### Kevin Buzzard (Aug 07 2019 at 14:02):

This has been talked about before and I know it's inconsistent but I don't know why. It's something to do with impredicativity of Prop

#### Chris Hughes (Aug 07 2019 at 14:10):

Because equality is a subsingleton, and univalence says it is isomorphic to something which is not a subsingleton. Even if you define a equality to return a type, rather than a Prop, this is still provably a subsingleton (the proof uses the proof irrelevant version of eq).

#### Chris Hughes (Aug 07 2019 at 14:11):

I think α ≃ β → α = β is consistent though, but not very useful.

#### Kevin Buzzard (Aug 07 2019 at 14:15):

So is even my undeleted post incorrect?

#### Kevin Buzzard (Aug 07 2019 at 14:16):

Because α = β → α ≃ β is a theorem

#### Chris Hughes (Aug 07 2019 at 14:18):

Those two function aren't inverses of each other in Lean, but univalence says they are.

#### Kevin Buzzard (Aug 07 2019 at 14:19):

Surely α ≃ β → α = β would be useful in Lean, because it would enable me to show that if R and S are isomorphic rings and R is Noetherian local then S is Noetherian local?

#### Chris Hughes (Aug 07 2019 at 14:21):

You also need the ring structures to be heq for that. Which won't be provable.

#### Kevin Buzzard (Aug 07 2019 at 14:23):

So you can't get from the bare α ≃ β → α = β statement about types to statements about isomorphic groups being equal groups by using some kind of trickery?

#### Kevin Buzzard (Aug 07 2019 at 14:23):

I would imagine that in HoTT they can do this somehow

#### Chris Hughes (Aug 07 2019 at 14:25):

I don't think so. In Lean, you have no idea what eq.mp gives you. In HoTT, you know from the right_inv part of the univalence equivalence, that eq.mpr is to_fun of your bijection. Then you can prove that eq.rec one_ring_strcuture = the_other_ring_structure

#### Chris Hughes (Aug 07 2019 at 14:29):

In the univalence equivalence inv_fun := eq.mp. The axiom says that eq.mp has a two sided inverse.

#### Floris van Doorn (Aug 07 2019 at 16:19):

In answer to the original question: from univalence you can show that bool = bool has two unequal elements (one corresponding to the identity function, and one corresponding to the function that swaps the elements), which contradicts axiom K.

#### Floris van Doorn (Aug 07 2019 at 16:23):

And I'm quite sure that Chris is right that weak univalence (α ≃ β → α = β) doesn't give you that isomorphic groups are equal.

#### Gun Pinyo (Aug 10 2019 at 15:57):

Hi, there. Regarding defined class in stdlib, many of them have one field. I try to understand why don't you just use def with @[class]? For example,

class inhabited (α : Sort u) :=
(default : α)

@[class] def inhabited' (α : Sort u) := α


inhabited' should be as usable as inhabited but we also don't need to write the constructor.

There are some classes that way such as in library/init/relator.lean. I can see the advantage of using the letter way but haven't seen the advantage of the former way. Could you please explain to me please?

<deleted>

<deleted>

<deleted>

#### Floris van Doorn (Aug 11 2019 at 05:25):

One difference is that inhabited' α is definitionally equal to α, while inhabited α is not (it is equivalent to α, in the sense that equiv (inhabited α) α can be proven).
Sometimes extra definitional equalities are convenient, but sometimes they have downsides. It is possible that the elaborator of Lean will unfold inhabited' in places where you didn't want to, and then you are not talking about the type inhabited' α anymore, but about α. The latter is not a class, which might cause issues with type class inference not firing.
Since inhabited is not a definition, it can never be unfolded.

#### Andrew Ashworth (Aug 11 2019 at 05:27):

This is a much better explanation of why, haha.

#### Gun Pinyo (Aug 11 2019 at 14:43):

@Floris van Doorn , how about we add @[irreducible] to inhabited' α, would it solved the problem with unwanted unfolding?

#### Reid Barton (Aug 11 2019 at 15:42):

In that case there won't be much advantage of the def over the single-field class

#### Floris van Doorn (Aug 11 2019 at 17:12):

That would also be fine. But as Reid said: if you don't want to unfold it, you can just as well make it a structure.

#### Gun Pinyo (Aug 11 2019 at 17:23):

Well, my point is that I don't want to keep writing .intro or something like that.

#### Andrew Ashworth (Aug 11 2019 at 17:39):

Angle bracket notation doesn't work for you?

#### Chris Hughes (Aug 11 2019 at 17:52):

If you marked it irreducible you'd have to define anintro and use that.

#### Gun Pinyo (Aug 14 2019 at 16:06):

I just discover that we can write numerals as elements of fin
type. So I want to refactor the following code:

def fin.zero {n : ℕ} : fin (n +1) := ⟨0, nat.zero_lt_succ n⟩
def vector.insert_nth_zero : v.insert_nth a fin.zero = a :: v :=
begin
cases v with l p,
simp [fin.zero, vector.insert_nth, vector.cons, list.insert_nth],
end

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
begin
cases v with l p,
simp [{!what should be here?!}, vector.insert_nth, vector.cons, list.insert_nth],
end


vector.insert_nth_zero' is the same as vector.insert_nth_zero
except that fin.zero is changed to 0. Everything should be fine, however, I don't know there to replace fin.zero in simp tactic now. Does anyone know how to fix this?

#### Joe (Aug 14 2019 at 17:01):

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
begin
cases v with l p,
simp only [vector.insert_nth], norm_cast
end


#### Joe (Aug 14 2019 at 17:05):

or maybe this

def vector.insert_nth_zero' : v.insert_nth a 0 = a :: v :=
begin
cases v with l p,
simp only [vector.insert_nth, vector.cons, subtype.mk_eq_mk],
show list.insert_nth 0 a l = a :: l,
simp [list.insert_nth]
end


#### Gun Pinyo (Aug 15 2019 at 14:02):

I still have another question regarding fin. Sometimes, I want to use pattern matching on i : fin n in the same way as one will do in ℕ but since the inductive part is in i.val so I need to do as follows:

def fin_is_even : Π n : ℕ, fin n → bool
| 0      i                        := i.elim0
| (n +1) ⟨0,    _⟩                := true
| (n +1) ⟨i_val +1, succ_i_is_lt⟩ :=
let i : fin n := ⟨i_val, nat.pred_le_pred succ_i_is_lt⟩
in bnot (fin_is_even n i)


Ok it works, but in practice, I find it quite annoying to write let i : fin n := ⟨i_val, nat.pred_le_pred succ_i_is_lt⟩ every time whereas i should be obtained directly from something like fin.succ i. Therefore, I try to use @[pattern] to help me with this as follows:

@[pattern]
def fin.zero {n : ℕ} : fin (n +1) := ⟨0, nat.zero_lt_succ n⟩

attribute [pattern] fin.succ

def fin_is_even' : Π n : ℕ, fin n → bool
| 0      i            := i.elim0
| (n +1) fin.zero     := true
| (n +1) (fin.succ i) := bnot (fin_is_even' n i)


However I get an error, what is wrong with my code? Did I misunderstand anything about @[pattern]?

err msg1:
invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
err msg2:
don't know how to synthesize placeholder context: fin_is_even' : Π (n : ℕ), fin n → bool ⊢ fin n

#### Chris Hughes (Aug 15 2019 at 15:03):

You're basically expecting the equation compiler to determine whether an element of fin n is in the image of fin.succ or not, and if it is what the element that maps to it is. This is very hard in general. I think the pattern attribute only works for things that are definitionally equal to a constructor. for example λ x, x + 2 = λ x, nat.succ (nat.succ x), by definition, so marking add with the pattern attribute works. Incidentall changing your definition of fin.zero also works - it also wanted to reduce the proof to a constructor, but it's probably not a desirable change.

@[pattern]
def fin.zero {n : ℕ} (h): fin (nat.succ n) := ⟨0, h⟩

attribute [pattern] fin.succ

def fin_is_even' : Π n : ℕ, fin n → bool
| 0      i            := i.elim0
| (n +1) (fin.zero h)     := true
--| (n +1) x := bnot (fin_is_even' n i)


#### Gun Pinyo (Aug 15 2019 at 17:31):

@Chris Hughes , thank you, now I can see why fin.succ doesn't work. Anyway, is there any other that allow us use something like fin.zero and fin.succ in pattern matching? I really miss the following alternative definition of fin

inductive fin' : ℕ → Type
| zero : fin' 0
| succ : Π {n : ℕ}, fin' n → fin' (n +1)


But I use this definition, it is incompatible with the standard library.

I think the pattern attribute only works for things that are definitionally equal to a constructor

How about this following code in data.vector? Is this definitionally equal to any constructor? I fact, I haven't seen any code using pattern matching on vector

@[pattern] def nil : vector α 0 := ⟨[],  rfl⟩

@[pattern] def cons : α → vector α n → vector α (nat.succ n)
| a ⟨ v, h ⟩ := ⟨ a::v, congr_arg nat.succ h ⟩


#### Chris Hughes (Aug 15 2019 at 17:46):

nil definitely is. cons definitely isn't.

Actually it depends on the vector you're trying to match with. If your vector is a variable then it won't work. If you do

match vector.mk l rfl with...


Then it has a better chance of working, but I think the prood of equality would have to be rfl.

#### Kevin Buzzard (Aug 16 2019 at 07:17):

I thought this variant of fin was in mathlib somewhere

Last updated: May 08 2021 at 02:46 UTC