# Base Library for ICL

• Author: Gert Smolka, Saarland University
• Version: 4 June 2014

GlobalGlobal

# Iteration

Section Iteration.
Variable X : Type.
Variable f : XX.

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

Lemma it_ind (p : XProp) x n :
p x → ( z, p zp (f z)) → p (it n x).

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

Lemma it_fp (sigma : Xnat) x :
( 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" := ( 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.

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

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

Instance iff_dec (X Y : Prop) :
dec Xdec Ydec (X Y).

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.

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.

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

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

Decidability laws for lists

Instance list_eq_dec X :
eq_dec Xeq_dec (list X).

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

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

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

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

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

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

Membership
We use the following facts from the standard library List.

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.

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

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.

Definition inclp (X : Type) (A : list X) (p : XProp) : Prop :=
x, x Ap x.

Setoid rewriting with list inclusion and list equivalence

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

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

Equivalence

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.

# Filter

Definition filter (X : Type) (p : XProp) (p_dec : x, dec (p x)) : list Xlist X :=
fix f A := match A with
| nilnil
| x::A'if decision (p x) then x :: f A' else f A'
end.

Section FilterLemmas.
Variable X : Type.
Variable p : XProp.
Context {p_dec : 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 Bfilter p A filter p B.

Lemma filter_fst x A :
p xfilter p (x::A) = x::filter p A.

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

Lemma filter_fst' x A :
¬ p xfilter p (x::A) = filter p A.

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

Lemma filter_and A :
filter p (filter q A) = filter (fun xp x q x) A.

End FilterLemmas_pq.

Section FilterComm.
Variable X : Type.
Variable p q : XProp.
Context {p_dec : x, dec (p x)}.
Context {q_dec : 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 zz 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 Brem A x rem B x.

Lemma rem_cons A B x :
A Brem (x::A) x B.

Lemma rem_cons' A B x y :
x Brem A y Brem (x::A) y B.

Lemma rem_in x y A :
x rem A yx A.

Lemma rem_neq x y A :
x yx Ax rem A y.

Lemma rem_app x A B :
x AB A ++ rem B x.

Lemma rem_app' x A B C :
rem A x Crem B x Crem (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 yrem (x::A) y = x::rem A y.

End Removal.

# 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_fp_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_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.

Lemma card_cons x A :
card (x::A) = if decision (x A) then card A else 1 + card A.

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

Lemma card_0 A :
card A = 0 → A = nil.

End Cardinality.

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

# 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 UA U.

Lemma power_nil U :
nil power U.

Definition rep (A U : list X) : list X :=
filter (fun xx 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 Ux Ax rep A U.

Lemma rep_equi A U :
A Urep A U A.

Lemma rep_mono A B U :
A Brep A U rep B U.

Lemma rep_eq' A B U :
( x, x U → (x A x B)) → rep A U = rep B U.

Lemma rep_eq A B U :
A Brep A U = rep B U.

Lemma rep_injective A B U :
A UB Urep A U = rep B UA B.

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

Lemma dupfree_power U :
dupfree Udupfree (power U).

Lemma dupfree_in_power U A :
A power Udupfree Udupfree A.

Lemma rep_dupfree A U :
dupfree UA power Urep A U = A.

Lemma power_extensional A B U :
dupfree UA power UB power UA BA = B.

End PowerRep.

# Finite closure iteration

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

Lemma pick (A : list X) :
{ x | x V step A x ¬ x A } + { x, x Vstep A xx 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 :
( A x, inclp A px Vstep A xp x) → inclp C p.

Lemma fp :
F C = C.

Lemma closure x :
x Vstep C xx C.

End FCI.
End FCI.

Lemma complete_induction (p : natProp) (x : nat) :
( x, ( y, y<xp y) → p x) → p x.

Lemma size_induction X (f : Xnat) (p : XProp) :
( x, ( y, f y < f xp y) → p x) →
x, p x.

Section pos.

Definition elAt := nth_error.
Notation "A '.[' i ']'" := (elAt A i) (no associativity, at level 50).

Fixpoint pos (X : Type) {e : eq_dec X} (s : X) (A : list X) :=
match A with
| nilNone
| a :: Aif decision (s = a) then Some 0 else match pos s A with NoneNone | Some nSome (S n) end
end.

Lemma el_pos X (E : eq_dec X) s A : s A m, pos s A = Some m.

Lemma pos_elAt X (_ : eq_dec X) s A i : pos s A = Some iA .[i] = Some s.

Lemma elAt_app X (A : list X) i B s : A .[i] = Some s(A ++ B).[i] = Some s.

Lemma elAt_el (X : Type) A (s : X) m : A .[ m ] = Some ss A.

Lemma el_elAt X {_ : eq_dec X} (s : X) A : s A m, A .[ m ] = Some s.

Lemma dupfree_elAt X (A : list X) n m s : dupfree AA.[n] = Some sA.[m] = Some sn = m.

Lemma nth_error_none A n l : nth_error l n = @None Alength l n.

End pos.