proposition: Lemma count_zero_iff: forall h (topkt: @Tuple h -> input) totup (r: UnConstrQueryStructure (PacketHistorySchema h)) (P: input -> bool) count, (forall t, totup (topkt t) = t) -> (forall inp, P inp = P (topkt (totup inp))) -> computes_to (Count (For (UnConstrQuery_In r Fin.F1 (fun t => Where (P (topkt t)) Return ())))) count -> ((0 <? count) <-> (exists inp, In_History totup r inp /\ P inp)).
proof: Proof. Transparent Query_For. Transparent Count. Transparent QueryResultComp. unfold Count, Query_For, Query_Where, Query_Return, UnConstrQuery_In. unfold QueryResultComp, FlattenCompList.flatten_CompList. intros h topkt totup r P count toinv Ptoinv Hcount. destruct Hcount as [l [Hcount Htmp]]. unfold In in *. inversion Htmp. rename H into Hlen. clear Htmp. destruct Hcount as [l' [Htmp Hperm]]. apply Pick_inv in Hperm. unfold In in *. destruct Htmp as [ltup [Hrel Hfold]]. apply Pick_inv in Hrel. unfold In in *. pose proof (permutation_length l' l Hperm) as Hpermlen. rewrite <- Hpermlen in *. clear Hperm. clear Hpermlen. clear l. split; intros H. - pose proof (fold_comp_list_length l' _ Hfold H) as Hlin0. destruct Hlin0 as [lin [Hlinm [lin' [Hll Hlinc]]]]. apply in_map_iff in Hlinm. destruct Hlinm as [x [Hpx Hlx]]. exists (topkt x). split. * red in Hrel. destruct Hrel as [l [Hmap [Heql Hdup]]]. red. rewrite <- Hmap in Hlx. apply in_map_iff in Hlx. destruct Hlx as [y [Hy1 Hy2]]. destruct y as [yidx yelem]. exists yidx. simpl in Hy1. subst x. apply Heql. rewrite toinv. apply Hy2. * subst lin. inversion Hll. destruct (P (topkt x)) eqn:Hpx. reflexivity. assert (Hle: lin' = []%list) by (apply H1; congruence). subst lin'. inversion Hlinc. - red in Hrel. destruct Hrel as [l [Hmap [Heql Hdup]]]. destruct H as [inp [Hinp Hpinp]]. red in Hinp. destruct Hinp as [idx Hinp]. apply Heql in Hinp. assert (Hinp': List.In (totup inp) ltup). { rewrite <- Hmap. apply in_map_iff. exists {| elementIndex := idx; indexedElement := (totup inp) |}. split. reflexivity. assumption. } pose (fun t => P (topkt t)) as P'. rewrite Ptoinv in Hpinp. apply (fold_comp_list_in _ P' ltup l' _ Hfold Hinp' Hpinp). Qed.
imports: Fiat.Narcissus.Examples.NetworkStack.IPv4Header Fiat.Narcissus.Examples.NetworkStack.TCP_Packet Bedrock.Word Coq.Arith.Arith Coq.Lists.List Fiat.QueryStructure.Automation.MasterPlan IndexedEnsembles Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTables Fiat.Narcissus.Examples.Guard.PacketFiltersLemmas Fiat.Narcissus.Examples.Guard.DropFields Coq.Sets.Ensembles