Propositional programming

The logical connectives we have seen provide a rich vocabulary for defining complex propositions from simpler ones. To illustrate, let's see how to express the statement that an element x occurs in a List l. Note that this property has a simple recursive structure:

  • If l is the empty list, then x cannot occur in it, so the property "x appears in l" is simply false.
  • Otherwise, l has the form List.cons head tail. In this case, x occurs in l if it is equal to head or if it occurs in tail.

We can translate this directly into a simple recursive function that takes an element and a List and returns a proposition:

In <a> (x: a) (l: List a)    : Type
In a x List.nil              = Empty
In a x (List.cons head tail) = Either (Equal a x head) (In a x tail)

When In is applied to a concrete list, it expands into a concrete sequence of nested disjunctions.

In_example_1 : In 4n [1n, 2n, 3n, 4n, 5n]
In_example_1 = (Either.right (Either.right (Either.right (Either.left Equal.refl))))

In_example_2 (n: Nat) (i: In n [2n, 4n]) : Sigma Nat (m => Equal Nat n (Nat.mul 2n m))
In_example_2 n (Either.left e)                                  = $ 1n e
In_example_2 n (Either.right l (Either rl rr) (Either.left e))  = $ 2n e
In_example_2 n (Either.right l (Either rl rr) (Either.right e)) = Empty.absurd e

We can also prove more generic and higher-level lemmas about In. Note, in the next example, how In starts being applied to a variable and is only expanded when we do case analysis on that variable:

In_map <a> <b> (f: a -> b) (l: List a) (x: a) (i: In x l) : In (f x) (List.map l f) 
In_map a b f (List.nil) x i = Empty.absurd i
In_map a b f (List.cons head tail) x (Either.right e) = Either.right (In_map f tail x e)
In_map a b f (List.cons head tail) x (Either.left e)  = 
    (Equal.rewrite e 
    (y => (Either (Equal (f x) (f y)) (In (f x) (List.map tail f)))) 
    (Either.left Equal.refl))

This way of defining propositions recursively, while convenient in some cases, also has some disadvantages. In particular, it is subject to the usual Kind restrictions on the definition of recursive functions, for example, the requirement that they be "obviously terminating". In the next chapter, we will see how to define propositions inductively, a different technique with its own set of strengths and limitations.

In_map_equiv

In_map_equiv <a> <b> (f: a -> b) (l: List a) (y: b) :
   Equivalence (In y (List.map l f)) (Sigma a (x => (Pair (Equal (f x) y) (In x l))))
In_map_equiv a b f l y = ?

In_app_equiv

In_app_equiv <a> (x: a) (l1: List a) (l2: List a) :
  (Equivalence (In x (List.concat l1 l2)) (Either (In x l1) (In x l2)))
In_app_equiv a x l1 l2 = ?

All

Remember that functions that return propositions can be seen as properties of their arguments. For example, if p has type Nat -> Type, then p n asserts that the property p is true for n.

Inspired by In, write a recursive function All asserting that some property p is true for all elements of a List l. To ensure that your definition is correct, prove the lemma All_In below. (Of course, your definition should not just repeat the left-hand side of All_In.)

All <t> (p: t -> Type) (l: List t)  : Type
All t p l = ?

All_in <t> (p: t -> Type) (l: List t) : Equivalence ((x: t) -> (i: In x l) -> p x) (All p l)
All_in t p l = ?

Combine_odd_even

Complete the definition of the function combine_odd_even below. It takes as arguments two properties of numbers, podd and peven, and should return a property p such that p n is equivalent to podd n when n is odd and equivalent to peven n otherwise

Combine_odd_even (podd: Nat -> Type) (peven: Nat -> Type) : Nat -> Type
Combine_odd_even podd peven = ?

To test your definition, prove the following theorems:

Combine_odd_even_intro
  (n: Nat)
  (podd:  Nat -> Type)
  (peven: Nat -> Type)
  (p1: (Equal (Nat.is_odd n) Bool.true)  -> podd  n)
  (p2: (Equal (Nat.is_odd n) Bool.false) -> peven n) : (Combine_odd_even (podd) (peven)) n
Combine_odd_even_intro n podd peven p1 p2 = ?

Combine_odd_even_elim_odd
  (n: Nat)
  (podd:  Nat -> Type)
  (peven: Nat -> Type)
  (p: (Combine_odd_even podd peven) n)
  (e: Equal (Nat.is_odd n) Bool.true) : podd n
Combine_odd_even_elim_odd n podd peven p e = ?

Combine_odd_elim_even
  (n: Nat)
  (podd: Nat -> Type)
  (peven: Nat -> Type)
  (p: (Combine_odd_even podd peven) n)
  (e: Equal (Nat.is_odd n) Bool.false) : peven n
Combine_odd_elim_even n podd peven p e = ?