# Zulip Chat Archive

## Stream: new members

### Topic: Basic Proving Questions

#### ccn (Jan 12 2022 at 02:34):

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 (Jan 12 2022 at 02:38):

`or.inl ha`

#### Reid Barton (Jan 12 2022 at 02:38):

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

or not

#### ccn (Jan 12 2022 at 02:47):

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 (Jan 12 2022 at 02:55):

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 (Jan 12 2022 at 03:03):

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 (Jan 12 2022 at 03:06):

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 (Jan 12 2022 at 03:28):

`#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 (Jan 12 2022 at 20:19):

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

#### ccn (Jan 12 2022 at 20:56):

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 (Jan 12 2022 at 21:04):

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

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

#### Kyle Miller (Jan 12 2022 at 21:05):

Oh, also `b`

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

#### ccn (Jan 12 2022 at 21:21):

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

#### ccn (Jan 12 2022 at 21:21):

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

#### Floris van Doorn (Jan 12 2022 at 22:30):

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 (Jan 12 2022 at 23:10):

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 (Jan 12 2022 at 23:14):

There's also docs#or.intro_left

#### ccn (Jan 13 2022 at 00:27):

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 (Jan 13 2022 at 00:29):

Try dsimp first

#### Kyle Miller (Jan 13 2022 at 00:29):

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 (Jan 13 2022 at 00:30):

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

#### ccn (Jan 13 2022 at 00:33):

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 (Jan 13 2022 at 00:34):

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 (Jan 13 2022 at 00:35):

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 (Jan 13 2022 at 00:38):

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

#### Eric Rodriguez (Jan 13 2022 at 00:39):

`norm_num`

#### ccn (Jan 13 2022 at 00:45):

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

#### Arthur Paulino (Jan 13 2022 at 00:46):

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

#### Kyle Miller (Jan 13 2022 at 00:47):

@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 (Jan 13 2022 at 00:47):

and eric means tactic#norm_num

#### Eric Rodriguez (Jan 13 2022 at 00:47):

but no, it's just a tactic; if your goal is `1233462734 > 0`

, then `by norm_num`

will solve it

#### Kyle Miller (Jan 13 2022 at 00:49):

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 (Jan 13 2022 at 00:51):

Someone else used `linarith`

what is that doing?

#### Kyle Miller (Jan 13 2022 at 00:52):

tactic#linarith automatically solves linear (in)equalities

#### ccn (Jan 13 2022 at 23:23):

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 (Jan 13 2022 at 23:30):

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 (Jan 13 2022 at 23:37):

@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 (Jan 13 2022 at 23:53):

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 (Jan 14 2022 at 00:27):

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 (Jan 14 2022 at 00:32):

The type of `h1`

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

#### ccn (Jan 17 2022 at 01:17):

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 (Jan 17 2022 at 01:20):

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 (Jan 17 2022 at 01:33):

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 (Jan 17 2022 at 01:35):

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 (Jan 17 2022 at 22:05):

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 (Jan 17 2022 at 22:26):

fyi, there's a missing colon after `example`

for the last one.

#### Kyle Miller (Jan 17 2022 at 22:27):

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 (Jan 17 2022 at 22:35):

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 (Jan 17 2022 at 22:41):

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 (Jan 17 2022 at 23:01):

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 (Jan 17 2022 at 23:09):

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 (Jan 17 2022 at 23:10):

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 (Jan 17 2022 at 23:10):

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

#### Kyle Miller (Jan 17 2022 at 23:10):

You need `f`

and `g`

as additional arguments for the lambda after the `:=`

.

#### ccn (Jan 17 2022 at 23:19):

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 (Jan 17 2022 at 23:52):

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 `k`

s 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 (Jan 18 2022 at 00:37):

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

#### Tomaz Gomes Mascarenhas (Jan 18 2022 at 00:39):

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

#### ccn (Jan 18 2022 at 01:53):

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 (Jan 18 2022 at 01:55):

@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 (Jan 18 2022 at 01:56):

@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 (Jan 18 2022 at 01:58):

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 (Jan 18 2022 at 01:58):

You can see for yourself by doing `#print y`

after your theorem.

#### ccn (Jan 18 2022 at 01:58):

that's useful!

#### ccn (Jan 18 2022 at 02:53):

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

what does `show p, from hp`

do?

#### Kyle Miller (Jan 18 2022 at 03:35):

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

#### Kevin Buzzard (Jan 18 2022 at 03:42):

it's the same as `hp`

-- it just announces what it's going to prove before it proves it.

#### Eric Wieser (Jan 19 2022 at 23:33):

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 (Jan 23 2022 at 02:25):

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 (Jan 23 2022 at 03:45):

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 (Jan 23 2022 at 04:40):

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 (Jan 23 2022 at 04:48):

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 (Jan 23 2022 at 05:13):

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 (Jan 23 2022 at 05:13):

you would have to write `abs_add _ _`

#### Mario Carneiro (Jan 23 2022 at 05:14):

`by apply abs_add`

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

#### Patrick Johnson (Jan 23 2022 at 14:46):

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 (Jan 23 2022 at 18:14):

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 (Jan 23 2022 at 18:18):

It also means you can see the proof state after `congr' 1`

by positioning the cursor there

#### ccn (Jan 25 2022 at 18:18):

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 (Jan 25 2022 at 18:24):

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 (Jan 25 2022 at 18:36):

Yeah it does, thank you! This `norm_num`

thing seems super powerful

#### ccn (Jan 25 2022 at 18:36):

What does it mean to normalize numerical expressions?

#### Alex J. Best (Jan 25 2022 at 18:39):

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

#### Kyle Miller (Jan 25 2022 at 18:43):

`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 (Jan 25 2022 at 18:44):

`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 (Jan 25 2022 at 18:55):

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 (Jan 25 2022 at 18:55):

Probably `import data.zmod.basic`

?

#### Alex J. Best (Jan 25 2022 at 18:56):

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

#### ccn (Jan 25 2022 at 19:04):

that solved it!

#### ccn (Jan 25 2022 at 19:04):

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

Your link to `dec_trivial`

didn't load for me, where can I read about it?

#### Alex J. Best (Jan 25 2022 at 19:06):

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 (Jan 25 2022 at 19:14):

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 (Jan 25 2022 at 19:15):

My confusion comes in because in the tactic screen everything looks the same:

Uploading image.png…

#### ccn (Jan 25 2022 at 19:16):

```
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 (Jan 25 2022 at 19:17):

Hmm `↑x ^ 3`

has type `zmod 7`

#### ccn (Jan 25 2022 at 19:18):

Oh so `this`

is actually everything `(mod 7)`

right?

#### ccn (Jan 25 2022 at 19:20):

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

#### ccn (Jan 25 2022 at 19:22):

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 (Jan 25 2022 at 19:33):

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 (Jan 25 2022 at 19:36):

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 (Jan 25 2022 at 19:38):

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 (Jan 25 2022 at 19:38):

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 (Jan 25 2022 at 19:39):

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 (Jan 25 2022 at 19:41):

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 (Jan 25 2022 at 19:42):

(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 (Jan 25 2022 at 19:46):

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 (Jan 25 2022 at 19:46):

How does that differ from things like `linarith`

and `ring`

then?

#### Alex J. Best (Jan 25 2022 at 19:46):

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 3What 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 (Jan 25 2022 at 19:47):

Alex J. Best said:

ccn said:

Alex J. Best said:

`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 3What 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 (Jan 25 2022 at 19:48):

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 (Jan 25 2022 at 19:50):

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 (Jan 25 2022 at 19:53):

What is the point of the `revert h; dec_trivial`

?

#### ccn (Jan 25 2022 at 19:54):

expanding it out it looks like this: image.png

#### Johan Commelin (Jan 25 2022 at 19:55):

`dec_trivial`

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

#### ccn (Jan 25 2022 at 19:55):

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

#### Johan Commelin (Jan 25 2022 at 19:55):

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

#### ccn (Jan 25 2022 at 19:56):

I see

#### Alex J. Best (Jan 25 2022 at 19:56):

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 (Jan 25 2022 at 19:56):

I haven't followed the thread. But `succ_ne_zero`

doesn't hold in `zmod 7`

, right? :wink:

#### ccn (Jan 25 2022 at 19:56):

Oh right

#### Johan Commelin (Jan 25 2022 at 19:57):

You could use `mul_zero`

and `zero_ne_one`

.

#### ccn (Jan 25 2022 at 19:57):

So that's like a more generalized version

#### ccn (Jan 25 2022 at 19:59):

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

?

#### Alex J. Best (Jan 25 2022 at 20:00):

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 (Jan 25 2022 at 20:00):

What constitutes the right form?

#### Alex J. Best (Jan 25 2022 at 20:01):

The lemma `ok`

is where this method really shines.

#### Alex J. Best (Jan 25 2022 at 20:02):

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 (Jan 25 2022 at 20:03):

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

#### Kyle Miller (Jan 25 2022 at 20:05):

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 (Jan 25 2022 at 20:05):

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 (Jan 25 2022 at 20:09):

thanks!

#### ccn (Jan 25 2022 at 20:11):

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 (Jan 25 2022 at 20:18):

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 (Jan 25 2022 at 20:18):

I suspect one of them being docs#eq

#### ccn (Jan 25 2022 at 20:25):

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

image.png

#### ccn (Jan 25 2022 at 20:25):

Isn't that like a hypothesis though?

#### Yaël Dillies (Jan 25 2022 at 20:26):

Precisely, it's an inductive!

#### Yaël Dillies (Jan 25 2022 at 20:26):

#### Yaël Dillies (Jan 25 2022 at 20:27):

The `... | ...`

bit breaks the inductive part. The `⟨...⟩`

bit breaks the structure part.

#### ccn (Jan 25 2022 at 20:27):

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

#### Yaël Dillies (Jan 25 2022 at 20:29):

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

#### Yaël Dillies (Jan 25 2022 at 20:31):

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 (Jan 25 2022 at 20:39):

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 (Jan 25 2022 at 20:40):

because `∨`

is an inductive with two constructors

#### Kyle Miller (Jan 25 2022 at 20:40):

`|`

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

#### Kyle Miller (Jan 25 2022 at 20:42):

If it helps, these are the parentheses:

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

#### ccn (Jan 25 2022 at 20:48):

Why is `and`

a structure but `or`

is an inductive shouldn't they be the same?

#### Yaël Dillies (Jan 25 2022 at 20:49):

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

#### Yaël Dillies (Jan 25 2022 at 20:49):

Think about it. How do you build an `and`

? How do you build an `or`

?

#### ccn (Jan 25 2022 at 20:49):

two things and put them together

#### ccn (Jan 25 2022 at 20:50):

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

#### Yaël Dillies (Jan 25 2022 at 20:50):

You're thinking docs#band and docs#bor

#### Yaël Dillies (Jan 25 2022 at 20:50):

But how to make the *type* of proofs of `P`

and `Q`

?

#### Kyle Miller (Jan 25 2022 at 20:51):

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

#### Yaël Dillies (Jan 25 2022 at 20:51):

and the *type* of proofs of `P`

or `Q`

?

#### ccn (Jan 25 2022 at 20:51):

When we have `p : Prop`

p is a proof of the proposition right?

#### Kyle Miller (Jan 25 2022 at 20:52):

Going back to "why is `and`

a structure": a `structure`

is an inductive with exactly one constructor

#### ccn (Jan 25 2022 at 20:52):

Yaël Dillies said:

But how to make the

typeof 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 (Jan 25 2022 at 20:53):

