proposition: Lemma QSInsertSpec_UnConstr_refine' : forall qsSchema (qs : _ ) (Ridx : _) (tup : _ ) (or : _ ) (NIntup : ~ GetUnConstrRelation qs Ridx tup), @DropQSConstraints_AbsR qsSchema or qs -> refine (or' <- (qs' <- Pick (QSInsertSpec or Ridx tup); b <- Pick (SuccessfulInsertSpec or Ridx qs' tup); ret (qs', b)); nr' <- {nr' | DropQSConstraints_AbsR (fst or') nr'}; ret (nr', snd or')) (schConstr_self <- {b | decides b (SatisfiesAttributeConstraints Ridx (indexedElement tup))}; schConstr <- {b | decides b (forall tup', GetUnConstrRelation qs Ridx tup' -> SatisfiesTupleConstraints Ridx (indexedElement tup) (indexedElement tup'))}; schConstr' <- {b | decides b (forall tup', GetUnConstrRelation qs Ridx tup' -> SatisfiesTupleConstraints Ridx (indexedElement tup') (indexedElement tup))}; qsConstr <- (@Iterate_Decide_Comp _ (fun Ridx' => SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup) (GetUnConstrRelation qs Ridx'))); qsConstr' <- (@Iterate_Decide_Comp _ (fun Ridx' => Ridx' <> Ridx -> forall tup', (GetUnConstrRelation qs Ridx') tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (EnsembleInsert tup (GetUnConstrRelation qs Ridx)))); match schConstr_self, schConstr, schConstr', qsConstr, qsConstr' with | true, true, true, true, true => ret (UpdateUnConstrRelation qs Ridx (EnsembleInsert tup (GetUnConstrRelation qs Ridx)), true) | _, _, _, _, _ => ret (qs, false) end).
proof: Proof. intros. setoid_rewrite refineEquiv_pick_eq'. unfold DropQSConstraints_AbsR in *; intros; subst. rewrite QSInsertSpec_refine with (default := ret or). unfold refine; intros; subst. computes_to_inv. repeat rewrite GetRelDropConstraints in *. assert ((fun Ridx' => SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup) (GetUnConstrRelation (DropQSConstraints or) Ridx')) = (fun Ridx' => SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup) (GetRelation or Ridx'))) as rewriteSat by (apply functional_extensionality; intros; rewrite GetRelDropConstraints; reflexivity); rewrite rewriteSat in H'''; clear rewriteSat. assert ((fun Ridx' => Ridx' <> Ridx -> forall tup', GetUnConstrRelation (DropQSConstraints or) Ridx' tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (EnsembleInsert tup (GetRelation or Ridx))) = (fun Ridx' => Ridx' <> Ridx -> forall tup', GetRelation or Ridx' tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (EnsembleInsert tup (GetRelation or Ridx)))) as rewriteSat by (apply functional_extensionality; intros; rewrite GetRelDropConstraints; reflexivity). setoid_rewrite rewriteSat in H''''; clear rewriteSat. generalize (Iterate_Decide_Comp_BoundedIndex _ _ H''') as H3'; generalize (Iterate_Decide_Comp_BoundedIndex _ _ H'''') as H4'; intros. revert H''' H''''. computes_to_inv. intros. eapply BindComputes with (a := match v0 as x', v1 as x0', v2 as x1', v3 as x2', v4 as x3' return decides x' _ -> decides x0' _ -> decides x1' _ -> decides x2' _ -> decides x3' _ -> _ with | true, true, true, true, true => fun H H0 H1 H2 H3 => (@Insert_Valid _ or Ridx tup H0 H1 H H2 H3, true) | _, _, _, _, _ => fun _ _ _ _ _ => (or, false) end H H' H'' H3' H4'). eapply BindComputes with (a := match v0 as x', v1 as x0', v2 as x1', v3 as x2', v4 as x3' return decides x' _ -> decides x0' _ -> decides x1' _ -> decides x2' _ -> decides x3' _ -> _ with | true, true, true, true, true => fun H H0 H1 H2 H3 => @Insert_Valid _ or Ridx tup H0 H1 H H2 H3 | _, _, _, _, _ => fun _ _ _ _ _ => or end H H' H'' H3' H4'). repeat (computes_to_econstructor; eauto). repeat find_if_inside; try computes_to_econstructor; simpl in *. unfold GetRelation, Insert_Valid, UpdateUnConstrRelation, UpdateRelation, EnsembleInsert ; simpl; split; intros; eauto. rewrite ilist2.ith_replace2_Index_neq; eauto using string_dec; simpl. rewrite ilist2.ith_replace2_Index_eq; unfold EnsembleInsert, GetRelation; simpl; intuition. computes_to_econstructor. eapply PickComputes with (a := match v0 as x', v1 as x0', v2 as x1', v3 as x2', v4 as x3' return decides x' _ -> decides x0' _ -> decides x1' _ -> decides x2' _ -> decides x3' _ -> _ with | true, true, true, true, true => fun H H0 H1 H2 H3 => true | _, _, _, _, _ => fun _ _ _ _ _ => false end H H' H'' H3' H4'). repeat find_if_inside; simpl; try (solve [unfold not; let H := fresh in intros H; eapply NIntup; eapply H; unfold EnsembleInsert; eauto]). intros; rewrite <- GetRelDropConstraints. unfold Insert_Valid, GetUnConstrRelation, DropQSConstraints, UpdateRelation; simpl. rewrite <- ilist2.ith_imap2, ilist2.ith_replace2_Index_eq; simpl; tauto. simpl in *. unfold not; intros; apply NIntup. rewrite GetRelDropConstraints; eapply H0; unfold DropQSConstraints, Insert_Valid, EnsembleInsert; simpl; eauto. unfold not; intros; apply NIntup; rewrite GetRelDropConstraints; eapply H0; unfold DropQSConstraints, Insert_Valid, EnsembleInsert; simpl; eauto. unfold not; intros; apply NIntup; rewrite GetRelDropConstraints; eapply H0; unfold DropQSConstraints, Insert_Valid, EnsembleInsert; simpl; eauto. unfold not; intros; apply NIntup; rewrite GetRelDropConstraints; eapply H0; unfold DropQSConstraints, Insert_Valid, EnsembleInsert; simpl; eauto. unfold not; intros; apply NIntup; rewrite GetRelDropConstraints; eapply H0; unfold DropQSConstraints, Insert_Valid, EnsembleInsert; simpl; eauto. simpl in *. repeat find_if_inside; simpl; eauto. repeat find_if_inside; simpl; eauto. repeat computes_to_econstructor. unfold Insert_Valid, GetUnConstrRelation, DropQSConstraints, UpdateRelation; simpl; eauto. computes_to_inv; subst. unfold Insert_Valid, GetUnConstrRelation, DropQSConstraints, UpdateUnConstrRelation; simpl; eauto. rewrite ilist2.imap_replace2_Index, <- ilist2.ith_imap2. simpl; computes_to_econstructor. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.IterateBoundedIndex Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements