proposition: Lemma Find_MatchingIndexesOK_InclA : forall (st : IndexSearchTermT) (MKey : KeyMapT) (MValues : ValuesMapT), (forall key indexes, MKeys.MapsTo key indexes MKey -> forall idx, List.In idx indexes -> exists item, MValues.MapsTo idx item MValues /\ InA E.eq key (projection item)) -> forall item idx, MValues.MapsTo idx item (Find_MatchingIndexes MKey st MValues) -> inclA E.eq st (projection item).
proof: Proof. induction st; simpl; unfold inclA; intros; intuition. - inversion H1. - case_eq (MKeys.find a MKey); intros; rewrite H2 in H0. + inversion H1; subst. * rewrite H4; pose proof (Find_MatchingIndexesOK_Subset _ _ _ H0) as H'. rewrite MValuesProperties.filter_iff in H'; intuition. apply MKeys.find_2 in H2. destruct (H _ _ H2 idx); intuition. destruct (in_dec eq_nat_dec idx l); simpl in *; congruence. rewrite <- (MoreMValuesFacts.BasicFacts.MapsTo_fun H7 H3); eauto. * destruct (E.eq_dec x a). rewrite e; pose proof (Find_MatchingIndexesOK_Subset _ _ _ H0) as H'. rewrite MValuesProperties.filter_iff in H'; intuition. apply MKeys.find_2 in H2. destruct (H _ _ H2 idx); intuition. destruct (in_dec eq_nat_dec idx l); simpl in *; congruence. rewrite <- (MoreMValuesFacts.BasicFacts.MapsTo_fun H7 H3); eauto. apply MKeys.find_2 in H2. apply (IHst _ _ H item idx); eauto. generalize H0. remember (fun (k : MValues.key) (_ : TItem) => bool_of_sumbool (in_dec eq_nat_dec k l)) as f. unfold not in f; setoid_rewrite <- Heqf. generalize MValues f; clear -projection; induction st; simpl; intros; eauto. match goal with | [ H : MValues.MapsTo _ _ _ |- _ ] => rewrite MValuesProperties.filter_iff in H; intuition end. destruct (MKeys.find a MKey); simpl in *. match goal with | [ H : MValues.MapsTo _ _ _ |- _ ] => setoid_rewrite Equal_filter_filter in H end. eapply (IHst _ f). setoid_rewrite Equal_filter_filter. eapply Equal_mapsto_iff; eauto. repeat f_equiv. repeat (apply functional_extensionality; intros). apply andb_comm. eauto. + apply MValues.empty_1 in H0; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.Peano_dec Coq.Structures.OrdersEx Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListInclusion