-definition sublist ≝
- λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
-
-lemma memb_exists: ∀S,a,l.memb S a l = true →
- ∃l1,l2.l=l1@(a::l2).
-#S #a #l elim l [normalize #abs @False_ind /2/]
-#b #tl #Hind #H cases (orb_true_l … H)
- [#eqba @(ex_intro … (nil S)) @(ex_intro … tl)
- >(proj1 … (eqb_true …) eqba) //
- |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
- @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
- ]
-qed.
-
-lemma length_append: ∀A.∀l1,l2:list A.
- |l1@l2| = |l1|+|l2|.
-#A #l1 elim l1 // normalize /2/
-qed.
-
-lemma sublist_length: ∀S,l1,l2.
- uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
-#S #l1 elim l1 //
-#a #tl #Hind #l2 #unique #sub
-cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub //]
-* #l3 * #l4 #eql2 >eql2 >length_append normalize
-applyS le_S_S <length_append @Hind [@(andb_true_l2 … unique)]
->eql2 in sub; #sub #x #membx
-cases (memb_append … (sub x (orb_true_r2 … membx)))
- [#membxl3 @memb_append_l1 //
- |#membxal4 cases (orb_true_l … membxal4)
- [#eqax @False_ind cases (andb_true_l … unique)
- >(proj1 … (eqb_true …) eqax) >membx normalize /2/
- |#membxl4 @memb_append_l2 //
- ]
- ]
-qed.
-
-axiom memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true →
-memb S x l = true ∧ (f x = true).
-
-axiom memb_filter_l: ∀S,f,l,x. memb S x l = true → (f x = true) →
-memb S x (filter ? f l) = true.
-
-axiom sublist_unique_append_l1:
- ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
-
-axiom sublist_unique_append_l2:
- ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
-
-definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
- foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.