proposition: Theorem oc_comp_spec_eq_until_bad : forall (A B C : Set)(c : OracleComp A B C), well_formed_oc c -> forall (eqdb : EqDec B) (eqdc : EqDec C)(S1 S2 : Set)(o1 : S1 -> A -> Comp (B * S1))(o2 : S2 -> A -> Comp (B * S2)) eqds1 eqds2 (bad1 : S1 -> bool)(bad2 : S2 -> bool)(inv : S1 -> S2 -> Prop), (forall a b, bad1 a = true -> well_formed_comp (o1 a b)) -> (forall a b, bad2 a = true -> well_formed_comp (o2 a b)) -> (forall x1 x2 a, inv x1 x2 -> bad1 x1 = bad2 x2 -> comp_spec (fun y1 y2 => (bad1 (snd y1) = bad2 (snd y2)) /\ (bad1 (snd y1) = false -> (inv (snd y1) (snd y2) /\ fst y1 = fst y2))) (o1 x1 a) (o2 x2 a)) -> (forall a b c d, bad1 c = true -> In (a, b) (getSupport (o1 c d)) -> bad1 b = true) -> (forall a b c d, bad2 c = true -> In (a, b) (getSupport (o2 c d)) -> bad2 b = true) -> ((forall s1 s2, inv s1 s2 -> bad1 s1 = bad2 s2 -> comp_spec (fun y1 y2 => (bad1 (snd y1) = bad2 (snd y2)) /\ (bad1 (snd y1) = false -> inv (snd y1) (snd y2) /\ (fst y1 = fst y2))) (c _ eqds1 o1 s1) (c _ eqds2 o2 s2))).
proof: Proof. induction 1; intuition; simpl in *. eapply (@comp_spec_consequence _ _ (@pair_EqDec B S1 eqdb eqds1) _ (@pair_EqDec B S2 eqdb eqds2)). eapply H1; intuition. intuition. assert (EqDec C). eapply EqDec_pair_l; eauto. assert C. eapply oc_base_exists; eauto. eapply (fun a => fst (oc_base_exists (o s a) (fun a' => fst (comp_base_exists (o1 s1 a'))))). eapply (@comp_spec_seq _ _ (fun x y => (bad1 (snd (snd x)) = bad2 (snd (snd y))) /\ (bad1 (snd (snd x)) = false -> (fst (snd x) = fst (snd y) /\ fst x = fst y /\ inv (snd (snd x)) (snd (snd y)))))). intuition. intuition. eapply comp_spec_consequence. eapply (@IHwell_formed_oc _ _ (S * S1) (S * S2) _ _ _ _ (fun a => bad1 (snd a)) (fun a => bad2 (snd a)) (fun a b => bad1 (snd a) = false -> (inv (snd a) (snd b) /\ fst a = fst b)))%type. intuition. simpl in *. wftac. eapply oc_comp_wf_inv; intuition. eapply H2. eapply H12. intuition. eapply H5; intuition. eauto. eauto. trivial. intuition. wftac. simpl in *. eapply oc_comp_wf_inv; intuition. eapply H3. eapply H12. intuition. eapply H6; intuition. eauto. eauto. trivial. intuition. simpl in *. case_eq (bad1 b); intuition. eapply comp_spec_irr_l; intuition. eapply oc_comp_wf_inv; eauto. eapply H2. intuition; simpl. eapply H5. eauto. eauto. trivial. eapply comp_spec_irr_r; intuition. eapply oc_comp_wf_inv; eauto. eapply H3. intuition; simpl. eapply H6. eauto. eauto. simpl. rewrite <- H12. trivial. eapply comp_spec_ret; simpl in *; intuition. destruct a2; simpl in *. assert (bad1 s0 = true). eapply (oc_comp_invariant_f). intuition. eapply H5; eauto. eauto. eauto. destruct b1. simpl in *. rewrite H16. symmetry. eapply (@oc_comp_invariant_f). intuition. eapply H6; eauto. eauto. eauto. destruct a2. simpl in *. assert (bad1 s0 = true). eapply (@oc_comp_invariant_f). intuition. eapply H5; eauto. eauto. eauto. congruence. destruct a2; simpl in *. assert (bad1 s0 = true). eapply (@oc_comp_invariant_f). intuition. eapply H5; eauto. eauto. eauto. congruence. destruct a2; simpl in *. assert (bad1 s0 = true). eapply (@oc_comp_invariant_f). intuition. eapply H5; eauto. eauto. eauto. congruence. subst. assert B. assert (B * S). eapply oc_base_exists. eapply o; intuition. intuition. assert (B' * S1). eapply comp_base_exists. eapply o1; intuition. intuition. intuition. eapply comp_spec_seq. intuition. intuition. eapply H1; intuition. intuition. intuition. intuition. eapply comp_spec_ret. simpl in *; intuition. destruct b3. destruct p. simpl in *. pairInv. trivial. destruct b3. simpl in *. subst. trivial. intuition. repeat simp_in_support. simpl in *. destruct x; simpl in *. eapply oc_comp_invariant_f; intuition. eapply H5; eauto. eauto. eauto. intuition. repeat simp_in_support. simpl in *. destruct x; simpl in *. eapply oc_comp_invariant_f; intuition. eapply H6; eauto. eauto. eauto. intuition. intuition. intuition. intuition. eapply comp_spec_ret. simpl in *; intuition. subst. intuition. assert C. eapply comp_base_exists; eauto. eapply comp_spec_seq; intuition. eapply comp_spec_eq_refl. subst. eapply comp_spec_ret. simpl in *; intuition. assert (A -> B). intuition. eapply (comp_base_exists (o1 s1 H9)). assert C. eapply oc_base_exists. eauto. intuition. assert C'. eapply oc_base_exists. eapply f. eapply oc_base_exists; eauto. intuition. assert (EqDec C). eapply oc_EqDec. eauto. intuition. intuition. eapply comp_spec_seq; intuition. eapply (@IHwell_formed_oc _ _ _ _ _ _ _ _ bad1 bad2 inv). eauto. eauto. intuition. intuition. intuition. trivial. trivial. intuition. destruct b0. simpl in *. case_eq (bad1 b); intuition. eapply comp_spec_eq_trans_l. eapply comp_spec_eq_symm. eapply comp_spec_right_ident. eapply comp_spec_eq_trans_r. 2:{ eapply comp_spec_right_ident. } eapply comp_spec_irr_l; intuition. eapply oc_comp_wf_inv; eauto. intuition. eapply H2; intuition. eapply H15. intuition. eapply H5; intuition. eauto. eauto. trivial. eapply comp_spec_irr_r; intuition. eapply oc_comp_wf_inv; eauto. intuition. eapply H3; intuition. eapply H19. intuition. eapply H6; intuition. eauto. eauto. simpl. rewrite <- H17. trivial. eapply comp_spec_ret. simpl in *; intuition. destruct a. destruct b0; simpl in *. assert (bad1 s0 = true). eapply (oc_comp_invariant_f (f a0) bad1); intuition. eapply H5. eapply H21. eapply H20. eapply H16. eapply H15. rewrite H20. symmetry. assert (bad2 s = true). rewrite <- H17. trivial. eapply (oc_comp_invariant_f (f c0) bad2); intuition. eapply H6. eapply H23. eapply H22. eapply H21. eapply H19. destruct a; simpl in *. destruct b0; simpl in *. assert (bad1 s0 = true). eapply oc_comp_invariant_f. intuition. eapply H5. eapply H22. eapply H21. eapply H16. eapply H15. congruence. destruct a; simpl in *. destruct b0; simpl in *. assert (bad1 s0 = true). eapply oc_comp_invariant_f. intuition. eapply H5. eapply H22. eapply H21. eapply H16. eapply H15. congruence. subst. eapply H1; intuition. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1