len.z3

(declare-fun len    ((List Int))            Int)
(declare-fun append ((List Int) (List Int)) (List Int))

(declare-const xs (List Int))
(declare-const ys (List Int))

; len defining equations
(assert (forall ((xs (List Int)))
  (= (len xs)
     (ite (= xs nil) 0 (+ 1 (len (tail xs)))))))

; append defining equations
(assert (forall ((xs (List Int)) (ys (List Int)))
  (= (append xs ys)
     (ite (= nil xs)
          ys
          (insert (head xs) (append (tail xs) ys))))))

; let's show something simple: len l >= 0
(push)
  (define-fun lt ((l1 (List Int)) (l2 (List Int))) Bool
    (= l1 (tail l2)))
  (define-fun p ((l (List Int))) Bool
    (<= 0 (len l)))

  (push)
    ; len induction hypotheses
    (assert (not
      (=>
        (and
          (forall ((k (List Int)))
            (=> (lt k xs) (p k)))
          (= xs nil))
        (p xs))))
    (check-sat)
  (pop)

  (push)
    (assert (not
      (=>
        (and
          (forall ((k (List Int)))
            (=> (lt k xs) (p k)))
          (exists ((z Int) (zs (List Int)))
            (and (= (head xs) z) (= (tail xs) zs))))
        (p xs))))
    (check-sat)
  (pop)
(pop)

(push)
  (define-fun lt ((l1 (List Int)) (l2 (List Int))) Bool
    (= l1 (tail l2)))
  (define-fun p ((l1 (List Int)) (l2 (List Int))) Bool
    (= (len (append l1 l2)) (+ (len l1) (len l2))))

  ; base case

  ; it's tempting to have a base case of xs = [] and ys = []
  ; and induction on both xs and ys. we'll show why this is bad below
  (push)
    (assert (not
      (=>
        (and (= xs nil) (= ys nil))
        (p xs ys))))
    (check-sat)
  (pop)

  ; here's our actual base case
  (push)
    (assert (not
      (=>
        (= xs nil)
        (p xs ys))))
    (check-sat)
  (pop)

  ; induction for xs
  (push)
    (assert (not
      (=>
        (forall ((k (List Int)))
          (=> (lt k xs) (p k ys)))
        (p xs ys))))
    (check-sat)
  (pop)

  ; trying to do the induction on ys fails. this wil hang forever. this is
  ; similar to how in a real proof you'd do the induction over just xs.
  (push)
    (set-option :timeout 1000)
    (assert (not
      (=>
        (forall ((k (List Int)))
          (=> (lt k ys) (p xs k)))
        (p xs ys))))
    (check-sat)
  (pop)

  ; now we've proved this by induction and can assume it
  (assert (p xs ys))
(pop)