Zulip Chat Archive

Stream: new members

Topic: more basics


view this post on Zulip Iocta (Jan 19 2020 at 02:14):

open classical

variables (α : Type) (p q : α  Prop)
variable a : α
variable r : Prop

example : (x :α, p x)  α :=
λ h, exists.elim h, _

view this post on Zulip Iocta (Jan 19 2020 at 02:16):

@Bryan Gin-ge Chen continuing

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2020 at 02:17):

(link to my past reply in the other thread)

Since α lives in Type, you have to use something like exists.classical_rec_on from mathlib's logic.basic. Also, the example becomes noncomputable because it uses the choice axiom.

view this post on Zulip Iocta (Jan 19 2020 at 02:18):

Hmm, maybe this isn't what I need then. I'm doing this one from the exercises

open classical

variables (α : Type) (p q : α  Prop)
variable a : α
variable r : Prop

example : ( x, p x  r)  ( x, p x)  r :=
iff.intro
(λ h,
and.intro (

(exists.elim h (λ a' h', (exists.intro a') h'.left)))
(exists.elim h (λ a' h', h'.right)))
(λ h,
exists.intro (have ex: _, from h.left, _) _)

view this post on Zulip Iocta (Jan 19 2020 at 02:21):

Is the hole I need to fill here equivalent to the one in the smaller snippet?

view this post on Zulip Iocta (Jan 19 2020 at 02:28):

or maybe I'm just going about this the wrong way..

view this post on Zulip Bryan Gin-ge Chen (Jan 19 2020 at 02:31):

This one can be done without classical. This should hopefully get you on the right track:

example : ( x, p x  r)  ( x, p x)  r :=
iff.intro
(λ h,
  and.intro
    (exists.elim h (λ a' h', (exists.intro a') h'.left))
    (exists.elim h (λ a' h', h'.right))
)
(λ h, exists.elim h.1 (λ x hx, _))

view this post on Zulip Iocta (Jan 19 2020 at 02:38):

Got it, thanks.

view this post on Zulip Iocta (Jan 27 2020 at 04:47):

I'm trying to figure out how to use exists.elim, so I wanted to put an underscore in that (\lambda z, _) and have it tell me what type z has. How can I make it tell me?

example : ( x, p x  q x)  ( x, p x)  ( x, q x) :=
iff.intro
(λ h,
(have foo: _, from exists.elim h (λ z, _),
_)
)
_

view this post on Zulip Kenny Lau (Jan 27 2020 at 05:19):

well what is the type of p?

view this post on Zulip Kenny Lau (Jan 27 2020 at 05:20):

also you should be able to see the type of z in the underscore after it?

view this post on Zulip Iocta (Jan 27 2020 at 06:16):

also you should be able to see the type of z in the underscore after it?

That's what I expected, but it doesn't appear

view this post on Zulip Mario Carneiro (Jan 27 2020 at 06:21):

When I put that in lean, there is an error over "exists" saying it can't synthesize |- Prop, but I can still hover over z to see z : α

view this post on Zulip Mario Carneiro (Jan 27 2020 at 06:22):

You can't use exists.elim unless lean knows what you are trying to prove (the _ in foo: _)

view this post on Zulip Mario Carneiro (Jan 27 2020 at 06:23):

If I remove the have and just use

example : ( x, p x  q x)  ( x, p x)  ( x, q x) :=
iff.intro
(λ h,
(exists.elim h (λ z, _))
)
_

then the underscores are highlighted as you would expect

view this post on Zulip Iocta (Jan 27 2020 at 06:31):

ah putting the cursor over z does display its type

view this post on Zulip Iocta (Jan 27 2020 at 06:33):

I didn't see it originally because there's a fair amount of latency before it appears

view this post on Zulip Iocta (Jan 27 2020 at 06:35):

dunno if that's an intentional delay in lean-mode to make it less distracting or it's just slow

view this post on Zulip Mario Carneiro (Jan 27 2020 at 06:38):

I would guess it's a mix of intentional latency by vscode and lean latency. Hovers that are too aggressive can really get in your way

view this post on Zulip Mario Carneiro (Jan 27 2020 at 06:38):

there is a setting for hover delay in preferences

view this post on Zulip Iocta (Jan 27 2020 at 06:40):

i'm using emacs, it just appears in the bottom bar rather than hovering

view this post on Zulip Iocta (Jan 27 2020 at 07:43):

How can I fill the holes?

variables (α : Type) (p q : α  Prop)
variable a : α
variable r : Prop

example : ( x, p x  q x)  ( x, p x)  ( x, q x) :=
iff.intro
(λ h1,
  exists.elim h1
  (λ a' hpq, or.elim hpq
    (λ pa, or.inl (exists.intro a' pa))
    (λ pq, or.inr (exists.intro a' pq))))
(λ h2, exists.intro a
  (or.elim h2
    (λz, or.inl (exists.elim z (λ s s', _)))
    (λz, or.inr _)))

view this post on Zulip Kevin Buzzard (Jan 27 2020 at 08:23):

Neither of them look true to me so you can't fill them in.

view this post on Zulip Mario Carneiro (Jan 27 2020 at 08:51):

the bad move was exists.intro a. The variable a is not necessary and has nothing to do with the x that satisfies the assumption

view this post on Zulip Iocta (Jan 27 2020 at 20:49):

Ok got it.

view this post on Zulip Iocta (Jan 27 2020 at 20:50):

Might be nice if it would warn me I was spending time trying to fill something that wasn't fillable, if it could tell

view this post on Zulip Kevin Buzzard (Jan 27 2020 at 21:40):

I am pretty sure that such a thing is undecidable!

view this post on Zulip Iocta (Jan 29 2020 at 07:08):

Am I on the right track?

open classical
example : ( x, p x)  ¬ ( x, ¬ p x) :=
iff.intro
(assume p_all_x exists_npx,
  exists.elim
    exists_npx
    (λ a hnpa,
      have hpa: p a, from  p_all_x a,
      absurd hpa hnpa ))
(assume exists_npx a,
  or.elim (em  (p a))
  id
  (λ hnpa, _))

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 07:14):

Well you're not using tactic mode so you're already at a big disadvantage

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 07:15):

I'm not at lean right now but if you post the local context at the underscore (the assumptions and goal) it should be easy to see whether or not the hole is fillable

view this post on Zulip Iocta (Jan 29 2020 at 07:18):

 04e.lean    60  12 error           don't know how to synthesize placeholder
 context:
 α : Type,
 p : α  Prop,
 exists_npx : ¬∃ (x : α), ¬p x,
 a : α,
 hnpa : ¬p a
  p a (lean-checker)

view this post on Zulip Johan Commelin (Jan 29 2020 at 07:19):

How would you prove it in maths?

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 07:27):

Yeah -- the hole is fillable but as Johan says you need to know where you're going.

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 07:29):

and it would be a little easier to fill it in tactic mode. Are you using Lean in a funny way? I'd be tempted to just type "begin end" in place of that underscore. Are you not using Lean "live"?

view this post on Zulip Iocta (Jan 29 2020 at 07:33):

I have emacs running lean-mode with flycheck, not sure if that's normal

view this post on Zulip Iocta (Jan 29 2020 at 07:35):

I haven't seen begin or end yet. been going through the tutorial. currently at https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html

view this post on Zulip Johan Commelin (Jan 29 2020 at 07:38):

@Iocta Honest question: are you a computer scientist or a mathematician? This seems to matter a lot for which style is best when learning Lean.

view this post on Zulip Johan Commelin (Jan 29 2020 at 07:39):

You are currently learning in CS mode. But there are also tutorials that approach Lean in math mode.

view this post on Zulip Johan Commelin (Jan 29 2020 at 07:40):

E.g. http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

view this post on Zulip Iocta (Jan 29 2020 at 07:46):

Oh interesting, I hadn't seen that, will take a look.

view this post on Zulip Kevin Buzzard (Jan 29 2020 at 08:19):

I haven't seen begin or end yet. been going through the tutorial. currently at https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html

You are just one chapter away from Nirvana :-)

view this post on Zulip Iocta (Feb 07 2020 at 04:22):

I'm returning to this problem. I got one step forward(?) but not seeing how to proceed.

variables (α : Type) (p q : α  Prop)
variable r : Prop


theorem contrapositive {p q : Prop} : (p  q)  (¬q  ¬p) :=
λ h hnq hp, hnq (h hp)


example : ( x, p x)  ¬ ( x, ¬ p x) :=
iff.intro
(assume p_all_x exists_npx,
  exists.elim
    exists_npx
    (λ a hnpa,
      have hpa: p a, from  p_all_x a,
      absurd hpa hnpa ))
(λ h,
  have cont: ¬∀ x, p x  x, ¬ p x,
  from (λ z, h (z (_) _)),
  contrapositive cont
)

view this post on Zulip Iocta (Feb 07 2020 at 04:25):

In math I'm not sure I've dug beneath the level of "when negating, just flip the quantifiers" so maybe some strategy there is what I'm missing

view this post on Zulip Yury G. Kudryashov (Feb 07 2020 at 04:34):

You can't prove ¬ (∃ x, ¬ p x) → (∀ x, p x) without using classical reasoning. Your term proves ¬ (∃ x, ¬ p x) → ¬¬(∀ x, p x).

view this post on Zulip Daniel Keys (Feb 09 2020 at 02:34):

@Iocta Here is a lengthy solution to that problem. I also had some issues with one of the directions, but ended up with two solutions after I was helped. The L_2 one using tactic mode is the one that I thought of in the first place but didn't know how to implement. TheL_1can be found within the topics in this chat room. You'll need to open classical.

variables (α : Type) (p q : α  Prop)
variable a : α

theorem T05R : ( x, p x)  ¬ ( x, ¬ p x) :=
begin
    intro hall,
    intro hexi,
    cases hexi with w hw,
    exact hw (hall w)
end

theorem T05L_1 : ¬ ( x, ¬ p x)  ( x, p x) :=
    (assume hnExnpx : ¬ ( x, ¬ p x),
    (λ x, or.elim (em (p x))
    (λ hpx : p x, hpx)
    (λ hnpx : ¬ p x,
    false.elim (hnExnpx (exists.intro x (λ hpx : p x, hnpx hpx))))))

local attribute [instance] classical.prop_decidable
theorem T05L_2 : ¬ ( x, ¬ p x)  ( x, p x) :=
begin
    intros h x,
    by_contradiction H,
    apply h,
    existsi x,
    exact H
end
theorem T05 : ( x, p x)  ¬ ( x, ¬ p x) :=
begin
    exact iff.intro (T05R α p a) (T05L_2 α p a)
end

view this post on Zulip Dan Stanescu (Feb 17 2020 at 14:14):

Newbie question: is there a built-in way to change a goal of the form a ≠ b to a = b -> false? I tried doing by_contradiction on it, but it changes instead to ¬a ≠ b. I can get what I want by something like:

theorem zNEo1 : (0 ≠ 1) = ¬ (0 = 1) := rfl
theorem zNEo2 : ¬ (0 = 1) → (0 ≠ 1) :=
begin
    intro h,
    rw zNEo1,
    exact h,
end

but I feel there should be a better way.

view this post on Zulip Patrick Massot (Feb 17 2020 at 14:16):

theorem zNEo2 : 0  1 :=
begin
    change 0 = 1  false,
end

Is this what you want?

view this post on Zulip Dan Stanescu (Feb 17 2020 at 14:38):

Yes, apparently this takes care of it. Didn't encounter change before. Thank you!

view this post on Zulip Chris Hughes (Feb 17 2020 at 14:39):

It might also be useful to just intro h, and it automatically unfolds \ne

view this post on Zulip Patrick Massot (Feb 17 2020 at 14:39):

It changes the goal to anything which is the same by definition (in a very precise sense).

view this post on Zulip Dan Stanescu (Feb 17 2020 at 14:45):

I thought I tried intro, but apparently not. So 0 ≠ 1 is indeed defined as 0 = 1 → false then?

view this post on Zulip Patrick Massot (Feb 17 2020 at 14:45):

Yes.

view this post on Zulip Patrick Massot (Feb 17 2020 at 14:46):

Are you using VScode?

view this post on Zulip Dan Stanescu (Feb 17 2020 at 14:46):

Yes.

view this post on Zulip Patrick Massot (Feb 17 2020 at 14:48):

You can right-click on the symbol, choose "Go to definition" to get to https://github.com/leanprover/lean/blob/master/library/init/logic.lean#L97-L98 then do the same on the negation symbol to go to https://github.com/leanprover/lean/blob/master/library/init/core.lean#L142-L143

view this post on Zulip Patrick Massot (Feb 17 2020 at 14:49):

This may look like a hard way of learning (sounds like: code is the documentation). But this is actually part of why proof assistants are so cool compared to traditional textbooks: you can always ask and get the answer.

view this post on Zulip Dan Stanescu (Feb 17 2020 at 15:08):

That is great advice. I didn't know about right-click, I only knew to hover the mouse over symbols to get how to type them.

view this post on Zulip Dan Stanescu (Feb 17 2020 at 15:13):

Actually one more question along the same lines. The manual talks about double negation elimination after the excluded middle em, but is there a way to have Lean replace ¬ ¬ P by P without writing our own tool?

view this post on Zulip Dan Stanescu (Feb 17 2020 at 15:27):

Just realized I can probably change it again. :smiley:

view this post on Zulip Chris Hughes (Feb 17 2020 at 15:27):

You can't just change it because they're not equal by definition. There is a lemma classical.not_not you could use to rewrite it.

view this post on Zulip Dan Stanescu (Feb 17 2020 at 15:28):

Great! Thanks again!

view this post on Zulip Patrick Massot (Feb 17 2020 at 15:33):

push_neg should do that for you as well.

view this post on Zulip Daniel Keys (Feb 25 2020 at 18:03):

Can someone explain why I can evaluate the truth value of the 'divide' but not the 'belongs' proposition below? Is there a way to evaluate tt or ff for the latter?

import data.set

def A1 : set  := {1,2,3}
#check (1  A1)
#reduce (1  A1)
-- #reduce to_bool (1 ∈ A1) fails
#check (2  (0:))
#reduce to_bool (2  (0:))

view this post on Zulip Daniel Keys (Feb 25 2020 at 18:48):

Or is this a bug?

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 18:48):

Hmm, I can't reproduce this. With no imports, with both Lean 3.4.2 and Lean 3.5.1, it's the last line which fails with

failed to synthesize type class instance for
⊢ decidable (2 ∣ 0)

With a recent mathlib imported (e.g. with import data.int.basic at the start of the file), I get no errors at all.

Can you say more about what version of Lean you're using / if you're importing some version of mathlib?

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 18:49):

Oh, sorry, I misunderstood. You commented out the line that fails. Let me try again.

view this post on Zulip Daniel Keys (Feb 25 2020 at 18:50):

I only import set, the divides works with just that. I edited to include the import.

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 18:51):

Well, it's not a bug. The error is

failed to synthesize type class instance for
⊢ decidable (1 ∈ A1)

which makes sense, since general set membership is not decidable.

view this post on Zulip Daniel Keys (Feb 25 2020 at 18:54):

Is there something I can do about actually evaluating it? The #reduce does show a Prop which should evaluate to tt.

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 18:54):

For explicit finite sets like this, you might want to use finsets instead:

import data.finset

def F1 : finset  := {1,2,3}
#reduce to_bool (1  F1) -- tt

view this post on Zulip Daniel Keys (Feb 25 2020 at 18:55):

OK, thanks! That works!

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 18:56):

There's a difference between "I know how to prove this in this one case" and "Lean has an algorithm which will solve all questions of this type", that's what's going on

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 18:58):

There is a question here that I don't know how to answer. How would you tell Lean to reduce the argument (1 ∈ A1) before attempting to apply to_bool to it? Somehow, Lean can reduce (1 ∈ A1) to (1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false) and #reduce to_bool (1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false) returns tt, as expected.

view this post on Zulip Daniel Keys (Feb 25 2020 at 18:58):

What is interesting is that the #reduce alone seems to show the same output for both finset and set. Like 1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false for both.

view this post on Zulip Daniel Keys (Feb 25 2020 at 19:00):

Obviously I was typing at the same time as Bryan Gin-ge Chen.

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 19:02):

You might find it interesting to include set_option pp.all true at the start of the file and then look at #print A1 and #print F1 to see how their internals differ.

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 19:04):

def A3 : set  := {n |  a b c : , n + a ^ 3 = b ^ 3 + c ^ 3}

#reduce to_bool (42  A3)

Here's an illustration of the original set problem. Until a few months ago, it was not known whether 42 was in this set or not.

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 19:06):

import tactic

def A3 : set  := {n |  a b c : , n + a ^ 3 = b ^ 3 + c ^ 3}

example : 42  A3 :=
begin
  use 80538738812075974,
  use 80435758145817515,
  use 12602123297335631,
  norm_num
end

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 19:11):

import tactic

def A1 : set  := {1, 2, 3}

instance {n : } : decidable (n  A1) := by unfold A1; simp; apply_instance

#eval to_bool (1  A1) -- tt

view this post on Zulip Daniel Keys (Feb 25 2020 at 19:11):

This result is very recent indeed, Kevin.

I saw the difference in finset versus set. Although I can't read through all of it, finset has several places with decidable. I guess that makes for the different result.

view this post on Zulip Daniel Keys (Feb 25 2020 at 19:12):

Thank you both!

view this post on Zulip Bryan Gin-ge Chen (Feb 25 2020 at 19:14):

It may be more enlightening to look at how finsets are implemented as compared to sets. In short, finsets are backed by explicit lists modulo ordering and a proof that each element occurs once, whereas sets are simply abstract functions to Prop.

view this post on Zulip Daniel Keys (Feb 25 2020 at 19:15):

Yes, indeed - this makes it clear.

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 19:16):

