proposition: Lemma LessHistoryPreservesFilter: forall inp h totup topkt r_o r_n, LessHistoryRelation totup r_o r_n -> refine (@FilterMethod_UnConstr h topkt totup r_o inp) (FilterMethod_UnConstr topkt totup r_n inp).
proof: Proof. red; intros. unfold FilterMethod_UnConstr in *. unfold LessHistoryRelation in H. destruct H as [Hfin H]. destruct (cf_cond OutgoingRule inp) eqn:outrule; destruct (negb (cf_cond IncomingRule inp)) eqn:ninrule; simpl in *; try apply H0. inversion H0. destruct H1. computes_to_econstructor. destruct x eqn:truefalse. - instantiate (1 := x). computes_to_econstructor. unfold decides; simpl. destruct H1. destruct H1. exists x0. split. * apply (H x0). apply (OutgoingToImpliesOutgoing x0 (ipv4_source (in_ip4 inp))). assumption. assumption. * assumption. - computes_to_econstructor; unfold decides; simpl. unfold not; intros. destruct H1. destruct H3. destruct H1. exists x0. split. * apply (H x0). apply (OutgoingToImpliesOutgoing x0 (ipv4_source (in_ip4 inp))). assumption. assumption. * assumption. - 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