-lemma notb_eq_true_r: ∀b. b = false → notb b = true.
-#b cases b normalize //
-qed.
-
-lemma notb_eq_false_l:∀b. notb b = false → b = true.
-#b cases b normalize //
-qed.
-
-lemma notb_eq_false_r:∀b. b = true → notb b = false.
-#b cases b normalize //
-qed.
-
-
-axiom filter_true: ∀S,f,a,l.
- memb S a (filter S f l) = true → f a = true.
-(*
-#S #f #a #l elim l [normalize #H @False_ind /2/]
-#b #tl #Hind normalize cases (f b) normalize *)
-
-axiom memb_filter_memb: ∀S,f,a,l.
- memb S a (filter S f l) = true → memb S a l = true.
-
-axiom unique_append_elim: ∀S:Alpha.∀P: S → Prop.∀l1,l2.
-(∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) →
-∀x. memb S x (unique_append S l1 l2) = true → P x.
-
-axiom not_memb_to_not_eq: ∀S,a,b,l.
- memb S a l = false → memb S b l = true → a==b = false.
-
-include "arithmetics/exp.ma".
-
-let rec pos S (i:re S) on i ≝
- match i with
- [ z ⇒ 0
- | e ⇒ 0
- | s y ⇒ 1
- | o i1 i2 ⇒ pos S i1 + pos S i2
- | c i1 i2 ⇒ pos S i1 + pos S i2
- | k i ⇒ pos S i
- ].
-
-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.
-