Changeset 2386 for src/Clight
 Timestamp:
 Oct 3, 2012, 1:26:48 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2332 r2386 1 (* Various small results used in at least two files in the frontend. *)1 (* Various small homeless results. *) 2 2 3 3 include "Clight/TypeComparison.ma". 4 4 include "common/Pointers.ma". 5 include "basics/jmeq.ma". 6 include "basics/star.ma". (* wellfounded relations *) 7 include "basics/lists/listb.ma". 8 include "basics/lists/list.ma". 9 10 11 (*  *) 12 (* Misc. *) 13 (*  *) 5 14 6 15 lemma eq_intsize_identity : ∀id. eq_intsize id id = true. … … 22 31  2: #Hneq' normalize // ] qed. 23 32 24 (* useful facts on various boolean operations *) 33 lemma le_S_O_absurd : ∀x:nat. S x ≤ 0 → False. /2 by absurd/ qed. 34 35 (*  *) 36 (* Useful facts on various boolean operations. *) 37 (*  *) 38 25 39 lemma andb_lsimpl_true : ∀x. andb true x = x. // qed. 26 40 lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed. … … 30 44 lemma notb_fold : ∀x. if x then false else true = (¬x). // qed. 31 45 32 (* useful facts on block *) 33 lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false. 34 #b1 #b2 #Hneq 35 @(eq_block_elim … b1 b2) 36 [ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??))) 37  2: #_ @refl ] qed. 38 39 lemma not_eq_block_rev : ∀b1,b2. b2 ≠ b1 → eq_block b1 b2 = false. 40 #b1 #b2 #Hneq 41 @(eq_block_elim … b1 b2) 42 [ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??))) 43  2: #_ @refl ] qed. 44 45 (* useful facts on Z *) 46 (*  *) 47 (* Useful facts on Z. *) 48 (*  *) 49 46 50 lemma Zltb_to_Zleb_true : ∀a,b. Zltb a b = true → Zleb a b = true. 47 51 #a #b #Hltb lapply (Zltb_true_to_Zlt … Hltb) #Hlt @Zle_to_Zleb_true … … 126 130 /2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??)))) 127 131 qed. 132 133 (* follows from (0 ≤ a < b → mod a b = a) *) 134 axiom Z_of_unsigned_bitvector_of_small_Z : 135 ∀z. OZ ≤ z → z < Z_two_power_nat 16 → Z_of_unsigned_bitvector 16 (bitvector_of_Z 16 z) = z. 136 137 theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p. 138 #n #m #p #Hle #Hlt /4 by monotonic_Zle_Zplus_r, Zle_to_Zlt, Zlt_to_Zle, transitive_Zle/ 139 qed. 140 141 (*  *) 142 (* Useful facts on blocks. *) 143 (*  *) 144 145 lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false. 146 #b1 #b2 #Hneq 147 @(eq_block_elim … b1 b2) 148 [ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??))) 149  2: #_ @refl ] qed. 150 151 lemma not_eq_block_rev : ∀b1,b2. b2 ≠ b1 → eq_block b1 b2 = false. 152 #b1 #b2 #Hneq 153 @(eq_block_elim … b1 b2) 154 [ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??))) 155  2: #_ @refl ] qed. 156 157 definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_block ?. 158 * #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2) 159 [ 1: #Heq >Heq cases r1 cases r2 normalize 160 >eqZb_z_z normalize try // @conj #H destruct (H) 161 try @refl 162  2: #Hneq cases r1 cases r2 normalize 163 >(eqZb_false … Hneq) normalize @conj 164 #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??))) 165 ] qed. 166 167 (*  *) 168 (* General results on lists. *) 169 (*  *) 170 171 (* If mem succeeds in finding an element, then the list can be partitioned around this element. *) 172 lemma list_mem_split : ∀A. ∀l : list A. ∀x : A. mem … x l → ∃l1,l2. l = l1 @ [x] @ l2. 173 #A #l elim l 174 [ 1: normalize #x @False_ind 175  2: #hd #tl #Hind #x whd in ⊢ (% → ?); * 176 [ 1: #Heq %{(nil ?)} %{tl} destruct @refl 177  2: #Hmem lapply (Hind … Hmem) * #l1 * #l2 #Heq_tl >Heq_tl 178 %{(hd :: l1)} %{l2} @refl 179 ] 180 ] qed. 181 182 lemma cons_to_append : ∀A. ∀hd : A. ∀l : list A. hd :: l = [hd] @ l. #A #hd #l @refl qed. 183 184 lemma fold_append : 185 ∀A,B:Type[0]. ∀l1, l2 : list A. ∀f:A → B → B. ∀seed. foldr ?? f seed (l1 @ l2) = foldr ?? f (foldr ?? f seed l2) l1. 186 #A #B #l1 elim l1 // 187 #hd #tl #Hind #l2 #f #seed normalize >Hind @refl 188 qed. 189 190 lemma filter_append : ∀A:Type[0]. ∀l1,l2 : list A. ∀f. filter ? f (l1 @ l2) = (filter ? f l1) @ (filter ? f l2). 191 #A #l1 elim l1 // 192 #hd #tl #Hind #l2 #f 193 >cons_to_append >associative_append 194 normalize cases (f hd) normalize 195 <Hind @refl 196 qed. 197 198 lemma filter_cons_unfold : ∀A:Type[0]. ∀f. ∀hd,tl. 199 filter ? f (hd :: tl) = 200 if f hd then 201 (hd :: filter A f tl) 202 else 203 (filter A f tl). 204 #A #f #hd #tl elim tl // qed. 205 206 207 lemma filter_elt_empty : ∀A:DeqSet. ∀elt,l. filter (carr A) (λx.¬(x==elt)) l = [ ] → All (carr A) (λx. x = elt) l. 208 #A #elt #l elim l 209 [ 1: // 210  2: #hd #tl #Hind >filter_cons_unfold 211 lapply (eqb_true A hd elt) 212 cases (hd==elt) normalize nodelta 213 [ 2: #_ #Habsurd destruct 214  1: * #H1 #H2 #Heq lapply (Hind Heq) #Hall whd @conj // 215 @H1 @refl 216 ] 217 ] qed. 218 219 lemma nil_append : ∀A. ∀(l : list A). [ ] @ l = l. // qed. 220 221 lemma mem_append : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) ↔ (mem … elt l1) ∨ (mem … elt l2). 222 #A #elt #l1 elim l1 223 [ 1: #l2 normalize @conj [ 1: #H %2 @H  2: * [ 1: @False_ind  2: #H @H ] ] 224  2: #hd #tl #Hind #l2 @conj 225 [ 1: whd in match (mem ???); * 226 [ 1: #Heq >Heq %1 normalize %1 @refl 227  2: #H1 lapply (Hind l2) * #HA #HB normalize 228 elim (HA H1) 229 [ 1: #H %1 %2 assumption  2: #H %2 assumption ] 230 ] 231  2: normalize * 232 [ 1: * /2 by or_introl, or_intror/ 233 #H %2 elim (Hind l2) #_ #H' @H' %1 @H 234  2: #H %2 elim (Hind l2) #_ #H' @H' %2 @H ] 235 ] 236 ] qed. 237 238 lemma mem_append_forward : ∀A:Type[0]. ∀elt : A. ∀l1,l2. mem … elt (l1 @ l2) → (mem … elt l1) ∨ (mem … elt l2). 239 #A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #H' #_ @H' @H qed. 240 241 lemma mem_append_backwards : ∀A:Type[0]. ∀elt : A. ∀l1,l2. (mem … elt l1) ∨ (mem … elt l2) → mem … elt (l1 @ l2) . 242 #A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #_ #H' @H' @H qed. 243 244 (*  *) 245 (* Generic properties of equivalence relations *) 246 (*  *) 247 248 lemma triangle_diagram : 249 ∀acctype : Type[0]. 250 ∀eqrel : acctype → acctype → Prop. 251 ∀refl_eqrel : reflexive ? eqrel. 252 ∀trans_eqrel : transitive ? eqrel. 253 ∀sym_eqrel : symmetric ? eqrel. 254 ∀a,b,c. eqrel a b → eqrel a c → eqrel b c. 255 #acctype #eqrel #R #T #S #a #b #c 256 #H1 #H2 @(T … (S … H1) H2) 257 qed. 258 259 lemma cotriangle_diagram : 260 ∀acctype : Type[0]. 261 ∀eqrel : acctype → acctype → Prop. 262 ∀refl_eqrel : reflexive ? eqrel. 263 ∀trans_eqrel : transitive ? eqrel. 264 ∀sym_eqrel : symmetric ? eqrel. 265 ∀a,b,c. eqrel b a → eqrel c a → eqrel b c. 266 #acctype #eqrel #R #T #S #a #b #c 267 #H1 #H2 @S @(T … H2 (S … H1)) 268 qed. 269 270 (*  *) 271 (* Quick and dirty implementation of finite sets relying on lists. The 272 * implementation is split in two: an abstract equivalence defined using inclusion 273 * of lists, and a concrete one where equivalence is defined as the closure of 274 * duplication, contraction and transposition of elements. We rely on the latter 275 * to prove stuff on folds over sets. *) 276 (*  *) 277 278 definition lset ≝ λA:Type[0]. list A. 279 280 (* The empty set. *) 281 definition empty_lset ≝ λA:Type[0]. nil A. 282 283 (* Standard operations. *) 284 definition lset_union ≝ λA:Type[0].λl1,l2 : lset A. l1 @ l2. 285 286 definition lset_remove ≝ λA:DeqSet.λl:lset (carr A).λelt:carr A. (filter … (λx.¬x==elt) l). 287 288 definition lset_difference ≝ λA:DeqSet.λl1,l2:lset (carr A). (filter … (λx.¬ (memb ? x l2)) l1). 289 290 (* Standard predicates on sets *) 291 definition lset_in ≝ λA:Type[0].λx : A. λl : lset A. mem … x l. 292 293 definition lset_disjoint ≝ λA:Type[0].λl1, l2 : lset A. 294 ∀x,y. mem … x l1 → mem … y l2 → x ≠ y. 295 296 definition lset_inclusion ≝ λA:Type[0].λl1,l2. 297 All A (λx1. mem … x1 l2) l1. 298 299 (* Definition of abstract set equivalence. *) 300 definition lset_eq ≝ λA:Type[0].λl1,l2. 301 lset_inclusion A l1 l2 ∧ 302 lset_inclusion A l2 l1. 303 304 (* Properties of inclusion. *) 305 lemma reflexive_lset_inclusion : ∀A. ∀l. lset_inclusion A l l. 306 #A #l elim l try // 307 #hd #tl #Hind whd @conj 308 [ 1: %1 @refl 309  2: whd in Hind; @(All_mp … Hind) 310 #a #H whd %2 @H 311 ] qed. 312 313 lemma transitive_lset_inclusion : ∀A. ∀l1,l2,l3. lset_inclusion A l1 l2 → lset_inclusion A l2 l3 → lset_inclusion A l1 l3 . 314 #A #l1 #l2 #l3 315 #Hincl1 #Hincl2 @(All_mp … Hincl1) 316 whd in Hincl2; 317 #a elim l2 in Hincl2; 318 [ 1: normalize #_ @False_ind 319  2: #hd #tl #Hind whd in ⊢ (% → ?); 320 * #Hmem #Hincl_tl whd in ⊢ (% → ?); 321 * [ 1: #Heq destruct @Hmem 322  2: #Hmem_tl @Hind assumption ] 323 ] qed. 324 325 lemma cons_preserves_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A l1 (x::l2). 326 #A #l1 #l2 #Hincl #x @(All_mp … Hincl) #a #Hmem whd %2 @Hmem qed. 327 328 lemma cons_monotonic_inclusion : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀x. lset_inclusion A (x::l1) (x::l2). 329 #A #l1 #l2 #Hincl #x whd @conj 330 [ 1: /2 by or_introl/ 331  2: @(All_mp … Hincl) #a #Hmem whd %2 @Hmem ] qed. 332 333 lemma lset_inclusion_concat : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A l1 (l3 @ l2). 334 #A #l1 #l2 #Hincl #l3 elim l3 335 try /2 by cons_preserves_inclusion/ 336 qed. 337 338 lemma lset_inclusion_concat_monotonic : ∀A. ∀l1,l2. lset_inclusion A l1 l2 → ∀l3. lset_inclusion A (l3 @ l1) (l3 @ l2). 339 #A #l1 #l2 #Hincl #l3 elim l3 340 try @Hincl #hd #tl #Hind @cons_monotonic_inclusion @Hind 341 qed. 342 343 (* lset_eq is an equivalence relation. *) 344 lemma reflexive_lset_eq : ∀A. ∀l. lset_eq A l l. /2 by conj/ qed. 345 346 lemma transitive_lset_eq : ∀A. ∀l1,l2,l3. lset_eq A l1 l2 → lset_eq A l2 l3 → lset_eq A l1 l3. 347 #A #l1 #l2 #l3 * #Hincl1 #Hincl2 * #Hincl3 #Hincl4 348 @conj @(transitive_lset_inclusion ??l2) assumption 349 qed. 350 351 lemma symmetric_lset_eq : ∀A. ∀l1,l2. lset_eq A l1 l2 → lset_eq A l2 l1. 352 #A #l1 #l2 * #Hincl1 #Hincl2 @conj assumption 353 qed. 354 355 (* Properties of inclusion vs union and equality. *) 356 lemma lset_union_inclusion : ∀A:Type[0]. ∀a,b,c. 357 lset_inclusion A a c → lset_inclusion ? b c → lset_inclusion ? (lset_union ? a b) c. 358 #A #a #b #c #H1 #H2 whd whd in match (lset_union ???); 359 @All_append assumption qed. 360 361 lemma lset_inclusion_union : ∀A:Type[0]. ∀a,b,c. 362 lset_inclusion A a b ∨ lset_inclusion A a c → lset_inclusion ? a (lset_union ? b c). 363 #A #a #b #c * 364 [ 1: @All_mp #elt #Hmem @mem_append_backwards %1 @Hmem 365  2: @All_mp #elt #Hmem @mem_append_backwards %2 @Hmem 366 ] qed. 367 368 lemma lset_inclusion_eq : ∀A : Type[0]. ∀a,b,c : lset A. 369 lset_eq ? a b → lset_inclusion ? b c → lset_inclusion ? a c. 370 #A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H1 H3) 371 qed. 372 373 lemma lset_inclusion_eq2 : ∀A : Type[0]. ∀a,b,c : lset A. 374 lset_eq ? b c → lset_inclusion ? a b → lset_inclusion ? a c. 375 #A #a #b #c * #H1 #H2 #H3 @(transitive_lset_inclusion … H3 H1) 376 qed. 377 378 (* Properties of lset_eq and mem *) 379 lemma lset_eq_mem : 380 ∀A:Type[0]. 381 ∀s1,s2 : lset A. 382 lset_eq ? s1 s2 → 383 ∀b.mem ? b s1 → mem ? b s2. 384 #A #s1 #s2 * #Hincl12 #_ #b 385 whd in Hincl12; elim s1 in Hincl12; 386 [ 1: normalize #_ * 387  2: #hd #tl #Hind whd in ⊢ (% → % → ?); * #Hmem' #Hall * #Heq 388 [ 1: destruct (Heq) assumption 389  2: @Hind assumption ] 390 ] qed. 391 392 lemma lset_eq_memb : 393 ∀A : DeqSet. 394 ∀s1,s2 : lset (carr A). 395 lset_eq ? s1 s2 → 396 ∀b.memb ? b s1 = true → memb ? b s2 = true. 397 #A #s1 #s2 #Heq #b 398 lapply (memb_to_mem A s1 b) #H1 #H2 399 lapply (H1 H2) #Hmem lapply (lset_eq_mem … Heq ? Hmem) @mem_to_memb 400 qed. 401 402 lemma lset_eq_memb_eq : 403 ∀A : DeqSet. 404 ∀s1,s2 : lset (carr A). 405 lset_eq ? s1 s2 → 406 ∀b.memb ? b s1 = memb ? b s2. 407 #A #s1 #s2 #Hlset_eq #b 408 lapply (lset_eq_memb … Hlset_eq b) 409 lapply (lset_eq_memb … (symmetric_lset_eq … Hlset_eq) b) 410 cases (b∈s1) 411 [ 1: #_ #H lapply (H (refl ??)) #Hmem >H @refl 412  2: cases (b∈s2) // #H lapply (H (refl ??)) #Habsurd destruct 413 ] qed. 414 415 lemma lset_eq_filter_eq : 416 ∀A : DeqSet. 417 ∀s1,s2 : lset (carr A). 418 lset_eq ? s1 s2 → 419 ∀l. 420 (filter ? (λwb.¬wb∈s1) l) = 421 (filter ? (λwb.¬wb∈s2) l). 422 #A #s1 #s2 #Heq #l elim l 423 [ 1: @refl 424  2: #hd #tl #Hind >filter_cons_unfold >filter_cons_unfold 425 >(lset_eq_memb_eq … Heq) cases (hd∈s2) 426 normalize in match (notb ?); normalize nodelta 427 try @Hind >Hind @refl 428 ] qed. 429 430 lemma cons_monotonic_eq : ∀A. ∀l1,l2 : lset A. lset_eq A l1 l2 → ∀x. lset_eq A (x::l1) (x::l2). 431 #A #l1 #l2 #Heq #x cases Heq #Hincl1 #Hincl2 432 @conj 433 [ 1: @cons_monotonic_inclusion 434  2: @cons_monotonic_inclusion ] 435 assumption 436 qed. 437 438 (* Properties of difference and remove *) 439 lemma lset_difference_unfold : 440 ∀A : DeqSet. 441 ∀s1, s2 : lset (carr A). 442 ∀hd. lset_difference A (hd :: s1) s2 = 443 if hd∈s2 then 444 lset_difference A s1 s2 445 else 446 hd :: (lset_difference A s1 s2). 447 #A #s1 #s2 #hd normalize 448 cases (hd∈s2) @refl 449 qed. 450 451 lemma lset_difference_unfold2 : 452 ∀A : DeqSet. 453 ∀s1, s2 : lset (carr A). 454 ∀hd. lset_difference A s1 (hd :: s2) = 455 lset_difference A (lset_remove ? s1 hd) s2. 456 #A #s1 457 elim s1 458 [ 1: // 459  2: #hd1 #tl1 #Hind #s2 #hd 460 whd in match (lset_remove ???); 461 whd in match (lset_difference A ??); 462 whd in match (memb ???); 463 lapply (eqb_true … hd1 hd) 464 cases (hd1==hd) normalize nodelta 465 [ 1: * #H #_ lapply (H (refl ??)) H #H 466 @Hind 467  2: * #_ #Hguard >lset_difference_unfold 468 cases (hd1∈s2) normalize in match (notb ?); normalize nodelta 469 <Hind @refl ] 470 ] qed. 471 472 lemma lset_difference_disjoint : 473 ∀A : DeqSet. 474 ∀s1,s2 : lset (carr A). 475 lset_disjoint A s1 (lset_difference A s2 s1). 476 #A #s1 elim s1 477 [ 1: #s2 normalize #x #y * 478  2: #hd1 #tl1 #Hind #s2 >lset_difference_unfold2 #x #y 479 whd in ⊢ (% → ?); * 480 [ 2: @Hind 481  1: #Heq >Heq elim s2 482 [ 1: normalize * 483  2: #hd2 #tl2 #Hind2 whd in match (lset_remove ???); 484 lapply (eqb_true … hd2 hd1) 485 cases (hd2 == hd1) normalize in match (notb ?); normalize nodelta * #H1 #H2 486 [ 1: @Hind2 487  2: >lset_difference_unfold cases (hd2 ∈ tl1) normalize nodelta try @Hind2 488 whd in ⊢ (% → ?); * 489 [ 1: #Hyhd2 destruct % #Heq lapply (H2 … (sym_eq … Heq)) #Habsurd destruct 490  2: @Hind2 ] 491 ] 492 ] 493 ] 494 ] qed. 495 496 497 lemma lset_remove_split : ∀A : DeqSet. ∀l1,l2 : lset A. ∀elt. lset_remove A (l1 @ l2) elt = (lset_remove … l1 elt) @ (lset_remove … l2 elt). 498 #A #l1 #l2 #elt /2 by filter_append/ qed. 499 500 lemma lset_inclusion_remove : 501 ∀A : DeqSet. 502 ∀s1, s2 : lset A. 503 lset_inclusion ? s1 s2 → 504 ∀elt. lset_inclusion ? (lset_remove ? s1 elt) (lset_remove ? s2 elt). 505 #A #s1 elim s1 506 [ 1: normalize // 507  2: #hd1 #tl1 #Hind1 #s2 * #Hmem #Hincl 508 elim (list_mem_split ??? Hmem) #s2A * #s2B #Hs2_eq destruct #elt 509 whd in match (lset_remove ???); 510 @(match (hd1 == elt) 511 return λx. (hd1 == elt = x) → ? 512 with 513 [ true ⇒ λH. ? 514  false ⇒ λH. ? ] (refl ? (hd1 == elt))) normalize in match (notb ?); 515 normalize nodelta 516 [ 1: @Hind1 @Hincl 517  2: whd @conj 518 [ 2: @(Hind1 … Hincl) 519  1: >lset_remove_split >lset_remove_split 520 normalize in match (lset_remove A [hd1] elt); 521 >H normalize nodelta @mem_append_backwards %2 522 @mem_append_backwards %1 normalize %1 @refl ] 523 ] 524 ] qed. 525 526 lemma lset_difference_lset_eq : 527 ∀A : DeqSet. ∀a,b,c. 528 lset_eq A b c → 529 lset_eq A (lset_difference A a b) (lset_difference A a c). 530 #A #a #b #c #Heq 531 whd in match (lset_difference ???) in ⊢ (??%%); 532 elim a 533 [ 1: normalize @conj @I 534  2: #hda #tla #Hind whd in match (foldr ?????) in ⊢ (??%%); 535 >(lset_eq_memb_eq … Heq hda) cases (hda∈c) 536 normalize in match (notb ?); normalize nodelta 537 try @Hind @cons_monotonic_eq @Hind 538 ] qed. 539 540 lemma lset_difference_lset_remove_commute : 541 ∀A:DeqSet. 542 ∀elt,s1,s2. 543 (lset_difference A (lset_remove ? s1 elt) s2) = 544 (lset_remove A (lset_difference ? s1 s2) elt). 545 #A #elt #s1 #s2 546 elim s1 try // 547 #hd #tl #Hind 548 >lset_difference_unfold 549 whd in match (lset_remove ???); 550 @(match (hd==elt) return λx. (hd==elt) = x → ? 551 with 552 [ true ⇒ λHhd. ? 553  false ⇒ λHhd. ? 554 ] (refl ? (hd==elt))) 555 @(match (hd∈s2) return λx. (hd∈s2) = x → ? 556 with 557 [ true ⇒ λHmem. ? 558  false ⇒ λHmem. ? 559 ] (refl ? (hd∈s2))) 560 >notb_true >notb_false normalize nodelta try // 561 try @Hind 562 [ 1: whd in match (lset_remove ???) in ⊢ (???%); >Hhd 563 elim (eqb_true ? elt elt) #_ #H >(H (refl ??)) 564 normalize in match (notb ?); normalize nodelta @Hind 565  2: >lset_difference_unfold >Hmem @Hind 566  3: whd in match (lset_remove ???) in ⊢ (???%); 567 >lset_difference_unfold >Hhd >Hmem 568 normalize in match (notb ?); 569 normalize nodelta >Hind @refl 570 ] qed. 571 572 (* Inversion lemma on emptyness *) 573 lemma lset_eq_empty_inv : ∀A. ∀l. lset_eq A l [ ] → l = [ ]. 574 #A #l elim l // 575 #hd' #tl' normalize #Hind * * @False_ind 576 qed. 577 578 (* Inversion lemma on singletons *) 579 lemma lset_eq_singleton_inv : ∀A,hd,l. lset_eq A [hd] (hd::l) → All ? (λx.x=hd) l. 580 #A #hd #l 581 * #Hincl1 whd in ⊢ (% → ?); * #_ @All_mp 582 normalize #a * [ 1: #H @H  2: @False_ind ] 583 qed. 584 585 (* Permutation of two elements on top of the list is ok. *) 586 lemma lset_eq_permute : ∀A,l,x1,x2. lset_eq A (x1 :: x2 :: l) (x2 :: x1 :: l). 587 #A #l #x1 #x2 @conj normalize 588 [ 1: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/ 589  2: /5 by cons_preserves_inclusion, All_mp, or_introl, or_intror, conj/ 590 ] qed. 591 592 (* "contraction" of an element. *) 593 lemma lset_eq_contract : ∀A,l,x. lset_eq A (x :: x :: l) (x :: l). 594 #A #l #x @conj 595 [ 1: /5 by or_introl, conj, transitive_lset_inclusion/ 596  2: /5 by cons_preserves_inclusion, cons_monotonic_inclusion/ ] 597 qed. 598 599 (* We don't need more than one instance of each element. *) 600 lemma lset_eq_filter : ∀A:DeqSet.∀tl.∀hd. 601 lset_eq A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl). 602 #A #tl elim tl 603 [ 1: #hd normalize /4 by or_introl, conj, I/ 604  2: #hd' #tl' #Hind #hd >filter_cons_unfold 605 lapply (eqb_true A hd' hd) cases (hd'==hd) 606 [ 2: #_ normalize in match (notb ?); normalize nodelta 607 lapply (cons_monotonic_eq … (Hind hd) hd') #H 608 lapply (lset_eq_permute ? tl' hd' hd) #H' 609 @(transitive_lset_eq ? ? (hd'::hd::tl') ? … H') 610 @(transitive_lset_eq ? ?? (hd'::hd::tl') … H) 611 @lset_eq_permute 612  1: * #Heq #_ >(Heq (refl ??)) normalize in match (notb ?); normalize nodelta 613 lapply (Hind hd) #H 614 @(transitive_lset_eq ? ? (hd::tl') (hd::hd::tl') H) 615 @conj 616 [ 1: whd @conj /2 by or_introl/ @cons_preserves_inclusion @cons_preserves_inclusion 617 @reflexive_lset_inclusion 618  2: whd @conj /2 by or_introl/ ] 619 ] 620 ] qed. 621 622 lemma lset_inclusion_filter_self : 623 ∀A:DeqSet.∀l,pred. 624 lset_inclusion A (filter ? pred l) l. 625 #A #l #pred elim l 626 [ 1: normalize @I 627  2: #hd #tl #Hind whd in match (filter ???); 628 cases (pred hd) normalize nodelta 629 [ 1: @cons_monotonic_inclusion @Hind 630  2: @cons_preserves_inclusion @Hind ] 631 ] qed. 632 633 lemma lset_inclusion_filter_monotonic : 634 ∀A:DeqSet.∀l1,l2. lset_inclusion (carr A) l1 l2 → 635 ∀elt. lset_inclusion A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2). 636 #A #l1 elim l1 637 [ 1: #l2 normalize // 638  2: #hd1 #tl1 #Hind #l2 whd in ⊢ (% → ?); * #Hmem1 #Htl1_incl #elt 639 whd >filter_cons_unfold 640 lapply (eqb_true A hd1 elt) cases (hd1==elt) 641 [ 1: * #H1 #_ lapply (H1 (refl ??)) #H1_eq >H1_eq in Hmem1; #Hmem 642 normalize in match (notb ?); normalize nodelta @Hind assumption 643  2: * #_ #Hneq normalize in match (notb ?); normalize nodelta 644 whd @conj 645 [ 1: elim l2 in Hmem1; try // 646 #hd2 #tl2 #Hincl whd in ⊢ (% → ?); * 647 [ 1: #Heq >Heq in Hneq; normalize 648 lapply (eqb_true A hd2 elt) cases (hd2==elt) 649 [ 1: * #H #_ #H2 lapply (H2 (H (refl ??))) #Habsurd destruct (Habsurd) 650  2: #_ normalize nodelta #_ /2 by or_introl/ ] 651  2: #H lapply (Hincl H) #Hok 652 normalize cases (hd2==elt) normalize nodelta 653 [ 1: @Hok 654  2: %2 @Hok ] ] 655  2: @Hind assumption ] ] ] 656 qed. 657 658 (* removing an element of two equivalent sets conserves equivalence. *) 659 lemma lset_eq_filter_monotonic : 660 ∀A:DeqSet.∀l1,l2. lset_eq (carr A) l1 l2 → 661 ∀elt. lset_eq A (filter ? (λx.¬(x==elt)) l1) (filter ? (λx.¬(x==elt)) l2). 662 #A #l1 #l2 * #Hincl1 #Hincl2 #elt @conj 663 /2 by lset_inclusion_filter_monotonic/ 664 qed. 665 666 (*  Concrete implementation of sets  *) 667 668 (* We can give an explicit characterization of equivalent sets: they are permutations with repetitions, i,e. 669 a composition of transpositions and duplications. We restrict ourselves to DeqSets. *) 670 inductive iso_step_lset (A : DeqSet) : lset A → lset A → Prop ≝ 671  lset_transpose : ∀a,x,b,y,c. iso_step_lset A (a @ [x] @ b @ [y] @ c) (a @ [y] @ b @ [x] @ c) 672  lset_weaken : ∀a,x,b. iso_step_lset A (a @ [x] @ b) (a @ [x] @ [x] @ b) 673  lset_contract : ∀a,x,b. iso_step_lset A (a @ [x] @ [x] @ b) (a @ [x] @ b). 674 675 (* The equivalence is the reflexive, transitive and symmetric closure of iso_step_lset *) 676 inductive lset_eq_concrete (A : DeqSet) : lset A → lset A → Prop ≝ 677  lset_trans : ∀a,b,c. iso_step_lset A a b → lset_eq_concrete A b c → lset_eq_concrete A a c 678  lset_refl : ∀a. lset_eq_concrete A a a. 679 680 (* lset_eq_concrete is symmetric and transitive *) 681 lemma transitive_lset_eq_concrete : ∀A,l1,l2,l3. lset_eq_concrete A l1 l2 → lset_eq_concrete A l2 l3 → lset_eq_concrete A l1 l3. 682 #A #l1 #l2 #l3 #Hequiv 683 elim Hequiv // 684 #a #b #c #Hstep #Hequiv #Hind #Hcl3 lapply (Hind Hcl3) #Hbl3 685 @(lset_trans ???? Hstep Hbl3) 686 qed. 687 688 lemma symmetric_step : ∀A,l1,l2. iso_step_lset A l1 l2 → iso_step_lset A l2 l1. 689 #A #l1 #l2 * /2/ qed. 690 691 lemma symmetric_lset_eq_concrete : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq_concrete A l2 l1. 692 #A #l1 #l2 #H elim H // 693 #a #b #c #Hab #Hbc #Hcb 694 @(transitive_lset_eq_concrete ???? Hcb ?) 695 @(lset_trans … (symmetric_step ??? Hab) (lset_refl …)) 696 qed. 697 698 (* lset_eq_concrete is conserved by cons. *) 699 lemma equivalent_step_cons : ∀A,l1,l2. iso_step_lset A l1 l2 → ∀x. iso_step_lset A (x :: l1) (x :: l2). 700 #A #l1 #l2 * // qed. (* That // was impressive. *) 701 702 lemma lset_eq_concrete_cons : ∀A,l1,l2. lset_eq_concrete A l1 l2 → ∀x. lset_eq_concrete A (x :: l1) (x :: l2). 703 #A #l1 #l2 #Hequiv elim Hequiv try // 704 #a #b #c #Hab #Hbc #Hind #x %1{(equivalent_step_cons ??? Hab x) (Hind x)} 705 qed. 706 707 lemma absurd_list_eq_append : ∀A.∀x.∀l1,l2:list A. [ ] = l1 @ [x] @ l2 → False. 708 #A #x #l1 #l2 elim l1 normalize 709 [ 1: #Habsurd destruct 710  2: #hd #tl #_ #Habsurd destruct 711 ] qed. 712 713 (* Inversion lemma for emptyness, step case *) 714 lemma equivalent_iso_step_empty_inv : ∀A,l. iso_step_lset A l [] → l = [ ]. 715 #A #l elim l // 716 #hd #tl #Hind #H inversion H 717 [ 1: #a #x #b #y #c #_ #Habsurd 718 @(False_ind … (absurd_list_eq_append ? y … Habsurd)) 719  2: #a #x #b #_ #Habsurd 720 @(False_ind … (absurd_list_eq_append ? x … Habsurd)) 721  3: #a #x #b #_ #Habsurd 722 @(False_ind … (absurd_list_eq_append ? x … Habsurd)) 723 ] qed. 724 725 (* Same thing for nonemptyness *) 726 lemma equivalent_iso_step_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → iso_step_lset A l1 l2 → l2 ≠ [ ]. 727 #A #l1 elim l1 728 [ 1: #l2 * #H @(False_ind … (H (refl ??))) 729  2: #hd #tl #H #l2 #_ #Hstep % #Hl2 >Hl2 in Hstep; #Hstep 730 lapply (equivalent_iso_step_empty_inv … Hstep) #Habsurd destruct 731 ] qed. 732 733 lemma lset_eq_concrete_cons_inv : ∀A,l1,l2. l1 ≠ [ ] → lset_eq_concrete A l1 l2 → l2 ≠ [ ]. 734 #A #l1 #l2 #Hl1 #H lapply Hl1 elim H 735 [ 2: #a #H @H 736  1: #a #b #c #Hab #Hbc #H #Ha lapply (equivalent_iso_step_cons_inv … Ha Hab) #Hb @H @Hb 737 ] qed. 738 739 lemma lset_eq_concrete_empty_inv : ∀A,l1,l2. l1 = [ ] → lset_eq_concrete A l1 l2 → l2 = [ ]. 740 #A #l1 #l2 #Hl1 #H lapply Hl1 elim H // 741 #a #b #c #Hab #Hbc #Hbc_eq #Ha >Ha in Hab; #H_b lapply (equivalent_iso_step_empty_inv … ?? (symmetric_step … H_b)) 742 #Hb @Hbc_eq @Hb 743 qed. 744 745 (* Square equivalence diagram *) 746 lemma square_lset_eq_concrete : 747 ∀A. ∀a,b,a',b'. lset_eq_concrete A a b → lset_eq_concrete A a a' → lset_eq_concrete A b b' → lset_eq_concrete A a' b'. 748 #A #a #b #a' #b' #H1 #H2 #H3 749 @(transitive_lset_eq_concrete ???? (symmetric_lset_eq_concrete … H2)) 750 @(transitive_lset_eq_concrete ???? H1) 751 @H3 752 qed. 753 754 (* Make the transposition of elements visible at toplevel *) 755 lemma transpose_lset_eq_concrete : 756 ∀A. ∀x,y,a,b,c,a',b',c'. 757 lset_eq_concrete A (a @ [x] @ b @ [y] @ c) (a' @ [x] @ b' @ [y] @ c') → 758 lset_eq_concrete A (a @ [y] @ b @ [x] @ c) (a' @ [y] @ b' @ [x] @ c'). 759 #A #x #y #a #b #c #a' #b' #c 760 #H @(square_lset_eq_concrete ????? H) /2 by lset_trans, lset_refl, lset_transpose/ 761 qed. 762 763 lemma switch_lset_eq_concrete : 764 ∀A. ∀a,b,c. lset_eq_concrete A (a@[b]@c) ([b]@a@c). 765 #A #a elim a // 766 #hda #tla #Hind #b #c lapply (Hind hda c) #H 767 lapply (lset_eq_concrete_cons … H b) 768 #H' normalize in H' ⊢ %; @symmetric_lset_eq_concrete 769 /3 by lset_transpose, lset_trans, symmetric_lset_eq_concrete/ 770 qed. 771 772 (* Folding a commutative and idempotent function on equivalent sets yields the same result. *) 773 lemma lset_eq_concrete_fold : 774 ∀A : DeqSet. 775 ∀acctype : Type[0]. 776 ∀l1,l2 : list (carr A). 777 lset_eq_concrete A l1 l2 → 778 ∀f:carr A → acctype → acctype. 779 (∀x1,x2. ∀acc. f x1 (f x2 acc) = f x2 (f x1 acc)) → 780 (∀x.∀acc. f x (f x acc) = f x acc) → 781 ∀acc. foldr ?? f acc l1 = foldr ?? f acc l2. 782 #A #acctype #l1 #l2 #Heq #f #Hcomm #Hidem 783 elim Heq 784 try // 785 #a' #b' #c' #Hstep #Hbc #H #acc <H H 786 elim Hstep 787 [ 1: #a #x #b #y #c 788 >fold_append >fold_append >fold_append >fold_append 789 >fold_append >fold_append >fold_append >fold_append 790 normalize 791 cut (f x (foldr A acctype f (f y (foldr A acctype f acc c)) b) = 792 f y (foldr A acctype f (f x (foldr A acctype f acc c)) b)) [ 793 elim c 794 [ 1: normalize elim b 795 [ 1: normalize >(Hcomm x y) @refl 796  2: #hdb #tlb #Hind normalize 797 >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ] 798  2: #hdc #tlc #Hind normalize elim b 799 [ 1: normalize >(Hcomm x y) @refl 800  2: #hdb #tlb #Hind normalize 801 >(Hcomm x hdb) >(Hcomm y hdb) >Hind @refl ] ] 802 ] 803 #Hind >Hind @refl 804  2: #a #x #b 805 >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x])) 806 normalize >Hidem @refl 807  3: #a #x #b 808 >fold_append >(fold_append ?? ([x]@[x])) >fold_append >fold_append 809 normalize >Hidem @refl 810 ] qed. 811 812 (* Folding over equivalent sets yields equivalent results, for any equivalence. *) 813 lemma inj_to_fold_inj : 814 ∀A,acctype : Type[0]. 815 ∀eqrel : acctype → acctype → Prop. 816 ∀refl_eqrel : reflexive ? eqrel. 817 ∀trans_eqrel : transitive ? eqrel. 818 ∀sym_eqrel : symmetric ? eqrel. 819 ∀f : A → acctype → acctype. 820 (∀x:A.∀acc1:acctype.∀acc2:acctype.eqrel acc1 acc2→eqrel (f x acc1) (f x acc2)) → 821 ∀l : list A. ∀acc1, acc2 : acctype. eqrel acc1 acc2 → eqrel (foldr … f acc1 l) (foldr … f acc2 l). 822 #A #acctype #eqrel #R #T #S #f #Hinj #l elim l 823 // 824 #hd #tl #Hind #acc1 #acc2 #Heq normalize @Hinj @Hind @Heq 825 qed. 826 827 (* We need to extend the above proof to arbitrary equivalence relation instead of 828 just standard equality. *) 829 lemma lset_eq_concrete_fold_ext : 830 ∀A : DeqSet. 831 ∀acctype : Type[0]. 832 ∀eqrel : acctype → acctype → Prop. 833 ∀refl_eqrel : reflexive ? eqrel. 834 ∀trans_eqrel : transitive ? eqrel. 835 ∀sym_eqrel : symmetric ? eqrel. 836 ∀f:carr A → acctype → acctype. 837 (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) → 838 (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) → 839 (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) → 840 ∀l1,l2 : list (carr A). 841 lset_eq_concrete A l1 l2 → 842 ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2). 843 #A #acctype #eqrel #R #T #S #f #Hinj #Hcomm #Hidem #l1 #l2 #Heq 844 elim Heq 845 try // 846 #a' #b' #c' #Hstep #Hbc #H inversion Hstep 847 [ 1: #a #x #b #y #c #HlA #HlB #_ #acc 848 >HlB in H; #H @(T … ? (H acc)) 849 >fold_append >fold_append >fold_append >fold_append 850 >fold_append >fold_append >fold_append >fold_append 851 normalize 852 cut (eqrel (f x (foldr ? acctype f (f y (foldr ? acctype f acc c)) b)) 853 (f y (foldr ? acctype f (f x (foldr ? acctype f acc c)) b))) 854 [ 1: 855 elim c 856 [ 1: normalize elim b 857 [ 1: normalize @(Hcomm x y) 858  2: #hdb #tlb #Hind normalize 859 lapply (Hinj hdb ?? Hind) #Hind' 860 lapply (T … Hind' (Hcomm ???)) #Hind'' 861 @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ] 862  2: #hdc #tlc #Hind normalize elim b 863 [ 1: normalize @(Hcomm x y) 864  2: #hdb #tlb #Hind normalize 865 lapply (Hinj hdb ?? Hind) #Hind' 866 lapply (T … Hind' (Hcomm ???)) #Hind'' 867 @S @(triangle_diagram ? eqrel R T S … Hind'') @Hcomm ] 868 ] ] 869 #Hind @(inj_to_fold_inj … eqrel R T S ? Hinj … Hind) 870  2: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc)) 871 >fold_append >fold_append >fold_append >(fold_append ?? ([x]@[x])) 872 normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @S @Hidem 873  3: #a #x #b #HeqA #HeqB #_ #acc >HeqB in H; #H @(T … (H acc)) 874 >fold_append >(fold_append ?? ([x]@[x])) >fold_append >fold_append 875 normalize @(inj_to_fold_inj … eqrel R T S ? Hinj) @Hidem 876 ] qed. 877 878 (* Prepare some wellfounded induction principles on lists. The idea is to perform 879 an induction on the sequence of filterees of a list : taking the first element, 880 filtering it out of the tail, etc. We give such principles for pairs of lists 881 and isolated lists. *) 882 883 (* The two lists [l1,l2] share at least the head of l1. *) 884 definition head_shared ≝ λA. λl1,l2 : list A. 885 match l1 with 886 [ nil ⇒ l2 = (nil ?) 887  cons hd _ ⇒ mem … hd l2 888 ]. 889 890 (* Relation on pairs of lists, as described above. *) 891 definition filtered_lists : ∀A:DeqSet. relation (list (carr A)×(list (carr A))) ≝ 892 λA:DeqSet. λll1,ll2. 893 let 〈la1,lb1〉 ≝ ll1 in 894 let 〈la2,lb2〉 ≝ ll2 in 895 match la2 with 896 [ nil ⇒ False 897  cons hda2 tla2 ⇒ 898 head_shared ? la2 lb2 ∧ 899 la1 = filter … (λx.¬(x==hda2)) tla2 ∧ 900 lb1 = filter … (λx.¬(x==hda2)) lb2 901 ]. 902 903 (* Notice the absence of plural : this relation works on a simple list, not a pair. *) 904 definition filtered_list : ∀A:DeqSet. relation (list (carr A)) ≝ 905 λA:DeqSet. λl1,l2. 906 match l2 with 907 [ nil ⇒ False 908  cons hd2 tl2 ⇒ 909 l1 = filter … (λx.¬(x==hd2)) l2 910 ]. 911 912 (* Relation on lists based on their lengths. We know this one is wellfounded. *) 913 definition length_lt : ∀A:DeqSet. relation (list (carr A)) ≝ 914 λA:DeqSet. λl1,l2. lt (length ? l1) (length ? l2). 915 916 (* length_lt can be extended on pairs by just measuring the first component *) 917 definition length_fst_lt : ∀A:DeqSet. relation (list (carr A) × (list (carr A))) ≝ 918 λA:DeqSet. λll1,ll2. lt (length ? (\fst ll1)) (length ? (\fst ll2)). 919 920 lemma filter_length : ∀A. ∀l. ∀f. filter A f l ≤ l. 921 #A #l #f elim l // 922 #hd #tl #Hind whd in match (filter ???); cases (f hd) normalize nodelta 923 [ 1: /2 by le_S_S/ 924  2: @le_S @Hind 925 ] qed. 926 927 (* The order on lists defined by their length is wf *) 928 lemma length_lt_wf : ∀A. ∀l. WF (list (carr A)) (length_lt A) l. 929 #A #l % elim l 930 [ 1: #a normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind 931  2: #hd #tl #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd 932 @(transitive_le … Hlt') @(monotonic_pred … Hlt) 933 qed. 934 935 (* Order on pairs of list by measuring the first proj *) 936 lemma length_fst_lt_wf : ∀A. ∀ll. WF ? (length_fst_lt A) ll. 937 #A * #l1 #l2 % elim l1 938 [ 1: * #a1 #a2 normalize in ⊢ (% → ?); #H lapply (le_S_O_absurd ? H) @False_ind 939  2: #hd1 #tl1 #Hind #a #Hlt % #a' #Hlt' @Hind whd in Hlt Hlt'; whd 940 @(transitive_le … Hlt') @(monotonic_pred … Hlt) 941 qed. 942 943 lemma length_to_filtered_lists : ∀A. subR ? (filtered_lists A) (length_fst_lt A). 944 #A whd * #a1 #a2 * #b1 #b2 elim b1 945 [ 1: @False_ind 946  2: #hd1 #tl1 #Hind whd in ⊢ (% → ?); * * #Hmem #Ha1 #Ha2 whd 947 >Ha1 whd in match (length ??) in ⊢ (??%); @le_S_S @filter_length 948 ] qed. 949 950 lemma length_to_filtered_list : ∀A. subR ? (filtered_list A) (length_lt A). 951 #A whd #a #b elim b 952 [ 1: @False_ind 953  2: #hd #tl #Hind whd in ⊢ (% → ?); whd in match (filter ???); 954 lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?); 955 normalize nodelta #Ha whd @le_S_S >Ha @filter_length ] 956 qed. 957 958 (* Prove wellfoundedness by embedding in lt *) 959 lemma filtered_lists_wf : ∀A. ∀ll. WF ? (filtered_lists A) ll. 960 #A #ll @(WF_antimonotonic … (length_to_filtered_lists A)) @length_fst_lt_wf 961 qed. 962 963 lemma filtered_list_wf : ∀A. ∀l. WF ? (filtered_list A) l. 964 #A #l @(WF_antimonotonic … (length_to_filtered_list A)) @length_lt_wf 965 qed. 966 967 definition Acc_elim : ∀A,R,x. WF A R x → (∀a. R a x → WF A R a) ≝ 968 λA,R,x,acc. 969 match acc with 970 [ wf _ a0 ⇒ a0 ]. 971 972 (* Stolen from Coq. Warped to avoid proptotype restriction. *) 973 let rec WF_rect 974 (A : Type[0]) 975 (R : A → A → Prop) 976 (P : A → Type[0]) 977 (f : ∀ x : A. 978 (∀ y : A. R y x → WF ? R y) → 979 (∀ y : A. R y x → P y) → P x) 980 (x : A) 981 (a : WF A R x) on a : P x ≝ 982 f x (Acc_elim … a) (λy:A. λRel:R y x. WF_rect A R P f y ((Acc_elim … a) y Rel)). 983 984 lemma lset_eq_concrete_filter : ∀A:DeqSet.∀tl.∀hd. 985 lset_eq_concrete A (hd :: (filter ? (λy.notb (eqb A y hd)) tl)) (hd :: tl). 986 #A #tl elim tl 987 [ 1: #hd // 988  2: #hd' #tl' #Hind #hd >filter_cons_unfold 989 lapply (eqb_true A hd' hd) 990 cases (hd'==hd) 991 [ 2: #_ normalize in match (notb false); normalize nodelta 992 >cons_to_append >(cons_to_append … hd') 993 >cons_to_append in ⊢ (???%); >(cons_to_append … hd') in ⊢ (???%); 994 @(transpose_lset_eq_concrete ? hd' hd [ ] [ ] (filter A (λy:A.¬y==hd) tl') [ ] [ ] tl') 995 >nil_append >nil_append >nil_append >nil_append 996 @lset_eq_concrete_cons >nil_append >nil_append 997 @Hind 998  1: * #H1 #_ lapply (H1 (refl ??)) #Heq normalize in match (notb ?); normalize nodelta 999 >Heq >cons_to_append >cons_to_append in ⊢ (???%); >cons_to_append in ⊢ (???(???%)); 1000 @(square_lset_eq_concrete A ([hd]@filter A (λy:A.¬y==hd) tl') ([hd]@tl')) 1001 [ 1: @Hind 1002  2: %2 1003  3: %1{???? ? (lset_refl ??)} /2 by lset_weaken/ ] 1004 ] 1005 ] qed. 1006 1007 1008 (* The "abstract", observational definition of set equivalence implies the concrete one. *) 1009 1010 lemma lset_eq_to_lset_eq_concrete_aux : 1011 ∀A,ll. 1012 head_shared … (\fst ll) (\snd ll) → 1013 lset_eq (carr A) (\fst ll) (\snd ll) → 1014 lset_eq_concrete A (\fst ll) (\snd ll). 1015 #A #ll @(WF_ind ????? (filtered_lists_wf A ll)) 1016 * * 1017 [ 1: #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hb2 >Hb2 #_ %2 1018  2: #hd1 #tl1 #b2 #Hwf #Hind_wf whd in ⊢ (% → ?); #Hmem 1019 lapply (list_mem_split ??? Hmem) * #l2A * #l2B #Hb2 #Heq 1020 destruct 1021 lapply (Hind_wf 〈filter … (λx.¬x==hd1) tl1,filter … (λx.¬x==hd1) (l2A@l2B)〉) 1022 cut (filtered_lists A 〈filter A (λx:A.¬x==hd1) tl1,filter A (λx:A.¬x==hd1) (l2A@l2B)〉 〈hd1::tl1,l2A@[hd1]@l2B〉) 1023 [ @conj try @conj try @refl whd 1024 [ 1: /2 by / 1025  2: >filter_append in ⊢ (???%); >filter_append in ⊢ (???%); 1026 whd in match (filter ?? [hd1]); 1027 elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?); 1028 normalize nodelta <filter_append @refl ] ] 1029 #Hfiltered #Hind_aux lapply (Hind_aux Hfiltered) Hind_aux 1030 cut (lset_eq A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B))) 1031 [ 1: lapply (lset_eq_filter_monotonic … Heq hd1) 1032 >filter_cons_unfold >filter_append >(filter_append … [hd1]) 1033 whd in match (filter ?? [hd1]); 1034 elim (eqb_true A hd1 hd1) #_ #H >(H (refl ??)) normalize in match (notb ?); 1035 normalize nodelta <filter_append #Hsol @Hsol ] 1036 #Hset_eq 1037 cut (head_shared A (filter A (λx:A.¬x==hd1) tl1) (filter A (λx:A.¬x==hd1) (l2A@l2B))) 1038 [ 1: lapply Hset_eq cases (filter A (λx:A.¬x==hd1) tl1) 1039 [ 1: whd in ⊢ (% → ?); * #_ elim (filter A (λx:A.¬x==hd1) (l2A@l2B)) // 1040 #hd' #tl' normalize #Hind * @False_ind 1041  2: #hd' #tl' * #Hincl1 #Hincl2 whd elim Hincl1 #Hsol #_ @Hsol ] ] 1042 #Hshared #Hind_aux lapply (Hind_aux Hshared Hset_eq) 1043 #Hconcrete_set_eq 1044 >cons_to_append 1045 @(transitive_lset_eq_concrete ? ([hd1]@tl1) ([hd1]@l2A@l2B) (l2A@[hd1]@l2B)) 1046 [ 2: @symmetric_lset_eq_concrete @switch_lset_eq_concrete ] 1047 lapply (lset_eq_concrete_cons … Hconcrete_set_eq hd1) #Hconcrete_cons_eq 1048 @(square_lset_eq_concrete … Hconcrete_cons_eq) 1049 [ 1: @(lset_eq_concrete_filter ? tl1 hd1) 1050  2: @(lset_eq_concrete_filter ? (l2A@l2B) hd1) ] 1051 ] qed. 1052 1053 lemma lset_eq_to_lset_eq_concrete : ∀A,l1,l2. lset_eq (carr A) l1 l2 → lset_eq_concrete A l1 l2. 1054 #A * 1055 [ 1: #l2 #Heq >(lset_eq_empty_inv … (symmetric_lset_eq … Heq)) // 1056  2: #hd1 #tl1 #l2 #Hincl lapply Hincl lapply (lset_eq_to_lset_eq_concrete_aux ? 〈hd1::tl1,l2〉) #H @H 1057 whd elim Hincl * // 1058 ] qed. 1059 1060 1061 (* The concrete one implies the abstract one. *) 1062 lemma lset_eq_concrete_to_lset_eq : ∀A,l1,l2. lset_eq_concrete A l1 l2 → lset_eq A l1 l2. 1063 #A #l1 #l2 #Hconcrete 1064 elim Hconcrete try // 1065 #a #b #c #Hstep #Heq_bc_concrete #Heq_bc 1066 cut (lset_eq A a b) 1067 [ 1: elim Hstep 1068 [ 1: #a' elim a' 1069 [ 2: #hda #tla #Hind #x #b' #y #c' >cons_to_append 1070 >(associative_append ? [hda] tla ?) 1071 >(associative_append ? [hda] tla ?) 1072 @cons_monotonic_eq >nil_append >nil_append @Hind 1073  1: #x #b' #y #c' >nil_append >nil_append 1074 elim b' try // 1075 #hdb #tlc #Hind >append_cons >append_cons in ⊢ (???%); 1076 >associative_append >associative_append 1077 lapply (cons_monotonic_eq … Hind hdb) #Hind' 1078 @(transitive_lset_eq ? ([x]@[hdb]@tlc@[y]@c') ([hdb]@[x]@tlc@[y]@c')) 1079 /2 by transitive_lset_eq/ ] 1080  2: #a' elim a' 1081 [ 2: #hda #tla #Hind #x #b' >cons_to_append 1082 >(associative_append ? [hda] tla ?) 1083 >(associative_append ? [hda] tla ?) 1084 @cons_monotonic_eq >nil_append >nil_append @Hind 1085  1: #x #b' >nil_append >nil_append @conj normalize 1086 [ 1: @conj [ 1: %1 @refl ] elim b' 1087 [ 1: @I 1088  2: #hdb #tlb #Hind normalize @conj 1089 [ 1: %2 %2 %1 @refl 1090  2: @(All_mp … Hind) #a0 * 1091 [ 1: #Heq %1 @Heq 1092  2: * /2 by or_introl, or_intror/ ] ] ] 1093 #H %2 %2 %2 @H 1094  2: @conj try @conj try /2 by or_introl, or_intror/ elim b' 1095 [ 1: @I 1096  2: #hdb #tlb #Hind normalize @conj 1097 [ 1: %2 %1 @refl 1098  2: @(All_mp … Hind) #a0 * 1099 [ 1: #Heq %1 @Heq 1100  2: #H %2 %2 @H ] ] ] ] ] 1101  3: #a #x #b elim a try @lset_eq_contract 1102 #hda #tla #Hind @cons_monotonic_eq @Hind ] ] 1103 #Heq_ab @(transitive_lset_eq … Heq_ab Heq_bc) 1104 qed. 1105 1106 lemma lset_eq_fold : 1107 ∀A : DeqSet. 1108 ∀acctype : Type[0]. 1109 ∀eqrel : acctype → acctype → Prop. 1110 ∀refl_eqrel : reflexive ? eqrel. 1111 ∀trans_eqrel : transitive ? eqrel. 1112 ∀sym_eqrel : symmetric ? eqrel. 1113 ∀f:carr A → acctype → acctype. 1114 (∀x,acc1,acc2. eqrel acc1 acc2 → eqrel (f x acc1) (f x acc2)) → 1115 (∀x1,x2. ∀acc. eqrel (f x1 (f x2 acc)) (f x2 (f x1 acc))) → 1116 (∀x.∀acc. eqrel (f x (f x acc)) (f x acc)) → 1117 ∀l1,l2 : list (carr A). 1118 lset_eq A l1 l2 → 1119 ∀acc. eqrel (foldr ?? f acc l1) (foldr ?? f acc l2). 1120 #A #acctype #eqrel #refl_eqrel #trans_eqrel #sym_eqrel #f #Hinj #Hsym #Hcontract #l1 #l2 #Heq #acc 1121 lapply (lset_eq_to_lset_eq_concrete … Heq) #Heq_concrete 1122 @(lset_eq_concrete_fold_ext A acctype eqrel refl_eqrel trans_eqrel sym_eqrel f Hinj Hsym Hcontract l1 l2 Heq_concrete acc) 1123 qed. 1124 1125 1126
Note: See TracChangeset
for help on using the changeset viewer.