I have trouble with these proofs that seem almost trivially obvious.
For instance, in the inductive case if I assume the property in the title and I want to show:
length (h'::h::l) = 1 + length (h::l)
Where do I go from here? It is so obviously true but I don't know what steps I can take without proving some kind of lemma. For instance I could say
length ([h']@(h::l)) = 1 + length (h::l)
But now I have to prove something along the lines of
length (l1@l2) = length l1 + length l2
I'm having trouble understanding when I need to prove lemmas, especially in the proofs that seem almost trivial.
When you prove program correctness, you're usually working with some implementation. If you will take a trivial implementation, then the proof would be also trivial. Suppose we have the following implementation:
let rec length = function
| [] -> 0
| x::xs -> 1 + length xs
We have a proof obligation:
length (x::xs) = 1 + length xs
We proof this using structural induction. I'm assuming, that list is defined as
type 'a list =
| Nil
| Cons ('a,'a list)
and [] is a syntactic sugar for Nil, while x::xs is a syntactic sugar for Cons (x,xs)
So we perform case by case analysis. We have only one applicable case, so we take case
| x::xs -> 1 + length xs
rewrite length (x::xs) with the right hand side, and we get:
1 + legnth xs = 1 + length xs
This can be proven by reflexivity of = operator. (If it is reflexive in your logic).
Note: the above implementation is trivial. In OCaml standard library List.length is implemented as follows:
let rec length_aux len = function
[] -> len
| a::l -> length_aux (len + 1) l
let length l = length_aux 0 l
Here proof obligation length (x::xs) = 1 + length xs produces an obligation to proof that length_aux 0 (x::xs) = 1 + length_aux 0 xs. This is less trivial.