# Base Library for ICL

• Version: 30 June 2014
• Author: Gert Smolka, Saarland University
• Acknowlegments: Sigurd Schneider, Dominik Kirst

Global Set Implicit Arguments.
Global

Require Export Omega List Morphisms.

Ltac inv H := inversion H; subst; clear H.

# De Morgan laws

Lemma DM_or (X Y : Prop) :
~ (X \/ Y) <-> ~ X /\ ~ Y.

Lemma DM_exists X (p : X -> Prop) :
~ (exists x, p x) <-> forall x, ~ p x.

# Size recursion

Lemma size_recursion (X : Type) (sigma : X -> nat) (p : X -> Type) :
(forall x, (forall y, sigma y < sigma x -> p y) -> p x) ->
forall x, p x.

# Iteration

Section Iteration.
Variable X : Type.
Variable f : X -> X.

Fixpoint it (n : nat) (x : X) : X :=
match n with
| 0 => x
| S n' => f (it n' x)
end.

Lemma it_ind (p : X -> Prop) x n :
p x -> (forall z, p z -> p (f z)) -> p (it n x).

Definition FP (x : X) : Prop := f x = x.

Lemma it_fp (sigma : X -> nat) x :
(forall n, FP (it n x) \/ sigma (it n x) > sigma (it (S n) x)) ->
FP (it (sigma x) x).
End Iteration.

# Decidability

Definition dec (X : Prop) : Type := {X} + {~ X}.

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

Definition decision (X : Prop) (D : dec X) : dec X := D.

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

Hint Extern 4 =>
match goal with
| [ |- dec ?p ] => exact (decision p)
end.

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

Instance True_dec : dec True :=
left I.

Instance False_dec : dec False :=
right (fun A => A).

Instance impl_dec (X Y : Prop) :
dec X -> dec Y -> dec (X -> Y).

Instance and_dec (X Y : Prop) :
dec X -> dec Y -> dec (X /\ Y).

Instance or_dec (X Y : Prop) :
dec X -> dec Y -> dec (X \/ Y).

Instance not_dec (X : Prop) :
dec X -> dec (~ X).

Instance iff_dec (X Y : Prop) :
dec X -> dec Y -> dec (X <-> Y).

Lemma dec_DN X :
dec X -> ~~ X -> X.

Lemma dec_DM_and X Y :
dec X -> dec Y -> ~ (X /\ Y) -> ~ X \/ ~ Y.

Lemma dec_DM_impl X Y :
dec X -> dec Y -> ~ (X -> Y) -> X /\ ~ Y.

Lemma dec_prop_iff (X Y : Prop) :
(X <-> Y) -> dec X -> dec Y.

Instance bool_eq_dec :
eq_dec bool.

Instance nat_eq_dec :
eq_dec nat.

Instance nat_le_dec (x y : nat) : dec (x <= y) :=
le_dec x y.

# Lists

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

Hint Unfold equi.

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).
Notation "A === B" := (equi A B) (at level 70).

Register additional simplification rules with autorewrite / simpl_list

Hint Rewrite <- app_assoc : list.
Hint Rewrite rev_app_distr map_app prod_length : list.

Lemma list_cycle (X : Type) (A : list X) x :
x::A <> A.

# Decidability laws for lists

Instance list_eq_dec X :
eq_dec X -> eq_dec (list X).

Instance list_in_dec (X : Type) (x : X) (A : list X) :
eq_dec X -> dec (x A).

Lemma list_sigma_forall X A (p : X -> Prop) (p_dec : forall x, dec (p x)) :
{x | x A /\ p x} + {forall x, x A -> ~ p x}.

Instance list_forall_dec X A (p : X -> Prop) :
(forall x, dec (p x)) -> dec (forall x, x A -> p x).

Instance list_exists_dec X A (p : X -> Prop) :
(forall x, dec (p x)) -> dec (exists x, x A /\ p x).

Lemma list_exists_DM X A (p : X -> Prop) :
(forall x, dec (p x)) ->
~ (forall x, x A -> ~ p x) -> exists x, x A /\ p x.

Lemma list_exists_not_incl X (A B : list X) :
eq_dec X ->
~ A B -> exists x, x A /\ ~ x B.

Lemma list_cc X (p : X -> Prop) A :
(forall x, dec (p x)) ->
(exists x, x A /\ p x) -> {x | x A /\ p x}.

# Membership

We use the following lemmas from Coq's 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 <-> exists x, f x = y /\ x A

Hint Resolve in_eq in_nil in_cons in_or_app.

Section Membership.
Variable X : Type.
Implicit Types x y : X.
Implicit Types A B : list X.

Lemma in_sing x y :
x [y] -> x = y.

Lemma in_cons_neq x y A :
x y::A -> x <> y -> x A.

Lemma not_in_cons x y A :
~ x y :: A -> x <> y /\ ~ x A.

# Disjointness

Definition disjoint A B :=
~ exists x, x A /\ x B.

Lemma disjoint_forall A B :
disjoint A B <-> forall x, x A -> ~ x B.

