## Stream: new members

### Topic: Guarantee a set to be a finset

#### JIANXIONG SUN (Aug 17 2018 at 21:20):

Can someone help me with the Jacobian Identity, there are so many brackets, how can I easily expand all the brackets ?

And how can I use a+b+c = (a+b)+c, the add_assoc can only prove a+b+c=a+(b+c)

structure vector (R : Type) :=
vec :: (x : R) (y : R) (z : R)

namespace vector

variables {R : Type} [comm_ring R]

def zero : vector R := vec 0 0 0

def add (a b : vector R) :=
vec (a.x + b.x) (a.y + b.y) (a.z + b.z)

def cross_prod (a b : vector R) :=
vec (a.y * b.z - a.z * b.y) (a.x * b.z - a.z * b.x) (a.x * b.y - a.y * b.x)

theorem jacobian : ∀ (a b c: vector R) ,
add (cross_prod a (cross_prod b c)) (add (cross_prod b (cross_prod c a))  (cross_prod c (cross_prod a b))) = zero :=
begin
intro a,
intro b,
intro c,
unfold cross_prod,
unfold zero,
dsimp,
congr,
simp,

end
end vector


#### Patrick Massot (Aug 17 2018 at 21:24):

Are you willing to use mathlib?

#### Patrick Massot (Aug 17 2018 at 21:25):

If yes then you can preface the file with import tactic.ring, and right after unfold_zero, write ring, tauto and be done

#### JIANXIONG SUN (Aug 17 2018 at 21:29):

It's a good method, but actually I want to show the steps of the proof :-)

#### Chris Hughes (Aug 17 2018 at 21:32):

a + b + c is definitionally equal to (a + b) + c, the pretty printer doesn't display the brackets since they are unnecessary.

#### Patrick Massot (Aug 17 2018 at 21:33):

it's more than definitional equality (!) it's parsing

(deleted)

#### Kenny Lau (Aug 17 2018 at 21:56):

how do we call that type of equality?

#### Patrick Massot (Aug 17 2018 at 21:57):

it's what the parser parses

#### Sebastian Ullrich (Aug 17 2018 at 21:58):

Structural equality

#### Patrick Massot (Aug 17 2018 at 21:58):

yeah, sounds more impressive

why "structure"?

#### Patrick Massot (Aug 17 2018 at 22:00):

why not "ontological equality"?

#### Chris Hughes (Aug 17 2018 at 22:00):

How many degrees of equality are there?

#### Sebastian Ullrich (Aug 17 2018 at 22:00):

Because the terms' structure as a tree of constructors is the same. See "structural induction", which is induction over that tree.

#### Chris Hughes (Aug 17 2018 at 22:03):

What type of equality do terms need to be for rw to work? I think that's slightly weaker than structural equality since it unfold reducibles

#### JIANXIONG SUN (Aug 19 2018 at 20:19):

Why there is always excessive memory when I import something?Is it the problem of the computer Capture.PNG

#### Patrick Massot (Aug 19 2018 at 20:23):

Your installation of mathlib seems to have a problem

#### Patrick Massot (Aug 19 2018 at 20:23):

maybe you should try to rebuild it

#### JIANXIONG SUN (Aug 19 2018 at 20:44):

I tried it but it seems not work

#### Simon Hudon (Aug 19 2018 at 21:03):

After rebuilding, did you restart your Lean server?

#### JIANXIONG SUN (Aug 20 2018 at 22:16):

How to switch the LHS and RHS of n equality?

variables {R : Type} [comm_ring R]
theorem mul : ∀ (a b c : R) , a * b * c = c * a * b :=
begin
intro a,
intro b,
intro c,
rw mul_comm,
apply mul_assoc,
end


I thought this can work but it seems that mul_assoc can only prove cab=c(ab)

#### Simon Hudon (Aug 20 2018 at 22:21):

You can try assoc_rw [mul_comm]

#### JIANXIONG SUN (Aug 20 2018 at 22:29):

You mean right after intro c?

#### JIANXIONG SUN (Aug 20 2018 at 22:31):

What's the meaning of the square bracket here?

