proposition: Lemma EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv: forall (n : nat) (lst : list (FiatWTuple n)) (ens : FiatWBag n), TuplesF.EnsembleIndexedListEquivalence (IndexedEnsemble_TupleToListW ens) (map TupleToListW lst) -> IndexedEnsembles.UnIndexedEnsembleListEquivalence ens lst.
proof: Proof. repeat match goal with | _ => cleanup | _ => solve [constructor] | _ => progress destruct_conjs | _ => progress map2_t | [ H: context[IndexedEnsemble_TupleToListW ?ens _] |- context [?ens ?element] ] => specialize (H (TupleToListW_indexed element)) | [ H: context[IndexedEnsemble_TupleToListW ?ens _], H': ?ens ?element |- _ ] => specialize (H (TupleToListW_indexed element)) | [ H: ?ens ?element |- _ ] => learn (IndexedEnsemble_TupleToListW_refl element ens H) | [ H: map TuplesF.indexedElement ?x = map TupleToListW ?y |- map IndexedEnsembles.indexedElement ?var = ?y ] => is_evar var; unify var (map2 (fun bedrockElement fiatTuple => {| IndexedEnsembles.elementIndex := TuplesF.elementIndex bedrockElement; IndexedEnsembles.indexedElement := fiatTuple |}) x y) ; pose "Removing this string will break the match that introduced it (this is Coq bug #3412)"%string | [ H: context[In (TupleToListW_indexed ?x) _] |- In ?x _ ] => rewrite <- (Equality.in_map_iff_injective TupleToListW_indexed) by (eauto using TupleToListW_indexed_inj) | [ H: TuplesF.indexedElement _ = TupleToListW _ |- _ ] => rewrite <- H in * | [ H: map _ _ = map _ _ |- _ ] => learn (map_map_sameLength H) | _ => progress rewrite BedrockWElement_roundtrip in * | _ => progress autounfold with FiatBedrockEquivalences Ensembles in * | _ => progress autorewrite with EnsembleIndexedListEquivalence_TupleToListW_UnIndexedEquiv | [ |- exists x, _ ] => eexists | _ => unfold TupleToListW_indexed in *; simpl in * end; apply IndexedEnsemble_TupleToListW_Characterization; try tauto. Qed.
imports: Bedrock.Platform.Facade.examples.TuplesF CertifiedExtraction.Utils Bedrock.Memory CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.AllOfLength CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.Zip2 Coq.Lists.List Coq.Program.Program Coq.Strings.String