## Stream: general

### Topic: question

image.png

#### sedev627 (Nov 27 2022 at 11:29):

I posted the above question, but not answered yet...

#### Sebastien Gouezel (Nov 27 2022 at 11:30):

Can you post a #mwe, with #backticks?

#### sedev627 (Nov 27 2022 at 11:32):

import tactic
import init.default
import init.data.nat
def arith_sum : ℕ → ℕ
| 0 := 0
| (nat.succ n) := nat.succ n + arith_sum n

def arith_formula (n : ℕ) : ℕ := n * (n + 1) / 2
open nat
theorem arith_eq (n : ℕ) : arith_formula n = arith_sum n :=
begin
rw arith_formula,
induction n,
{
ring,
},
{
rw arith_sum,
rw ← n_ih,
sorry,
},
end


#### sedev627 (Nov 27 2022 at 11:32):

Is it working...?

#### Patrick Johnson (Nov 27 2022 at 11:33):

That is not a #mwe.

#### sedev627 (Nov 27 2022 at 11:33):

Oh sorry... I'll fix it

Is it okay....?

(deleted)

#### sedev627 (Nov 27 2022 at 11:39):

Precisely... I stuck at "How to erase common constant 1/2 in equation....?".

#### sedev627 (Nov 27 2022 at 11:51):

Did I have some mistakes in above question...?

#### Patrick Johnson (Nov 27 2022 at 12:02):

lemma arith_eq {n : ℕ} : arith_formula n = arith_sum n :=
begin
rw arith_formula, induction n with n ih, { ring },
{ rw [arith_sum, ←ih, ←nat.add_one, ←nat.mul_left_inj (by linarith : 0 < 2),
add_mul _ _ 2, nat.div_mul_cancel, nat.div_mul_cancel], ring,
repeat { rw ←even_iff_two_dvd, apply nat.even_mul_succ_self }},
end


Thank you....!

#### sedev627 (Nov 27 2022 at 12:37):

Patrick Johnson said:

lemma arith_eq {n : ℕ} : arith_formula n = arith_sum n :=
begin
rw arith_formula, induction n with n ih, { ring },
{ rw [arith_sum, ←ih, ←nat.add_one, ←nat.mul_left_inj (by linarith : 0 < 2),
add_mul _ _ 2, nat.div_mul_cancel, nat.div_mul_cancel], ring,
repeat { rw ←even_iff_two_dvd, apply nat.even_mul_succ_self }},
end


It has error "unknown identifier 'nat.mul_left_inj'"... where is nat.mul_left_inj?

#### Patrick Johnson (Nov 27 2022 at 12:47):

I forgot to update my mathlib. Here is the fixed proof:

lemma arith_eq {n : ℕ} : arith_formula n = arith_sum n :=
begin
rw arith_formula, induction n with n ih, { ring },
{ rw [arith_sum, ←ih, ←nat.add_one, ←mul_right_cancel_iff_of_pos (by linarith : 0 < 2),
add_mul _ _ 2, nat.div_mul_cancel, nat.div_mul_cancel], ring,
all_goals { rw ←even_iff_two_dvd, apply nat.even_mul_succ_self }},
end


You also have to import data.nat.parity

#### sedev627 (Nov 27 2022 at 12:49):

It is working....!!!! Thank you!

#### Kyle Miller (Nov 28 2022 at 09:45):

@sedev627 You can also use the tactic#qify tactic, where you can give it information about whether something evenly divides, which lets it convert everything to rational arithmetic. Then ring works.

import tactic
import init.default
import init.data.nat
import data.nat.parity
import tactic.qify

def arith_sum : ℕ → ℕ
| 0 := 0
| (nat.succ n) := nat.succ n + arith_sum n

def arith_formula (n : ℕ) : ℕ := n * (n + 1) / 2
open nat

lemma two_dvd_mul_succ_self (n : ℕ) : 2 ∣ n * (n + 1) :=
by { rw [← even_iff_two_dvd], exact nat.even_mul_succ_self n }

