We define the relation Perm that one list is a permutation of another. This definition also uses a ``non-dependent'' elimination rule.
** 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}{P:(list s)->(list s)->Prop}(P (nil s) (nil s))-> ({xs,ys:list s}(Perm xs ys)->(P xs ys)->{a:s}{axs:list s} (Adjoin a xs axs)->{ays:list s}(Adjoin a ys ays)->P axs ays)-> {xs,ys:list s}(Perm xs ys)->P xs ys 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]and (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))-> or ({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))-> or ({phi:Prop} ({n:list A}(Eq (insert a h n) l)->(Eq (insert a n m) k)->phi)-> phi) (or (and (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]and (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))