solitaire undo

Stream: lean4

[Locria Cyber]

I have modeled a simple solitaire logic where you can put any cards anywhere.

I want to prove that every valid action can be undone. It's trivial to understand, but is hard to prove in Lean.

Code:

inductive Suit
| A
| B
| C
| D

structure Card where
  suit: Suit
  value: Nat

abbrev Track := List Card

def List.splitAt? : (n: Nat) -> (l: List α) -> Option (List α × List α)
| 0, l => .some ([], l)
| .succ _, [] => .none
| .succ i, (x :: xs) => do
  let (splited, xs') <- splitAt? i xs
  (x :: splited, xs')

def Fin.ofNat? (x: Nat) : Option (Fin n) :=
  if isLt : x < n then
    .some <| Fin.mk x isLt
  else
    .none

structure Deck where
  tracks: Array Track

inductive Action
/-- Move `amount` cards from track to track -/
| move (from_track: Nat) (to_track: Nat) (amount: Nat)

def Action.reverse : Action -> Action
| .move from_ to_ amt => .move to_ from_ amt

namespace Deck

def do? (deck: Deck) : (action: Action) -> Option Deck
| .move from_track to_track amount => do
  let from_track <- Fin.ofNat? from_track

  let tracks := deck.tracks
  let (taken, modified_track) <- tracks[from_track].splitAt? amount
  let tracks := tracks.set from_track modified_track
  let to_track <- Fin.ofNat? to_track
  let tracks := tracks.set to_track (List.append taken tracks[to_track])
  .some { tracks := tracks }

/-- valid Action are reversible -/
theorem biject_valid :
  do? deck action = some deck' ->
  do? deck' (action.reverse) = some deck
:= by sorry -- no idea how to prove this

theorem biject (deck: Deck) (action: Action)
: match do? deck action with
  | .none => True
  | .some deck' => do? deck' action.reverse = .some deck
:=match h: do? deck action with
  | .none => True.intro
  | .some _deck' => biject_valid h

end Deck

[Locria Cyber]

Also, is there a way to do property testing in Lean?

[Andrés Goens]

Locria Cyber said:

Also, is there a way to do property testing in Lean?

have you seen LSpec/SlimCheck? https://github.com/lurk-lab/LSpec

[Locria Cyber]

Andrés Goens said:

Locria Cyber said:

Also, is there a way to do property testing in Lean?

have you seen LSpec/SlimCheck? https://github.com/lurk-lab/LSpec

no. thanks! I'll try it out

[Locria Cyber]

On match unification

For some reason, this is not type checking

abbrev biject_T (deck: Deck) (action: Action) :=
match do? deck action with
  | .none => True
  | .some deck' => do? deck' action.reverse = Option.some deck

def biject (deck: Deck) (action: Action)
: biject_T deck action
:=
  match h: do? deck action with
  | .none => True.intro
  | .some _deck' => biject_valid h

Isn't abbrev suppose to expand biject_T deck action?

The if I manually expand the expression biject_T deck action it works (see first code sample of this thread).

[Sebastian Ullrich]

No, abbrev does not immediately expand to its definition, it merely makes the definition always reducible (especially under typeclass search, unlike def). But the discriminant generalization of match works basically syntactically, without reduction.

[Locria Cyber]

Sebastian Ullrich said:

No, abbrev does not immediately expand to its definition, it merely makes the definition always reducible (especially under typeclass search, unlike def). But the discriminant generalization of match works basically syntactically, without reduction.

How do I make it expand when used as type?

[Mac Malone]

(edit: forget what I said; I misunderstood what you wanted)