Distinctness

We defines the property Distin, that all the elements of a list are distinct. Like that of Adjoin, we use the impredicative definition and prove a an elimination rule.

 ** Module lib_list_Distin Imports lib_list_Member lib_nat_Le
  Distin = ... : {s|Type}(list s)->Prop
  Dis1 = ... : {s|Type}Distin (nil s)
  Dis2 = ... :
    {s|Type}{a:s}{xs:list s}(not (Member a xs))->(Distin xs)->
    Distin (cons a xs)
  Dis_elim = ... :
    {s|Type}{T:(list s)->Prop}(T (nil s))->
    ({a:s}{xs:list s}(not (Member a xs))->(T xs)->T (cons a xs))->
    {xs:list s}(Distin xs)->T xs
  Distin_inv = ... :
    {s|Type}{a|s}{l|list s}(Distin (cons a l))->
    and (not (Member a l)) (Distin l)
  Distin_append = ... :
    {s|Type}{l1,l2:list s}(Distin l1)->(Distin l2)->
    ({a:s}(Member a l1)->not (Member a l2))->Distin (append l1 l2)
  Distin_inj_map = ... :
    {s|Type}{u|Type}{l:list s}{f:s->u}
    ({a1,a2:s}(Member a1 l)->(Member a2 l)->(Eq (f a1) (f a2))->
     Eq a1 a2)->(Distin l)->Distin (map f l)
  Distin_prod = ... :
    {s|Type}{u|Type}{l1:list s}{l2:list u}(Distin l1)->(Distin l2)->
    Distin (prod_list l1 l2)
  Distin_inj_build = ... :
    {s|Type}{f:nat->s}{n:nat}
    ({k1,k2:nat}(Lt k1 n)->(Lt k2 n)->(Eq (f k1) (f k2))->Eq k1 k2)->
    Distin (build_list f n)
  Distin_sublist_Le_length = ... :
    {s|Type}{xs,ys:list s}(Distin xs)->
    ({a:s}(Member a xs)->Member a ys)->Le (length xs) (length ys)