Zulip Chat Archive

Stream: new members

Topic: Dependent and


view this post on Zulip 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)

view this post on Zulip Kenny Lau (Jul 03 2020 at 11:02):

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

view this post on Zulip Fox Thomson (Jul 03 2020 at 11:09):

Thank you!

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:31):

did you want is_group instead of group?

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:31):

group A is not a Prop

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:33):

I think you have an #xy problem

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:44):

could you show your code?

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:45):

(btw abelian_group in mathlib is called comm_group)

view this post on Zulip 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 }

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:49):

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

view this post on Zulip Fox Thomson (Jul 03 2020 at 11:50):

Thank you!

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:51):

moves has an unnecessary typeclass argument

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:52):

It probably could, but it doesn't try

view this post on Zulip Mario Carneiro (Jul 03 2020 at 11:53):

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

view this post on Zulip Kevin Buzzard (Jul 03 2020 at 11:53):

Isn't this called impartial_game or something?

view this post on Zulip Fox Thomson (Jul 03 2020 at 11:55):

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

view this post on Zulip Reid Barton (Jul 03 2020 at 12:38):

Probably pgame.similar

view this post on Zulip 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?

view this post on Zulip 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