Help representing a system

Stream: lean4

[Jesse Slater]

I am trying to figure out the best way to represent a system. I am currently representing it with Nat x Nat, but (0, 0) is invalid. I am getting around that by just assuming in all of my theorems that the state is not (0,0). Is there any better way I could represent the system to avoid this? In the future I will generalize this to more dimensions, and I will likely end up having more invalid states, but it will always be a small finite number. Is there a good way to represent this more general case??

[Eric Wieser]

You could represent your system with a docs4#Subtype, but that's essentially the same as your current approach of passing around a proof that the state is not zero. All that changes is you now you pass it around in one argument instead of two.

[Chris Bailey]

Sometimes it's convenient to make your own subtype, as in Fin.

structure MyState where
  x : Nat
  y : Nat
  hx : 0 < x
  hy : 0 < y

[Chris Bailey]

You might also get some inspiration from the std definition of RBMap, where they have a base type and then a subtype using an inductive prop to describe the well-formed states.