proposition: Lemma check_diseqs_complete_aux_spec : forall a dist t, check_diseqs_complete_aux a dist t = true <-> forall y, In y dist -> exists 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; auto. intros _ y H; inversion 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); try discriminate; rewrite aexistsbi_spec; intros [i [H1 H2]]; rewrite IHq; clear IHq; intros H3 y [H4|H4]; auto; subst y; exists i; split; auto; generalize H2; case (t .[ i]); try discriminate; intros [a' b']; rewrite orb_true_iff, !andb_true_iff, !Int63.eqb_spec; intros [[H4 H5]|[H4 H5]]; subst a' b'; auto. intro H1; 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 Hy; apply H1; auto. rewrite aexistsbi_false_spec; destruct (H1 b (or_introl (refl_equal b))) as [i [H2 H3]]; intro H; rewrite <- (H _ H2); destruct H3 as [H3|H3]; rewrite H3; rewrite !eqb_refl; auto; rewrite orb_true_r; auto. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms