proposition: Lemma UnConstrPreservesFilterMethod: forall h topkt totup r_o r_n inp res, DropQSConstraints_AbsR r_o r_n -> computes_to (@FilterMethod h topkt totup r_o inp) res <-> computes_to (FilterMethod_UnConstr topkt totup r_n inp) res.
proof: Proof. intros. unfold FilterMethod, FilterMethod_UnConstr in *. destruct (OutgoingRule.(cf_cond) inp) eqn:out. reflexivity. destruct (negb (IncomingRule.(cf_cond) inp)) eqn:inc. reflexivity. split; intros; apply Bind_inv in H0; destruct H0 as [b [Hbin Hbres]]; unfold DropQSConstraints_AbsR in H; rewrite <- H in *; computes_to_econstructor; unfold In_History, In_History_Constr; [ change (GetUnConstrRelationBnd (DropQSConstraints r_o) ``"History") with (GetUnConstrRelation (DropQSConstraints r_o) Fin.F1); rewrite GetRelDropConstraints; apply Hbin | apply Hbres | change (GetRelationBnd r_o ``"History") with (GetRelation r_o Fin.F1); rewrite <- GetRelDropConstraints; apply Hbin | apply Hbres]. 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