# Base Library for ICL

• Version: 25 June 2014
• Author: Gert Smolka, Saarland University
• Acknowlegments: Sigurd Schneider, Dominik Karst

(* 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; try clear H.

# Size recursion

Lemma size_recursion (X : Type) (sigma : X nat) (p : X Type) :
( x, ( y, sigma y < sigma x p y) p x)
x, p x.
Proof.
intros D x. apply D.
cut ( 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.
Qed.

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 ( 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 :
( n, FP (it n x) sigma (it n x) > sigma (it (S n) x))
FP (it (sigma x) x).
Proof.
intros A.
assert (B: 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" := ( 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 AA).

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

(* Notations for 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 *)

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

A useful lemma

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 âˆŠ A).
Proof.
intros D. apply in_dec. exact D.
Defined.

Lemma list_sigma_forall X A (p : X Prop) (p_dec : x, dec (p x)) :
{x | x âˆŠ A p x} + { x, x âˆŠ 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) :
( x, dec (p x)) dec ( x, x âˆŠ 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) :
( x, dec (p x)) dec ( x, x âˆŠ 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) :
( x, dec (p x))
¬ ( x, x âˆŠ A ¬ p x) x, x âˆŠ A p x.
Proof.
intros D E.
destruct (list_sigma_forall A p) as [F|F].
+ destruct F as [x F]. eauto.
Qed.

Lemma list_exists_not_incl X (A B : list X) :
eq_dec X
¬ A âŠ† B x, x âˆŠ A ¬ x âˆŠ 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 :
( x, dec (p x))
( x, x âˆŠ A p x) {x | x âˆŠ 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 âˆŠ 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.
Proof.
simpl. intros [[]|[]]. reflexivity.
Qed.

Lemma in_cons_neq x y A :
x âˆŠ y::A x y x âˆŠ A.
Proof.
simpl. intros [[]|D] E; congruence.
Qed.

Lemma not_in_cons x y A :
¬ x âˆŠ y :: A x y ¬ x âˆŠ A.
Proof.
intuition; subst; auto.
Qed.

Definition disjoint A B :=
¬ x, x âˆŠ A x âˆŠ B.

Lemma disjoint_nil B :
disjoint nil B.
Proof.
firstorder.
Qed.

Lemma disjoint_nil' A :
disjoint A nil.
Proof.
firstorder.
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_forall A B :
disjoint A B x, x âˆŠ A ¬ x âˆŠ B.
Proof.
split.
- intros D x E F. apply D. x. auto.
- intros D [x [E F]]. exact (D x E F).
Qed.

Lemma disjoint_cons x A B :
disjoint (x::A) B ¬ x âˆŠ 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.
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.

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 âˆŠ 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 âˆŠ 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 âˆŠ A A âŠ† B.

Proof.
intros C D y E.
assert (F: y âˆŠ 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 :=
x, x âˆŠ 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 âˆŠ 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 : x, dec (p x)) : list X list X :=
fix f A := match A with
| nilnil
| 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 : x, dec (p x)}.

Lemma in_filter_iff x A :
x âˆŠ filter p A x âˆŠ 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 :
( x, x âˆŠ 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 : x, dec (p x)}.
Context {q_dec : x, dec (q x)}.

Lemma filter_pq_mono A :
( x, x âˆŠ 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 :
( x, x âˆŠ 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 xp 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 : 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).
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 zz x) A.

Lemma in_rem_iff x A y :
x âˆŠ rem A y x âˆŠ A x y.
Proof.
apply in_filter_iff.
Qed.

Lemma rem_not_in x y A :
x = y ¬ x âˆŠ A ¬ x âˆŠ 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 âˆŠ 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 âˆŠ rem A y x âˆŠ A.
Proof.
apply rem_incl.
Qed.

Lemma rem_neq x y A :
x y x âˆŠ A x âˆŠ rem A y.
Proof.
intros E F. apply in_rem_iff. auto.
Qed.

Lemma rem_app x A B :
x âˆŠ 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 âˆŠ A rem A x = A.
Proof.
intros D. apply filter_id.
intros y E F. subst. auto.
Qed.

Lemma rem_reorder x A :
x âˆŠ 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 âˆŠ 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::Aif 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).
Proof.
intros D.
induction A as [|y A]; simpl.
- decide (y x) as [E|E]; simpl.
+ rewrite IHA.
× { decide (y âˆŠ A) as [G|G];
decide (y âˆŠ 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 âˆŠ A) as [F|F].
× auto.
× rewrite rem_id; auto.
Qed.

Lemma card_not_in_rem A x :
¬ x âˆŠ 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 âˆŠ 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 âˆŠ 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 x, x âˆŠ B ¬ x âˆŠ 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 âˆŠ 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 âˆŠ B ¬ x âˆŠ 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 âˆŠ 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.
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) :
( x y, x âˆŠ A y âˆŠ 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 : 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 âˆŠ 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 âˆŠ A) as [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
| nilnil
| x::A'if decision (x âˆŠ 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 âˆŠ 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 âˆŠ 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 âˆŠ 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 âˆŠ 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 âˆŠ power U.

Proof. induction U; simpl; auto. Qed.

Definition rep (A U : list X) : list X :=
filter (fun xx âˆŠ A) U.

Lemma rep_power A U :
rep A U âˆŠ power U.

Proof.
revert A; induction U as [|x U]; intros A.
- simpl; auto.
- simpl. decide (x âˆŠ 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 âˆŠ A x âˆŠ 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 :
( x, x âˆŠ U (x âˆŠ A x âˆŠ 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 âˆŠ 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 âˆŠ 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 âˆŠ 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 âˆŠ 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 âˆŠ power U B âˆŠ 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 : 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 âˆŠ V step A x x âˆŠ A }.
Proof.
destruct (list_sigma_forall V (fun xstep A x ¬ x âˆŠ A)) as [E|E].
- auto.
- right. intros x F G.
decide (x âˆŠ 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 :
( A x, inclp A p x âˆŠ 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 âˆŠ V step C x x âˆŠ C.
Proof.
assert (A2:= fp).
unfold F in A2.
destruct (pick C) as [[y _]| B].