source: LTS/Permutation.ma @ 3534

Last change on this file since 3534 was 3527, checked in by piccolo, 5 years ago

fixed permutation axioms

File size: 7.7 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "basics/deqsets.ma".
16include "arithmetics/nat.ma".
17
18record multiset (A : DeqSet) : Type[0] ≝
19{ mult : (A → ℕ) }.
20 
21definition m_eq : ∀A.multiset A → multiset A → Prop ≝
22λA,m1,m2.∀a.mult … m1 a = mult … m2 a.
23
24lemma m_eq_reflexive : ∀A.reflexive … (m_eq A).
25//
26qed.
27
28lemma m_eq_symmetric : ∀A.symmetric … (m_eq A).
29//
30qed.
31
32lemma m_eq_transitive : ∀A.transitive … (m_eq A).
33//
34qed.
35
36definition empty_multiset : ∀A.multiset A ≝ λA.mk_multiset … (λ_.O).
37definition singleton : ∀A : DeqSet.A → multiset A ≝ λA,a.mk_multiset … (λx.if x == a then 1 else O).
38definition multiset_union : ∀A.multiset A → multiset A → multiset A ≝
39λA,m1,m2.mk_multiset … (λx.mult … m1 x + mult … m2 x).
40
41notation "hvbox(C break  ⊔ A)" left associative with precedence 55 for @{ 'm_un $C $A }.
42interpretation "m_union" 'm_un x y = (multiset_union ? x y).
43
44notation > "hvbox(C break ≅ A)" non associative with precedence 45 for @{'m_eq $C $A}.
45interpretation "m_eq" 'm_eq x y = (m_eq ? x y).
46
47notation "ⓧ" with precedence 90 for @{'empty_m}.
48interpretation "empty_mult" 'empty_m = (empty_multiset ?).
49
50notation "❨ term 19 C ❩ " with precedence 10 for @{ 'sing $C}.
51interpretation "singleton_m" 'sing x = (singleton ? x).
52
53lemma m_union_commutative : ∀A.∀m1,m2 : multiset A.(multiset_union … m1 m2) ≅ (multiset_union … m2 m1).
54normalize //
55qed.
56
57lemma m_union_associative : ∀A.∀m1,m2,m3 : multiset A.(m1 ⊔ m2) ⊔ m3 ≅ m1 ⊔ (m2 ⊔ m3).
58normalize //
59qed.
60
61lemma m_union_neutral_l : ∀A.∀m : multiset A.ⓧ ⊔ m ≅ m.
62normalize //
63qed.
64
65lemma m_union_neutral_r : ∀A.∀m : multiset A.m ⊔ ⓧ ≅ m.
66normalize //
67qed.
68
69include "basics/lists/list.ma".
70
71let rec list_to_multiset (A : DeqSet) (l : list A) on l : multiset A ≝
72match l with
73[ nil ⇒ ⓧ
74| cons x xs ⇒ ❨ x ❩ ⊔ list_to_multiset … xs
75].
76
77lemma m_eq_union_left_cancellable : ∀A.∀m,m1,m2 : multiset A.
78m1 ≅ m2 → m ⊔ m1 ≅ m ⊔ m2.
79#A #m #m1 #m2 normalize //
80qed.
81
82lemma m_eq_equal_right : ∀A.∀m,m1,m2 : multiset A.m ⊔ m1 ≅ m ⊔ m2 → m1 ≅ m2.
83normalize #A #m #m1 #m2 #H #a /2/
84qed.
85
86lemma list_to_multiset_append : ∀A.∀l1,l2.
87list_to_multiset A (l1 @ l2) ≅ list_to_multiset … l1 ⊔ list_to_multiset … l2.
88#A #l1 elim l1
89[ normalize //]
90#x #xs #IH #l2 change with (❨x❩ ⊔ list_to_multiset ??) in ⊢ (??%?);
91change with (❨x❩ ⊔ list_to_multiset ??) in ⊢ (???(??%?));
92whd in match (list_to_multiset ??); @m_eq_symmetric
93@(m_eq_transitive … (m_union_associative …))
94@m_eq_union_left_cancellable @m_eq_symmetric @IH
95qed.
96
97
98definition is_permutation : ∀A : DeqSet.list A → list A → Prop ≝
99λA,l1,l2.list_to_multiset … l1 ≅ list_to_multiset … l2.
100
101lemma is_permutation_eq : ∀A : DeqSet.∀l : list A.is_permutation … l l.
102//
103qed.
104
105lemma is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 →
106                                       is_permutation A (x :: l1) (x :: l2).
107normalize //
108qed.
109
110lemma permute_append_all : ∀A.∀l1,l2,l3,l4.is_permutation A (l1@l2) (l3@l4) →
111is_permutation A (l2 @l1) (l4@l3).
112#A #l1 #l2 #l3 #l4 normalize #H #a >(list_to_multiset_append … a)
113>(list_to_multiset_append … a) >m_union_commutative
114>m_union_commutative in ⊢ (???%); <list_to_multiset_append <list_to_multiset_append @H
115qed.
116
117lemma permute_append_l1 : ∀A.∀l1,l2,l3.is_permutation A l1 (l2 @ l3) →
118is_permutation A l1 (l3 @ l2).
119#A #l1 #l2 #l3 #H #a >list_to_multiset_append >m_union_commutative <list_to_multiset_append @H
120qed.
121
122lemma is_permutation_commutative : ∀A.symmetric … (is_permutation A).
123//
124qed.
125
126lemma is_permutation_transitive : ∀A.transitive … (is_permutation A).
127//
128qed.
129
130lemma is_permutation_append_left_cancellable : ∀A.∀l,l1,l2.is_permutation A l1 l2 →
131is_permutation A (l @ l1) (l @ l2).
132#A #l #l1 #l2 #H #a >list_to_multiset_append >list_to_multiset_append
133@m_eq_union_left_cancellable @H
134qed.
135
136lemma is_permutation_append : ∀A.∀l1,l2,l3,l4.
137is_permutation A l1 l2 → is_permutation A l3 l4 →
138is_permutation A (l1 @ l3) (l2 @ l4).
139#A  #l1 #l2 #l3 #l4 #H1 #H2 #a >list_to_multiset_append
140>list_to_multiset_append normalize >H1 >H2 %
141qed.
142
143lemma permute_equal_right : ∀A.∀l1,l2,l.
144is_permutation A (l1 @ l) (l2 @ l) → is_permutation A l1 l2.
145#A #l1 #l2 #l normalize #H #a lapply(H a) >list_to_multiset_append >list_to_multiset_append
146>m_union_commutative >m_union_commutative in ⊢ (???% → ?);
147normalize //
148qed.
149
150lemma permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y.
151  (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7)
152 →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9)
153 →is_permutation A
154   (y ::((l6 @((x ::l5) @(l1 @l2))) @l7))
155   (((x ::l4 @y ::l3) @l8) @l9)).
156#A #l1 #l2 #l3 #l4 #l5 #l6 #l7 #l8 #l9 #x #y
157change with ([x] @ ?) in match ([x] @ ?);
158change with ([y] @ ?) in match ([y] @ ?);
159>append_nil #H1 #H2 whd in match (append ???) in ⊢ (???%);
160change with ([x] @ ?) in match ([x] @ ?) in ⊢ (???%);
161change with ([y] @ ?) in match ([y] @ ?) in ⊢ (???%);
162@permute_append_l1 >associative_append in ⊢ (???%);
163<associative_append in ⊢ (???%); <associative_append in ⊢ (???%);
164<associative_append <associative_append <associative_append
165@(is_permutation_transitive … ((((([y]@l4)@l3)@l8)@l9)@[x]))
166[ >associative_append >associative_append >associative_append
167  >associative_append >associative_append >associative_append
168  >associative_append >associative_append >associative_append
169  @is_permutation_append_left_cancellable
170  <associative_append in ⊢ (???%); <associative_append in ⊢ (???%); <associative_append in ⊢ (???%);
171  @permute_append_l1
172  @(is_permutation_transitive … ([x]@l6@l5@l1@l2@l7))
173  [2: @is_permutation_append_left_cancellable
174      @(is_permutation_transitive … ((l5 @ l1) @ ((l6@l2)@l7)))
175      [2: >associative_append in ⊢ (???%); >associative_append in ⊢ (???%);
176         @is_permutation_append
177         [2: <associative_append in ⊢ (???%); assumption
178         | >associative_append in H1 : (??%?); #H1 @permute_equal_right
179           [ @(l6@l7) | >associative_append assumption ]
180         ]
181      | <associative_append in ⊢ (??(???%)?); @is_permutation_commutative
182        @permute_append_l1 >associative_append in ⊢ (???%); @is_permutation_append_left_cancellable
183        >associative_append @permute_append_l1 //
184      ]
185  | <associative_append <associative_append <associative_append in ⊢ (???%);
186    <associative_append in ⊢ (???%); @permute_append_all @is_permutation_append_left_cancellable
187    @permute_append_all @is_permutation_append_left_cancellable @permute_append_l1 //
188  ]
189| @permute_append_all @is_permutation_append_left_cancellable @permute_append_all
190  @is_permutation_append_left_cancellable @permute_append_all
191  @is_permutation_append_left_cancellable @permute_append_all
192  @is_permutation_append_left_cancellable @permute_append_l1 //
193]
194qed.
Note: See TracBrowser for help on using the repository browser.