Prove length (h::l) = 1 + length l

Question

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.

I'm voting to close this question as off-topic because it's a math question, not a programming question. — wvdz
It's related to a programming course and its a proof of a program in ocaml. I disagree. — Connor
@wvdz see Type Theory: propositions are types, proofs are programs. Maybe add a Coq tag. — Str.

ivg ivg · Accepted Answer · 2015-11-25T12:57:45

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.

Prove length (h::l) = 1 + length l

2 Answers