theorem arith_eq (n : ℕ) : arith_formula n = arith_sum n :=
begin
rw arith_formula,
induction n,
{
ring,
},
{
rw arith_sum,
rw ← n_ih,

qify [two_dvd_mul_succ_self],
ring,
},
end


#### sedev627 (Nov 30 2022 at 02:21):

Can Type casting be do in lean prover?

#### sedev627 (Nov 30 2022 at 02:23):

Kyle Miller said:

sedev627 You can also use the tactic#qify tactic, where you can give it information about whether something evenly divides, which lets it convert everything to rational arithmetic. Then ring works.

import tactic
import init.default
import init.data.nat
import data.nat.parity
import tactic.qify

def arith_sum : ℕ → ℕ
| 0 := 0
| (nat.succ n) := nat.succ n + arith_sum n

def arith_formula (n : ℕ) : ℕ := n * (n + 1) / 2
open nat

lemma two_dvd_mul_succ_self (n : ℕ) : 2 ∣ n * (n + 1) :=
by { rw [← even_iff_two_dvd], exact nat.even_mul_succ_self n }

theorem arith_eq (n : ℕ) : arith_formula n = arith_sum n :=
begin
rw arith_formula,
induction n,
{
ring,
},
{
rw arith_sum,
rw ← n_ih,

qify [two_dvd_mul_succ_self],
ring,
},
end


Oh... I saw it just now... This is what I want.. thank you :)

#### sedev627 (Dec 26 2022 at 05:30):

Is there any examples using is_compact?

#### sedev627 (Dec 28 2022 at 18:39):

import tactic

def id_ {α : Type} (a : α) : α :=
a

class has_mul_ (α : Type*) :=
(mul : α → α → α)

class semigroup_ (α : Type*) extends has_mul_ α :=
(mul_assoc : ∀ a b c : α, mul (mul a b) c = mul a (mul b c))

class has_one_ (α : Type*) :=
(one : α)

class monoid_ (α : Type*) extends semigroup_ α, has_one α :=
(one_mul : ∀ a : α , mul one a = a)
(mul_one : ∀ a : α , mul a one = a)

class has_inv_ (α : Type*) :=
(inv : α → α)

class group_ (α : Type*) extends monoid_ α, has_inv_ α :=
(mul_left_inv : ∀ a : α , mul (inv a) a = one)

class subgroup_ (α : Type*) [group_ α] (S : set α) : Prop :=
(mul_inv : ∀ {a b}, a ∈ S → b ∈ S →  mul a (inv b) ∈ S)


I struggled to define subgroup. What's wrong?

#### Martin Dvořák (Dec 28 2022 at 18:44):

Seems you allow S to be empty.

#### sedev627 (Dec 28 2022 at 18:47):

Martin Dvořák said:

Seems you allow S to be empty.

What should I do? I'm a beginner...

#### Martin Dvořák (Dec 28 2022 at 18:49):

What doesn't work that you want to do?

#### sedev627 (Dec 28 2022 at 18:51):

I want subgroup_ to be well defined. However, the code now has an error.

Show us.

image.png

#### sedev627 (Dec 28 2022 at 18:53):

Can you see it...?

#### Mario Carneiro (Dec 28 2022 at 18:55):

mul and inv are functions in their respective namespaces has_mul_ and has_inv_

#### Mario Carneiro (Dec 28 2022 at 18:55):

so you should either open them or write has_mul_.mul (or make a notation for it)

Thank you!!!

#### Mario Carneiro (Dec 28 2022 at 18:56):

the reason you don't need to do that when you use extends is because they are actually local variables in that case (you can see them in the context in the goal view)

#### Martin Dvořák (Dec 28 2022 at 19:17):

Now when your code is syntactically correct, let's turn to the semantics. Do you want the empty set to be a subgroup?

#### Riccardo Brasca (Dec 28 2022 at 19:20):

Unless you want to really change the mathematical definition, the empty set is not a subgroup...

Last updated: Aug 03 2023 at 10:10 UTC