[3554] | 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 | |
---|
| 15 | include "basics/lists/listb.ma". |
---|
| 16 | include "../src/utilities/hide.ma". |
---|
| 17 | include "../src/ASM/Util.ma". |
---|
| 18 | include "../src/utilities/option.ma". |
---|
| 19 | |
---|
[3574] | 20 | definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ |
---|
| 21 | λA,B,f,a,b,x.if x == a then b else f x. |
---|
| 22 | |
---|
[3563] | 23 | lemma bind_inversion : ∀A,B : Type[0].∀m : option A. |
---|
| 24 | ∀f : A → option B.∀y : B. |
---|
| 25 | ! x ← m; f x = return y → |
---|
| 26 | ∃ x.(m = return x) ∧ (f x = return y). |
---|
| 27 | #A #B * [| #a] #f #y normalize #EQ [destruct] |
---|
| 28 | %{a} %{(refl …)} // |
---|
| 29 | qed. |
---|
| 30 | |
---|
[3554] | 31 | (*NO DUPLICATES in lists*) |
---|
| 32 | |
---|
| 33 | let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ |
---|
| 34 | match l with |
---|
| 35 | [ nil ⇒ True |
---|
| 36 | | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs |
---|
| 37 | ]. |
---|
| 38 | |
---|
| 39 | lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → |
---|
| 40 | no_duplicates … l2. |
---|
| 41 | #A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/ |
---|
| 42 | qed. |
---|
| 43 | |
---|
| 44 | lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → |
---|
| 45 | no_duplicates … l1. |
---|
| 46 | #A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ] |
---|
| 47 | inversion(x ∈ xs @l2) in H1; normalize [ #_ * #H @⊥ @H %] #H1 #_ |
---|
| 48 | % inversion(x ∈ xs) normalize [2: //] #H3 #_ >(memb_append_l1 … H3) in H1; |
---|
| 49 | #EQ destruct(EQ) |
---|
| 50 | qed. |
---|
| 51 | |
---|
| 52 | lemma no_duplicates_append_commute : ∀ A : DeqSet.∀l1,l2 : list A. |
---|
| 53 | no_duplicates … (l1 @ l2) → |
---|
| 54 | no_duplicates … (l2 @ l1). |
---|
| 55 | #A #l1 elim l1 |
---|
| 56 | [ #l2 >append_nil //] |
---|
| 57 | #x #xs #IH #l2 * #H1 #H2 lapply(IH … H2) lapply H1 -H1 -IH -H2 |
---|
| 58 | elim l2 -l1 |
---|
| 59 | [ >append_nil #H1 #H2 % // ] |
---|
| 60 | #y #ys #IH * #H1 * #H2 #H3 % |
---|
| 61 | [2: @IH |
---|
| 62 | [ % #H4 @H1 cases(memb_append … H4) |
---|
| 63 | [ #H5 >memb_append_l1 // |
---|
| 64 | | #H5 >memb_append_l2 // @orb_Prop_r >H5 // |
---|
| 65 | ] |
---|
| 66 | | // |
---|
| 67 | ] |
---|
| 68 | | % #H4 cases(memb_append … H4) |
---|
| 69 | [ #H5 @(absurd ?? H2) >memb_append_l1 // |
---|
| 70 | | whd in match (memb ???); inversion(y==x) |
---|
| 71 | [ #H5 #_ <(\P H5) in H1; #H1 @H1 >memb_append_l2 // |
---|
| 72 | | #_ normalize nodelta #H5 @(absurd ?? H2) >memb_append_l2 // |
---|
| 73 | ] |
---|
| 74 | ] |
---|
| 75 | ] |
---|
| 76 | qed. |
---|
| 77 | |
---|
| 78 | lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D. |
---|
| 79 | x ∈ l1 = false → x ∈ l2 = false → x ∈ (l1 @ l2) = false. |
---|
| 80 | #D #l1 elim l1 |
---|
| 81 | [ #l2 #x #_ #H @H ] |
---|
| 82 | #x #xs #IH #l2 #x1 whd in match (memb ???); inversion (x1 == x) normalize nodelta |
---|
| 83 | [ #_ #EQ destruct] #EQx1 #EQxs #EQl2 whd in match (memb ???); >EQx1 |
---|
| 84 | normalize nodelta @IH // |
---|
| 85 | qed. |
---|
| 86 | |
---|
| 87 | lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . |
---|
| 88 | no_duplicates … (l1 @ l2) → x ∈ l1 → x ∈ l2 → False. |
---|
| 89 | #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); |
---|
| 90 | inversion (x == x1) normalize nodelta |
---|
| 91 | [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % |
---|
| 92 | | #_ @IH // |
---|
| 93 | ] |
---|
| 94 | qed. |
---|
| 95 | |
---|
| 96 | (* subset *) |
---|
| 97 | |
---|
| 98 | let rec subset (A : Type[0]) (l1,l2 : list A) on l1 : Prop ≝ |
---|
| 99 | match l1 with |
---|
| 100 | [ nil ⇒ True |
---|
| 101 | | cons x xs ⇒ mem … x l2 ∧ subset … xs l2 |
---|
| 102 | ]. |
---|
| 103 | |
---|
| 104 | interpretation "subset" 'subseteq a b = (subset ? a b). |
---|
| 105 | |
---|
| 106 | lemma subset_append_l2 : ∀A,l2,l1.subset A l2 (l1 @ l2). |
---|
| 107 | #A #l2 elim l2 // normalize #x #xs #IH #l1 % // @mem_append_l2 whd /2/ |
---|
| 108 | qed. |
---|
| 109 | |
---|
| 110 | lemma refl_subset : ∀A.reflexive … (subset A). |
---|
| 111 | #A #l1 elim l1 // #x #xs #IH normalize % /2/ change with ([?]@xs) in match (x :: xs); |
---|
| 112 | @subset_append_l2 |
---|
| 113 | qed. |
---|
| 114 | |
---|
| 115 | lemma subset_def : ∀A : DeqSet.∀l1,l2 : list A.(∀x.x ∈l1 → x ∈ l2) → l1 ⊆ l2. |
---|
| 116 | #A #l1 elim l1 // #x #xs #IH #l2 #H % |
---|
| 117 | [ @memb_to_mem >H // >memb_hd // |
---|
| 118 | | @IH #y #H1 @H >memb_cons // >H1 // |
---|
| 119 | ] |
---|
| 120 | qed. |
---|
| 121 | |
---|
| 122 | lemma subset_append : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l2 ⊆ l3 → (l1 @ l2) ⊆ l3. |
---|
| 123 | #A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % /2/ |
---|
| 124 | qed. |
---|
| 125 | |
---|
| 126 | lemma subset_def_inv : ∀A.∀l1,l2 : list A. l1 ⊆ l2 → ∀x.mem … x l1 → mem … x l2. |
---|
| 127 | #A #l1 elim l1 [ #l2 * #x * ] #x #xs #IH #l2 * #H1 #H2 #y * |
---|
| 128 | [ #EQ destruct // | #H3 @IH // ] |
---|
| 129 | qed. |
---|
| 130 | |
---|
| 131 | lemma transitive_subset : ∀A.transitive … (subset A). |
---|
| 132 | #A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % |
---|
| 133 | [ @(subset_def_inv … H3) // | @IH // ] |
---|
| 134 | qed. |
---|
| 135 | |
---|
| 136 | lemma subset_append_h1 : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l1 ⊆ (l3 @ l2). |
---|
| 137 | #A #l1 elim l1 // #x #x2 #IH #l2 #l3 * #H1 #H2 % [ @mem_append_l1 // | @IH // ] |
---|
| 138 | qed. |
---|
| 139 | |
---|
| 140 | lemma subset_append_h2 : ∀A.∀l1,l2,l3 : list A.l2 ⊆ l3 → l2 ⊆ (l1 @ l3). |
---|
| 141 | #A #l1 elim l1 // #x #xs #IH #l2 elim l2 // #y #ys #IH #l3 * #H1 #H2 % |
---|
| 142 | [ @mem_append_l2 // | @IH // ] |
---|
| 143 | qed. |
---|
| 144 | |
---|
[3575] | 145 | (* some useful deqsets *) |
---|
| 146 | |
---|
| 147 | definition DeqUnit ≝ mk_DeqSet unit (λ_.λ_.true) ?. |
---|
| 148 | @hide_prf ** % // qed. |
---|
| 149 | |
---|
| 150 | definition DeqFalse ≝ mk_DeqSet False (λ_.λ_.true) ?. |
---|
| 151 | @hide_prf * qed. |
---|
| 152 | |
---|
[3554] | 153 | (* list of elements with decidable equality *) |
---|
| 154 | |
---|
| 155 | let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝ |
---|
| 156 | match l1 with |
---|
| 157 | [ nil ⇒ λl2.match l2 with [nil ⇒ true | _ ⇒ false ] |
---|
| 158 | | cons x xs ⇒ λl2.match l2 with [ cons y ys ⇒ x == y ∧ eqb_list … xs ys | _ ⇒ false ] |
---|
| 159 | ]. |
---|
| 160 | |
---|
[3579] | 161 | lemma eqb_list_elim : ∀P : bool → Prop. |
---|
| 162 | ∀D,l1,l2.(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eqb_list D l1 l2). |
---|
| 163 | #P #D #l1 lapply P -P elim l1 |
---|
| 164 | [ #P * /2/ #x #xs #H1 #H2 @H2 % #EQ destruct] |
---|
| 165 | #x #xs #IH #P * /2/ #y #ys #H1 #H2 normalize |
---|
| 166 | inversion(?==?) #EQ normalize [2: @H2 % #EQ1 destruct >(\b (refl …)) in EQ; #EQ destruct] |
---|
| 167 | @IH [ #EQ1 destruct @H1 >(\P EQ) % | * #H @H2 % #EQ1 destruct @H %] |
---|
| 168 | qed. |
---|
| 169 | |
---|
[3554] | 170 | definition DeqSet_List : DeqSet → DeqSet ≝ |
---|
| 171 | λX.mk_DeqSet (list X) (eqb_list …) ?. |
---|
| 172 | #x elim x [ * /2 by refl, conj/ #y #ys normalize % #EQ destruct] -x |
---|
| 173 | #x #xs #IH * [ normalize % #EQ destruct] #y #ys normalize % inversion(x == y) |
---|
| 174 | #EQ normalize nodelta |
---|
| 175 | [ #H >(proj1 … (IH ys) H) @eq_f2 [2: %] @(proj1 … (eqb_true …)) assumption |
---|
| 176 | | #EQ destruct |
---|
| 177 | | #EQ1 destruct @(proj2 … (IH …)) % |
---|
| 178 | | #EQ1 destruct <EQ @(proj2 … (eqb_true …)) % |
---|
| 179 | ] |
---|
| 180 | qed. |
---|
| 181 | |
---|
| 182 | unification hint 0 ≔ C; |
---|
| 183 | X ≟ DeqSet_List C |
---|
| 184 | (* ---------------------------------------- *) ⊢ |
---|
| 185 | list C ≡ carr X. |
---|
| 186 | |
---|
| 187 | |
---|
| 188 | unification hint 0 ≔ D,p1,p2; |
---|
| 189 | X ≟ DeqSet_List D |
---|
| 190 | (* ---------------------------------------- *) ⊢ |
---|
| 191 | eqb_list D p1 p2 ≡ eqb X p1 p2. |
---|
| 192 | |
---|
| 193 | lemma mem_list : ∀A : Type[0]. |
---|
| 194 | ∀l : list A.∀x : A.mem … x l → |
---|
| 195 | ∃l1,l2.l=l1 @ [x] @ l2. |
---|
| 196 | #A #l elim l |
---|
| 197 | [ #x *] |
---|
| 198 | #x #xs #IH #y * |
---|
| 199 | [ #EQ destruct %{[]} %{xs} % |
---|
| 200 | | #H cases(IH … H) #l1 * #l2 #EQ destruct |
---|
| 201 | %{(x :: l1)} %{l2} % |
---|
| 202 | ] |
---|
| 203 | qed. |
---|
| 204 | |
---|
| 205 | (* associative list *) |
---|
| 206 | |
---|
| 207 | definition associative_list : DeqSet → Type[0] → Type[0] ≝ |
---|
| 208 | λA,B.list (A × (list B)). |
---|
| 209 | |
---|
| 210 | let rec update_list (A : DeqSet) (B : Type[0]) (l : associative_list A B) |
---|
| 211 | on l : A → list B → associative_list A B ≝ |
---|
| 212 | λa,b.match l with |
---|
| 213 | [ nil ⇒ [〈a,b〉] |
---|
| 214 | | cons x xs ⇒ if (a == (\fst x)) then 〈a,b〉 :: xs |
---|
| 215 | else x :: (update_list … xs a b) |
---|
| 216 | ]. |
---|
| 217 | |
---|
| 218 | let rec get_element (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : A → list B ≝ |
---|
| 219 | λa.match l with [ nil ⇒ nil ? |
---|
| 220 | | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a |
---|
| 221 | ]. |
---|
| 222 | |
---|
| 223 | let rec domain_of_associative_list (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : list A ≝ |
---|
| 224 | match l with |
---|
| 225 | [ nil ⇒ [] |
---|
| 226 | | cons x xs ⇒ \fst x :: domain_of_associative_list … xs |
---|
| 227 | ]. |
---|
| 228 | |
---|
| 229 | lemma get_element_append_l: |
---|
| 230 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
| 231 | x ∈ domain_of_associative_list … l1 → |
---|
| 232 | get_element … (l1@l2) x = get_element … l1 x. |
---|
| 233 | #A #B #l1 elim l1 normalize [ #l2 #x * ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) |
---|
| 234 | #H [ >(\b H) | >(\bf H) ] normalize /2/ |
---|
| 235 | qed. |
---|
| 236 | |
---|
| 237 | lemma get_element_append_r: |
---|
| 238 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
| 239 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → |
---|
| 240 | get_element ?? (l1@l2) x = get_element … l2 x. |
---|
| 241 | #A #B #l1 elim l1 normalize [ #l2 #x // ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) |
---|
| 242 | #H [ >(\b H) | >(\bf H) ] normalize /2 by/ * #K cases (K I) |
---|
| 243 | qed. |
---|
| 244 | |
---|
| 245 | lemma get_element_append_l1 : |
---|
| 246 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
| 247 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) → |
---|
| 248 | get_element ?? (l1@l2) x = get_element … l1 x. |
---|
| 249 | #A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ] |
---|
| 250 | #l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize |
---|
| 251 | [ * #H @⊥ @H % ] #H @IH assumption |
---|
| 252 | qed. |
---|
| 253 | |
---|
| 254 | lemma get_element_append_r1 : |
---|
| 255 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
| 256 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → |
---|
| 257 | get_element ?? (l1@l2) x = get_element … l2 x. |
---|
| 258 | #A #B #l1 elim l1 normalize // #x #xs #IH #l2 #a cases (?==?) |
---|
| 259 | normalize [* #H cases H //] #H >IH normalize // |
---|
| 260 | qed. |
---|
| 261 | |
---|
| 262 | lemma memb_append_l22 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A. |
---|
| 263 | ¬ (x ∈ l1) → x∈ l1 @ l2 = (x ∈ l2). |
---|
| 264 | #A #x #l1 elim l1 normalize // #y #ys #IH #l2 cases(x==y) |
---|
| 265 | normalize [*] @IH |
---|
| 266 | qed. |
---|
| 267 | |
---|
| 268 | lemma memb_append_l12 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A. |
---|
| 269 | ¬ (x ∈ l2) → x∈ l1 @ l2 = (x ∈ l1). |
---|
| 270 | #A #x #l1 elim l1 |
---|
| 271 | [ #l2 #H whd in match (append ???); @not_b_to_eq_false @Prop_notb >H % ] |
---|
| 272 | #y #ys #IH #l2 #H1 whd in match (memb ???); >IH // |
---|
| 273 | qed. |
---|
| 274 | |
---|
| 275 | lemma foldr_map_append : |
---|
| 276 | ∀A,B:Type[0]. ∀l1, l2 : list A. |
---|
| 277 | ∀f:A → list B. ∀seed. |
---|
| 278 | foldr ?? (λx,acc. (f x) @ acc) seed (l1 @ l2) = |
---|
| 279 | append ? (foldr ?? (λx,acc. (f x) @ acc) (nil ?) l1) |
---|
| 280 | (foldr ?? (λx,acc. (f x) @ acc) seed l2). |
---|
| 281 | #A #B #l1 elim l1 normalize // /3 by eq_f, trans_eq/ |
---|
| 282 | qed. |
---|
| 283 | |
---|
| 284 | lemma cons_append : ∀A.∀x : A.∀l.x::l = ([x]@l). |
---|
| 285 | // |
---|
| 286 | qed. |
---|
| 287 | |
---|
| 288 | lemma domain_of_associative_list_append : ∀A,B.∀l1,l2 : associative_list A B. |
---|
| 289 | domain_of_associative_list ?? (l1 @ l2) = |
---|
| 290 | (domain_of_associative_list ?? l1) @ (domain_of_associative_list ?? l2). |
---|
| 291 | #A #B #l1 elim l1 // #x #xs #IH #l2 normalize // |
---|
| 292 | qed. |
---|
| 293 | |
---|
| 294 | (*monoids*) |
---|
| 295 | |
---|
| 296 | record monoid: Type[1] ≝ |
---|
| 297 | { carrier :> DeqSet |
---|
| 298 | ; op: carrier → carrier → carrier |
---|
| 299 | ; e: carrier |
---|
| 300 | ; neutral_r : ∀x. op … x e = x |
---|
| 301 | ; neutral_l : ∀x. op … e x = x |
---|
| 302 | ; is_associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z) |
---|
| 303 | }. |
---|
| 304 | |
---|
| 305 | definition is_abelian ≝ λM : monoid. |
---|
| 306 | ∀x,y : M.op … M x y = op … M y x. |
---|
| 307 | |
---|
| 308 | record monoid_action (I : monoid) (M : Type[0]) : Type[0] ≝ |
---|
| 309 | { act :2> I → M → M |
---|
| 310 | ; act_neutral : ∀x.act (e …) x = x |
---|
| 311 | ; act_op : ∀i,j,x.act (op … i j) x = act j (act i x) |
---|
| 312 | }. |
---|
| 313 | |
---|
| 314 | (* partial order *) |
---|
| 315 | |
---|
| 316 | record partial_order (A : Type[0]) : Type[0] ≝ |
---|
| 317 | { po_rel :2> A → A → Prop |
---|
| 318 | ; refl_po_rel : reflexive … po_rel |
---|
| 319 | ; antisym_po_rel : ∀x,y : A.po_rel … x y → po_rel … y x → x = y |
---|
| 320 | ; trans_po_rel : transitive … po_rel |
---|
| 321 | }. |
---|
| 322 | |
---|
| 323 | (* fold2 *) |
---|
| 324 | |
---|
| 325 | let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B) |
---|
| 326 | (l2 : list C) (f : A → B → C → A) on l1 : option A≝ |
---|
| 327 | match l1 with |
---|
| 328 | [ nil ⇒ match l2 with [ nil ⇒ return a | cons y ys ⇒ None ? ] |
---|
| 329 | | cons x xs ⇒ |
---|
| 330 | match l2 with |
---|
| 331 | [ nil ⇒ None ? |
---|
| 332 | | cons y ys ⇒ ! ih ← (foldr2 … a xs ys f); |
---|
| 333 | return f ih x y |
---|
| 334 | ] |
---|
| 335 | ]. |
---|
| 336 | |
---|
| 337 | (* dependent map*) |
---|
| 338 | |
---|
| 339 | let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝ |
---|
| 340 | (match l return λx.l=x → ? with |
---|
| 341 | [ nil ⇒ λ_.nil ? |
---|
| 342 | | cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?) |
---|
| 343 | ])(refl …). |
---|
| 344 | [ >prf %% | >prf %2 assumption] |
---|
| 345 | qed. |
---|
| 346 | |
---|
| 347 | lemma dependent_map_append : ∀A,B,l1,l2,f. |
---|
| 348 | dependent_map A B (l1 @ l2) (λa,prf.f a prf) = |
---|
| 349 | (dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)). |
---|
| 350 | [2: @hide_prf /2/ | 3: @hide_prf /2/] |
---|
| 351 | #A #B #l1 elim l1 normalize /2/ |
---|
| 352 | qed. |
---|
| 353 | |
---|
| 354 | lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f. |
---|
| 355 | ∀EQ:l1 = l2. |
---|
| 356 | dependent_map A B l1 (λa,prf.f a prf) = |
---|
| 357 | dependent_map A B l2 (λa,prf.f a ?). |
---|
| 358 | [2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ] |
---|
| 359 | qed. |
---|
| 360 | |
---|
| 361 | definition applica : ∀A,B : Type[0].∀ l : list A.(∀a : A.mem … a l → B) → ∀a : A.mem … a l → B ≝ |
---|
| 362 | λA,B,l,f,x,prf.f x prf. |
---|
| 363 | |
---|
| 364 | lemma proof_irrelevance_temp : ∀A,B : Type[0].∀l : list A. |
---|
| 365 | ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2. |
---|
| 366 | applica … f x prf1 = applica … f x prf2. |
---|
| 367 | // |
---|
| 368 | qed. |
---|
| 369 | |
---|
| 370 | lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A. |
---|
| 371 | ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2. |
---|
| 372 | f x prf1 = f x prf2. |
---|
| 373 | #A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp |
---|
| 374 | qed. |
---|
| 375 | |
---|
| 376 | lemma dependent_map_extensional : ∀A,B : Type[0].∀l : list A. |
---|
| 377 | ∀f,g : (∀a.mem … a l → B).(∀a,prf1,prf2.f a prf1 = g a prf2) → |
---|
| 378 | dependent_map … l f = dependent_map … l g. |
---|
| 379 | #A #B #l elim l // #x #xs #IH #f #g #H whd in ⊢ (??%%); |
---|
| 380 | @eq_f2 // @IH // |
---|
[3563] | 381 | qed. |
---|
[3574] | 382 | |
---|
| 383 | (* nth_opt*) |
---|
| 384 | |
---|
| 385 | lemma nth_first : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| > n → nth_opt … n (l1 @ l2) = nth_opt … n l1. |
---|
| 386 | #A #l1 elim l1 [ #l2 #n normalize #H @⊥ /2/] #x #xs #IH #l2 * // #n #H @IH normalize in H; /2/ |
---|
| 387 | qed. |
---|
| 388 | |
---|
| 389 | lemma nth_second : ∀A.∀l1,l2 : list A.∀n : ℕ.|l1| ≤ n → nth_opt … n (l1 @ l2) = nth_opt … (n - |l1|) l2. |
---|
| 390 | #A #l1 elim l1 [normalize //] #x #xs #IH #l2 * [ normalize #H @⊥ /2/] #n #H normalize @IH /2/ |
---|
| 391 | qed. |
---|
[3579] | 392 | |
---|
| 393 | (* All2 *) |
---|
| 394 | |
---|
| 395 | let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝ |
---|
| 396 | match l1 with |
---|
| 397 | [ nil ⇒ match l2 with [nil ⇒ True | cons _ _ ⇒ False] |
---|
| 398 | | cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys] |
---|
| 399 | ]. |
---|