proposition: Lemma refine_DuplicateFree {qsSchema} : forall (qs : UnConstrQueryStructure qsSchema) Ridx tup', (forall tup , tup = tup' \/ tup <> tup') -> refine {b : bool | decides b (forall tup : IndexedElement, GetUnConstrRelation qs Ridx tup -> DuplicateFree tup' (indexedElement tup))} (xs <- For (UnConstrQuery_In qs Ridx (fun tup => Where (tupleAgree_computational' tup tup' (allAttributes _) ) Return tup)); ret (If_Opt_Then_Else (hd_error xs) (fun _ => false) true))%comp.
proof: Proof. unfold refine; intros. computes_to_inv; subst. destruct v0; simpl; computes_to_econstructor; simpl; intros. unfold not; intro. unfold UnConstrQuery_In in H0; simpl; subst. apply (For_computes_to_nil (fun tup0 => (tupleAgree_computational' tup0 (indexedElement tup) (allAttributes (GetNRelSchemaHeading (qschemaSchemas qsSchema) Ridx)))) _ H0 _ H1). apply agreeAllAttributes_eq; eauto. intro. apply For_computes_to_In with (x := r) in H0; intuition. destruct_ex; intuition; subst. apply H1 in H3. apply agreeAllAttributes_eq in H2; unfold DuplicateFree in *. rewrite <- H2 in H3; apply H3; reflexivity. rewrite agreeAllAttributes_eq; eapply (H a). Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Common.ilist2 Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Specification.Constraints.DuplicateFree Fiat.Computation.Core Fiat.Computation.Refinements.General Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements Fiat.Common.Tactics.CacheStringConstant Fiat.QueryStructure.Automation.Common