# Library Ergo.FoldProps

Require Import Sets.
Require SetEqProperties. Module EProps := SetEqProperties.
Require SetProperties. Module Props := SetProperties.
Require Import SetoidList.

Set Implicit Arguments.
Unset Strict Implicit.
Generalizable All Variables.
Open Scope set_scope.

Section Reverse_Induction.
Variable A : Type.

Lemma rev_list_rec :
P:list AType,
P nil
( (a:A) (l:list A), P (rev l) → P (rev (a :: l))) →
l:list A, P (rev l).
Proof.
induction l; auto.
Qed.

Theorem rev_rec :
P:list AType,
P nil
( (x:A) (l:list A), P lP (app l (x :: nil))) →
l:list A, P l.
Proof.
intros.
generalize (rev_involutive l).
intros E; rewrite <- E.
apply rev_list_rec.
auto.
simpl in |- ×.
intros.
apply (X0 a (rev l0)).
auto.
Qed.
End Reverse_Induction.

Module SetFoldInd.
Import SetInterface.
Section fold_induction.
Context `{FSetSpecs : @SetInterface.FSetSpecs elt elt_OT F}.
Variable A : Type.
Variable P : set eltAType.

Variable f : eltAA.
Variable i : A.
Variable s : set elt.

Hypothesis P_m : s s' a, s [=] s'P s aP s' a.
Hypothesis Hi : P {} i.
Hypothesis Hstep : e a s',
e \In s¬e \In s'P s' aP {e; s'} (f e a).

Definition Pl (l : list elt) (a : A) :=
s, equivlistA _eq (elements s) lP s a.
Lemma Hli : Pl nil i.
Proof.
intros s' Hs'.
assert (Hemp : Empty s'). intros e He.
rewrite elements_iff in He.
rewrite (Hs' e) in He; inversion He.
assert (Hemp' := Props.empty_is_empty_1 Hemp).
exact (P_m (symmetry Hemp') Hi).
Qed.

Fixpoint set_of_list (l : list elt) : set elt :=
match l with
| nil{}
| a::q{a; set_of_list q}
end.
Remark sofl_1 :
l, equivlistA _eq (elements (set_of_list l)) l.
Proof.
induction l; simpl; intro e.
rewrite Props.elements_empty; reflexivity.
rewrite <- elements_iff; rewrite add_iff; rewrite elements_iff.
split; intro H.
destruct H; [constructor | constructor 2; rewrite <- (IHl e)]; auto.
inversion H; [left | right]; auto.
rewrite (IHl e); auto.
Qed.

Lemma fold_ind_aux : Pl (elements s) (fold f s i).
Proof.
rewrite fold_1.
assert ( e, InA _eq e (elements s) → e \In s).
intros; auto with set.
assert (H2 := elements_3w s).
revert H2 H; pattern (elements s); apply rev_rec.
intros; simpl; exact Hli.
intros x L IH IHdup IHin; rewrite fold_left_app; simpl.
intros s' Hs'.
cut ({x; set_of_list L} [=] s'); [intro Heq |].
assert (NoDupA _eq (x::(app L nil))).
refine (NoDupA_swap _ IHdup); intuition.
refine (P_m Heq _); apply Hstep.
apply IHin; rewrite InA_app_iff; intuition.
rewrite elements_iff.
rewrite (sofl_1 L x); inversion H; rewrite <- app_nil_end in H2; auto.
apply IH.
inversion H; rewrite <- app_nil_end in H3; auto.
intros e He; apply IHin.
rewrite InA_alt in He |- *; destruct He as [y [Hy1 Hy2]].
y; intuition.
apply sofl_1.
• cut : (K.add x (set_of_list L)) = s'
intro l; rewrite add_iff; split; intro Hl.
apply elements_2; rewrite (Hs' l); destruct Hl.
rewrite InA_alt; x; intuition.
assert (X:= (proj1 (sofl_1 L l)) (elements_1 H)).
rewrite InA_alt in X |- *; destruct X; x0; intuition.
rewrite elements_iff in Hl; rewrite (Hs' l) in Hl.
destruct (InA_app _ Hl); [right | left].
apply elements_2; rewrite (sofl_1 L l); auto.
inversion H; try inversion H1; intuition.
Qed.

Theorem fold_ind : P s (fold f s i).
Proof.
apply fold_ind_aux.
induction (elements s); constructor; intuition.
Qed.
End fold_induction.
Corollary fold_ind2 `{FSetSpecs : @SetInterface.FSetSpecs elt elt_OT F} :
(A : Type) (P : AType) (f : eltAA) (i : A) (s : set elt),
P i → ( e a, e \In sP aP (f e a)) →
P (fold f s i).
Proof.
refine (fun A P f i s Hi Hstep
@fold_ind elt elt_OT F FSetSpecs A (fun _P) f i s _ Hi _).
trivial.
exact (fun e a _ H _ HaHstep e a H Ha).
Qed.

Section fold_relation.
Context `{FSetSpecs : @SetInterface.FSetSpecs elt elt_OT F}.
Variables A Acc1 Acc2 : Type.
Variable R : Acc1Acc2Type.

Variable f1 : eltAcc1Acc1.
Variable f2 : eltAcc2Acc2.
Variable i1 : Acc1.
Variable i2 : Acc2.
Variable s : set elt.

Hypothesis Hi : R i1 i2.
Hypothesis Hstep : k a1 a2,
k \In sR a1 a2R (f1 k a1) (f2 k a2).

Lemma fold_rel : R (fold f1 s i1) (fold f2 s i2).
Proof.
assert (Hin : k, InA _eq k (elements s) → k \In s).
intros; apply elements_2; auto.
revert Hin; do 2 rewrite fold_1; pattern (elements s).
apply rev_rec; simpl; auto.
intros k L IH Hin; do 2 rewrite fold_left_app; simpl; apply Hstep.
apply Hin; rewrite <- InA_rev; auto; rewrite rev_unit; constructor.
reflexivity.
apply IH; intros k0 Hk0; apply Hin.
rewrite InA_alt in Hk0 |- *; destruct Hk0 as [y [Hy1 Hy2]].
y; intuition.
Qed.
End fold_relation.

End SetFoldInd.