Changeset 3552 for LTS/Permutation.ma


Ignore:
Timestamp:
Apr 9, 2015, 11:04:21 PM (5 years ago)
Author:
piccolo
Message:

closed all daemons

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Permutation.ma

    r3527 r3552  
    1515include "basics/deqsets.ma".
    1616include "arithmetics/nat.ma".
     17include "utils.ma".
    1718
    1819record multiset (A : DeqSet) : Type[0] ≝
     
    4243interpretation "m_union" 'm_un x y = (multiset_union ? x y).
    4344
    44 notation > "hvbox(C break A)" non associative with precedence 45 for @{'m_eq $C $A}.
     45notation > "hvbox(C break A)" non associative with precedence 45 for @{'m_eq $C $A}.
    4546interpretation "m_eq" 'm_eq x y = (m_eq ? x y).
    4647
     
    5152interpretation "singleton_m" 'sing x = (singleton ? x).
    5253
    53 lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union … m1 m2) ≅ (multiset_union … m2 m1).
    54 normalize //
    55 qed.
    56 
    57 lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 m1 ⊔ (m2 ⊔ m3).
    58 normalize //
    59 qed.
    60 
    61 lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m m.
    62 normalize //
    63 qed.
    64 
    65 lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ m.
     54lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union ? m1 m2) ⩬ (multiset_union ? m2 m1).
     55normalize //
     56qed.
     57
     58lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 m1 ⊔ (m2 ⊔ m3).
     59normalize //
     60qed.
     61
     62lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m m.
     63normalize //
     64qed.
     65
     66lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ m.
    6667normalize //
    6768qed.
     
    7677
    7778lemma m_eq_union_left_cancellable : ∀A.∀m,m1,m2 : multiset A.
    78 m1 ≅ m2 → m ⊔ m1 ≅ m ⊔ m2.
     79m1 ⩬ m2 → m ⊔ m1 ⩬ m ⊔ m2.
    7980#A #m #m1 #m2 normalize //
    8081qed.
    8182
    82 lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ≅ m ⊔ m2 → m1 ≅ m2.
     83lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ⩬ m ⊔ m2 → m1 ⩬ m2.
    8384normalize #A #m #m1 #m2 #H #a /2/
    8485qed.
    8586
    8687lemma list_to_multiset_append : ∀A.∀l1,l2.
    87 list_to_multiset A (l1 @ l2) list_to_multiset … l1 ⊔ list_to_multiset … l2.
     88list_to_multiset A (l1 @ l2) list_to_multiset … l1 ⊔ list_to_multiset … l2.
    8889#A #l1 elim l1
    8990[ normalize //]
     
    9596qed.
    9697
     98lemma is_multiset_mem_neq_zero : ∀A : DeqSet.
     99∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O.
     100#A #l elim l [ #x *] #x #xs #IH #y *
     101[ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct
     102| #H normalize cases(?==?) normalize [ % #EQ destruct] @IH //
     103]
     104qed.
     105
     106lemma mem_neq_zero_is_multiset : ∀A : DeqSet.
     107∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l.
     108#A #l elim l [ #x * #H cases H % ]
     109#x #xs #IH #y normalize inversion(y==x) normalize nodelta
     110#H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption
     111qed.
    97112
    98113definition is_permutation : ∀A : DeqSet.list A → list A → Prop ≝
    99 λA,l1,l2.list_to_multiset … l1 ≅ list_to_multiset … l2.
     114λA,l1,l2.list_to_multiset … l1 ⩬ list_to_multiset … l2.
     115
     116lemma is_permutation_mem : ∀A :DeqSet.
     117∀l1,l2 : list A.∀x : A.mem … x l1 →
     118is_permutation A l1 l2 → mem … x l2.
     119#A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption
     120qed.
    100121
    101122lemma is_permutation_eq : ∀A : DeqSet.∀l : list A.is_permutation … l l.
     
    193214]
    194215qed.
     216
     217lemma is_permutation_case : ∀A : DeqSet.
     218∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l →
     219∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2.
     220#A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%]
     221#l1 * #l2 #EQ destruct %{l1} %{l2} % //
     222@(permute_equal_right … [x]) @permute_append_all
     223@(is_permutation_transitive … H)
     224/4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/
     225qed.
     226
     227lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
     228∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
     229∀perm : is_permutation A l1 l2.
     230(∀a : A.
     231 ∀prf : mem … a l1.f a prf = g a ?) →
     232is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)).
     233[2: @(is_permutation_mem … perm) //]
     234#A #B #l1 elim l1 -l1
     235[ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ]
     236#x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct
     237>dependent_map_append >dependent_map_append @permute_append_l1 >associative_append
     238whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%);
     239whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?);
     240generalize in ⊢ (? → ???(??(??%)?));
     241#prf1 #prf2
     242>(proof_irrelevance_all … g x prf1 prf2)
     243@is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%);
     244whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1
     245@(is_permutation_transitive …(IH … (l3@l4) …) )
     246[2: assumption
     247|3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //]
     248| @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 //
     249]
     250>dependent_map_append @is_permutation_append
     251[ >dependent_map_extensional [ @is_permutation_eq | // |]
     252| >dependent_map_extensional [ @is_permutation_eq | // |]
     253]
     254qed.
Note: See TracChangeset for help on using the changeset viewer.