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 A→ Type,
      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 A → Type,
      P nil →
      (∀ (x:A) (l:list A), P l → P (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 elt → A → Type.

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

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

    Definition Pl (l : list elt) (a : A) :=
      ∀ s, equivlistA _eq (elements s) l → P 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.

      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 : A → Type) (f : elt → A → A) (i : A) (s : set elt),
      P i → (∀ e a, e \In s → P a → P (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 _ Ha ⇒ Hstep e a H Ha).
  Qed.

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

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

    Hypothesis Hi : R i1 i2.
    Hypothesis Hstep : ∀ k a1 a2,
      k \In s → R a1 a2 → R (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.