Basic Proving Questions

Stream: new members

[ccn]

My tactic state is this:

X : Type,
A B : set X,
x : X,
ha : x ∈ A,
heq : ∀ (x : X), x ∈ B ↔ x ∈ A ∪ B,
heqa : x ∈ B ↔ x ∈ A ∪ B,
heqb : x ∈ A ∪ B → x ∈ B
⊢ x ∈ B

The union is defined as x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B, so it seems like I need a proof of x ∈ A ∨ x ∈ B from ha : x ∈ A, how could I do it?

[Reid Barton]

or.inl ha

[Reid Barton]

I am not sure offhand whether the other proposition is an explicit argument to or.inl or not

[ccn]

Reid Barton said:

or.inl ha

Hey I think you're right, thank you!

Here it is:

 inductive or (a b : Prop) :
Prop

    inl : ∀ (a b : Prop), a → a ∨ b
    inr : ∀ (a b : Prop), b → a ∨ b

I have an issue though, when I write have ho := or.inl ha (x ∈ B), I get this as my tactic state:

function expected at
  or.inl ha
term has type
  x ∈ A ∨ ?m_1
state:
X : Type,
A B : set X,
x : X,
ha : x ∈ A,
heq : ∀ (x : X), x ∈ B ↔ x ∈ A ∪ B,
heqa : x ∈ B ↔ x ∈ A ∪ B,
heqb : x ∈ A ∪ B → x ∈ B
⊢ x ∈ B

[Kyle Miller]

That's suggesting that or.inl is taking only one argument, and you want or.inl ha. I expect that rw heqa, exact or.inl ha, ought to finish the proof.

[ccn]

Hmm, you're right, that closes the goal. I don't think I fully understand or.inl ha doesn't it take two parameters namely a and b ? inl : ∀ (a b : Prop), a → a ∨ b

[Alex J. Best]

I guess that's a bug in our documentation generator.
If you do this in Lean

#check @or.inl

we can see that Lean thinks the type is

∀ {a b : Prop}, a → a ∨ b

which has implicit a and b arguments

[Kyle Miller]

#print or at least gets it all right:

inductive or : Prop → Prop → Prop
constructors:
or.inl : ∀ {a b : Prop}, a → a ∨ b
or.inr : ∀ {a b : Prop}, b → a ∨ b

[Alex J. Best]

With doc-gen#151 this should be fixed after the next time docs build

[ccn]

Last night Kyle showed me that

exact or.inl ha

finishes the following proof

X : Type,
A B : set X,
x : X,
ha : x ∈ A,
heq : ∀ (x : X), x ∈ B ↔ x ∈ A ∪ B,
heqa : x ∈ B ↔ x ∈ A ∪ B,
heqb : x ∈ A ∪ B → x ∈ B
⊢ x ∈ A ∪ B

I'm having trouble seeing why this is true, or.inl ha would just be ∀ {b : Prop}, x ∈ A -> x ∈ A V b I think I'm interpreting the implicit arguments wrong...

[Kyle Miller]

@ccn The secret is in the definition of union docs#set.union

It's definitionally "x in A or x in B"

[Kyle Miller]

Oh, also b ends up being "x in B", which Lean infers through its elaboration process.

[ccn]

So it's able to guess it because it knows that that's what my goal is?

[ccn]

Is there a way to specifically create the term "x in A or x in B" without letting it infer?

[Floris van Doorn]

There are a couple of ways:

import data.set.basic

open set

example {α : Type*} {s t : set α} {x : α} : x ∈ s ∪ t :=
begin
  -- -- uncomment ONE:
  -- simp
  -- dsimp only [mem_union_eq]
  -- change x ∈ s ∨ x ∈ t
end

[Kyle Miller]

ccn said:

Is there a way to specifically create the term "x in A or x in B" without letting it infer?

You can also use @or.inl to turn all the implicit arguments into explicit arguments. Fill in as many underscores as you want: @or.inl _ _ ha (the second underscore would be for the "b").

[Reid Barton]

There's also docs#or.intro_left

[ccn]

I was proving a basic set theory fact and this suprised me

X : Type,
A B : set X,
x : X,
hint : x ∈ A ∩ Bᶜ
⊢ (λ (a : X), a ∉ B) x

I'm not really sure what the goal is here, am I supposed to be making a function? I've tried exact x and exact hint but they don't work.

[Yakov Pechersky]

Try dsimp first

[Kyle Miller]

A #mwe would be good for this to know how you got into this situation. You can do dsimp only to beta reduce that lambda expression, giving you something definitionally equal.

[Eric Rodriguez]

fwiw this is the function mapping "a" to the proposition "a is not in B", applied to x.

[ccn]

Kyle Miller said:

A #mwe would be good for this to know how you got into this situation. You can do dsimp only to beta reduce that lambda expression, giving you something definitionally equal.

No problem, I am working on the real number game (https://www.ma.imperial.ac.uk/~buzzard/xena/rng090720/?world=1&level=6), click that link and paste in this code, you should be where I am at:

rw ext_iff,
intro x,
split,
{
  intro hdiff,
  split,
  exact hdiff.1,
  exact hdiff.2,
},
{
  intro hint,
  split,
  exact hint.1,
}

[ccn]

Eric Rodriguez said:

fwiw this is the function mapping "a" to the proposition "a is not in B", applied to x.

Ok, so that means I'm trying to prove that x is not in B right?

[ccn]

That was a good tip, hint.2 solved it for me!

It's a little weird why it didn't just say prove x is not in B though...

[ccn]

Is there a general way to prove arbitrary "true" inequalities like 57374 < 99999999 ?

[Eric Rodriguez]

norm_num

[ccn]

Would you be referring to this: https://leanprover-community.github.io/mathlib_docs/tactic/norm_num.html#norm_num.prove_lt_nat ?

[Arthur Paulino]

Btw you can just write docs#norm_num.prove_lt_nat and zulip will figure out the link :+1:

[Kyle Miller]

@ccn docs#set.diff is defined using set separation notation -- it takes a set and a predicate. What happened is that you split it, which while works, "breaks the set API", so you got something that notationally looks weird. (dsimp only does renormalize it, though).

You're supposed to use rw mem_sdiff_iff like the level introduces to not have things look weird.

[Kyle Miller]

and eric means tactic#norm_num

[Eric Rodriguez]

but no, it's just a tactic; if your goal is 1233462734 > 0, then by norm_num will solve it

[Kyle Miller]

And for similar reasons, I gave you bad advice about how to prove union membership earlier. You should be doing rw mem_union_iff first to not accidentally rely on implementation details.

[ccn]

Someone else used linarith what is that doing?

[Kyle Miller]

tactic#linarith automatically solves linear (in)equalities

[ccn]

I've been working on this limit proof, but I get stuck around here

import data.real.basic algebra.geom_sum
import analysis.special_functions.log
import order.succ_pred

def lim_to_inf (x : ℕ → ℝ) (l : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, abs (x n - l) < ε

#check (3 : ℝ)

theorem zero_point_nine_recurring_is_one :
  lim_to_inf (λ n, 9 / 10 * geom_sum (1 / 10) n) 1 :=
begin
  intro ε,
  intro hε,
  use nat.ceil ((real.log (ε)) / (real.log 1/10) - 1) + 1,
  intro n,
  intro hn,
  rw ge_iff_le at hn,
  have h1 := nat.lt_succ_self (⌈real.log ε / (real.log 1 / 10) - 1⌉₊),
  have h2 := lt_of_lt_of_le h1 hn,
  have h3 := nat.le_ceil (real.log ε / (real.log 1 / 10) - 1),
  -- have h4 := lt_of_le_of_lt h3 h2,
end

When I uncomment the last line there I get the following

type mismatch at application
  lt_of_le_of_lt h3 h2
term
  h2
has type
  ⌈real.log ε / (real.log 1 / 10) - 1⌉₊ < n
but is expected to have type
  ↑⌈real.log ε / (real.log 1 / 10) - 1⌉₊ < ?m_1
state:
ε : ℝ,
hε : ε > 0,
n : ℕ,
hn : ⌈real.log ε / (real.log 1 / 10) - 1⌉₊ + 1 ≤ n,
h1 : ⌈real.log ε / (real.log 1 / 10) - 1⌉₊ < ⌈real.log ε / (real.log 1 / 10) - 1⌉₊.succ,
h2 : ⌈real.log ε / (real.log 1 / 10) - 1⌉₊ < n,
h3 : real.log ε / (real.log 1 / 10) - 1 ≤ ↑⌈real.log ε / (real.log 1 / 10) - 1⌉₊
⊢ |(λ (n : ℕ), 9 / 10 * geom_sum (1 / 10) n) n - 1| < ε

I know that this has to do with coercion in some way, but I'm not sure how to get it to work, I think I need to somehow convert it all to real numbers, any tips?

[Yakov Pechersky]

Can you give your h1, h2, h3 explicit types? It'll be clearer to you and to us what you expect them to be.

[Kyle Miller]

@ccn Just answering your question without checking what you're doing:

  have h2' := nat.cast_lt.mpr h2,
  have h4 := lt_of_le_of_lt h3 h2',

I found this by

  have h2' : (⌈real.log ε / (real.log 1 / 10) - 1⌉₊ : ℝ) < (n : ℝ) := by library_search,

[ccn]

Yakov Pechersky said:

Can you give your h1, h2, h3 explicit types? It'll be clearer to you and to us what you expect them to be.

Sure I'll send it when I get home

[ccn]

Yakov Pechersky said:

Can you give your h1, h2, h3 explicit types? It'll be clearer to you and to us what you expect them to be.

I want to make the inequalities involving real numbers for now, would the type of that be ℝ < ℝ

[Reid Barton]

The type of h1 is whatever it is a proof of. It's displayed in the proof state you pasted earlier.

[ccn]

I have this proof:

example (a b c : ℝ) (hc : c ≤ 0) (hab :  a ≤ b) : b*c ≤ a*c :=
begin
  rw ← sub_nonneg,
  calc 0 ≤ (a - b)*c : mul_nonneg_of_nonpos_of_nonpos (by rwa sub_nonpos) hc
    ...  = a*c - b*c : by ring,
end

But I'm having trouble understanding some parts of it. Namely what the (by rwa sub_nonpos) is producing and how the calc tactic works.

[ccn]

To my understanding the by command will produce something? So it would be re-writing the current goal and outputting what that is (without changing what the actual goal is).

Does the calc tactic take a chain of inequalities and then just compress it to to the final inequality (in our case 0 \le a*c - b*c) and then exit tactic mode?

[Eric Rodriguez]

You're right about calc, although in a technical sense it's not actually a tactic. It has a special place in leans core systems but it's not super important; but note that you can calc in term mode

[Eric Rodriguez]

For the by, lean is working outside in - it knows what inequality you want, so it can synthesise the exact required goal for that specific term. You can see that by replacing the by with a begin end and seeing the goal there

[ccn]

I was recalling the different ways to define something:

I thought that when we have something like

def double (x: N) : N := x + x

It's the same as

def double : N -> N := lambda x, x + x

I wanted to try that out on this example:

example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : non_decreasing (g ∘ f) :=
λ x₁ x₂ h, hg (f x₁) (f x₂) (hf x₁ x₂ h)

I tried to do it myself, but I know something is off:

example  (ℝ → ℝ) → (ℝ → ℝ) → non_decreasing f  → non_decreasing g → non_decreasing (g ∘ f) :=
λ x₁ x₂ h, hg (f x₁) (f x₂) (hf x₁ x₂ h)

What would be the correct way of stating it?

[Kyle Miller]

fyi, there's a missing colon after example for the last one.

[Kyle Miller]

Haven't tested, but for the dependent types you need the pi:

example : Π (f : ℝ → ℝ) (g : ℝ → ℝ), non_decreasing f  → non_decreasing g → non_decreasing (g ∘ f) :=
λ f g x₁ x₂ h, hg (f x₁) (f x₂) (hf x₁ x₂ h)

[ccn]

Ah ok, that's making more sense, I managed to use check to get the type:

 ∀ (f g : ℝ → ℝ), non_decreasing f → non_decreasing g → non_decreasing (g ∘ f)

I recall that the forall symbol is the same thing as the pi symbol under the proposition and types correspondance?

[Kyle Miller]

Oh, sure, forall is idiomatic here.

The forall and pi symbols are completely equivalent, yielding the same type (a pi type). The pretty printer, when printing a pi type, looks to see if it's wrapping a Prop, and if it is the expression is printed with a forall rather than a pi symbol.

[ccn]

So this theorem:

theorem x  (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : non_decreasing (g ∘ f) :=
λ x₁ x₂ h, hg (f x₁) (f x₂) (hf x₁ x₂ h)

Even though the Pi isn't there is dependent just because of (hf : non_decreasing f) (hg : non_decreasing g) using f and g which were declared as arguments earlier?

[ccn]

Also if they have the same type then how come the same proof term doesn't work:

theorem y : ∀ (f g : ℝ → ℝ), non_decreasing f → non_decreasing g → non_decreasing (g ∘ f) :=
λ x₁ x₂ h, hg (f x₁) (f x₂) (hf x₁ x₂ h)

[Kyle Miller]

The rule is simply that when you move an argument from "before the colon" to after, you add a Π like so:

theorem x (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : non_decreasing (g ∘ f) := ...

is

theorem x (f g : ℝ → ℝ) (hf : non_decreasing f) : Π (hg : non_decreasing g), non_decreasing (g ∘ f) := ...

is

theorem x (f g : ℝ → ℝ) : Π (hf : non_decreasing f), Π (hg : non_decreasing g), non_decreasing (g ∘ f) := ...

is

theorem x (f : ℝ → ℝ) : Π (g : ℝ → ℝ), Π (hf : non_decreasing f), Π (hg : non_decreasing g), non_decreasing (g ∘ f) := ...

is

theorem x : Π (f : ℝ → ℝ), Π (g : ℝ → ℝ), Π (hf : non_decreasing f), Π (hg : non_decreasing g), non_decreasing (g ∘ f) := ...

(of course, using foralls instead of pis if you want). You can merge adjacent pis into a single one (that's a syntactic convenience). And, if it's non-dependent, you can use a function arrow (another syntactic convenience.)

[Kyle Miller]

That doesn't work because things before the colon are all automatically introduced with an implicit lambda.

[Kyle Miller]

You need f and g as additional arguments for the lambda after the :=.

[ccn]

Kyle Miller said:

That doesn't work because things before the colon are all automatically introduced with an implicit lambda.

woah that's super cool, how did you know about that?

[Tomaz Gomes Mascarenhas]

About the cases tactic:

when we try to case an element directly, like:

constant g : Option Nat → Option Nat
constant f : Option Nat →  Option Nat → Option Nat

theorem thm : ∀ {k : Option Nat}, f (g k) k = some 4 → g k = some 3 :=
  by intros k h
     cases k
     (...)

all the ks in the hypothesis gets substituted by none and some val. But, if we pattern match on (g k), then the (g k) in the hypothesis don't get substituted:

theorem thm : ∀ {k : Option Nat}, f (g k) k = some 4 → g k = some 3 :=
  by intros k h
     cases (g k)
     (...)

How do I substitute the (g k) in the hypothesis in this context?

[Yakov Pechersky]

Does "cases v : g k" work for you?

[Tomaz Gomes Mascarenhas]

oh, didn't know about that hehe. Yes, thanks! It is still weird though, this difference in the behaviour of this tactic

[ccn]

Kyle Miller said:

You need f and g as additional arguments for the lambda after the :=.

Ok, so I think I built this correctly now:

theorem y : ∀ (f g : ℝ → ℝ), non_decreasing f → non_decreasing g → non_decreasing (g ∘ f) :=
λ f g hf hg x₁ x₂ h, hg (f x₁) (f x₂) (hf x₁ x₂ h)

Are the types (f g hf hg x₁ x₂ h) of my lambda function automatically inferred?

[Kyle Miller]

@ccn I'm not sure how I knew about the implicit lambda, but this is how many programming languages seem to work (although many don't have dependent types).

Anyway, here are some examples:

def foo (x : ℕ) : ℕ := x + 1

#reduce foo
/- λ (x : ℕ), x.succ -/

def foo' : Π (x : ℕ), ℕ := λ x, x + 1

#reduce foo'
/- λ (x : ℕ), x.succ -/

def foo'' : ℕ → ℕ := λ x, x + 1

#reduce foo''
/- λ (x : ℕ), x.succ -/

[Kyle Miller]

@ccn Yes. λ x, x + 1 is short for λ (x : _), x + 1, for example, and Lean will try to fill in the the placeholder (the _).

[ccn]

So under the "type" way of thinking, I've showed a concrete example of an element of the correct type. In the proof way of thinking, we've found a proof for arbitrary f, g?

[Kyle Miller]

You can see for yourself by doing #print y after your theorem.

[ccn]

that's useful!

[ccn]

theorem t1 : p → q → p :=
assume hp : p,
assume hq : q,
show p, from hp

what does show p, from hp do?

[Kyle Miller]

https://leanprover.github.io/reference/expressions.html#structured-proofs

[Kevin Buzzard]

it's the same as hp -- it just announces what it's going to prove before it proves it.

[Eric Wieser]

Another model is that show P, from hp (in term mode) has the same effect as (id hp : P), both of which are a less forgetful version of (p : P).

[ccn]

I found this calc proof:

  calc
  |(u + v) n - (l + l')| = |u n + v n - (l + l')|   : rfl
                     ... = |(u n - l) + (v n - l')| : by congr' 1 ; ring
                     ... ≤ |u n - l| + |v n - l'|   : by apply abs_add
                     ... ≤  ε                       : by linarith,

I have a question about this line:

  |(u + v) n - (l + l')| = |u n + v n - (l + l')|   : rfl

I read about what rfl is and apparently it is eq.refl _ how is this different than refl? how can rfl work here if the two things on either side are different? Wouldn't we be using the fact that (a +b)*c = ac + bc ?

And also about the line

                     ... = |(u n - l) + (v n - l')| : by congr' 1 ; ring

I don't really understand what by congr' 1 ; ring is doing I know that congr' tries to prove equalities between applications of functions by recursively proving the arguments are the same. But what is the function here? Also what does the ; do in this case.

Thanks.

[Patrick Johnson]

I guess you're referring to this tutorial.

Tactic refl can be used in proof mode to prove any reflexive relation between definitionally equal terms.

Term rfl is defined to be equal to the constructor eq.refl of the equality type eq. Whenever two terms are definitionally equal, rfl can construct an equality between them.

In your example, u and v are functions from natural numbers to real numbers. Adding two functions is defined as u + v = λ x, u x + v x. That's definitional equality, so |(u + v) n - (l + l')| is definitionally equal to |u n + v n - (l + l')| and rfl can prove (construct) the equality.

Tactic congr' 1 reduces the goal from |u n + v n - (l + l')| = |u n - l + (v n - l')| to u n + v n - (l + l') = u n - l + (v n - l'). The absolute value is a unary function (see here). The semicolon applies the tactic on the right to every subgoal created by the tactic on the left. congr' 1 created just one goal, so ring is used to solve that goal. Semicolon is used instead of a comma to save us from adding parentheses around congr' 1 ; ring

[ccn]

Patrick Johnson said:

I guess you're referring to this tutorial.

Tactic refl can be used in proof mode to prove any reflexive relation between definitionally equal terms.

Term rfl is defined to be equal to the constructor eq.refl of the equality type eq. Whenever two terms are definitionally equal, rfl can construct an equality between them.

In your example, u and v are functions from natural numbers to real numbers. Adding two functions is defined as u + v = λ x, u x + v x. That's definitional equality, so |(u + v) n - (l + l')| is definitionally equal to |u n + v n - (l + l')| and rfl can prove (construct) the equality.

Tactic congr' 1 reduces the goal from |u n + v n - (l + l')| = |u n - l + (v n - l')| to u n + v n - (l + l') = u n - l + (v n - l'). The absolute value is a unary function (see here). The semicolon applies the tactic on the right to every subgoal created by the tactic on the left. congr' 1 created just one goal, so ring is used to solve that goal. Semicolon is used instead of a comma to save us from adding parentheses around congr' 1 ; ring

Great explanation thank you!

[ccn]

I also had another related question. I am reading this proof

-- A sequence admits at most one limit
-- 0037
example : seq_limit u l → seq_limit u l' → l = l' :=
begin
  -- sorry
  intros hl hl',
  apply eq_of_abs_sub_le_all,
  intros ε ε_pos,
  cases hl (ε/2) (by linarith) with N hN,
  cases hl' (ε/2) (by linarith) with N' hN',
  calc |l - l'| = |(l-u (max N N')) + (u (max N N') -l')| : by ring_nf
  ... ≤ |l - u (max N N')| + |u (max N N') - l'| : by apply abs_add
  ... =  |u (max N N') - l| + |u (max N N') - l'| : by rw abs_sub_comm
  ... ≤ ε : by linarith [hN (max N N') (le_max_left _ _), hN' (max N N') (le_max_right _ _)]
  -- sorry
end

But I have trouble with this line:

  ... ≤ |l - u (max N N')| + |u (max N N') - l'| : by apply abs_add

why aren't they just writing abs_add here? Doesn't apply get used when you have a function like p -> q and your goal is q so using apply you can change your goal to just p?

https://leanprover-community.github.io/mathlib_docs/algebra/order/group.html#abs_add

[Mario Carneiro]

if you write just abs_add, it would be a type error since abs_add has a type like \forall x y, |x + y| <= |x| + |y| while the goal is |a + b| <= |a| + |b| for some a,b

[Mario Carneiro]

you would have to write abs_add _ _

[Mario Carneiro]

by apply abs_add is saying "add underscores as necessary to make the types match up"

[Patrick Johnson]

Doesn't apply get used when you have a function like p -> q and your goal is q so using apply you can change your goal to just p?

That's correct. Note that A → B is a non-dependent function type (the type of the result does not depend on the value of the argument). A more general function type is Π (x : A), ϕ, where ϕ is some expression that depends on x. The Π symbol can be written as ∀ (they are interchangeable).

Term abs_add is a function whose type is ∀ x y, |x + y| ≤ |x| + |y|. As its type says, abs_add is a function that takes two arguments x and y, and returns a term of type |x + y| ≤ |x| + |y|. When you perform apply abs_add, the apply tactic looks at the type of the goal and figures out what x and y should be.

[Kyle Miller]

ccn said:

                     ... = |(u n - l) + (v n - l')| : by congr' 1 ; ring

If congr' 1 leads to only one goal, it's considered to be better style to write it like this:

                     ... = |(u n - l) + (v n - l')| : by { congr' 1, ring }

That makes is so that whenever you see ; then you can be sure it's because more than one goal is being manipulated.

Just thought I'd mention this. (I'm not sure when this became the style. Maybe within the last two years?)

[Reid Barton]

It also means you can see the proof state after congr' 1 by positioning the cursor there

[ccn]

I have this proof I wrote down on paper and I'd like to try to get it into a lean proof:

4x^3 - 7y^3 ≠ 2003

pf:

2003 ≡ 1 (mod 7) because 2002 = 7 * 286

x^3 mod 7 is congruent to {0, 1, -1} because

0^3 ≡ 0, 1^3 ≡ 1, 2^3 ≡ 1, 3^3 ≡ -1, 4^3  ≡ 1, 5^3 ≡ -1, 6^3 ≡ -1, 7^3 ≡ 0

so the pattern 0 1 1 -1 1 -1 -1 0 repeats forever

thus 4x^3 is congruent to one of {0 4, -4}.

For a contradiction assume 4x^3 - 7y^3 = 2003, then

4x^3 - 7y^3 ≡ 2003

4x^3  ≡ 1

which is impossible

My main questions are how we would show 2003 ≡ 1 (mod 7) and how we would prove something like this:

x^3 mod 7 is congruent to {0, 1, -1} because

0^3 ≡ 0, 1^3 ≡ 1, 2^3 ≡ 1, 3^3 ≡ -1, 4^3 ≡ 1, 5^3 ≡ -1, 6^3 ≡ -1, 7^3 ≡ 0

so the pattern 0 1 1 -1 1 -1 -1 0 repeats forever

Thanks!

[Kyle Miller]

Is this the answer to your first question?

import data.int.modeq
import tactic

example : 2003 ≡ 1 [ZMOD 7] :=
begin
  rw int.modeq_iff_dvd,
  norm_num,
end

[ccn]

Yeah it does, thank you! This norm_num thing seems super powerful

[ccn]

What does it mean to normalize numerical expressions?

[Alex J. Best]

Some other useful tactics for this sort of thing are docs#dec_trivial and tactic#norm_cast or tactic#push_cast to deal with coercions from the integers to integers mod a number

Here's how I'd show this

lemma ok : ∀ x : zmod 7, x^3 ∈ [(0 : zmod 7), 1, -1] := dec_trivial
lemma problem (x y : ℤ) : 4 * x^3 - 7 * y^3 ≠ 2003 :=
begin
  suffices : (4 * x^3 - 7 * y^3 : zmod 7) ≠ 2003,
  { intro h,
    apply this,
    apply_fun (coe : ℤ → zmod 7) at h,
    push_cast at h,
    exact h, },
  have : (2003 : zmod 7) = (1 : zmod 7),
  dec_trivial,
  rw this,
  have : (7 : zmod 7) = (0 : zmod 7),
  dec_trivial,
  simp only [this, zero_mul, sub_zero],
  generalize : (↑x : zmod 7) = X,
  rcases ok X with h | h | h | ⟨⟨⟩⟩;
  rw [h]; dec_trivial,
end

[Kyle Miller]

zmod, like what @Alex J. Best, is a lot easier to work with and probably a better choice.

I wanted to see what it was like continuing to work with ZMOD for the next part:

example (x : ℤ) : x^3 ≡ 0 [ZMOD 7] ∨ x^3 ≡ 1 [ZMOD 7] ∨ x^3 ≡ -1 [ZMOD 7] :=
begin
  have h1 : (x % 7)^3 ≡ x^3 [ZMOD 7],
  { apply int.modeq.pow,
    exact int.mod_modeq x 7, },
  have h2 : ∀ n, x^3 ≡ n [ZMOD 7] ↔ (x % 7)^3 ≡ n [ZMOD 7],
  { intro n,
    split,
    { intro h, exact h1.trans h },
    { intro h, exact h1.symm.trans h }, },
  simp_rw h2,
  generalize hy : x % 7 = y,
  have h3 : 0 ≤ y,
  { subst y,
    apply int.mod_nonneg,
    norm_num, },
  have h4 : y < 7,
  { subst y,
    apply int.mod_lt_of_pos,
    norm_num, },
  clear h1 h2 hy x,
  simp_rw int.modeq_iff_dvd,
  interval_cases using h3 h4;
  norm_num,
end

[Kyle Miller]

interval_cases seems to be rather slow in this proof. I don't have much experience with it to know whether that's expected

[ccn]

Thanks for the help both of you!

@Alex J. Best I'm trying to explore your proof but it's giving me some issues, do I need to import some things? image.png

[Alex J. Best]

Probably import data.zmod.basic?

[Alex J. Best]

I wrote this in another file with other stuff in so I'm not sure sorry!

[ccn]

that solved it!

[ccn]

Alex J. Best said:

Some other useful tactics for this sort of thing are docs#dec_trivial and tactic#norm_cast or tactic#push_cast to deal with coercions from the integers to integers mod a number

Here's how I'd show this

lemma ok : ∀ x : zmod 7, x^3 ∈ [(0 : zmod 7), 1, -1] := dec_trivial
lemma problem (x y : ℤ) : 4 * x^3 - 7 * y^3 ≠ 2003 :=
begin
  suffices : (4 * x^3 - 7 * y^3 : zmod 7) ≠ 2003,
  { intro h,
    apply this,
    apply_fun (coe : ℤ → zmod 7) at h,
    push_cast at h,
    exact h, },
  have : (2003 : zmod 7) = (1 : zmod 7),
  dec_trivial,
  rw this,
  have : (7 : zmod 7) = (0 : zmod 7),
  dec_trivial,
  simp only [this, zero_mul, sub_zero],
  generalize : (↑x : zmod 7) = X,
  rcases ok X with h | h | h | ⟨⟨⟩⟩;
  rw [h]; dec_trivial,
end

Your link to dec_trivial didn't load for me, where can I read about it?

[Alex J. Best]

Oh right, its a funny one, both a tactic and a term, but defined via notation so there isn't a docs link.
Anyway you can read this section of tpil to learn about it https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#decidable-propositions

[ccn]

So I'm trying to understand what's happening in this section of the proof:

  suffices : (4 * x^3 - 7 * y^3 : zmod 7) ≠ 2003,
  { intro h,
    apply this,
    apply_fun (coe : ℤ → zmod 7) at h,
    push_cast at h,
    exact h, },

So far my translation is, let's prove (4 * x^3 - 7 * y^3 : zmod 7) ≠ 2003 so for the sake of contradiction, we assume (4 * x^3 - 7 * y^3 : zmod 7) = 2003, now we have to derive a contradiction.

What does the apply this mean?

[ccn]

My confusion comes in because in the tactic screen everything looks the same:
Uploading image.png…

[ccn]

xy: ℤ
this: 4 * ↑x ^ 3 - 7 * ↑y ^ 3 ≠ 2003
h: 4 * x ^ 3 - 7 * y ^ 3 = 2003
⊢ 4 * ↑x ^ 3 - 7 * ↑y ^ 3 = 2003

[ccn]

Hmm ↑x ^ 3 has type zmod 7

[ccn]

Oh so this is actually everything (mod 7) right?

[ccn]

Disregard above questions, I think I understand what's going on now.

[ccn]

I guess it's just confusing when the goal state says something like this:

2 goals
xy: ℤ
⊢ 2003 = 1

and you don't know it's mod 7 until you hover

[Alex J. Best]

Yeah that is a bit unfortunate, I don't know any way of getting it to tell you that info other than hovering.
But yes the idea is first to move the goal to zmod 7
Here's another way of phrasing the same proof, maybe its simpler to see what's happening?

lemma ok : ∀ x : zmod 7, x^3 ∈ [(0 : zmod 7), 1, -1] := dec_trivial
lemma problem (x y : ℤ) : 4 * x^3 - 7 * y^3 ≠ 2003 :=
begin
  intro h, -- asume they are equal
  apply_fun (coe : ℤ → zmod 7) at h, -- then they are equal mod 7
  push_cast at h, -- simplifying coercions
  have : (2003 : zmod 7) = (1 : zmod 7),
  dec_trivial,
  rw this at h,
  have : (7 : zmod 7) = (0 : zmod 7),
  dec_trivial,
  simp only [this, zero_mul, sub_zero] at h, -- more simplifying
  rcases ok (x : zmod 7) with h' | h' | h' | ⟨⟨⟩⟩; -- now we have only the 3 cases from before
  rw [h'] at h; revert h; dec_trivial, -- h is decidably a contradiction in all cases
end

[ccn]

Ok, I'm understanding more and more of this proof, only part that's tripping me up is now this:

  rcases ok (x : zmod 7) with h' | h' | h' | ⟨⟨⟩⟩; -- now we have only the 3 cases from before
  rw [h'] at h; revert h; dec_trivial, -- h is decidably a contradiction in all case

So I'm assuming h' | h' | h' | ⟨⟨⟩⟩ gives us the three cases on the value of what x could be what does the ⟨⟨⟩⟩ do though?

[Alex J. Best]

it gets rid of the trivial goal that x is in the empty list, if you delete just | ⟨⟨⟩⟩ and the semicolon you'll see there are 4 goals, adding the | ⟨⟨⟩⟩ back there are only 3

[Alex J. Best]

but the trick is I didn't write that by hand :wink: I used rcases? ok (x : zmod 7), which tells me the magic words to type for me

[Alex J. Best]

Well it tries to anyway, seems there is a bit of a bug with x : zmod 7 but hopefully you can see it tells us almost the right thing here

[ccn]

Alex J. Best said:

it gets rid of the trivial goal that x is in the empty list, if you delete just | ⟨⟨⟩⟩ and the semicolon you'll see there are 4 goals, adding the | ⟨⟨⟩⟩ back there are only 3

What does it mean for x to be in the empty list

[Kyle Miller]

(Maybe there should be a pretty printer option to print certain numerals in the form (2007 : zmod 7)? I've found this to be confusing to manipulate before.)

[ccn]

Alex J. Best said:

Oh right, its a funny one, both a tactic and a term, but defined via notation so there isn't a docs link.
Anyway you can read this section of tpil to learn about it https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#decidable-propositions

So dec_trivial is like if a computer has an algorithm to figure out if this thing is true or not

[ccn]

How does that differ from things like linarith and ring then?

[Alex J. Best]

ccn said:

Alex J. Best said:

it gets rid of the trivial goal that x is in the empty list, if you delete just | ⟨⟨⟩⟩ and the semicolon you'll see there are 4 goals, adding the | ⟨⟨⟩⟩ back there are only 3

What does it mean for x to be in the empty list

Well it doesn't make sense, so we don't need to consider that case, but lean needs to be reminded of that somehow.

[ccn]

Alex J. Best said:

ccn said:

Alex J. Best said:

it gets rid of the trivial goal that x is in the empty list, if you delete just | ⟨⟨⟩⟩ and the semicolon you'll see there are 4 goals, adding the | ⟨⟨⟩⟩ back there are only 3

What does it mean for x to be in the empty list

Well it doesn't make sense, so we don't need to consider that case, but lean needs to be reminded of that somehow.

How come that case is generated anyways then?

[Alex J. Best]

There are a few difference but the main one is that linarith and ring are allowed to fail, if a decidable algorithm exists it will always (eventually return) either a proof or a disproof.

[Alex J. Best]

ccn said:

How come that case is generated anyways then?

These cases appear because the definition of x^3 ∈ [(0 : zmod 7), 1, -1] unfolds to x^3 ∈ [(0 : zmod 7), 1] \/ x^3 = -1 which is then x^3 ∈ [(0 : zmod 7)] \/ x^3 = 1 \/ x^3 = -1 which becomes x^3 ∈ [] \/ x^3 = 0 \/ x^3 = 1 \/ x^3 = -1. The empty list is treated the same as all others in the definition of being a member of a list

[ccn]

What is the point of the revert h; dec_trivial ?

[ccn]

expanding it out it looks like this: image.png

[Johan Commelin]

dec_trivial tries to prove the goal, without looking at your assumptions.

[ccn]

Wouldn't we want to use somethign like docs#succ_ne_zero ?

[Johan Commelin]

So any assumptions that should be used must be reverted into the goal first.

[ccn]

I see

[Alex J. Best]

ccn said:

Wouldn't we want to use somethign like docs#succ_ne_zero ?

this goal is about zmod 7 so succ_ne_zero won't apply I think

[Johan Commelin]

I haven't followed the thread. But succ_ne_zero doesn't hold in zmod 7, right? :wink:

[ccn]

Oh right

[Johan Commelin]

You could use mul_zero and zero_ne_one.

[ccn]

So that's like a more generalized version

[ccn]

where does the the decidability aspect come into the proving of 4 * 0 = 1 -> false ?

[Alex J. Best]

You can use other proof methods here, but the nice thing about decidability is that once we get to a small finite statement in the right form we can be pretty sure it will work without worrying about what other lemmas we need.

[ccn]

What constitutes the right form?

[Alex J. Best]

The lemma ok is where this method really shines.

[Alex J. Best]

ccn said:

What constitutes the right form?

Well the main thing is what Johan says, dec_trivial doesn't look at your assumptions, so you have to use revert to make the goal statement false on its own.

[ccn]

Ok, I get the gist of it, I think it'll get more clear the more I use it

[Kyle Miller]

ccn said:

What constitutes the right form?

There's are a great number of decidable instances in mathlib, and "the right form" is that one of them matches your proposition. (Though, even if one matches, that doesn't guarantee dec_trivial will succeed...)

[Kyle Miller]

If you click the dropdown under docs#decidable you can see them (not that this is very helpful -- the only point is that there are quite a few!)

[ccn]

thanks!

[ccn]

I know about the ⟨⟩ as the anonymouse construction notation so when we prove something like there exists x in N P(x), we can just do like ⟨3, Q 3⟩ or something like that, but I feel like it's being used in a different fashion in

  rcases ok (x : zmod 7) with h' | h' | h' | ⟨⟨⟩⟩, -- now we have only the 3 cases from before

what's going on there?

[Yaël Dillies]

It's being used in the exact same way here. Its point is to construct and destruct structures. In that case, it destructs one-field structures.

[Yaël Dillies]

I suspect one of them being docs#eq

[ccn]

Ok so this thing is a structure and we're taking it apart?
image.png

[ccn]

Isn't that like a hypothesis though?

[Yaël Dillies]

Precisely, it's an inductive!

[Yaël Dillies]

docs#list.mem

[Yaël Dillies]

The ... | ... bit breaks the inductive part. The ⟨...⟩ bit breaks the structure part.

[ccn]

An inductive type is a type where you make some constructors which describe how to make new elements right?

[Yaël Dillies]

Hmm, yes, but that's true of everything.

[Yaël Dillies]

Take it as a pinch of salt, I'm not a type theorist, but an inductive type at your level is a primitive in the calculus of inductive constructions. Each inductive has a bunch of constructors, and constructors can refer to each other (in specific ways and the rules are complicated). Structures too are inductives, but they only have one constructor.

[ccn]

Ok, I'm trying to understand the usage of the ... | ... and the ⟨...⟩ on this example:

h1 : a ∧ b ∧ c ∨ d

and in the docs they do rcases h1 with ⟨ha, hb, hc⟩ | hd

Why didn't they just do : rcases h1 with ⟨ha, hb, hc, hd⟩ ?

[Yaël Dillies]

because ∨ is an inductive with two constructors

[Kyle Miller]

| is for alternatives, angle brackets are for (generalized) products. So, different constructors vs arguments to same constructor

[Kyle Miller]

If it helps, these are the parentheses:

h1 : (a ∧ (b ∧ c)) ∨ d

[ccn]

Why is and a structure but or is an inductive shouldn't they be the same?

[Yaël Dillies]

If they were the same, we wouldn't need both!

[Yaël Dillies]

Think about it. How do you build an and? How do you build an or?

[ccn]

two things and put them together

[ccn]

But they would be different right? One is true in the example of T and F and the other false?

[Yaël Dillies]

You're thinking docs#band and docs#bor

[Yaël Dillies]

But how to make the type of proofs of P and Q?

[Kyle Miller]

by "build", Yael means roughly, "how would you prove an 'and'? how would you prove an 'or'?"

[Yaël Dillies]

and the type of proofs of P or Q?

[ccn]

When we have p : Prop p is a proof of the proposition right?

[Kyle Miller]

Going back to "why is and a structure": a structure is an inductive with exactly one constructor

[ccn]

Yaël Dillies said:

But how to make the type of proofs of P and Q?

So you would want P and Q to have the type Prop and then you need p: P and q:Q

[Kyle Miller]

(structure is a special case with some special notation because it's useful)

[Julian Berman]

Wait, is that correct? -- zulip lagged, sorry -- p : Prop -- p is the statement, not the proof, and f : p f is a proof of p, right?

[Patrick Massot]

ccn said:

When we have p : Prop p is a proof of the proposition right?

No. p: Prop means p is a proposition. Then hp : p means hp is a proof of that proposition p.

[Yaël Dillies]

Julian Berman said:

Wait, is that correct? -- zulip lagged, sorry -- p : Prop -- p is the statement, not the proof, and f : p f is a proof of p, right?

Whoops sorry, read that too quick

[ccn]

Ok, I see. so if we have p q: Prop then p ∧ q should also be a proposition and then j : p ∧ q would mean j is a proof of p ∧ q right?

[ccn]

If I replace the and symbol with or in above, then that would be right when we're talking about the or as well right?

[Julian Berman]

Yep, those are also ways to make propositions out of other ones things.

[ccn]

So this is somehow a roadblock for us to have or and and both be inductive types?

[Yaël Dillies]

Strictly speaking, they both are.

[Kyle Miller]

Don't be fooled by structure, they're both inductive types. They can be written like this:

inductive and (P Q : Prop) : Prop
| intro (p : P) (q : Q) : and

inductive or (P Q : Prop) : Prop
| inl (p : P) : or
| inr (q : Q) : or

[ccn]

My question is why can't they be described in the same fashion

[Arthur Paulino]

by "build", Yael means roughly, "how would you prove an 'and'? how would you prove an 'or'?"

this question is really insightful

[Yaël Dillies]

Isn't that the same fashion enough to you?

[Kyle Miller]

I guess like Yael said earlier, if they were described in exactly the same way, then and and or would be logically equivalent. That doesn't sound right, right?

[Arthur Paulino]

I think I understand his doubt. Abstracting technicalities, and and or have different levels of restrictions to be instantiated

[Arthur Paulino]

For an and, you need two things to be true in order to build it. Whereas for an or one true thing is enough

[ccn]

Arthur Paulino said:

For an and, you need two things to be true in order to build it. Whereas for an or one true thing is enough

Oh ok, this helps me think about it!

[Kyle Miller]

Then you need to think about the reverse for rcases: if you have an and, then you can get both things out of it, and if you have an or, you can get one thing, but you don't know which, so you have to be able to handle both cases.

[ccn]

Alex J. Best said:

ccn said:

How come that case is generated anyways then?

These cases appear because the definition of x^3 ∈ [(0 : zmod 7), 1, -1] unfolds to x^3 ∈ [(0 : zmod 7), 1] \/ x^3 = -1 which is then x^3 ∈ [(0 : zmod 7)] \/ x^3 = 1 \/ x^3 = -1 which becomes x^3 ∈ [] \/ x^3 = 0 \/ x^3 = 1 \/ x^3 = -1. The empty list is treated the same as all others in the definition of being a member of a list

So because the or is an inductive type with multiple constructors we can use the ... | ... syntax to break it into different cases (but if that's true why is the first case x^3 = 0 rather than x^3 being in the empty list?), in any case when we deal with the empty list somehow ⟨⟨⟩⟩ solves it automatically? How is it doing that?

[ccn]

Are these list.mem's constructors? image.png

[ccn]

Is it normal in the docs to not say that it's an inductive type ?

[Kyle Miller]

list.mem is not an inductive type

[Kyle Miller]

it's a function that creates an or expression (so creates an inductive type)

[Kyle Miller]

list.mem a [b1, b2] is a = b1 or a = b2 or false

[ccn]

Yaël Dillies said:

Precisely, it's an inductive!

Wait is an inductive an instance of an inductive type?

[ccn]

If list.mem has two constructors (like the or example)though shouldn't we be using the ... | ... on it rather than using the ⟨⟩

[Kyle Miller]

list.mem is just a recursive function, and I wouldn't call those two cases with red arrows in your image "constructors". I presume Yael is referring to this function's output

[ccn]

Ok, so somehow the ⟨⟨⟩⟩ can solve list.mem (↑x ^ 3) list.nil, what's happening there?

[Yaël Dillies]

false too is an inductive type!

[ccn]

image.png I thought they're supposed to have constructors?

[ccn]

how do you even make this thing

[Kyle Miller]

ccn said:

how do you even make this thing

exactly :smile:

[ccn]

oh ok, so you're allowed to have zero constructor inductive type

[ccn]

And you're not allowed to make something false is what that means?

[ccn]

image.png

[Yaël Dillies]

It's even stronger! If you happen to have made a term of type false, then :explosion:

[Kyle Miller]

(I'm not understanding why rcases needs two levels of angle brackets for this nil case. The first level seems to do nothing...)

[Kyle Miller]

it's really called the principle of explosion :boom:

[Kyle Miller]

this is the main way you use false, by getting anything you want from it:

false.elim : Π {C : Sort u_1}, false → C

[ccn]

What does it mean for true to have a constructor?

[Kyle Miller]

it means you can prove true by definition

[Kyle Miller]

the proof is true.intro

[ccn]

So true can prove itself

[Kyle Miller]

and false having no constructors: by definition you cannot prove it

[ccn]

I see

[Kyle Miller]

ccn said:

So true can prove itself

true is not a proof of true, if that's what you mean. true.intro is the proof of true

[ccn]

right right

[ccn]

Ok, if you have h: a ∧b then we can deconstruct it like ⟨ha, hb⟩ but what does if you deconstructed something by using ⟨⟩ that means that whatever you deconstructed has no constructors?

[Arthur Paulino]

⟨⟩ is the constructor that takes no parameter

structure Q
def q : Q := ⟨⟩
#check q -- q : Q

[ccn]

Ok so the ⟨...⟩ is only used on things with only one constructor?

[Kyle Miller]

I'm confused with you here, @ccn. Angle brackets are for a constructor of an inductive type, but false has no constructors. Maybe this is undocumented behavior of rcases?

[Arthur Paulino]

ccn said:

Ok so the ⟨...⟩ is only used on things with only one constructor?

Hm? :thinking:
Things that have constructors can only have one constructor

[Yaël Dillies]

Wrong, Arthur. All inductives have constructors.

[Kyle Miller]

rcases lets you use angle brackets for each constructor using ⟨...⟩ | ⟨...⟩ | ... | ⟨...⟩

[Kyle Miller]

@Yaël Dillies Arthur is referring to generic constructor syntax being for only one-constructor inductives

[Arthur Paulino]

Yaël Dillies said:

Wrong, Arthur. All inductives have constructors.

But I mean, each inductive has its own constructor (and it's unique) (except for things like false?)

[Yaël Dillies]

I'm confused by what you're confused about

[Yaël Dillies]

⟨⟩ to me is just syntax for the nullary ⟨...⟩ | ⟨...⟩ | ... | ⟨...⟩.

[Yaël Dillies]

or the unary version with no arguments, typically for docs#eq

[Kyle Miller]

it might be "just" syntax for that, but it appears to be undocumented

[Kyle Miller]

It seems like it needs either a special case, or it's a side-effect of how rcases is implemented, to have ⟨⟩ work for false

[Arthur Paulino]

ccn said:

Ok so the ⟨...⟩ is only used on things with only one constructor?

What got me confused was that this question seemed to raise the possibility of certain types having two or more constructors

[Kyle Miller]

Like or?

[Arthur Paulino]

mindblow
I never thought of it this way :open_mouth:

[Arthur Paulino]

Indeed, it has two distinct constructors

[Arthur Paulino]

But then his question holds. Is it possible to instantiate or with two distinct anonymous constructors?

[Yaël Dillies]

For sum at least, I don't see how. How would Lean know which side to put a : α in α ⊕ α? For p ∨ p, proof irrelevance means it doesn't matter.

[Mario Carneiro]

Kyle Miller said:

(I'm not understanding why rcases needs two levels of angle brackets for this nil case. The first level seems to do nothing...)

The reason is because the general case of rcases destructuring is ⟨a⟩ | ⟨b, c⟩ | ⟨d, e, f⟩ (if the inductive had one argument in the first constructor, two in the second and three in the third). You can also leave off trailing arguments and they will be filled with _ as needed. When a constructor has only one argument the angle brackets can be omitted when there is already a | indicating that we need to pattern match, but this leads to an ambiguity if you use an empty bracket: ⟨⟩ | ⟨hb⟩ matching a \/ b could mean either ⟨_⟩ | ⟨b⟩ (bind _ha : a and hb : b) or ⟨⟨⟩⟩ | ⟨b⟩ (bind _ha : a and hb : b, and then pattern match _ha : a with pattern ⟨⟩, which in this case would fail but might clear the case if a was, say, false). So the convention in this case is to use double brackets.

[Mario Carneiro]

Kyle Miller said:

It seems like it needs either a special case, or it's a side-effect of how rcases is implemented, to have ⟨⟩ work for false

There is kind of a syntactic hole for zero-ary patterns. (a | b | c) matches a 3-variant inductive, (a | b) matches 2-variant, a is a no op but ⟨a⟩ can be used to match a 1-variant inductive (a structure), but what would you write for a zero-variant inductive? ()? ⟨⟩? Nothing at all? In reality, anything other than an atomic pattern like a or _ can be used to indicate that you want to keep matching, and once it hits a false anything beyond that is ignored. So you could use (_|_) or ⟨⟨but⟩|⟨why⟩⟩ if you wanted, and the convention is to use ⟨⟩ to match on a unit structure (like unit or eq) or an empty inductive like false or empty.

[ccn]

Hey I want to prove this theorem,

theorem induction_nfactltnexpnm1ngt3
  (n : ℕ)
  (h₀ : 3 ≤ n) :
  nat.factorial n < n^(n - 1) :=
begin

end

I've come up with the proof on paper by using induction on numbers greater than 3, so my base case is when n = 3, but when I try to start the proof off with induction n with k IH I get

case nat.zero
h₀: 3 ≤ 0
⊢ 0! < 0 ^ (0 - 1)
case nat.succ
k: ℕ
IH: 3 ≤ k → k! < k ^ (k - 1)
h₀: 3 ≤ k.succ
⊢ (k.succ)! < k.succ ^ (k.succ - 1)

as a tactic state which isn't really what I wanted to prove (the base case).

How could I model this correctly? (eg having base case of k =3)

[Yaël Dillies]

Do induction on h₀!

[ccn]

Ah, I didn't know it could be used more generally like that. What's going on when it's not a varaible, but a hypothesis instead?

[Yaël Dillies]

docs#nat.le is defined inductively, so induction simply follows the definition.

[ccn]

Thank you! image.png which part is inductive?

[ccn]

isn't it using less_than_or_equal ?

[ccn]

Ah, and that is recursive: image.png

[Kyle Miller]

One downside of induction on the le is that the syntax goes so wrong. Is this something we can fix? (Also: is there a reason we have nat.le in front of nat.less_than_or_equal?)

[Kyle Miller]

One solution is having a custom induction principle for le notation for nat

[Yaël Dillies]

Do you mean docs#nat.le_induction? :wink:

[Kyle Miller]

It seems like that doesn't work with induction, but refine is fine:

theorem induction_nfactltnexpnm1ngt3
  (n : ℕ)
  (h₀ : 3 ≤ n) :
  nat.factorial n < n^(n - 1) :=
begin
  refine nat.le_induction _ (λ n' ih, _) n h₀,

end

(@ccn That's how you can get some better syntax for your contexts.)

[ccn]

How would I prove something like c * x^a < c * (x+1)^a (I'm just adding one to x, but it has to get bigger)

[Mario Carneiro]

first get rid of the c with docs#mul_lt_mul_left

[Mario Carneiro]

then use docs#pow_lt_pow_of_lt_left

[ccn]

Thanks Mario!

[ccn]

What do you use to prove this?

example (k : ℕ) (h: 3 <= k) : 0 < k - 1 :=
begin
  linarith,
end

linarith fails here, if I change k to be an integer instead of a natural number it works though...

linarith failed to find a contradiction
state:
k : ℕ,
h : 3 ≤ k,
ᾰ : 0 ≥ k - 1
⊢ false

[Patrick Johnson]

example (k : ℕ) (h: 3 ≤ k) : 0 < k - 1 :=
nat.sub_pos_of_lt (lt_of_lt_of_le dec_trivial h)

[ccn]

Thanks Patrick

[ccn]

I worked on this proof for a while and managed to get it this far:

theorem induction_nfactltnexpnm1ngt3
  (n : ℕ)
  (h₀ : 3 ≤ n) :
  nat.factorial n < n^(n - 1) :=
begin
  induction h₀ with k h₀,
  {
    norm_num,
  },
  {
    have h: k < k.succ := lt_add_one k,
    have hpos: 0 <= k := zero_le k,
    have kpos: 0 < k-1 := nat.sub_pos_of_lt (lt_of_le_of_lt dec_trivial h₀),
    have hpow : k^(k-1) < k.succ^(k-1), from pow_lt_pow_of_lt_left h hpos kpos,
    have kp1pos : 0 < k.succ, by linarith,
    have hf : k.succ * k ^ (k-1) < k.succ * (k.succ) ^ (k-1), from (mul_lt_mul_left kp1pos).mpr hpow,

    calc k.succ.factorial = k.succ * k.factorial : rfl
                      ... < k.succ * k ^ (k-1) : (mul_lt_mul_left kp1pos).mpr h₀_ih
                      ... < k.succ * (k.succ) ^ (k-1): hf
                      ... = k.succ ^ k: sorry
                      ... = k.succ ^ (k.succ-1): rfl
  }
end

aside from the one sorry, this proof should be correct, but I'd like to reduce the size of it somehow so it reads more like this:

Could anyone help me reduce the size of my proof?

I mainly want to get rid of the trivial inequalities involving zero.

[Mario Carneiro]

to prove the sorry, rewrite with docs#pow_succ and then docs#nat.sub_add_cancel

[Mario Carneiro]

also don't forget to make an #mwe when you post theorems here

[Mario Carneiro]

(i.e. put the import line)

[Mario Carneiro]

Here's how I would write it:

import tactic.linarith

theorem fact_lt_pow_self_sub_one
  (n : ℕ)
  (h₀ : 3 ≤ n) :
  nat.factorial n < n^(n - 1) :=
begin
  induction h₀ with k h₀ ih, {dec_trivial},
  simp,
  refine ((mul_lt_mul_left (nat.succ_pos _)).2 ih).trans_le _,
  refine (nat.mul_le_mul_left _ $ nat.pow_le_pow_of_le_left (nat.le_succ _) _).trans _,
  rw [← pow_succ, nat.sub_add_cancel],
  exact le_trans dec_trivial h₀
end

[Mario Carneiro]

Here it is with a calc block if you're into that sort of thing:

import tactic.linarith

open_locale nat
theorem fact_lt_pow_self_sub_one
  (n : ℕ)
  (h₀ : 3 ≤ n) :
  nat.factorial n < n^(n - 1) :=
begin
  induction h₀ with k h₀ ih, {dec_trivial},
  have k1 : 1 ≤ k := le_trans dec_trivial h₀,
  calc k.succ * k!
      < k.succ * k ^ (k - 1) : (mul_lt_mul_left (nat.succ_pos _)).2 ih
  ... ≤ k.succ ^ (k - 1 + 1) : nat.mul_le_mul_left _ $ nat.pow_le_pow_of_le_left (nat.le_succ _) _
  ... = k.succ ^ k : by rw [nat.sub_add_cancel k1],
end

[Patrick Johnson]

If you prefer to do induction on nat instead of ≤

example {n : ℕ} (h : 3 ≤ n) : n.factorial < n ^ (n - 1) :=
begin
  obtain ⟨n, rfl⟩ := nat.exists_eq_add_of_le h, induction n with n hn, dec_trivial,
  simp [nat.add_succ, nat.factorial] at *, nth_rewrite 3 nat.succ_add, rw pow_succ,
  apply (mul_lt_mul_left (nat.zero_lt_succ _)).mpr (lt_trans hn _), simp_rw nat.succ_add,
  exact nat.pow_lt_pow_of_lt_left (nat.lt_succ_self _) (nat.zero_lt_succ _),
end

[ccn]

Thanks for showing me your approaches, it helps me learn a lot!

[ccn]

Mario Carneiro said:

Here it is with a calc block if you're into that sort of thing:

import tactic.linarith

open_locale nat
theorem fact_lt_pow_self_sub_one
  (n : ℕ)
  (h₀ : 3 ≤ n) :
  nat.factorial n < n^(n - 1) :=
begin
  induction h₀ with k h₀ ih, {dec_trivial},
  have k1 : 1 ≤ k := le_trans dec_trivial h₀,
  calc k.succ * k!
      < k.succ * k ^ (k - 1) : (mul_lt_mul_left (nat.succ_pos _)).2 ih
  ... ≤ k.succ ^ (k - 1 + 1) : nat.mul_le_mul_left _ $ nat.pow_le_pow_of_le_left (nat.le_succ _) _
  ... = k.succ ^ k : by rw [nat.sub_add_cancel k1],
end

How does the dollar sign work here?

[Arthur Paulino]

$ nat.pow_le_pow_of_le_left (nat.le_succ _) _ is the same as (nat.pow_le_pow_of_le_left (nat.le_succ _) _)

It's just a way to write with less parentheses

[ccn]

Is the purpose so you can delimit in a more readable fashion?

[Patrick Johnson]

Also note that $ is right associative, so a $ b $ c $ d is equal to a (b (c d))

[ccn]

Previously we were able to have this proof:

  have main : ∀ (x : zmod 7), x^3 ∈ [(0 : zmod 7), 1, -1],
    dec_trivial

I wanted to prove another fact about modular arithmetic, but the same proof didn't work:

  have main : ∀ (n : ℕ), (4^n: zmod 12) = (4: zmod 12),
    dec_trivial

because it failed to synthesize the type class.

Would I have to prove this by induction?

[Mario Carneiro]

It's not at all obvious that the same kind of proof works. 4^n % 12 could have arbitrary non-periodic behavior

[Mario Carneiro]

In fact it doesn't, this is Fermat's little theorem, but there is definitely something to show

[Mario Carneiro]

In this case the simplest proof is induction, like you suggest, since the period is 1

[Damiano Testa]

I'm not at a computer now, but is it even true for n=0?

[ccn]

You're right, It'll have to be for positive naturals.

[ccn]

Thanks for the feedback

[Andrew Lubrino]

removed

[ccn]

I've modified the statement to be this now: ∀ (n : ℕ), (4^(n+1): zmod 12) = (4: zmod 12)

in the induction step, I have this:

case nat.succ
k: ℕ
IH: 4 ^ (k + 1) = 4
⊢ 4 ^ (k.succ + 1) = 4

(note these numbers are mod 12).

I want to use the fact that if 4^(k+1) = 4 (mod 12), then I can multiply both sides by any constant (in this case 4).

I've been looking around for the modular arithmetic docuemntation, but just found this link: https://leanprover-community.github.io/mathlib_docs/number_theory/modular.html which doesn't seem right when I read the contents. Where could I find the theorem I need here?

[Damiano Testa]

Does rw [pow_succ, IH] get you to 4 * 4 = 4?

[ccn]

Yes it does!

[Damiano Testa]

You may need an succ_eq_add_one as well. apparently not!

[ccn]

so now I just need to prove 4 * 4 = 4 (mod 12) I can just use norm_num for something like that right?

[ccn]

norm_num just makes the goal 16 = 4

[Damiano Testa]

At this stage, dec_trivial might work? Not sure...

[ccn]

Oh, you're right dec_trivial works, that works because that fact is something that could be derived from an algorithm, is that right?

[Damiano Testa]

I think so, but a very specific type of algorithm: brute-force.

[Damiano Testa]

Your previous statement was a fact about all natural numbers, while this one is about elements of zmod 12.

[ccn]

Which works because these are now finite things?

[Damiano Testa]

Brute-force works in the latter but not in the former

[ccn]

Thanks for the help, I'm still a little interested in the basic number theory facts though, do you think you could point me to where I could learn about them in the docs?

[Damiano Testa]

Things are more subtle than this and I do not really know the details, but for dec_trivial to work you should really have a finite statement, not just a trivial-looking one.

[Damiano Testa]

The pow_succ was simply manipulating powers in lean: you should "happen to know" that powers by natural numbers are defined inductively and therefore there should be a lemma about pow_zero and one about pow_succ (and of course others as well!).

[Damiano Testa]

For actually learning number theory, I am not sure, since I learned what I know before using Lean, from people and books: two activities that have changed much in recent years! :lol:

[ccn]

No problem, I managed to find a thoerem I wanted to use:

 theorem nat.modeq_iff_dvd {n a b : ℕ} :
a ≡ b [MOD n] ↔ ↑n ∣ ↑b - ↑a

My goal state looks like this:

function expected at
  nat.modeq_iff_dvd
term has type
  ?m_2 ≡ ?m_3 [MOD ?m_1] ↔ ↑?m_1 ∣ ↑?m_3 - ↑?m_2
state:
n : ℕ,
main : ∀ (n : ℕ), 4 ^ (n + 1) = 4,
twenty_fact : 20 = -4
⊢ 12 ∣ 4 ^ (n + 1) + 20

and my usage of that theorem is

  rw ← (nat.modeq_iff_dvd 12 (4^(n+1)) 20),

am I doing it wrong?

[Reid Barton]

Yes, n a b are implicit parameters (in {}), so don't write them

[ccn]

If I leave off the arguments I get the error: rewrite tactic failed, did not find instance of the pattern in the target expression ↑?m_1 ∣ ↑?m_2 - ↑?m_3

[Reid Barton]

But then, the pattern won't match because there is a + and not a -

[ccn]

Ah I see

[ccn]

So I need to turn my 20 into a - (- 20)

[ccn]

I tried using this:

rw ← neg_neg 20, but it fails because it cannot synthesize the type class

[ccn]

```@[simp]
theorem neg_neg {G : Type u} [add_group G] (a : G) :
--a = a

[Reid Barton]

Oh right because you are using nat

[ccn]

Oh ok, that's because the numbers doesn't have an additive inverse right?

[ccn]

Shouldn't there be a neg_neg that works for what I'm trying to do?

[Damiano Testa]

The arrows ↑ next to ?m_i mean that whatever ?m_i was (a natural number in this case) has been coerced into some other type (an integer in this case). So, if you want to proceed along this path, you should change the divisibility statement about natural numbers to one about integers.

[Note: I guessed the types of ?m_i and ↑?m_i since I've played with these objects, but the error above does not tell you what the types are.]

[ccn]

Ah I see, I'll keep playing with it then to get the right types

[Damiano Testa]

I also have a lingering doubt: if you use -(-20), then -20 is not a natural number and you might run into more issues applying the result above anyway.

[ccn]

You're right, I've changed my twenty fact to look like -20 = 4 (mod 12)

[Damiano Testa]

Does this congruence really work in Lean? What is the type of -20? ℤ?

[ccn]

Damiano Testa said:

Does this congruence really work in Lean? What is the type of -20? ℤ?

This is what my proof is looking like:

theorem induction_12dvd4expnp1p20
  (n : ℕ) :
  12 ∣ 4^(n+1) + 20 :=
begin
  have main : ∀ (n : ℕ), (4^(n+1): zmod 12) = (4: zmod 12) :=
  begin
    intro n,
    induction n with k IH,
    {
      norm_num,
    },
    {
      rw [pow_succ, IH],
      dec_trivial,
    }
  end,
  have twenty_fact : (-20 : zmod 12) = (4 : zmod 12),
    dec_trivial,
  rw ← int.coe_nat_dvd,
  -- rw ← (nat.modeq_iff_dvd),
end

[ccn]

I think i'm having trouble because I forgot that everything has a different type in lean

[ccn]

What do you think the best way forward would be?

[ccn]

I was trying to use rw ← int.coe_nat_dvd, but I think that's making things harder to prove

[ccn]

I also think I'm confused about the difference between MOD and zmod

[ccn]

I have a goal state of

n: ℕ
main: ∀ (n : ℕ), 4 ^ (n + 1) = 4
twenty_fact: -20 = 4
⊢ ↑(4 ^ (n + 1) + 20) = ↑0

where the arrow means that they both have type zmod 12, I want to push the cast through, by using push_cast, but when I do that the goal state changes to

⊢ (0 + 1 + 1 + 1 + 1) ^ (n + 1) + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 = 0

How can I do this properly?

[Damiano Testa]

Below is my solution, in case you are interested!

import data.zmod.algebra

lemma four_eq_one : (4 : zmod 3) = 1 := rfl

theorem induction_12dvd4expnp1p20
  (n : ℕ) :
  12 ∣ 4^(n+1) + 20 :=
begin
  show  4 * 3 ∣ 4 * 4 ^ n + 4 * 5,
  rw ← mul_add,
  refine mul_dvd_mul_left 4 ((zmod.nat_coe_zmod_eq_zero_iff_dvd _ _).mp _),
  simpa [four_eq_one],
end

[Kevin Buzzard]

Oh very nice Damiano! I was working on something but it was longer. Do we have

example (a b n : ℕ) : a ∣ b + a * n → a ∣ b := by sorry

? I was wondering whether it was easier or harder to avoid zmod completely.

[ccn]

Cool, I seemed to have tunnel visioned on getting the coe stuff to work instead of trying a new approach, thanks for new angles on the question

[ccn]

Kevin Buzzard said:

Oh very nice Damiano! I was working on something but it was longer. Do we have

example (a b n : ℕ) : a ∣ b + a * n → a ∣ b := by sorry

? I was wondering whether it was easier or harder to avoid zmod completely.

If that's not in the mathlib, I could help add it in

[Kevin Buzzard]

My solution using it:

import tactic

open nat

lemma dvd_of_dvd_add_mul_left (a b n : ℕ) : a ∣ b + a * n → a ∣ b := sorry

theorem induction_12dvd4expnp1p20
  (n : ℕ) :
  12 ∣ 4^(n+1) + 20 :=
begin
  induction n with k IH,
  { norm_num },
  { rw [pow_succ, succ_eq_add_one],
    apply dvd_of_dvd_add_mul_left _ _ 5,
    exact dvd_mul_of_dvd_right IH 4 },
end

[ccn]

ok, so this would complete it:

lemma dvd_of_dvd_add_mul_left (a b n : ℕ) : a ∣ b + a * n → a ∣ b :=
begin
  refine (nat.dvd_add_left _).mp,
  exact dvd_mul_right a n,
end

[ccn]

Should I add it to mathlib?

[Kevin Buzzard]

You could try! I don't know the naming convention well enough to know whether it's left or right, and it should perhaps be an iff. We might have it; I just couldn't find it. Nice proof!

[Kevin Buzzard]

I guess people might say that it's just an easy combination of two existing lemmas

[ccn]

After studying your proofs the biggest thing that caused me trouble was involving modular arithmetic because I have trouble with coe stuff

[Mario Carneiro]

No one seems to have mentioned norm_fin yet. It should be able to prove (16 : zmod 12) = 4

[ccn]

Kevin Buzzard said:

You could try! I don't know the naming convention well enough to know whether it's left or right, and it should perhaps be an iff. We might have it; I just couldn't find it. Nice proof!

What's the procedure for checking? I've looked here so far and I didn't see it on a first look over: https://leanprover-community.github.io/mathlib_docs/data/nat/modeq.html#nat.modeq

[Kevin Buzzard]

Here's a proof which doesn't use it:

theorem induction_12dvd4expnp1p20
  (n : ℕ) :
  12 ∣ 4^(n+1) + 20 :=
begin
  induction n with k IH,
  { norm_num },
  { rw [pow_succ, succ_eq_add_one, ← nat.dvd_add_left (show 12 ∣ 60, by norm_num)],
    exact dvd_mul_of_dvd_right IH 4 },
end

inspired by your nat.dvd_add_left proof.

[Mario Carneiro]

actually that's a lie, it only works on fin not zmod. Alternatively you can rewrite the goal to 16 % 12 = 4 % 12 and use norm_num

[Kevin Buzzard]

Damiano's is still shorter though :-)

[ccn]

So in Damiano's proof somehow we used the fact : (4 : zmod 3) = 1 so that 4^n would simplify to 1^n ? which in-turn became just 1 ?

[Damiano Testa]

@ccn My line of reasoning was that I always try to get common factors out of the way from congruences and you had a 4 dividing everything in sight. Once that is gone, you are really trying to prove that 4^n = 1 mod 3, which is one step away from 4 = 1 mod 3, which is so trivial that even rfl solves it!

I hope that the thought process helps!

[ccn]

Damiano Testa said:

ccn My line of reasoning was that I always try to get common factors out of the way from congruences and you had a 4 dividing everything in sight. Once that is gone, you are really trying to prove that 4^n = 1 mod 3, which is one step away from 4 = 1 mod 3, which is so trivial that even rfl solves it!

I hope that the thought process helps!

It does help! for the proof of 4^n = 1 mod 3 that probably has induction in it somewhere right?

[ccn]

But rfl is able to do it?

[Kevin Buzzard]

You're going slightly the wrong way. The point is thatsimp knows that 1^n=1. The route is 4^n=1^n=1, not 4^n=4=1.

[Damiano Testa]

There are hidden coercions in the statement: you use the lemma to see that 4^n=1^n, after that simp uses that 1^n=1.

[Damiano Testa]

If you see, in the simpa I explicitly told the simplifier that four_eq_one was a useful lemma. It turned out that I was right! :stuck_out_tongue_closed_eyes:

[Kevin Buzzard]

Can't that be changed to simp? (edit: apparently not!)

[Damiano Testa]

(btw, the a in simpa takes care of another rfl: the proof that 1 + 5 = 0 mod 3.)

[Damiano Testa]

Also, I recently learned that if you use simpa where simp suffices, you get an error.

[Kevin Buzzard]

Oh I see -- you're using the fact that simpa tries refl whereas simp doesn't? Or tries it harder, or something?

[Damiano Testa]

To beat this problem to death, the strategy seems to be that the human makes all the variable useless, and then a combination of simp and rfl should solve your problems.

[Damiano Testa]

Kevin Buzzard said:

Oh I see -- you're using the fact that simpa tries refl whereas simp doesn't? Or tries it harder, or something?

I do not really know what simpa does in this case that simp does not, but it seems to try some form of rfl after doing its simplifications.

[Kevin Buzzard]

def X := ℕ
example : X = ℕ := by simp -- fails
example : X = ℕ := by simpa -- works

simp knows eq_self_iff_true but eq_self_iff_true won't trigger on X = ℕ because simp won't unfold semireducible definitions. I only learnt this recently (when writing my course notes). We all say "rw works up to syntactic equality" but that's not quite true. rw will unfold reducible definitions but will leave semireducible ones alone, and simp inherits this behaviour. The default reducibility of a definition is semireducible. The erw tactic will unfold semireducible definitions too.

[Kevin Buzzard]

@[reducible] def X := ℕ
example : X = ℕ := by simp -- works
example : X = ℕ := by simpa -- fails lol

Is that a bug in simpa??

[Mario Carneiro]

what are you guys doing to my baby

[Mario Carneiro]

that's not how you use simpa

[Kevin Buzzard]

That was why I was so surprised Damiano was using it in the first place!

[Kevin Buzzard]

It's not at all the intended usage; he was using it to do simp, refl

[Mario Carneiro]

aha,simpa uses assumption <|> trivial once it's done its simp work

[Mario Carneiro]

and trivial does several things, including refl

[Kevin Buzzard]

@Damiano Testa the point about simpa is that it's supposed to reduce the goal to an (also simplified) assumption. That's why I initially said "doesn't simp work?" because as far as I could see there were no assumptions!

[Mario Carneiro]

I think simpa should be more aggressive about complaining when you aren't using it on an assumption

[Mario Carneiro]

You should just write simp; trivial if that's what you want

[Johan Commelin]

maybe rename it to simpA :smiley:

[Damiano Testa]

Ok, I did not know that I was abusing the a in simpa so much! :rofl:

[Johan Commelin]

A for Aggressively Asserting Assumptions.

[Mario Carneiro]

well it can do like ring and succeed but passive-aggressively say Try this: simp; trivial, knowing that you can't check in a proof that prints stuff to mathlib

[Damiano Testa]

If I had started with this proof

theorem induction_12dvd4expnp1p20
  (n : ℕ) :
  12 ∣ 4^(n+1) + 20 :=
dvd_trans (mul_dvd_mul_left 4 ((zmod.nat_coe_zmod_eq_zero_iff_dvd (4 ^ n + 5) 3).mp
  (by simpa [four_eq_one]))) dvd_rfl

people may not have noticed the rough behaviour on simpa. :grinning:

[Eric Rodriguez]

I've used simpa for simp; refl a lot too. It's very handy

[Damiano Testa]

theorem induction_12dvd4expnp1p20
  (n : ℕ) :
  12 ∣ 4^(n+1) + 20 :=
dvd_trans (mul_dvd_mul_left 4 ((zmod.nat_coe_zmod_eq_zero_iff_dvd (4 ^ n + 5) 3).mp
  (by simp [four_eq_one]; trivial))) dvd_rfl

no simpas were abused in this proof.

[Bolton Bailey]

ccn said:

Kevin Buzzard said:

You could try! I don't know the naming convention well enough to know whether it's left or right, and it should perhaps be an iff. We might have it; I just couldn't find it. Nice proof!

What's the procedure for checking? I've looked here so far and I didn't see it on a first look over: https://leanprover-community.github.io/mathlib_docs/data/nat/modeq.html#nat.modeq

see docs#coprime_add_mul_right_right for an example of how we did naming conventions for something similar in the past. In that situation there were 8 different lemma possibilities, here there should only be 4.

[Patrick Massot]

Maybe simp should try refl at the end.

[Damiano Testa]

If simp tried refl would the proof above no longer need the call to four_eq_one?
I tried and removing the explicit four_eq_one does not make simp; refl work (nor simp; trivial).

[Vincent Beffara]

Patrick Massot said:

Maybe simp should try refl at the end.

Wouldn't this break all the proofs that end with simp, refl?

[Damiano Testa]

It certainly would, but I think that the question implicitly suggested to fix all the resulting issues. It would be quite a major golf!

[Johan Commelin]

Lower bound:

rg "simp[,;] refl" | wc -l
91

This doesn't count proofs of the form

simp,
refl

that span 2 lines.

[Damiano Testa]

Nor the ones that have simp [lemmas][,;] refl :stuck_out_tongue_wink:

[Damiano Testa]

Also, I imagine that the abusive simpa proofs would fail, since simp would have worked...

[Vincent Beffara]

Maybe simp should try refl at the end, and then if it closes the goal, monkeypatch refl into a noop so that it is ignored :joy:

[Vincent Beffara]

(just kidding of course)

[Reid Barton]

Patrick Massot said:

Maybe simp should try refl at the end.

Or at least refl with reducible transparency (like how rw works, I think?)
I always find it funny when simp simplifies some complicated goal down to 0 = 0 or something and then gets stuck

[Andrew Yang]

simp should call eq_self_iff_true on things like a = a and solve it, which I suppose is quite similar to calling refl with redicible transparency?

[Vincent Beffara]

What does simp [rfl] do?

[Damiano Testa]

Note that

example {α : Type*} {a : α}: a = a := by simp

works. Squeezing you obtain simp only [eq_self_iff_true]. So, I think that simp already uses eq_self_iff_true, at least sometimes.

[Damiano Testa]

In the specific example at hand, without the extra refl, the outcome of simp is to leave 1 + 5 = 0, where all the numbers are in zmod 3.

[Yakov Pechersky]

It shouldn't do refl automatically. In some cases, those refl can be really heavy. Would you imagine it does refl after each simp rewrite, or just at the end? Even if it's just at the end, that means when I'm developing a proof and want to do the simp to squeeze_simp to simp only development step in the middle of a proof, I might trigger really expensive refls that fail anyway.

[Reid Barton]

I agree simp shouldn't do a "full" refl. Am I misremembering which kind of triviality simp likes to get stuck on?

[Henry Pearson]

Hi, I've written a formalisation of avl trees and I am now trying to build some basic theorems for it. My first step was trying to show that well formed trees are closed under all of the given definitions of operations, but this requires quite specific case analysis, so I've ended up with some quite complex tactic states (which lean helps with)!
My issue is now that lean fails to apply the rw tactic in one case and I can't seem to work out why. The relevant parts of the tactic state are:

t_val : α
t_right_left : avlnode α
t_right_val : α
t_right_right : avlnode α

⊢ (((nil.node val nil).node t_val t_right_left).node t_right_val t_right_right).balance_factor ≤ 1

Relevant definitions are:

inductive avlnode (α : Type u)
  | nil                                               : avlnode
  | node (left : avlnode) (val : α) (right : avlnode) : avlnode

/- gives the balance factor of a node -/
def balance_factor : avlnode α → int
  | nil              := 0
  | (node nil _ nil) := 0
  | (node nil _ r)   := (depth r + 1)
  | (node l _ nil)   := - (depth l + 1)
  | (node l _ r)     := (depth r) - (depth l)

def depth : avlnode α → int
  | nil              := 0
  | (node nil _ nil) := 0
  | (node l _ r)     := (int.max (depth l) (depth r)) + 1

And the tactic that lean fails on is

rw balance_factor,

Any help would be much appreciated!!

[Anne Baanen]

It's a bit hard to parse your goal (a good #mwe would help a lot!) but I suspect that the problem is that balance_factor isn't quite compiled to the code you expect. Namely, I assume you want to use the rewrite rule balance_factor (node l _ r) := (depth r) - (depth l), right?

[Anne Baanen]

However, the equation compiler will actually split r into a nil case (for the 4th line) and a node case (for the 5th line). So instead of rw balance_factor you should write cases t_right_right; rw balance_factor.

[Henry Pearson]

Ah I see - that is very helpful!!

[Henry Pearson]

Thanks a lot

[ccn]

How can I do cases on if a number is irrational or not?

[Yaël Dillies]

by_cases irrational x

[Kyle Miller]

It might be convenient to have a variant of docs#irrational_iff_ne_rational for when a number is not irrational. That way you could more quickly split on this sort of or:

lemma irrational_or_rational (x : ℝ) :
  irrational x ∨ ∃ (a b : ℤ), x = a / b :=
begin
  convert classical.em (irrational x),
  simp [irrational_iff_ne_rational],
end

[Yaël Dillies]

Yeah, I'm a bit disappointed to see that irrational is already the negation.

[ccn]

I was trying to use the by_cases irrational x in the following proof, it works out but I'm having trouble proving the two different cases in it:

theorem algebra_others_exirrpowirrrat :
  ∃ a b, irrational a ∧ irrational b ∧ ¬ irrational (a^b) :=
begin
  have sqrt_2 :=  real.sqrt 2,
  by_cases irrational (sqrt_2^sqrt_2),
  {
    have h': ¬ irrational ((sqrt_2^sqrt_2)^sqrt_2) := by sorry,
    exact ⟨(sqrt_2^sqrt_2), sqrt_2, h, irrational_sqrt_two, h'⟩,
  },
  {
     exact ⟨sqrt_2, sqrt_2, irrational_sqrt_two, irrational_sqrt_two, h⟩,
  }
end

Can someone help me get this to work?

[Kyle Miller]

Use let sqrt_2, not have sqrt_2

[ccn]

Kyle Miller said:

Use let sqrt_2, not have sqrt_2

with the proof of ((sqrt_2^sqrt_2)^sqrt_2) I tried using dec_trivial and norm_num to no avail. The proof for that really is that that whole thing will simplify to the number 2, which is not irrational. How would we prove that then?

[Mario Carneiro]

you should rewrite ((sqrt_2^sqrt_2)^sqrt_2) = sqrt_2^(sqrt_2*sqrt_2) and then use the theorem that says sqrt_2*sqrt_2 = 2

[Mario Carneiro]

the let is probably doing no favors here, you should just open real instead if you find it too verbose

[Kyle Miller]

Is there a more direct way to prove foo here?

Code

import data.real.irrational
import analysis.special_functions.pow

open real

lemma foo {x : ℝ} (h : 0 ≤ x) :
  sqrt x ^ (2 : ℝ) = x :=
begin
  convert_to sqrt x ^ 2 = x,
  transitivity,
  swap,
  apply real.rpow_nat_cast,
  norm_num,
  simp [h],
end

theorem algebra_others_exirrpowirrrat :
  ∃ a b, irrational a ∧ irrational b ∧ ¬ irrational (a^b) :=
begin
  by_cases irrational (sqrt 2^sqrt 2),
  { have h': ¬ irrational ((sqrt 2^sqrt 2)^sqrt 2),
    { rw ←real.rpow_mul,
      simp [foo, irrational_iff_ne_rational],
      use [2, 1],
      norm_num,
      exact real.sqrt_nonneg 2, },
    exact ⟨(sqrt 2^sqrt 2), sqrt 2, h, irrational_sqrt_two, h'⟩, },
  { exact ⟨sqrt 2, sqrt 2, irrational_sqrt_two, irrational_sqrt_two, h⟩, }
end
````

[ccn]

Kyle Miller said:

Is there a more direct way to prove foo here?

import data.real.irrational
import analysis.special_functions.pow

open real

lemma foo {x : ℝ} (h : 0 ≤ x) :
  sqrt x ^ (2 : ℝ) = x :=
begin
  convert_to sqrt x ^ 2 = x,
  transitivity,
  swap,
  apply real.rpow_nat_cast,
  norm_num,
  simp [h],
end

theorem algebra_others_exirrpowirrrat :
  ∃ a b, irrational a ∧ irrational b ∧ ¬ irrational (a^b) :=
begin
  by_cases irrational (sqrt 2^sqrt 2),
  { have h': ¬ irrational ((sqrt 2^sqrt 2)^sqrt 2),
    { rw ←real.rpow_mul,
      simp [foo, irrational_iff_ne_rational],
      use [2, 1],
      norm_num,
      exact real.sqrt_nonneg 2, },
    exact ⟨(sqrt 2^sqrt 2), sqrt 2, h, irrational_sqrt_two, h'⟩, },
  { exact ⟨sqrt 2, sqrt 2, irrational_sqrt_two, irrational_sqrt_two, h⟩, }
end

What if we first simplify the stack of powers to 2, then use

@[simp]
theorem int.not_irrational (m : ℤ) :
¬irrational ↑m

[ccn]

Mario Carneiro said:

you should rewrite ((sqrt_2^sqrt_2)^sqrt_2) = sqrt_2^(sqrt_2*sqrt_2) and then use the theorem that says sqrt_2*sqrt_2 = 2

Do you know the lame of the lemma for that first part, I've been having trouble finding it

[Kyle Miller]

docs#real.rpow_mul

[ccn]

Kyle Miller said:

docs#real.rpow_mul

I'm working on that now:

lemma basic : 0 ≤ (2: ℝ) :=
begin
 norm_num,
end

lemma z: ¬ irrational ((sqrt 2^sqrt 2)^sqrt 2) :=
begin
 intro h,
 rw ← (rpow_mul (sqrt_nonneg 2) (sqrt 2) (sqrt 2)) at h,
 rw ← (sqrt_mul basic 2) at h,
 rw sqrt_mul_self basic at h,
 rw sq_sqrt basic at h,
end

that last rw tactic doesn't seem to work though, and I can't figure out why, it gives me this goal state:

rewrite tactic failed, did not find instance of the pattern in the target expression
  sqrt 2 ^ 2
state:
h : irrational (sqrt 2 ^ 2)
⊢ false

[Kyle Miller]

That's where the foo lemma I was asking about came from -- I'd run into the same issue.

[ccn]

Ohh ok.

[Kyle Miller]

The exponent needs to be a nat for that lemma, but it's a real

[ccn]

Can't we make it into one?

[Kyle Miller]

That's what I did in the foo lemma, and my question is whether there's a simpler way to do this.

[Kyle Miller]

It's likely I just don't know my way around Lean's reals, but maybe it's a random oversight that there's no direct lemma yet.

[ccn]

I get your reasoning more now

[ccn]

Kyle Miller said:

The exponent needs to be a nat for that lemma, but it's a real

I learned how to do this:

lemma basic_2 : (sqrt 2)^(2 : ℕ) = (sqrt 2)^(2 : ℝ) :=
begin
  norm_cast,
end

after that, we can use the lemma. It feels hacky but it does work.

[Damiano Testa]

Kyle Miller said:

Is there a more direct way to prove foo here?

This also works:

lemma foo {x : ℝ} (h : 0 ≤ x) :
  sqrt x ^ (2 : ℝ) = x :=
begin
  have : sqrt x ^ ((2 : ℕ) : ℝ) = x, { rw [real.rpow_nat_cast, sq_sqrt h] },
  exact_mod_cast this,
end

[Hossam Karim]

I am learning lean and trying to prove the associativity of ++ on List

example (xs ys zs : List a):
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by
  induction xs with
  | nil => simp
  | cons h t ih =>
  rw [ih]

Now lean complains that it cannot do the rewrite:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  t ++ (ys ++ zs)
case cons
a : Type ?u.246
ys zs : List a
h : a
t : List a
ih : t ++ (ys ++ zs) = t ++ ys ++ zs
⊢ h :: t ++ (ys ++ zs) = h :: t ++ ys ++ zs

Although my understanding is that t ++ (ys ++ zs) can be rewritten in the goal. Am I missing something here?

[Alex J. Best]

I think the brackets aren't where you think they are, if you hover over the info-view in vscode the highlighting will show that the goal is really like ⊢ (h :: t) ++ (ys ++ zs) = (h :: t) ++ ys ++ zs

[Alex J. Best]

The lemma List.cons_append will help you finish the proof from here though

[Hossam Karim]

Understood. Thanks a lot @Alex J. Best

[ccn]

I'm working through this calc block, so far everything seems good aside from the two ring_nf blocks which are complaining to me:

theorem induction_sumkexp3eqsumksq
  (n : ℕ) :
  ∑ k in finset.range n, k^3 = (∑ k in finset.range n, k)^2 :=
begin
  symmetry,
  induction n with j IH,
  {
    refl,
  },
  {
    calc (∑ (k : ℕ) in finset.range j.succ, k)^2 = ((∑ (k : ℕ) in finset.range j, k) + j )^2 : by rw finset.sum_range_succ  -- rewrite summation
   ... = (∑ (k : ℕ) in finset.range j, k)^2 + 2 * (∑ (k : ℕ) in finset.range j, k) * j + j^2 : by rw add_sq _ _ -- (a + b)^2
   ... = (∑ (k : ℕ) in finset.range j, k)^2 + 2 * (j * (j-1)/2) * j + j^2 : by rw finset.sum_range_id j -- sum = j*(j-1)/2
   ... = (∑ (k : ℕ) in finset.range j, k^3) + 2 * (j * (j-1)/2) * j + j^2 : by rw IH
   ... = (∑ (k : ℕ) in finset.range j, k^3) + j^2 * (j-1) + j^2 : by ring_nf -- 2 * ( ... )/2 = ( ... )
   ... = (∑ (k : ℕ) in finset.range j, k^3) + j^3 : by ring_nf -- (j +1)^2 (j+1) = (j+1)^3
   ... = (∑ (k : ℕ) in finset.range j.succ, k^3) : by rw ← finset.sum_range_succ, -- by the definition of summation
  }
end

any tips on which tactics I should be using there?

[ccn]

I simply get "tactic failed, there are unsolved goals":
image.png

[Alex J. Best]

The problem with this step is that it actually requires an argument, as this is nat division cancellation requires that j*(j-1) is even, which of course it is, but even that requires a short argument, I doubt there is any tactic in mathlib that will just do this step. I recommend you break this step out as a separate lemma

lemma aux (j : ℕ) : 2 * (j * (j-1)/2) * j = j^2 * (j-1) := sorry

[ccn]

So my aim with this new lemma would be to use this right?

@[simp]
theorem div_mul_cancel {G₀ : Type u_2} [group_with_zero G₀] (a : G₀) {b : G₀} (h : b ≠ 0) :
(a / b) * b = a

[Alex J. Best]

Unfortunately not, nat division is not group with zero division, you probably need docs#nat.mul_div_cancel'

[ccn]

Alex J. Best said:

The problem with this step is that it actually requires an argument, as this is nat division cancellation requires that j*(j-1) is even, which of course it is, but even that requires a short argument, I doubt there is any tactic in mathlib that will just do this step. I recommend you break this step out as a separate lemma

lemma aux (j : ℕ) : 2 * (j * (j-1)/2) * j = j^2 * (j-1) := sorry

Oh and your reasoning here is that division is defined as this

 def nat.div (x y : ℕ) :
ℕ

so you're not allowed to divide the natural 1 by the natural 2, because that would create something that's not a natural right?

[Reid Barton]

Note that this is the cost of totalizing /, if / took a proof of divisibility as an argument, then the proof would be contained in the statement of finset.sum_range_succ and then reasoning like the kind you are doing here becomes automatable by a tactic.

[Alex J. Best]

Yes @ccn, lean gets around this by definition nat division to be the floor of the actual value, and in the cases where you have divisibility you have to often manually supply this fact

[ccn]

I see

[ccn]

This would be the theorem I'm looking for right? (docs#nat.even_succ)

 theorem nat.even_succ {n : ℕ} :
even n.succ ↔ ¬even n

or is there one that's even closer?

[Alex J. Best]

In general its best to avoid introducing division as much as possible, it looks like in this case using docs#finset.sum_range_id_mul_two instead of finset.sum_range_id a few lines above would save you a lot of work

[ccn]

Thanks Alex I always learn a lot from you

[ccn]

One last thing, the calc block is still having an issue with the last ring_nf here:

    calc (∑ (k : ℕ) in finset.range j.succ, k)^2 = ((∑ (k : ℕ) in finset.range j, k) + j )^2 : by rw finset.sum_range_succ  -- rewrite summation
   ... = (∑ (k : ℕ) in finset.range j, k)^2 + 2 * (∑ (k : ℕ) in finset.range j, k) * j + j^2 : by rw add_sq _ _ -- (a + b)^2
   ... = (∑ (k : ℕ) in finset.range j, k)^2 +  (∑ (k : ℕ) in finset.range j, k) * 2 * j + j^2 : by ring
   ... = (∑ (k : ℕ) in finset.range j, k)^2 + (j * (j-1)) * j + j^2 : by rw finset.sum_range_id_mul_two j -- sum = j*(j-1)/2
   ... = (∑ (k : ℕ) in finset.range j, k^3) + (j * (j-1)) * j + j^2 : by rw IH
   ... = (∑ (k : ℕ) in finset.range j, k^3) + j^2 * (j-1) + j^2 : by ring_nf -- 2 * ( ... )/2 = ( ... )
   ... = (∑ (k : ℕ) in finset.range j, k^3) + j^3 : by ring_nf -- (j +1)^2 (j+1) = (j+1)^3
   ... = (∑ (k : ℕ) in finset.range j.succ, k^3) : by rw ← finset.sum_range_succ, -- by the definition of summation

Do you know why it can't do this one?

[ccn]

Wouldn't all it have to do j^2 * (j - 1) + j^2 = j^2 *( j - 1 + 1) = j^2 * j = j^3, can it not handle that?

[Alex J. Best]

This is due to natural number subtraction being a bit tricky (similar to division) the possibility that j = 0 in which case j-1 is also 0, but this is not usual in rings.
Splitting on those cases seems to work though with thisa instead

by cases j; norm_num; ring_nf

[ccn]

Alex J. Best said:

This is due to natural number subtraction being a bit tricky (similar to division) the possibility that j = 0 in which case j-1 is also 0, but this is not usual in rings.
Splitting on those cases seems to work though with thisa instead

by cases j; norm_num; ring_nf

I see. When you do that type of syntax does that mean in case one, norm_num can solve it and in the second case ring_nf can solve it?

[Alex J. Best]

It just means try norm_num on all goals, then try ring_nf on all remaining goals. It has the same effect in the end as what you said except the second goal gets norm_num then ring_nf applied

[Alex J. Best]

The syntax for what you said is by cases j; [norm_num, ring_nf], and in fact it does work in this case too

[ccn]

I think that also makes sense because in the first case it's just a whole bunch of zero's being multiplied and the second case there's at most one zero there right?

Also was this causing a problem (having both j and j-1 as zero) because a ring can't have two zeros'?

[Alex J. Best]

The lemma m - n + n = m is always true in rings and is true in nat when m >= n. But as nat is not a ring (only a semiring, for this reason) ring_nf doesn't know it can apply that lemma (and even if it did it would have to find a way to prove the condition. By doing cases we get one case where everything is zero and similifies and another one where the subtraction simplifies with succ and dissapears

[ccn]

So I'm looking to prove this theorem:

theorem induction_pprime_pdvdapowpma
  (p a : ℕ)
  (h₀ : 0 < a)
  (h₁ : nat.prime p) :
  p ∣ (a^p - a) :=
begin
  sorry,
end

I've come up with the proof on paper, which is first change what we want to prove to a^p - a ≡ 0 (mod p) (since it's equivalent) then note that from fermats little theorem we have a^(p-1) ≡ 1 (mod p) and then to re-write a^p = a^(p-1) * a, use that fact to go from a^p - a ≡ 0 (mod p) to a^(p-1) * a - a ≡ 0 (mod p) to 1 * a - a ≡ 0 (mod p) to 0 ≡ 0 (mod p) which is easy to prove.

I've done some research on the main theorem (fermats little theorem) and found this theorem

section
variables [group_with_zero K] [fintype K]

lemma pow_card_sub_one_eq_one (a : K) (ha : a ≠ 0) : a ^ (q - 1) = 1 :=
calc a ^ (fintype.card K - 1) = (units.mk0 a ha ^ (fintype.card K - 1) : Kˣ) :
    by rw [units.coe_pow, units.coe_mk0]
  ... = 1 : by { classical, rw [← fintype.card_units, pow_card_eq_one], refl

(Note I don't think this is the same as the one you find on mathlib today: https://leanprover-community.github.io/mathlib_docs/field_theory/finite/basic.html#zmod.pow_card_sub_one_eq_one because the project I'm working on uses a different version).

I'm a little confused on how to call this theorem, but it would be great if someone could help me use it to prove a^(p-1) = 1 mod p .

Thanks

[Kevin Buzzard]

@ccn re your earlier question: I find these much easier if you just work over a field instead:

import tactic

open_locale big_operators

theorem induction_sumkexp3eqsumksq
  (n : ℕ) :
  ∑ k in finset.range n, k^3 = (∑ k in finset.range n, k)^2 :=
begin
  suffices : ∑ k in finset.range n, (k : ℚ)^3 = (∑ k in finset.range n, (k : ℚ))^2,
    assumption_mod_cast,
  have : (∑ k in finset.range n, (k : ℚ)) = n * (n - 1) / 2,
  { induction n with d hd,
    { simp },
    { simp [finset.sum_range_succ, hd],
      ring }
  },
  rw this, clear this,
  induction n with j IH,
  { simp },
  { simp [finset.sum_range_succ, IH],
    ring }
end

[ccn]

Thanks for the new view on it! It looks cleaner

[ccn]

I've decided I'd like to try solving some topology exercise in lean:

I'm going to start with this first question I've highlighted here,

image.png

I've been trying to understand the docs for topology and I got it up to this point:

import topology.basic

theorem open_set_for_each (X : topological_space) (h : A ⊂ X) (h₁ : ∀ x ∈ A, ∃ U, x ∈ U ∧ U ⊂ A) : is_open X U :=
begin
end

In know there are some things that are rough with this theorem so I'm hoping I can get some tips to fix it up (since it doesn't even compile), thanks!

[Kevin Buzzard]

Maybe you want to read the error message and deal with it. What is it?

[ccn]

topological_spaces.lean:3:77
don't know how to synthesize placeholder
context:
X : ⁇,
h : ⁇ ⊂ X,
x : ⁇,
H : x ∈ ⁇
⊢ Type ?
topological_spaces.lean:3:94
unknown identifier 'A'
topological_spaces.lean:3:109
unknown identifier 'U'

[ccn]

When it says unable to synthesize placeholder what exactly does that mean?

[Kevin Buzzard]

So Lean is saying "what the heck is this A that you just randomly started talking about without ever mentioning its type?"

[Kevin Buzzard]

and judging by the tactic state it doesn't know what X is either

[Kevin Buzzard]

Why don't you take a look at the topology workshop I did in my formalising mathematics course last year?

[ccn]

Ok, I'll try to understand the docs a little more The main definition is the type class topological space α which endows a type α with a topology. So pretty much I just want X to be some arbitrary set, and then the topology is a collection of subsets of X with those properties

[ccn]

So my type a should be X right?

[Kevin Buzzard]

No, you want X to be a type. Lean does type theory.

[ccn]

Ah right, no sets...

[Kevin Buzzard]

There's how to do basic topology https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/src/week_4/Part_C_topology.lean

[Kevin Buzzard]

and there's the blog post explaining what's going on in that Lean file https://xenaproject.wordpress.com/2021/02/10/formalising-mathematics-workshop-4/

[ccn]

Ok, I will check those out right now. One thing I want to get out of the way first though, if I want to say collection of subsets of X in type theory, what would be the type of that?

[Kevin Buzzard]

set (set X)

[Kevin Buzzard]

Checkout the the definition of docs#topological_space

[ccn]

Kevin Buzzard said:

There's how to do basic topology https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/src/week_4/Part_C_topology.lean

I started working through this repo a little bit, so now I have a new question, at one point in the groups file, we had defined the following

@[simp] theorem mul_one : a * 1 = a :=
begin
  apply mul_eq_of_eq_inv_mul,
  symmetry,
  exact mul_left_inv a,
end

@[simp] theorem mul_right_inv : a * a⁻¹ = 1 :=
begin
  apply mul_eq_of_eq_inv_mul,
  symmetry,
  exact mul_one a⁻¹,
end

attribute [simp] one_mul mul_left_inv mul_assoc

Then later in the file you supply this proof

@[simp] lemma inv_mul_cancel_left : a⁻¹ * (a * b) = b :=
begin
  rw ← mul_assoc, -- the simplifier wouldn't do it that way
                  -- so we have to do it manually
  simp, -- simplifier takes it from here,
        -- rewriting a⁻¹ * a to 1 and then 1 * b to b
end

The simplifier can't do this because when it has lemmas of the form A = B then it is only allowed to replace A's with B's, so with mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
it couldn't have helped us in that lemma due to this reason, so that's why we need the initial rewrite? If we had the other version of mul_assoc where LHS is swapped with RHS it would be a problem because the simplifier would get caught in a loop right?

[Kevin Buzzard]

Right -- with these proofs at the beginning of the theory you are often rewriting in both directions and you can't have both A=B and B=A as simp lemmas

[ccn]

What is the section of the docs which has the definitions for infinite summations and products?

[Kyle Miller]

docs#tsum (found it by looking at https://leanprover-community.github.io/undergrad.html)

[ccn]

docs#tprod

[ccn]

Oh maybe it's this? https://leanprover-community.github.io/mathlib_docs/data/tprod.html#list.tprod

[Reid Barton]

unlucky

[ccn]

I'm just trying to write this: image.png

[Reid Barton]

right, tprod definitely seems like a thing that should exist but I don't know if it does

[Kevin Buzzard]

Oops

[Kevin Buzzard]

Take logs, use tsum, and then exp? :blush:

[Kevin Buzzard]

Presumably if one of the terms in a general product is 0 then the classical convention that the product "diverges to zero" can be replaced with lean's convention that it converges to a junk value, namely zero.

[ccn]

I recall that in order to say that a is the largest number satisfying a proposition P we could write ∀ x, a < x → ¬ P(x) Is that the way we would write it in lean as well, or is there a faster way?

[Yaël Dillies]

What about docs#is_greatest?

[Damiano Testa]

@ccn in your formula, there is a missing assumption: you presumably want ˋP aˋ to also hold! (Note that ˋis_greatestˋ includes this.)
[My backticks appear to have broken.]

[ccn]

I haven't worked with sets much in lean, could someone show me how we can use is_greatest to prove something simple like a theorem which proves that 3 is the largest odd integer less than 5 ?

[Yakov Pechersky]

does this work?

example : is_greatest {x : nat | odd x /\ x < 5} 3 := dec_trivial

[ccn]

Yeah it does make sense, thanks I see how to use it now!

[ccn]

I want to make a statement for a_1, ... ,a_n which are real numbers where ∑ k in finset.range n, a_k = ... what's the best way to go about that?

[ccn]

So far I've only had a finite number of parameters to my theorems/functions

[Yakov Pechersky]

Where did you get your various a_'s from? There's probably a better way to phrase what you want than just having 1 to n.

[ccn]

Yakov Pechersky said:

Where did you get your various a_'s from? There's probably a better way to phrase what you want than just having 1 to n.

Trying to write this out: image.png

[Eric Rodriguez]

I guess the lean way to state that is with an indexing set {ι : Type*} [fintype ι] and two functions a b : ι → ℝ (E: thanks Kyle!)

[Kyle Miller]

(small typo: it should be [fintype ι])

[ccn]

I tried that out, but I'm getting still some issue:

import data.real.basic

open_locale big_operators

theorem cauchy {l : Type*} [fintype l] (a b : l → ℝ) (n : ℕ) :
  (∑ i in finset.range (n + 1) , (a i) * (b i) )^2 ≤ (∑ i in finset.range (n + 1), (a i) ^2) * (∑ i in finset.range (n + 1), (b i) ^2)

[ccn]

type mismatch at application
  a i
term
  i
has type
  ℕ : Type
but is expected to have type
  l : Type ?

[ccn]

So the finset.range thing is wrong because it 's producing a natural number?

[ccn]

It's like I need to produce n distinct indices

[Eric Rodriguez]

Σ i : ι, a i (also I'm writing ι for iota instead of l but it doesn't matter ;b)

[Eric Rodriguez]

you're trying to plug in a nat to a function that doesn't take nats

[ccn]

Eric Rodriguez said:

Σ i : ι, a i (also I'm writing ι for iota instead of l but it doesn't matter ;b)

Ah ok, I understand it now. And this represents the same thing as the cauchy inequality because the l is a fintype so it can be labelled 1 to n, for some n ?

[Yaël Dillies]

Yes, but also you never need to. On paper, we think of sums as an iterative process. We take the first element, add the second, the third...

[Yaël Dillies]

This is not at all what's done in mathlib. Instead, we sum in all orders at once, and commutativity of addition tells us that we always ended up with the same result.

[Yaël Dillies]

So we can get from "sum of elements of a list" to "sum of elements of a set".

[Yaël Dillies]

In practice, the VM chooses an arbitrary order to do the calculation, but that's not so important to the concept.

[ccn]

If I have a polynomial like (x^2 + 1) * (x^2 + 3) = x^4 + 4^2 + 3 (but assume I was just given x^4 + 4^2 + 3), I want to talk about the product of all the complex roots of that polynomial (so in that case +-i and +-sqrt(3)*i), is there a way to get this product in general from a polynomail using lean?

[ccn]

I found this which gives me the roots: https://leanprover-community.github.io/mathlib_docs_demo/data/polynomial/ring_division.html#polynomial.roots

[ccn]

Now I need to somehow filter out the complex ones and multiply them all together...

[Eric Rodriguez]

docs#multiset.prod, docs#multiset.filter, docs#complex.im may be helpful

[ccn]

So your suggestion is to check if complex.im r is non-zero (where r is the root is non-zero) as a way to filter the roots right?

[ccn]

Is it possible to define a polynomial like x^4 + 4x^2 + 3 and then get it's roots in lean, or is it just on arbitrary polynomials?

[Mario Carneiro]

If it's a specific polynomial you can just factor it

[ccn]

I think I found a way to do it, if I start with a specific polynomial P, than I can do {x : ℂ | P(x) = 0} to get the complex roots...

[ccn]

For doing a finset prod, is this the cleanest way you know of finset.prod {1, 2, 3} (λ x, x) = 6?

[David Landsberg]

(deleted)

[David Landsberg]

(deleted)

[Anne Baanen]

For small numbers, you can just let it directly compute:

import algebra.big_operators.basic

open_locale big_operators

example : finset.prod ({1, 2, 3} : finset ℕ) (λ x, x) = 6 :=
rfl

[Anne Baanen]

For larger computations, the norm_num tactic is usually faster. There are enough lemmas available here that you can just replace rfl with by norm_num.

[Eric Rodriguez]

ccn said:

I think I found a way to do it, if I start with a specific polynomial P, than I can do {x : ℂ | P(x) = 0} to get the complex roots...

just remember that Lean will also give you the real roots in this too :) also you'll want to use a multiset if you want to count the roots with multiplicity

[ccn]

Is there an easy way to talk about the sum of the digits of a number in lean?

[Yaël Dillies]

Use docs#nat.to_digits and docs#list.sum

[ccn]

Given a specific polynomial like 83x^4 + -3x^3 + 238x^2 + 99999x + 42 how do I get lean to talk about the cofficient on the term x^2 ?

[Yaël Dillies]

docs#polynomial.coeff ?

[ccn]

Yeah that would work, I'm trying to figure out how to define 83x^4 + -3x^3 + 238x^2 + 99999x + 42 as a specific polynomial so I can use the .coeff is that even possible?

[Yaël Dillies]

Yes of course. You can use docs#polynomial.C and docs#polynomial.X

[Reuben Dunn]

Hello all! I'm new here, and I'm a beginner in this field. I was wondering if there's somewhere appropriate for me to post "stupid" questions about basic concepts in automated theorem proving and proof verification, which might not be about Lean specifically. I don't want to spam this community with topics that aren't relevant, but I'm not sure where the best place for that type of thing is.

[Johan Commelin]

@Reuben Dunn You might want to try out the brand new https://proofassistants.stackexchange.com/

[Reuben Dunn]

Johan Commelin said:

Reuben Dunn You might want to try out the brand new https://proofassistants.stackexchange.com/

Awesome, that looks right up my alley. I'm surprised because I tried searching for something like that recently and didn't find this! So it really is brand new.

[Mario Carneiro]

That's not to say that such questions are off topic here though

[ccn]

Johan Commelin said:

Reuben Dunn You might want to try out the brand new https://proofassistants.stackexchange.com/

Is this appropriate for questions relating to proving specific statements and questions relating to mathlib?

[Johan Commelin]

I don't know... I guess that's being worked out during the current beta phase...

[Julian Berman]

There's also this thing: https://proofassistants.meta.stackexchange.com/

[Julian Berman]

Which you can ask that question on if you want some assurance -- but yeah you could just ask it if you're more comfortable there and if someone closes it big deal.

[Stuart Presnell]

Whether or not it's appropriate for PASE, if it's a question specifically about mathlib you might get an answer more quickly by asking here on Zulip.

[ccn]

I want to write a summation like image.png in lean, how can I do it?

[Anne Baanen]

You can use docs#finset.sum, which has \sum notation if you add open_locale big_operators

[ccn]

I'm thinking I'll have to do a double summation like ∑ i in finset.range n, ∑ j in {k : ℕ | i + k = n}, ... would that be best?

[Anne Baanen]

So your example would look something like:

import algebra.big_operators.basic
open_locale big_operators

example : ∑ (i : fin n) (j : fin n), if (h : (i + j : ℕ) = n) then some_function i j else 0

[ccn]

Are those first two little n's supposed to be the N ?

[ccn]

nevermind, I found fin in the docs now.

[ccn]

thanks Anne!

[Anne Baanen]

It would be neat if we could add (h : i + j = n) as indices to our sum, rather than having to use an if-then-else, but apparently fintype is defined only for Types, not Props. :(

[Kyle Miller]

That bound is known as docs#finset.nat.antidiagonal

[ccn]

I had to write the if statement like if (i + j : ℕ) = n then some_function i j else 0 (without the h)

[Kyle Miller]

I had just been using it for

theorem fib_eq_sum_choose_antidiagonal : ∀ (n : ℕ),
  (n + 1).fib = ∑ p in finset.nat.antidiagonal n, nat.choose p.1 p.2 :=
sorry

[ccn]

I think you can also use it like: ∑ i j in (finset.nat.antidiagonal n), something i j

[Yury G. Kudryashov]

I don't think that you can use it this way.

[ccn]

Is there an easy way to get the units place of a real number?, so far Ive found nat.to_digits but that's only for naturals, any idea on what I can use there?

[Yaël Dillies]

Do you mean the floor (not the unit place for negative reals)? docs#int.floor or docs#nat.floor depending on your use.

[ccn]

Yeah what I know is that the number is a positive real like 128.232323... and I want to get the ones place to get the answer 8

[ccn]

When I try this out #eval nat.floor (3.2 : ℝ) I just get

code generation failed, VM does not have code for 'classical.choice'

[Kyle Miller]

Reals aren't computable, so #eval won't work for that

[Kyle Miller]

norm_num should probably know how to compute this:

import data.real.basic
import tactic

example : nat.floor (3.2 : ℝ) = 3 :=
begin
  norm_num, -- should work
end

[Kyle Miller]

This works though:

example : nat.floor (3.2 : ℝ) = 3 :=
begin
  rw nat.floor_eq_iff; norm_num,
end

[Yaël Dillies]

So what you want is nat.floor x % 10

[ccn]

Thanks that works well!

[ccn]

If I wanted to figure out the number of terms after simplification of the expansion of (8* x^2 + 4 * x* y + 3 * y^2)^n would there be a nice way to do it in lean?

[Kevin Buzzard]

It's 2n+1, you don't need lean. What's your actual question? Is n a variable? Do you want a formula or an algorithm etc

[Callum Cassidy-Nolan]

I'm trying to state and then prove that it's equal to that in lean, so I'm having trouble writing the statement I'm trying to prove

[Kevin Buzzard]

I guess there would be a way to do this. A polynomial is stored as a function with finite support and you just want to count the size of the support.

[Kevin Buzzard]

import data.mv_polynomial

def card_support {σ : Type} (R : Type) [comm_ring R] (f : mv_polynomial σ R) : ℕ :=
begin
  delta mv_polynomial at f,
  delta add_monoid_algebra at f, -- f is now a finsupp
  exact f.support.card,
end

There's probably a more idiomatic way to do it.

[Callum Cassidy-Nolan]

Ah ok, thanks for showing me that!

[Kyle Miller]

It looks like f.support.card works without all that unfolding.

def card_support {σ : Type} (R : Type) [comm_ring R] (f : mv_polynomial σ R) : ℕ :=
f.support.card

[Kevin Buzzard]

Oh great! mv_polynomial.support exists :-)

[Callum Cassidy-Nolan]

So I've been experimenting with the multivariable polynomial API, and I've figured some things out, but I'm having trouble understanding how to evaluate them properly, my first try was this:

theorem trying_it
  (P : mv_polynomial (fin 4) ℝ)
  (h₀: P = X 0 + X 1 + X 2 + X 3) :
   P.eval 1 2 3 4 = 10 := sorry

I think my problem is that I don't fully understand the definitions together:

 noncomputable def mv_polynomial.eval {R : Type u} {σ : Type u_1} [comm_semiring R] (f : σ → R) :
mv_polynomial σ R →+* R

I don't really understand what R →+* R means (the + and *) , but if I understand that right, I first need to build some type of function which maps from sigma into the real numbers (for my case), so that function encodes my 1 2 3 4 ? Is that right?

[Callum Cassidy-Nolan]

Also is it correct to say that sigma is acting like an index set/index type ? image.png

[Reid Barton]

P.eval 1 2 3 4 seems very optimistic to me

[Reid Barton]

Callum Cassidy-Nolan said:

I don't really understand what R →+* R means (the + and *) , but if I understand that right, I first need to build some type of function which maps from sigma into the real numbers (for my case), so that function encodes my 1 2 3 4 ? Is that right?

Yes, that's f

[Reid Barton]

I think you could use https://leanprover-community.github.io/mathlib_docs/data/matrix/notation.html for this

[Reid Barton]

Your σ is fin 4

[Yakov Pechersky]

"mv_polynomial.eval ![1, 2, 3, 4] P" if you import finvec notation

[Daniel Packer]

If I have an ite (i=j) 1 0 built up from using classical to get decidability on the type of i, is there a way I can compare it to an ite (i=j) 1 0 built from using an instance like [decidable (i=j)]?

[Anne Baanen]

The tactic#congr family might help here

[Daniel Packer]

Nice! That did it. Thanks a ton!

[Eric Rodriguez]

usually this means that a lemma statement went wrong somewhere

[Eric Rodriguez]

so, if you don't mind me asking, does the classical ite come from your code or mathlib?

[Daniel Packer]

It came from my code. I introduced a open_locale classical because the linter told me to replace all instances of [decidable_eq] with classical in the proof

[Daniel Packer]

Okay, I figured out what was probably wrong. I had first inserted classicals in the tactics of proofs on an as-needed basis, but later decided to just open_locale classical, but in this one proof I had forgotten to take out the classical tactic.

[Yakov Pechersky]

the two are not interchangeable. open_locale classical changes the statements of all your definitions and lemmas. classical as the tactic only changes the proofs.

[Yakov Pechersky]

You want the latter, not the former. The former restricts your definitions and lemmas to be only valid over things that are classically defined, instead of things that are either classically or decidably defined.

[Yakov Pechersky]

Whether or not you rely on decidability inside the proof doesn't matter for the proof itself, which is what the "classical" tactic does.

[Daniel Packer]

Ah, I see. So if I have a term-mode proof, should I turn it into a tactic-mode proof so that I can hit it with the classical tactic?

[Daniel Packer]

Separately, doing this breaks the statements of some theorems with ite in them, is there a way to fix that without putting in [decidable_eq]s into the hypothesis?

[Yaël Dillies]

The way to fix them is to add decidable_eq hypotheses.

[Daniel Packer]

Okay, previously having decidable_eq in the hypothesis got the mathlib linter mad at me. Is there a way to tell which decidable_eqs are okay to have? Is it exactly when you need it to make the theorem statement work?

[Yaël Dillies]

Yes, exactly! :smiley:

[Yaël Dillies]

The idea is that the decidable instances appearing in the type should be general while the ones appearing in the proof can be whatever. And you want to have as few decidability hypotheses as possible, so any that doesn't appear in the type should be declared in the proof.

[Yaël Dillies]

Note the difference between def and lemma here. Because lemma forgets the proof as soon as it's done, you can poison it with classical as much as you want. If you do that in a definition however, you'll make it noncomputable.

[Yakov Pechersky]

More details: an if-then-else that branches on a condition P must have that P is decidable! Otherwise you can't actually consider the two branches

[Daniel Packer]

Ah nice! This makes so much sense. Thank you all for the explanation.

[Yaël Dillies]

I should also add that usually some goals within a def are proofs, and those behave just as in a lemma, so you can classical-poison them as much as you want even though they are "part of a def".

[Yaël Dillies]

The important distinction is Type-valued vs Prop-valued goal.

[Daniel Packer]

Right! So if I want a Prop, then I do the classical tactic, and if I want to make a (computable) definition, then I should use decidable_eq.
(And I should never use open_locale classical?)

[Yaël Dillies]

open_locale classical is the mathematician's cheat code. Short term gain, long-earned pain.

[Eric Rodriguez]

I wish finsupp could be fixed :(

[Yaël Dillies]

Couldn't we follow the same idea as for dfinsupp? There it seems to work well.

[Stuart Presnell]

What’s wrong with finsupp? Is it just that the use of open_locale classical would be a big chore to unwind?

[Yaël Dillies]

No, not quite. It would indeed be a big chore to unwind, but mostly the definition of finsupp is such that it requires an awful lot of decidability. dfinsupp circumvents the problem by having a more flexible representation of the support.

[Kevin Buzzard]

What's wrong with finsupp is that it's hard for mathematicians to use because it's constructive and mathematicians have no idea what decidable equality means because in maths it's an axiom. In fact nobody likes finsupp because it's too constructive for the classical people and somehow not constructive enough for the constructive people, is my understanding of it (I remember Reid bashing it from a constructivist point of view at some point in the past). One day I'll write a purely classical finsupp :-) It's just f : X -> Y and the hypothesis that the preimage of univ - 0 is set.finite.

[Eric Rodriguez]

the main reason I care about it is that currently we have to do ugly hacks to make the nat multiplicative inductions computable; I don't much care mathematically but it just seems to me that they should be computable in principle

[Kevin Buzzard]

So there in your link is the claim that finsupp is noncomputable, and yet it uses finset instead of set.finite so it's not classical either.

[Reid Barton]

Yeah finsupp is actually wrong in multiple ways, if you're expecting finsupp X R to be the free R-module on X.

[Reid Barton]

dfinsupp is also wrong, but less so.

[Callum Cassidy-Nolan]

I've just written out this question :

import topology.basic

theorem open_set_for_each
  (X : Type)
  [topological_space X]
  (A : set X)
  (h₁ : ∀ x ∈ A, ∃ (U : set X), x ∈ U ∧ U ⊂ A) :
  is_open A :=
begin
  sorry
end

When I look at the topology api I see this: image.png

How does is_open know I'm talking about X ?

Also, what does it mean when I write X : Type ? Am I just stating that it's an aribitrary type? I have trouble understanding Type u and all that stuff.

[Mario Carneiro]

When writing code for mathlib you usually want to use X : Type* instead of X : Type

[Mario Carneiro]

X : Type means X is a type in the lowest universe; X : Type* means X is a type in any universe

[Mario Carneiro]

you don't need to know much about universes other than to know there is more than one and so X : Type is putting a restriction on users of your theorem. In 98% of cases you can just write Type* instead of Type and pay no more heed to it

[Callum Cassidy-Nolan]

I am a little curious about the universes, I'm not sure what those are but I know that there are different type levels, like Type 0, Type 1 and so on, why are there so many?

[Callum Cassidy-Nolan]

Also what is the difference between X : Type* and X : Type u

[Mario Carneiro]

Ideally there would be only one universe, the type of all types. Unfortunately Russell and Girard proved this is inconsistent, so the type of all types has to live in a bigger type

[Mario Carneiro]

So in lean Type 0 : Type 1 and Type 1 : Type 2 and so on

[Mario Carneiro]

You will almost never see the higher universes show up in practice, but they are theoretically important

[Mario Carneiro]

X : Type* is the same as X : Type _, which is to say X has Type "lean figure it out"

[Callum Cassidy-Nolan]

Ok, so the goal is that we want to say that X is an arbitrary type, but there's no type we can put on the underscore X : _ to make that happen (based on Russel and Girard) ?

[Mario Carneiro]

usually it will end up being a universe variable, so you get X : Type u with u being a universe parameter to the theorem

[Callum Cassidy-Nolan]

So instead we build a tower of types that are increasing and then let it be one of the levels in the tower?

[Mario Carneiro]

Right, we get a family of theorems, one for each universe we want to instantiate X to

[Callum Cassidy-Nolan]

Do we ever use specific levels?

[Callum Cassidy-Nolan]

it seems like we have infinite of them just to solve the paradox.

[Mario Carneiro]

Concrete types usually have the lowest possible level we can assign to them. So for example nat : Type 0

[Callum Cassidy-Nolan]

What would have gone wrong if we did nat : Type * ?

[Mario Carneiro]

and if A : Type u and B : Type v then A ⊕ B : Type (max u v)

[Mario Carneiro]

If we did nat : Type u, then it wouldn't really be one type, it would be a family of types, denoted nat.{u} : Type u. This is fine, but lean will often not be able to solve for u when you use nat in a theorem so users will have to pay closer attention to the universes

[Callum Cassidy-Nolan]

So Type u is the type of families of Type u ??

[Mario Carneiro]

so as a result, this technique is generally reserved to cases where universes really are important, like ordinal.{u} and cardinal.{u}, or they might be available as variants of an existing definition, for example empty : Type 0 and pempty.{u} : Type u

[Mario Carneiro]

Type u is the type of all types in universe u

[Mario Carneiro]

Type u is equal to Sort (u+1), which extends the universe hierarchy one step downward to the universe Prop = Sort 0, which is special in a few ways

[Callum Cassidy-Nolan]

So then nat : Type u makes nat a type in universe u?

[Mario Carneiro]

You mean in the definition? Normally if you write nat : Type u you get a type error because nat doesn't have type Type u, it has type Type 0

[Mario Carneiro]

if you put that in the definition then it would become a family of types nat.{u} as mentioned, so you would have nat.{0} : Type 0, nat.{1} : Type 1 and so on

[Callum Cassidy-Nolan]

Ok, and since we only need one version of the naturals we just do nat : Type 0 ?

[Mario Carneiro]

exactly

[Callum Cassidy-Nolan]

Would integers also reside in Type 0 ?

[Mario Carneiro]

yep

[Callum Cassidy-Nolan]

Or would it be a larger number?

[Callum Cassidy-Nolan]

Oh ok

[Mario Carneiro]

it is occasionally technically useful to have a copy of the natural numbers in higher universes, and we use ulift.{u v} : Type u -> Type (max u v) for that

[Callum Cassidy-Nolan]

I understand why we needed infinite types, because of the paradox, but what are the point of the Sort's ?

[Mario Carneiro]

Some theorems are true for both Prop and Type u

[Mario Carneiro]

and it is useful to be able to prove them only once and have the theorem apply in both contexts

[Callum Cassidy-Nolan]

Why do we need both ?

[Mario Carneiro]

why have propositions? or why have types? Both are useful

[Mario Carneiro]

obviously we need nat and we need 2 + 2 = 4

[Callum Cassidy-Nolan]

So it's to do with the types as propositions mindset thing right?

[Mario Carneiro]

yeah, basically

[Callum Cassidy-Nolan]

So why not set them equal? Like : Type u is equal to Sort u if they represent the same thing?

[Mario Carneiro]

That's the way it used to be, but inductive types that have type Sort u are really badly behaved so we usually have them in Type u or Prop

[Mario Carneiro]

I suppose we could write Sort (u+1) but that's a really common case

[Mario Carneiro]

and Type = Type 0 is especially common since it's the type of all your favorite types

[Callum Cassidy-Nolan]

Ok, so it's due to some implementation thing in Lean not due to some conceptual thing like, we need infinite types to dodge the paradox ?

[Mario Carneiro]

No this is just a design question. Coq does it differently, there is no Sort but there is Prop, Set and Type u and don't ask me why they need two base universes

[Mario Carneiro]

oh and SProp

[Mario Carneiro]

Agda has Prop u and Type u IIRC

[Callum Cassidy-Nolan]

Ok, I think I came out of this understanding a little more (at least why there are infinite of them).

[Callum Cassidy-Nolan]

Thank you

[Mario Carneiro]

Oh and of course ZFC just has one universe

[Callum Cassidy-Nolan]

Because everything is a set?

[Mario Carneiro]

everything except the set of all sets

[Mario Carneiro]

there are sets and classes and some classes can't be sets

[Callum Cassidy-Nolan]

That doesn't exist right?

[Mario Carneiro]

and the universe itself is one of them

[Mario Carneiro]

so roughly speaking ZFC loses the type theory ability to say that everything expressible in the system has some type

[Mario Carneiro]

that's what really forces the infinite hierarchy

[Callum Cassidy-Nolan]

Right

[Callum Cassidy-Nolan]

Using types we still can't say "a : <type of all types>", but we can say a : Type* to say that it resides in of the layers which is equivalent ?

[Mario Carneiro]

Well, Type* isn't really a type, it's notation for Type <something that lean will deduce from context>

[Callum Cassidy-Nolan]

What about in a situation like this:

theorem open_set_for_each
  (X : Type*)
  [topological_space X]
  (A : set X)
  (h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊂ A) :
  is_open A :=
begin
  sorry
end

[Mario Carneiro]

If you say X : Type* in an assumption, then lean will deduce that you want it to live in a universe named by a fresh universe variable

[Mario Carneiro]

so lean turns your theorem into

theorem open_set_for_each.{u}
  (X : Type u)
  [topological_space X]
  (A : set X)
  (h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊂ A) :
  is_open A :=
begin
  sorry
end

[Mario Carneiro]

(the lean 3 syntax for that is actually a little different BTW, theorem {u} open_set_for_each, but this is weird and has been changed to be the sensible thing in lean 4)

[Callum Cassidy-Nolan]

And the only way we can actually use that theorem is by specifying an actual number ?

[Mario Carneiro]

no, we can specify a universe expression as well

[Callum Cassidy-Nolan]

What would that look like?

[Mario Carneiro]

for example if you are proving some other theorem with a {u} in it then you might use open_set_for_each.{u}, or maybe open_set_for_each.{u+1} or open_set_for_each.{max u 3}

[Mario Carneiro]

lean is very good at figuring the right indexes out so you almost never have to specify

[Callum Cassidy-Nolan]

In that situation is u : nat ?

[Mario Carneiro]

not exactly. You can think of it that way, it represents a natural number, but not in a way that lean itself has access to. You can't write def foo (n : nat) : Type n := ...

[Callum Cassidy-Nolan]

So how do I say u is a universe variable thing?

[Mario Carneiro]

This is also on pain of contradiction, because if such a foo existed then the type of foo itself would have to live in Type ω

[Mario Carneiro]

You use universe(s) u to declare universe variables, analogous to variable(s) n : nat statements

[Mario Carneiro]

and to declare universe variables in a theorem statement you put the names in braces before the theorem name, like this

theorem {u} open_set_for_each
  (X : Type u)
  [topological_space X]
  (A : set X)
  (h₀ : ∀ x ∈ A, ∃ (U : set X), is_open U ∧ x ∈ U ∧ U ⊂ A) :
  is_open A :=
begin
  sorry
end

[Mario Carneiro]

Or you can use Type* which implicitly declares an anonymous universe variable for the statement

[Mario Carneiro]

Another trick I like is to just use (X) which declares X : Sort*, which lean will solve to Sort u or Prop or Type u as appropriate based on how it is used

[Mario Carneiro]

it's short and very difficult to get wrong