proposition: Lemma refine_For_In_Empty : forall ResultT MySchema R bod, refine (Query_For (@UnConstrQuery_In ResultT _ (DropQSConstraints (QSEmptySpec MySchema)) R bod)) (ret []).
proof: Proof. intros; rewrite refine_For. unfold UnConstrQuery_In, QueryResultComp; simplify with monad laws. unfold In, DropQSConstraints, GetUnConstrRelation in *. rewrite <- ith_imap2. unfold QSEmptySpec; simpl rawRels. rewrite Build_EmptyRelation_IsEmpty; simpl. rewrite refine_pick_val with (A := list RawTuple) (a := []). - unfold FlattenCompList.flatten_CompList; simplify with monad laws. simpl; simplify with monad laws. rewrite refine_pick_val with (A := list ResultT) (a := []); reflexivity. - eexists []; simpl; unfold In; intuition econstructor. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common.ilist2 Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Update Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements