Library Aux
Require Import List Min Arith Div2.
Notation "n .+1" := (S n)(at level 2, left associativity, format "n .+1"): nat_scope.
Notation "n .+1" := (S n)(at level 2, left associativity, format "n .+1"): nat_scope.
Minus
The exponential function
Some iterators on list
Section Fold2.
Variable A B C: Type.
Variable f: A -> B -> C -> C.
Definition dhead a (l : list A) :=
match l with nil => a | b :: _ => b end.
Variable g: A -> B -> C.
Lemma map2_length l1 l2:
length (map2 l1 l2) = min (length l1) (length l2).
End Fold2.
Implicit Arguments dhead[A].
Implicit Arguments fold2[A B C].
Implicit Arguments map2[A B C].
Implicit Arguments dmap2[A B C].
Section Perm.
Variable A: Type.
Inductive perm: list A -> list A -> Prop :=
perm_id: forall l, perm l l
| perm_swap: forall a b l, perm (a::b::l) (b::a::l)
| perm_skip: forall a l1 l2, perm l1 l2 -> perm (a::l1) (a::l2)
| perm_trans: forall l1 l2 l3, perm l1 l2 -> perm l2 l3 -> perm l1 l3.
Lemma perm_sym l1 l2: perm l1 l2 -> perm l2 l1.
Lemma perm_cons_app a l1 l2: perm ((a:: l1) ++ l2) (l1 ++ (a:: l2)).
Lemma perm_length l1 l2: perm l1 l2 -> length l1 = length l2.
Lemma perm_in a l1 l2: perm l1 l2 -> In a l1 -> In a l2.
Lemma perm_in_inv a l1: In a l1 -> exists l2, perm l1 (a:: l2).
Lemma perm_incl_r l1 l2 l3: perm l1 l2 -> incl l1 l3 -> incl l2 l3.
Lemma perm_incl_l l1 l2 l3: perm l1 l2 -> incl l3 l1 -> incl l3 l2.
End Perm.
Implicit Arguments perm[A].
Section Uniq.
Variable A: Type.
Inductive uniq: list A -> Prop :=
uniq_nil: uniq nil
| uniq_cons: forall a l, ~ In a l -> uniq l -> uniq (a::l).
Lemma uniq_perm l1 l2: perm l1 l2 -> uniq l1 -> uniq l2.
Lemma uniq_cons_inv a l: uniq (a::l) -> uniq l.
Lemma uniq_app_inv_l l1 l2: uniq (l1 ++ l2) -> uniq l1.
Lemma uniq_app_inv_r l1 l2: uniq (l1 ++ l2) -> uniq l2.
Lemma perm_incl_inv l1 l2:
uniq l1 -> uniq l2 -> incl l1 l2 -> exists l3, perm l2 (l1 ++ l3).
End Uniq.
Lemma list_split (A: Type) n1 n2 (l: list A):
length l = n1 + n2 ->
exists l1, exists l2, l = l1 ++ l2 /\ length l1 = n1 /\ length l2 = n2.
Lemma length_split (A B: Type) (a b: A) (lk: list B) l1 l2:
length lk = length ((a:: l1) ++ b :: l2)%list ->
exists k1, exists k2, exists lk1, exists lk2,
lk = ((k1::lk1) ++ k2::lk2)%list /\ length lk1 = length l1 /\ length lk2 = length l2.
Lemma list_app_inj (A: Type) (l1 l2 l3 l4: list A):
length l1 = length l3 -> l1 ++ l2 = l3 ++ l4 -> l1 = l3 /\ l2 = l4.
Lemma list_case (A:Type) (l: list A): l = nil \/ l <> nil.
Lemma list_dec (A: Type) (P: A -> Prop) l:
(forall x, P x \/ ~ P x) -> (forall x, In x l -> P x) \/ (exists x, In x l /\ ~ P x).
Implicit Arguments uniq[A].
Georges' trick for easy case analysis
Inductive eq_Spec (A: Type) (x y: A): bool -> Prop :=
|eq_Spect: x = y -> eq_Spec A x y true
|eq_Specf: x <> y -> eq_Spec A x y false.
Implicit Arguments eq_Spec[A].
Binomial Coefficient defined using Pascal's triangle
Fixpoint bin (a b : nat) {struct a} : nat :=
match a, b with
_, O => 1
| O, S b' => 0
| S a', S b' => bin a' (S b') + bin a' b'
end.
match a, b with
_, O => 1
| O, S b' => 0
| S a', S b' => bin a' (S b') + bin a' b'
end.
Basic properties of binomial coefficients
Lemma bin_0: forall (n : nat), bin n 0 = 1.
Lemma bin_1: forall (n : nat), bin n 1 = n.
Lemma bin_more: forall (n m : nat), n < m -> bin n m = 0.
Lemma bin_nn: forall (n : nat), bin n n = 1.
Lemma bin_def:
forall (n k : nat), bin (S n) (S k) = bin n (S k) + bin n k.
Fixpoint iter {A: Type} (f: A -> A) (n: nat) (x: A) :=
match n with
| O => x
| S n1 => f (iter f n1 x)
end.
Lemma bin_1: forall (n : nat), bin n 1 = n.
Lemma bin_more: forall (n m : nat), n < m -> bin n m = 0.
Lemma bin_nn: forall (n : nat), bin n n = 1.
Lemma bin_def:
forall (n k : nat), bin (S n) (S k) = bin n (S k) + bin n k.
Fixpoint iter {A: Type} (f: A -> A) (n: nat) (x: A) :=
match n with
| O => x
| S n1 => f (iter f n1 x)
end.
A bit of ssreflect
Coercion b2Prop (x : bool) := x = true.
Lemma b2PropT: b2Prop true.
Hint Resolve b2PropT.
Require Import Bool.
Lemma andbP b1 b2: b1 && b2 <-> b1 /\ b2.
Some facts about div2
Lemma div2_double_p n m : div2 (2 * n + m) = n + div2 m.
Lemma div2_prop n: n + div2 (n * (n - 1)) = div2 (n.+1 * n).
Lemma minus_minus_le m n: n <= m -> m - (m - n) = n.
Lemma minus0_le m n: m <= n -> m - n = 0.
Fixpoint eq_nat (m n: nat) :=
match m, n with (S m), (S n) => eq_nat m n | 0, 0 => true | _, _ => false end.
Notation "m ?= n" := (eq_nat m n) (at level 70): nat_scope.
Inductive eq_nat_spec: nat -> nat -> bool -> Type :=
eq_nat_spect: forall m, eq_nat_spec m m true
| eq_nat_specb: forall m n, m <> n -> eq_nat_spec m n false.
Lemma eq_natP m n: eq_nat_spec m n (m ?= n).
Notation "x .+2" := (S (S x)) (at level 9): nat_scope.