proposition: Theorem oc_comp_invariant : forall (A B C : Set)(c : OracleComp A B C)(S : Set)(P : S -> Prop) (eqds : EqDec S) (o : S -> A -> Comp (B * S))(s : S), (forall a b c d, In (a, b) (getSupport (o c d)) -> P c -> P b) -> P s -> forall a b, In (a, b) (getSupport (c _ _ o s)) -> P b.
proof: Proof. Opaque getSupport. induction c; intuition; simpl in *. eapply H; eauto. Transparent getSupport. repeat simp_in_support. destruct x. simpl in *. specialize (IHc (S * S0) (fun x => P (snd x)) _ (fun (x : S * S0) (y : A) => p <-$ (o (fst x) y) S0 eqds o0 (snd x); ret (fst (fst p), (snd (fst p), snd p))) (s, s0))%type. eapply IHc; intros. 3:{ eapply H3. } repeat simp_in_support. simpl. destruct c1. destruct x. eapply H. eapply H0. eapply H4. eapply H5. trivial. repeat simp_in_support. trivial. repeat simp_in_support. destruct x. eapply H. eapply H0. eapply IHc. eapply H0. eapply H1. eauto. eauto. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms