Library MyInt31
Require Import Vbase.
Require Export Cyclic31.
Local Open Scope int31.
Definition int31_ltu x y := (phi x <? phi y)%Z.
Notation "n <? m" :=
(int31_ltu n m) (at level 70, no associativity) : int31_scope.
Lemma eqb31P: forall x y, reflect (x = y) (eqb31 x y).
Proof.
ins; unfold eqb31, compare31; desf; constructor; revert Heq;
destruct (Z.compare_spec (phi x) (phi y)); try red; ins; subst; try omega.
by apply (f_equal phi_inv) in H; rewrite !phi_inv_phi in *.
Qed.
Canonical Structure int31_eqMixin := EqMixin eqb31P.
Canonical Structure int31_eqType := Eval hnf in EqType int31 int31_eqMixin.
Lemma int31_ltuP : forall x y, reflect (phi x < phi y)%Z (int31_ltu x y).
Proof.
by ins; case_eq (int31_ltu x y); constructor; [apply Z.ltb_lt|apply Z.ltb_nlt].
Qed.
Require Export Cyclic31.
Local Open Scope int31.
Definition int31_ltu x y := (phi x <? phi y)%Z.
Notation "n <? m" :=
(int31_ltu n m) (at level 70, no associativity) : int31_scope.
Lemma eqb31P: forall x y, reflect (x = y) (eqb31 x y).
Proof.
ins; unfold eqb31, compare31; desf; constructor; revert Heq;
destruct (Z.compare_spec (phi x) (phi y)); try red; ins; subst; try omega.
by apply (f_equal phi_inv) in H; rewrite !phi_inv_phi in *.
Qed.
Canonical Structure int31_eqMixin := EqMixin eqb31P.
Canonical Structure int31_eqType := Eval hnf in EqType int31 int31_eqMixin.
Lemma int31_ltuP : forall x y, reflect (phi x < phi y)%Z (int31_ltu x y).
Proof.
by ins; case_eq (int31_ltu x y); constructor; [apply Z.ltb_lt|apply Z.ltb_nlt].
Qed.
Directives for extraction
Extract Inductive int31 => "int"
["(fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 => x0 + 2 * (x1 + 2 * (x2 + 2 * (x3 + 2 * (x4 + 2 * ( x5 + 2 * (x6 + 2 * (x7 + 2 * (x8 + 2 * (x9 + 2 * ( x10 + 2 * (x11 + 2 * (x12 + 2 * (x13 + 2 * (x14 + 2 * ( x15 + 2 * (x16 + 2 * (x17 + 2 * (x18 + 2 * (x19 + 2 * ( x20 + 2 * (x21 + 2 * (x22 + 2 * (x23 + 2 * (x24 + 2 * ( x25 + 2 * (x26 + 2 * (x27 + 2 * (x28 + 2 * (x29 + 2 * x30 ))))))))))))))))))))))))))))))"].
Extract Constant On => "0".
Extract Constant In => "1".
Extract Constant Tn => "-1".
Extract Constant Twon => "2".
Extract Constant add31 => "( + )".
Extract Constant sub31 => "( - )".
Extract Constant mul31 => "( * )".
Extract Constant mul31 => "( * )".
Extract Constant phi => "Big.of_int".
Extract Constant phi_inv => "Big.to_int".