Zulip Chat Archive

Stream: new members

Topic: SIGSEGV, coercion


view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:12):

the ext thing does clears a few things, I was wondering how it did ext to things that didn't look obviously equal

that's a neat trick I like it makes it more like python :),

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:14):

I did want to ask, when I run your code Mario, I get errors with rw [mul_div_cancel' _ a.nz], as it can't finish the proof. Is that issue also on your system? I just want to make sure my simp is the same as yours

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:14):

what error

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:14):

"rewrite tactic failed, did not find instance of the pattern in the target expression
a.val * (?m_1 / a.val)"

the line is red for me on vscode

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:16):

and you copied the entire rest of the file?

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:16):

what is the state at the error

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:17):

the lemma G1_inv_val should have fired from the simp on the first line resulting in the goal ⊢ a.val * (4 / a.val) = 4

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:17):

yeah, that whole thing you sent over

state:
2 goals
a : G1
 a * (4 / a) = 4

a : G1
 

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:18):

yeah I'm not sure why mine is using arrows

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:18):

aha, have we changed the simp normal form for subtype.val recently? @Johan Commelin ?

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:18):

I'm not using a particularly up to date mathlib, it could be my fault

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:20):

ok, I get the same error as you after updating

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:20):

I'm on lean 3.16.5

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:20):

#3204

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:20):

oh nice, ok it clears a few things

view this post on Zulip Johan Commelin (Jul 02 2020 at 11:21):

subtype now uses coe everywhere as SNF

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:21):

apparently this changed a few days ago

view this post on Zulip Johan Commelin (Jul 02 2020 at 11:21):

Yup, thanks to Floris. Finally readable subtypes :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:25):

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}

instance : has_coe G1  := subtype.val

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

@[simp] def G1mul (a b : G1) : G1 :=  a * (b / 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 : G1) : ) = a * (b / 2) := rfl

/-- ##Def of One --/

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

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

-- clearly follow other axioms since from field

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

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

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

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


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

@[simp] lemma G1_val_mul_inv (a : G1) : (a * (a⁻¹ : G1) : ) = 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,
}

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:31):

Okay so now we add the has_coe thing and any a.val to just the normal a...So sort of just 'factorised' out the .val from coercion

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:32):

the function is still there, you will see an up arrow when lean prints it back to you

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:32):

but lean knows to insert the function automatically now

view this post on Zulip Mario Carneiro (Jul 02 2020 at 11:32):

but you do need more type ascriptions to make it happen in the right places

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:34):

ok, I guess that's good

view this post on Zulip Danila Kurganov (Jul 02 2020 at 11:35):

thanks again

view this post on Zulip Scott Morrison (Jul 02 2020 at 13:44):

(wrong thread)


Last updated: May 12 2021 at 23:13 UTC