Base Library for ICL

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

(* Switch Coq into implicit argument mode *)

Global Set Implicit Arguments.
(* Load basic Coq libraries *)

Require Export Omega List Morphisms.

(* Inversion tactic *)

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 : XProp) :
  ¬ ( x, p x) x, ¬ p x.

Size recursion

Lemma size_recursion (X : Type) (sigma : Xnat) (p : XType) :
  ( x, ( y, sigma y < sigma xp y) → p x) →
   x, p x.


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)

  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.


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

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

(* Register dec as a type class *)

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.

(* Hints for auto concerning dec *)

Hint Extern 4 ⇒
match goal with
  | [ |- dec ?p ] ⇒ exact (decision p)

(* Improves type class inference *)

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

(* Register instance rules for dec *)

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

(* Coq 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).

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.


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

(* The following comments are for coqdoc *)

Register additional simplification rules with autorewrite / simpl_list

Hint Rewrite <- app_assoc : list.
Hint Rewrite rev_app_distr map_app prod_length : list.
(* Print Rewrite HintDb list. *)

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) :
  ( x, dec (p x)) → dec ( x, x Ap x).

Instance list_exists_dec X A (p : XProp) :
  ( 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_exists_not_incl X (A B : list X) :
  eq_dec X
  ¬ A B x, x A ¬ x B.

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


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 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::Ax yx A.

  Lemma not_in_cons x y A :
    ¬ x y :: Ax y ¬ x A.


  Definition disjoint A B :=
    ¬ x, x A x B.

  Lemma disjoint_forall A B :
    disjoint A B x, x A¬ x B.

  Lemma disjoint_symm A B :
    disjoint A Bdisjoint B A.

  Lemma disjoint_incl A B B' :
    B' Bdisjoint A Bdisjoint 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'.


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 : 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_sing x A y :
    x::A [y]x = y A [y].

  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.

  Lemma incl_app_left A B C :
    A ++ B CA C B C.

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


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.


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'

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_id A :
    ( x, x Ap 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 xfilter p (x::A) = x::filter p A.

  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.

  Lemma rem_id x A :
    ¬ x Arem A x = A.

  Lemma rem_reorder x A :
    x AA x :: rem A x.

  Lemma rem_inclr A B x :
    A B¬ x AA 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.


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::Aif decision (x A) then card A else 1 + card A

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

  Lemma card_not_in_rem A x :
    ¬ x Acard A = card (rem A x).

  Lemma card_le A B :
    A Bcard A card B.

  Lemma card_eq A B :
    A Bcard 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 x, x B ¬ x A.

  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.

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 XProp :=
| dupfreeN : dupfree nil
| dupfreeC x A : ¬ x Adupfree Adupfree (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 Bdupfree Adupfree Bdupfree (A++B).

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

  Lemma dupfree_filter p (p_dec : x, dec (p x)) A :
    dupfree Adupfree (filter p A).

  Lemma dupfree_dec A :
    eq_dec Xdec (dupfree A).

  Lemma dupfree_card A (eq_X_dec : eq_dec X) :
    dupfree Acard 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
      | nilnil
      | x::A'if decision (x A') then undup A' else x :: undup A'

  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 Aundup 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')

  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.

  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.

Deprecated names, defined for backward compatibilitly

Definition dupfree_inv := dupfree_cons.