Dependent and

Stream: new members

[Fox Thomson]

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]

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

[Fox Thomson]

Thank you!

[Fox Thomson]

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]

did you want is_group instead of group?

[Mario Carneiro]

group A is not a Prop

[Mario Carneiro]

I think you have an #xy problem

[Fox Thomson]

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]

could you show your code?

[Mario Carneiro]

(btw abelian_group in mathlib is called comm_group)

[Fox Thomson]

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]

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

[Fox Thomson]

Thank you!

[Mario Carneiro]

moves has an unnecessary typeclass argument

[Kenny Lau]

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]

It probably could, but it doesn't try

[Mario Carneiro]

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

[Kevin Buzzard]

Isn't this called impartial_game or something?

[Fox Thomson]

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

[Reid Barton]

Probably pgame.similar

[Eric Wieser]

Mario Carneiro said:

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

Whats the relevance of making similar_game a Prop?

[Utensil Song]

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.