From Undecidability.Shared.Libs.PSL Require Import BaseLists Dupfree.
(* *** Power lists *)
Section Power.
Variable X : Type.
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]; cbn; 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; cbn; auto.
Qed.
End Power.
Section PowerRep.
Variable X : eqType.
Implicit Types A U : list X.
Definition rep (A U : list X) : list X :=
filter (fun x => Dec (x el A)) U.
Lemma rep_cons A x U :
x el A -> rep A (x::U) = x :: rep A U.
Proof.
intros H. apply filter_fst. auto.
Qed.
Lemma rep_cons' A x U :
~ x el A -> rep A (x::U) = rep A U.
Proof.
intros H. apply filter_fst'. auto.
Qed.
Lemma rep_cons_eq x A U :
~ x el U -> rep (x::A) U = rep A U.
Proof.
intros D. apply filter_pq_eq. intros y E.
apply Dec_reflect_eq. split.
- intros [<-|F]; tauto.
- auto.
Qed.
Lemma rep_power A U :
rep A U el power U.
Proof.
revert A; induction U as [|x U]; intros A.
- cbn; auto.
- decide (x el A) as [H|H].
+ rewrite (rep_cons _ H). cbn. auto using in_map.
+ rewrite (rep_cons' _ H). cbn. auto.
Qed.
Lemma rep_incl A U :
rep A U <<= A.
Proof.
intros x. unfold rep. rewrite in_filter_iff, Dec_reflect.
intuition.
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.
intros E; rewrite !Dec_reflect; 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. intros x E.
apply Dec_reflect_eq. auto.
Qed.
Lemma rep_eq A B U :
A === B -> rep A U = rep B U.
Proof.
intros D. apply filter_pq_eq. intros x E.
apply Dec_reflect_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. apply Dec_reflect_eq. 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]; cbn.
- 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']; cbn; 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.
- cbn in G. apply in_app_iff in G as [G|G].
+ rewrite rep_cons'. now auto.
contradict E. apply (power_incl G), E.
+ apply in_map_iff in G as [A' [<- H]].
specialize (IHF _ H).
rewrite rep_cons. 2:now auto.
rewrite rep_cons_eq. now rewrite IHF. exact E.
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.
(* *** Power lists *)
Section Power.
Variable X : Type.
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]; cbn; 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; cbn; auto.
Qed.
End Power.
Section PowerRep.
Variable X : eqType.
Implicit Types A U : list X.
Definition rep (A U : list X) : list X :=
filter (fun x => Dec (x el A)) U.
Lemma rep_cons A x U :
x el A -> rep A (x::U) = x :: rep A U.
Proof.
intros H. apply filter_fst. auto.
Qed.
Lemma rep_cons' A x U :
~ x el A -> rep A (x::U) = rep A U.
Proof.
intros H. apply filter_fst'. auto.
Qed.
Lemma rep_cons_eq x A U :
~ x el U -> rep (x::A) U = rep A U.
Proof.
intros D. apply filter_pq_eq. intros y E.
apply Dec_reflect_eq. split.
- intros [<-|F]; tauto.
- auto.
Qed.
Lemma rep_power A U :
rep A U el power U.
Proof.
revert A; induction U as [|x U]; intros A.
- cbn; auto.
- decide (x el A) as [H|H].
+ rewrite (rep_cons _ H). cbn. auto using in_map.
+ rewrite (rep_cons' _ H). cbn. auto.
Qed.
Lemma rep_incl A U :
rep A U <<= A.
Proof.
intros x. unfold rep. rewrite in_filter_iff, Dec_reflect.
intuition.
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.
intros E; rewrite !Dec_reflect; 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. intros x E.
apply Dec_reflect_eq. auto.
Qed.
Lemma rep_eq A B U :
A === B -> rep A U = rep B U.
Proof.
intros D. apply filter_pq_eq. intros x E.
apply Dec_reflect_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. apply Dec_reflect_eq. 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]; cbn.
- 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']; cbn; 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.
- cbn in G. apply in_app_iff in G as [G|G].
+ rewrite rep_cons'. now auto.
contradict E. apply (power_incl G), E.
+ apply in_map_iff in G as [A' [<- H]].
specialize (IHF _ H).
rewrite rep_cons. 2:now auto.
rewrite rep_cons_eq. now rewrite IHF. exact E.
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.