SIGSEGV, coercion

Stream: new members

[Danila Kurganov]

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 :),

[Danila Kurganov]

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

[Mario Carneiro]

what error

[Danila Kurganov]

"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

[Mario Carneiro]

and you copied the entire rest of the file?

[Mario Carneiro]

what is the state at the error

[Mario Carneiro]

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

[Danila Kurganov]

yeah, that whole thing you sent over

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

a : G1
⊢ ℚ

[Danila Kurganov]

yeah I'm not sure why mine is using arrows

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

ok, I get the same error as you after updating

[Danila Kurganov]

I'm on lean 3.16.5

[Mario Carneiro]

#3204

[Danila Kurganov]

oh nice, ok it clears a few things

[Johan Commelin]

subtype now uses coe everywhere as SNF

[Mario Carneiro]

apparently this changed a few days ago

[Johan Commelin]

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

[Mario Carneiro]

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,
}

[Danila Kurganov]

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

[Mario Carneiro]

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

[Mario Carneiro]

but lean knows to insert the function automatically now

[Mario Carneiro]

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

[Danila Kurganov]

ok, I guess that's good

[Danila Kurganov]

thanks again

[Scott Morrison]

(wrong thread)