finset.decidable_mem : Π {α : Type u_1} [h : decidable_eq α] (a : α) (s : finset α), decidable (a ∈ s)

Note that you still need decidable equality on your type, it's not just finiteness. The naturals have decidable equality.

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 19:17):

import tactic
import data.finset
import data.real.basic

noncomputable def A1 : finset  := {1, 2, 3}

#eval to_bool ((1 : )  A1) -- fails

The reals don't.

view this post on Zulip Iocta (Mar 01 2020 at 07:06):

Thanks.

view this post on Zulip Iocta (Mar 01 2020 at 07:06):

When applying simp, is there a way to find out what it did?

view this post on Zulip Bryan Gin-ge Chen (Mar 01 2020 at 07:13):

Yes, to a certain extent. See the options described here.

view this post on Zulip Bryan Gin-ge Chen (Mar 01 2020 at 07:14):

There's also squeeze_simp if you import mathlib's tactics.

view this post on Zulip Iocta (Mar 01 2020 at 07:21):

aha

view this post on Zulip Reid Barton (Mar 01 2020 at 15:16):

I usually use set_option trace.simplify.rewrite true instead, that shows you only what simp actually did (at least approximately, I remember there being some weird caveats). The trace.simplify output is everything simp tried (which is to say, everything) even if it didn't work.

view this post on Zulip Reid Barton (Mar 01 2020 at 15:16):

Oh I see that's also documented a bit further down.

view this post on Zulip Daniel Keys (Mar 01 2020 at 20:23):

For a general a :ℝ, do we have anything that can be used to produce 0 ≤ a ^ 2? I've been trying with norm_num, but it doesn't work for all a.

view this post on Zulip Alex J. Best (Mar 01 2020 at 20:28):

pow_two_nonneg in algebra/group_power.lean

view this post on Zulip Daniel Keys (Mar 01 2020 at 20:29):

Thanks! That is what I was after, but didn't know where to find it.

view this post on Zulip Alex J. Best (Mar 01 2020 at 20:32):

Yeah I had to guess the name and then search for it in the vscode menu, which requires a little experience, but in this case it is a mathlib convention that squaring is always called pow_two and that 0 ≤ is called nonneg.

view this post on Zulip Kevin Buzzard (Mar 01 2020 at 20:45):

You could probably find this with library_search

view this post on Zulip Daniel Keys (Mar 01 2020 at 20:52):

Didn't use library_search yet. Not sure how to use it. Don't you need to know something to start with, like pow_two for example?

view this post on Zulip Alex J. Best (Mar 01 2020 at 20:56):

Kevin is right you don't need to know anything for this really:

import data.real.basic

example (a : ) : 0  a^2 := by library_search

view this post on Zulip Alex J. Best (Mar 01 2020 at 20:56):

and library_search tells you exactly the same lemma name

view this post on Zulip Daniel Keys (Mar 01 2020 at 20:58):

I see! Great, thanks!

view this post on Zulip Daniel Keys (Mar 01 2020 at 20:59):

This will help a lot, it was very frustrating sometimes as I was searching through lots of files for almost everything.

view this post on Zulip Iocta (Mar 06 2020 at 22:14):

-- With simp
example : (p  q)  r  p  (q  r) :=
iff.intro
begin
intro h,
simp *
end
begin
intro h,
simp *
end
 05.1.lean    87   1 info            0. [simplify.rewrite] [h]: p ==> true
 0. [simplify.rewrite] [h]: q ==> true
 0. [simplify.rewrite] [h]: r ==> true
 0. [simplify.rewrite] [and_self]: true  true ==> true
 0. [simplify.rewrite] [and_self]: true  true ==> true
 (lean-checker)
 05.1.lean    91   1 info            0. [simplify.rewrite] [h]: p ==> true
 0. [simplify.rewrite] [h]: q ==> true
 0. [simplify.rewrite] [and_self]: true  true ==> true
 0. [simplify.rewrite] [h]: r ==> true
 0. [simplify.rewrite] [and_self]: true  true ==> true
 (lean-checker)

How do I translate what trace is saying into code?

view this post on Zulip Johan Commelin (Mar 06 2020 at 22:16):

Use squeeze_simp?

view this post on Zulip Johan Commelin (Mar 06 2020 at 22:17):

It will turn it into code for you.

view this post on Zulip Iocta (Mar 08 2020 at 00:52):

squeeze_simp doesn't seem to reduce the options much here.

example : (p  q)  r  p  (q  r) :=
iff.intro
begin
intro h,
squeeze_simp *, -- Try this: simp only [*, and_self]
end
begin
intro h,
simp *
end

How do I turn the output of set_option trace.simplify.rewrite true (in the example above) manually? I'm not sure what it's trying to tell me. How do I rewrite [h] : q ==> true?

view this post on Zulip Reid Barton (Mar 08 2020 at 01:03):

This example is kind of too simple and relies more on internal behavior of simp than on lemmas.

view this post on Zulip Reid Barton (Mar 08 2020 at 01:04):

But you could start with rw h.1.2

view this post on Zulip Reid Barton (Mar 08 2020 at 01:04):

Wait no

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 01:04):

cases h

view this post on Zulip Reid Barton (Mar 08 2020 at 01:05):

You need whatever lemma it is that says if h : p, then p = true

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 01:05):

just use cases and split

view this post on Zulip Reid Barton (Mar 08 2020 at 01:05):

This rewriting strategy is not a natural way to prove this particular example

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 01:06):

