proposition: Theorem compFold_repeat_spec : forall (C D: Set)(ls1 : list C)(ls2 : list D)(pre : C -> D -> Prop), list_pred pre ls1 ls2 -> forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(post : A -> B -> Prop)(c1 : C -> Comp A)(P1 : A -> bool)(c2 : D -> Comp B)(P2 : B -> bool) a b, post a b -> (forall a b, pre a b -> comp_spec post (c1 a) (c2 b)) -> (forall a b, post a b -> (P1 a = true <-> P2 b = true)) -> comp_spec post (compFold _ (fun acc v => if (P1 acc) then (ret acc) else (c1 v)) a ls1) (compFold _ (fun acc v => if (P2 acc) then (ret acc) else (c2 v)) b ls2).
proof: Proof. induction 1; intuition. simpl. eapply comp_spec_ret. trivial. simpl. case_eq (P1 a); intuition. assert (P2 b = true). eapply H3; eauto. rewrite H5. prog_simp. eauto. case_eq (P2 b); intuition. assert (P1 a = true). eapply H3; intuition; eauto. congruence. eapply comp_spec_seq; intuition. Qed.
imports: FCF.FCF