Need help in proving involution in Lean4

Stream: new members

[Shubham Kumar 🦀 (he/him)]

so I have a function nSwap which takes a List Int and a swaps the first 2 elements so x :: y :: rest becomes y :: x :: rest
I want to prove involution in lean for this function, how to define the theorem because there is also an argument for program counter which is passed to the function which doesn't really have any role in this proof. So I am not sure how to "phrase" the proof for lack of a better word

the function nSwap is :

  def nSwap (s : Stack) (pc : Nat) : Stack × Nat :=
    match s with
    | [] => ([], pc)
    | x :: [] => ([x], pc)
    | x :: y :: xs => (y :: x :: xs, pc + 1)

it returns a cartesian product too which might cause a problem in proof as well

[Shubham Kumar 🦀 (he/him)]

here Stack is defined as def Stack := List Int

[Kevin Buzzard]

And can you formalise what you want to prove?

[Kevin Buzzard]

Oh I see -- that's the question? Why not state something about (nswap s pc).1?

[Shubham Kumar 🦀 (he/him)]

oh that's something I was looking for I am used to fst, yes that .1 seems like what I was looking for

[Shubham Kumar 🦀 (he/him)]

thanks @Kevin Buzzard

[Shubham Kumar 🦀 (he/him)]

I was able to formalise it :

  theorem involution_nswap (s : Stack) :
    Prod.fst (nSwap (Prod.fst $ nSwap s 0) 0) = s :=
  sorry

[Kevin Buzzard]

.fst should also work. .1 is a generic "first field of this structure even if I don't know the name" projection

[Kevin Buzzard]

You can use dot / projection notation to shorten the formalisation a bit: Prod.fst x is the same as x.fst and also as x.1 if x : Prod A B.

[Shubham Kumar 🦀 (he/him)]

yeah I saw Prod.fst by the vscode tooltip and then replaced it. It's a bad habit of mine to keep everything functional as much as possible to make sense for me. When I write the final proof I often replace that with the short notation. But I initially keep the semantics sane.

Thanks for the pointers @Kevin Buzzard but I don't know how to proceed further, Prod.casesOn seems like a function to eliminate cases

[Shubham Kumar 🦀 (he/him)]

but yeah I am stuck after formalisation of the proof

[Shubham Kumar 🦀 (he/him)]

Maybe I need something to break the = maybe something related to Eq

[Shubham Kumar 🦀 (he/him)]

for Lists

[Shubham Kumar 🦀 (he/him)]

is there a way to access stdlib, I cannot google or find it on lean4 (https://leanprover.github.io/) website

[Shubham Kumar 🦀 (he/him)]

to understand what I should do I turned that proposition into a function

  def f (s : Stack) : Prop :=
    ((nSwap (nSwap s 0).1 0).1) = s

  def stack_ex_1 : Stack := [1, 2, 3, 4]

  #eval f stack_ex_1

when I eval the function I am getting

failed to synthesize
  Decidable (f stack_ex_1)

what does this mean?

[Shubham Kumar 🦀 (he/him)]

Also I can't seem to unfold : unknown identifier 'unfold'
do I need to import something?

[Kevin Buzzard]

Did you take a look at Theorem Proving In Lean? You should be able to prove your result by induction on s. There are lots of basic examples on how to prove theorems about inductive types in there. I don't think you'll need std4, which you can find on the lean GitHub site next to lean4

[Kyle Miller]

@Shubham Kumar 🦀 (he/him) You can do the proof with cases twice:

def Stack := List Int

def nSwap (s : Stack) (pc : Nat) : Stack × Nat :=
  match s with
  | [] => ([], pc)
  | x :: [] => ([x], pc)
  | x :: y :: xs => (y :: x :: xs, pc + 1)

theorem involution_nswap (s : Stack) :
  Prod.fst (nSwap (Prod.fst $ nSwap s 0) 0) = s :=
by
  cases s with
  | nil => rfl
  | cons x xs =>
    cases xs with
    | nil => rfl
    | cons y xs => rfl

That's using a structured style.

[Kyle Miller]

You can also give the proof as a functional program using match, following the cases of nSwap:

theorem involution_nswap (s : Stack) :
  Prod.fst (nSwap (Prod.fst $ nSwap s 0) 0) = s :=
  match s with
  | [] => rfl
  | _ :: [] => rfl
  | _ :: _ :: _ => rfl

[Kyle Miller]

Shubham Kumar 🦀 (he/him) said:

when I eval the function I am getting

failed to synthesize
  Decidable (f stack_ex_1)

what does this mean?

The Prop type is sort of like Bool, and in fact there's a bijective function Bool -> Prop, but there's not a general algorithm for the inverse function Prop -> Bool. If there were, you could just #eval riemann_hypothesis and wait for the answer.

The Decidable typeclass is essentially a way to partially evaluate this function, where for individual values of p : Prop you record whether it's true or false. When you write #eval f stack_ex_1 I guess there's a Lean 4 feature that invokes this system to try to turn f stack_ex_1 into a Bool. But, you haven't written a Decidable instance for this term, so you get the error.

[Kyle Miller]

If you change the defintion to abbrev Stack := List Int and change f to return a Bool rather than a Prop, while being sure to use the Bool-valued equality, then you can get it to work:

def f (s : Stack) : Bool :=
  ((nSwap (nSwap s 0).1 0).1) == s

def stack_ex_1 : Stack := [1, 2, 3, 4]

#eval f stack_ex_1
-- true