Global Set Implicit Arguments.
Global
Require Export Omega List Morphisms.

Export ListNotations.
Notation "| A |" := (length A) (at level 65).
Notation "x 'el' A" := (In x A) (at level 70).
Notation "A <<= B" := (incl A B) (at level 70).

# Membership

We use the following facts from the standard library List.
• in_eq : x x::A
• in_nil : ¬ x nil
• in_cons : x A x y::A
• in_or_app : x A x B x A++B
• in_app_iff : x A++B x A x B
• in_map_iff : y map f A x, f x = y x A

Hint Resolve in_eq in_nil in_cons in_or_app.

Lemma in_sing X (x y : X) :
x [y]x = y.

Lemma in_cons_neq X (x y : X) A :
x y::Ax yx A.

Definition disjoint (X : Type) (A B : list X) :=
¬ x, x A x B.

Lemma disjoint_forall X (A B : list X) :
disjoint A B x, x A¬ x B.

Lemma disjoint_cons X (x : X) A B :
disjoint (x::A) B ¬ x B disjoint A B.

# Inclusion

We use the following facts from the standard library List.
• A B = y, x A x B
• incl_refl : A A
• incl_tl : A B A x::B
• incl_cons : x B A B x::A B
• incl_appl : A B A B++C
• incl_appr : A C A B++C
• incl_app : A C B C A++B C

Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app.

Lemma incl_nil X (A : list X) :
nil A.

Hint Resolve incl_nil.

Lemma incl_map X Y A B (f : XY) :
A Bmap f A map f B.

Section Inclusion.
Variable X : Type.
Implicit Types A B : list X.

Lemma incl_nil_eq A :
A nilA=nil.

Lemma incl_shift x A B :
A Bx::A x::B.

Lemma incl_lcons x A B :
x::A B x B A B.

Lemma incl_rcons x A B :
A x::B¬ x AA B.

Lemma incl_lrcons x A B :
x::A x::B¬ x AA B.

End Inclusion.

# Equivalence

Definition equi X (A B : list X) : Prop :=
A B B A.

Notation "A === B" := (equi A B) (at level 70).

Hint Unfold equi.

Section Equi.
Variable X : Type.
Implicit Types A B : list X.

Lemma equi_push x A :
x AA x::A.

Lemma equi_dup x A :
x::A x::x::A.

Lemma equi_swap x y A:
x::y::A y::x::A.

Lemma equi_shift x A B :
x::A++B A++x::B.

Lemma equi_rotate x A :
x::A A++[x].
End Equi.

# Automatic Decision Inference

Definition dec (X : Prop) : Type := {X} + {¬ X}.
Definition decision (X : Prop) (D : dec X) : dec X := D.

Definition eq_nat_Dec (x y : nat) : dec (x = y) :=
eq_nat_dec x y.

Definition eq_list_dec (X : Type) :
( x y : X, dec (x=y)) → A B : list X, dec (A = B).
Defined.

Notation "'eq_dec' X" := ( x y : X, dec (x=y)) (at level 70).

Instance in_Dec (X : Type) (x : X) (A : list X) : eq_dec Xdec (x A).
Defined.

Instance le_Dec (x y : nat) : dec (x y) :=
le_dec x y.

Instance True_dec : dec True :=
left I.
Instance False_dec : dec False :=
right (fun AA).
Instance impl_dec (X Y : Prop) : dec Xdec Ydec (XY).
Instance and_dec (X Y : Prop) : dec Xdec Ydec (X Y).
Instance or_dec (X Y : Prop) : dec Xdec Ydec (X Y).

(* Standard modules make "not" and "iff" opaque for type class inference, can be seen with Print HintDb typeclass_instances. *)

Instance not_dec (X : Prop) : dec Xdec (¬ X).

Hint Unfold dec.

Tactic Notation "decide" constr(p) :=
destruct (decision p).
Tactic Notation "decide" constr(p) "as" simple_intropattern(i) :=
destruct (decision p) as i.

Tactic Notation "decide" "claim" :=
match goal with
| |- dec (?p) ⇒ exact (decision p)
end.

Hint Extern 4 ⇒
match goal with
| [ |- dec ((fun __) _) ] ⇒ simpl
end : typeclass_instances.

Lemma dec_DN X :
dec X~~ XX.

Lemma dec_DM_and X Y :
dec Xdec Y¬ (X Y)¬ X ¬ Y.

Lemma dec_DM_impl X Y :
dec Xdec Y¬ (XY)X ¬ Y.

Lemma dec_prop_iff (X Y : Prop) :
(X Y) → dec Xdec Y.

# List Quantification

Lemma sigma_forall_list X A (p : XProp) (p_dec : x, dec (p x)) :
{x | x A ¬ p x} + { x, x Ap x}.

Instance forall_list_dec X A (p : XProp) (p_dec : x, dec (p x)) :
dec ( x, x Ap x).

Instance exists_list_dec X A (p : XProp) (p_dec : x, dec (p x)) :
dec ( x, x A p x).

Lemma dec_DM_forall X A (p : XProp) :
( x, dec (p x)) →
¬ ( x, x Ap x) x, x A ¬ p x.

Lemma dec_cc X (p : XProp) A :
eq_dec X → ( x, dec (p x)) →
( x, x A p x) → {x | x A p x}.

# Filter

Section Filter.
Variable X : Type.
Variable p : XProp.
Variable p_dec : x, dec (p x).
Fixpoint filter (A : list X) : list X :=
match A with
| nilnil
| x::A'if decision (p x) then x :: filter A' else filter A'
end.
End Filter.

Section FilterLemmas.
Variable X : Type.
Variable p : XProp.
Context {p_dec : x, dec (p x)}.

Lemma in_filter x A :
x filter p A x A p x.

Lemma filter_incl A :
filter p A A.

Lemma filter_mono A B :
A Bfilter p A filter p B.

End FilterLemmas.

Section FilterLemmas_pq.
Variable X : Type.
Variable p q : XProp.
Context {p_dec : x, dec (p x)}.
Context {q_dec : x, dec (q x)}.

Lemma filter_pq_incl A :
( x, x Ap xq x) → filter p A filter q A.

Lemma filter_pq_eq A :
( x, x A → (p x q x)) → filter p A = filter q A.

End FilterLemmas_pq.

Lemma separation X A p (D : x : X, dec (p x)) :
{B | x, x B x A p x}.

# Setoid Rewriting

Instance equi_Equivalence X : Equivalence (@equi X).

Instance cons_equi_proper X :
Proper (eq ==> @equi X ==> @equi X) (@cons X).

Instance app_equi_proper X :
Proper (@equi X ==> @equi X ==> @equi X) (@app X).

Instance in_equi_proper X :
Proper (eq ==> @equi X ==> iff) (@In X).

Instance incl_equi_proper X :
Proper (@equi X ==> @equi X ==> iff) (@incl X).

Instance incl_preorder X : PreOrder (@incl X).

# Duplicate-free lists

Inductive dupfree (X : Type) : list XProp :=
| dupfreeN : dupfree nil

Section Dupfree.
Variable X : Type.
Implicit Types A B : list X.

Lemma dupfree_inv x A :
dupfree (x::A) → ¬x A dupfree A.

Lemma dupfree_app A B :
disjoint A Bdupfree Adupfree Bdupfree (A++B).

Lemma dupfree_map Y A (f : XY) :
( x y, x Ay Af x = f yx=y) →

Lemma dupfree_filter p (p_dec : x, dec (p x)) A :

Lemma dupfree_dec A :
eq_dec Xdec (dupfree A).

End Dupfree.

Section Undup.
Variable X : Type.
Context {eq_X_dec : eq_dec X}.
Implicit Types A B : list X.

Fixpoint undup (A : list X) : list X :=
match A with
| nilnil
| x::A'if decision (x A') then undup A' else x :: undup A'
end.

Lemma undup_equi A :
undup A A.

Lemma undup_dupfree A :
dupfree (undup A).

Lemma undup_homo A B :
A B undup A undup B.

Lemma undup_iso A B :
A B undup A undup B.

Lemma undup_eq A :
dupfree Aundup A = A.

Lemma undup_idempotent A :
undup (undup A) = undup A.

End Undup.

Section DupfreeLength.
Variable X : Type.
Implicit Types A B : list X.

Lemma dupfree_reorder A x :
dupfree Ax A
A', A x::A' |A'| < |A| dupfree (x::A').
Lemma dupfree_le A B :

Lemma dupfree_eq A B :

Lemma dupfree_lt A B x :
x B¬ x A|A| < |B|.

Lemma dupfree_ex A B :
eq_dec Xdupfree Adupfree B|A| < |B| x, x B ¬ x A.

Lemma dupfree_equi A B :
eq_dec Xdupfree Adupfree BA B|A|=|B|A B.

End DupfreeLength.

# Cardinality

Section Cardinality.
Variable X : Type.
Context {eq_X_dec : eq_dec X}.
Implicit Types A B : list X.

Definition card (A : list X) : nat := |undup A|.

Lemma card_le A B :
A Bcard A card B.

Lemma card_eq A B :
A Bcard A = card B.

Lemma card_equi A B :
A Bcard A = card BA B.

Lemma card_lt A B x :
A Bx B¬ x Acard A < card B.

Lemma card_or A B :
A BA B card A < card B.

Lemma card_ex A B :
card A < card B x, x B ¬ x A.

End Cardinality.