Guarantee a set to be a finset

Stream: new members

[JIANXIONG SUN]

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

[Patrick Massot]

Are you willing to use mathlib?

[Patrick Massot]

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]

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

[Chris Hughes]

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

[Patrick Massot]

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

[Patrick Massot]

(deleted)

[Kenny Lau]

how do we call that type of equality?

[Patrick Massot]

it's what the parser parses

[Sebastian Ullrich]

Structural equality

[Patrick Massot]

yeah, sounds more impressive

[Kenny Lau]

why "structure"?

[Patrick Massot]

why not "ontological equality"?

[Chris Hughes]

How many degrees of equality are there?

[Sebastian Ullrich]

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

[Chris Hughes]

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]

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

[Patrick Massot]

Your installation of mathlib seems to have a problem

[Patrick Massot]

maybe you should try to rebuild it

[JIANXIONG SUN]

I tried it but it seems not work

[Simon Hudon]

After rebuilding, did you restart your Lean server?

[JIANXIONG SUN]

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]

You can try assoc_rw [mul_comm]

[JIANXIONG SUN]

You mean right after intro c?

[JIANXIONG SUN]

What's the meaning of the square bracket here?

[Simon Hudon]

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

[Simon Hudon]

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]

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

[Simon Hudon]

Are you using mathlib?

[Mario Carneiro]

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]

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

[JIANXIONG SUN]

I would try this tomorrow, thank you

[Simon Hudon]

Why do you say AC rewriting is overpowered?

[JIANXIONG SUN]

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

[Simon Hudon]

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

[Olli]

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]

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

[Patrick Massot]

I have a hint: use tactic mode

[Olli]

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]

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]

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]

Then move on to interesting maths

[Patrick Massot]

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

[Olli]

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]

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]

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]

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]

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]

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

[Olli]

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]

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

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

[Olli]

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]

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]

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

[Patrick Massot]

but at least use rintro

[Patrick Massot]

Because unpacking stuff is not that interesting

[Patrick Massot]

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

[Bryan Gin-ge Chen]

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]

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

[Olli]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

(deleted)

[Olli]

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]

Or try my hint :-)

[Olli]

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]

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]

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

[Kenny Lau]

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

[Chris Hughes]

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

[Reid Barton]

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]

easier said than done

[Kenny Lau]

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

[Reid Barton]

Yes, the one hypothesis I meant was nine

[Kevin Buzzard]

Why not do cases on p mod 4?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Why not do cases on p mod 4?

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

[Huyen Chau Nguyen]

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]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Huyen Chau Nguyen]

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