Zulip Chat Archive

Stream: general

Topic: class instances in definition of Prop


Kenny Lau (Apr 25 2020 at 13:55):

universe u
def how_do_I_make_this_work : Prop :=
 (G : Type u) [group G] (x : G) (hx : x * x = x), x = 1
failed to synthesize type class instance for
G : Type u,
_inst_1 : group G,
x : G
⊢ has_mul G

failed to synthesize type class instance for
G : Type u,
_inst_1 : group G,
x : G,
hx : x * x = x
⊢ has_one G

Sebastien Gouezel (Apr 25 2020 at 14:04):

One answer for two threads.

universe u
def how_do_I_make_this_work : Prop :=
 (G : Type u) [group G] (x : G) (hx : by {unfreezeI, exact x * x = x}),
by {unfreezeI, exact x = 1}

Kenny Lau (Apr 25 2020 at 14:05):

def how_do_I_make_this_work : Prop :=
 (G : Type u) [group G] (x : G), by unfreezeI; exact  (hx : x * x = x), x = 1

Kevin Buzzard (Apr 25 2020 at 16:23):

See the mess I got into at codewars

Reid Barton (Apr 25 2020 at 16:24):

by exactI is the tactic for this, though it's still a bit annoying

Reid Barton (Apr 25 2020 at 16:25):

unfreezeI is mainly for letting you case on instance arguments, I think.

Kevin Buzzard (Apr 25 2020 at 16:25):

@Kenny Lau didn't you have this problem in codewars with the 5 units question? That has a typeclass in the defintion of SUBMISSION

Kenny Lau (Apr 25 2020 at 16:25):

I inserted the instances manually...

Reid Barton (Apr 25 2020 at 16:27):

there's also

inductive {u} how_do_I_make_this_work : Prop
| mk (G : Type u) [group G] (x : G) (hx : x * x = x) : x = 1  how_do_I_make_this_work

Kevin Buzzard (Apr 25 2020 at 16:28):

Can SUBMISSION be defined in the same way?

import topology.metric_space.basic

def converges_to {X : Type*} [metric_space X] (s :   X) (x : X) :=
 (ε : ) ( : 0 < ε),  N : ,  (n : ) (hn : N  n), dist x (s n) < ε

notation s `  ` x := converges_to s x

def SUBMISSION :=  {X : Type*} [h : metric_space X] {s :   X} (x₀ x₁ : X),
  by letI := h; exact
   (h₀ : s  x₀) (h₁ : s  x₁), x₀ = x₁

Kevin Buzzard (Apr 25 2020 at 16:29):

def SUBMISSION :=  {X : Type*} [metric_space X] {s :   X} (x₀ x₁ : X),
  by exactI
   (h₀ : s  x₀) (h₁ : s  x₁), x₀ = x₁

would have been better

Reid Barton (Apr 25 2020 at 16:29):

wait I think I translated it wrong

Reid Barton (Apr 25 2020 at 16:30):

structure {u} how_do_I_make_this_work : Prop:=
(out (G : Type u) [group G] (x : G) (hx : x * x = x) : x = 1)

Reid Barton (Apr 25 2020 at 16:32):

structure {u} SUBMISSION : Prop :=
(out {X : Type u} [h : metric_space X] {s :   X} (x₀ x₁ : X) (h₀ : s  x₀) (h₁ : s  x₁) : x₀ = x₁)

Reid Barton (Apr 25 2020 at 16:34):

You can also use Type* but in general I don't trust it

Kevin Buzzard (Apr 25 2020 at 16:37):

theorem submission : SUBMISSION := @limit_unique

will need to be changed as well I guess. I don't really know why they do it like this, it's to do with preventing some kind of cheating. I don't understand it well enough to know whether the switch to a structure will cause problems. I guess one just adds \< \>.


Last updated: Dec 20 2023 at 11:08 UTC