Stream: new members

Topic: def extending something else

Fox Thomson (Jul 15 2020 at 13:28):

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 (Jul 15 2020 at 13:38):

I would start by getting rid of all the classes

Fox Thomson (Jul 15 2020 at 13:40):

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

Reid Barton (Jul 15 2020 at 13:42):

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

Reid Barton (Jul 15 2020 at 13:43):

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 (Jul 15 2020 at 13:48):

I will have a go, thank you!

Reid Barton (Jul 15 2020 at 14:04):

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

Reid Barton (Jul 15 2020 at 14:04):

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

Last updated: May 18 2021 at 17:44 UTC