(`structure`

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

#### Julian Berman (Jan 25 2022 at 20:54):

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 (Jan 25 2022 at 20:56):

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 (Jan 25 2022 at 20:58):

Julian Berman said:

Wait, is that correct? -- zulip lagged, sorry --

`p : Prop`

-- p is thestatement, not the proof, and`f : p`

`f`

is a proof of`p`

, right?

Whoops sorry, read that too quick

#### ccn (Jan 25 2022 at 20:59):

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 (Jan 25 2022 at 21:00):

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 (Jan 25 2022 at 21:00):

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

#### ccn (Jan 25 2022 at 21:02):

So this is somehow a roadblock for us to have `or`

and `and`

both be inductive types?

#### Yaël Dillies (Jan 25 2022 at 21:04):

Strictly speaking, they both are.

#### Kyle Miller (Jan 25 2022 at 21:04):

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 (Jan 25 2022 at 21:05):

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

#### Arthur Paulino (Jan 25 2022 at 21:06):

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 (Jan 25 2022 at 21:06):

Isn't that the same fashion enough to you?

#### Kyle Miller (Jan 25 2022 at 21:06):

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 (Jan 25 2022 at 21:07):

I think I understand his doubt. Abstracting technicalities, `and`

and `or`

have different levels of restrictions to be instantiated

#### Arthur Paulino (Jan 25 2022 at 21:08):

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 (Jan 25 2022 at 21:09):

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 (Jan 25 2022 at 21:10):

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 (Jan 25 2022 at 21:18):

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 (Jan 25 2022 at 21:22):

Are these `list.mem`

's constructors? image.png

#### ccn (Jan 25 2022 at 21:23):

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

#### Kyle Miller (Jan 25 2022 at 21:23):

list.mem is not an inductive type

#### Kyle Miller (Jan 25 2022 at 21:23):

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

#### Kyle Miller (Jan 25 2022 at 21:24):

`list.mem a [b1, b2]`

is `a = b1 or a = b2 or false`

#### ccn (Jan 25 2022 at 21:24):

Yaël Dillies said:

Precisely, it's an inductive!

Wait is an inductive an instance of an inductive type?

#### ccn (Jan 25 2022 at 21:26):

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 (Jan 25 2022 at 21:27):

`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 (Jan 25 2022 at 21:29):

Ok, so somehow the `⟨⟨⟩⟩`

can solve `list.mem (↑x ^ 3) list.nil`

, what's happening there?

#### Yaël Dillies (Jan 25 2022 at 21:30):

`false`

too is an inductive type!

#### ccn (Jan 25 2022 at 21:32):

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

#### ccn (Jan 25 2022 at 21:32):

how do you even make this thing

#### Kyle Miller (Jan 25 2022 at 21:33):

ccn said:

how do you even make this thing

exactly :smile:

#### ccn (Jan 25 2022 at 21:33):

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

#### ccn (Jan 25 2022 at 21:33):

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

#### ccn (Jan 25 2022 at 21:34):

#### Yaël Dillies (Jan 25 2022 at 21:35):

It's even stronger! If you happen to have made a term of type `false`

, then :explosion:

#### Kyle Miller (Jan 25 2022 at 21:35):

(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 (Jan 25 2022 at 21:35):

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

#### Kyle Miller (Jan 25 2022 at 21:36):

this is the main way you use `false`

, by getting anything you want from it:

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

#### ccn (Jan 25 2022 at 21:36):

What does it mean for true to have a constructor?

#### Kyle Miller (Jan 25 2022 at 21:37):

it means you can prove `true`

by definition

#### Kyle Miller (Jan 25 2022 at 21:37):

the proof is `true.intro`

#### ccn (Jan 25 2022 at 21:37):

So true can prove itself

#### Kyle Miller (Jan 25 2022 at 21:38):

and `false`

having no constructors: by definition you cannot prove it

#### ccn (Jan 25 2022 at 21:38):

I see

#### Kyle Miller (Jan 25 2022 at 21:38):

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 (Jan 25 2022 at 21:39):

right right

#### ccn (Jan 25 2022 at 21:40):

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 (Jan 25 2022 at 21:43):

`⟨⟩`

is the constructor that takes no parameter

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

#### ccn (Jan 25 2022 at 21:45):

Ok so the `⟨...⟩`

is only used on things with only one constructor?

#### Kyle Miller (Jan 25 2022 at 21:45):

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 (Jan 25 2022 at 21:46):

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 (Jan 25 2022 at 21:46):

Wrong, Arthur. All inductives have constructors.

#### Kyle Miller (Jan 25 2022 at 21:47):

`rcases`

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

#### Kyle Miller (Jan 25 2022 at 21:47):

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

#### Arthur Paulino (Jan 25 2022 at 21:47):

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 (Jan 25 2022 at 21:47):

I'm confused by what you're confused about

#### Yaël Dillies (Jan 25 2022 at 21:48):

`⟨⟩`

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

.

#### Yaël Dillies (Jan 25 2022 at 21:48):

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

#### Kyle Miller (Jan 25 2022 at 21:49):

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

#### Kyle Miller (Jan 25 2022 at 21:50):

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 (Jan 25 2022 at 21:54):

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 (Jan 25 2022 at 21:55):

Like `or`

?

#### Arthur Paulino (Jan 25 2022 at 21:56):

*mindblow*

I never thought of it this way :open_mouth:

#### Arthur Paulino (Jan 25 2022 at 21:56):

Indeed, it has two distinct constructors

#### Arthur Paulino (Jan 25 2022 at 22:16):

But then his question holds. Is it possible to instantiate `or`

with two distinct anonymous constructors?

#### Yaël Dillies (Jan 25 2022 at 22:20):

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 (Jan 26 2022 at 06:41):

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 (Jan 26 2022 at 06:48):

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 (Jan 28 2022 at 17:52):

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 (Jan 28 2022 at 17:58):

Do induction on `h₀`

!

#### ccn (Jan 28 2022 at 18:13):

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 (Jan 28 2022 at 18:14):

docs#nat.le is defined inductively, so `induction`

simply follows the definition.

#### ccn (Jan 28 2022 at 18:15):

Thank you! image.png which part is inductive?

#### ccn (Jan 28 2022 at 18:16):

isn't it using `less_than_or_equal`

?

#### ccn (Jan 28 2022 at 18:17):

Ah, and that is recursive: image.png

#### Kyle Miller (Jan 28 2022 at 18:44):

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 (Jan 28 2022 at 18:44):

One solution is having a custom induction principle for `le`

notation for `nat`

#### Yaël Dillies (Jan 28 2022 at 18:46):

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

#### Kyle Miller (Jan 28 2022 at 19:12):

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 (Jan 29 2022 at 23:53):

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 (Jan 29 2022 at 23:54):

first get rid of the c with docs#mul_lt_mul_left

#### Mario Carneiro (Jan 29 2022 at 23:54):

then use docs#pow_lt_pow_of_lt_left

#### ccn (Jan 30 2022 at 00:03):

Thanks Mario!

#### ccn (Jan 30 2022 at 01:55):

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 (Jan 30 2022 at 02:02):

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

#### ccn (Jan 30 2022 at 02:35):

Thanks Patrick

#### ccn (Jan 30 2022 at 02:36):

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 (Jan 30 2022 at 02:44):

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

#### Mario Carneiro (Jan 30 2022 at 02:47):

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

#### Mario Carneiro (Jan 30 2022 at 02:48):

(i.e. put the `import`

line)

#### Mario Carneiro (Jan 30 2022 at 02:57):

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 (Jan 30 2022 at 03:03):

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 (Jan 30 2022 at 03:29):

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 (Jan 30 2022 at 03:49):

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

#### ccn (Jan 30 2022 at 03:56):

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 (Jan 30 2022 at 03:59):

`$ 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 (Jan 30 2022 at 04:01):

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

#### Patrick Johnson (Jan 30 2022 at 04:03):

Also note that `$`

is right associative, so `a $ b $ c $ d`

is equal to `a (b (c d))`

#### ccn (Feb 01 2022 at 01:48):

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 (Feb 01 2022 at 02:06):

It's not at all obvious that the same kind of proof works. `4^n % 12`

could have arbitrary non-periodic behavior

#### Mario Carneiro (Feb 01 2022 at 02:06):

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

#### Mario Carneiro (Feb 01 2022 at 02:07):

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

#### Damiano Testa (Feb 01 2022 at 02:27):

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

?

#### ccn (Feb 01 2022 at 02:30):

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

#### ccn (Feb 01 2022 at 02:30):

Thanks for the feedback

#### Andrew Lubrino (Feb 01 2022 at 02:32):

removed

#### ccn (Feb 01 2022 at 02:37):

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 (Feb 01 2022 at 02:41):

Does `rw [pow_succ, IH]`

get you to `4 * 4 = 4`

?

#### ccn (Feb 01 2022 at 02:42):

Yes it does!

#### Damiano Testa (Feb 01 2022 at 02:42):

~~You may need an ~~ apparently not!`succ_eq_add_one`

as well.

#### ccn (Feb 01 2022 at 02:43):

so now I just need to prove `4 * 4 = 4`

(mod 12) I can just use `norm_num`

for something like that right?

#### ccn (Feb 01 2022 at 02:44):

norm_num just makes the goal `16 = 4`

#### Damiano Testa (Feb 01 2022 at 02:45):

At this stage, `dec_trivial`

might work? Not sure...

#### ccn (Feb 01 2022 at 02:46):

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 (Feb 01 2022 at 02:47):

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

#### Damiano Testa (Feb 01 2022 at 02:47):

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

#### ccn (Feb 01 2022 at 02:48):

Which works because these are now finite things?

#### Damiano Testa (Feb 01 2022 at 02:48):

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

#### ccn (Feb 01 2022 at 02:48):

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 (Feb 01 2022 at 02:49):

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 (Feb 01 2022 at 02:51):

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 (Feb 01 2022 at 02:53):

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 (Feb 01 2022 at 03:07):

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 (Feb 01 2022 at 03:08):

Yes, `n a b`

are implicit parameters (in `{}`

), so don't write them

#### ccn (Feb 01 2022 at 03:09):

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 (Feb 01 2022 at 03:09):

But then, the pattern won't match because there is a `+`

and not a `-`

#### ccn (Feb 01 2022 at 03:09):

Ah I see

#### ccn (Feb 01 2022 at 03:09):

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

#### ccn (Feb 01 2022 at 03:12):

I tried using this:

` rw ← neg_neg 20,`

but it fails because it cannot synthesize the type class

#### ccn (Feb 01 2022 at 03:13):

```@[simp]

theorem neg_neg {G : Type u} [add_group G] (a : G) :

--a = a

```
```

#### Reid Barton (Feb 01 2022 at 03:14):

Oh right because you are using `nat`

#### ccn (Feb 01 2022 at 03:15):

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

#### ccn (Feb 01 2022 at 03:16):

Shouldn't there be a `neg_neg`

that works for what I'm trying to do?

#### Damiano Testa (Feb 01 2022 at 03:23):

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 (Feb 01 2022 at 03:28):

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

#### Damiano Testa (Feb 01 2022 at 03:33):

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 (Feb 01 2022 at 03:35):

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

#### Damiano Testa (Feb 01 2022 at 03:38):

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

#### ccn (Feb 01 2022 at 03:49):

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 (Feb 01 2022 at 03:50):

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

#### ccn (Feb 01 2022 at 03:50):

What do you think the best way forward would be?

#### ccn (Feb 01 2022 at 03:51):

I was trying to use ` rw ← int.coe_nat_dvd,`

but I think that's making things harder to prove

#### ccn (Feb 01 2022 at 04:01):

I also think I'm confused about the difference between `MOD`

and `zmod`

#### ccn (Feb 01 2022 at 08:08):

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 (Feb 01 2022 at 08:20):

Below is my solution, in case you are interested!

#### Kevin Buzzard (Feb 01 2022 at 08:22):

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 (Feb 01 2022 at 08:23):

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 (Feb 01 2022 at 08:26):

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 (Feb 01 2022 at 08:26):

My solution using it:

#### ccn (Feb 01 2022 at 08:33):

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 (Feb 01 2022 at 08:33):

Should I add it to mathlib?

#### Kevin Buzzard (Feb 01 2022 at 08:34):

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 (Feb 01 2022 at 08:34):

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

#### ccn (Feb 01 2022 at 08:35):

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

#### Mario Carneiro (Feb 01 2022 at 08:36):

No one seems to have mentioned `norm_fin`

yet. It should be able to prove `(16 : zmod 12) = 4`

#### ccn (Feb 01 2022 at 08:37):

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 (Feb 01 2022 at 08:38):

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 (Feb 01 2022 at 08:38):

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 (Feb 01 2022 at 08:39):

Damiano's is still shorter though :-)

#### ccn (Feb 01 2022 at 08:40):

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 (Feb 01 2022 at 08:41):

@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 (Feb 01 2022 at 08:41):

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 (Feb 01 2022 at 08:42):

But `rfl`

is able to do it?

#### Kevin Buzzard (Feb 01 2022 at 08:42):

You're going slightly the wrong way. The point is that`simp`

knows that `1^n=1`

. The route is 4^n=1^n=1, not 4^n=4=1.

#### Damiano Testa (Feb 01 2022 at 08:43):

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 (Feb 01 2022 at 08:45):

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 (Feb 01 2022 at 08:46):

Can't that be changed to `simp`

? (edit: apparently not!)

#### Damiano Testa (Feb 01 2022 at 08:46):

(btw, the `a`

in `simpa`

takes care of another `rfl`

: the proof that `1 + 5 = 0 mod 3`

.)

#### Damiano Testa (Feb 01 2022 at 08:48):

Also, I recently learned that if you use `simpa`

where `simp`

suffices, you get an error.

#### Kevin Buzzard (Feb 01 2022 at 08:49):

Oh I see -- you're using the fact that `simpa`

tries `refl`

whereas `simp`

doesn't? Or tries it harder, or something?

#### Damiano Testa (Feb 01 2022 at 08:49):

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 (Feb 01 2022 at 08:50):

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 (Feb 01 2022 at 08:54):

```
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 (Feb 01 2022 at 08:55):

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

Is that a bug in `simpa`

??

#### Mario Carneiro (Feb 01 2022 at 08:56):

what are you guys doing to my baby

#### Mario Carneiro (Feb 01 2022 at 08:56):

that's not how you use `simpa`

#### Kevin Buzzard (Feb 01 2022 at 08:56):

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

#### Kevin Buzzard (Feb 01 2022 at 08:56):

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

#### Mario Carneiro (Feb 01 2022 at 08:59):

aha,`simpa`

uses `assumption <|> trivial`

once it's done its simp work

#### Mario Carneiro (Feb 01 2022 at 08:59):

and `trivial`

does several things, including `refl`

#### Kevin Buzzard (Feb 01 2022 at 09:00):

@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 (Feb 01 2022 at 09:01):

I think `simpa`

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

#### Mario Carneiro (Feb 01 2022 at 09:02):

You should just write `simp; trivial`

if that's what you want

#### Johan Commelin (Feb 01 2022 at 09:02):

maybe rename it to `simpA`

:smiley:

#### Damiano Testa (Feb 01 2022 at 09:02):

Ok, I did not know that I was abusing the `a`

in `simpa`

so much! :rofl:

#### Johan Commelin (Feb 01 2022 at 09:02):

`A`

for Aggressively Asserting Assumptions.

#### Mario Carneiro (Feb 01 2022 at 09:03):

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 (Feb 01 2022 at 09:03):

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 (Feb 01 2022 at 09:04):

I've used `simpa`

for `simp; refl`

a lot too. It's very handy

#### Damiano Testa (Feb 01 2022 at 09:06):

```
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 `simpa`

s were abused in this proof.

#### Bolton Bailey (Feb 01 2022 at 09:08):

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 (Feb 01 2022 at 09:34):

Maybe `simp`

should try `refl`

at the end.

#### Damiano Testa (Feb 01 2022 at 10:03):

~~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 (Feb 01 2022 at 10:15):

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 (Feb 01 2022 at 10:26):

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 (Feb 01 2022 at 10:28):

Lower bound:

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

This doesn't count proofs of the form

```
simp,
refl
```

that span 2 lines.

#### Damiano Testa (Feb 01 2022 at 10:28):

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

:stuck_out_tongue_wink:

#### Damiano Testa (Feb 01 2022 at 10:29):

Also, I imagine that the abusive `simpa`

proofs would fail, since `simp`

would have worked...

#### Vincent Beffara (Feb 01 2022 at 10:32):

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 (Feb 01 2022 at 10:34):

(just kidding of course)

#### Reid Barton (Feb 01 2022 at 10:56):

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 (Feb 01 2022 at 11:03):

`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 (Feb 01 2022 at 11:24):

What does `simp [rfl]`

do?

#### Damiano Testa (Feb 01 2022 at 13:15):

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 (Feb 01 2022 at 13:16):

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 (Feb 01 2022 at 14:43):

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 (Feb 01 2022 at 14:56):

I agree `simp`

shouldn't do a "full" `refl`

. Am I misremembering which kind of triviality `simp`

likes to get stuck on?

#### Henry Pearson (Feb 02 2022 at 11:24):

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 (Feb 02 2022 at 11:28):

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 (Feb 02 2022 at 11:31):

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 (Feb 02 2022 at 11:34):

Ah I see - that is very helpful!!

#### Henry Pearson (Feb 02 2022 at 11:34):

Thanks a lot

#### ccn (Feb 02 2022 at 20:02):

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

#### Yaël Dillies (Feb 02 2022 at 20:13):

`by_cases irrational x`

#### Kyle Miller (Feb 02 2022 at 20:18):

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 (Feb 02 2022 at 20:21):

Yeah, I'm a bit disappointed to see that `irrational`

is already the negation.

#### ccn (Feb 03 2022 at 01:52):

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 (Feb 03 2022 at 02:43):

Use `let sqrt_2`

, not `have sqrt_2`

#### ccn (Feb 03 2022 at 03:09):

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 (Feb 03 2022 at 03:16):

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 (Feb 03 2022 at 03:17):

the `let`

is probably doing no favors here, you should just `open real`

instead if you find it too verbose

#### Kyle Miller (Feb 03 2022 at 03:36):

Is there a more direct way to prove `foo`

here?

Code

#### ccn (Feb 03 2022 at 03:42):

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 (Feb 03 2022 at 03:57):

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 (Feb 03 2022 at 04:00):

#### ccn (Feb 03 2022 at 04:17):

Kyle Miller said:

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 (Feb 03 2022 at 04:19):

That's where the `foo`

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

#### ccn (Feb 03 2022 at 04:19):

Ohh ok.

#### Kyle Miller (Feb 03 2022 at 04:19):

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

#### ccn (Feb 03 2022 at 04:19):

Can't we make it into one?

#### Kyle Miller (Feb 03 2022 at 04:20):

That's what I did in the `foo`

lemma, and my question is whether there's a simpler way to do this.

#### Kyle Miller (Feb 03 2022 at 04:21):

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 (Feb 03 2022 at 04:22):

I get your reasoning more now

#### ccn (Feb 03 2022 at 04:45):

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 (Feb 03 2022 at 08:58):

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 (Feb 03 2022 at 13:34):

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 (Feb 03 2022 at 13:40):

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 (Feb 03 2022 at 13:41):

The lemma `List.cons_append`

will help you finish the proof from here though

#### Hossam Karim (Feb 03 2022 at 13:42):

Understood. Thanks a lot @Alex J. Best

#### ccn (Feb 03 2022 at 19:19):

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 (Feb 03 2022 at 19:21):

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

image.png

#### Alex J. Best (Feb 03 2022 at 19:28):

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 (Feb 03 2022 at 19:34):

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 (Feb 03 2022 at 19:36):

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

#### ccn (Feb 03 2022 at 19:37):

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 (Feb 03 2022 at 19:38):

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 (Feb 03 2022 at 19:42):

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 (Feb 03 2022 at 19:44):

I see

#### ccn (Feb 03 2022 at 19:44):

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 (Feb 03 2022 at 19:45):

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 (Feb 03 2022 at 19:51):

Thanks Alex I always learn a lot from you

#### ccn (Feb 03 2022 at 19:52):

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 (Feb 03 2022 at 19:53):

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 (Feb 03 2022 at 19:57):

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 (Feb 03 2022 at 20:04):

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 (Feb 03 2022 at 20:07):

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 (Feb 03 2022 at 20:08):

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 (Feb 03 2022 at 20:13):

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 (Feb 03 2022 at 20:17):

The lemma `m - n + n = m`

is always true in `ring`

s 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 (Feb 04 2022 at 22:36):

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 (Feb 05 2022 at 00:21):

@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 (Feb 05 2022 at 00:23):

Thanks for the new view on it! It looks cleaner

#### ccn (Feb 06 2022 at 22:06):

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,

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 (Feb 06 2022 at 22:07):

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

#### ccn (Feb 06 2022 at 22:09):

```
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 (Feb 06 2022 at 22:09):

When it says `unable to synthesize placeholder`

what exactly does that mean?

#### Kevin Buzzard (Feb 06 2022 at 22:10):

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

#### Kevin Buzzard (Feb 06 2022 at 22:10):

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

#### Kevin Buzzard (Feb 06 2022 at 22:11):

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

#### ccn (Feb 06 2022 at 22:12):

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 (Feb 06 2022 at 22:13):

So my `type a`

should be `X`

right?

#### Kevin Buzzard (Feb 06 2022 at 22:13):

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

#### ccn (Feb 06 2022 at 22:13):

Ah right, no sets...

#### Kevin Buzzard (Feb 06 2022 at 22:14):

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

#### Kevin Buzzard (Feb 06 2022 at 22:15):

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 (Feb 06 2022 at 22:16):

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 (Feb 06 2022 at 22:16):

`set (set X)`

#### Kevin Buzzard (Feb 06 2022 at 22:17):

Checkout the the definition of docs#topological_space

#### ccn (Feb 07 2022 at 00:31):

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 (Feb 07 2022 at 07:26):

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 (Feb 07 2022 at 19:39):

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

#### Kyle Miller (Feb 07 2022 at 19:46):

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

#### ccn (Feb 07 2022 at 20:04):

#### ccn (Feb 07 2022 at 20:04):

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

#### Reid Barton (Feb 07 2022 at 20:04):

unlucky

#### ccn (Feb 07 2022 at 20:04):

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

#### Reid Barton (Feb 07 2022 at 20:06):

right, `tprod`

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

#### Kevin Buzzard (Feb 07 2022 at 20:07):

Oops

#### Kevin Buzzard (Feb 07 2022 at 20:08):

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

#### Kevin Buzzard (Feb 07 2022 at 20:09):

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 (Feb 08 2022 at 20:56):

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 (Feb 08 2022 at 20:59):

What about docs#is_greatest?

#### Damiano Testa (Feb 08 2022 at 21:10):

@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 (Feb 08 2022 at 21:43):

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 (Feb 08 2022 at 21:44):

does this work?

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

#### ccn (Feb 08 2022 at 21:45):

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

#### ccn (Feb 08 2022 at 22:37):

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 (Feb 08 2022 at 22:38):

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

#### Yakov Pechersky (Feb 09 2022 at 00:05):

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 (Feb 09 2022 at 01:32):

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 (Feb 09 2022 at 01:34):

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 (Feb 09 2022 at 01:40):

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

)

#### ccn (Feb 09 2022 at 01:44):

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 (Feb 09 2022 at 01:44):

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

#### ccn (Feb 09 2022 at 01:45):

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

#### ccn (Feb 09 2022 at 01:46):

It's like I need to produce n distinct indices

#### Eric Rodriguez (Feb 09 2022 at 01:48):

`Σ i : ι, a i`

(also I'm writing ι for iota instead of `l`

but it doesn't matter ;b)

#### Eric Rodriguez (Feb 09 2022 at 01:48):

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

#### ccn (Feb 09 2022 at 19:34):

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 (Feb 09 2022 at 20:16):

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 (Feb 09 2022 at 20:18):

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 (Feb 09 2022 at 20:18):

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

#### Yaël Dillies (Feb 09 2022 at 20:20):

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

#### ccn (Feb 10 2022 at 01:42):

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 (Feb 10 2022 at 01:53):

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

#### ccn (Feb 10 2022 at 01:54):

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

#### Eric Rodriguez (Feb 10 2022 at 01:56):

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

#### ccn (Feb 10 2022 at 02:22):

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 (Feb 10 2022 at 02:23):

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 (Feb 10 2022 at 02:30):

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

#### ccn (Feb 10 2022 at 02:35):

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 (Feb 10 2022 at 02:56):

For doing a `finset`

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

?

#### David Landsberg (Feb 10 2022 at 03:46):

(deleted)

#### David Landsberg (Feb 10 2022 at 03:47):

(deleted)

#### Anne Baanen (Feb 10 2022 at 10:30):

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 (Feb 10 2022 at 10:37):

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 (Feb 10 2022 at 10:46):

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 (Feb 10 2022 at 21:15):

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

#### Yaël Dillies (Feb 10 2022 at 21:20):

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

#### ccn (Feb 10 2022 at 21:42):

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 (Feb 10 2022 at 21:43):

#### ccn (Feb 10 2022 at 22:02):

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 (Feb 10 2022 at 22:04):

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

#### Reuben Dunn (Feb 11 2022 at 06:04):

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 (Feb 11 2022 at 06:12):

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

#### Reuben Dunn (Feb 11 2022 at 06:16):

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 (Feb 11 2022 at 06:27):

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

#### ccn (Feb 11 2022 at 14:05):

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 (Feb 11 2022 at 14:35):

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

#### Julian Berman (Feb 11 2022 at 14:37):

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

#### Julian Berman (Feb 11 2022 at 14:37):

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 (Feb 11 2022 at 16:23):

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 (Feb 14 2022 at 16:45):

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

#### Anne Baanen (Feb 14 2022 at 16:47):

You can use docs#finset.sum, which has `\sum`

notation if you add `open_locale big_operators`

#### ccn (Feb 14 2022 at 16:47):

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 (Feb 14 2022 at 16:48):

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 (Feb 14 2022 at 16:48):

Are those first two little `n`

's supposed to be the `N`

?

#### ccn (Feb 14 2022 at 16:52):

nevermind, I found `fin`

in the docs now.

#### ccn (Feb 14 2022 at 16:52):

thanks Anne!

#### Anne Baanen (Feb 14 2022 at 16:53):

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 `Type`

s, not `Prop`

s. :(

#### Kyle Miller (Feb 14 2022 at 16:58):

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

#### ccn (Feb 14 2022 at 16:58):

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

(without the h)

#### Kyle Miller (Feb 14 2022 at 17:01):

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 (Feb 14 2022 at 17:02):

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

#### Yury G. Kudryashov (Feb 14 2022 at 23:41):

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

#### ccn (Feb 16 2022 at 01:01):

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 (Feb 16 2022 at 01:15):

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

#### ccn (Feb 16 2022 at 01:24):

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 (Feb 16 2022 at 01:25):

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 (Feb 16 2022 at 01:29):

Reals aren't computable, so `#eval`

won't work for that

#### Kyle Miller (Feb 16 2022 at 01:30):

`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 (Feb 16 2022 at 01:32):

This works though:

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

#### Yaël Dillies (Feb 16 2022 at 01:35):

So what you want is `nat.floor x % 10`

#### ccn (Feb 16 2022 at 05:12):

Thanks that works well!

#### ccn (Feb 16 2022 at 05:14):

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 (Feb 16 2022 at 08:34):

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 (Feb 16 2022 at 22:23):

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 (Feb 16 2022 at 22:43):

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 (Feb 16 2022 at 22:49):

```
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 (Feb 16 2022 at 22:50):

Ah ok, thanks for showing me that!

#### Kyle Miller (Feb 16 2022 at 22:59):

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 (Feb 16 2022 at 23:03):

Oh great! `mv_polynomial.support`

exists :-)

