class instances in definition of Prop

Stream: general

[Kenny Lau]

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]

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]

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]

See the mess I got into at codewars

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

@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]

I inserted the instances manually...

[Reid Barton]

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]

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) :=
∀ (ε : ℝ) (hε : 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]

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]

wait I think I translated it wrong

[Reid Barton]

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]

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]

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

[Kevin Buzzard]

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 \< \>.