high-powered tactics like simp and rw are not really needed for basic logic questions like this, just use the basic tactics.

view this post on Zulip Iocta (Mar 08 2020 at 01:54):

example : (p  q)  r  p  (q  r) :=
iff.intro
begin
intro h,
cases h with hpq hr,
cases hpq,
repeat {apply and.intro},
repeat {assumption},
end
begin
intro h,
cases h with hp hqr,
cases hqr,
repeat {apply and.intro},
repeat {assumption},
end

works. What would I do with split here?

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 01:55):

split stops you having to do repeat

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 01:55):

it splits an and goal into two goals

view this post on Zulip Iocta (Mar 08 2020 at 02:17):

Not quite seeing how to use it here. What's the function I want to apply to both branches?

view this post on Zulip Iocta (Mar 08 2020 at 07:02):

There must be a shorter way to write this?

example : ¬p  ¬q  ¬(p  q) :=
begin
intros h hpq,
cases h with hnp hnq,
cases hpq with hp hq,
apply hnp hp,
cases hpq with hp hq,
apply hnq hq,
end

view this post on Zulip Kenny Lau (Mar 08 2020 at 07:07):

import logic.basic tactic.tauto

variables (p q : Prop)
example : ¬p  ¬q  ¬(p  q) := not_and_of_not_or_not
example : ¬p  ¬q  ¬(p  q) := λ h, h.cases_on (mt and.left) (mt and.right)
example : ¬p  ¬q  ¬(p  q) := by tauto

view this post on Zulip Iocta (Mar 08 2020 at 07:08):

neat

view this post on Zulip Iocta (Mar 08 2020 at 23:57):

Am I down the wrong path?

example : ¬(p  q)  p  ¬q :=
begin
intro h,
cases (em p) with hp hnp,
cases (em q) with hq hnq,
constructor,
exact hp,
intro hq',
apply h,
intro hp',
exact hq,
constructor,
exact hp,
exact hnq,
cases (em q) with hq hnq,
constructor,
sorry,
end

view this post on Zulip Iocta (Mar 08 2020 at 23:58):

 example   335   1 error           tactic failed, there are unsolved goals
 state:
 2 goals
 p q : Prop,
 h : ¬(p  q),
 hnp : ¬p,
 hq : q
  ¬q

 case or.inr
 p q : Prop,
 h : ¬(p  q),
 hnp : ¬p,
 hnq : ¬q
  p  ¬q (lean-checker)

view this post on Zulip Kevin Buzzard (Mar 09 2020 at 00:06):

You know not X is by definition X -> false? So in the first goal you can intro hq2 and then revert h! When your hypotheses can be used to get a contradiction as yours can, in both cases) then exfalso is sometimes a useful tactic; it replaces the goal by false.

view this post on Zulip Iocta (Mar 09 2020 at 00:28):

thanks

view this post on Zulip Iocta (Mar 09 2020 at 01:21):

 05.01.b.    15   3 error           solve1 tactic failed, focused goal has not been solved
 state:
 α : Type,
 p q : α  Prop,
 h :  (x : α), p x  q x,
 x : α
  p x (lean-checker)

In tactic mode: What's the equivalent of intro h here? I want to get inside of the \forall.

view this post on Zulip Iocta (Mar 09 2020 at 01:22):

(or is that not idiomatic?)

view this post on Zulip Mario Carneiro (Mar 09 2020 at 01:35):

It is generally easier to work forward at this point; have h2 := h x will give you a proof of p x ∧ q x

view this post on Zulip Iocta (Mar 09 2020 at 02:05):

ok

view this post on Zulip Reid Barton (Mar 09 2020 at 04:32):

(what would you expect the tactic state to look like after intro h?)

view this post on Zulip Iocta (Mar 09 2020 at 18:40):

I guess intro isn't really the right word. What Mario said does what I wanted.

view this post on Zulip Iocta (Mar 09 2020 at 19:05):

How can I avoid repeating assumption?

example (p q r : Prop) (hp : p) :
(p  q  r)  (q  p  r)  (q  r  p) :=
by split; try {split}; {left, assumption} <|> {right, left, assumption} <|> {right, right, assumption}

view this post on Zulip Johan Commelin (Mar 09 2020 at 19:19):

@Iocta I'm not sure if there is much you can do.

view this post on Zulip Johan Commelin (Mar 09 2020 at 19:20):

But if you want to golf this, then certainly by tauto is a lot shorter...

view this post on Zulip Iocta (Mar 09 2020 at 19:23):

Alright

view this post on Zulip Johan Commelin (Mar 09 2020 at 19:26):

I mean... I don't know if you wanted such a logic hammer...

view this post on Zulip Mario Carneiro (Mar 10 2020 at 01:33):

It's actually not a bad example of an introductory level tactic

namespace tactic.interactive
meta def leftright (t : itactic) : tactic unit :=
t <|> (tactic.left >> leftright) <|> (tactic.right >> leftright)
end tactic.interactive

example (p q r : Prop) (hp : p) :
(p  q  r)  (q  p  r)  (q  r  p) :=
by repeat {split}; leftright {assumption}

view this post on Zulip Mario Carneiro (Mar 10 2020 at 01:35):

There is a completely different style of proof represented by

example (p q r : Prop) (hp : p) :
(p  q  r)  (q  p  r)  (q  r  p) :=
by simp [hp]

Here the idea is that you use rewrite rules p ==> true, plus true \/ a ==> true, a \/ true ==> true and true /\ true ==> true to simplify the entire goal to true

view this post on Zulip Iocta (Mar 10 2020 at 04:40):

Ah cool

view this post on Zulip Iocta (Mar 11 2020 at 00:38):

How to fix this?

import tactic.squeeze

namespace hidden

inductive natural : Type
| zero : natural
| succ : natural  natural


open natural


def add (m n : natural) : natural :=
natural.rec_on n m (λ n add_m_n, succ add_m_n)

def mul (m n : natural) : natural :=
natural.rec_on n zero (λ n mul_m_n, add mul_m_n m)


def pred (n : natural) : natural :=
natural.rec_on n zero (λ n pred_n, n)

def sub (m n : natural) : natural :=
natural.rec_on n m (λ n sub_m_n, pred sub_m_n)

local infix ` <*> ` := mul

theorem mul_dist_add (m n k : natural ) : k <*>  add m n = add (k <*> m) (k <*> n) :=
sorry

theorem mul_assoc (m n k : natural ) : m <*> ( n <*> k ) = ( m <*> n ) <*> k :=
natural.rec_on k
(show m <*> (n <*> zero) = (m <*> n) <*> zero, from rfl)
(assume k,
  (assume ih:  m <*> ( n <*> k ) = ( m <*> n ) <*> k,
    show  m <*> ( n <*> (succ k) ) = ( m <*> n ) <*> (succ k),
    from calc
      m <*> ( n <*> (succ k) ) = m <*> (add (n <*> k) n ) : by refl
      ... = add (m <*> (n <*> k)) (m <*> n)  : by apply mul_dist_add
      ... = add ((m <*> n) <*> k) (m <*> n) : by apply ih

  ))

end hidden
 06.1.lean    40  50 error           invalid apply tactic, failed to unify
   add (m <*> (n <*> k)) (m <*> n) = add (m <*> n <*> k) (m <*> n)
 with
   m <*> (n <*> k) = m <*> n <*> k
 state:
 m n k k : natural,
 ih : m <*> (n <*> k) = m <*> n <*> k
  add (m <*> (n <*> k)) (m <*> n) = add (m <*> n <*> k) (m <*> n) (lean-checker)

view this post on Zulip Reid Barton (Mar 11 2020 at 00:41):

The easy way is by rw ih

view this post on Zulip Reid Barton (Mar 11 2020 at 00:41):

there's also a harder way

view this post on Zulip Iocta (Mar 11 2020 at 00:47):

How do I do the harder way? I tried using trace to see what simp * was doing but it wasn't all that helpful

view this post on Zulip Reid Barton (Mar 11 2020 at 00:47):

Using congr_arg somehow

view this post on Zulip Reid Barton (Mar 11 2020 at 00:48):

maybe congr_arg (\lam x, add x (m <*> n)) ih

view this post on Zulip Reid Barton (Mar 11 2020 at 00:48):

anyways, this is where rw starts to become indispensable

view this post on Zulip Iocta (Mar 11 2020 at 00:53):

ok that works

view this post on Zulip Mario Carneiro (Mar 11 2020 at 00:54):

You can probably use \t for this

view this post on Zulip Mario Carneiro (Mar 11 2020 at 00:55):

ih ▸ rfl works

view this post on Zulip Mario Carneiro (Mar 11 2020 at 01:02):

The unnecessarily compressed proof:

theorem mul_assoc (m n k) : m <*> (n <*> k) = (m <*> n) <*> k :=
natural.rec_on k rfl $ λ k ih,
(mul_dist_add _ _ _).trans (ih.symm  rfl)

view this post on Zulip Iocta (Mar 11 2020 at 01:04):

What's the difference between exact and apply? Example: exact (eq.subst ih rfl) but apply (eq.subst ih rfl) doesn't.

view this post on Zulip Mario Carneiro (Mar 11 2020 at 01:05):

apply f means refine f or refine f _ or refine f _ _ or ... depending on the type of f. Sometimes it can't guess right, and more importantly for your example, it can't communicate the expected type of f when elaborating it because it doesn't know yet

view this post on Zulip Mario Carneiro (Mar 11 2020 at 01:05):

On the other hand eq.subst requires that the expected type be known

view this post on Zulip Iocta (Mar 11 2020 at 01:08):

ah ok

view this post on Zulip Iocta (Mar 11 2020 at 19:24):

theorem zero_add (n : natural) : add n zero = n :=
natural.cases_on n
(by refl)
(assume m: natural,
  (assume ih : add m zero = m,
  show add (succ m) zero = succ m,
  from calc
    add (succ m) zero = succ (add m zero) : by refl
    ... = succ m : by simp * at *))
 06.1.lean    31   1 error           "eliminator" elaborator type mismatch, term
   λ (m : natural) (ih : add m zero = m),
     show add (succ m) zero = succ m, from
       eq.trans (eq.refl (add (succ m) zero))
         (eq.mpr
            (id
               (eq.trans
                  (eq.trans
                     ((λ (a a_1 : natural) (e_1 : a = a_1) (a_2 a_3 : natural) (e_2 : a_2 = a_3),
                         congr (congr_arg eq e_1) e_2)
                        (succ (add m zero))
                        (succ m)
                        ((λ (a a_1 : natural) (e_1 : a = a_1), congr_arg succ e_1) (add m zero) m ih)
                        (succ m)
                        (succ m)
                        (eq.refl (succ m)))
                     succ.inj_eq)
                  (propext (eq_self_iff_true m))))
            trivial)
 has type
    (m : natural), add m zero = m  add (succ m) zero = succ m
 but is expected to have type
    (a : natural), add (succ a) zero = succ a

view this post on Zulip Iocta (Mar 11 2020 at 19:25):

How to fix this?

view this post on Zulip Iocta (Mar 11 2020 at 19:26):

I think it's saying "you're trying to depend on ih but I'm not providing it"

view this post on Zulip Mario Carneiro (Mar 11 2020 at 19:26):

use rec_on not cases_on

view this post on Zulip Iocta (Mar 11 2020 at 19:26):

oh. that was easy :-)

view this post on Zulip Iocta (Mar 11 2020 at 19:29):

is it a good idea to introduce that m to avoid confusing that variable with the enclosing n, or should I just use n again?

view this post on Zulip Iocta (Mar 11 2020 at 19:30):

(really just asking what the convention is)

view this post on Zulip Iocta (Mar 11 2020 at 19:40):

aha, the code I can find looks to pretty uniformly reuse n

view this post on Zulip Reid Barton (Mar 11 2020 at 20:02):

Yes, this seems to be the normal convention

view this post on Zulip Iocta (Mar 12 2020 at 00:57):

namespace hidden

universe u

inductive list (α : Type u)
| nil {} : list
| cons : α  list  list

namespace list

variable {α : Type}

notation h :: t  := cons h t

def append (s t : list α) : list α :=
list.rec t (λ x l u, x::u) s

notation s ++ t := append s t

theorem nil_append (t : list α) : nil ++ t = t := rfl

theorem cons_append (x : α) (s t : list α) :
  x::s ++ t = x::(s ++ t) := rfl

theorem append_nil (t : list α) : t ++ nil = t :=
list.rec_on t
rfl
(assume t,
  (assume ih: t ++ nil = t, sorry ))


end list

end hidden
 06.2.lean    29  17 error           none of the overloads are applicable
 error for hidden.list.append
 type mismatch at application
   append t
 term
   t
 has type
   α
 but is expected to have type
   list ?m_1

 error for has_append.append
 failed to synthesize type class instance for
 α : Type,
 t : list α,
 t : α
  has_append α

view this post on Zulip Iocta (Mar 12 2020 at 00:58):

I'm guessing I'm doing the namespacing wrong?

view this post on Zulip Reid Barton (Mar 12 2020 at 01:23):

I think your code is just wrong

view this post on Zulip Reid Barton (Mar 12 2020 at 01:25):

in the inductive case, what happened to the element that is the first argument to cons? You aren't taking enough arguments

view this post on Zulip Mario Carneiro (Mar 12 2020 at 01:55):

I think the issue is that the ++ notation is conflicting with the one from core (which uses the has_append typeclass)

view this post on Zulip Mario Carneiro (Mar 12 2020 at 01:57):

oh, reid is right, there is another argument to list.rec_on. The setup should look like this:

theorem append_nil (t : list α) : t ++ nil = t :=
list.rec_on t
rfl
(assume a t,
  (assume ih: t ++ nil = t,
    show (a :: t) ++ nil = a :: t, from
    sorry ))

view this post on Zulip Iocta (Mar 12 2020 at 05:07):

Oh, I see

view this post on Zulip Iocta (Mar 12 2020 at 20:11):

https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

def length : Π {α : Type u}, list α  nat :=
(λ α, (λ s, list.rec_on s 0 (λ a s len, len + 1)))

How do I state a theorem "length nil = 0"?

view this post on Zulip Iocta (Mar 12 2020 at 20:13):

example : length  nil  = 0 :=
sorry
 06.2.lean    55  19 error           don't know how to synthesize placeholder
 context:
  Type ? (lean-checker)

view this post on Zulip Patrick Massot (Mar 12 2020 at 20:16):

Lean complains it doesn't know the type of nil.

view this post on Zulip Patrick Massot (Mar 12 2020 at 20:16):

Because there is no way it can reconstruct α from your statement.

view this post on Zulip Patrick Massot (Mar 12 2020 at 20:17):

Good news is: one the statement will type-check, the proof will be pretty short.

view this post on Zulip Reid Barton (Mar 12 2020 at 20:17):

There's no implicit generalization like in Haskell and some other languages. You have to write something like example (a : Type) : length (nil : list a) = 0

view this post on Zulip Iocta (Mar 12 2020 at 20:19):

aha, that works

view this post on Zulip Patrick Massot (Mar 12 2020 at 20:20):

Because Reid gave away the statement, you are allowed only three characters to write the proof.

view this post on Zulip Iocta (Mar 12 2020 at 20:22):

yeah, got it

view this post on Zulip Iocta (Mar 12 2020 at 21:09):

def reverse : Π {α : Type u}, list α  list α :=
(λ α,
  (λ s,
    list.rec_on s
    nil
    (λ (x: α) (s: list α) (reversed: list α),
      append reversed (x::nil)  )))
 06.2.lean    90   7 error           type mismatch at application
   append reversed
 term
   reversed
 has type
   list α : Type u
 but is expected to have type
   list ?m_1 : Type
...
   type mismatch, term
     ?m_2 ++ ?m_3
   has type
     list ?m_1 : Type
   but is expected to have type
     list α : Type u (lean-checker)

view this post on Zulip Iocta (Mar 12 2020 at 21:11):

I can just delete the u and it works, but what is the difference between u and no u?

view this post on Zulip Iocta (Mar 12 2020 at 21:12):

because the def length : Π {α : Type u}, list α → nat := one does have a u

view this post on Zulip Reid Barton (Mar 12 2020 at 21:16):

Somewhere you must have Type with no u

view this post on Zulip Iocta (Mar 12 2020 at 21:18):

yeah I do

view this post on Zulip Iocta (Mar 13 2020 at 22:26):

I'm not getting the picture here. "Define an inductive data type consisting of terms built up from the following constructors..." https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html

namespace hidden

universe u
variable {α : Type u}


inductive expr (α : Type u)
| const (n: nat) : expr
| var (n: nat) : expr
| plus (s t : expr)  : expr
| times (s t: expr)  : expr

namespace expr
def eval (x: expr α) : nat :=
begin
cases x,
case const : {exact x},
case var : {exact x},
case plus : s t {exact ((eval s) + (eval t))},
case times : s t  {exact ((eval s) * (eval t))},
end
end expr
end hidden
 06.03.le    19  26 error           unknown identifier 'eval'
 state:
 case hidden.expr.plus
 α : Type u,
 s t : expr α
   (lean-checker)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:28):

You can't use eval in the definition of eval

view this post on Zulip Iocta (Mar 13 2020 at 22:29):

Then how do I recurse?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:31):

This is all a bit CS for me, so don't take what I have to say too seriously.

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:31):

but when you made the inductive type, Lean made a recursor for you

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:31):

After the definition of expr, try #print prefix expr

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:32):

wait, better is #print prefix hidden.expr

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:33):

All that crazy stuff got made when you defined expr. In particular hidden.expr.rec got made, and if that doesn't do the job then nothing will

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:35):

or you can use match but maybe that's not covered until chapter 8

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:35):

hmm maybe you can't use match, I should stop talking. Does the recursor do it for you?

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:37):

I think you're supposed to be eating f : nat -> nat as well, and var n is supposed to evaluate to f n

view this post on Zulip Iocta (Mar 13 2020 at 22:37):

If you mean like this

def eval (x: expr α) : nat :=
begin
cases x,
case const : n {exact n },
case var : n {exact n},
case plus : s t {exact (s.rec + t.rec)},
case times : s t  {exact (s.rec ) * (t.rec)},
end

then

 06.03.le    21  18 error           type mismatch at application
   expr.rec s
 term
   s
 has type
   expr α : Type
 but is expected to have type
   Π (n : ), ?m_1 (const ?m_2 n) : Sort (imax 1 ?)

view this post on Zulip Chris Hughes (Mar 13 2020 at 22:37):

This is how you recurse

def eval : expr α  nat
| (const _ x) := x
| (var _ x) := x
| (plus s t) := eval s + eval t
| (times s t) := eval s * eval t

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:38):

You're not really supposed to be making data using tactic mode, but that is not the issue right now. How about induction x instead of cases x?

view this post on Zulip Chris Hughes (Mar 13 2020 at 22:38):

You can use induction instead of cases as well, but eval won't be called eval it will be called something like x_ih

view this post on Zulip Iocta (Mar 13 2020 at 22:39):

Aha, that helps

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:41):

That usage of the equation compiler isn't covered until chapter 8

view this post on Zulip Chris Hughes (Mar 13 2020 at 22:44):

The chapter 7 approved way

def eval (x : expr α) : nat :=
expr.rec_on x id id (λ s t ns nt, ns + nt) (λ s t ns nt, ns * nt)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:46):

I think the idea is that the second id should be an f

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:46):

which is an input function

view this post on Zulip Iocta (Mar 13 2020 at 22:49):

Oh that's pretty close to something I had earlier

def eval (x: expr α) : nat :=
expr.rec_on x
id
id
(λ s t, s + t)
(λ s t, s * t)

view this post on Zulip Iocta (Mar 13 2020 at 22:51):

which doesn't work because the latter functions are supposed to take ( outside outside inside inside) not just (inside inside)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:51):

You know you can use _ to figure out what is going on?

view this post on Zulip Iocta (Mar 13 2020 at 22:51):

yeah I just didn't grok what it was telling me

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:53):

def eval (x: expr α) : nat :=
expr.rec_on x
id
id
(λ s t, _)
(_)

->

scratch2.lean:18:8: error
don't know how to synthesize placeholder
context:
α : Type u,
x s t : expr α
⊢ ℕ → ℕ → ℕ
▹
scratch2.lean:19:1: error
don't know how to synthesize placeholder
context:
α : Type u,
x : expr α
⊢ expr α → expr α → ℕ → ℕ → ℕ

so the first hole is expecting two more inputs and the second is expecting four

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:54):

and you can see that s and t have type expr alpha not nat

view this post on Zulip Iocta (Mar 13 2020 at 22:54):

I do see it now :-)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:54):

:-)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:54):

My ability to debug soared once I realised I could understand the error messages

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 22:55):

when I was a beginner I was just all "oh crap it still doesn't work" but now I learnt how to read the error messages I can go "oh look, type class inference failed" or "oh look, I put the wrong number of variables" etc. It is liberating :-)

view this post on Zulip Iocta (Mar 13 2020 at 22:56):

That's consistent with my limited experience so far as well

view this post on Zulip Iocta (Mar 13 2020 at 23:05):

now should I be able to use eval? #reduce expr.eval (const 0)

 06.03.le    18  26 error           failed to synthesize type class instance for
 α : Type u
  has_zero (Type ?) (lean-checker)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:05):

What is the type of const?

view this post on Zulip Iocta (Mar 13 2020 at 23:06):

const : Π (α : Type u_1),   expr α

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:07):

The error says "you wrote 0, so I'll try and figure out a term of the type I was expecting called 0, oh wait, I was expecting a term of type Type u_1

view this post on Zulip Iocta (Mar 13 2020 at 23:07):

aha, so #reduce expr.eval (const nat 0)

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:07):

const alpha 0

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:08):

what is this alpha doing in expr? That's the problem

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:08):

Why not just remove the alpha?

view this post on Zulip Iocta (Mar 13 2020 at 23:09):

yeah that works

view this post on Zulip Iocta (Mar 13 2020 at 23:09):

I haven't got the hang of the alphas and us yet

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:10):

I had to read TPIL three times before I got the hang of it (but then again I suspect I had less of a CS background than you). What helped with me was just coming up with projects and working on them.

view this post on Zulip Chris Hughes (Mar 13 2020 at 23:18):

You have to write const α 0

view this post on Zulip Chris Hughes (Mar 13 2020 at 23:19):

You can change the definition of expr to fix this. Use brackets like this | const {} (n: nat) : expr

view this post on Zulip Kevin Buzzard (Mar 13 2020 at 23:19):

But is alpha playing any role at all? How about we remove all occurences of alpha?

view this post on Zulip Iocta (Mar 15 2020 at 21:04):

I need some help with "Use pattern matching to prove that the composition of surjective functions is surjective"

open function

#print surjective

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}
open function

lemma surjective_comp {g : β  γ} {f : α  β}
  (hg : surjective g) (hf : surjective f) :
surjective (g  f) :=
sorry

view this post on Zulip Iocta (Mar 15 2020 at 21:07):

if I intro gam: \gamma can I destruct it into an element of beta that it came from?

view this post on Zulip Patrick Massot (Mar 15 2020 at 21:59):

Do you want to use mathlib or are you doing TPIL exercises?

view this post on Zulip Patrick Massot (Mar 15 2020 at 22:07):

It seems to be a TPIL exercise. I have no idea what Jeremy had in mind. The closest to a term-mode proof I could do is

lemma surjective_comp {g : β  γ} {f : α  β}
  (hg : surjective g) (hf : surjective f) :
surjective (g  f) :=
assume z,
let y, hy := hg z, x, hx := hf y in
x, by rwa  hx at hy

view this post on Zulip Patrick Massot (Mar 15 2020 at 22:07):

You could replace let with match, adjusting the syntax as needed.

view this post on Zulip Patrick Massot (Mar 15 2020 at 22:08):

But I would rather import mathlib tactics and write:

begin
  intro z,
  rcases hg z with y, rfl,
  rcases hf y with x, rfl,
  use x,
end

view this post on Zulip Iocta (Mar 16 2020 at 01:22):

that's pretty slick

view this post on Zulip Iocta (Mar 16 2020 at 04:08):

What's the match version look like? I'm not getting the syntax right.

match hg, hf with
y, hy, x, hx := hg g , hf f
end
x, by simp [hx, hy]

view this post on Zulip Iocta (Mar 18 2020 at 06:23):

instance sum_inhabited {a b : Type u} [inhabited a] [inhabited b] : inhabited  (sum a b) :=
 default _ 

works but how do I find out what's going in the _?

view this post on Zulip Iocta (Mar 18 2020 at 06:36):

or, (independent of how to find out), what is going in the _?

view this post on Zulip Bryan Gin-ge Chen (Mar 18 2020 at 06:39):

#print sum_inhabited helps here:

@[instance]
protected def sum_inhabited : Π {a b : Type u} [_inst_1 : inhabited a] [_inst_2 : inhabited b], inhabited (a  b) :=
λ {a b : Type u} [_inst_1 : inhabited a] [_inst_2 : inhabited b], {default := default (a  b) sum.inhabited_right}

(Sometimes you have to turn off pretty printing and notation with #print with set_option pp.all true to get the info you want, but this seems like enough.)

view this post on Zulip Bryan Gin-ge Chen (Mar 18 2020 at 06:41):

Compare the output with set_option pp.notation false:

@[instance]
protected def sum_inhabited : Π {a b : Type u} [_inst_1 : inhabited a] [_inst_2 : inhabited b], inhabited (sum a b) :=
λ {a b : Type u} [_inst_1 : inhabited a] [_inst_2 : inhabited b], {default := default (sum a b) sum.inhabited_right}

view this post on Zulip Iocta (Mar 18 2020 at 06:44):

I see

view this post on Zulip Mario Carneiro (Mar 18 2020 at 06:51):

By the way, the only way a proof of an inhabited instance like ⟨ default _ ⟩ can work is if there is already an inhabited instance for that type

view this post on Zulip Mario Carneiro (Mar 18 2020 at 06:51):

in other words, the instance is useless because it's already there, and by apply_instance should also work

view this post on Zulip Iocta (Mar 18 2020 at 06:52):

mhmm

view this post on Zulip Iocta (Mar 19 2020 at 22:00):

can I import a module import foo.bar and access foo.bar.baz without opening bar?

view this post on Zulip Iocta (Mar 19 2020 at 22:05):

import logic.basic seems to open it automatically?

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 22:06):

The definitions in logic.basic are probably not in any namespace called logic or logic.basic

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 22:07):

Definition X in file Y is just called X after you import Y

view this post on Zulip Iocta (Mar 19 2020 at 22:07):

#check not_or_distrib doesn't work unless I import logic.basic

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 22:08):

that's because this function is defined in logic.basic

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 22:09):

but the only namespace used in logic.basic is classical, so after you import logic.basic you have stuff like not_or_distrib (in the root namespace) and classical.not_forall (in the classical namespace)

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 22:10):

there is no logic.basic namespace, even after importing it

view this post on Zulip Iocta (Mar 19 2020 at 22:12):

I see

view this post on Zulip Iocta (Mar 20 2020 at 03:54):

Doing #3 from https://leanprover.github.io/logic_and_proof/sets_in_lean.html

import data.set
import logic.basic

variables {I U : Type}
variables (A : I  set U) (B : I  set U) (C : set U)



theorem Inter.intro {x : U} (h :  i, x  A i) : x   i, A i :=
by simp; assumption

@[elab_simple]
theorem Inter.elim {x : U} (h : x   i, A i) (i : I) : x  A i :=
by simp at h; apply h

theorem Union.intro {x : U} (i : I) (h : x  A i) :
  x   i, A i :=
by {simp, existsi i, exact h}

theorem Union.elim {b : Prop} {x : U}
(h₁ : x   i, A i) (h₂ :  (i : I), x  A i  b) : b :=
by {simp at h₁, cases h₁ with i h, exact h₂ i h}



example : ( i, A i)  ( i, B i)  ( i, A i  B i) :=
assume x h T h2,
begin
simp * at *,
apply exists.elim h2,
intro i,
intro teq,
apply and.elim h,
intros fa fb,
apply eq.subst teq,
apply and.intro,
apply fa i,
apply fb i,
end

I have a proof using the regular logic functions, but I'm not sure how to write the proof using Inter.elim etc.

example : ( i, A i)  ( i, B i)  ( i, A i  B i) :=
begin
intros x h S h2,

end

view this post on Zulip Iocta (Mar 20 2020 at 03:55):

I U : Type,
A B : I  set U,
x : U,
h : x  ( (i : I), A i)   (i : I), B i,
S : set U,
h2 : S  set.range (λ (i : I), A i  B i)
 x  S

view this post on Zulip Kenny Lau (Mar 20 2020 at 04:15):

thanks for creating a copy-paste-able example.

view this post on Zulip Kenny Lau (Mar 20 2020 at 04:17):

you might want to start from here:

example : ( i, A i)  ( i, B i)  ( i, A i  B i) :=
begin
  intros x h,
  have h1 : x  ( (i : I), A i) := h.1,
  have h2 : x  ( (i : I), B i) := h.2,
end
state:
I U : Type,
A B : I  set U,
x : U,
h : x  ( (i : I), A i)   (i : I), B i,
h1 : x   (i : I), A i,
h2 : x   (i : I), B i
 x   (i : I), A i  B i

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:17):

Note that you can also do this directly:

example : ( i, A i)  ( i, B i)  ( i, A i  B i) :=
begin
rintros x h1, h2,

end

view this post on Zulip Iocta (Mar 22 2020 at 03:35):

example : ( i, A i)  ( i, B i)  ( i, A i  B i) :=
begin
intros j h ,
cases h,
apply Inter.intro _ _,
simp only [set.mem_inter_eq],
intro i,
split,
apply Inter.elim,
apply h_left,
apply Inter.elim,
apply h_right,
end

works but I'm guessing there's a better solution, this isn't easy to follow.

view this post on Zulip Iocta (Mar 22 2020 at 07:44):

section
parameters {A : Type} {R : A  A  Prop}
parameter (irreflR : irreflexive R)
parameter (transR : transitive R)

local infix < := R

def R' (a b : A) : Prop := R a b  a = b
local infix  := R'




theorem reflR' (a : A) : a  a :=
or.inr rfl

theorem transR' {a b c : A} (h1 : a  b) (h2 : b  c):
  a  c :=
or.elim h1
(assume rab, or.elim h2
  (assume rbc,  (or.inl (transR rab rbc)))
  (assume eqbc, (or.inl (eq.subst eqbc rab) )) )
(assume eqab, or.elim h2
  (assume rbc, (or.inl (eq.substr eqab rbc)))
  (assume eqbc, (or.inr (eq.substr eqab eqbc))))


theorem transR'' {a b c : A} (h1 : a  b) (h2 : b  c):
  a  c :=
begin
intros,
cases h1,
cases h2,
left,
apply transR
end
 lap14.4.…    35   1 error           unknown identifier 'transR'

I did a term proof, now trying the tactic proof. In the last line, how come it doesn't know about transR?

view this post on Zulip Shing Tak Lam (Mar 22 2020 at 08:29):

@Iocta

Add include transR below the parameter (transR : transitive R)

So the beginning looks like

section
parameters {A : Type} {R : A  A  Prop}
parameter (irreflR : irreflexive R)
parameter (transR : transitive R)
include transR

(I found it in this GitHub issue here, and the page number referred to doesn't seem to be correct... Maybe there was a prior edition to TPIL?)

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 09:24):

Don't use parameters, use variables

view this post on Zulip Iocta (Mar 22 2020 at 22:12):

that was from https://leanprover.github.io/logic_and_proof/relations_in_lean.html

view this post on Zulip Iocta (Apr 01 2020 at 22:01):

I want to say "a < b and b < a so a < a but that's not allowed so by contradiction a = b" but I'm not sure how to write that in Lean at the sorry.

section
parameters {A : Type} {R : A  A  Prop}
variable (irreflR : irreflexive R)
variable (transR : transitive R)

local infix < := R

def R' (a b : A) : Prop := R a b  a = b
local infix  := R'


theorem reflR' (a : A) : a  a :=
or.inr rfl


include transR

theorem transR'' {a b c : A} (h1 : a  b) (h2 : b  c):
  a  c :=
begin
intros,
cases h1,
cases h2,
left,
apply transR h1 h2,
left,
apply eq.subst h2,
exact h1,
apply eq.substr h1,
exact h2,
end



theorem antisymmR' {a b : A} (h1 : a  b) (h2 : b  a) :
  a = b :=
begin
cases h1,
cases h2,
sorry
end


end

view this post on Zulip Iocta (Apr 01 2020 at 22:09):

Specifically, why doesn't this work

include irreflR
theorem antisymmR' {a b : A} (h1 : a  b) (h2 : b  a) :
  a = b :=
begin
cases h1,
cases h2,
apply irreflR,
end

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 22:21):

Try to apply transitivity first

view this post on Zulip Iocta (Apr 01 2020 at 22:23):

theorem antisymmR' {a b : A} (h1 : a  b) (h2 : b  a) :
  a = b :=
begin
cases h1,
cases h2,
apply transR h1 h2,
end

"invalid apply tactic"

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 22:41):

After cases h2 you have three goals. The tactic state for your first goal is

case or.inl
A : Type,
R : A → A → Prop,
transR : transitive R,
a b : A,
h1 : R a b,
h2 : R b a
⊢ a = b

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 22:41):

apply irreflR doesn't work because irreflR says R x x -> false and your goal is not false.

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 22:42):

apply transR h1 h2 does not work because transR h1 h2 has type R a a which is not a function (so you can't apply it) and is not equal to a = b anyway.

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 22:43):

The way to make progress with this first goal is exfalso. Although I am slightly concerned here because I don't see irreflR in your local context. Did you mean to include it?

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 22:46):

You're playing a bit fast and loose with multiple goals as well. Sometimes this can come back to bite you -- e.g. some tactics randomly apply to all goals or whatever, and things change when you don't mean them to. It's maybe better to write something like this:

theorem antisymmR' {a b : A} (h1 : a  b) (h2 : b  a) :
  a = b :=
begin
  cases h1,
  { cases h2,
    { exfalso,
      sorry},
    { sorry}
  },
  { sorry}
end

view this post on Zulip Iocta (Apr 02 2020 at 00:09):

Ah exfalso is what I needed

view this post on Zulip Iocta (Apr 02 2020 at 00:09):

Is there a shorter way to write apply eq.subst foo?

view this post on Zulip Alex J. Best (Apr 02 2020 at 00:11):

rw foo?

view this post on Zulip Iocta (Apr 02 2020 at 18:40):

What do I do here?

