Zulip Chat Archive

Stream: new members

Topic: Need help in proving involution in Lean4


Shubham Kumar 🦀 (he/him) (Oct 30 2022 at 07:22):

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) (Oct 30 2022 at 07:23):

here Stack is defined as def Stack := List Int

Kevin Buzzard (Oct 30 2022 at 07:34):

And can you formalise what you want to prove?

Kevin Buzzard (Oct 30 2022 at 07:35):

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

Shubham Kumar 🦀 (he/him) (Oct 30 2022 at 07:49):

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) (Oct 30 2022 at 07:49):

thanks @Kevin Buzzard

Shubham Kumar 🦀 (he/him) (Oct 30 2022 at 08:44):

I was able to formalise it :

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

Kevin Buzzard (Oct 30 2022 at 08:46):

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

Kevin Buzzard (Oct 30 2022 at 08:47):

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) (Oct 30 2022 at 08:56):

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) (Oct 30 2022 at 08:58):

but yeah I am stuck after formalisation of the proof

Shubham Kumar 🦀 (he/him) (Oct 30 2022 at 08:59):

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

Shubham Kumar 🦀 (he/him) (Oct 30 2022 at 08:59):

for Lists

Shubham Kumar 🦀 (he/him) (Oct 30 2022 at 09:08):

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

Shubham Kumar 🦀 (he/him) (Oct 30 2022 at 09:52):

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) (Oct 30 2022 at 09:58):

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

Kevin Buzzard (Oct 30 2022 at 11:20):

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 (Oct 30 2022 at 11:48):

@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 (Oct 30 2022 at 11:49):

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 (Oct 30 2022 at 11:54):

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 (Oct 30 2022 at 11:56):

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

Last updated: Dec 20 2023 at 11:08 UTC