proposition: Lemma fold_comp_list_length: forall l l', fold_right (fun b a : Comp (list ()) => l <- b; l' <- a; ret (l ++ l')%list) (ret []) l' l -> 0 <? Datatypes.length l -> exists lin, List.In lin l' /\ (exists lin', lin lin' /\ 0 <? Datatypes.length lin').
proof: Proof. intros l l'. generalize dependent l. induction l'. - simpl. intros. inversion H. subst l. inversion H0. - simpl. intros. destruct H as [l1 [Hl1 Hl]]. red in Hl1. red in Hl. destruct Hl as [l2 [Hl2 Hl]]. red in Hl2. red in Hl. inversion Hl. destruct (0 <? Datatypes.length l2) eqn:Hlen2. * pose proof (IHl' l2 Hl2 Hlen2) as IH. destruct IH as [lin [Hlin1 Hlin2]]. exists lin. split. right; assumption. assumption. * apply Nat.ltb_ge in Hlen2. inversion Hlen2. rewrite <- H in H0. rewrite app_length in H0. rewrite H2 in H0. rewrite Nat.add_0_r in H0. exists a. split. left; reflexivity. exists l1. split. assumption. rewrite H2. apply H0. 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