#### Callum Cassidy-Nolan (Feb 17 2022 at 00:14):

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 (Feb 17 2022 at 00:15):

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

#### Reid Barton (Feb 17 2022 at 00:17):

`P.eval 1 2 3 4`

seems very optimistic to me

#### Reid Barton (Feb 17 2022 at 00:18):

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 (Feb 17 2022 at 00:19):

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

#### Reid Barton (Feb 17 2022 at 00:20):

Your `σ`

is `fin 4`

#### Yakov Pechersky (Feb 17 2022 at 02:26):

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

#### Daniel Packer (Feb 17 2022 at 15:15):

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 (Feb 17 2022 at 15:17):

The tactic#congr family might help here

#### Daniel Packer (Feb 17 2022 at 15:17):

Nice! That did it. Thanks a ton!

#### Eric Rodriguez (Feb 17 2022 at 15:32):

usually this means that a lemma statement went wrong somewhere

#### Eric Rodriguez (Feb 17 2022 at 15:32):

so, if you don't mind me asking, does the `classical`

ite come from your code or mathlib?

#### Daniel Packer (Feb 17 2022 at 15:55):

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 (Feb 17 2022 at 16:00):

Okay, I figured out what was probably wrong. I had first inserted `classical`

s 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 (Feb 17 2022 at 19:52):

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 (Feb 17 2022 at 19:53):

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 (Feb 17 2022 at 19:54):

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 (Feb 17 2022 at 20:12):

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 (Feb 17 2022 at 20:15):

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 (Feb 17 2022 at 20:17):

