(** * 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. Global Unset Strict Implicit. (* 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. Proof. tauto. Qed. Lemma DM_exists X (p : X -> Prop) : ~ (exists x, p x) <-> forall x, ~ p x. Proof. firstorder. Qed. (** * 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. Proof. intros D x. apply D. cut (forall n y, sigma y < n -> p y). now eauto. clear x. intros n. induction n; intros y E. - exfalso; omega. - apply D. intros x F. apply IHn. omega. Defined. Arguments size_recursion {X} sigma {p} _ _. (** * 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). Proof. intros A B. induction n; simpl; auto. Qed. 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). Proof. intros A. assert (B: forall n, FP (it n x) \/ sigma x >= n + sigma (it n x)). { intros n; induction n; simpl. - auto. - destruct IHn as [B|B]. + left. now rewrite B. + destruct (A n) as [C|C]. * left. now rewrite C. * right. simpl in C. omega. } destruct (A (sigma x)), (B (sigma x)); auto; exfalso; omega. Qed. End Iteration. (** * Decidability *) Definition dec (X : Prop) : Type := {X} + {~ X}. Notation "'eq_dec' X" := (forall x y : X, dec (x=y)) (at level 70). (* Register dec as a type class *) Existing Class dec. Definition decision (X : Prop) (D : dec X) : dec X := D. Arguments decision 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) end. (* 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 A => A). Instance impl_dec (X Y : Prop) : dec X -> dec Y -> dec (X -> Y). Proof. unfold dec; tauto. Defined. Instance and_dec (X Y : Prop) : dec X -> dec Y -> dec (X /\ Y). Proof. unfold dec; tauto. Defined. Instance or_dec (X Y : Prop) : dec X -> dec Y -> dec (X \/ Y). Proof. unfold dec; tauto. Defined. (* 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 X -> dec (~ X). Proof. unfold not. auto. Defined. Instance iff_dec (X Y : Prop) : dec X -> dec Y -> dec (X <-> Y). Proof. unfold iff. auto. Qed. Lemma dec_DN X : dec X -> ~~ X -> X. Proof. unfold dec; tauto. Qed. Lemma dec_DM_and X Y : dec X -> dec Y -> ~ (X /\ Y) -> ~ X \/ ~ Y. Proof. unfold dec; tauto. Qed. Lemma dec_DM_impl X Y : dec X -> dec Y -> ~ (X -> Y) -> X /\ ~ Y. Proof. unfold dec; tauto. Qed. Lemma dec_prop_iff (X Y : Prop) : (X <-> Y) -> dec X -> dec Y. Proof. unfold dec; tauto. Defined. Instance bool_eq_dec : eq_dec bool. Proof. intros x y. hnf. decide equality. Defined. Instance nat_eq_dec : eq_dec nat. Proof. intros x y. hnf. decide equality. Defined. 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). (* The following comments are for coqdoc *) (** printing el #∊# *) (** printing <<= #⊆# *) (** printing === #≡# *) (** 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. Proof. intros B. assert (C: |x::A| <> |A|) by (simpl; omega). apply C. now rewrite B. Qed. (** * Decidability laws for lists *) Instance list_eq_dec X : eq_dec X -> eq_dec (list X). Proof. intros D. apply list_eq_dec. exact D. Defined. Instance list_in_dec (X : Type) (x : X) (A : list X) : eq_dec X -> dec (x el A). Proof. intros D. apply in_dec. exact D. Defined. Lemma list_sigma_forall X A (p : X -> Prop) (p_dec : forall x, dec (p x)) : {x | x el A /\ p x} + {forall x, x el A -> ~ p x}. Proof. induction A as [|x A]; simpl. - tauto. - destruct IHA as [[y [D E]]|D]. + eauto. + destruct (p_dec x) as [E|E]. * eauto. * right. intros y [[]|F]; auto. Defined. Arguments list_sigma_forall {X} A p {p_dec}. Instance list_forall_dec X A (p : X -> Prop) : (forall x, dec (p x)) -> dec (forall x, x el A -> p x). Proof. intros p_dec. destruct (list_sigma_forall A (fun x => ~ p x)) as [[x [D E]]|D]. - right. auto. - left. intros x E. apply dec_DN; auto. Defined. Instance list_exists_dec X A (p : X -> Prop) : (forall x, dec (p x)) -> dec (exists x, x el A /\ p x). Proof. intros p_dec. destruct (list_sigma_forall A p) as [[x [D E]]|D]. - unfold dec. eauto. - right. intros [x [E F]]. exact (D x E F). Defined. Lemma list_exists_DM X A (p : X -> Prop) : (forall x, dec (p x)) -> ~ (forall x, x el A -> ~ p x) -> exists x, x el A /\ p x. Proof. intros D E. destruct (list_sigma_forall A p) as [F|F]. + destruct F as [x F]. eauto. + contradiction (E F). Qed. Lemma list_exists_not_incl X (A B : list X) : eq_dec X -> ~ A <<= B -> exists x, x el A /\ ~ x el B. Proof. intros D E. apply list_exists_DM; auto. intros F. apply E. intros x G. apply dec_DN; auto. Qed. Lemma list_cc X (p : X -> Prop) A : (forall x, dec (p x)) -> (exists x, x el A /\ p x) -> {x | x el A /\ p x}. Proof. intros D E. destruct (list_sigma_forall A p) as [[x [F G]]|F]. - eauto. - exfalso. destruct E as [x [G H]]. apply (F x); auto. Defined. (** * Membership We use the following lemmas from Coq's standard library List. - [in_eq : x el x::A] - [in_nil : ~ x el nil] - [in_cons : x el A -> x el y::A] - [in_or_app : x el A \/ x el B -> x el A++B] - [in_app_iff : x el A++B <-> x el A \/ x el B] - [in_map_iff : y el map f A <-> exists x, f x = y /\ x el 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 el [y] -> x = y. Proof. simpl. intros [[]|[]]. reflexivity. Qed. Lemma in_cons_neq x y A : x el y::A -> x <> y -> x el A. Proof. simpl. intros [[]|D] E; congruence. Qed. Lemma not_in_cons x y A : ~ x el y :: A -> x <> y /\ ~ x el A. Proof. intuition; subst; auto. Qed. (** * Disjointness *) Definition disjoint A B := ~ exists x, x el A /\ x el B. Lemma disjoint_forall A B : disjoint A B <-> forall x, x el A -> ~ x el B. Proof. split. - intros D x E F. apply D. exists x. auto. - intros D [x [E F]]. exact (D x E F). Qed. Lemma disjoint_symm A B : disjoint A B -> disjoint B A. Proof. firstorder. Qed. Lemma disjoint_incl A B B' : B' <<= B -> disjoint A B -> disjoint A B'. Proof. firstorder. Qed. Lemma disjoint_nil B : disjoint nil B. Proof. firstorder. Qed. Lemma disjoint_nil' A : disjoint A nil. Proof. firstorder. Qed. Lemma disjoint_cons x A B : disjoint (x::A) B <-> ~ x el B /\ disjoint A B. Proof. split. - intros D. split. + intros E. apply D. eauto. + intros [y [E F]]. apply D. eauto. - intros [D E] [y [[F|F] G]]. + congruence. + apply E. eauto. Qed. Lemma disjoint_app A B C : disjoint (A ++ B) C <-> disjoint A C /\ disjoint B C. Proof. split. - intros D. split. + intros [x [E F]]. eauto 6. + intros [x [E F]]. eauto 6. - intros [D E] [x [F G]]. apply in_app_iff in F as [F|F]; eauto. Qed. 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 el 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. Proof. intros x []. Qed. Hint Resolve incl_nil. Lemma incl_map X Y A B (f : X -> Y) : A <<= B -> map f A <<= map f B. Proof. intros D y E. apply in_map_iff in E as [x [E E']]. subst y. apply in_map_iff. eauto. Qed. Section Inclusion. Variable X : Type. Implicit Types A B : list X. Lemma incl_nil_eq A : A <<= nil -> A=nil. Proof. intros D. destruct A as [|x A]. - reflexivity. - exfalso. apply (D x). auto. Qed. Lemma incl_shift x A B : A <<= B -> x::A <<= x::B. Proof. auto. Qed. Lemma incl_lcons x A B : x::A <<= B <-> x el B /\ A <<= B. Proof. split. - intros D. split; hnf; auto. - intros [D E] z [F|F]; subst; auto. Qed. Lemma incl_sing x A y : x::A <<= [y] -> x = y /\ A <<= [y]. Proof. rewrite incl_lcons. intros [D E]. apply in_sing in D. auto. Qed. Lemma incl_rcons x A B : A <<= x::B -> ~ x el A -> A <<= B. Proof. intros C D y E. destruct (C y E) as [F|F]; congruence. Qed. Lemma incl_lrcons x A B : x::A <<= x::B -> ~ x el A -> A <<= B. Proof. intros C D y E. assert (F: y el x::B) by auto. destruct F as [F|F]; congruence. Qed. Lemma incl_app_left A B C : A ++ B <<= C -> A <<= C /\ B <<= C. Proof. firstorder. Qed. End Inclusion. Definition inclp (X : Type) (A : list X) (p : X -> Prop) : Prop := forall x, x el A -> p x. (** * Setoid rewriting with list inclusion and list equivalence *) Instance incl_preorder X : PreOrder (@incl X). Proof. constructor; hnf; unfold incl; auto. Qed. Instance equi_Equivalence X : Equivalence (@equi X). Proof. constructor; hnf; firstorder. Qed. Instance incl_equi_proper X : Proper (@equi X ==> @equi X ==> iff) (@incl X). Proof. hnf. intros A B D. hnf. firstorder. Qed. Instance cons_incl_proper X x : Proper (@incl X ==> @incl X) (@cons X x). Proof. hnf. apply incl_shift. Qed. Instance cons_equi_proper X x : Proper (@equi X ==> @equi X) (@cons X x). Proof. hnf. firstorder. Qed. Instance in_incl_proper X x : Proper (@incl X ==> Basics.impl) (@In X x). Proof. intros A B D. hnf. auto. Qed. Instance in_equi_proper X x : Proper (@equi X ==> iff) (@In X x). Proof. intros A B D. firstorder. Qed. Instance app_incl_proper X : Proper (@incl X ==> @incl X ==> @incl X) (@app X). Proof. intros A B D A' B' E. auto. Qed. Instance app_equi_proper X : Proper (@equi X ==> @equi X ==> @equi X) (@app X). Proof. hnf. intros A B D. hnf. intros A' B' E. destruct D, E; auto. Qed. (** * Equivalence *) Section Equi. Variable X : Type. Implicit Types A B : list X. Lemma equi_push x A : x el A -> A === x::A. Proof. auto. Qed. Lemma equi_dup x A : x::A === x::x::A. Proof. auto. Qed. Lemma equi_swap x y A: x::y::A === y::x::A. Proof. split; intros z; simpl; tauto. Qed. Lemma equi_shift x A B : x::A++B === A++x::B. Proof. split; intros y. - intros [D|D]. + subst; auto. + apply in_app_iff in D as [D|D]; auto. - intros D. apply in_app_iff in D as [D|D]. + auto. + destruct D; subst; auto. Qed. Lemma equi_rotate x A : x::A === A++[x]. Proof. split; intros y; simpl. - intros [D|D]; subst; auto. - intros D. apply in_app_iff in D as [D|D]. + auto. + apply in_sing in D. auto. Qed. 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. Arguments filter {X} p {p_dec} A. Section FilterLemmas. Variable X : Type. Variable p : X -> Prop. Context {p_dec : forall x, dec (p x)}. Lemma in_filter_iff x A : x el filter p A <-> x el A /\ p x. Proof. induction A as [|y A]; simpl. - tauto. - decide (p y) as [B|B]; simpl; rewrite IHA; intuition; subst; tauto. Qed. Lemma filter_incl A : filter p A <<= A. Proof. intros x D. apply in_filter_iff in D. apply D. Qed. Lemma filter_mono A B : A <<= B -> filter p A <<= filter p B. Proof. intros D x E. apply in_filter_iff in E as [E E']. apply in_filter_iff. auto. Qed. Lemma filter_id A : (forall x, x el A -> p x) -> filter p A = A. Proof. intros D. induction A as [|x A]; simpl. - reflexivity. - decide (p x) as [E|E]. + f_equal; auto. + exfalso. auto. Qed. Lemma filter_app A B : filter p (A ++ B) = filter p A ++ filter p B. Proof. induction A as [|y A]; simpl. - reflexivity. - rewrite IHA. decide (p y); reflexivity. Qed. Lemma filter_fst x A : p x -> filter p (x::A) = x::filter p A. Proof. simpl. decide (p x); tauto. Qed. Lemma filter_fst' x A : ~ p x -> filter p (x::A) = filter p A. Proof. simpl. decide (p x); tauto. Qed. 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 el A -> p x -> q x) -> filter p A <<= filter q A. Proof. intros D x E. apply in_filter_iff in E as [E E']. apply in_filter_iff. auto. Qed. Lemma filter_pq_eq A : (forall x, x el A -> (p x <-> q x)) -> filter p A = filter q A. Proof. intros C; induction A as [|x A]; simpl. - reflexivity. - decide (p x) as [D|D]; decide (q x) as [E|E]. + f_equal. auto. + exfalso. apply E, (C x); auto. + exfalso. apply D, (C x); auto. + auto. Qed. Lemma filter_and A : filter p (filter q A) = filter (fun x => p x /\ q x) A. Proof. set (r x := p x /\ q x). induction A as [|x A]; simpl. reflexivity. decide (q x) as [E|E]; simpl; rewrite IHA. - decide (p x); decide (r x); unfold r in *|-; auto; tauto. - decide (r x); unfold r in *|-; auto; tauto. Qed. 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). Proof. rewrite !filter_and. apply filter_pq_eq. tauto. Qed. 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 el rem A y <-> x el A /\ x <> y. Proof. apply in_filter_iff. Qed. Lemma rem_not_in x y A : x = y \/ ~ x el A -> ~ x el rem A y. Proof. intros D E. apply in_rem_iff in E. tauto. Qed. Lemma rem_incl A x : rem A x <<= A. Proof. apply filter_incl. Qed. Lemma rem_mono A B x : A <<= B -> rem A x <<= rem B x. Proof. apply filter_mono. Qed. Lemma rem_cons A B x : A <<= B -> rem (x::A) x <<= B. Proof. intros E y F. apply E. apply in_rem_iff in F. destruct F as [[|]]; congruence. Qed. Lemma rem_cons' A B x y : x el B -> rem A y <<= B -> rem (x::A) y <<= B. Proof. intros E F u G. apply in_rem_iff in G as [[[]|G] H]. exact E. apply F. apply in_rem_iff. auto. Qed. Lemma rem_in x y A : x el rem A y -> x el A. Proof. apply rem_incl. Qed. Lemma rem_neq x y A : x <> y -> x el A -> x el rem A y. Proof. intros E F. apply in_rem_iff. auto. Qed. Lemma rem_app x A B : x el A -> B <<= A ++ rem B x. Proof. intros E y F. decide (x=y) as [[]|]; auto using rem_neq. Qed. Lemma rem_app' x A B C : rem A x <<= C -> rem B x <<= C -> rem (A ++ B) x <<= C. Proof. unfold rem; rewrite filter_app; auto. Qed. Lemma rem_equi x A : x::A === x::rem A x. Proof. split; intros y; intros [[]|E]; decide (x=y) as [[]|D]; eauto using rem_in, rem_neq. Qed. Lemma rem_comm A x y : rem (rem A x) y = rem (rem A y) x. Proof. apply filter_comm. Qed. Lemma rem_fst x A : rem (x::A) x = rem A x. Proof. unfold rem. rewrite filter_fst'; auto. Qed. Lemma rem_fst' x y A : x <> y -> rem (x::A) y = x::rem A y. Proof. intros E. unfold rem. rewrite filter_fst; auto. Qed. Lemma rem_id x A : ~ x el A -> rem A x = A. Proof. intros D. apply filter_id. intros y E F. subst. auto. Qed. Lemma rem_reorder x A : x el A -> A === x :: rem A x. Proof. intros D. rewrite <- rem_equi. apply equi_push, D. Qed. Lemma rem_inclr A B x : A <<= B -> ~ x el A -> A <<= rem B x. Proof. intros D E y F. apply in_rem_iff. intuition; subst; auto. Qed. 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 el A) then card A else 1 + card A end. Lemma card_in_rem x A : x el A -> card A = 1 + card (rem A x). Proof. intros D. induction A as [|y A]; simpl. - contradiction D. - decide (y <> x) as [E|E]; simpl. + rewrite IHA. * { decide (y el A) as [G|G]; decide (y el rem A x) as [K|K]; (reflexivity || exfalso). - auto. - eapply G, in_rem_iff, K. } * destruct D; tauto. + apply dec_DN in E; auto; subst y. decide (x el A) as [F|F]. * auto. * rewrite rem_id; auto. Qed. Lemma card_not_in_rem A x : ~ x el A -> card A = card (rem A x). Proof. intros D; rewrite rem_id; auto. Qed. Lemma card_le A B : A <<= B -> card A <= card B. Proof. revert B. induction A as [|x A]; intros B D; simpl. - omega. - apply incl_lcons in D as [D D1]. decide (x el A) as [E|E]. + auto. + rewrite (card_in_rem D). cut (card A <= card (rem B x)). omega. apply IHA. auto. Qed. Lemma card_eq A B : A === B -> card A = card B. Proof. intros [E F]. apply card_le in E. apply card_le in F. omega. Qed. Lemma card_cons_rem x A : card (x::A) = 1 + card (rem A x). Proof. rewrite (card_eq (rem_equi x A)). simpl. decide (x el rem A x) as [D|D]. - exfalso. apply in_rem_iff in D; tauto. - reflexivity. Qed. Lemma card_0 A : card A = 0 -> A = nil. Proof. destruct A as [|x A]; intros D. - reflexivity. - exfalso. rewrite card_cons_rem in D. omega. Qed. Lemma card_ex A B : card A < card B -> exists x, x el B /\ ~ x el A. Proof. intros D. decide (B <<= A) as [E|E]. - exfalso. apply card_le in E. omega. - apply list_exists_not_incl; auto. Qed. Lemma card_equi A B : A <<= B -> card A = card B -> A === B. Proof. revert B. induction A as [|x A]; simpl; intros B D E. - symmetry in E. apply card_0 in E. now rewrite E. - apply incl_lcons in D as [D D1]. decide (x el A) as [F|F]. + rewrite (IHA B); auto. + rewrite (IHA (rem B x)). * symmetry. apply rem_reorder, D. * auto. * apply card_in_rem in D. omega. Qed. Lemma card_lt A B x : A <<= B -> x el B -> ~ x el A -> card A < card B. Proof. intros D E F. decide (card A = card B) as [G|G]. + exfalso. apply F. apply (card_equi D); auto. + apply card_le in D. omega. Qed. Lemma card_or A B : A <<= B -> A === B \/ card A < card B. Proof. intros D. decide (card A = card B) as [F|F]. - left. apply card_equi; auto. - right. apply card_le in D. omega. Qed. End Cardinality. Instance card_equi_proper X (D: eq_dec X) : Proper (@equi X ==> eq) (@card X D). Proof. hnf. apply card_eq. Qed. (** * Duplicate-free lists *) Inductive dupfree (X : Type) : list X -> Prop := | dupfreeN : dupfree nil | dupfreeC x A : ~ x el 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 el A /\ dupfree A. Proof. split; intros D. - inv D; auto. - apply dupfreeC; tauto. Qed. Lemma dupfree_app A B : disjoint A B -> dupfree A -> dupfree B -> dupfree (A++B). Proof. intros D E F. induction E as [|x A E' E]; simpl. - exact F. - apply disjoint_cons in D as [D D']. constructor; [|exact (IHE D')]. intros G. apply in_app_iff in G; tauto. Qed. Lemma dupfree_map Y A (f : X -> Y) : (forall x y, x el A -> y el A -> f x = f y -> x=y) -> dupfree A -> dupfree (map f A). Proof. intros D E. induction E as [|x A E' E]; simpl. - constructor. - constructor; [|now auto]. intros F. apply in_map_iff in F as [y [F F']]. rewrite (D y x) in F'; auto. Qed. Lemma dupfree_filter p (p_dec : forall x, dec (p x)) A : dupfree A -> dupfree (filter p A). Proof. intros D. induction D as [|x A C D]; simpl. - left. - decide (p x) as [E|E]; [|exact IHD]. right; [|exact IHD]. intros F. apply C. apply filter_incl in F. exact F. Qed. Lemma dupfree_dec A : eq_dec X -> dec (dupfree A). Proof. intros D. induction A as [|x A]. - left. left. - decide (x el A) as [E|E]. + right. intros F. inv F; tauto. + destruct (IHA) as [F|F]. * unfold dec. auto using dupfree. * right. intros G. inv G; tauto. Qed. Lemma dupfree_card A (eq_X_dec : eq_dec X) : dupfree A -> card A = |A|. Proof. intros D. induction D as [|x A E F]; simpl. - reflexivity. - decide (x el A) as [G|]. + contradiction (E G). + omega. Qed. 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 el A') then undup A' else x :: undup A' end. Lemma undup_id_equi A : undup A === A. Proof. induction A as [|x A]; simpl. - reflexivity. - decide (x el A) as [E|E]; rewrite IHA; auto. Qed. Lemma dupfree_undup A : dupfree (undup A). Proof. induction A as [|x A]; simpl. - left. - decide (x el A) as [E|E]; auto. right; auto. now rewrite undup_id_equi. Qed. Lemma undup_incl A B : A <<= B <-> undup A <<= undup B. Proof. now rewrite !undup_id_equi. Qed. Lemma undup_equi A B : A === B <-> undup A === undup B. Proof. now rewrite !undup_id_equi. Qed. Lemma undup_id A : dupfree A -> undup A = A. Proof. intros E. induction E as [|x A E F]; simpl. - reflexivity. - rewrite IHF. decide (x el A) as [G|G]; tauto. Qed. Lemma undup_idempotent A : undup (undup A) = undup A. Proof. apply undup_id, dupfree_undup. Qed. 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 el power U -> A <<= U. Proof. revert A; induction U as [|x U]; simpl; intros A D. - destruct D as [[]|[]]; auto. - apply in_app_iff in D as [E|E]. now auto. apply in_map_iff in E as [A' [E F]]. subst A. auto. Qed. Lemma power_nil U : nil el power U. Proof. induction U; simpl; auto. Qed. Definition rep (A U : list X) : list X := filter (fun x => x el A) U. Lemma rep_power A U : rep A U el power U. Proof. revert A; induction U as [|x U]; intros A. - simpl; auto. - simpl. decide (x el A) as [D|D]; auto using in_map. Qed. Lemma rep_incl A U : rep A U <<= A. Proof. unfold rep. intros x D. apply in_filter_iff in D. apply D. Qed. Lemma rep_in x A U : A <<= U -> x el A -> x el rep A U. Proof. intros D E. apply in_filter_iff; auto. Qed. Lemma rep_equi A U : A <<= U -> rep A U === A. Proof. intros D. split. now apply rep_incl. intros x. apply rep_in, D. Qed. Lemma rep_mono A B U : A <<= B -> rep A U <<= rep B U. Proof. intros D. apply filter_pq_mono. auto. Qed. Lemma rep_eq' A B U : (forall x, x el U -> (x el A <-> x el B)) -> rep A U = rep B U. Proof. intros D. apply filter_pq_eq. auto. Qed. Lemma rep_eq A B U : A === B -> rep A U = rep B U. Proof. intros D. apply filter_pq_eq. firstorder. Qed. Lemma rep_injective A B U : A <<= U -> B <<= U -> rep A U = rep B U -> A === B. Proof. intros D E F. transitivity (rep A U). - symmetry. apply rep_equi, D. - rewrite F. apply rep_equi, E. Qed. Lemma rep_idempotent A U : rep (rep A U) U = rep A U. Proof. unfold rep at 1 3. apply filter_pq_eq. intros x D. split. + apply rep_incl. + intros E. apply in_filter_iff. auto. Qed. Lemma dupfree_power U : dupfree U -> dupfree (power U). Proof. intros D. induction D as [|x U E D]; simpl. - constructor. now auto. constructor. - apply dupfree_app. + intros [A [F G]]. apply in_map_iff in G as [A' [G G']]. subst A. apply E. apply (power_incl F). auto. + exact IHD. + apply dupfree_map; congruence. Qed. Lemma dupfree_in_power U A : A el power U -> dupfree U -> dupfree A. Proof. intros E D. revert A E. induction D as [|x U D D']; simpl; intros A E. - destruct E as [[]|[]]. constructor. - apply in_app_iff in E as [E|E]. + auto. + apply in_map_iff in E as [A' [E E']]. subst A. constructor. * intros F; apply D. apply (power_incl E'), F. * auto. Qed. Lemma rep_dupfree A U : dupfree U -> A el power U -> rep A U = A. Proof. intros D; revert A. induction D as [|x U E F]; intros A G. - destruct G as [[]|[]]; reflexivity. - simpl in G. apply in_app_iff in G as [G|G]. + simpl. decide (x el A) as [H|H]. * exfalso. apply E. apply (power_incl G), H. * auto. + apply in_map_iff in G as [A' [G H]]. subst A. simpl. decide (x=x \/ x el A') as [G|G]. * f_equal. rewrite <- (IHF A' H) at 2. apply filter_pq_eq. apply power_incl in H. intros z K. split; [|now auto]. intros [L|L]; subst; tauto. * exfalso; auto. Qed. Lemma power_extensional A B U : dupfree U -> A el power U -> B el power U -> A === B -> A = B. Proof. intros D E F G. rewrite <- (rep_dupfree D E). rewrite <- (rep_dupfree D F). apply rep_eq, G. Qed. 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 el V /\ step A x /\ ~ x el A } + { forall x, x el V -> step A x -> x el A }. Proof. destruct (list_sigma_forall V (fun x => step A x /\ ~ x el A)) as [E|E]. - auto. - right. intros x F G. decide (x el A). assumption. exfalso. eapply E; eauto. Qed. Definition F (A : list X) : list X. destruct (pick A) as [[x _]|_]. - exact (x::A). - exact A. Defined. Definition C := it F (card V) nil. Lemma it_incl n : it F n nil <<= V. Proof. apply it_ind. now auto. intros A E. unfold F. destruct (pick A) as [[x G]|G]; intuition. Qed. Lemma incl : C <<= V. Proof. apply it_incl. Qed. Lemma ind p : (forall A x, inclp A p -> x el V -> step A x -> p x) -> inclp C p. Proof. intros B. unfold C. apply it_ind. + intros x []. + intros D G x. unfold F. destruct (pick D) as [[y E]|E]. * intros [[]|]; intuition; eauto. * intuition. Qed. Lemma fp : F C = C. Proof. pose (sigma (A : list X) := card V - card A). replace C with (it F (sigma nil) nil). - apply it_fp. intros n. simpl. set (J:= it F n nil). unfold FP, F. destruct (pick J) as [[x B]|B]. + right. assert (G: card J < card (x :: J)). { apply card_lt with (x:=x); intuition. } assert (H: card (x :: J) <= card V). { apply card_le, incl_cons. apply B. apply it_incl. } unfold sigma. omega. + auto. - unfold C, sigma. f_equal. change (card nil) with 0. omega. Qed. Lemma closure x : x el V -> step C x -> x el C. Proof. assert (A2:= fp). unfold F in A2. destruct (pick C) as [[y _]| B]. + contradiction (list_cycle A2). + apply B. Qed. End FCI. End FCI. (** * Deprecated names, defined for backward compatibilitly *) Definition dupfree_inv := dupfree_cons.