more basics

Stream: new members

[Iocta]

open classical

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

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

[Iocta]

@Bryan Gin-ge Chen continuing

[Bryan Gin-ge Chen]

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

[Iocta]

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, _) _)

[Iocta]

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

[Iocta]

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

[Bryan Gin-ge Chen]

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, _))

[Iocta]

Got it, thanks.

[Iocta]

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, _),
_)
)
_

[Kenny Lau]

well what is the type of p?

[Kenny Lau]

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

[Iocta]

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

[Mario Carneiro]

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 : α

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

ah putting the cursor over z does display its type

[Iocta]

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

[Iocta]

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

[Mario Carneiro]

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

[Mario Carneiro]

there is a setting for hover delay in preferences

[Iocta]

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

[Iocta]

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 _)))

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Iocta]

Ok got it.

[Iocta]

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

[Kevin Buzzard]

I am pretty sure that such a thing is undecidable!

[Iocta]

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, _))

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Iocta]

 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)

[Johan Commelin]

How would you prove it in maths?

[Kevin Buzzard]

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

[Kevin Buzzard]

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"?

[Iocta]

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

[Iocta]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Iocta]

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

[Kevin Buzzard]

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 :-)

[Iocta]

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
)

[Iocta]

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

[Yury G. Kudryashov]

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

[Daniel Keys]

@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

[Dan Stanescu]

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.

[Patrick Massot]

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

Is this what you want?

[Dan Stanescu]

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

[Chris Hughes]

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

[Patrick Massot]

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

[Dan Stanescu]

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

[Patrick Massot]

Yes.

[Patrick Massot]

Are you using VScode?

[Dan Stanescu]

Yes.

[Patrick Massot]

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

[Patrick Massot]

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.

[Dan Stanescu]

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.

[Dan Stanescu]

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?

[Dan Stanescu]

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

[Chris Hughes]

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.

[Dan Stanescu]

Great! Thanks again!

[Patrick Massot]

push_neg should do that for you as well.

[Daniel Keys]

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:ℤ))

[Daniel Keys]

Or is this a bug?

[Bryan Gin-ge Chen]

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?

[Bryan Gin-ge Chen]

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

[Daniel Keys]

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

[Bryan Gin-ge Chen]

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.

[Daniel Keys]

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

[Bryan Gin-ge Chen]

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

[Daniel Keys]

OK, thanks! That works!

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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.

[Daniel Keys]

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.

[Daniel Keys]

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

[Bryan Gin-ge Chen]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Daniel Keys]

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.

[Daniel Keys]

Thank you both!

[Bryan Gin-ge Chen]

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.

[Daniel Keys]

Yes, indeed - this makes it clear.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Iocta]

Thanks.

[Iocta]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Iocta]

aha

[Reid Barton]

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.

[Reid Barton]

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

[Daniel Keys]

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.

[Alex J. Best]

pow_two_nonneg in algebra/group_power.lean

[Daniel Keys]

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

[Alex J. Best]

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.

[Kevin Buzzard]

You could probably find this with library_search

[Daniel Keys]

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?

[Alex J. Best]

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

[Alex J. Best]

and library_search tells you exactly the same lemma name

[Daniel Keys]

I see! Great, thanks!

[Daniel Keys]

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

[Iocta]

-- 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?

[Johan Commelin]

Use squeeze_simp?

[Johan Commelin]

It will turn it into code for you.

[Iocta]

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?

[Reid Barton]

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

[Reid Barton]

But you could start with rw h.1.2

[Reid Barton]

Wait no

[Kevin Buzzard]

cases h

[Reid Barton]

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

[Kevin Buzzard]

just use cases and split

[Reid Barton]

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

[Kevin Buzzard]

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

[Iocta]

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?

[Kevin Buzzard]

split stops you having to do repeat

[Kevin Buzzard]

it splits an and goal into two goals

[Iocta]

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

[Iocta]

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

[Kenny Lau]

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

[Iocta]

neat

[Iocta]

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

[Iocta]

 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)

[Kevin Buzzard]

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.

[Iocta]

thanks

[Iocta]

 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.

[Iocta]

(or is that not idiomatic?)

[Mario Carneiro]

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

[Iocta]

ok

[Reid Barton]

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

[Iocta]

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

[Iocta]

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}

[Johan Commelin]

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

[Johan Commelin]

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

[Iocta]

Alright

[Johan Commelin]

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

[Mario Carneiro]

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}

[Mario Carneiro]

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

[Iocta]

Ah cool

[Iocta]

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)

[Reid Barton]

The easy way is by rw ih

[Reid Barton]

there's also a harder way

