proposition: Theorem hybrid_replace_c2_equiv : forall i x a, i < n -> evalDist (b <-$ (c2 a); hybrid <-$ computeHybrid n i a; ret (listReplace hybrid i b b)) x == evalDist (computeHybrid n i a) x.
proof: Proof. induction n; destruct i; intuition; try lia. unfold computeHybrid. unfold minus. unfold forNats. fold forNats. unfold compMap. fold compMap. comp_simp. inline_first. comp_skip. inline_first. comp_irr_l. inline_first. comp_skip. comp_simp. simpl. intuition. unfold computeHybrid. unfold minus. fold minus. unfold forNats. fold forNats. unfold compMap. fold compMap. inline_first. do 2 comp_at comp_inline leftc 1%nat. comp_swap_l. comp_skip. assert (evalDist (a1 <-$ (lsb' <-$ compMap B_EqDec (fun _ : nat => (c1 a)) (forNats i); ret x0 :: lsb'); a2 <-$ compMap B_EqDec (fun _ : nat => (c2 a)) (forNats (n0 - i)); ret a1 ++ a2) x == evalDist (ls <-$ (a1 <-$ compMap B_EqDec (fun _ : nat => (c1 a)) (forNats i); a2 <-$ compMap B_EqDec (fun _ : nat => (c2 a)) (forNats (n0 - i)); ret a1 ++ a2); ret (x0 :: ls)) x). inline_first. comp_skip. inline_first. comp_skip. comp_simp. rewrite app_comm_cons. intuition. rewrite H1. clear H1. eapply eqRat_trans. 2:{ comp_skip. eapply IHn0. lia. lia. eapply eqRat_refl. } unfold computeHybrid. inline_first. comp_skip. inline_first. comp_skip. inline_first. comp_skip. comp_simp. simpl. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid