-(*
-Effective searching
-
-The fact of being able to decide, via a computable boolean function, the
-equality between elements of a given set is an essential prerequisite for
-effectively searching an element of that set inside a data structure. In this
-section we shall define several boolean functions acting on lists of elements in
-a DeqSet, and prove some of their properties.*)
+(*
+ More Data Types
+*)
-include "basics/list.ma".
include "tutorial/chapter4.ma".
+include "arithmetics/nat.ma".
-(* The first function we define is an effective version of the membership relation,
-between an element x and a list l. Its definition is a straightforward recursion on
-l.*)
-let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝
- match l with
- [ nil ⇒ false
- | cons a tl ⇒ (x == a) ∨ memb S x tl
+(******************************** Option Type *********************************)
+
+(* Matita may only define total functions. However, not always we may return a
+meaningful value: for instance, working on natural numbers, the predecessor of
+0 is undefined. In these situations, we may either return a default value
+(usually, pred 0 = 0), or decide to return an "option type" as a result. An
+Option type is a polymorphic type that represents encapsulation of an optional
+value. It consists of either an empty constructor (traditionally called None),
+or a constructor encapsulating the original data type A (written Some A): *)
+
+inductive option (A:Type[0]) : Type[0] ≝
+ None : option A
+ | Some : A → option A.
+
+let rec pred (n:nat) : option nat ≝
+ match n with
+ [ O ⇒ None nat
+ | S a ⇒ Some nat a
].
-notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
-interpretation "boolean membership" 'memb a l = (memb ? a l).
-
-(* We can now prove several interesing properties for memb:
-- memb_hd: x is a member of x::l
-- memb_cons: if x is a member of l than x is a member of a::l
-- memb_single: if x is a member of [a] then x=a
-- memb_append: if x is a member of l1@l2 then either x is a member of l1
- or x is a member of l2
-- memb_append_l1: if x is a member of l1 then x is a member of l1@l2
-- memb_append_l2: if x is a member of l2 then x is a member of l1@l2
-- memb_exists: if x is a member of l, than l can decomposed as l1@(x::l2)
-- not_memb_to_not_eq: if x is not a member of l and y is, then x≠y
-- memb_map: if a is a member of l, then (f a) is a member of (map f l)
-- memb_compose: if a is a member of l1 and b is a meber of l2 than
- (op a b) is a member of (compose op l1 l2)
-*)
+(* The type option A is isomorphic to the disjoint sum between A and unit. The
+two bijections are simply defined as follows: *)
+
+definition option_to_sum : ∀A.option A → unit + A ≝ λA.λx:option A.
+ match x with
+ [ None ⇒ inl ?? it
+ | Some a ⇒ inr ?? a ].
+
+definition sum_to_option :∀A. unit + A → option A ≝ λA.λx:unit+A.
+ match x with
+ [ inl a ⇒ None A
+ | inr a ⇒ Some A a ].
+
+(* The fact that going from the option type to the sum and back again we get the
+original element follows from a straightforward case analysis: *)
+
+lemma option_bij1: ∀A,x. sum_to_option A (option_to_sum A x) = x.
+#A * [normalize // | #a normalize // ] qed.
+
+(* The other direction is just slightly more complex, since we need to exploit
+the fact that the unit type contains a single element: we could use lemma
+eq_unit or proceed by cases on the unit element. *)
+
+lemma option_bij2: ∀A,x. option_to_sum A (sum_to_option A x) = x.
+#A * #x [normalize cases x // | //] qed.
+
+(* We shall see more examples of functions involving the otion type in the
+next section. *)
+
+(********************************** Lists *************************************)
+
+(* The option type, as well as the cartesian product or the sum are simple
+examples of polymorphic types, that is types that depend in a uniform and
+effective way on other types. This form of polymorphism (sometimes called
+"parametric" polymporphism to distinguish it from the "ad hoc" polymorphism
+typical of object oriented languages) is a major feature of modern functional
+programming languages: in many intersting cases, it allows to write generic
+functions operating on inputs without depending on their type. Typical examples
+can be found on lists.
+For instance, appending two lists is an operation that is essentially
+independent from the type A of the elements in the list, and we would like to
+write a single append function working parametrically on A.
+
+The first step is to define a type for lists polimorphic over the type A of its
+elements: *)
+
+inductive list (A:Type[0]) : Type[0] :=
+ | nil: list A
+ | cons: A -> list A -> list A.
+
+(* The definition should be clear: a list is either empty (nil) or it is
+obtained by concatenating (cons) an element of type A to a given list. In other
+words, the type of lists is the smallest inductive type generated by the two
+constructors nil and cons.
+
+The first element of a list is called its "head". If the list is empty the head
+is undefined: as discussed in the previous section, we should either return a
+``default'' element, or decide to return an option type.
+We have an additional complication in this case, since the ``default'' element
+should have type A, and we know nothing about A (it could even be an empty
+type!). We have no way to guess a canonical element, and the only possibility
+(along this approach) is to take it in input. These are the two options: *)
+
+definition hd ≝ λA.λl: list A.λd:A.
+ match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+definition option_hd ≝ λA.λl:list A.
+ match l with [ nil ⇒ None ? | cons a _ ⇒ Some ? a ].
+
+(* What remains of a list after removing its head is called the "tail" of the
+list. Again, the tail of an empty list is undefined, but in this case the result
+must be a list, and we have a canonical inhabitant of lists, that is the empty
+list. So, it is natural to extend the definition of tail saying that the tail of
+nil is nil (that is very similar to say that the predecessor of 0 is 0): *)
+
+definition tail ≝ λA.λl: list A.
+ match l with [ nil ⇒ nil ? | cons hd tl ⇒ tl].
+
+(* Using destruct, it is easy to prove that cons is injective in both
+arguments. *)
+
+lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.
+ cons ?a1 l1 = cons ? a2 l2 → a1 = a2.
+#A #a1 #a2 #l1 #l2 #Heq destruct // qed.
+
+lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.
+ cons ? a1 l1 = cons ? a2 l2 → l1 = l2.
+#A #a1 #a2 #l1 #l2 #Heq destruct // qed.
+
+(* The append function is defined by recursion over the first list: *)
+let rec append A (l1: list A) l2 on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons hd tl ⇒ cons ? hd (append A tl l2) ].
-lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
-#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
-qed.
+(******************************* list notation ********************************)
-lemma memb_cons: ∀S,a,b,l.
- memb S a l = true → memb S a (b::l) = true.
-#S #a #b #l normalize cases (a==b) normalize //
-qed.
+(* Before discussing more operations over lists, it is convenient to introduce a
+bit of notation; in particular, we shall write a::l for (cons ? a l);
+[a1;a2,…, an] for the list composed by the elements a1, a2,…, an and l1@l2 for
+the concatenation of l1 and l2.
-lemma memb_single: ∀S,a,x. memb S a (x::[]) = true → a = x.
-#S #a #x normalize cases (true_or_false … (a==x)) #H
- [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
-qed.
+This can be obtained by the following declarations: *)
-lemma memb_append: ∀S,a,l1,l2.
-memb S a (l1@l2) = true → memb S a l1= true ∨ memb S a l2 = true.
-#S #a #l1 elim l1 normalize [#l2 #H %2 //]
-#b #tl #Hind #l2 cases (a==b) normalize /2/
-qed.
+notation "hvbox(hd break :: tl)"
+ right associative with precedence 47 for @{'cons $hd $tl}.
-lemma memb_append_l1: ∀S,a,l1,l2.
- memb S a l1= true → memb S a (l1@l2) = true.
-#S #a #l1 elim l1 normalize
- [normalize #le #abs @False_ind /2/
- |#b #tl #Hind #l2 cases (a==b) normalize /2/
- ]
-qed.
+notation "[ list0 term 19 x sep ; ]"
+ non associative with precedence 90
+ for ${fold right @'nil rec acc @{'cons $x $acc}}.
-lemma memb_append_l2: ∀S,a,l1,l2.
- memb S a l2= true → memb S a (l1@l2) = true.
-#S #a #l1 elim l1 normalize //
-#b #tl #Hind #l2 cases (a==b) normalize /2/
-qed.
+notation "hvbox(l1 break @ l2)"
+ right associative with precedence 47 for @{'append $l1 $l2}.
-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) >(\P eqba) //
- |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
- @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
- ]
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+(* Note that [ ] is an alternative notation for the empty list, and [a] is a
+list containing a singleton element a.
+Let us check the notation: *)
+
+example append_ex1: [true;false]@[true] = [true;false;true].
+normalize // qed.
+
+(* As a simple exerices, now that we have a comfortable notation, let to prove
+that append is associative, and that nil is a neutral element for it. *)
+
+lemma associative_append: ∀A.∀l1,l2,l3:list A. l1 @ (l2 @ l3) = (l1 @ l2) @ l3.
+#A #l1 elim l1 [normalize //]
+#a #tl #Hind #l2 #l3 normalize @eq_f @Hind qed.
+
+lemma append_nil: ∀A.∀l:list A. l@[ ] = l.
+#A #l elim l // #a #tl #Hind normalize >Hind // qed.
+
+let rec length (A:Type[0]) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ O
+ | cons a tl ⇒ 1+(length A tl)
+ ].
+
+interpretation "list length" 'card l = (length ? l).
+
+lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
+#A #l elim l //
qed.
-lemma not_memb_to_not_eq: ∀S,a,b,l.
- memb S a l = false → memb S b l = true → a==b = false.
-#S #a #b #l cases (true_or_false (a==b)) //
-#eqab >(\P eqab) #H >H #abs @False_ind /2/
-qed.
-
-lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true →
- memb S2 (f a) (map … f l) = true.
-#S1 #S2 #f #a #l elim l normalize [//]
-#x #tl #memba cases (true_or_false (a==x))
- [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
- |#eqx >eqx cases (f a==f x) normalize /2/
- ]
+lemma length_append: ∀A.∀l1,l2:list A.
+ |l1@l2| = |l1|+|l2|.
+#A #l1 elim l1 // normalize /2/
qed.
-lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
- memb S1 a1 l1 = true → memb S2 a2 l2 = true →
- memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
-#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
-#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
- [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map //
- |#membtl @memb_append_l2 @Hind //
- ]
+let rec nth (A:Type[0]) (l:list A) n on n ≝
+ match n with
+ [ O ⇒ option_hd ? l
+ | S x ⇒ nth A (tail ? l) x
+ ].
+
+lemma nth_length : ∀A,l,n. n < length A l → nth A l n ≠ None ?.
+#A #l elim l
+ [#n normalize #H @False_ind /2 by absurd/
+ |#a #tl #Hind #n normalize
+ #H lapply (le_S_S_to_le … H) -H cases n
+ [#_ normalize % #H1 destruct (H1)
+ |#m #H normalize @Hind @H
+ ]
+ ]
qed.
-(*
-Unicity
-If we are interested in representing finite sets as lists, is is convenient
-to avoid duplications of elements. The following uniqueb check this property.
-*)
+(*************************** More list operations *****************************)
-let rec uniqueb (S:DeqSet) l on l : bool ≝
- match l with
- [ nil ⇒ true
- | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
+(* We conclude this section discussing another important operation over lists,
+namely the reverse funtion, retrurning a list with the same elements of the
+original list but in reverse order.
+
+One could define the revert operation as follows: *)
+
+let rec rev A (l1: list A) on l1 ≝
+ match l1 with
+ [ nil ⇒ nil ?
+ | cons a tl ⇒ rev A tl @ [a]
].
-(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
+(* However, this implementation is sligtly inefficient, since it has a quadratic
+complexity. A better solution consists in exploiting an accumulator, passing
+through the following auxilary function: *)
-let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
- match l1 with
+let rec rev_append A (l1,l2:list A) on l1 ≝
+ match l1 with
[ nil ⇒ l2
- | cons a tl ⇒
- let r ≝ unique_append S tl l2 in
- if memb S a r then r else a::r
+ | cons a tl ⇒ rev_append A tl (a::l2)
].
-lemma memb_unique_append: ∀S,a,l1,l2.
- memb S a (unique_append S l1 l2) = true → memb S a l1= true ∨ memb S a l2 = true.
-#S #a #l1 elim l1 normalize [#l2 #H %2 //]
-#b #tl #Hind #l2 cases (true_or_false … (a==b)) #Hab >Hab normalize /2/
-cases (memb S b (unique_append S tl l2)) normalize
- [@Hind | >Hab normalize @Hind]
-qed.
+definition reverse ≝λS.λl.rev_append S l [].
+
+lemma reverse_single : ∀S,a. reverse S [a] = [a].
+// qed.
+
+example example_rev1: reverse ? [true;false] = [false;true].
+normalize // qed.
+
+(* Let us prove the following results, as a simple exercise.
+
+lemma reverse_cons : ∀A,a,l. reverse A (a::l) = (reverse A l)@[a].
+
+If you try a brute force approach (e.g., induction on l); you will get in
+trouble. The point is that reverse is defined as a particular case of
+rev_append, and you should suitably generalize your result taking rev_append in
+mind.
+*)
+
+lemma rev_append_append: ∀A,l1,l2,l3.
+ rev_append A l1 (l2@l3) = rev_append A l1 l2 @l3.
+#A #l1 elim l1 //
+#hd #tl normalize #Hind #l2 #l3 @(Hind (hd::l2)) qed.
+
+(* Now we get reverse_cons as a trivial corollary, since
+ reverse A (a::l) = rev_append A (a::l) [ ] = rev_append l [a] =
+ rev_append l ([ ]@[a]) = (rev_append l [ ])@[a] = reverse A l @ [a]
+*)
+
+lemma reverse_cons : ∀A,a,l. reverse A (a::l) = reverse A l@[a].
+#A #a #l normalize <rev_append_append % qed.
+
+(* More generally, we can prove the following property of rev_append
+specyfing its general behaviour *)
-lemma unique_append_elim: ∀S:DeqSet.∀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.
-#S #P #l1 #l2 #Hl1 #Hl2 #x #membx cases (memb_unique_append … membx) /2/
+lemma rev_append_def : ∀S,l1,l2.
+ rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 #l2 normalize <rev_append_append //
qed.
-lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true →
- uniqueb S (unique_append S l1 l2) = true.
-#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
-cases (true_or_false … (memb S a (unique_append S tl l2)))
-#H >H normalize [@Hind //] >H normalize @Hind //
+lemma reverse_append: ∀S,l1,l2.
+ reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons >Hind >associative_append //
qed.
-(*
-Sublists
+lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
+>reverse_single >Hind // qed.
-*)
-definition sublist ≝
- λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
-
-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_r … 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)
- [#eqxa @False_ind lapply (andb_true_l … unique)
- <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 //
- ]
- ]
+
+(***************************** List iterators *********************************)
+
+(* In general, an iterator for some data type is an object that enables to
+traverse its structure performing a given computation.
+There is a canonical set of iterators over lists deriving from the programming
+experience. In this section we shall review a few of them, proving some of their
+properties.
+
+A first, famous iterator is the map function, that applies a function f to each
+element of a list [a1,…, an], building the list [f a1; … ; f an]. *)
+
+let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
+ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+
+(* The map function distributes over append, as can be simply proved by
+induction over the first list: *)
+
+lemma map_append : ∀A,B,f,l1,l2.
+ (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
+#A #B #f #l1 elim l1
+ [ #l2 @refl | #h #t #IH #l2 normalize >IH // ] qed.
+
+lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
+#A #B #l #f elim l // #a #tl #Hind normalize //
qed.
-lemma sublist_unique_append_l1:
- ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
-#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/]
-#x #tl #Hind #l2 #a
-normalize cases (true_or_false … (a==x)) #eqax >eqax
-[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2)))
- [#H >H normalize // | #H >H normalize >(\b (refl … a)) //]
-|cases (memb S x (unique_append S tl l2)) normalize
- [/2/ |>eqax normalize /2/]
-]
+(* The most important iterator is traditionally called "fold"; we shall only
+consider the so called fold-right variant, that takes in input a function
+f:A→B→B, a list [a1; …; an] of elements of type A, a base element b:B and
+returns the value f a1 (f a2 (… (f an b) …)). *)
+
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
+ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+
+(* Many other interesting functions can be defined in terms of foldr. A first
+interesting example is the filter function, taking in input a boolean test p and
+a list l and returning the sublist of all elements of l satisfying the test. *)
+
+definition filter ≝
+ λT.λp:T → bool.
+ foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
+
+(* As another example, we can generalize the map function to an operation taking
+in input a binary function f:A → B → C, two lists [a1;… ;an] and [b1;… ;bm] and
+returning the list [f a1 b1; ˙… ;f an b1;… ;f a1 b_m; … f an bm]. *)
+
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+ foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
+
+(* The folded function
+ λi,acc.(map ?? (f i) l2)@acc
+takes in input an element i and an accumulator, and add to the accumulator the
+values obtained by mapping the partial instantiation (f i) on the elements of
+l2. This function is iterated over all elements of the first list l1, starting
+with an empty accumulator. *)
+
+(************************************ Vectors *********************************)
+
+(* A vector of length n of elements of type A is simply defined in Matita as a
+record composed by a list of elements of type A, plus a proof that the list has
+the expected length. Vectors are a paradigmatic example of dependent type, that
+is of a type whose definition depends on a term. *)
+
+record Vector (A:Type[0]) (n:nat): Type[0] ≝
+{ vec :> list A;
+ len: length ? vec = n }.
+
+(* Given a list l we may trivially turn it into a vector of length |l|; we just
+need to prove that |l|=|l| that follows from the reflexivity of equality. *)
+
+lemma Vector_of_list ≝ λA,l.mk_Vector A (|l|) l (refl ??).
+
+(* Then we can prove that any vector of zero lenght has no elements: *)
+
+lemma vector_nil: ∀A.∀v:Vector A 0.
+ v = Vector_of_list A [ ].
+#A * * // #a #tl normalize #H destruct
+qed.
+
+(* It is convenient to re-define on vectors the hd, tail and cons operations
+on lists *)
+
+definition vec_tail ≝ λA.λn.λv:Vector A n.
+ mk_Vector A (pred n) (tail A v) ?.
+>length_tail >(len A n v) //
qed.
-lemma sublist_unique_append_l2:
- ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
-#S #l1 elim l1 [normalize //] #x #tl #Hind normalize
-#l2 #a cases (memb S x (unique_append S tl l2)) normalize
-[@Hind | cases (a==x) normalize // @Hind]
+definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
+ mk_Vector A (S n) (cons A a v) ?.
+normalize >(len A n v) //
qed.
-lemma decidable_sublist:∀S,l1,l2.
- (sublist S l1 l2) ∨ ¬(sublist S l1 l2).
-#S #l1 #l2 elim l1
- [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/
- |#a #tl * #subtl
- [cases (true_or_false (memb S a l2)) #memba
- [%1 whd #x #membx cases (orb_true_l … membx)
- [#eqax >(\P eqax) // |@subtl]
- |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd
- ]
- |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_cons //
- ]
- ]
+definition vec_hd ≝ λA.λn.λv:Vector A (S n). hd A v ?.
+elim v * [normalize #H destruct | #a #H #eq @a]
qed.
-(*
-Filtering
-*)
+(* Any vector of lenght (S n) can be expanded as a concatenation of a head and a
+tail vector of length n *)
-lemma memb_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 cases (true_or_false (f b)) #H
-normalize >H normalize [2:@Hind]
-cases (true_or_false (a==b)) #eqab
- [#_ >(\P eqab) // | >eqab normalize @Hind]
-qed.
-
-lemma memb_filter_memb: ∀S,f,a,l.
- memb S a (filter S f l) = true → memb S a l = true.
-#S #f #a #l elim l [normalize //]
-#b #tl #Hind normalize (cases (f b)) normalize
-cases (a==b) normalize // @Hind
+lemma vec_expand: ∀A,n,v.
+ v = vec_cons A (vec_hd A n v) n (vec_tail A (S n) v).
+#A #n * #l cases l [normalize in ⊢ (%→?); #H destruct |//]
qed.
-
-lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true →
-memb S x l = true ∧ (f x = true).
-/3/ qed.
-
-lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true →
-memb S x (filter ? f l) = true.
-#S #f #x #l #fx elim l normalize //
-#b #tl #Hind cases (true_or_false (x==b)) #eqxb
- [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize //
- |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind]
- ]
-qed.
-(*
-Exists
+(* Most functions operating on lists can be naturally extended to vectors:
+interesting cases are vec_append, concatenating vectors, and vec_map, mapping a
+function f on all elements of the input vector and returning a vector of the
+same dimension of the input one. *)
-*)
+definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
+mk_Vector A (n1+n2) (v1@v2) ?.
+>length_append >(len … v1) >(len … v2) // qed.
+
+definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
+mk_Vector B n (map ?? f v)
+ (trans_eq … (length_map …) (len A n v)).
+
+(* Since a vector is automatically coerced, if needed, to the list of its
+elements, we may simply use typical functions over lists (such as nth) to
+extract/filter specific components.
+
+The following function (change_vec A n v a i) replaces the content of the vector
+v at position i with the value a. *)
+
+let rec change_vec (A:Type[0]) (n:nat) on n ≝
+match n return λn0.∀v:Vector A n0.A→nat→Vector A n0 with
+[ O ⇒ λv,a,i.v
+| S m ⇒ λv,a,i.
+ match i with
+ [ O ⇒ vec_cons A a m (vec_tail … v)
+ | S j ⇒ vec_cons A (vec_hd A m v) m (change_vec A m (vec_tail … v) a j)
+ ]
+].
+
+(* A frequent operation between vectors is their comparison. The following
+lemma allow us to reduce the comparisons of vectors of a same lenght to the
+comparison of their components. *)
+
+lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.
+ (∀i. i < n → nth A v1 i = nth A v2 i) → v1 = v2.
+#A #n elim n -n
+ [#v1 #v2 #_ >(vector_nil A v1) >(vector_nil A v2) //
+ |#n #Hind #v1 #v2 #H >(vec_expand … v1) >(vec_expand … v2)
+ >(Hind (vec_tail … v1) (vec_tail … v2))
+ [cut (vec_hd A n v1 = vec_hd A n v2) // lapply (H 0 (lt_O_S ?)) -H
+ >(vec_expand … v1) in ⊢ (%→?); >(vec_expand … v2) in ⊢ (%→?);
+ change with (Some ?? = Some ?? → ?) #H destruct (H) @e0
+ |#i #ltin @(H (S i)) @le_S_S //
+ ]
+ ]
+qed.
-let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
-match l with
-[ nil ⇒ false
-| cons h t ⇒ orb (p h) (exists A p t)
-].
\ No newline at end of file
projects / helm.git / blobdiff