## Thursday, May 11, 2017

### Proving a mem/map property

Here are two well known "classic" functions over polymorphic lists.

map f l computes a new list from l by applying f to each of its elements.

let rec map (f : 'a -> 'b) : 'a list -> 'b list = function
| [] -> []
| h :: t -> f h :: map f t
;;


mem x l returns true is x is an element of l and returns false if it is not.

let rec mem (a : 'a) : 'a list -> bool  = function
| [] -> false
| x :: l -> a = x || mem a l
;;


If y is an element of the list obtained by mapping f over l then there must be an element x in l such that f x = y. Conversely, if there exists an x in l such that y = f x, then y must be a member of the list obtained by mapping f over l.

We attempt a proof of correctness of the given definitions with respect to this property.

Lemma mem_map_iff:

∀ (f : α → β) (l : α list) (y : β),
mem y (map f l) ⇔ ∃(x : α), f x = y ∧ mem x l.

Proof:
• We first treat the forward implication
          
∀ (f : α → β) (l : α list) (y : β),
mem y (map f l) ⇒ ∃(x : α), f x = y ∧ mem x l

and proceed by induction on l.

• l = []:
• Show mem y (map f []) ⇒ ∃(x : α), f x = y ∧ mem x [].
• mem y (map f []) ≡ False.
• Proof follows (ex falso quodlibet).

• l has form x' :: l (use l now to refer to the tail):
• Assume the induction hypothesis:
• mem y (map f l) ⇒ ∃x, f x = y ∧ mem x l.
• We are required to show for an arbitrary (x' : α):
• mem y (map f (x' :: l)) ⇒ ∃(x : α), f x = y ∧ mem x (x' :: l).
• By simplification, we can rewrite the above to:
• f x' = y ∨ mem y (map f l) ⇒ ∃(x : α), f x = y ∧ (x' = x ∨ mem x l).
• We assume then an (x' : α) and a (y : β) such that:
1. f x' = y ∨ mem y (map f l).
2. mem y (map f l) ⇒ ∃(x : α), f x = y ∧ mem x l.
• Show ∃(x : α), f x = y ∧ (x' = x ∨ mem x l):
• First consider f x' = y in (1).
• Take x = x' in the goal.
• Then by (1) f x = y ∧ x = x'.
• So x' is a witness.
• Now consider mem y (map f l) in (1).
• ∃(x* : α), f x* = y ∧ mem x* l by (2).
• Take x = x* in the goal.
• By the above f x* = y ∧ mem x* l
• So x* is a witness.

• We now work on the reverse implication. We want to show that

∀ (f : α → β) (l : α list) (y : β),
∃(x : α), f x = y ∧ mem x l ⇒ mem y (map f l)

and proceed by induction on l.

• l = []:
• Assume x, y with f x = y ∧ mem x [].
• Show mem y (map f []):
• mem x [] ≡ false.
• Proof follows (ex falso quodlibet).
• l has form x' :: l (use l now to refer to the tail):
• Assume the induction hypothesis:
• ∃(x : α), f x = y ∧ mem x l ⇒ mem y (map f l).
• We are required to show for an arbitrary (x' : α):
• ∃ (x : α), f x = y ∧ mem x (x' :: l) ⇒ mem y (map f (x' :: l))
• By simplification, we can rewrite the above to:
• ∃ (x : α), f x = y ∧ x = x' ∨ mem x l ⇒ f x' = y ∨ mem y (map f l).
• Assume the goal and induction hypotheses:
• There is (x : α) and (y : β) such that:
1. f x = y ∧ (x = x' ∨ mem x l)
2. f x = y ∧ mem x l ⇒ mem y (map f l)
• Show f x' = y ∨ mem y (map f l):
• Assume x = x' in (1) and show f x' = y:
• Since, f x = y is given by (1.), f x' = y.
• Assume mem x l in (1) and show mem y (map f l):
• Rewrite mem y (map f l) via (2) to f x = y ∧ mem x l.
• f x = y by (1) so mem y (map f l).

References:
"Sofware Foundations" -- Pierce et. al.