Auto eliminate match

Stream: lean4

[Henrik Böving]

I'm currently implementing some zipper datastructure on a tree for my tableaux prover. I got these types:

inductive Tableau (α : Type u) where
  | tip (data : α) : Tableau α
  | inner (data : α) (children : List (Tableau α)) : Tableau α
  deriving Repr, Inhabited, BEq

inductive Path (α : Type u) where
  | top : Path α
  | node (invLefts : List (Tableau α)) (parentPath : Path α) (parentData : α) (rights : List (Tableau α)) : Path α
  deriving Repr, Inhabited, BEq

structure Location (α : Type u) where
  focus : Tableau α
  parent : Path α
  deriving Repr, Inhabited, BEq

and am defining a function goLeft that should shift the focus from the current node to its left partner like so:

open Location Tableau Position

def goLeft! [Inhabited α] (loc : Location α) : Location α :=
  match loc.parent with
  | top => panic! "Can't visit left of top"
  | node [] up data right => panic! "Can't visit left of first"
  | node (l::left) up data right => ⟨l, node left up data (loc.focus::right)⟩

which is basically the exact same function as in the original zipper paper...however I would like to also have a proof based one that doesnt panic just like List.get and get! so I wrote:

def goLeft (loc : Location α) (h : loc.parent = node (l::left) up data right) : Location α :=
  match loc.parent with
  | node (l::left) up data right => sorry

but its requiring me to still fill out more cases here which I will of course be able to just prove False from and eliminate by hand but I was wondering whether there would be a more automated way to do this?

[Henrik Böving]

Hm I guess I could also just:

def goLeft (loc : Location α) (h : loc.parent = node (l::left) up data right) : Location α :=
  ⟨l, node left up data (loc.focus::right)⟩

?

[Henrik Böving]

Also I have a slight doubt this is actually the proof I want to get passed? I mean sure it works out like this but is my API actually reasonable/usable like this? My idea was that this proof could be generated if you are matching on loc.parent yourself but maybe that's not actually how this data structure should be used? I'm unsure about that as well

[Arthur Paulino]

What is Position?

[Henrik Böving]

Oh sorry, that is supposed to be Path

[Henrik Böving]

Corrected!

[Arthur Paulino]

May I question your types?

[Arthur Paulino]

The reason I'd question your types is because I suspect it's possible to simplify the API

[Henrik Böving]

I did remove the tip part by now yeah

[Henrik Böving]

that makes things easier

[Henrik Böving]

But sure go ahead

[Arthur Paulino]

It's just that I see three lists in your types and it made me think that ensuring cohesion might be a bit painful. The question is: how do you make sure that every Tableau α in invLefts and rights has the same parent?

[Henrik Böving]

The nodes in there are just sub trees, the parent is stored seperately and while traversing through the zipper the nodes and parent get updated accordingly so this is not really an issue

[Arthur Paulino]

If you don't ensure that structurally, I think your functions will end up needing hypotheses like that h

[Henrik Böving]

As long as the user uses the API the structure will just remain consistent i dont really see your point?

[Chris B]

I think you're supposed to use dependent pattern matching. This is a little bootleg since you didn't give all the variables, but:

variable
  (left right : List <| Tableau α)
  (up parent : Path α)
  (data : α)
def goLeft (l : Tableau α) (h : parent = node (l::left) up data right) : Nat :=
  match parent, h with
  | node (l::left) up data right, _ => 0

[Henrik Böving]

ahhhhh, I thought it would just understand that automatically

[Arthur Paulino]

(I'm learning as I talk, sorry and please let me know if I'm bothering you :sweat_smile:)
I was talking about these two approaches:

def List.ascending [LE α] : List α → Prop
  | a :: b :: t => a ≤ b ∧ ascending (b :: t)
  | _ => True

structure NonEmptyAscendingList (α : Type) [LE α] where
  data : List α
  nonEmpty : data ≠ []
  ascending : data.ascending

def NonEmptyAscendingList.getLeast {α : Type} [LE α] : NonEmptyAscendingList α → α
  | ⟨[], h, _⟩     => by simp at h
  | ⟨h :: _, _, _⟩ => h

def getLeast {α : Type} [LE α] (l : List α) (h : l ≠ []) (ha : l.ascending) : α :=
  match l with
  | [] => by simp at h
  | h :: _ => h

NonEmptyAscendingList has its hypotheses as structure fields so NonEmptyAscendingList.getLeast can be implemented with less parameters. Whereas getLeast needs the hypotheses everytime.
(ignore the fact that ha is not being used in this example, but suppose it was)

[Henrik Böving]

This can work out here yes, but for a zipper the situation of the left list being empty or the right list being empty and in fact also the situation of both lists being empty is a valid state so there is no invariants I can require at construction time, whether the structure is valid or not depends on its use, they can only be used in a wrong way, not constructed.