proposition: Lemma cpr_correct n1 n2 res : match ([n1] ?= [n2])%Z with | Lt => cpr_num n1 n2 res = Lt | Gt => cpr_num n1 n2 res = Gt | Eq => cpr_num n1 n2 res = res end.
proof: Proof. generalize n2 res; clear n2 res. induction n1 as [ | a n1 Hrec]. intros n2 res; simpl cpr_num; nrom. generalize (to_Z_pos n2); case Z.compare_spec; auto with zarith; generalize (zerop_correct n2); case zerop_num; auto with zarith; intros H1 H2 H3; contradict H1; auto with zarith. intros [ | b n2]. intros res; unfold cpr_num. generalize (to_Z_pos (a::n1)); case Z.compare_spec; auto with zarith; generalize (zerop_correct (a::n1)); case zerop_num; auto with zarith; nrom; intros H1 H2 H3; contradict H1; auto with zarith. intros res; unfold cpr_num; fold cpr_num. set (v := (match a ?= b with Eq => res | _ => a ?= b end)). generalize (base_lexi_order _ _ [n1] [n2] _ (to_Z_bounded a) (to_Z_bounded b)); nrom; case Z.compare. intros (HH, HH0). unfold v; rewrite compare_spec; case Z.compare_spec; nrom; intros HH2; try (contradict HH2; auto with zarith; fail). generalize (Hrec n2 res); case Z.compare_spec; auto; intros HH3; contradict HH3; auto with zarith. intros [HH2 | (HH2, HH3)]. generalize (Hrec n2 v); rewrite HH2; unfold v; rewrite compare_spec; case Z.compare_spec; auto. generalize (Hrec n2 v); rewrite HH2; unfold v. rewrite Z.compare_refl. rewrite compare_spec; case Z.compare_spec; auto with zarith ; intros HH; contradict HH; auto with zarith. intros [HH2 | (HH2, HH3)]. generalize (Hrec n2 v); case Z.compare_spec; auto with zarith. intros HH; contradict HH2; auto with zarith. intros HH; contradict HH2; auto with zarith. unfold v; rewrite compare_spec; case Z.compare_spec; auto. generalize (Hrec n2 v); rewrite HH2, Z.compare_refl. unfold v; rewrite compare_spec; case Z.compare_spec; auto. intros HH4; contradict HH3; auto with zarith. intros HH4; contradict HH3; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63