Lemma disjoint_symm A B :
disjoint A B -> disjoint B A.

Lemma disjoint_incl A B B' :
B' B -> disjoint A B -> disjoint A B'.

Lemma disjoint_nil B :
disjoint nil B.

Lemma disjoint_nil' A :
disjoint A nil.

Lemma disjoint_cons x A B :
disjoint (x::A) B <-> ~ x B /\ disjoint A B.

Lemma disjoint_app A B C :
disjoint (A ++ B) C <-> disjoint A C /\ disjoint B C.

End Membership.

Hint Resolve disjoint_nil disjoint_nil'.

# Inclusion

We use the following lemmas from Coq's standard library List.
• 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 : X -> Y) :
A B -> map f A map f B.

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

Lemma incl_nil_eq A :
A nil -> A=nil.

Lemma incl_shift x A B :
A B -> x::A x::B.

Lemma incl_lcons x A B :
x::A B <-> x B /\ A B.

Lemma incl_sing x A y :
x::A [y] -> x = y /\ A [y].

Lemma incl_rcons x A B :
A x::B -> ~ x A -> A B.

Lemma incl_lrcons x A B :
x::A x::B -> ~ x A -> A B.

Lemma incl_app_left A B C :
A ++ B C -> A C /\ B C.

End Inclusion.

Definition inclp (X : Type) (A : list X) (p : X -> Prop) : Prop :=
forall x, x A -> p x.

# Setoid rewriting with list inclusion and list equivalence

Instance incl_preorder X :
PreOrder (@incl X).

Instance equi_Equivalence X :
Equivalence (@equi X).

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

Instance cons_incl_proper X x :
Proper (@incl X ==> @incl X) (@cons X x).

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

Instance in_incl_proper X x :
Proper (@incl X ==> Basics.impl) (@In X x).

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

Instance app_incl_proper X :
Proper (@incl X ==> @incl X ==> @incl X) (@app X).

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

# Equivalence

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

Lemma equi_push x A :
x A -> A 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.

# Filter

Definition filter (X : Type) (p : X -> Prop) (p_dec : forall x, dec (p x)) : list X -> list X :=
fix f A := match A with
| nil => nil
| x::A' => if decision (p x) then x :: f A' else f A'
end.

Section FilterLemmas.
Variable X : Type.
Variable p : X -> Prop.
Context {p_dec : forall x, dec (p x)}.

Lemma in_filter_iff x A :
x filter p A <-> x A /\ p x.

Lemma filter_incl A :
filter p A A.

Lemma filter_mono A B :
A B -> filter p A filter p B.

Lemma filter_id A :
(forall x, x A -> p x) -> filter p A = A.

Lemma filter_app A B :
filter p (A ++ B) = filter p A ++ filter p B.

Lemma filter_fst x A :
p x -> filter p (x::A) = x::filter p A.

Lemma filter_fst' x A :
~ p x -> filter p (x::A) = filter p A.

End FilterLemmas.

Section FilterLemmas_pq.
Variable X : Type.
Variable p q : X -> Prop.
Context {p_dec : forall x, dec (p x)}.
Context {q_dec : forall x, dec (q x)}.

Lemma filter_pq_mono A :
(forall x, x A -> p x -> q x) -> filter p A filter q A.

Lemma filter_pq_eq A :
(forall x, x A -> (p x <-> q x)) -> filter p A = filter q A.

Lemma filter_and A :
filter p (filter q A) = filter (fun x => p x /\ q x) A.

End FilterLemmas_pq.

Section FilterComm.
Variable X : Type.
Variable p q : X -> Prop.
Context {p_dec : forall x, dec (p x)}.
Context {q_dec : forall x, dec (q x)}.

Lemma filter_comm A :
filter p (filter q A) = filter q (filter p A).
End FilterComm.

# Element removal

Section Removal.
Variable X : Type.
Context {eq_X_dec : eq_dec X}.

Definition rem (A : list X) (x : X) : list X :=
filter (fun z => z <> x) A.

Lemma in_rem_iff x A y :
x rem A y <-> x A /\ x <> y.

Lemma rem_not_in x y A :
x = y \/ ~ x A -> ~ x rem A y.

Lemma rem_incl A x :
rem A x A.

Lemma rem_mono A B x :
A B -> rem A x rem B x.

Lemma rem_cons A B x :
A B -> rem (x::A) x B.

Lemma rem_cons' A B x y :
x B -> rem A y B -> rem (x::A) y B.

Lemma rem_in x y A :
x rem A y -> x A.

Lemma rem_neq x y A :
x <> y -> x A -> x rem A y.

Lemma rem_app x A B :
x A -> B A ++ rem B x.

Lemma rem_app' x A B C :
rem A x C -> rem B x C -> rem (A ++ B) x C.

Lemma rem_equi x A :
x::A x::rem A x.

Lemma rem_comm A x y :
rem (rem A x) y = rem (rem A y) x.

Lemma rem_fst x A :
rem (x::A) x = rem A x.

Lemma rem_fst' x y A :
x <> y -> rem (x::A) y = x::rem A y.

Lemma rem_id x A :
~ x A -> rem A x = A.

Lemma rem_reorder x A :
x A -> A x :: rem A x.

Lemma rem_inclr A B x :
A B -> ~ x A -> A rem B x.

End Removal.

Hint Resolve rem_not_in rem_incl rem_mono rem_cons rem_cons' rem_app rem_app' rem_in rem_neq rem_inclr.

# Cardinality

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

Fixpoint card A :=
match A with
| nil => 0
| x::A => if decision (x A) then card A else 1 + card A
end.

Lemma card_in_rem x A :
x A -> card A = 1 + card (rem A x).

Lemma card_not_in_rem A x :
~ x A -> card A = card (rem A x).

Lemma card_le A B :
A B -> card A <= card B.

Lemma card_eq A B :
A B -> card A = card B.

Lemma card_cons_rem x A :
card (x::A) = 1 + card (rem A x).

Lemma card_0 A :
card A = 0 -> A = nil.

Lemma card_ex A B :
card A < card B -> exists x, x B /\ ~ x A.

Lemma card_equi A B :
A B -> card A = card B -> A B.

Lemma card_lt A B x :
A B -> x B -> ~ x A -> card A < card B.

Lemma card_or A B :
A B -> A B \/ card A < card B.

End Cardinality.

Instance card_equi_proper X (D: eq_dec X) :
Proper (@equi X ==> eq) (@card X D).

# Duplicate-free lists

Inductive dupfree (X : Type) : list X -> Prop :=
| dupfreeN : dupfree nil
| dupfreeC x A : ~ x A -> dupfree A -> dupfree (x::A).

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

Lemma dupfree_cons x A :
dupfree (x::A) <-> ~ x A /\ dupfree A.

Lemma dupfree_app A B :
disjoint A B -> dupfree A -> dupfree B -> dupfree (A++B).

Lemma dupfree_map Y A (f : X -> Y) :
(forall x y, x A -> y A -> f x = f y -> x=y) ->
dupfree A -> dupfree (map f A).

Lemma dupfree_filter p (p_dec : forall x, dec (p x)) A :
dupfree A -> dupfree (filter p A).

Lemma dupfree_dec A :
eq_dec X -> dec (dupfree A).

Lemma dupfree_card A (eq_X_dec : eq_dec X) :
dupfree A -> card A = |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
| nil => nil
| x::A' => if decision (x A') then undup A' else x :: undup A'
end.

Lemma undup_id_equi A :
undup A A.

Lemma dupfree_undup A :
dupfree (undup A).

Lemma undup_incl A B :
A B <-> undup A undup B.

Lemma undup_equi A B :
A B <-> undup A undup B.

Lemma undup_id A :
dupfree A -> undup A = A.

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

End Undup.

# Power lists

Section PowerRep.
Variable X : Type.
Context {eq_X_dec : eq_dec X}.

Fixpoint power (U : list X ) : list (list X) :=
match U with
| nil => [nil]
| x :: U' => power U' ++ map (cons x) (power U')
end.

Lemma power_incl A U :
A power U -> A U.

Lemma power_nil U :
nil power U.

Definition rep (A U : list X) : list X :=
filter (fun x => x A) U.

Lemma rep_power A U :
rep A U power U.

Lemma rep_incl A U :
rep A U A.

Lemma rep_in x A U :
A U -> x A -> x rep A U.

Lemma rep_equi A U :
A U -> rep A U A.

Lemma rep_mono A B U :
A B -> rep A U rep B U.

Lemma rep_eq' A B U :
(forall x, x U -> (x A <-> x B)) -> rep A U = rep B U.

Lemma rep_eq A B U :
A B -> rep A U = rep B U.

Lemma rep_injective A B U :
A U -> B U -> rep A U = rep B U -> A B.

Lemma rep_idempotent A U :
rep (rep A U) U = rep A U.

Lemma dupfree_power U :
dupfree U -> dupfree (power U).

Lemma dupfree_in_power U A :
A power U -> dupfree U -> dupfree A.

Lemma rep_dupfree A U :
dupfree U -> A power U -> rep A U = A.

Lemma power_extensional A B U :
dupfree U -> A power U -> B power U -> A B -> A = B.

End PowerRep.

# Finite closure iteration

Module FCI.
Section FCI.
Variable X : Type.
Context {eq_X_dec : eq_dec X}.
Variable step : list X -> X -> Prop.
Context {step_dec : forall A x, dec (step A x)}.
Variable V : list X.

Lemma pick (A : list X) :
{ x | x V /\ step A x /\ ~ x A } + { forall x, x V -> step A x -> x A }.

Definition F (A : list X) : list X.
Defined.

Definition C := it F (card V) nil.

Lemma it_incl n :
it F n nil V.

Lemma incl :
C V.

Lemma ind p :
(forall A x, inclp A p -> x V -> step A x -> p x) -> inclp C p.

Lemma fp :
F C = C.

Lemma closure x :
x V -> step C x -> x C.

End FCI.
End FCI.

# Deprecated names, defined for backward compatibilitly

Definition dupfree_inv := dupfree_cons.