proposition: Lemma check_diseqs_complete_aux_false_spec : forall a dist t, check_diseqs_complete_aux a dist t = false <-> exists y, In y dist /\ forall i, i <? length t -> (t.[i] <> Some (a,y) /\ t.[i] <> Some (y,a)).
proof: Proof. intros a dist t; induction dist as [ |b q IHq]; simpl; split; try discriminate. intros [y [H _]]; elim H. case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t). intros _; rewrite IHq; clear IHq; intros [y [H3 H4]]; exists y; auto. rewrite aexistsbi_false_spec; intros H _; exists b; split; auto; intros i Hi; split; intro H1; generalize (H _ Hi); rewrite H1, !eqb_refl; try discriminate; rewrite orb_true_r; discriminate. intros [y [H1 H2]]; case_eq (aexistsbi (fun _ (x : option (int * int)) => match x with | Some (a', b') => (a =? a') && (b =? b') || (a =? b') && (b =? a') | None => false end) t); auto; rewrite aexistsbi_spec; intros [i [H3 H4]]; rewrite IHq; clear IHq; exists y; destruct H1 as [H1|H1]; auto; subst y; case_eq (t.[i]); [intros [a' b'] Heq|intro Heq]; rewrite Heq in H4; try discriminate; rewrite orb_true_iff, !andb_true_iff, !eqb_spec in H4; destruct H4 as [[H4 H5]|[H4 H5]]; subst a' b'; generalize (H2 _ H3); rewrite Heq; intros [H4 H5]; [elim H4|elim H5]; auto. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms