proposition: Lemma CompileInsert_spec : forall vtmp 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 -> NoDuplicates [[[vtmp; vtable; vtuple]]] -> vtmp ∉ ext -> vtable ∉ ext -> vtuple ∉ ext -> NotInTelescope vtmp tenv -> NotInTelescope vtuple tenv -> NotInTelescope vtable tenv -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> TuplesF.minFreshIndex (IndexedEnsemble_TupleToListW table) idx -> {{ [[ (NTSomeBag k1 k2 vtable) ->> table as _ ]] :: [[ (NTSome (H := @WrapInstance _ _ WTupleCompilation.FiatWrapper) vtuple) ->> tuple as _ ]] :: tenv }} Call vtmp 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 ]] :: [[ (NTSomeBag k1 k2 vtable) ->> rep as _ ]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. PreconditionSet_t. apply ProgOk_Remove_Skip_R; hoare. apply generalized CompileInsert; repeat (compile_do_side_conditions || Lifted_t). eauto. apply ProgOk_Chomp_None; intros. repeat match goal with | [ H: NotInTelescope ?k ?tenv |- context[DropName ?k ?tenv] ] => setoid_rewrite (DropName_NotInTelescope _ _ H) | _ => setoid_rewrite Propagate_anonymous_ret | _ => fold @DropName end. apply CompileDeallocW_discretely; repeat (compile_do_side_conditions || decide_NotInTelescope). apply CompileSkip. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.FiatBedrockLemmas CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CallRules.Tuple