Permutation

We define the relation Perm that one list is a permutation of another.

 ** Module lib_list_Perm Imports lib_list_Distin
 $Perm : {s|Type}(list s)->(list s)->Prop
 $perm1 : {s|Type}Perm (nil s) (nil s)
 $perm2 :
    {s|Type}{xs,ys:list s}(Perm xs ys)->{a:s}{axs:list s}
    (Adjoin a xs axs)->{ays:list s}(Adjoin a ys ays)->Perm axs ays
 $Perm_elim :
    {s|Type}{C_Perm:(list s)->(list s)->Prop}(C_Perm (nil s) (nil s))->
    ({xs,ys:list s}(Perm xs ys)->{a:s}{axs:list s}(Adjoin a xs axs)->
     {ays:list s}(Adjoin a ys ays)->(C_Perm xs ys)->C_Perm axs ays)->
    {x1,x2|list s}(Perm x1 x2)->C_Perm x1 x2
 ** Label (!Perm!) Perm
 ** Label (!Perm elim!) Perm_elim
 ** Label (!Perm perm1!) perm1
 ** Label (!Perm perm2!) perm2
[[s|Type][C_Perm:(list s)->(list s)->Prop]
 [f_perm1:C_Perm (nil s) (nil s)]
 [f_perm2:{xs,ys:list s}(Perm xs ys)->{a:s}{axs:list s}
  (Adjoin a xs axs)->{ays:list s}(Adjoin a ys ays)->(C_Perm xs ys)->
  C_Perm axs ays][xs,ys:list s][x1:Perm xs ys][a:s][axs:list s]
 [x2:Adjoin a xs axs][ays:list s][x3:Adjoin a ys ays]
    Perm_elim C_Perm f_perm1 f_perm2 (perm1|s)  ==>  f_perm1
 || Perm_elim C_Perm f_perm1 f_perm2 (perm2 xs ys x1 a axs x2 ays x3)
    ==>
    f_perm2 xs ys x1 a axs x2 ays x3
     (Perm_elim C_Perm f_perm1 f_perm2 x1)]

  Perm_fact = ... :
    {s|Type}{xs,ys|list s}{a|s}(Perm xs ys)->
    Perm (cons a xs) (cons a ys)
  Perm_refl = ... : {s|Type}{xs:list s}Perm xs xs
  Perm_sym = ... : {s|Type}{xs,ys|list s}(Perm xs ys)->Perm ys xs
  Perm_Adjoin_com1 = ... :
    {s|Type}{a|s}{vs,xs,ys,zs|list s}(Perm vs xs)->(Adjoin a xs ys)->
    (Adjoin a zs ys)->Perm vs zs
  Perm_Adjoin_com2 = ... :
    {s|Type}{a|s}{xs,ys,zs,us|list s}(Adjoin a xs ys)->(Perm ys zs)->
    (Adjoin a us zs)->Perm xs us
  Perm_Adjoin_com2_corr = ... :
    {s|Type}{a|s}{xs,ys|list s}(Perm (cons a xs) (cons a ys))->
    Perm xs ys
  Perm_Adjoin_com3 = ... :
    {s|Type}{a|s}{xs,zs,ys|list s}(Adjoin a xs ys)->(Perm ys zs)->
    Ex ([us:list s](Perm xs us /\ Adjoin a us zs))
  Perm_trans = ... :
    {s|Type}{xs,ys,zs|list s}(Perm xs ys)->(Perm ys zs)->Perm xs zs
  Perm_of_Distin = ... :
    {s|Type}{xs,ys:list s}(Distin xs)->
    ({a:s}(Member a xs)->Member a ys)->(Eq (length xs) (length ys))->
    Perm xs ys
  surjective_imp_Perm = ... :
    {s|Type}{l:list s}{f,g:s->s}(Distin l)->
    ({x:s}(Member x l)->Member (g x) l)->({x:s}Eq (f (g x)) x)->
    Perm l (map f l)

There is also an alternative, much more extensive but incompatible implementation of permutations.

 ** Module lib_list_PermII Imports lib_list_length lib_rel_closure
  insert = ... : {A|Type(0)}A->(list A)->(list A)->list A
  insertnil = ... :
    {A|Type(0)}{a|A}{h,k|list A}(Eq (insert a h k) (nil A))->absurd
  insertsingleton = ... :
    {A|Type(0)}{a,b|A}{h,k|list A}(Eq (insert a h k) (cons b (nil A)))->
    and3 (Eq (nil A) h) (Eq a b) (Eq (nil A) k)
  insertapp = ... :
    {A|Type(0)}{a|A}{h,k|list A}{l,m:list A}
    (Eq (insert a h k) (append l m))->
    (({phi:Prop}
     ({n:list A}(Eq (insert a h n) l)->(Eq (append n m) k)->phi)->phi)
     \/ {phi:Prop}
     ({n:list A}(Eq (append l n) h)->(Eq (insert a n k) m)->phi)->phi)
  inseqins = ... :
    {A|Type(0)}{a|A}{h,k,l,m|list A}(Eq (insert a h k) (insert a l m))->
    (({phi:Prop}
     ({n:list A}(Eq (insert a h n) l)->(Eq (insert a n m) k)->phi)->phi)
     \/
     ((Eq l h /\ Eq k m) \/ {phi:Prop}
      ({n:list A}(Eq (insert a l n) h)->(Eq (insert a n k) m)->phi)->
      phi))
  swap = ... : {A|Type(0)}(Rel (list A) (list A))->Prop
  conscl = ... :
    {A|Type(0)}A->(Rel (list A) (list A))->(list A)->(list A)->Prop
  consClosed = ... : {A|Type(0)}(Rel (list A) (list A))->Prop
  iclSwap = ... : {A|Type(0)}IntersectionClosed (swap|A)
  iclConscl = ... : {A|Type(0)}IntersectionClosed (consClosed|A)
  Fbase = ... : {A|Type(0)}Pred (Rel (list A) (list A))
  iclBase = ... : {A|Type(0)}IntersectionClosed (Fbase|A)
  PermBase = ... : {A|Type(0)}Rel (list A) (list A)
  swapBase = ... : {A|Type(0)}swap (PermBase|A)
  consclBase = ... : {A|Type(0)}consClosed (PermBase|A)
  Perm = ... : {A|Type(0)}Rel (list A) (list A)
  equivPerm = ... : {A|Type(0)}equiv (Perm|A)
  reflPerm = ... : {A|Type(0)}refl (Perm|A)
  symPerm = ... : {A|Type(0)}sym (Perm|A)
  transPerm = ... : {A|Type(0)}trans (Perm|A)
  reflPerm' = ... : {A|Type(0)}SubRel (Eq|(list A)) (Perm|A)
  swapPerm = ... : {A|Type(0)}swap (Perm|A)
  consclPerm = ... : {A|Type(0)}consClosed (Perm|A)
  appcl = ... :
    {A|Type(0)}(list A)->(Rel (list A) (list A))->(list A)->(list A)->
    Prop
  appClosed = ... : {A|Type(0)}(Rel (list A) (list A))->Prop
  iclAppcl = ... : {A|Type(0)}IntersectionClosed (appClosed|A)
  appclPerm = ... : {A|Type(0)}appClosed (Perm|A)
  recPerm = ... :
    {A|Type(0)}{l,m:list A}(Perm l m)->{R:Rel (list A) (list A)}
    ({l'6:list A}R l'6 l'6)->
    ({l'7,m'8:list A}(Perm l'7 m'8)->(R l'7 m'8)->R m'8 l'7)->
    ({l'8,m'9,n:list A}(Perm l'8 m'9)->(R l'8 m'9)->(Perm m'9 n)->
     (R m'9 n)->R l'8 n)->
    ({l'9,m'10:list A}R (append l'9 m'10) (append m'10 l'9))->
    ({a:A}{m'11,n:list A}(Perm m'11 n)->(R m'11 n)->
     R (cons a m'11) (cons a n))->R l m
  PermE = ... :
    {A|Type(0)}{R:Rel (list A) (list A)}({l,m|list A}(Eq l m)->R l m)->
    ({l,m|list A}(Perm l m)->(R l m)->R m l)->
    ({l,m,n|list A}(Perm l m)->(R l m)->(Perm m n)->(R m n)->R l n)->
    ({l,m|list A}R (append l m) (append m l))->
    ({a|A}{m,n|list A}(Perm m n)->(R m n)->R (cons a m) (cons a n))->
    SubRel (Perm|A) R
  indPerm = ... : {A|Type(0)}Rel (list A) (list A)
  PermIsInductive = ... : {A|Type(0)}SubRel (Perm|A) (indPerm|A)
  PermRrespR = ... :
    {A|Type(0)}{B|Type}{R:Rel B (list A)}
    ({l,m:list A}{h:B}(R h (append l m))->R h (append m l))->
    ({b:A}{l,m:list A}(Perm l m)->({h:B}(R h l)->R h m)->{k:B}
     (R k (cons b l))->R k (cons b m))->SubRel (Perm|A) (impliesRel R R)
  PermLrespR = ... :
    {A|Type(0)}{B|Type}{R:Rel (list A) B}
    ({l,m:list A}{h:B}(R (append l m) h)->R (append m l) h)->
    ({b:A}{l,m:list A}(Perm l m)->({h:B}(R l h)->R m h)->{k:B}
     (R (cons b l) k)->R (cons b m) k)->
    SubRel (Perm|A) (coimpliesRel R R)
  PermPredE = ... :
    {A|Type(0)}{P:Pred (list A)}
    ({l,m:list A}(P (append l m))->P (append m l))->
    ({b:A}{l,m:list A}(Perm l m)->(iff (P l) (P m))->(P (cons b l))->
     P (cons b m))->{l,m:list A}(Perm l m)->(P l)->P m
  nilPermlemma = ... :
    {A|Type(0)}{l,m|list A}(Perm l m)->(Eq (nil A) l)->Eq (nil A) m
  nilPerm = ... : {A|Type(0)}{l:list A}(Perm (nil A) l)->Eq (nil A) l
  singletonPermlemma = ... :
    {A|Type(0)}{l,m:list A}(Perm l m)->{a:A}(Eq (singleton a) l)->
    Ex ([b:A](Eq a b /\ Eq (singleton b) m))
  singletonPerm = ... :
    {A|Type(0)}{a,b:A}(Perm (singleton a) (singleton b))->Eq a b
  PermRespLength = ... :
    {A|Type(0)}{l,m|list A}(Perm l m)->Eq (length l) (length m)
  PermResidue = ... : {A|Type(0)}A->Rel (list A) (list A)
  insResidue = ... :
    {A|Type(0)}{a:A}{h,k,l:list A}(Eq (insert a h k) l)->
    PermResidue a (append h k) l
  swapResidue = ... :
    {A|Type(0)}{a:A}{l,m,n:list A}(PermResidue a n (append l m))->
    PermResidue a n (append m l)
  consclResidue = ... :
    {A|Type(0)}{a,b:A}{l,m:list A}(Perm l m)->
    ({h:list A}(PermResidue a h l)->PermResidue a h m)->{k:list A}
    (PermResidue a k (cons b l))->PermResidue a k (cons b m)
  funopResidue = ... :
    {A|Type(0)}{a:A}{h,k,l:list A}(PermResidue a h l)->
    (PermResidue a k l)->Perm h k
  transResiduelemma = ... :
    {A|Type(0)}{a:A}{l,m,h|list A}(Perm l m)->(Eq (cons a h) l)->
    PermResidue a h m
  heredPermlemma = ... :
    {A|Type(0)}{a:A}{l,m|list A}(Perm (cons a l) (cons a m))->Perm l m
  hereditary = ... : {A|Type(0)}(Rel (list A) (list A))->Prop
  heredPerm = ... : {A|Type(0)}hereditary (Perm|A)
  transposePerm = ... :
    {A|Type(0)}{a,b|A}{l,m,n|list A}
    Perm (insert a l (insert b m n)) (insert b l (insert a m n))