SIGSEGV errors

Stream: new members

[Danila Kurganov]

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]

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

[Mario Carneiro]

?

[Danila Kurganov]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

Does it trigger again immediately on restart?

[Kevin Buzzard]

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

[Danila Kurganov]

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

[Mario Carneiro]

#mwe please

[Danila Kurganov]

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

[Mario Carneiro]

in particular we need all the imports and opens

[Mario Carneiro]

use triple backtick

[Mario Carneiro]

#backticks

[Danila Kurganov]

sweet #backticks
the whole file?
my imports are:

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Danila Kurganov]

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

[Mario Carneiro]

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

[Danila Kurganov]

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]

well at least it didn't segfault for me

[Danila Kurganov]

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]

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

[Mario Carneiro]

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

[Danila Kurganov]

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

[Danila Kurganov]

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]

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]

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]

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

[Mario Carneiro]

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]

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