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