proposition: Lemma CompileInsert : forall vret vtable vtuple fpointer (env: Env QsADTs.ADTValue) ext tenv N k1 k2 idx (table: FiatWBag N) (tuple: FiatWTuple N), GLabelMap.MapsTo fpointer (Axiomatic WBagOfTuples2ADTSpec.Insert) env -> Lifted_MapsTo ext tenv vtable (wrapBag k1 k2 table) -> Lifted_MapsTo ext tenv vtuple (wrap tuple) -> Lifted_not_mapsto_adt ext tenv vret -> NoDuplicates [[[vret; vtable; vtuple]]] -> vret ∉ ext -> vtable ∉ ext -> vtuple ∉ ext -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> TuplesF.minFreshIndex (IndexedEnsemble_TupleToListW table) idx -> {{ tenv }} Call vret fpointer (vtable :: vtuple :: nil) {{ [[ ( freshIdx <- {freshIdx : nat | IndexedEnsembles.UnConstrFreshIdx table freshIdx}; ret (Ensembles.Add IndexedEnsembles.IndexedElement table {| IndexedEnsembles.elementIndex := freshIdx; IndexedEnsembles.indexedElement := tuple |})) as rep ]] :: [[`vret ->> (Word.natToWord 32 0) as _ ]] :: [[ (NTSomeBag k1 k2 vtable) ->> rep as _ ]] :: DropName vtable (DropName vret (DropName vtuple tenv)) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || PreconditionSet_t). facade_eauto. fiat_t. apply minFresh_UnConstrFresh; eauto. facade_eauto. facade_eauto. unfold BagConstructor; repeat f_equal. apply Ensembles.Extensionality_Ensembles. lazymatch goal with | [ H: TuplesF.minFreshIndex _ ?x, H': TuplesF.minFreshIndex _ ?y |- _ ] => learn (minFreshIndex_unique H H'); subst end. apply Fiat_Bedrock_Insert. repeat apply DropName_remove; eauto 1. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.FiatBedrockLemmas CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CallRules.Tuple