[Iocta]

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

[Reid Barton]

Using congr_arg somehow

[Reid Barton]

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

[Reid Barton]

anyways, this is where rw starts to become indispensable

[Iocta]

ok that works

[Mario Carneiro]

You can probably use \t for this

[Mario Carneiro]

ih ▸ rfl works

[Mario Carneiro]

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)

[Iocta]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

ah ok

[Iocta]

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

[Iocta]

How to fix this?

[Iocta]

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

[Mario Carneiro]

use rec_on not cases_on

[Iocta]

oh. that was easy :-)

[Iocta]

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?

[Iocta]

(really just asking what the convention is)

[Iocta]

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

[Reid Barton]

Yes, this seems to be the normal convention

[Iocta]

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 α

[Iocta]

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

[Reid Barton]

I think your code is just wrong

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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 ))

[Iocta]

Oh, I see

[Iocta]

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"?

[Iocta]

example : length  nil  = 0 :=
sorry

 06.2.lean    55  19 error           don't know how to synthesize placeholder
 context:
 ⊢ Type ? (lean-checker)

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Reid Barton]

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

[Iocta]

aha, that works

[Patrick Massot]

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

[Iocta]

yeah, got it

[Iocta]

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)

[Iocta]

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

[Iocta]

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

[Reid Barton]

Somewhere you must have Type with no u

[Iocta]

yeah I do

[Iocta]

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)

[Kevin Buzzard]

You can't use eval in the definition of eval

[Iocta]

Then how do I recurse?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

After the definition of expr, try #print prefix expr

[Kevin Buzzard]

wait, better is #print prefix hidden.expr

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Iocta]

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 ?)

[Chris Hughes]

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

[Kevin Buzzard]

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?

[Chris Hughes]

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

[Iocta]

Aha, that helps

[Kevin Buzzard]

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

[Chris Hughes]

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)

[Kevin Buzzard]

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

[Kevin Buzzard]

which is an input function

[Iocta]

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)

[Iocta]

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

[Kevin Buzzard]

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

[Iocta]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Iocta]

I do see it now :-)

[Kevin Buzzard]

:-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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 :-)

[Iocta]

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

[Iocta]

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)

[Kevin Buzzard]

What is the type of const?

[Iocta]

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

[Kevin Buzzard]

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

[Iocta]

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

[Kevin Buzzard]

const alpha 0

[Kevin Buzzard]

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

[Kevin Buzzard]

Why not just remove the alpha?

[Iocta]

yeah that works

[Iocta]

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

[Kevin Buzzard]

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.

[Chris Hughes]

You have to write const α 0

[Chris Hughes]

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

[Kevin Buzzard]

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

[Iocta]

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

[Iocta]

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

[Patrick Massot]

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

[Patrick Massot]

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⟩

[Patrick Massot]

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

[Patrick Massot]

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

[Iocta]

that's pretty slick

[Iocta]

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

[Iocta]

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 _?

[Iocta]

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

[Bryan Gin-ge Chen]

#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.)

[Bryan Gin-ge Chen]

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}

[Iocta]

I see

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

mhmm

[Iocta]

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

[Iocta]

import logic.basic seems to open it automatically?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Iocta]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Iocta]

I see

[Iocta]

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

[Iocta]

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

[Kenny Lau]

thanks for creating a copy-paste-able example.

[Kenny Lau]

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

[Kevin Buzzard]

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

[Iocta]

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.

[Iocta]

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?

[Shing Tak Lam]

@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?)

[Kevin Buzzard]

Don't use parameters, use variables

[Iocta]

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

[Iocta]

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

[Iocta]

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

[Yury G. Kudryashov]

Try to apply transitivity first

[Iocta]

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"

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Iocta]

Ah exfalso is what I needed

[Iocta]

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

[Alex J. Best]

rw foo?

[Iocta]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

hmm rw [S] seems to work better

[Kevin Buzzard]

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.

[Iocta]

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

[Iocta]

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

[Reid Barton]

Looks like around each of the last two lines.

[Reid Barton]

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

  { },
  { }

to my tactic block immediately

[Reid Barton]

(Actually, I add

  {
},
  {
}

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

[Iocta]

alright

[Iocta]

there's no autoformatter for lean is there?

[Daniel Keys]

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

[Johan Commelin]

@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!

[Iocta]

What's this '' notation mean?

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

[Ryan Lahfa]

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

[Ryan Lahfa]

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

[Ryan Lahfa]

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

[Iocta]

Oh I see

[Kevin Buzzard]

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

[Iocta]

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

[Iocta]

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

[Johan Commelin]

Replace all the nat.succ bla with bla + 1

[Johan Commelin]

After that by ring should do it.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

So it would be cheating

[Kenny Lau]

induct on k

[Kenny Lau]

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]

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

@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

[Iocta]

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

[Mario Carneiro]

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))

[Mario Carneiro]

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

[Iocta]

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

[Mario Carneiro]

because it found another path first

[Mario Carneiro]

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

[Iocta]

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

[Mario Carneiro]

right

[Iocta]

so is there a simp_harder?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

You can use simp_rw to control the order of rewrites

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

is tactic.interactive.solve_by_elimthe tree-search one?

[Mario Carneiro]

That does implicational theorems, not rewrites

[Mario Carneiro]

cc is maybe closer to this

[Mario Carneiro]

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

[Kevin Buzzard]

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]

[Iocta]

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

doesn't work

[Mario Carneiro]

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

[Iocta]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

with include or something?

[Mario Carneiro]

with have

[Iocta]

as in have succ_mul, from succ_mul,?

[Kevin Buzzard]

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

[Mario Carneiro]

or just have := succ_mul

[Reid Barton]

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

[Iocta]

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

[Kevin Buzzard]

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

[Iocta]

^

[Kevin Buzzard]

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

[Iocta]

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

[Iocta]

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)))

[Iocta]

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

[Mario Carneiro]

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

[Iocta]

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)

[Iocta]

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

[Reid Barton]

I have no idea what to make of this

[Reid Barton]

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

[Iocta]

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

[Iocta]

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

[Iocta]

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?

[Kevin Buzzard]

because * is notation for has_mul.mul

[Iocta]

I dunno what answer I was looking for :-P

[Kevin Buzzard]

:-)

[Iocta]

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?

[Kevin Buzzard]

My guess is the former

[Kevin Buzzard]

Actually, they do look hard

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Iocta]

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

[Bryan Gin-ge Chen]

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

[Iocta]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Sorry, I take that back. Just use leanproject up

[Iocta]

deleted everything and rebuilt, working now

[Bryan Gin-ge Chen]

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.

[Iocta]

er not quite working

[Iocta]

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

[Kevin Buzzard]

Restart Lean? Did you use leanproject up?

[Iocta]

i switched to 3.7.2 and ran leanproject up and restarted lean

[Kevin Buzzard]

leanproject up would have switched for you

[Kevin Buzzard]

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

[Iocta]

am i not supposed to have lean installed outside leanproject?

[Kevin Buzzard]

no

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Iocta]

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

[Kevin Buzzard]

elan provides the lean binary

[Kevin Buzzard]

elan and leanproject are designed to work together

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

No download of Lean source code required

[Iocta]

using elan with leanproject works for me

[Kevin Buzzard]

So the error is gone?

[Kevin Buzzard]

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

[Iocta]

yeah the error is gone

[Iocta]

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

[Iocta]

looks like yes

[Iocta]

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

[Shing Tak Lam]

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.

[Uranus Testing]

Or even shorter

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

[Iocta]

Thanks

[Stephanie Zhou]

What's the command for taking the derivative?

[Kenny Lau]

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

[Kenny Lau]

import analysis.calculus.deriv

[Kevin Buzzard]

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?

[Patrick Massot]

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

[Patrick Massot]

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

[Johan Commelin]

@Kevin Buzzard Yes, by simp

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

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

[Kenny Lau]

are they automatically generated?

[Kenny Lau]

wow this is very nice

[Johan Commelin]

Welcome back!

[Ryan Lahfa]

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

[Johan Commelin]

WIP

[Johan Commelin]

We have a PR on FTC

[Johan Commelin]

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

[Ryan Lahfa]

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

[Johan Commelin]

Bochner

[Ryan Lahfa]

Every day is a learning experience here

[Yury G. Kudryashov]

More-or-less it's Lebesgue.

[Ryan Lahfa]

Yury G. Kudryashov said:

More-or-less it's Lebesgue.

Yes, I pulled Wikipedia and makes sense to adopt this one.

[Ryan Lahfa]

(but I think that a Riemann integral tutorial would be nice… :-°)

[Yury G. Kudryashov]

It's already formalized for general measure spaces in measure_theory/.

[Yury G. Kudryashov]

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.

[Iocta]

is there a way to know which moves preserve provability?

[Kevin Buzzard]

That's surely undecidable

[Iocta]

we seem to have decided for some of them though

[Kenny Lau]

what is a move?

[Iocta]

adding anything to a proof

[Mario Carneiro]

I think that for the most part you can determine for each "move" whether it necessarily preserves provability or not

[Mario Carneiro]

Anything reversible preserves provability. intro, revert, have, split, rw, simp

[Mario Carneiro]

apply is the main source of potentially lossy moves, but it depends on the theorem. clear is also not reversible

[Mario Carneiro]

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

[Mario Carneiro]

induction is also not reversible, since if you do the induction wrong you can get unprovable goals

[Iocta]

I see

[Iocta]

are "target" and "goal" synonymous?

[Mario Carneiro]

Depends on who you ask. Lean usually uses the term to mean a target expression together with its list of hypotheses

[Bhavik Mehta]

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

[Pit Sinning]

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.

[Patrick Massot]

Chapter 21 is clearly in mathlib

[Patrick Massot]

and 22 also

[Jeremy Avigad]

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.

[Iocta]

What's next after the books?

[Patrick Massot]

Did you do the new tutorials and the beginning of the new book?

[Iocta]

Link?

[Patrick Massot]

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

[Iocta]

Hadn't seen those, thanks

[Iocta]

those filenames haha :-)

[Iocta]

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?

[Bryan Gin-ge Chen]

Those aren't mutually exclusive.

[Iocta]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

I realise that this is not quite what you asked

[Mario Carneiro]

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

[Carlo Cabrera]

How do I tell Lean I've derived a contradiction? Here is a snippet from Lean's tactic state... Tactic State Snippet

[Kenny Lau]

example (R : Prop) (H : R ∧ ¬R) : false := by cc

[Mario Carneiro]

by contradiction is the correct answer

[Mario Carneiro]

or by exact notr r

[Kenny Lau]

oh I didn't notice that r and notr were there lol

[Mario Carneiro]

I suspect carlo put them together to make it more obvious for lean

[Carlo Cabrera]

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.

[Kenny Lau]

also, #mwe

[Mario Carneiro]

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

[Mario Carneiro]

so notr r : false

[Mario Carneiro]

using apply you can apply notr and the goal will change to R

[Carlo Cabrera]

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

[Kenny Lau]

I notice that notr is basically h2 notq

[Kenny Lau]

so how about by exact h2 notq r

[Mario Carneiro]

kenny wants a #mwe so he can golf your theorem to oblivion

[Carlo Cabrera]

He probably already has, this is from Imperial's exercise sheets. I guess you can't make it shorter than "cc"

[Kenny Lau]

yeah no I'm not going through 1000 exercise sheets to find your theorem

[Carlo Cabrera]

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))

[Dan Stanescu]

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

[Jalex Stark]

why are you using by if you're already in tactic mode?

[Jalex Stark]

I think @Carlo Cabrera is talking about the contradiction tactic, which looks for P and ¬ P in the hypotheses

[Jalex Stark]

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

[Dan Stanescu]

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

[Dan Stanescu]

Not sure he had any.

[Jalex Stark]

@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

[Iocta]

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?

[Kenny Lau]

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

[Kenny Lau]

it's to make it look more like the term mode version have h : _, from _

[Kenny Lau]

but in this case it is simply unnecessary

[Iocta]

ok

[Patrick Massot]

Either from or by is unnecessary

[Kenny Lau]

that's right, because from is unnecessary

[Patrick Massot]

Removing from and keeping by also works

[Carlo Cabrera]

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.

[Johan Commelin]

by { exfalso, exact (h₂ ∘ h₁) id }?

[Johan Commelin]

Meh, me confused

[Patrick Massot]

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

[Carlo Cabrera]

Excellent, thank you.

[Kenny Lau]

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

[Kevin Buzzard]

Aargh

[Kenny Lau]

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

[Kevin Buzzard]

The horribleist approach to complement the two simple ones

[Kevin Buzzard]

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

[Kenny Lau]

example (P Q : Prop)
    (h₁ : P → Q)
    (h₂ : Q → ¬P) :
    ¬P :=
implies.trans (and_self P).mpr (and.rec (implies.trans h₁ h₂))

[Iocta]

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?

[Jalex Stark]

please give a #mwe
Is R a commutative ring?

[Jalex Stark]

are you avoiding use of the ring tactic?

[Kevin Buzzard]

Are you avoiding use the of the zero_mul lemma? ;-)

[Jalex Stark]

If you want to learn the proof of zero_mul for natural numbers, play the natural number game

[Jalex Stark]

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

[Kevin Buzzard]

but currently your question is unanswerable because you didn't supply the typeclass of R in a mwe

[Iocta]

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

[Kevin Buzzard]

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?

[Kenny Lau]

how about one topic for one question

[Reid Barton]

if you're talking about Kenny's most recent message, I can assure you they are the same character

[Kevin Buzzard]

@Iocta can you start a new topic instead of just posting on some other one?