How to prove in HOLCF that double reversion of a list doesn't change it

Question

Here is a simple theory written on the plain HOL:

theory ToyList
  imports Main
begin

no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
hide_type list
hide_const rev

datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)

primrec snoc :: "'a list => 'a => 'a list" (infixr "#>" 65)
  where
    "[] #> y = y # []" |
    "(x # xs) #> y = x # (xs #> y)"

primrec rev :: "'a list => 'a list"
  where
    "rev [] = []" |
    "rev (x # xs) = (rev xs) #> x"

lemma rev_snoc [simp]: "rev(xs #> y) = y # (rev xs)"
  apply(induct_tac xs)
  apply(auto)
done

theorem rev_rev [simp]: "rev(rev xs) = xs"
  apply(induct_tac xs)
  apply(auto)
done

end

snoc is an opposite of cons. It adds an item to the end of the list.

I want to prove a similar lemma via HOLCF. At a first stage I consider only strict lists. I declared the domain of strict lists in HOLCF. Also I declared two recursive functions:

• ssnoc - appends an item to the end of a list
• srev - reverses a list

Prefix s means "strict".

theory Test
  imports HOLCF
begin

domain 'a SList = SNil | SCons "'a" "'a SList"

fixrec ssnoc :: "'a SList → 'a → 'a SList"
  where
    "ssnoc ⋅ SNil ⋅ x = SCons ⋅ x ⋅ SNil" |
    "ssnoc ⋅ ⊥ ⋅ x = ⊥" |
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ ssnoc ⋅ (SCons ⋅ x ⋅ xs) ⋅ y = SCons ⋅ x ⋅ (ssnoc ⋅ xs ⋅ y)"

fixrec srev :: "'a SList → 'a SList"
  where
    "srev ⋅ ⊥ = ⊥" |
    "srev ⋅ SNil = SNil" |
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ srev ⋅ (SCons ⋅ x ⋅ xs) = ssnoc ⋅ (srev ⋅ xs) ⋅ x"

lemma srev_singleton [simp]:
  "srev ⋅ (SCons ⋅ a ⋅ SNil) = SCons ⋅ a ⋅ SNil"
  apply(induct)
  apply(simp_all)
done

lemma srev_ssnoc [simp]:
  "srev ⋅ (ssnoc ⋅ xs ⋅ a) = SCons ⋅ a ⋅ (srev ⋅ xs)"
  apply(induct xs)
  apply(simp_all)
done

lemma srev_srev [simp]:
  "srev ⋅ (srev ⋅ xs) = xs"
  apply(induct xs)
  apply(simp_all)
done

end

I'm trying to prove that double reversion of the list equals to the original list (srev_srev lemma). I have declared two helper lemmas:

• srev_singleton - reverse of the singleton list is the original singleton list
• srev_ssnoc - reversion of the list equals to the list starting from the last item of the original list appending reversion of the rest items of the original list

But I can't prove any of the lemmas. Could you point out the errors?

Also why the precondition "x ≠ ⊥ ∧ xs ≠ ⊥" is necessary in the function definitions? And why should I declare "srev ⋅ ⊥ = ⊥" and "ssnoc ⋅ ⊥ ⋅ x = ⊥" explicitly. I guess that in HOLCF by default functions are undefined if any of the arguments is undefined.

Answer 1

If your intention is to model lists a la Haskell (aka "lazy lists"), then you should use something like:

domain 'a list = Nil ("[]") | Cons (lazy 'a) (lazy "'a list") (infix ":" 65)

(note the "lazy" annotations for Cons). Then you do not need the assumptions on your third equation. E.g.,

fixrec append :: "'a list → 'a list → 'a list"
  where
    "append $ [] $ ys = ys"
  | "append $ (x : xs) $ ys = x : (append $ xs $ ys)"

for what you called ssnoc and

fixrec reverse :: "'a list → 'a list"
  where
    "reverse $ [] = []"
  | "reverse $ (x : xs) = append $ xs $ (x : [])"

for reverse.

However, since this type of lists allows for "infinite" values, you will not be able to prove that reverse $ (reverse $ xs) = xs hold in general (because it doesn't). This only holds for finite lists, which can be characterized inductively. (See, e.g., https://arxiv.org/abs/1306.1340 for a more detailed discussion.)

If, however, you do not want to model lazy lists (i.e., really don't want the "lazy" annotations in your datatype), then your equations might not hold without the assumptions. Now if the equations have those assumptions, they can only be applied in cases where the assumptions are satisfied. So gain, you will not be able to proof (without additional assumptions) that reverse $ (reverse $ xs) = xs. It might again be possible to obtain the appropriate assumptions by an inductive predicate, but I did not investigate further.

Update: After playing a bit with strict lists in HOLCF, I have some more comments:

First, my guess is that the preconditions in the fixrec specifications are necessary due to the internal construction, but we are able to get rid of them afterwards.

I managed to prove your lemma as follows. For completeness I give the whole content of my theory file. First make sure that notation doesn't clash with existing one:

no_notation
  List.Nil ("[]") and
  Set.member ("op :") and
  Set.member ("(_/ : _)" [51, 51] 50)

Then define the type of strict lists

domain 'a list = Nil ("[]") | Cons 'a "'a list" (infixr ":" 65)

and the function snoc.

fixrec snoc :: "'a list → 'a → 'a list"
  where
    "snoc $ [] $ y = y : []"
  | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ snoc $ (x:xs) $ y = x : snoc $ xs $ y"

Now, we obtain an unconditional variant of the second equation by:

1. Showing that snoc is strict in its first argument (note the usage of fixrec_simp).
2. Showing that snoc is strict in its second argument (here induction is needed).
3. And finally, obtaining the equation by case analysis on all three variables.

lemma snoc_bot1 [simp]: "snoc $ ⊥ $ y = ⊥" by fixrec_simp
lemma snoc_bot2 [simp]: "snoc $ xs $ ⊥ = ⊥" by (induct xs) simp_all
lemma snoc_Cons [simp]: "snoc $ (x:xs) $ y = x : snoc $ xs $ y"
  by (cases "x = ⊥"; cases "xs = ⊥"; cases "y = ⊥";simp)

Then the function reverse

fixrec reverse :: "'a list → 'a list"
  where
    "reverse $ [] = []"
  | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ reverse $ (x : xs) = snoc $ (reverse $ xs) $ x"

and again an unconditional variant of its second equation:

lemma reverse_bot [simp]: "reverse $ ⊥ = ⊥" by fixrec_simp
lemma reverse_Cons [simp]: "reverse $ (x : xs) = snoc $ (reverse $ xs) $ x"
  by (cases "x = ⊥"; cases "xs = ⊥"; simp)

Now the lemma about reverse and snoc you also had:

lemma reverse_snoc [simp]: "reverse $ (snoc $ xs $ y) = y : reverse $ xs"
  by (induct xs) simp_all

And finally the desired lemma:

lemma reverse_reverse [simp]:
  "reverse $ (reverse $ xs) = xs"
  by (induct xs) simp_all

The way I obtained this solution was by just looking into the remaining subgoals of your failed attempts, then get more failed attempts, look into the remaining subgoals, repeat, ...