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 ,
  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:
ε : ,
 : ε > 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 ks in the hypothesis gets substituted by none and some val. But, if we pattern match on (g k), then the (g k) in the hypothesis don't get substituted:

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

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

Yakov Pechersky (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 3

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

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

ccn (Jan 25 2022 at 19:47):

Alex J. Best said:

ccn said:

Alex J. Best said:

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

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

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

How come that case is generated anyways then?

Alex J. Best (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):

docs#list.mem

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 type of proofs of P and Q?

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

Kyle Miller (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 the statement, 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):

image.png

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 succ_eq_add_one as well. apparently not!

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

docs#real.rpow_mul

ccn (Feb 03 2022 at 04:17):

Kyle Miller said:

docs#real.rpow_mul

I'm working on that now:

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

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

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

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

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

ccn (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,

image.png

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

import topology.basic

theorem open_set_for_each (X : topological_space) (h : A  X) (h₁ :  x  A,  U, x  U  U  A) : is_open X U :=
begin
end

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

Kevin Buzzard (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):

docs#tprod

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

docs#polynomial.coeff ?

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 Types, not Props. :(

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 classicals in the tactics of proofs on an as-needed basis, but later decided to just open_locale classical, but in this one proof I had forgotten to take out the classical tactic.

Yakov Pechersky (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_eqs 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