proposition: Lemma refine_Query_In_Where_Const_neq {qs_schema} {ResultT} {A} {_ : @Query_eq A} : forall Index (r_o : UnConstrQueryStructure qs_schema) (r_n : IndexedQueryStructure qs_schema Index) idx (body : _ -> Comp (list ResultT)) Q a a', DelegateToBag_AbsR r_o r_n -> refine For (UnConstrQuery_In r_o idx (fun tup : RawTuple => Where (a <> a' /\ Q tup) (body tup) )) (If A_eq_dec a a' Then (ret [ ]) Else For (UnConstrQuery_In r_o idx (fun tup : RawTuple => Where (Q tup) (body tup) )) ).
proof: Proof. Admitted. Corollary refine_Count_Query_In_Where_Const_neq {qs_schema} {ResultT} {A} {_ : @Query_eq A} : forall Index (r_o : UnConstrQueryStructure qs_schema) (r_n : IndexedQueryStructure qs_schema Index) idx (body : _ -> Comp (list ResultT)) Q a a', DelegateToBag_AbsR r_o r_n -> refine (Count For (UnConstrQuery_In r_o idx (fun tup : RawTuple => Where (a <> a' /\ Q tup) (body tup) ))) (If A_eq_dec a a' Then (ret 0) Else (Count For (UnConstrQuery_In r_o idx (fun tup : RawTuple => Where (Q tup) (body tup) )))). Proof. intros; rewrite refine_Query_In_Where_Const_neq; eauto. find_if_inside; simpl; eauto. rewrite refine_Count; simplify with monad laws; reflexivity. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.Tactics.CacheStringConstant Fiat.Computation.Decidable Fiat.Computation.IfDec Fiat.Computation.FoldComp Fiat.Computation.FueledFix Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Automation.MasterPlan Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindStringPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Bedrock.Word Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Narcissus.Stores.Cache Fiat.Narcissus.Stores.DomainNameStore Fiat.Narcissus.BinLib.AlignedDomainName Fiat.Narcissus.BinLib.AlignedByteString Fiat.Examples.DnsServer.DecomposeSumField Fiat.Examples.DnsServer.SimpleDnsLemmas Fiat.Examples.DnsServer.DnsAutomation Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema