proposition: Theorem comp_spec_iso : forall (A B : Set){eqda : EqDec A}{eqdb : EqDec B}(c1 : Comp A)(c2 : Comp B)(f : A -> B)(f_inv : B -> A), (forall x : B, In x (getSupport c2) -> f (f_inv x) = x) -> (forall x : A, In x (getSupport c1) -> f_inv (f x) = x) -> (forall x : B, In x (getSupport c2) -> In (f_inv x) (getSupport c1)) -> (forall x : A, In x (getSupport c1) -> comp_spec (fun a b => a = (f x) <-> b = x) c2 c1) -> comp_spec (fun a b => f a = b) c1 c2.
proof: Proof. intuition. intuition. remember f_inv as f_inv2. exists (x <-$ c1; ret (x, f x)). intuition; subst. unfold marginal_l. dist_inline_first. rewrite <- evalDist_right_ident. dist_skip. dist_compute. unfold marginal_r. dist_inline_first. rewrite <- evalDist_right_ident. eapply (@distro_iso_eq _ _ _ _ f f_inv). intuition. intuition. intuition. intuition. rewrite evalDist_event_equiv. symmetry. rewrite evalDist_event_equiv. eapply comp_spec_impl_eq. eapply (@comp_spec_consequence _ _ _ _ _ _ eq). eapply comp_spec_event_equiv. eapply comp_spec_symm. eapply comp_spec_consequence. eapply H2. eauto. intuition. case_eq (eqb x b); intuition. rewrite eqb_leibniz in H5. subst. intuition. subst. repeat rewrite eqb_refl. intuition. case_eq (eqb (f x) a); intuition. rewrite eqb_leibniz in H4. subst. intuition. subst. repeat rewrite eqb_refl. intuition. rewrite H5. rewrite H4. intuition. intuition. subst. trivial. subst. trivial. intuition. dist_compute. repeat simp_in_support. trivial. Unshelve. intuition. intuition. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1