Require Export Prelim.
Export ListNotations.
Notation "x 'el' A" := (In x A) (at level 70).
Notation "A <<= B" := (incl A B) (at level 70).
Notation "| A |" := (length A) (at level 65).
Definition equi X (A B : list X) : Prop := incl A B /\ incl B A.
Notation "A === B" := (equi A B) (at level 70).
Hint Unfold equi.
Hint Extern 4 =>
match goal with
|[ H: ?x el nil |- _ ] => destruct H
end.
(*** Lists *)
(* Register additional simplification rules with autorewrite / simpl_list *)
(* Print Rewrite HintDb 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.
Proof.
intros B.
assert (C: |x::A| <> |A|) by (cbn; omega).
apply C. now rewrite B.
Qed.
(**** Decisions for lists *)
Instance list_in_dec X (x : X) (A : list X) :
eq_dec X -> dec (x el A).
Proof.
intros D. apply in_dec. exact D.
Qed.
(* Certifying find *)
Lemma cfind 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.
destruct (find (fun x => Dec (p x)) A) eqn:E.
- apply find_some in E. firstorder.
- right. intros. eapply find_none in E; eauto.
Qed.
Arguments cfind {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 (find (fun x => Dec (~ p x)) A) eqn:Eq.
- apply find_some in Eq as [H1 H0 %Dec_true]; right; auto.
- left. intros x E. apply find_none with (x := x) in Eq. apply dec_DN; auto. auto.
Qed.
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 (find (fun x => Dec (p x)) A) eqn:Eq. (* New: eta expansion needed *)
- apply find_some in Eq as [H0 H1 %Dec_true]. firstorder. (* New: Need firstorder here *)
- right. intros [x [E F]]. apply find_none with (x := x) in Eq; auto. eauto. (* New: Why can't auto solve this? *)
Qed.
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 (find (fun x => Dec (p x)) A) eqn:Eq.
+ apply find_some in Eq as [? ?%Dec_true]. eauto.
+ exfalso. apply E. intros. apply find_none with (x := x) in Eq; eauto.
Qed.
Lemma list_exists_not_incl (X: eqType) (A B : list X) :
~ A <<= B -> exists x, x el A /\ ~ x el B.
Proof.
intros 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 (cfind A p) as [[x [F G]]|F].
- eauto.
- exfalso. destruct E as [x [G H]]. apply (F x); auto.
Qed.
(**** 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) (A B: list X).
Lemma in_sing x y :
x el [y] -> x = y.
Proof.
cbn. intros [[]|[]]. reflexivity.
Qed.
Lemma in_cons_neq x y A :
x el y::A -> x <> y -> x el A.
Proof.
cbn. 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.
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; cbn; 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; cbn.
- 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.
Lemma in_concat_iff A l (a:A) : a el concat l <-> exists l', a el l' /\ l' el l.
Proof.
induction l; cbn.
- intuition. now destruct H.
- rewrite in_app_iff, IHl. firstorder subst. auto. (* TODO: find something faster than firstorder subst *)
Qed.
Export ListNotations.
Notation "x 'el' A" := (In x A) (at level 70).
Notation "A <<= B" := (incl A B) (at level 70).
Notation "| A |" := (length A) (at level 65).
Definition equi X (A B : list X) : Prop := incl A B /\ incl B A.
Notation "A === B" := (equi A B) (at level 70).
Hint Unfold equi.
Hint Extern 4 =>
match goal with
|[ H: ?x el nil |- _ ] => destruct H
end.
(*** Lists *)
(* Register additional simplification rules with autorewrite / simpl_list *)
(* Print Rewrite HintDb 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.
Proof.
intros B.
assert (C: |x::A| <> |A|) by (cbn; omega).
apply C. now rewrite B.
Qed.
(**** Decisions for lists *)
Instance list_in_dec X (x : X) (A : list X) :
eq_dec X -> dec (x el A).
Proof.
intros D. apply in_dec. exact D.
Qed.
(* Certifying find *)
Lemma cfind 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.
destruct (find (fun x => Dec (p x)) A) eqn:E.
- apply find_some in E. firstorder.
- right. intros. eapply find_none in E; eauto.
Qed.
Arguments cfind {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 (find (fun x => Dec (~ p x)) A) eqn:Eq.
- apply find_some in Eq as [H1 H0 %Dec_true]; right; auto.
- left. intros x E. apply find_none with (x := x) in Eq. apply dec_DN; auto. auto.
Qed.
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 (find (fun x => Dec (p x)) A) eqn:Eq. (* New: eta expansion needed *)
- apply find_some in Eq as [H0 H1 %Dec_true]. firstorder. (* New: Need firstorder here *)
- right. intros [x [E F]]. apply find_none with (x := x) in Eq; auto. eauto. (* New: Why can't auto solve this? *)
Qed.
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 (find (fun x => Dec (p x)) A) eqn:Eq.
+ apply find_some in Eq as [? ?%Dec_true]. eauto.
+ exfalso. apply E. intros. apply find_none with (x := x) in Eq; eauto.
Qed.
Lemma list_exists_not_incl (X: eqType) (A B : list X) :
~ A <<= B -> exists x, x el A /\ ~ x el B.
Proof.
intros 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 (cfind A p) as [[x [F G]]|F].
- eauto.
- exfalso. destruct E as [x [G H]]. apply (F x); auto.
Qed.
(**** 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) (A B: list X).
Lemma in_sing x y :
x el [y] -> x = y.
Proof.
cbn. intros [[]|[]]. reflexivity.
Qed.
Lemma in_cons_neq x y A :
x el y::A -> x <> y -> x el A.
Proof.
cbn. 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.
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; cbn; 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; cbn.
- 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.
Lemma in_concat_iff A l (a:A) : a el concat l <-> exists l', a el l' /\ l' el l.
Proof.
induction l; cbn.
- intuition. now destruct H.
- rewrite in_app_iff, IHl. firstorder subst. auto. (* TODO: find something faster than firstorder subst *)
Qed.