undesired solution to [exercises/concept/pacman-rules]

[TressaDanvers]

There is a valid solution to the win function in the Pacman Rules exercise which is as follows:

pub fn win(
  has_eaten_all_dots: Bool,
  power_pellet_active: Bool,
  touching_ghost: Bool,
) -> Bool {
  has_eaten_all_dots && { power_pellet_active == touching_ghost }
}

As you can see, this is not equivalent to the intended solution of:

pub fn win(
  has_eaten_all_dots: Bool,
  power_pellet_active: Bool,
  touching_ghost: Bool,
) -> Bool {
  has_eaten_all_dots && !lose(power_pellet_active, touching_ghost)
}

If we expand that solution out we get:

pub fn win(
  has_eaten_all_dots: Bool,
  power_pellet_active: Bool,
  touching_ghost: Bool,
) -> Bool {
  has_eaten_all_dots && !{ !power_pellet_active && touching_ghost }
}

a ∧ (b ↔ c) is not equivalent to a ∧ !(!b ∧ c).