Shayne Fletcher: 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 []):
- 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.

Thursday, May 11, 2017

Proving a `mem`/`map` property