def extending something else

Stream: new members

[Fox Thomson]

I am trying to make a set of classes that inherit from each other with the final one being inductive so cannot be defined as a normal class. I have already asked about this in the "dependent and" thread but I have since updated this so that the base class similar contains data. This did not cause any issues to shared as lean was able to figure out that I was using the same equivalence for the occurrences of similar but it is causing problems from impartial as I need to add an instance definition to be able to talk about things which depend on the other two definitions but then when I want to prove things I also need to show that two instances are the same:

class similar (G : pgame) := (similar_moves : G.left_moves ≃ G.right_moves)

-- This one can figure out it is similar by itself
class shared (G : pgame) extends similar G :=
(shared_moves : ∀ i : G.moves, G.move_left i ≈ G.move_right i)

-- This is the class which is causing problems
@[class] def impartial : pgame → Type _
| G := Σ [shared G],
            by exactI (∀ i : G.moves, impartial (G.move i))
using_well_founded { dec_tac := pgame.pgame_wf_tac }

-- This definition is required so that the next lemma compiles
@[instance] def impartial_shared (G : pgame) [h : impartial G] : shared G :=
begin
    unfold1 impartial at h,
    cases h,
    assumption
end

-- This gets an error at "exact h₂ i" saying "(@move G h₁ i).impartial" and "(@move G (@impartial_shared G h) i)" are not the same
@[instance] lemma impartial_move_impartial (G : pgame) [h : impartial G] (i : G.moves) : impartial (G.move i) :=
begin
    unfold1 impartial at h,
    casesI h with h₁ h₂,
    exact h₂ i
end

Ideally I would like to be able to write

class impartial (G : pgame) extends shared G :=
( impartial_moves : ∀ i : G.moves, impartial (G.move i) )

But I don't think there is any support for inductive class definitions.

[Reid Barton]

I would start by getting rid of all the classes

[Fox Thomson]

How come, they seemed to be making a lot of things easier.

[Reid Barton]

Well, clearly they aren't making this easier, right?

[Reid Barton]

In my experience classes are a convenience when they work well, and a nightmare when they don't. I'd at least try to express what you want without classes first, and then maybe consider using classes after that.

[Fox Thomson]

I will have a go, thank you!

[Reid Barton]

but really I think it's just better to aim for (G : impartial_pgame) than (G : pgame) [impartial G], anyways

[Reid Barton]

and then you might decide that an impartial_pgame doesn't really need to contain a pgame after all