section
parameters {A : Type} {R : A  A  Prop}
parameter (reflR : reflexive R)
parameter (transR : transitive R)

def S (a b : A) : Prop := R a b  R b a

include reflR
include transR

open classical

example : transitive S :=
begin
intros a b c h1 h2,

end

end

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 19:08):

Do you understand the goal you are trying to prove? unfold S if you don't?

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 19:08):

hmm rw [S] seems to work better

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 19:09):

rw [S] at *, maybe even better. But you probably don't need to do this as far as Lean is concerned -- if you can finish the proof from here then try deleting this line and see if the proof still works.

view this post on Zulip Iocta (Apr 02 2020 at 19:44):

Ah ok

example : transitive S :=
begin
intros a b c h1 h2,
cases h1 with rab rba,
cases h2 with rbc rcb,
apply and.intro,
apply transR rab rbc,
apply transR rcb rba,
end

view this post on Zulip Iocta (Apr 02 2020 at 19:44):

am I supposed to put { } somewhere in there for the reasons you mentioned yesterday?

view this post on Zulip Reid Barton (Apr 02 2020 at 19:45):

Looks like around each of the last two lines.

view this post on Zulip Reid Barton (Apr 02 2020 at 19:46):

After apply and.intro you have two goals, so I usually add

  { },
  { }

to my tactic block immediately

view this post on Zulip Reid Barton (Apr 02 2020 at 19:47):

(Actually, I add

  {
},
  {
}

then fix up the } when I finish the subgoals.)

view this post on Zulip Iocta (Apr 02 2020 at 19:48):

alright

view this post on Zulip Iocta (Apr 02 2020 at 19:52):

there's no autoformatter for lean is there?

view this post on Zulip Daniel Keys (Apr 03 2020 at 01:26):

Actually VS Code does do some general formatting. For example, if you type { it inserts {}; if you then put your cursor in between the braces and press Enter, the closing brace is indented to the same level as its opening counterpart. With a little practice you can adjust your style to it (or the other way around).

view this post on Zulip Johan Commelin (Apr 03 2020 at 05:06):

@Iocta If you mean, take a file with "bad" formatting style, and automatically turn it into something that stylistically will make mathlib maintainers happy.... no, I'm not aware of such a tool. And I would be very happy to know about it if you find one!

view this post on Zulip Iocta (Apr 03 2020 at 19:57):

What's this '' notation mean?

def surj_on (f : X  Y) (A : set X) (B : set Y) := B  f '' A

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 19:58):

Iocta said:

What's this '' notation mean?

def surj_on (f : X  Y) (A : set X) (B : set Y) := B  f '' A

It means take the image of f over A

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 19:58):

f '' A := f(A) if you prefer

view this post on Zulip Ryan Lahfa (Apr 03 2020 at 19:58):

You have the same for preimage using a ''⁻¹ if I'm not wrong.

view this post on Zulip Iocta (Apr 03 2020 at 20:01):

Oh I see

view this post on Zulip Kevin Buzzard (Apr 03 2020 at 20:06):

You can always put #print notation '' etc to see definition of notation in lean. You can also hover over it, and even jump to the definition of the underlying term

view this post on Zulip Iocta (Apr 03 2020 at 20:08):

nice! the online books don't have that hover-info feature but copying into my editor isn't hard

view this post on Zulip Iocta (Apr 04 2020 at 07:46):

This feels too manual. Is there a simp_harder or something?

open nat

example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from calc
  (nat.succ m) * (n + k) = m * (n + k) + (n + k)   : by rw [nat.succ_mul]
  ... = (m * n) + (m * k) + (n + k) : by rw [ih]
  ... = (m * n) + ((m * k) + n) + k : by simp
  ... = (m * n) + (n + (m * k)) + k : by simp [add_comm]
  ... = (nat.succ m) * n + (nat.succ m) * k  : by simp [succ_mul] )))

view this post on Zulip Johan Commelin (Apr 04 2020 at 07:48):

Replace all the nat.succ bla with bla + 1

view this post on Zulip Johan Commelin (Apr 04 2020 at 07:48):

After that by ring should do it.

view this post on Zulip Johan Commelin (Apr 04 2020 at 07:49):

But I don't know if you have access to ring...

view this post on Zulip Johan Commelin (Apr 04 2020 at 07:50):

Also... ring will just use mul_add which is the statement that you are trying to prove.

view this post on Zulip Johan Commelin (Apr 04 2020 at 07:50):

So it would be cheating

view this post on Zulip Kenny Lau (Apr 04 2020 at 08:59):

induct on k

view this post on Zulip Kenny Lau (Apr 04 2020 at 09:01):

open nat

example :  m n k : nat, m * (n + k) = m * n + m * k :=
λ m n k, nat.rec_on k rfl $ λ k ih, show m * (n + k) + m = m * n + (m * k + m), by rw [ih, add_assoc]

view this post on Zulip Kenny Lau (Apr 04 2020 at 09:02):

here is the official proof in core:

