``` ```

# Useful Properties of Basic Datatypes

``` Require Import Arith. Require Import List. Require Import ListSet. Require Import Omega. Lemma length_of_append:   forall (A: Set) (xs ys: (list A)),     (length (xs ++ ys)) = (length xs) + (length ys) . Lemma map_elim:   forall (A B: Set) (f: A -> B) (xs: (list A)) (y: B),     (In y (map f xs)) ->     exists x: A, (In x xs) /\ y = (f x) . Lemma map_intro:   forall (A B: Set) (f: A -> B) (x: A) (xs: (list A)),     (In x xs) ->     (In (f x) (map f xs)) . Lemma length_of_map:   forall (A B: Set) (f: A -> B) (xs: (list A)),     (length (map f xs)) = (length xs) . Lemma map_of_append:   forall (A B: Set) (f: A -> B) (xs ys: (list A)),     (map f (xs ++ ys)) = (map f xs) ++ (map f ys) . Lemma cons_destruct:     forall (A: Set) (x y: A) (xs ys: (list A)),       (x = y) -> (xs = ys) -> (x :: xs) = (y :: ys) . Lemma plus_minus_assoc:   forall (n m p: nat),     (p <= m) ->     n + m - p = n + (m - p) . Lemma myarith_1:   forall (n m: nat),     (m <= n) ->     (n - m + m) = n . Lemma myarith_2:   forall (n m p: nat),     ((m + p) <= n) ->     (n - m - p) = (n - (m + p)) . Lemma empty_is_empty_1:   forall (A: Set) (eqdec: forall (x y: A), { x = y } + { x <> y }),     forall (x: A),       ~(set_In x (empty_set A)) . Lemma empty_is_empty_2:   forall (A: Set) (eqdec: forall (x y: A), { x = y } + { x <> y }),     forall (s: (set A)),       (forall (x: A), ~(set_In x s)) ->       (s = (empty_set A)) . Lemma empty_union_left:   forall (A: Set) (eqdec: forall (x y: A), { x = y } + { x <> y }),     forall (s1 s2: (set A)),     (set_union eqdec s1 s2) = (empty_set A) ->     s1 = (empty_set A) . Lemma empty_union_right:   forall (A: Set) (eqdec: forall (x y: A), { x = y } + { x <> y }),     forall (s1 s2: (set A)),     (set_union eqdec s1 s2) = (empty_set A) ->     s2 = (empty_set A) . ```
Index
This page has been generated by coqdoc