Zulip Chat Archive

Stream: new members

Topic: Guarantee a set to be a finset


view this post on Zulip 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 add,
  unfold cross_prod,
  unfold zero,
  dsimp,
  congr,
  simp,
  rw mul_add,
  rw add_comm,
  rw mul_add,
  rw add_comm,
  rw add_assoc,

end
end vector

view this post on Zulip Patrick Massot (Aug 17 2018 at 21:24):

Are you willing to use mathlib?

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

view this post on Zulip JIANXIONG SUN (Aug 17 2018 at 21:29):

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

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

view this post on Zulip Patrick Massot (Aug 17 2018 at 21:33):

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

view this post on Zulip Patrick Massot (Aug 17 2018 at 21:34):

(deleted)

view this post on Zulip Kenny Lau (Aug 17 2018 at 21:56):

how do we call that type of equality?

view this post on Zulip Patrick Massot (Aug 17 2018 at 21:57):

it's what the parser parses

view this post on Zulip Sebastian Ullrich (Aug 17 2018 at 21:58):

Structural equality

view this post on Zulip Patrick Massot (Aug 17 2018 at 21:58):

yeah, sounds more impressive

view this post on Zulip Kenny Lau (Aug 17 2018 at 21:59):

why "structure"?

view this post on Zulip Patrick Massot (Aug 17 2018 at 22:00):

why not "ontological equality"?

view this post on Zulip Chris Hughes (Aug 17 2018 at 22:00):

How many degrees of equality are there?

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

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

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

view this post on Zulip Patrick Massot (Aug 19 2018 at 20:23):

Your installation of mathlib seems to have a problem

view this post on Zulip Patrick Massot (Aug 19 2018 at 20:23):

maybe you should try to rebuild it

view this post on Zulip JIANXIONG SUN (Aug 19 2018 at 20:44):

I tried it but it seems not work

view this post on Zulip Simon Hudon (Aug 19 2018 at 21:03):

After rebuilding, did you restart your Lean server?

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

view this post on Zulip Simon Hudon (Aug 20 2018 at 22:21):

You can try assoc_rw [mul_comm]

view this post on Zulip JIANXIONG SUN (Aug 20 2018 at 22:29):

You mean right after intro c?

view this post on Zulip JIANXIONG SUN (Aug 20 2018 at 22:31):

What's the meaning of the square bracket here?

view this post on Zulip Simon Hudon (Aug 20 2018 at 22:31):

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

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

view this post on Zulip JIANXIONG SUN (Aug 20 2018 at 22:37):

It says that `assoc_rwis an unknown identifier, Capture.PNG

view this post on Zulip Simon Hudon (Aug 20 2018 at 22:38):

Are you using mathlib?

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

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

view this post on Zulip JIANXIONG SUN (Aug 20 2018 at 22:45):

I would try this tomorrow, thank you

view this post on Zulip Simon Hudon (Aug 20 2018 at 22:55):

Why do you say AC rewriting is overpowered?

view this post on Zulip JIANXIONG SUN (Aug 20 2018 at 23:00):

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

view this post on Zulip Simon Hudon (Aug 20 2018 at 23:04):

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

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

view this post on Zulip Simon Hudon (Aug 27 2018 at 19:18):

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

view this post on Zulip Patrick Massot (Aug 27 2018 at 19:18):

I have a hint: use tactic mode

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

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

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

view this post on Zulip Patrick Massot (Aug 27 2018 at 19:23):

Then move on to interesting maths

view this post on Zulip Patrick Massot (Aug 27 2018 at 19:24):

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

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

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

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

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

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

view this post on Zulip Olli (Aug 27 2018 at 19:46):

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

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

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

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

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

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

view this post on Zulip Patrick Massot (Aug 27 2018 at 19:53):

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

view this post on Zulip Patrick Massot (Aug 27 2018 at 19:54):

but at least use rintro

view this post on Zulip Patrick Massot (Aug 27 2018 at 19:54):

Because unpacking stuff is not that interesting

view this post on Zulip Patrick Massot (Aug 27 2018 at 19:55):

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

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

view this post on Zulip Patrick Massot (Aug 27 2018 at 20:14):

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

view this post on Zulip Olli (Aug 28 2018 at 15:14):

I could use another hint here as I can't seem to make progress:
https://gist.github.com/luxbock/e8a4146ab822049da4d440adc8d7f01c

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

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

view this post on Zulip Bryan Gin-ge Chen (Aug 28 2018 at 15:50):

There's a previous thread about this here (with proofs avoiding excluded middle) https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/Logic.20.26.20Proof/near/127708058

view this post on Zulip Kevin Buzzard (Aug 28 2018 at 16:00):

(deleted)

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

view this post on Zulip Kevin Buzzard (Aug 28 2018 at 16:36):

Or try my hint :-)

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

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

view this post on Zulip 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,
  rw [mul_assoc, nat.add_mul_div_left,  nat.dvd_add_iff_left] at nine,
  { exact absurd nine dec_trivial },
  { exact dvd_mul_right _ _ },
  { exact dec_trivial }
end

view this post on Zulip Kenny Lau (Sep 12 2018 at 17:19):

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

view this post on Zulip 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 _),
    nat.dvd_iff_mod_eq_zero, nat.add_mul_mod_self_left] at nine;
  contradiction

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

view this post on Zulip Kenny Lau (Sep 12 2018 at 17:55):

easier said than done

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

view this post on Zulip Reid Barton (Sep 12 2018 at 18:02):

Yes, the one hypothesis I meant was nine

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 18:48):

Why not do cases on p mod 4?

view this post on Zulip Kevin Buzzard (Sep 12 2018 at 18:55):

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

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (May 14 2019 at 07:29):

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

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

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