private meta def sort_add :=
`[simp [nat.add_assoc, nat.add_comm, nat.add_left_comm]]

protected lemma left_distrib :  (n m k : ), n * (m + k) = n * m + n * k
| 0        m k := by simp [nat.zero_mul]
| (succ n) m k :=
  begin simp [succ_mul, left_distrib n m k], sort_add end

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 10:28):

This is a level in the natural number game and it might be interesting to compare with the tactic mode proof I wrote

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 10:29):

@Scott Morrison said to me recently that he thought I should exploit more automation in the natural number game but when I wrote the lean code I didn't understand anything about automation

view this post on Zulip Iocta (Apr 04 2020 at 18:21):

Since this works,

open nat
example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from calc
  (nat.succ m) * (n + k) = (m * n) + ((m * k) + n) + k : by simp [*, succ_mul]
  ... = (m * n) + (n + (m * k)) + k : by simp [*, succ_mul, ih, add_comm]
  ... = (nat.succ m) * n + (nat.succ m) * k  : by simp [succ_mul] )))

how come I can't delete between the first two = in the calc?

open nat
example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from calc
  (nat.succ m) * (n + k) = (m * n) + (n + (m * k)) + k : by simp [*, succ_mul, ih, add_comm]
  ... = (nat.succ m) * n + (nat.succ m) * k  : by simp [succ_mul] )))

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:24):

The answer to "why didn't simp work" is almost always visible from the final goal state in the error message, which is where simp got stuck

 n + (k + (m * n + m * k)) = k + (m * n + (n + m * k))

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:24):

It needs to reassociate some things to finish, so add add_left_comm

view this post on Zulip Iocta (Apr 04 2020 at 18:26):

How come it didn't find the path I used?

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:28):

because it found another path first

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:28):

simp doesn't explore all paths, it just rewrites with random things from its set

view this post on Zulip Iocta (Apr 04 2020 at 18:28):

once it makes any progress on one path, it won't try others?

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:29):

right

view this post on Zulip Iocta (Apr 04 2020 at 18:29):

so is there a simp_harder?

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:29):

so it is important that you give simp a confluent system of rewrites

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:30):

the point is that it's not supposed to be a tree search, it's more like a net where all paths lead to the desired result

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:31):

You can use simp_rw to control the order of rewrites

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:31):

or simp [foo, bar]; simp [baz]

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:32):

but if you put all the rewrites in one bag don't expect to get any particular order

view this post on Zulip Iocta (Apr 04 2020 at 18:35):

is tactic.interactive.solve_by_elimthe tree-search one?

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:35):

That does implicational theorems, not rewrites

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:36):

cc is maybe closer to this

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:36):

But I don't think there is any mechanism that explores all paths in the simp set. The number of paths grows very rapidly

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 18:38):

Here's the nng proof fwiw:

lemma mul_add (t a b : mynat) : t * (a + b) = t * a + t * b :=
begin [nat_num_game]
  induction b with d hd,
  { rewrite [add_zero, mul_zero, add_zero],
  },
  {
    rw add_succ,
    rw mul_succ,
    rw hd,
    rw mul_succ,
    rw add_assoc, -- ;-)
    refl,
  }
end

You don't need the last refl if you remove [nat_num_game]

view this post on Zulip Iocta (Apr 04 2020 at 18:39):

(nat.succ m) * (n + k) = (m * n) + (n + (m * k)) + k : by cc

doesn't work

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:39):

Given h : f 0 = f 1, there are 2^n points in the space of all rewrites of [f 0, ..., f 0]

view this post on Zulip Iocta (Apr 04 2020 at 18:41):

sure. and I guess with practice i'll remember what all the relevant theorems are called so I won't have to think about it

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:41):

Or just be more controlled in your rewrites so it does what you want

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:42):

I don't actually use cc, there is some trick to making it useful

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:42):

you probably have to put all the relevant lemmas in the context

view this post on Zulip Iocta (Apr 04 2020 at 18:44):

with include or something?

view this post on Zulip Mario Carneiro (Apr 04 2020 at 18:44):

with have

view this post on Zulip Iocta (Apr 04 2020 at 19:01):

as in have succ_mul, from succ_mul,?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 19:02):

it's have H, from <proof of H>

view this post on Zulip Mario Carneiro (Apr 04 2020 at 19:02):

or just have := succ_mul

view this post on Zulip Reid Barton (Apr 04 2020 at 19:06):

I don't think cc will instantiate lemmas, does it?

view this post on Zulip Iocta (Apr 04 2020 at 19:11):

open nat
example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from
  begin
  have := nat.succ_mul,
  have := nat.add_left_comm,
  cc,
  end)))

doesn't work

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 19:12):

ie

m n k m : ℕ,
ih : m * (n + k) = m * n + m * k,
this : ∀ (n m : ℕ), succ n * m = n * m + m,
this : ∀ (n m k : ℕ), n + (m + k) = m + (n + k)
⊢ succ m * (n + k) = succ m * n + succ m * k

cc failing

view this post on Zulip Iocta (Apr 04 2020 at 19:13):

^

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 19:13):

(I don't know anything about cc, I was just posting so people could diagnose)

view this post on Zulip Iocta (Apr 04 2020 at 19:16):

for comparison,

open nat
example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from
  begin
  simp [succ_mul, ih, add_left_comm],
  end)))

does work

view this post on Zulip Iocta (Apr 04 2020 at 19:20):

need another theorem in order to use simp only

example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from
  begin
  simp only [nat.succ_mul, ih, nat.add_left_comm, nat.add_assoc],
  end)))

view this post on Zulip Iocta (Apr 04 2020 at 19:22):

but the cc version of that doesn't work either

open nat
example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from
  begin
  have := nat.succ_mul,
  have := nat.add_left_comm,
  have := nat.add_assoc,
  cc,
  end)))
m n k m : ,
ih : m * (n + k) = m * n + m * k,
this :  (n m : ), succ n * m = n * m + m,
this :  (n m k : ), n + (m + k) = m + (n + k),
this :  (n m k : ), n + m + k = n + (m + k)
 succ m * (n + k) = succ m * n + succ m * k

view this post on Zulip Mario Carneiro (Apr 04 2020 at 19:23):

reid says you need to instantiate the lemmas, i.e. have := nat.succ_mul m (n+k) and so on

view this post on Zulip Iocta (Apr 04 2020 at 19:34):

open nat
example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from
  begin
  rw [succ_mul, ih, add_left_comm, add_assoc, succ_mul, succ_mul],
  cc,
  end)))

works, deleting cc, makes it fail with

m n k m : ,
ih : m * (n + k) = m * n + m * k
 n + (m * n + (m * k + k)) = m * n + n + (m * k + k)

view this post on Zulip Iocta (Apr 04 2020 at 19:39):

if I'm interpreting that right it did instantiate the lemmas

view this post on Zulip Reid Barton (Apr 04 2020 at 19:41):

I have no idea what to make of this

view this post on Zulip Reid Barton (Apr 04 2020 at 19:42):

from the proof term, it looks like maybe cc has built-in knowledge that + is commutative and associative

view this post on Zulip Iocta (Apr 04 2020 at 19:47):

using rw [add_left_comm, add_assoc] instead of cc works there, so it does seem that way

view this post on Zulip Iocta (Apr 04 2020 at 19:48):

I wondered if the lemmas in the rw list above were being pulled into cc's scope so I tried deleting the last succ_mul

open nat
example :  m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on m
(show 0 * (n + k) = 0 * n + 0 * k, from by rw [zero_mul, zero_mul, zero_mul])
(assume m,
  (assume ih:  m * (n + k) = m * n + m * k,
  (show (nat.succ m) * (n + k) = (nat.succ m) * n + (nat.succ m) * k,
  from
  begin
  rw [succ_mul, ih, add_left_comm, add_assoc, succ_mul],
  cc,
  end)))

but no

m n k m : ,
ih : m * (n + k) = m * n + m * k
 n + (m * n + (m * k + k)) = m * n + n + succ m * k

view this post on Zulip Iocta (Apr 04 2020 at 21:01):

variable m : nat
#check m * m

when I put the cursor over * why does it tell me about has_mul.mul instead of nat.mul?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 21:02):

because * is notation for has_mul.mul

view this post on Zulip Iocta (Apr 04 2020 at 21:03):

I dunno what answer I was looking for :-P

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 21:03):

:-)

view this post on Zulip Iocta (Apr 04 2020 at 21:11):

looks like Logic and Proof doesn't have "... in Lean" versions for the last few chapters. is that because nobody's gotten around to writing them or because those chapters are too hard to port to Lean or some other reason?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 21:12):

My guess is the former

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 21:12):

Actually, they do look hard

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 21:13):

Chapter 19 alone would be quite an effort for a beginner.

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 21:14):

They could certainly be done in Lean but it would be far more effort than the earlier chapters.

view this post on Zulip Iocta (Apr 04 2020 at 22:19):

import data.real.basic seems to cause compilation and I'm running out of ram. That's not supposed to happen, right?

view this post on Zulip Bryan Gin-ge Chen (Apr 04 2020 at 22:20):

Are you using leanproject to download mathlib olean files? What version of Lean are you using?

view this post on Zulip Iocta (Apr 04 2020 at 22:25):

I was using 3.7.0 with leanproject. I'll try upgrading to 3.7.2.

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:26):

Try restarting Lean. There is no 3.7.0. don't upgrade to 3.7.2

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:26):

Sorry, I take that back. Just use leanproject up

view this post on Zulip Iocta (Apr 04 2020 at 22:40):

deleted everything and rebuilt, working now

view this post on Zulip Bryan Gin-ge Chen (Apr 04 2020 at 22:42):

Lean 3.7.0c and 3.7.1c have some issues that prevent olean files from being loaded properly in Windows. They should all be fixed in 3.7.2c.

view this post on Zulip Iocta (Apr 04 2020 at 22:45):

er not quite working


view this post on Zulip Iocta (Apr 04 2020 at 22:45):

_target/deps/mathlib/src/data/real/basic.lean:240:13: error: unexpected token (lean-checker)

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:46):

Restart Lean? Did you use leanproject up?

view this post on Zulip Iocta (Apr 04 2020 at 22:46):

i switched to 3.7.2 and ran leanproject up and restarted lean

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:46):

leanproject up would have switched for you

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:47):

Exit VS Code and restart. What errors do you get?

view this post on Zulip Iocta (Apr 04 2020 at 22:47):

am i not supposed to have lean installed outside leanproject?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:47):

no

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:48):

You are supposed to let elan do the work of deciding which Lean binary you will be using

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:48):

I don't know why people insist on using non-default set-ups. I don't have any source code for any Lean installed on my computer and I never compile it.

view this post on Zulip Iocta (Apr 04 2020 at 22:49):

ok but i mean leanproject doesn't provide the lean, right?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:49):

elan provides the lean binary

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:49):

elan and leanproject are designed to work together

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:50):

anyone who starts telling VS Code where their Lean installation is, or changing their LEAN_PATH or anything like that is asking for trouble

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:50):

https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian_details.md

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 22:51):

No download of Lean source code required

view this post on Zulip Iocta (Apr 04 2020 at 22:54):

using elan with leanproject works for me

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 23:04):

So the error is gone?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 23:05):

When mathlib upgrades to 3.8.0 or whatever, leanproject up will edit your toml and then when you run your project elan will download it automatically

view this post on Zulip Iocta (Apr 04 2020 at 23:41):

yeah the error is gone

view this post on Zulip Iocta (Apr 05 2020 at 01:13):

I see my editor is running ~/.elan/toolchains/leanprover-community-lean-3.7.2/bin/lean --server -M1024 -T100000 /path/to/project/leanpkg.path I don't see that last argument documented in lean --help, is it doing what it looks like? namely, providing path to a file containing the list of directories where the project source and deps are

view this post on Zulip Iocta (Apr 05 2020 at 01:27):

looks like yes

view this post on Zulip Iocta (Apr 05 2020 at 03:02):

how do I do this?

inductive X : Type
| one : X
| two : X

namespace X

def R : X  X  Prop
| one one := true
| one two := true
| two one := true
| two two := false


example : not (reflexive R) :=
begin
intro reflR,
sorry
end

view this post on Zulip Shing Tak Lam (Apr 05 2020 at 03:09):

You can use reflR to get a term of type R two two, which is false.

example : not (reflexive R) :=
begin
intro reflR,
exact (reflR two)
end

Also see below, if all you have is intro and exact, you don't need tactic mode.

view this post on Zulip Uranus Testing (Apr 05 2020 at 03:12):

Or even shorter

example : not (reflexive R) :=
λ r, r two

view this post on Zulip Iocta (Apr 05 2020 at 03:14):

Thanks

view this post on Zulip Stephanie Zhou (Apr 06 2020 at 18:33):

What's the command for taking the derivative?

view this post on Zulip Kenny Lau (Apr 06 2020 at 18:36):

Lean is not an imperative programming language, and you can find derivatives here

view this post on Zulip Kenny Lau (Apr 06 2020 at 18:36):

import analysis.calculus.deriv

view this post on Zulip Kevin Buzzard (Apr 06 2020 at 18:36):

Is derivative in the kind of state where users can use it? For example, can I prove that the derivative of sin(cos(x)) is what the undergraduates think it is?

view this post on Zulip Patrick Massot (Apr 06 2020 at 18:37):

Kenny, you should try to get into the habit of posting links to the docs rather than source code.

view this post on Zulip Patrick Massot (Apr 06 2020 at 18:39):

as in https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:39):

@Kevin Buzzard Yes, by simp

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:40):

https://leanprover-community.github.io/mathlib_docs/analysis/complex/exponential.html#real.deriv_cos

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:41):

https://leanprover-community.github.io/mathlib_docs/analysis/calculus/deriv.html#deriv.comp

view this post on Zulip Kenny Lau (Apr 06 2020 at 18:41):

@Patrick Massot ah, I didn't know that they exist

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:41):

Hmm, maybe by simp won't work... because of the composition

view this post on Zulip Kenny Lau (Apr 06 2020 at 18:41):

are they automatically generated?

view this post on Zulip Kenny Lau (Apr 06 2020 at 18:42):

wow this is very nice

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:42):

Welcome back!

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:42):

Quick question, what is the state with integration/integrals?

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:42):

WIP

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:43):

We have a PR on FTC

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:43):

There is a very general definition, and a bunch of general API, but it's not complete

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:43):

Is it going to be a general integral and we would have Lebesgue, Riemann, Kurzweil-Henstock?

view this post on Zulip Johan Commelin (Apr 06 2020 at 18:43):

Bochner

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:44):

Every day is a learning experience here

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 18:46):

More-or-less it's Lebesgue.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:47):

Yury G. Kudryashov said:

More-or-less it's Lebesgue.

Yes, I pulled Wikipedia and makes sense to adopt this one.

view this post on Zulip Ryan Lahfa (Apr 06 2020 at 18:47):

(but I think that a Riemann integral tutorial would be nice… :-°)

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 18:47):

It's already formalized for general measure spaces in measure_theory/.

view this post on Zulip Yury G. Kudryashov (Apr 06 2020 at 18:50):

There is a PR that glues it to integrals over intervals but its author @Joe disappeared. I'm going to wait for an update for about a month. If there will be no updates, I'll probably take over this PR.

view this post on Zulip Iocta (Apr 10 2020 at 08:05):

is there a way to know which moves preserve provability?

view this post on Zulip Kevin Buzzard (Apr 10 2020 at 08:06):

That's surely undecidable

view this post on Zulip Iocta (Apr 10 2020 at 08:07):

we seem to have decided for some of them though

view this post on Zulip Kenny Lau (Apr 10 2020 at 08:07):

what is a move?

view this post on Zulip Iocta (Apr 10 2020 at 08:08):

adding anything to a proof

view this post on Zulip Mario Carneiro (Apr 10 2020 at 08:09):

I think that for the most part you can determine for each "move" whether it necessarily preserves provability or not

view this post on Zulip Mario Carneiro (Apr 10 2020 at 08:10):

Anything reversible preserves provability. intro, revert, have, split, rw, simp

view this post on Zulip Mario Carneiro (Apr 10 2020 at 08:11):

apply is the main source of potentially lossy moves, but it depends on the theorem. clear is also not reversible

view this post on Zulip Mario Carneiro (Apr 10 2020 at 08:13):

cases preserves provability, but only if you case on a variable. If you case on an expression you might lose information about what term it was unless you use the form cases h : e

view this post on Zulip Mario Carneiro (Apr 10 2020 at 08:14):

induction is also not reversible, since if you do the induction wrong you can get unprovable goals

view this post on Zulip Iocta (Apr 10 2020 at 08:21):

I see

view this post on Zulip Iocta (Apr 10 2020 at 08:45):

are "target" and "goal" synonymous?

view this post on Zulip Mario Carneiro (Apr 10 2020 at 09:02):

Depends on who you ask. Lean usually uses the term to mean a target expression together with its list of hypotheses

view this post on Zulip Bhavik Mehta (Apr 21 2020 at 10:01):

Iocta said:

looks like Logic and Proof doesn't have "... in Lean" versions for the last few chapters. is that because nobody's gotten around to writing them or because those chapters are too hard to port to Lean or some other reason?

For whatever it's worth, I think almost all of the combinatorics section has proofs in mathlib, and I've done the ones which don't

view this post on Zulip Pit Sinning (Apr 21 2020 at 10:13):

Iocta said:

looks like Logic and Proof doesn't have "... in Lean" versions for the last few chapters. is that because nobody's gotten around to writing them or because those chapters are too hard to port to Lean or some other reason?

If you look at the Git of the book, it certainly appears that those chapters were planned for, but the files were last edited 3 years ago so I wouldn't hold my breath.

view this post on Zulip Patrick Massot (Apr 21 2020 at 10:14):

Chapter 21 is clearly in mathlib

view this post on Zulip Patrick Massot (Apr 21 2020 at 10:14):

and 22 also

view this post on Zulip Jeremy Avigad (Apr 21 2020 at 14:26):

Rob, Floris, and I perpetually have back-burner plans to expand Logic and Proof, but other projects always seem to take precedence. I'll be using it again in the fall, and I am hoping to add more then.

view this post on Zulip Iocta (May 08 2020 at 20:37):

What's next after the books?

view this post on Zulip Patrick Massot (May 08 2020 at 20:39):

Did you do the new tutorials and the beginning of the new book?

view this post on Zulip Iocta (May 08 2020 at 20:46):

Link?

view this post on Zulip Patrick Massot (May 08 2020 at 20:49):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Tutorials.20update/near/196123657 and https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/new.20Lean.20.2F.20mathlib.20tutorial

view this post on Zulip Iocta (May 08 2020 at 21:12):

Hadn't seen those, thanks

view this post on Zulip Iocta (May 08 2020 at 21:13):

those filenames haha :-)

view this post on Zulip Iocta (May 09 2020 at 22:21):

I'm curious, Do you find it works to learn a subject by formalizing it, or do you have to understand it really well already before formalizing it?

view this post on Zulip Bryan Gin-ge Chen (May 09 2020 at 22:22):

Those aren't mutually exclusive.

view this post on Zulip Iocta (May 09 2020 at 22:23):

Do you find it works to learn a subject for the first time by formalizing it, or do you have to understand it really well already before formalizing it?

view this post on Zulip Kevin Buzzard (May 09 2020 at 22:42):

I have understood everything I've formalised really quite well, although I will be the first to admit that formalising perfectoid spaces taught me that the theory of complete topological rings was more subtle than I had realised.

Conversely @Athina told me when she was watching me teach mathematics undergraduates that she could see evidence that learning new mathematics at the same time as learning Lean was hard

view this post on Zulip Kevin Buzzard (May 09 2020 at 22:42):

I realise that this is not quite what you asked

view this post on Zulip Mario Carneiro (May 10 2020 at 02:23):

I think you should be somewhat familiar, at the level where you just had a midterm on the topic. You don't need to be an expert, but you should have the general feel for the terrain. Reading the wikipedia page is usually sufficient, if you are the type that can absorb what is written there

view this post on Zulip Carlo Cabrera (May 10 2020 at 21:56):

How do I tell Lean I've derived a contradiction? Here is a snippet from Lean's tactic state... Tactic State Snippet

view this post on Zulip Kenny Lau (May 10 2020 at 21:57):

example (R : Prop) (H : R  ¬R) : false := by cc

view this post on Zulip Mario Carneiro (May 10 2020 at 21:57):

by contradiction is the correct answer

view this post on Zulip Mario Carneiro (May 10 2020 at 21:58):

or by exact notr r

view this post on Zulip Kenny Lau (May 10 2020 at 21:58):

oh I didn't notice that r and notr were there lol

view this post on Zulip Mario Carneiro (May 10 2020 at 21:59):

I suspect carlo put them together to make it more obvious for lean

view this post on Zulip Carlo Cabrera (May 10 2020 at 22:00):

Excellent, thanks, Kenny and Mario. I did try to put them together to see if that got me somewhere, but it seems it did not by itself.

view this post on Zulip Kenny Lau (May 10 2020 at 22:00):

also, #mwe

view this post on Zulip Mario Carneiro (May 10 2020 at 22:00):

but the right way to put them together is to apply the \not R proof to the R proof, because \not R is short for R -> false

view this post on Zulip Mario Carneiro (May 10 2020 at 22:00):

so notr r : false

view this post on Zulip Mario Carneiro (May 10 2020 at 22:01):

using apply you can apply notr and the goal will change to R

view this post on Zulip Carlo Cabrera (May 10 2020 at 22:02):

To be fair I noticed that "cc" actually proved what I needed to without additional work, but I was trying to get a feel for using tactics by doing it the long way

view this post on Zulip Kenny Lau (May 10 2020 at 22:03):

I notice that notr is basically h2 notq

view this post on Zulip Kenny Lau (May 10 2020 at 22:03):

so how about by exact h2 notq r

view this post on Zulip Mario Carneiro (May 10 2020 at 22:04):

kenny wants a #mwe so he can golf your theorem to oblivion

view this post on Zulip Carlo Cabrera (May 10 2020 at 22:05):

He probably already has, this is from Imperial's exercise sheets. I guess you can't make it shorter than "cc"

view this post on Zulip Kenny Lau (May 10 2020 at 22:11):

yeah no I'm not going through 1000 exercise sheets to find your theorem

view this post on Zulip Carlo Cabrera (May 10 2020 at 23:54):

I guess I'm not understanding how by contradiction works yet. Here's one case where I expect it to work, but doesn't:

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
begin
    have pnotp : P  ¬P,
        intro h,
        by exact h₂ (h₁ h),
end

In a simpler example, I can show that (P → ¬P) → ¬P, but for some reason the approach doesn't work in the example I gave above. (i.e. one where instead of two hypotheses, there is a single one that says (P → ¬P))

view this post on Zulip Dan Stanescu (May 11 2020 at 00:04):

Carlo Cabrera said:

I guess I'm not understanding how by contradiction works yet. Here's one case where I expect it to work, but doesn't:

You mean something like this?

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
begin
    by_contradiction H,
    exact h₂ (h₁ H) H,
end

view this post on Zulip Jalex Stark (May 11 2020 at 00:04):

why are you using by if you're already in tactic mode?

view this post on Zulip Jalex Stark (May 11 2020 at 00:06):

I think @Carlo Cabrera is talking about the contradiction tactic, which looks for P and ¬ P in the hypotheses

view this post on Zulip Jalex Stark (May 11 2020 at 00:07):

and @Dan Stanescu is talking about the by_contradiction tactic which puts the negation of the goal into the hypotheses and makes false the new goal

view this post on Zulip Dan Stanescu (May 11 2020 at 00:10):

@Jalex Stark I was wondering. contradiction needs something very obvious, like both P and not P, but @Carlo Cabrera didn't have both in his context.

view this post on Zulip Dan Stanescu (May 11 2020 at 00:10):

Not sure he had any.

view this post on Zulip Jalex Stark (May 11 2020 at 00:12):

@Carlo Cabrera is this the proof you want?

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
begin
intro hp,
have := (h₂  h₁) hp,
contradiction,
end

view this post on Zulip Iocta (May 11 2020 at 05:57):

theorem mul_zero (a : R) : a * 0 = 0 :=
begin
  have h : a * 0 + a * 0 = a * 0 + 0,
  from by rw [mul_add, add_zero, add_zero],
  rw add_left_cancel h
end

is from doing anything?

view this post on Zulip Kenny Lau (May 11 2020 at 06:36):

https://github.com/leanprover-community/lean/blob/master/library/init/meta/interactive.lean#L297

/--
A synonym for `exact` that allows writing `have/suffices/show ..., from ...` in tactic mode.
-/
meta def «from» := exact

view this post on Zulip Kenny Lau (May 11 2020 at 06:37):

it's to make it look more like the term mode version have h : _, from _

view this post on Zulip Kenny Lau (May 11 2020 at 06:38):

but in this case it is simply unnecessary

view this post on Zulip Iocta (May 11 2020 at 07:22):

ok

view this post on Zulip Patrick Massot (May 11 2020 at 07:25):

Either from or by is unnecessary

view this post on Zulip Kenny Lau (May 11 2020 at 07:27):

that's right, because from is unnecessary

view this post on Zulip Patrick Massot (May 11 2020 at 07:31):

Removing from and keeping by also works

view this post on Zulip Carlo Cabrera (May 11 2020 at 08:07):

Jalex Stark said:

Carlo Cabrera is this the proof you want?

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
begin
intro hp,
have := (h₂  h₁) hp,
contradiction,
end

@Jalex Stark Yes! That was what I had in mind. I don't know why I was using by, thanks for pointing that out. Would you say that this is the simplest approach to the example?

Thanks for your comments too, @Dan Stanescu. I learned something from you both here.

view this post on Zulip Johan Commelin (May 11 2020 at 08:11):

by { exfalso, exact (h₂ ∘ h₁) id }?

view this post on Zulip Johan Commelin (May 11 2020 at 08:12):

Meh, me confused

view this post on Zulip Patrick Massot (May 11 2020 at 08:13):

The simplest approach is

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
λ hp, h₂ (h₁ hp) hp

or

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
by tauto

depending on taste

view this post on Zulip Carlo Cabrera (May 11 2020 at 08:21):

Excellent, thank you.

view this post on Zulip Kenny Lau (May 11 2020 at 08:21):

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
assume hp : P,
  have hq : Q, from h₁ hp,
  have hnp : ¬P, from h₂ hq,
  show false, from hnp hp

view this post on Zulip Kevin Buzzard (May 11 2020 at 08:21):

Aargh

view this post on Zulip Kenny Lau (May 11 2020 at 08:21):

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
assume Aargh : P,
  have hq : Q, from h₁ Aargh,
  have hnp : ¬P, from h₂ hq,
  show false, from hnp Aargh

view this post on Zulip Kevin Buzzard (May 11 2020 at 08:21):

The horribleist approach to complement the two simple ones

view this post on Zulip Kevin Buzzard (May 11 2020 at 08:27):

I can't actually see what the question is because I'm on mobile and one of the hypotheses is h-box : P box Q. From the code it looks like the box should be an implies sign, but I can see an implies sign in h2 so I'm confused

view this post on Zulip Kenny Lau (May 11 2020 at 08:31):

example (P Q : Prop)
    (h₁ : P  Q)
    (h₂ : Q  ¬P) :
    ¬P :=
implies.trans (and_self P).mpr (and.rec (implies.trans h₁ h₂))

view this post on Zulip Iocta (May 11 2020 at 19:25):

theorem zero_mul (a : R) : 0 * a  = 0 :=
begin
rw  add_left_neg a,
rw add_mul,
rw add_comm,
rw add_left_neg a,
rw add_comm (a * a) (-a * a),
have h: (-a * a) + (a * a) = -(a * a) + (a * a),
from sorry,
rw h,
rw add_left_neg (a * a),
end

How can I fill sorry, or is there a better way to solve this problem?

view this post on Zulip Jalex Stark (May 11 2020 at 19:27):

please give a #mwe
Is R a commutative ring?

view this post on Zulip Jalex Stark (May 11 2020 at 19:27):

are you avoiding use of the ring tactic?

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:27):

Are you avoiding use the of the zero_mul lemma? ;-)

view this post on Zulip Jalex Stark (May 11 2020 at 19:29):

If you want to learn the proof of zero_mul for natural numbers, play the natural number game

view this post on Zulip Jalex Stark (May 11 2020 at 19:29):

If you want to learn it for general commutative rings then you should be thinking about what the axioms are and what order you want to develop the theory in

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:29):

but currently your question is unanswerable because you didn't supply the typeclass of R in a mwe

view this post on Zulip Iocta (May 11 2020 at 19:30):

variables {R : Type*} [ring R]

theorem zero_mul (a : R) : 0 * a  = 0 :=
begin
rw  add_left_neg a,
rw add_mul,
rw add_comm,
rw add_left_neg a,
rw add_comm (a * a) (-a * a),
have h: (-a * a) + (a * a) = -(a * a) + (a * a),
from sorry,
rw h,
rw add_left_neg (a * a),
end

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:31):

Kevin Buzzard said:

I can't actually see what the question is because I'm on mobile and one of the hypotheses is h-box : P box Q. From the code it looks like the box should be an implies sign, but I can see an implies sign in h2 so I'm confused

Oh -- back to this -- on mobile the implication for h1 didn't render but the one for h2 did?

view this post on Zulip Kenny Lau (May 11 2020 at 19:31):

how about one topic for one question

view this post on Zulip Reid Barton (May 11 2020 at 19:32):

if you're talking about Kenny's most recent message, I can assure you they are the same character

view this post on Zulip Kevin Buzzard (May 11 2020 at 19:32):

@Iocta can you start a new topic instead of just posting on some other one?


Last updated: May 06 2021 at 21:09 UTC