## Stream: new members

### Topic: SIGSEGV errors

#### Danila Kurganov (Jul 02 2020 at 10:38):

Hi. My Lean keeps giving me a SIGSEGV error every 5 minutes or so while I'm working on it, are there any general fixes for this?

#### Kevin Buzzard (Jul 02 2020 at 10:39):

Are you putting .s at the end of your file? That can cause this

?

#### Danila Kurganov (Jul 02 2020 at 10:40):

.s? I have no .s's anywhere from what I can tell

#### Mario Carneiro (Jul 02 2020 at 10:40):

The thing you were last typing is often important to debugging this kind of thing

#### Kevin Buzzard (Jul 02 2020 at 10:40):

I meant ., but there was a new segfault introduced recently and possibly also removed recently

#### Mario Carneiro (Jul 02 2020 at 10:41):

Does it trigger again immediately on restart?

#### Kevin Buzzard (Jul 02 2020 at 10:41):

If you can reliably reproduce the segfault we'd be interested to see it

#### Danila Kurganov (Jul 02 2020 at 10:41):

ok, here's what I've been typing:

lemma G1mul_left_inv (a : G1) : a⁻¹ * a = G1one :=
begin
ext, simp, -- ring,
-- rw mul_assoc,
-- it seems like doing norm_num does some infinite loop!
refine (mul_left_inj' _).mp _,
exact 2,
exact two_ne_zero,
rw [mul_assoc, div_mul_cancel],

sorry
--unfold has_inv.inv,
--simp,
end


#### Danila Kurganov (Jul 02 2020 at 10:42):

ok, one sec I'll try to reproduce the segfault, and fix my code block

#### Mario Carneiro (Jul 02 2020 at 10:42):

in particular we need all the imports and opens

#### Mario Carneiro (Jul 02 2020 at 10:42):

use triple backtick

#backticks

#### Danila Kurganov (Jul 02 2020 at 10:43):

sweet #backticks
the whole file?
my imports are:

import data.real.basic
import tactic.interactive
open nat


#### Mario Carneiro (Jul 02 2020 at 10:43):

enough to make the lemma in question have the errors you expect

#### Mario Carneiro (Jul 02 2020 at 10:44):

what you gave isn't enough because I don't know what G1 and G1one are

#### Danila Kurganov (Jul 02 2020 at 10:45):

oh that's the whole file since I told simp many things, I'll just upload the whole .lean

#### Mario Carneiro (Jul 02 2020 at 10:45):

feel free to paste the entire code block here, zulip will hide it appropriately

#### Danila Kurganov (Jul 02 2020 at 10:46):

oh nice, that's better

import data.real.basic

import tactic.interactive

open nat

def G1 := {x : ℚ // 0 < x}

def G2 := { x : ℚ | 0 < x}

#check G1
#check ℚ
#check G2

variable a : G1
#check a.val
#check a.property

#check pos_of_one_div_pos
#check mul_pos

example : 0 < 4 := by exact four_pos
example (a b c: ℚ ) : a * b/c = a/c * b := by library_search

-- so we want G1 -- a type -- to make a group
example (a : G1) : 0 < a.val := a.property --> a.property stores 0 < a.val

/-- ##Def of mul --/

@[simp] def G1mul (a b : G1) : G1 := ⟨ (a.val) * (b.val / 2), mul_pos a.property (half_pos b.property) ⟩
instance : has_mul G1 := ⟨ G1mul ⟩ -- now we have *

/-- ##Def of One --/

@[simp] def G1one  : G1 := ⟨ 2, two_pos⟩
instance : has_one G1 := ⟨ G1one ⟩

-- clearly follow other axioms since from field

/-- ##Def and Lemmas for Inverse --/

lemma G1_val_pos (a : G1) : 0 < a.val⁻¹  :=
begin
cases a with x y,
simp, exact y,
end

def G1_inv (a : G1) : G1 := ⟨ 4/(a.val), mul_pos four_pos (G1_val_pos a)⟩
instance : has_inv G1 := ⟨ G1_inv ⟩

-- what does extensionality mean in this context?
/-- ##Extensionality and Simplification Lemmas  --/
@[ext] lemma ext (a b : G1) (hVal : a.val = b.val): a = b :=
begin
cases a with x y,
cases b with w z,
simp * at *,
-- I see that simp is doing something, but what exactly is it doing?
end

@[simp] lemma mul_val (a b :G1) : (a * b).val = a.val*(b.val/2) :=
begin
refl,
end

@[simp] lemma G1one_div_two : G1one.val/2 = (1 : ℚ) :=
begin
refl,
end

@[simp] lemma G1one_mul_half : G1one.val * (1/2) = (1 : ℚ) :=
begin
refl,
end

@[simp] lemma G1one_mul_two_inv : G1one.val * 2⁻¹ = (1 : ℚ ) :=
begin
refl,
end

@[simp] lemma G1_val_mul_inv (a : G1) : a.val * a⁻¹.val = 4 :=
begin
refine (div_left_inj' _).mp _,
exact a.val, -- DK : I don't know how it magically changed everything to a.val but I'm not complaining
intro h1,
have h2 : 0 < a.val := a.property,
rw h1 at h2,
by exact (and_not_self (0 ≤ 0)).mp h2, -- DK : Is there an easier way to use h2?
rw [mul_comm, mul_div_assoc, div_self, mul_one],
ring,
intro h,
have h2 : 0 < a.val := a.property, -- DK : I'm repeating things from before, is this good practice?
rw h at h2,
by exact (and_not_self (0 ≤ 0)).mp h2, -- DK : I did it!!
end

/-- ##Group Axioms --/
lemma G1mul_assoc (a b c : G1) : a * b * c = a * (b * c) :=
begin
ext, simp, ring,
end

lemma G1one_mul (a : G1) : G1one * a = a :=
begin
ext, simp, ring, --simp, ring, -- DK : I added G1one to simp, made it better
end

lemma G1mul_one ( a : G1) : a * G1one = a :=
begin
ext, simp, ring,
end

-- DK : Below was 'G1mul_left_inv' which I thought was a typo given the goal
-- DK : so I changed it to right, also further amending the Poof.
lemma G1mul_left_inv (a : G1) : a⁻¹ * a = G1one :=
begin
ext, simp, -- ring,
-- rw mul_assoc,
-- it seems like doing norm_num does some infinite loop!
refine (mul_left_inj' _).mp _,
exact 2,
-- DK : I am using my approach from the previous question, not sure if it's ok
-- DK : since it's quite different to your structure
exact two_ne_zero,
rw [mul_assoc, div_mul_cancel],

sorry
--unfold has_inv.inv,
--simp,
end

/-- ##Poof G1 is a group  --/
instance : group G1 := {
-- mul
mul := G1mul,
-- mul_assoc
mul_assoc := G1mul_assoc,
-- one
one := G1one,
-- one_mul
one_mul := G1one_mul,
-- mul_one
mul_one := G1mul_one,
-- inv
inv := G1_inv,
-- mul_left_inv
mul_left_inv := G1mul_left_inv,
}


#### Mario Carneiro (Jul 02 2020 at 10:46):

well at least it didn't segfault for me

#### Danila Kurganov (Jul 02 2020 at 10:47):

yeah, when I do nothing it's fine, but when I try to fix the (lemma G1mul_left_inv) at the end it does it eventually

i'll try to reproduce it and send over what I've done

#### Mario Carneiro (Jul 02 2020 at 10:48):

hm, the norm_num loop seems to be an issue with simp normal form battling norm_num normal form

#### Mario Carneiro (Jul 02 2020 at 10:49):

example (a : ℚ) : 1 / 2 * a = a := by norm_num


#### Danila Kurganov (Jul 02 2020 at 10:51):

Ok, that explains one of the infinite loops I was having!

#### Danila Kurganov (Jul 02 2020 at 10:58):

I think I'll just do my thing and if it segfaults again just mimic what I've done to get the server to stop. Thanks for now :+1:

#### Mario Carneiro (Jul 02 2020 at 10:59):

I took the liberty of cleaning up the proofs a bit. Hope this helps:

import data.real.basic

import tactic.interactive

open nat

-- One way to define a subtype (G1) out of a type (ℚ)
def G1 := {x : ℚ // 0 < x}
-- This instead is a "set"
def G2 := { x : ℚ | 0 < x}

lemma G1.nz (a : G1) : a.val ≠ 0 := ne_of_gt a.2

@[simp] def G1mul (a b : G1) : G1 := ⟨ (a.val) * (b.val / 2), mul_pos a.property (half_pos b.property) ⟩
instance : has_mul G1 := ⟨ G1mul ⟩ -- now we have *

@[simp] theorem G1_mul_val (a b : G1) : (a * b).val = (a.val) * (b.val / 2) := rfl

/-- ##Def of One --/

@[simp] def G1one : G1 := ⟨ 2, two_pos⟩
instance : has_one G1 := ⟨ G1one ⟩

@[simp] theorem G1_one_val : (1 : G1).val = 2 := rfl

-- clearly follow other axioms since from field

/-- ##Def and Lemmas for Inverse --/

lemma G1_val_pos (a : G1) : 0 < a.val⁻¹ := by simpa using a.2

def G1_inv (a : G1) : G1 := ⟨ 4/(a.val), mul_pos four_pos (G1_val_pos a)⟩
instance : has_inv G1 := ⟨ G1_inv ⟩

@[simp] theorem G1_inv_val (a : G1) : a⁻¹.val = 4 / a.val := rfl

-- what does extensionality mean in this context?
/-- ##Extensionality and Simplification Lemmas  --/
@[ext] lemma ext : ∀ (a b : G1) (hVal : a.val = b.val), a = b
| ⟨x,y⟩ ⟨w, z⟩ rfl := rfl

@[simp] lemma mul_val (a b :G1) : (a * b).val = a.val*(b.val/2) := rfl

@[simp] lemma G1_val_mul_inv (a : G1) : a.val * a⁻¹.val = 4 :=
begin
simp,
rw [mul_div_cancel' _ a.nz],
end

/-- ##Group Axioms --/
lemma G1mul_assoc (a b c : G1) : a * b * c = a * (b * c) :=
begin
ext, simp, ring,
end

lemma G1one_mul (a : G1) : 1 * a = a :=
begin
ext, simp, ring,
end

lemma G1mul_one ( a : G1) : a * 1 = a :=
begin
ext, simp, ring,
end

-- example (a : ℚ) : 1 / 2 * a = a := by norm_num

-- DK : Below was 'G1mul_left_inv' which I thought was a typo given the goal
-- DK : so I changed it to right, also further amending the Poof.
lemma G1mul_left_inv (a : G1) : a⁻¹ * a = 1 :=
begin
ext, simp, ring,
simp [a.nz],
end

/-- ##Poof G1 is a group  --/
instance : group G1 := {
-- mul
mul := G1mul,
-- mul_assoc
mul_assoc := G1mul_assoc,
-- one
one := G1one,
-- one_mul
one_mul := G1one_mul,
-- mul_one
mul_one := G1mul_one,
-- inv
inv := G1_inv,
-- mul_left_inv
mul_left_inv := G1mul_left_inv,
}


#### Danila Kurganov (Jul 02 2020 at 11:07):

Oh that is much better than what I have

So does the lemma_name.ext let you use the .ext as a method onto some object?

maybe .ext is a bad name for it, extension

#### Johan Commelin (Jul 02 2020 at 11:09):

ext in this context means roughly speaking that X and Y are equal if all their "components" are equal.

#### Mario Carneiro (Jul 02 2020 at 11:09):

yes, if you give theorems names like G1.foo then you can write a.foo instead of G1.foo a if one of the arguments to the theorem has type G1

#### Johan Commelin (Jul 02 2020 at 11:10):

And sometimes, you can get away with less than all components, because for example some of the components are proofs

Last updated: May 08 2021 at 03:17 UTC