question

Stream: general

[sedev627]

image.png

[sedev627]

Can I get some advice....?

[sedev627]

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

[Sebastien Gouezel]

Can you post a #mwe, with #backticks?

[sedev627]

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,
    rw ← add_one,
    sorry,
  },
end

[sedev627]

Is it working...?

[Patrick Johnson]

That is not a #mwe.

[sedev627]

Oh sorry... I'll fix it

[sedev627]

Is it okay....?

[sedev627]

(deleted)

[sedev627]

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

[sedev627]

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

[Patrick Johnson]

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

[sedev627]

Thank you....!

[sedev627]

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]

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]

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

[Kyle Miller]

@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,
    rw ← add_one,

    qify [two_dvd_mul_succ_self],
    ring,
  },
end

[sedev627]

Can Type casting be do in lean prover?

[sedev627]

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,
    rw ← add_one,

    qify [two_dvd_mul_succ_self],
    ring,
  },
end

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

[sedev627]

Is there any examples using is_compact?

[Bulhwi Cha]

@sedev627 See https://leanprover-community.github.io/mathematics_in_lean/07_Topology.html#compactness.

[sedev627]

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]

Seems you allow S to be empty.

[sedev627]

Martin Dvořák said:

Seems you allow S to be empty.

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

[Martin Dvořák]

What doesn't work that you want to do?

[sedev627]

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

[Martin Dvořák]

Show us.

[sedev627]

image.png

[sedev627]

Can you see it...?

[Mario Carneiro]

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

[Mario Carneiro]

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

[sedev627]

Thank you!!!

[Mario Carneiro]

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]

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]

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