Recursion to Induction

A worked solution is below!

Problem 2: On Your Own

Consider the following Python function:

(define any
  (lambda (f l)
    (match l
      ['() #f]
      [(cons head tail)
       (or (f head) (any f tail))])))

For the following claim, write a formal proof of the claim.

Claim

For any list l, (any (lambda (v) #f) l) ≡ #f.

Proof

We will proceed through induction on the structure of the list l.

Base Case: let l be null. Then the LHS traces as
(any (lambda (v) #f) null)
-->* #f
Since the LHS evaluates to the RHS, they are equivalent in this case.

Induction Hypothesis: Consider the arbitrary list l = (cons head tail), and assume that (any (lambda (v) #f) tail) ≡ #f.

Inductive Step: Now consider the claim for this arbitrary list l = (cons head tail):
(any (lambda (v) #f) l) ≡ #f.

The LHS traces as
(any (lambda (v) #f) l)
-->* (or ((lambda (v) #f) head) (any (lambda (v) #f) tail))
--> (or #f (any (lambda (v) #f) tail))
--> (any (lambda (v) #f) tail)

By the Induction Hypothesis, we know that (any (lambda (v) #f) tail) ≡ #f, and therefore the LHS evaluated to #f.

Since the LHS evaluated to the RHS, they are equivalent.

Thus (any (lambda (v) #f) l) ≡ #f for any list l.