#### Simon Hudon (Aug 20 2018 at 22:31):

Actually, in your situation, ac_refl, is even simpler: by intros; ac_refl

#### Simon Hudon (Aug 20 2018 at 22:32):

What's the meaning of the square bracket here?

Like with rw, assoc_rw takes a list of expressions as an argument: assoc_rw [rule1,rule2,rule3]

#### JIANXIONG SUN (Aug 20 2018 at 22:37):

It says that assoc_rwis an unknown identifier, Capture.PNG

#### Simon Hudon (Aug 20 2018 at 22:38):

Are you using mathlib?

#### Mario Carneiro (Aug 20 2018 at 22:41):

the non crazy overpowered solution is just to use <-:

theorem mul (a b c : R) : a * b * c = c * a * b :=
by rw [mul_comm, ← mul_assoc]


#### Mario Carneiro (Aug 20 2018 at 22:43):

simp will also do AC rewriting, so by simp [mul_comm, mul_assoc] also works without mathlib

#### JIANXIONG SUN (Aug 20 2018 at 22:45):

I would try this tomorrow, thank you

#### Simon Hudon (Aug 20 2018 at 22:55):

Why do you say AC rewriting is overpowered?

#### JIANXIONG SUN (Aug 20 2018 at 23:00):

I have mathlib on the computer，maybe there some other problems

#### Simon Hudon (Aug 20 2018 at 23:04):

You need to import tactic.rewrite, sorry, I forgot to mention that

#### Olli (Aug 27 2018 at 19:15):

Would it be possible to get a hint for what to do here:
https://gist.github.com/luxbock/981f990d263516589146ffeb3825e421

This is Chapter 3 exercise from the book. My hypothesis h is a lambda, and the only way I know how to make progress with it is by applying it to something, but I have nothing else to go by

#### Simon Hudon (Aug 27 2018 at 19:18):

You can use and.intro (assume h', _) (assume h', _)

#### Patrick Massot (Aug 27 2018 at 19:18):

I have a hint: use tactic mode

#### Olli (Aug 27 2018 at 19:19):

I am trying to make it through without tactics, as I'm still trying to wrap my head around propositions as types, and tactics have yet to be introduced at this point

#### Kevin Buzzard (Aug 27 2018 at 19:21):

Patrick has a point though. I found it much easier to learn tactic mode first. Without it, the goal is an and statement and you can construct proofs of such statements with and.intro as Simon says. In general I guess this is the way to think about it. For each of these things (and, or, implies etc) you need to learn how to construct it (i.e. make it) and how to eliminate it (i.e. use it). and.intro is a constructor for and.

#### Patrick Massot (Aug 27 2018 at 19:23):

I'll tell you how a mathematician would do it. First install mathlib (of course). Then

import tactic.interactive

variables (p q r : Prop) [decidable p] [decidable q]
example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
by tauto


#### Patrick Massot (Aug 27 2018 at 19:23):

Then move on to interesting maths

#### Patrick Massot (Aug 27 2018 at 19:24):

Of course the downside is you'll probably depend on people actually understanding terms

#### Olli (Aug 27 2018 at 19:24):

I did skim the tactics chapter and played around with it a little bit. My goal is to prove each statement in as many ways as possible to get familiar with all the features

#### Olli (Aug 27 2018 at 19:25):

I'm currently reading the book "How to Proove It" alongside trying to learn Lean, so I'm far from a mathematician who needs to use it for anything serious. It's more of an exercise in mind expansion for me

#### Patrick Massot (Aug 27 2018 at 19:27):

Let me emphasize: when I write "how a mathematician would do it", I really mean this, and not "how everybody should do it". I'm only providing one point of view. Other people will have other interesting points of view

#### Olli (Aug 27 2018 at 19:28):

Sure undestood :). I figure most people have a very different background from someone like myself, so I just wanted to give some context for the level I'm at

#### Kevin Buzzard (Aug 27 2018 at 19:46):

Well here's a tactic mode proof:

example (p q r : Prop) : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
begin
split,
{ intro H,
split,
{ intro Hp,
apply H,
left,
exact Hp
},
{ intro Hq,
apply H,
right,
exact Hq
}
},
intro H,
cases H with Hpr Hqr,
intro Hpq,
cases Hpq with Hp Hq,
{ apply Hpr,
exact Hp
},
{ apply Hqr,
exact Hq
}
end


It's cool to step through it looking at the goals etc at each step.

#### Olli (Aug 27 2018 at 19:46):

finally got it via the term way, very satisfying once it clicks

#### Olli (Aug 27 2018 at 19:47):

I think I'll enjoy the tactics language as well, as I've found stack based languages fun to play with in the past

#### Kevin Buzzard (Aug 27 2018 at 19:49):

...and here's a term proof:

example (p q r : Prop) : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
⟨λ h,⟨λ hp,h $or.inl hp,λ hq, h$ or.inr hq⟩,λ h hpq,or.elim hpq h.1 h.2⟩


#### Kevin Buzzard (Aug 27 2018 at 19:51):

The and.intro is swallowed up with these ⟨⟩ brackets, but you can still see the or stuff.

#### Olli (Aug 27 2018 at 19:51):

yep, I can follow that. The one I wrote is a bit more verbose, but I see how they are the same thing

#### Patrick Massot (Aug 27 2018 at 19:52):

If you don't like decidability assumptions but still like automation, what about:

example (p q r : Prop) : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
begin
split,
{ intro H,
split ; cc },
rintro ⟨Hpr, Hqr⟩ (Hp | Hq) ; cc
end


#### Patrick Massot (Aug 27 2018 at 19:53):

Or you can replace the ccwith Kevin's hand-crafted proofs

#### Patrick Massot (Aug 27 2018 at 19:54):

but at least use rintro

#### Patrick Massot (Aug 27 2018 at 19:54):

Because unpacking stuff is not that interesting

#### Patrick Massot (Aug 27 2018 at 19:55):

and of course there are many many variations, including hybrid tactic/term proofs

#### Bryan Gin-ge Chen (Aug 27 2018 at 20:13):

When I hover over rintro in VS code I seem to get an error in the popup about interactive.param_desc. I don't really get it but maybe there's some missing description like in Kevin's post here https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/lean.20golf/near/132604473 . I'm guessing this is low priority and I shouldn't worry about this anyways.

Reading the rintro docstring made me want to play around with rintro?. However, appending a question mark to rcases in the above proof just resulted in an "unexpected token" error. Is there a better example I can try?

#### Patrick Massot (Aug 27 2018 at 20:14):

The small_nat thing was fixed by Mario today, but maybe not pushed yet

#### Olli (Aug 28 2018 at 15:14):

I could use another hint here as I can't seem to make progress:

#### Kevin Buzzard (Aug 28 2018 at 15:30):

Oh but this is tricky! Here's a hint: prove not p. Or just use the law of the excluded middle :-)

#### Kevin Buzzard (Aug 28 2018 at 15:35):

theorem easy (p : Prop) : ¬(p ↔ ¬p) :=
assume h,
have hpinp : p → ¬p, from h.mp,  -- p → p → false
have hnpip : ¬p → p, from h.mpr, -- p → false → p
begin
cases classical.em p with hp hnp,
exact hpinp hp hp,
exact hnp (hnpip hnp),
end

#print axioms easy -- more than none


Sorry -- I'm a mathematician.

(deleted)

#### Olli (Aug 28 2018 at 16:30):

thanks, there are other exercises that are marked under classical reasoning but this one isn't one of them, I'll study up on the previous discussion

#### Kevin Buzzard (Aug 28 2018 at 16:36):

Or try my hint :-)

#### Olli (Aug 28 2018 at 16:43):

I got it now, but had to look up almost the full solution before getting it. very tricky indeed.

My plan is to solve all the exercises first using term level solutions that read as naturally as possible, then go and write a second pass removing all the syntax sugar, and then move on to the tactics chapter and re-write them all using those again

#### Xita Meyers (Sep 12 2018 at 16:53):

Hello, I currently have:

nine : 2 ∣ p / 2,
thing11 : 3 + 4 * (p / 4) = p
⊢ false


p is a prime. I'm stuck; does anyone have any hints on how to proceed?

