proposition: Lemma queensBodyE' xs : queensBody M xs = if xs is [::] then Ret [::] else select xs >>= (fun xys => get >>= (fun st => guard (queens_ok (queens_next st xys.1)) >> put (queens_next st xys.1) >> ((fmap (cons xys.1)) (queensBody M xys.2)))).
proof: Proof. case: xs => [|h t]. rewrite queensBodyE // hyloME //; exact: decr_size_select. rewrite {1}queensBodyE hyloME; last exact: decr_size_select. rewrite {-1}[h :: t]lock decr_size_select /bassert 2!bindA. rewrite (_ : nilp _ = false) //. bind_ext => -[x ys]. case: assertPn => /= ysht; last by rewrite !bindfailf. rewrite !bindretf /opdot_queens /opdot. bind_ext => st. rewrite !bindA; bind_ext; case. bind_ext; case. by rewrite queensBodyE. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib