proposition: Lemma fold_comp_list_in: forall (T: Type) (P: T -> bool) (ltup: list T) l inp, fold_right (fun b a : Comp (list ()) => l <- b; l' <- a; ret (l ++ l')%list) (ret []) (map (fun t : T => {l : list () | (P t -> ret [()] ↝ l) /\ (~ P t -> l = [])}) ltup) l -> List.In inp ltup -> P inp -> 0 <? Datatypes.length l.
proof: Proof. intros T P. induction ltup. - intros; auto. - intros l inp Hf Hin Hp. cbn in Hf. destruct Hf as [x [Hx [y [Hy Happ]]]]. unfold In in *. inversion Happ. destruct Hin as [Hin | Hin]. * subst inp. inversion Hx. apply H0 in Hp. inversion Hp. auto. * pose proof (IHltup y inp Hy Hin Hp) as Hind. rewrite app_length. apply Nat.ltb_lt; apply Nat.lt_lt_add_l; apply Nat.ltb_lt; assumption. 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