The way to fix them *is* to add `decidable_eq`

hypotheses.

#### Daniel Packer (Feb 17 2022 at 20:18):

Okay, previously having `decidable_eq`

in the hypothesis got the mathlib linter mad at me. Is there a way to tell which `decidable_eq`

s are okay to have? Is it exactly when you need it to make the theorem statement work?

#### Yaël Dillies (Feb 17 2022 at 20:31):

Yes, exactly! :smiley:

#### Yaël Dillies (Feb 17 2022 at 20:34):

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 (Feb 17 2022 at 20:35):

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 (Feb 17 2022 at 20:36):

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 (Feb 17 2022 at 20:36):

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

#### Yaël Dillies (Feb 17 2022 at 20:38):

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 (Feb 17 2022 at 20:38):

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

#### Daniel Packer (Feb 17 2022 at 20:40):

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 (Feb 17 2022 at 20:43):

`open_locale classical`

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

#### Eric Rodriguez (Feb 17 2022 at 20:48):

I wish finsupp could be fixed :(

#### Yaël Dillies (Feb 17 2022 at 21:01):

Couldn't we follow the same idea as for `dfinsupp`

? There it seems to work well.

#### Stuart Presnell (Feb 18 2022 at 11:09):

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 (Feb 18 2022 at 13:11):

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 (Feb 18 2022 at 14:43):

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 (Feb 18 2022 at 14:45):

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 (Feb 18 2022 at 14:48):

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 (Feb 18 2022 at 15:04):

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 (Feb 18 2022 at 15:09):

`dfinsupp`

is also wrong, but less so.

#### Callum Cassidy-Nolan (Feb 20 2022 at 03:56):

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 (Feb 20 2022 at 03:57):

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

instead of `X : Type`

#### Mario Carneiro (Feb 20 2022 at 03:58):

`X : Type`

means `X`

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

means `X`

is a type in any universe

#### Mario Carneiro (Feb 20 2022 at 03:59):

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 (Feb 20 2022 at 04:00):

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 (Feb 20 2022 at 04:01):

Also what is the difference between `X : Type*`

and `X : Type u`

#### Mario Carneiro (Feb 20 2022 at 04:01):

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 (Feb 20 2022 at 04:01):

So in lean `Type 0 : Type 1`

and `Type 1 : Type 2`

and so on

#### Mario Carneiro (Feb 20 2022 at 04:02):

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

#### Mario Carneiro (Feb 20 2022 at 04:03):

`X : Type*`

is the same as `X : Type _`

, which is to say X has Type "lean figure it out"

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:03):

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 (Feb 20 2022 at 04:03):

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 (Feb 20 2022 at 04:04):

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 (Feb 20 2022 at 04:04):

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

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:04):

Do we ever use specific levels?

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:04):

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

#### Mario Carneiro (Feb 20 2022 at 04:05):

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

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:05):

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

?

#### Mario Carneiro (Feb 20 2022 at 04:05):

and if `A : Type u`

and `B : Type v`

then `A ⊕ B : Type (max u v)`

#### Mario Carneiro (Feb 20 2022 at 04:07):

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 (Feb 20 2022 at 04:07):

So `Type u`

is the type of families of `Type u`

??

#### Mario Carneiro (Feb 20 2022 at 04:08):

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 (Feb 20 2022 at 04:08):

`Type u`

is the type of all types in universe u

#### Mario Carneiro (Feb 20 2022 at 04:09):

`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 (Feb 20 2022 at 04:09):

So then `nat : Type u`

makes `nat`

a type in universe `u`

?

#### Mario Carneiro (Feb 20 2022 at 04:10):

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 (Feb 20 2022 at 04:10):

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 (Feb 20 2022 at 04:11):

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

?

#### Mario Carneiro (Feb 20 2022 at 04:11):

exactly

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:11):

Would integers also reside in `Type 0`

?

#### Mario Carneiro (Feb 20 2022 at 04:11):

yep

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:11):

Or would it be a larger number?

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:12):

Oh ok

#### Mario Carneiro (Feb 20 2022 at 04:12):

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 (Feb 20 2022 at 04:13):

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

's ?

#### Mario Carneiro (Feb 20 2022 at 04:13):

Some theorems are true for both `Prop`

and `Type u`

#### Mario Carneiro (Feb 20 2022 at 04:13):

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

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:14):

Why do we need both ?

#### Mario Carneiro (Feb 20 2022 at 04:14):

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

#### Mario Carneiro (Feb 20 2022 at 04:14):

obviously we need `nat`

and we need `2 + 2 = 4`

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:14):

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

#### Mario Carneiro (Feb 20 2022 at 04:14):

yeah, basically

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:15):

So why not set them equal? Like : `Type u`

is equal to `Sort u`

if they represent the same thing?

#### Mario Carneiro (Feb 20 2022 at 04:16):

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 (Feb 20 2022 at 04:16):

I suppose we could write `Sort (u+1)`

but that's a really common case

#### Mario Carneiro (Feb 20 2022 at 04:17):

and `Type = Type 0`

is especially common since it's the type of all your favorite types

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:17):

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 (Feb 20 2022 at 04:18):

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 (Feb 20 2022 at 04:18):

oh and `SProp`

#### Mario Carneiro (Feb 20 2022 at 04:19):

Agda has `Prop u`

and `Type u`

IIRC

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:20):

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

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:20):

Thank you

#### Mario Carneiro (Feb 20 2022 at 04:21):

Oh and of course ZFC just has one universe

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:21):

Because everything is a set?

#### Mario Carneiro (Feb 20 2022 at 04:21):

everything except the set of all sets

#### Mario Carneiro (Feb 20 2022 at 04:21):

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

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:21):

That doesn't exist right?

#### Mario Carneiro (Feb 20 2022 at 04:22):

and the universe itself is one of them

#### Mario Carneiro (Feb 20 2022 at 04:22):

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

#### Mario Carneiro (Feb 20 2022 at 04:23):

that's what really forces the infinite hierarchy

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:23):

Right

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:24):

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 (Feb 20 2022 at 04:25):

Well, `Type*`

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

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:26):

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 (Feb 20 2022 at 04:26):

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 (Feb 20 2022 at 04:27):

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 (Feb 20 2022 at 04:27):

(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 (Feb 20 2022 at 04:28):

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

#### Mario Carneiro (Feb 20 2022 at 04:28):

no, we can specify a universe expression as well

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:29):

What would that look like?

#### Mario Carneiro (Feb 20 2022 at 04:29):

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 (Feb 20 2022 at 04:29):

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

#### Callum Cassidy-Nolan (Feb 20 2022 at 04:29):

In that situation is `u : nat`

?

#### Mario Carneiro (Feb 20 2022 at 04:30):

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 (Feb 20 2022 at 04:31):

So how do I say `u`

is a universe variable thing?

#### Mario Carneiro (Feb 20 2022 at 04:31):

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 (Feb 20 2022 at 04:32):

You use `universe(s) u`

to declare universe variables, analogous to `variable(s) n : nat`

statements

#### Mario Carneiro (Feb 20 2022 at 04:33):

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 (Feb 20 2022 at 04:34):

Or you can use `Type*`

which implicitly declares an anonymous universe variable for the statement

#### Mario Carneiro (Feb 20 2022 at 04:35):

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 (Feb 20 2022 at 04:36):

it's short and very difficult to get wrong

Last updated: Dec 20 2023 at 11:08 UTC