proposition: Lemma refine_Add_binsert : forall or nr iel, or ≃ benumerate nr -> UnConstrFreshIdx or (elementIndex iel) -> RepInvPlus nr -> Add IndexedElement or iel ≃ benumerate (binsert nr (indexedElement iel)).
proof: Proof. simpl; intros; destruct_EnsembleIndexedListEquivalence; clear H. split. - exists (S (elementIndex iel) ). unfold UnConstrFreshIdx, Add in *; intros. inversion H; subst; unfold In in *. + apply H0 in H2; auto with arith. + inversion H2; subst; auto with arith. - destruct (permutation_map_cons indexedElement (binsert_enumerate (indexedElement iel) nr H1) iel lor eq_refl eqv_or) as [lor' (eqv_lor' & perm_lor') ]. exists lor'; intuition; eauto. intuition. + unfold In, Add in *; eapply Permutation_in; [ symmetry; eassumption | simpl; rewrite <- eqv_nr; inversion H; subst; intuition; unfold In in *; inversion H2; subst; eauto]. + eapply Permutation_in in H; eauto; simpl in *; intuition. * constructor 2; subst; constructor. * constructor; rewrite eqv_nr; eauto. + unfold UnConstrFreshIdx in H0. apply NoDup_Permutation_rewrite with (l:=map elementIndex (iel :: lor)). apply Permutation_map; symmetry; assumption. simpl; apply NoDup_cons; clear eqv_or. unfold not; intros. apply in_map_iff in H; destruct H; destruct H. apply eqv_nr in H2. apply H0 in H2. omega. * assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Arith.Arith Coq.Structures.OrderedTypeEx Fiat.Common.String_as_OT Fiat.Common.i2list Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.ADTRefinement.GeneralBuildADTTactics Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.Common.List.ListFacts TransparentAbstract