proposition: Lemma check_diseqs_complete_spec : forall dist t, check_diseqs_complete dist t = true <-> forall x y, In2 x y dist -> exists i, i <? length t /\ (t.[i] = Some (x,y) \/ t.[i] = Some (y,x)).
proof: Proof. intros dist t; induction dist as [ |a q IHq]; simpl; split; auto. intros _ x y H; inversion H. case_eq (check_diseqs_complete_aux a q t); try discriminate; rewrite check_diseqs_complete_aux_spec, IHq; clear IHq; intros H1 H2 x y H3; inversion H3; auto. intro H; case_eq (check_diseqs_complete_aux a q t). rewrite IHq; clear IHq; intros _ x y H1; apply H; constructor 2; auto. rewrite check_diseqs_complete_aux_false_spec; clear IHq; intros [y [H1 H2]]; destruct (H _ _ (In2_hd _ a _ _ H1)) as [i [H3 [H4|H4]]]; elim (H2 _ H3); rewrite H4; intros H5 H6; [elim H5|elim H6]; auto. Qed.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms