tp : type.
bool : tp.
nat : tp.

value : tp → type.
v_zero : value nat.
v_succ : value nat → value nat.
v_true : value bool.
v_false : value bool.

term : tp → type.
true : term bool.
false : term bool.
switch : term bool → term T → term T → term T.
z : term nat.
succ : term nat → term nat.
pred : term nat → term nat.
iszero : term nat → term bool.

rec eval : ( ⊢ term T) → ( ⊢ value T) =
fn m ⇒
  case m of
  | [ ⊢ true] ⇒ [ ⊢ v_true]
  | [ ⊢ false] ⇒ [ ⊢ v_false]
  | [ ⊢ switch T1 T2 T3] ⇒
    (case eval [ ⊢ T1] of
     | [ ⊢ v_true] ⇒ eval [ ⊢ T2]
     | [ ⊢ v_false] ⇒ eval [ ⊢ T3])
  | [ ⊢ z] ⇒ [ ⊢ v_zero]
  | [ ⊢ succ N] ⇒ let [ ⊢ V] = eval [ ⊢ N] in [ ⊢ v_succ V]
  | [ ⊢ pred N] ⇒
    (case eval [ ⊢ N] of
     | [ ⊢ v_zero] ⇒ [ ⊢ v_zero]
     | [ ⊢ v_succ V] ⇒ [ ⊢ V]);

list : term nat → type.
nil : list z.
cons : tp → list N → list (succ N).

yes_or_no : type.
yes : yes_or_no.
no : yes_or_no.

leq : term nat → term nat → type.
le_z : leq z N.
le_s : leq N M → leq (succ N) (succ M).

rec lemma_leq : ( ⊢ leq M N) → ( ⊢ leq M (succ N)) =
fn d ⇒
  case d of
  | [ ⊢ le_z] ⇒ [ ⊢ le_z]
  | [ ⊢ le_s D] ⇒ let [ ⊢ E] = lemma_leq [ ⊢ D] in [ ⊢ le_s E];

exists_smaller_or_equal_list : term nat → type.
smaller_or_equal_list : list M → leq M N → exists_smaller_or_equal_list N.

rec filter :
  ( ⊢ list N) →
    (( ⊢ tp) → ( ⊢ yes_or_no)) → ( ⊢ exists_smaller_or_equal_list N) =
fn l ⇒ fn f ⇒
  case l of
  | [ ⊢ nil] ⇒ [ ⊢ smaller_or_equal_list nil le_z]
  | [ ⊢ cons H T] ⇒ (let [ ⊢ smaller_or_equal_list T' Prf] = filter [ ⊢ T] f
    in
    case f [ ⊢ H] of
    | [ ⊢ yes] ⇒ [ ⊢ smaller_or_equal_list (cons H T') (le_s Prf)]
    | [ ⊢ no] ⇒ let [ ⊢ Prf'] = lemma_leq [ ⊢ Prf] in
      [ ⊢ smaller_or_equal_list T' Prf']);

© Computation and Logic Group
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9