proposition: Lemma cacheGetDNPointer_pf : forall (ce : CacheFormat) (cd : CacheDecode) (p : string) (q : pointerT), Equiv ce cd -> (association_list_find_first (snd cd) q = Some p <-> List.In q (association_list_find_all (snd ce) p)).
proof: Proof. intros [? ?] [? ?] ? ?; simpl; intuition eauto; subst. - subst; induction a0; simpl in *; try congruence. destruct a; simpl in *; find_if_inside; subst. + inversion H2; subst; intros. find_if_inside; subst; simpl; eauto. + inversion H2; subst; intros. find_if_inside; subst; simpl; eauto; congruence. - subst; induction a0; simpl in *; intuition. destruct a; simpl in *; find_if_inside. + inversion H2; subst; intros. find_if_inside; subst; simpl; eauto; try congruence. apply IHa0 in H1; eauto. exfalso; apply H3; revert H1; clear. induction a0; simpl; intros; try congruence. destruct a; find_if_inside; injections; auto. + inversion H2; subst; intros. find_if_inside; subst; simpl; eauto; try congruence. simpl in H1; intuition eauto; subst. congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.DNSPacket Bedrock.Word