-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) ].