proposition: Lemma refine_QueryResultComp_body_Where_False {ResultT : Type} {heading} (body : @RawTuple heading -> Comp (list ResultT)) P R : (forall tup, In _ R tup -> ~ P (indexedElement tup)) -> FiniteEnsemble R -> refine (QueryResultComp R (fun tup => Where (P tup) (body tup))) (ret nil).
proof: Proof. intros; unfold QueryResultComp. destruct H0. refine pick val _; eauto. simplify with monad laws. rewrite refine_flatten_CompList_func' with (f' := fun _ => ret nil). apply flatten_CompList_nil'. intros; computes_to_econstructor; computes_to_inv; subst; intuition. unfold UnIndexedEnsembleListEquivalence in H0; destruct_ex; intuition; subst. apply in_map_iff in H1; destruct_ex; intuition; subst. apply H in H2; intuition. apply H0; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.SumType Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Bedrock.Word Bedrock.Memory