proposition: Theorem compFold_perm : forall (A B : Set)(inv : B -> Prop)(ls1 ls2 : list A), Permutation ls1 ls2 -> forall (eqd : EqDec B) (c : B -> A -> Comp B) init x, (forall b a1 a2 x, In a1 ls1 -> In a2 ls2 -> inv b -> evalDist (b' <-$ c b a1; c b' a2) x == evalDist (b' <-$ c b a2; c b' a1) x) -> (forall a b b', In a ls1 -> inv b -> In b' (getSupport (c b a)) -> inv b') -> inv init -> evalDist (compFold _ c init ls1) x == evalDist (compFold _ c init ls2) x.
proof: Proof. induction 1; intuition. unfold compFold. fold compFold. comp_skip. eapply IHPermutation; intuition. eapply H1. simpl. right. eapply H4. eapply H5. trivial. eapply H1. simpl. left. eauto. eauto. trivial. unfold compFold. fold compFold. eapply (trans _ (evalDist (init'0 <-$ (init' <-$ c init y; c init' x); compFold eqd c init'0 l) x0)). inline_first. intuition. eapply trans. comp_skip. eapply eqRat_refl. inline_first. intuition. eapply trans. eapply IHPermutation1; intuition. eapply H1; intuition. eapply Permutation_in; eauto. eapply IHPermutation2; intuition. eapply H1; intuition. eapply Permutation_in. eapply Permutation_sym. eauto. trivial. eapply H2; eauto. eapply Permutation_in. eapply Permutation_sym. eauto. trivial. Qed.
imports: FCF.FCF Permutation