#### Kenny Lau (Sep 12 2018 at 17:18):

example (p : ℕ) (nine : 2 ∣ p / 2) (thing11 : 3 + 4 * (p / 4) = p) : false :=
begin
rw ← thing11 at nine,
change 2 ∣ (3 + (2 * 2) * (p / 4)) / 2 at nine,
{ exact absurd nine dec_trivial },
{ exact dvd_mul_right _ _ },
{ exact dec_trivial }
end


#### Kenny Lau (Sep 12 2018 at 17:19):

@Chris Hughes somehow I find this very hard; can you help?

#### Chris Hughes (Sep 12 2018 at 17:31):

My best attempt is this

example (p : ℕ) (nine : 2 ∣ p / 2) (thing11 : 3 + 4 * (p / 4) = p) : false :=
by rw [← thing11, show 4 = 2 * 2, from rfl, mul_assoc, nat.add_mul_right_div _ _ (nat.succ_pos _),


#### Reid Barton (Sep 12 2018 at 17:48):

The high level strategy here is to substitute thing11 into nine -- now you have just one hypothesis -- and then simplify it using properties of divisibility until you get something like 2 divides 3 which can be killed by dec_trivial

#### Kenny Lau (Sep 12 2018 at 17:55):

easier said than done

#### Kenny Lau (Sep 12 2018 at 17:56):

considering how we both substituted thing11 into nine on the first step and never touched thing11 afterwards

#### Reid Barton (Sep 12 2018 at 18:02):

Yes, the one hypothesis I meant was nine

#### Kevin Buzzard (Sep 12 2018 at 18:48):

Why not do cases on p mod 4?

#### Kevin Buzzard (Sep 12 2018 at 18:55):

There are a bunch of missing (perhaps) lemmas which would make this easy.

#### Kevin Buzzard (Sep 12 2018 at 18:57):

I ran into one of these earlier today, I had p/2 < x <= p-1 and I wanted to prove -p/2 <= x-p or some such thing, it was harder than it should be but I felt that we could make this easier somehow.

#### Kenny Lau (Sep 12 2018 at 19:01):

Why not do cases on p mod 4?

because nobody knows that p mod 4 is given 2 | p/2

#### Huyen Chau Nguyen (May 14 2019 at 04:04):

Hey guys, I want to ask about the cardinality of sets. I'm totally newbie to Lean so the questions might be trivial. Still, I need your help.

I encounter this error message:

"type mismatch, term
{l : list ℕ | isCanonnicalPartition n l}
has type
set (list ℕ)
but is expected to have type
finset (list ℕ)"

I interpret this as the LHS of my statement had been declared a finset, whereas Lean isnt sure the RHS is really a finset.

How could I tell Lean that a set constructed in a particular way is guaranteed to be a finset? Or is there any other way to fix this error message?

Thank you very much for your response!

#### Kevin Buzzard (May 14 2019 at 07:18):

a finset is not the same as a set. A finset is not "a set, plus some more stuff".

#### Kevin Buzzard (May 14 2019 at 07:20):

If you want some help, I would urge you to post a minimal working example of your code, rather than a fragment or just an error message. Quote code within triple backticks   , or even better use  lean  to quote Lean code with syntax highlighting.

#### Kevin Buzzard (May 14 2019 at 07:24):

There are lots of potential solutions to your situation but it's difficult to know what the best one is without seeing the code. As an example, if you want to say that a set is equal to a finset, you could just coerce the finset into a set. Alternatively if you want to map a set plus a proof that it's finite into type finset then this is no doubt also possible (but I don't know the finset API well enough to know how to do it off the top of my head). The best solution might be to never use sets at all. It depends on what you want to do.

#### Mario Carneiro (May 14 2019 at 07:29):

finite.to_finset will convert a set that is finite to a finset

#### Mario Carneiro (May 14 2019 at 07:30):

but in this case you are left with proving that the set is finite, which basically amounts to constructing a finset

#### Huyen Chau Nguyen (May 14 2019 at 09:36):

Okie thank you guys, I would post part of my code back here later.

Last updated: May 15 2021 at 23:13 UTC