proposition: Theorem evalDet_bind_assoc : forall (A : Set)(c1 : Comp A)(B C : Set)(c2 : A -> Comp B)(c3 : B -> Comp C), evalDet_equiv (Bind (Bind c1 c2) c3) (Bind c1 (fun a => (Bind (c2 a) c3))).
proof: Proof. intuition. unfold evalDet_equiv. intuition. inversion H; clear H; subst. Ltac evalDet_tac := match goal with | [H1 : evalDet_steps ?x (cs_done ?a1 ?s1), H2 : evalDet_steps ?x (@cs_eof _) |- _ ] => exfalso; eauto using evalDet_steps_done_eof_func; intuition | [H : evalDet_steps (cs_more (Bind _ _) _) (cs_done _ _) |- _ ] => apply evalDet_steps_bind_done_inv in H | [H : evalDet_steps (cs_more (Bind _ _) _) (@cs_eof _) |- _ ] => apply evalDet_steps_bind_eof_inv in H; intuition | [H : exists _ : _, _ |- _ ] => destruct H; intuition | [H1 : evalDet_steps ?x (cs_done ?a1 ?s1), H2 : evalDet_steps ?x (cs_done ?a2 ?s2) |- _ ] => assert (a1 = a2 /\ s1 = s2); eauto using evalDet_steps_done_func; intuition; subst; clear H1; eauto end. repeat evalDet_tac. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eauto. repeat evalDet_tac. econstructor. eapply evalDet_bind_eof; eauto. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eapply evalDet_bind_eof; eauto. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eauto. inversion H; clear H; subst. repeat evalDet_tac. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eauto. eauto. repeat evalDet_tac. econstructor. eapply evalDet_steps_trans. eapply evalDet_bind_eof; eauto. eapply evalDet_bind_eof; eauto. econstructor. econstructor. eapply evalDet_bind_eof. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eauto. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eauto. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia