proposition: Lemma BagSanityConditions_Add: forall n (r : FiatWBag n) el, TuplesF.functional (IndexedEnsemble_TupleToListW r) -> IndexedEnsembles.UnConstrFreshIdx r (IndexedEnsembles.elementIndex el) -> BagSanityConditions (Ensembles.Add IndexedEnsembles.IndexedElement r el).
proof: Proof. split; unfold TuplesF.functional, TuplesF.minFreshIndex; intros; intuition. - destruct t1; destruct t2; simpl in *; subst; f_equal. destruct H2; destruct H1; intuition. destruct H2; destruct H3; subst. + unfold TuplesF.tupl in *. unfold RelatedIndexedTupleAndListW in *; simpl in *; intuition. subst. destruct x; destruct x0; simpl in *; subst. apply Lift_Ensemble in H2; apply Lift_Ensemble in H1. pose proof (H _ _ H1 H2 (eq_refl _)); injections; eauto. + destruct H2. unfold RelatedIndexedTupleAndListW in *; simpl in *; intuition; subst. destruct x0; destruct el; simpl in *; subst. unfold TuplesF.UnConstrFreshIdx in H1. unfold IndexedEnsembles.UnConstrFreshIdx in H0. apply H0 in H1; simpl in *. omega. + destruct H1. unfold RelatedIndexedTupleAndListW in *; simpl in *; intuition; subst. destruct x; destruct el; simpl in *; subst. unfold IndexedEnsembles.UnConstrFreshIdx in H0. apply H0 in H2; simpl in *. omega. + destruct H2; destruct H1. unfold RelatedIndexedTupleAndListW in *; simpl in *; intuition; subst. reflexivity. - exists (S (IndexedEnsembles.elementIndex el)); split. + unfold TuplesF.UnConstrFreshIdx in *; intros. destruct H1 as [? [? ? ] ]. unfold RelatedIndexedTupleAndListW in *; simpl in *; intuition; subst. destruct element; simpl in *; subst. * destruct H1. destruct x; simpl in *. apply H0 in H1; simpl in *; omega. destruct H1; omega. + intros. inversion H1; subst. unfold TuplesF.UnConstrFreshIdx in *. assert (lt (TuplesF.elementIndex (IndexedElement_TupleToListW el)) (IndexedEnsembles.elementIndex el) ). eapply H2. econstructor; split. unfold Ensembles.Add. econstructor 2. reflexivity. unfold RelatedIndexedTupleAndListW; eauto. destruct el; simpl in *; omega. unfold TuplesF.UnConstrFreshIdx in *; intros. assert (lt (IndexedEnsembles.elementIndex el) idx'). eapply (H2 {| TuplesF.elementIndex := _; TuplesF.indexedElement := _ |}); simpl. unfold IndexedEnsemble_TupleToListW. simpl; eexists; split. econstructor 2. reflexivity. unfold RelatedIndexedTupleAndListW; simpl; split; eauto. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.QueryStructures.Basics CertifiedExtraction.Extraction.QueryStructures.TupleToListW CertifiedExtraction.Extraction.QueryStructures.EnsemblesOfTuplesAndListW CertifiedExtraction.Extraction.QueryStructures.CallRules.CallRules CertifiedExtraction.Extraction.QueryStructures.Wrappers Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Bedrock.Platform.Facade.CompileUnit2 CertifiedExtraction.ADT2CompileUnit CertifiedExtraction.Extraction.Extraction CertifiedExtraction.Extraction.QueryStructures.Decompose Bedrock.Memory Bedrock.Platform.Facade.DFModule Bedrock.Platform.Facade.CompileUnit2