% Types tp: type. bool: tp. nat : tp. % Values value: tp -> type. v_zero: value nat. v_succ: value nat -> value nat. v_true: value bool. v_false: value bool. % Typed expressions 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 ] => % Prf : leq M N from which we want to conclude that leq M (succ N) let [ |- Prf' ] = lemma_leq [ |- Prf ] in [ |- smaller_or_equal_list T' Prf' ] ) ;