Jason (jcreed) wrote,


More outline progress. Avi Silterra gave me a good example to work with - the subset type of composite naturals. A very natural instance of there being more than one proof of the relevant property. Every factorization is a different proof. Moreover, the naive way of coding it up fails the valid-type-in-unpromoted-gamma check! Namely:
nat : type. z : nat. s : nat -> nat.
sum : nat -> nat -> nat -> type.
prod : nat -> nat -> nat -> type.
comp : type.
comp_rule : {x : nat} {a / nat} {b / nat}
            {p / prod (s(s a)) (s(s b)) x} comp.

is no good because in the context where a and b are -irrelevant- nats, prod (s(s a)) (s(s b)) x isn't really a type! This manifests itself as the fact that although we would want
comp_rule 12 3 4 (proof that 3 x 4 = 12)
comp_rule 12 2 6 (proof that 2 x 6 = 12)

to be equal, the respective third arguments cannot even be equal in the irrelevant equality judgment because they don't have the same type. But there is a fix, thankfully. I just need to encapsulate "x is composite" as a predicate:
is_comp : nat -> type.
is_comp_rule : {x : nat} {a : nat} {b : nat}
               {p : prod (s(s a)) (s(s b))}
               is_comp x.

and say
comp_rule : {x : nat} {p / is_comp x} comp.
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment