proposition: Lemma queensE n : queens n = queens_state_nondeter n.
proof: Proof. rewrite (getput_prepend (queens n)) /queens_state_nondeter; bind_ext => x. rewrite {1}/queens putpermsC; bind_ext => y. rewrite safe2E. set f := (do ok <- (do _ <- _; _); _ >> guard ok in RHS). rewrite (_ : f = do uds <- get; put (safe1 uds (place n y)).2 >> Ret (safe1 uds (place n y)).1 >> put x >> guard (safe1 uds (place n y)).1); last first. rewrite {}/f bindA; bind_ext => u. case: (safe1 _ _) => a b. rewrite 2!bindA bindretf bindA. by under eq_bind do rewrite bindretf. rewrite assertE -bindA; congr (_ >> _). rewrite -bindA. rewrite putgetput. rewrite 2!bindA. rewrite bindretf. rewrite -2!bindA. by rewrite 2!putput. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib