## Stream: new members

### Topic: Dependent and

#### Fox Thomson (Jul 03 2020 at 11:00):

How do I say I want two statements P and Q to be true where I am using properties that depend on P in Q, for example, if I was to define something like

def is_abelian_group (α : Type _) : α → Prop := is_group α ∧ (∀ g h : α, g*h = h*g)


#### Kenny Lau (Jul 03 2020 at 11:02):

def is_abelian_group (α : Type _) : Prop := ∃ [is_group α], by exactI (∀ g h : α, g*h = h*g)


Thank you!

#### Fox Thomson (Jul 03 2020 at 11:29):

I am now having trouble using this, I want to be able to say

import algebra.group

def is_abelian_group (α : Type) : Prop := ∃ [group α], by exactI (∀ g h : α, g*h = h*g)

lemma abelian_group_is_group (α : Type) : is_abelian_group α → group α :=
begin
intro h,
unfold is_abelian_group at h,
casesI h with hgroup habelian,
assumption
end


However, I get the error "induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop"

#### Mario Carneiro (Jul 03 2020 at 11:31):

did you want is_group instead of group?

#### Mario Carneiro (Jul 03 2020 at 11:31):

group A is not a Prop

#### Mario Carneiro (Jul 03 2020 at 11:33):

I think you have an #xy problem

#### Fox Thomson (Jul 03 2020 at 11:39):

What I was trying to do was to define a class on pgames which inducts on itself and also depended on another class, class does not seem to allow for inductive definitions so I was defining in the form pgame → Prop and using well founded recursion

#### Mario Carneiro (Jul 03 2020 at 11:45):

(btw abelian_group in mathlib is called comm_group)

#### Fox Thomson (Jul 03 2020 at 11:47):

class similar_game (G : pgame) := (similar_moves : G.left_moves = G.right_moves)

def moves (G : pgame) [similar_game G] : Type u := G.left_moves
def moves_to_left_moves (G : pgame) [similar_game G] : G.moves → G.left_moves := id
def moves_to_right_moves (G : pgame) [h:similar_game G] : G.moves → G.right_moves :=
begin
rw ←h.similar_moves,
exact id
end
instance moves_to_left_moves_coe (G : pgame) [similar_game G] : has_coe G.moves G.left_moves :=
⟨ moves_to_left_moves G ⟩
instance moves_to_right_moves_coe (G : pgame) [similar_game G] : has_coe G.moves G.right_moves :=
⟨ moves_to_right_moves G ⟩

@[class] def impartial : pgame → Prop
| G := ∃ [similar_game G],
by exactI (∀ i : G.moves, G.move_left i = G.move_right i ∧
∃ [similar_game (G.move_left i)], impartial (G.move_left i))
using_well_founded { dec_tac := pgame.pgame_wf_tac }


#### Mario Carneiro (Jul 03 2020 at 11:49):

class similar_game (G : pgame) : Prop := ...

Thank you!

#### Mario Carneiro (Jul 03 2020 at 11:51):

moves has an unnecessary typeclass argument

#### Kenny Lau (Jul 03 2020 at 11:51):

Mario Carneiro said:

class similar_game (G : pgame) : Prop := ...

this is very unfortunate. why can't Lean figure out that it's a Prop?

#### Mario Carneiro (Jul 03 2020 at 11:52):

It probably could, but it doesn't try

#### Mario Carneiro (Jul 03 2020 at 11:53):

If you put #lint at the bottom it will tell you about unnecessary arguments

#### Kevin Buzzard (Jul 03 2020 at 11:53):

Isn't this called impartial_game or something?

#### Fox Thomson (Jul 03 2020 at 11:55):

Which would be the better convention, similar and impartial or similar_game and impartial_game?

#### Reid Barton (Jul 03 2020 at 12:38):

Probably pgame.similar

#### Eric Wieser (Jul 03 2020 at 13:59):

Mario Carneiro said:

class similar_game (G : pgame) : Prop := ...

Whats the relevance of making similar_game a Prop?

#### Utensil Song (Jul 03 2020 at 14:14):

I think its because "induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop" wants a Prop. And Lean chooses not to infer a "Prop class" for (maybe) performance reason.

Last updated: May 09 2021 at 19:11 UTC