proposition: Lemma Fiat_Bedrock_Filters_Equivalence: forall (N : nat) (table : FiatWBag N) (key : W) (x9 : list TuplesF.tupl) (idx1: Fin.t N) (k1 := (Word.natToWord 32 (projT1 (Fin.to_nat idx1)))), BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> TuplesF.EnsembleIndexedListEquivalence (TuplesF.keepEq eq (Word.wzero _) (IndexedEnsemble_TupleToListW table) k1 key) x9 -> IndexedEnsembles.EnsembleIndexedListEquivalence (IndexedEnsembles.IndexedEnsemble_Intersection table (fun x0 : FiatWTuple N => ((if Word.weq match MakeWordHeading_allWords idx1 in _ = W return W with | eq_refl => GetAttributeRaw x0 idx1 end key then true else false) && true)%bool = true)) (map (ListWToTuple_Truncated N) x9).
proof: Proof. intros. apply EnsembleIndexedListEquivalence_TupleToListW. erewrite <- ListWToTuple_Truncated_map_keepEq by eassumption. rewrite TuplesF_EnsembleIndexedListEquivalence_EquivEnsembles; try eassumption. unfold IndexedEnsemble_TupleToListW, TuplesF.keepEq, Ensembles.Included, Ensembles.In, IndexedEnsembles.IndexedEnsemble_Intersection, Array.sel in *. rewrite Same_set_pointwise; repeat match goal with | _ => cleanup | _ => eassumption | _ => progress unfold RelatedIndexedTupleAndListW, TuplesF.tupl in * | [ |- exists _, _ ] => eexists | [ H: exists _, _ |- _ ] => destruct H | [ |- context[andb _ true] ] => rewrite Bool.andb_true_r | [ H: context[andb _ true] |- _ ] => rewrite Bool.andb_true_r in H | [ H: (if ?cond then true else false) = _ |- _ ] => destruct cond; try discriminate; [idtac] end. - setoid_rewrite H4. set (IndexedEnsembles.indexedElement x0). clear H0. unfold k1. rewrite nth_error_GetAttributeRaw; eauto using BinNat.N.lt_trans, BinNat_lt_Fin_to_nat. - unfold W, k1 in *; rewrite H3. unfold k1 in *; rewrite nth_error_GetAttributeRaw by eauto using BinNat.N.lt_trans, BinNat_lt_Fin_to_nat; simpl. destruct (Word.weq _ _); (reflexivity || exfalso; eauto). Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.BinNatUtils CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW Fiat.QueryStructure.Specification.Representation.Tuple Bedrock.Memory Coq.Lists.List CertifiedExtraction.Utils