# Zulip Chat Archive

## Stream: new members

### Topic: SIGSEGV, coercion

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

#### 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

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

what error

#### 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

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

and you copied the entire rest of the file?

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

what is the state at the error

#### 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`

#### 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
⊢ ℚ
```

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

yeah I'm not sure why mine is using arrows

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

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

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

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

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

ok, I get the same error as you after updating

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

I'm on lean 3.16.5

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

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

oh nice, ok it clears a few things

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

`subtype`

now uses `coe`

everywhere as SNF

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

apparently this changed a few days ago

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

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

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

#### 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

#### 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

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

but lean knows to insert the function automatically now

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

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

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

ok, I guess that's good

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

thanks again

#### Scott Morrison (Jul 02 2020 at 13:44):

(wrong thread)

Last updated: Dec 20 2023 at 11:08 UTC