Library integral_type
Require Import eqtype ssreflect ssrbool.
Require Import ZArith_ext.
Module Type IntegralType.
Variable t : eqType.
Hypothesis t_dec : forall (x y : t), {x = y} + {x <> y}.
Variable nat2t : nat -> t.
Variable t_plus : t -> t -> t.
Hypothesis t_plus_assoc : forall a b c, t_plus a (t_plus b c) = t_plus (t_plus a b) c.
Hypothesis t_plus_comm : forall n m, t_plus n m = t_plus m n.
Hypothesis t_plus_0 : forall a, t_plus a (nat2t 0) = a.
Hypothesis t_plus_1 : forall a, t_plus (nat2t 1) (nat2t a) = nat2t (S a).
Variable t_minus : t -> t -> t.
Variable t_mult : t -> t -> t.
Variable t_div : t -> t -> t.
Variable t_mod : t -> t -> t.
Variable t_valabs : t -> t.
Variable t_ge : t -> t -> Prop.
Variable t_gt : t -> t -> Prop.
Variable t_geb : t -> t -> bool.
Variable t_gtb : t -> t -> bool.
Hypothesis t_geb_true : forall a b : t, t_geb a b = true -> t_ge a b.
Hypothesis t_geb_true' : forall a b : t, t_ge a b -> t_geb a b = true.
Hypothesis t_gtb_true : forall a b : t, t_gtb a b = true -> t_gt a b.
Hypothesis t_gtb_true' : forall a b : t, t_gt a b -> t_gtb a b = true.
Variable t_eqb : t -> t -> bool.
Hypothesis t_eqb_eq : forall x y : t, t_eqb x y = true -> x = y.
Hypothesis t_eqb_refl : forall x : t, t_eqb x x = true.
Hypothesis t_eqb_false : forall x y : t, t_eqb x y = false <-> x <> y.
Hypothesis t_eqb_false' : forall x y : t, x <> y -> t_eqb x y = false.
Hypothesis nat2t_inj : forall a b, nat2t a = nat2t b -> a = b.
Hypothesis tP : Equality.axiom t_eqb.
Variable t_non_zero : Type.
Variable t_non_zero2t : t_non_zero -> t.
Hypothesis t_non_zero2t_0 : forall x, t_non_zero2t x <> nat2t 0.
Variable t2t_non_zero : forall (i : t), i <> nat2t O -> t_non_zero.
Hypothesis t_non_zero2t_t2t_non_zero : forall z (H : z <> nat2t O), t_non_zero2t (t2t_non_zero z H) = z.
Hypothesis t_non_zero2t_inj : forall x y, t_non_zero2t x = t_non_zero2t y -> x = y.
Variable t_non_zero_eqb : t_non_zero -> t_non_zero -> bool.
Hypothesis t_non_zeroP : Equality.axiom t_non_zero_eqb.
Hypothesis t_ge_refl : forall a, t_ge a a.
Hypothesis t_gt_t_ge : forall a b, (~~ t_gtb a b) = t_geb b a.
Hypothesis t_gtb_def : forall a b, t_gtb a b = t_geb a b && (a != b).
Hypothesis t_gt_weak : forall a b, t_gt a b -> t_ge a b.
Hypothesis t_ge_trans : forall a b c, t_ge a b -> t_ge b c -> t_ge a c.
Hypothesis t_gt_1 : forall n, t_gt (t_plus (nat2t 1) n) n.
End IntegralType.
Require Import Lists_ext.
Module IntegralType_Prop (X : IntegralType).
Import X.
Lemma t_inj_plus : forall n m : nat, nat2t (n + m) = t_plus (nat2t n) (nat2t m).
Proof.
elim=> [m|n IH m].
by rewrite t_plus_comm t_plus_0.
rewrite plus_Sn_m -(t_plus_1 n) -(t_plus_1 (_ + _)) -t_plus_assoc; f_equal.
by apply IH.
Qed.
Definition my_max (a b : t) := if t_geb a b then a else b.
Lemma le_my_max_r : forall a b, t_ge (my_max a b) b.
Proof.
move=> a b.
rewrite /my_max.
move H : (t_geb _ _) => [].
by apply t_geb_true.
by apply t_ge_refl.
Qed.
Lemma le_my_max_l : forall a b, t_ge (my_max b a) b.
Proof.
move=> a b.
rewrite /my_max.
move H : (t_geb _ _) => [].
by apply t_ge_refl.
move/negbT : H => H.
rewrite -t_gt_t_ge in H.
move/negPn : H => H.
apply t_gt_weak.
by apply t_gtb_true.
Qed.
Lemma my_ge_gt_dec : forall a b, t_ge a b \/ t_gt b a.
Proof.
move=> a b.
move H : (t_geb a b) => [|].
left.
by apply t_geb_true.
right.
apply t_gtb_true.
apply/negPn.
move/negbT : H.
apply contra.
move=> H.
apply t_geb_true'.
rewrite t_gt_t_ge in H.
by apply t_geb_true.
Qed.
Lemma t_gt_trans : forall a b c, t_gt a b -> t_gt b c -> t_gt a c.
Proof.
move=> a b c b_a.
move/t_gtb_true'.
move/negPn.
rewrite t_gt_t_ge => c_b.
apply t_gtb_true.
apply/negPn.
rewrite t_gt_t_ge.
move: c_b.
apply contra => c_a.
apply t_gt_weak in b_a.
apply t_geb_true'.
apply t_ge_trans with a => //.
by apply t_geb_true.
Qed.
Lemma my_max_assoc : forall a b c, my_max a (my_max b c) = my_max (my_max a b) c.
Proof.
move=> a b c.
rewrite /my_max.
move b_c : (t_geb b c) => [|].
move a_b : (t_geb a b) => [|].
move a_c : (t_geb a c) => [|] //.
apply t_geb_true in b_c.
apply t_geb_true in a_b.
move: (t_ge_trans _ _ _ a_b b_c).
move/t_geb_true'.
by rewrite a_c.
by rewrite b_c.
move a_c : (t_geb a c) => [|].
move a_b : (t_geb a b) => [|].
by rewrite a_c.
move/negbT : b_c.
rewrite -t_gt_t_ge.
move/negPn => c_b.
move/negbT : a_b.
rewrite -t_gt_t_ge.
move/negPn => b_a.
have a_c2 : t_gtb c a = true.
apply t_gtb_true'.
apply t_gt_trans with b => //.
by apply t_gtb_true.
by apply t_gtb_true.
rewrite -t_gt_t_ge in a_c.
by rewrite a_c2 in a_c.
move a_b : (t_geb a b) => [|].
by rewrite a_c.
by rewrite b_c.
Qed.
Definition my_max_list l def := List.fold_left my_max l def.
Lemma my_max_list_prop1 : forall tl def x, t_ge (my_max_list tl (my_max def x)) x.
Proof.
elim => [def x /= | hd tl IH def x /=].
by apply le_my_max_r.
case: (my_ge_gt_dec hd x) => X.
by apply t_ge_trans with hd.
rewrite -my_max_assoc.
apply t_ge_trans with (my_max x hd) => //.
by apply le_my_max_l.
Qed.
Lemma my_max_list_prop : forall l def x, List.In x l -> t_ge (my_max_list l def) x.
Proof.
elim=> // hd tl IH def x /= [-> | H]; by [apply my_max_list_prop1 | apply IH].
Qed.
Lemma my_max_list_disj : forall l, disj (t_plus (nat2t 1) (my_max_list l (nat2t O)) :: List.nil) l.
Proof.
move=> l.
apply disj_cons_L; first by apply disj_nil_L.
move/(my_max_list_prop _ (nat2t O)).
move/t_geb_true'.
rewrite -t_gt_t_ge.
move/negP.
apply.
apply t_gtb_true'.
by apply t_gt_1.
Qed.
Lemma t_geb_false : forall a b : t, ~~ t_geb a b -> ~ t_ge a b.
Proof. move=> a b. move/negP => H. by move/t_geb_true'. Qed.
Lemma t_gtb_false : forall a b : t, ~~ t_gtb a b -> ~ t_gt a b.
Proof. move=> a b. move/negP => H. by move/t_gtb_true'. Qed.
Lemma t_geb_false' : forall a b : t, ~ t_ge a b -> ~~ t_geb a b.
Proof. move=> a b H. apply/negP. contradict H. by apply t_geb_true. Qed.
Lemma t_gtb_false' : forall a b : t, ~ t_gt a b -> ~~ t_gtb a b.
Proof. move=> a b H. apply/negP. contradict H. by apply t_gtb_true. Qed.
End IntegralType_Prop.
Inductive negpos : Set :=
| neg : positive -> negpos
| pos : positive -> negpos.
Definition negpos_eqb a b :=
match (a, b) with
| (neg a', neg b') => Ndec.Peqb a' b'
| (pos a', pos b') => Ndec.Peqb a' b'
| _ => false
end.
Lemma negposP : Equality.axiom negpos_eqb.
Proof.
move=> x y.
apply: (iffP idP) => H.
destruct x; destruct y => //.
rewrite /negpos_eqb /= in H.
move/positiveP:H => H.
subst => //.
rewrite /negpos_eqb /= in H.
move/positiveP:H => H.
subst => //.
subst.
destruct y; rewrite /negpos_eqb => /=.
apply/positiveP => //.
apply/positiveP => //.
Qed.
Canonical Structure negpos_eqMixin := EqMixin negposP.
Canonical Structure negpos_eqType := Eval hnf in EqType _ negpos_eqMixin.
Module ZIT <: IntegralType.
Definition t : eqType := Z_eqType.
Lemma t_dec : forall (x y : t), {x = y} + {x <> y}.
Proof. exact Z_eq_dec. Qed.
Definition nat2t : nat -> t := Z_of_nat.
Definition t_plus : t -> t -> t := Zplus.
Lemma t_plus_assoc : forall a b c, t_plus a (t_plus b c) = t_plus (t_plus a b) c.
Proof. exact Zplus_assoc. Qed.
Lemma t_plus_comm : forall n m, t_plus n m = t_plus m n.
Proof. exact Zplus_comm. Qed.
Lemma t_plus_0 : forall a, t_plus a (nat2t 0) = a.
Proof. move=> a. rewrite /t_plus /nat2t /= Zplus_0_r //. Qed.
Lemma t_plus_1 : forall a, t_plus (nat2t 1) (nat2t a) = nat2t (S a).
Proof. move=> a. rewrite /t_plus /nat2t !Z_S [Z_of_nat 0]/= Zplus_0_l Zplus_comm; done. Qed.
Definition t_minus : t -> t -> t := Zminus.
Definition t_mult : t -> t -> t := Zmult.
Definition t_div : t -> t -> t := Zdiv.
Definition t_mod : t -> t -> t := Zmod.
Definition t_valabs : t -> t := Zabs.
Definition t_ge : t -> t -> Prop := Zge.
Definition t_gt : t -> t -> Prop := Zgt.
Definition t_geb : t -> t -> bool := Zge_bool.
Definition t_gtb : t -> t -> bool := Zgt_bool.
Lemma t_geb_true : forall a b : t, t_geb a b = true -> t_ge a b.
Proof. exact Zge_bool_true. Qed.
Lemma t_geb_true' : forall a b : t, t_ge a b -> t_geb a b = true.
Proof. exact Zge_bool_true'. Qed.
Lemma t_gtb_true : forall a b : t, t_gtb a b = true -> t_gt a b.
Proof. exact Zgt_bool_true. Qed.
Lemma t_gtb_true' : forall a b : t, t_gt a b -> t_gtb a b = true.
Proof. exact Zgt_bool_true'. Qed.
Definition t_eqb : t -> t -> bool := Zeq_bool.
Lemma t_eqb_eq : forall x y : t, t_eqb x y = true -> x = y.
Proof. exact Zeq_bool_eq. Qed.
Lemma t_eqb_refl : forall x : t, t_eqb x x = true.
Proof. exact Zeq_bool_refl. Qed.
Lemma t_eqb_false : forall x y : t, t_eqb x y = false <-> x <> y.
Proof. split. by apply Zeq_bool_neq. by apply Zeq_bool_neq'. Qed.
Lemma t_eqb_false' : forall x y : t, x <> y -> t_eqb x y = false.
Proof. exact Zeq_bool_neq'. Qed.
Lemma nat2t_inj : forall a b, nat2t a = nat2t b -> a = b.
Proof.
move=> a b.
by move/Z_of_nat_inj.
Qed.
Lemma tP : Equality.axiom t_eqb.
Proof. exact Zeq_boolP. Qed.
Definition t_non_zero : Set := negpos.
Definition t_non_zero2t (x : t_non_zero) : t :=
match x with neg p => Zneg p | pos p => Zpos p end.
Lemma t_non_zero2t_0 : forall x, t_non_zero2t x <> nat2t 0.
Proof. case=> p //=. Qed.
Definition t2t_non_zero (i : t) (H : i <> nat2t O) : t_non_zero.
Proof.
case:i H => // p H.
exact (pos p).
exact (neg p).
Defined.
Lemma t_non_zero2t_t2t_non_zero : forall z (H : z <> nat2t O), t_non_zero2t (t2t_non_zero z H) = z.
Proof. case=> //. Qed.
Lemma t_non_zero2t_inj : forall x y, t_non_zero2t x = t_non_zero2t y -> x = y.
Proof. case=> p; case=> p' //=; case=> -> //. Qed.
Definition t_non_zero_eqb : t_non_zero -> t_non_zero -> bool := negpos_eqb.
Lemma t_non_zeroP : Equality.axiom t_non_zero_eqb.
Proof. exact negposP. Qed.
Lemma t_ge_refl : forall a, t_ge a a.
Proof.
move=> a.
apply Zle_ge.
apply Zle_refl.
Qed.
Lemma t_gt_t_ge : forall a b, (~~ t_gtb a b) = t_geb b a.
Proof.
move=> a b.
by rewrite -Zge_bool_Zgt_bool.
Qed.
Lemma t_gtb_def a b : t_gtb a b = t_geb a b && (a != b).
Proof.
rewrite /t_gtb /t_geb.
apply/Zgt_boolP.
case: ifP.
case/andP.
move/Zge_boolP => X.
move/eqP => Y; omega.
move/negP.
move => X Y; apply X.
apply/andP; split.
apply/Zge_boolP; omega.
apply/eqP; omega.
Qed.
Lemma t_gt_weak : forall a b, t_gt a b -> t_ge a b.
Proof.
move=> a b.
rewrite /t_gt /t_ge; omega.
Qed.
Lemma t_ge_trans : forall a b c, t_ge a b -> t_ge b c -> t_ge a c.
exact Zge_trans.
Qed.
Lemma t_gt_1 : forall n, t_gt (t_plus (nat2t 1) n) n.
move=> n.
rewrite /t_gt /t_plus /nat2t [Z_of_nat _]/=.
omega.
Qed.
End ZIT.
Module Import ZIT_prop_m := IntegralType_Prop ZIT.
Ltac open_integral_type_hyp :=
match goal with
| |- is_true (ZIT.t_gtb _ _) => apply ZIT.t_gtb_true'; unfold ZIT.t_gt
| H : is_true (ZIT.t_gtb _ _) |- _ =>
move: {H}(ZIT.t_gtb_true _ _ H) => H; unfold ZIT.t_gt in H
| |- is_true (~~ ZIT.t_gtb _ _) => apply t_gtb_false'; unfold ZIT.t_gt
| H : is_true (~~ ZIT.t_gtb _ _) |- _ =>
move: {H}(t_gtb_false _ _ H) => H; unfold ZIT.t_gt in H
| |- is_true (~~ ZIT.t_geb _ _) => apply t_geb_false'; unfold ZIT.t_ge
| |- is_true (ZIT.t_geb _ _) => apply ZIT.t_geb_true'; unfold ZIT.t_ge
| H : is_true (ZIT.t_geb _ _) |- _ =>
move: {H}(ZIT.t_geb_true _ _ H) => H; unfold ZIT.t_ge in H
| H : is_true (~~ ZIT.t_geb _ _) |- _ =>
move: {H}(t_geb_false _ _ H) => H; unfold ZIT.t_ge in H
| |- is_true (ZIT.t_eqb _ _) => apply/ZIT.tP
| H : is_true (ZIT.t_eqb _ _) |- _ => move/ZIT.tP : H => H
| H : context [ZIT.t_plus _ _] |- _ => unfold ZIT.t_plus in H
| H : context [ZIT.t_minus _ _] |- _ => unfold ZIT.t_minus in H
| H : context [ZIT.t_mult _ _] |- _ => unfold ZIT.t_mult in H
| H : context [ZIT.t_gt _ _] |- _ => unfold ZIT.t_gt in H
| H : context [ZIT.t_ge _ _] |- _ => unfold ZIT.t_ge in H
| H : context [ZIT.nat2t _] |- _ => unfold ZIT.nat2t in H
end.
Ltac open_integral_type_goal :=
match goal with
| |- _ => unfold ZIT.t_plus, ZIT.t_minus, ZIT.t_mult, ZIT.t_gt, ZIT.t_ge, ZIT.nat2t
end.
Lemma ZIT_ring_theory : @ring_theory ZIT.t Z0 1%Z Zplus Zmult Zminus Zopp (@eq _).
Proof.
constructor.
exact Zplus_0_l.
exact Zplus_comm.
exact Zplus_assoc.
exact Zmult_1_l.
exact Zmult_comm.
exact Zmult_assoc.
exact Zmult_plus_distr_l.
move=> x [] //.
exact Zplus_opp_r.
Qed.
Add Ring ZIT_ring : ZIT_ring_theory.
Require Import ZArith_ext.
Module Type IntegralType.
Variable t : eqType.
Hypothesis t_dec : forall (x y : t), {x = y} + {x <> y}.
Variable nat2t : nat -> t.
Variable t_plus : t -> t -> t.
Hypothesis t_plus_assoc : forall a b c, t_plus a (t_plus b c) = t_plus (t_plus a b) c.
Hypothesis t_plus_comm : forall n m, t_plus n m = t_plus m n.
Hypothesis t_plus_0 : forall a, t_plus a (nat2t 0) = a.
Hypothesis t_plus_1 : forall a, t_plus (nat2t 1) (nat2t a) = nat2t (S a).
Variable t_minus : t -> t -> t.
Variable t_mult : t -> t -> t.
Variable t_div : t -> t -> t.
Variable t_mod : t -> t -> t.
Variable t_valabs : t -> t.
Variable t_ge : t -> t -> Prop.
Variable t_gt : t -> t -> Prop.
Variable t_geb : t -> t -> bool.
Variable t_gtb : t -> t -> bool.
Hypothesis t_geb_true : forall a b : t, t_geb a b = true -> t_ge a b.
Hypothesis t_geb_true' : forall a b : t, t_ge a b -> t_geb a b = true.
Hypothesis t_gtb_true : forall a b : t, t_gtb a b = true -> t_gt a b.
Hypothesis t_gtb_true' : forall a b : t, t_gt a b -> t_gtb a b = true.
Variable t_eqb : t -> t -> bool.
Hypothesis t_eqb_eq : forall x y : t, t_eqb x y = true -> x = y.
Hypothesis t_eqb_refl : forall x : t, t_eqb x x = true.
Hypothesis t_eqb_false : forall x y : t, t_eqb x y = false <-> x <> y.
Hypothesis t_eqb_false' : forall x y : t, x <> y -> t_eqb x y = false.
Hypothesis nat2t_inj : forall a b, nat2t a = nat2t b -> a = b.
Hypothesis tP : Equality.axiom t_eqb.
Variable t_non_zero : Type.
Variable t_non_zero2t : t_non_zero -> t.
Hypothesis t_non_zero2t_0 : forall x, t_non_zero2t x <> nat2t 0.
Variable t2t_non_zero : forall (i : t), i <> nat2t O -> t_non_zero.
Hypothesis t_non_zero2t_t2t_non_zero : forall z (H : z <> nat2t O), t_non_zero2t (t2t_non_zero z H) = z.
Hypothesis t_non_zero2t_inj : forall x y, t_non_zero2t x = t_non_zero2t y -> x = y.
Variable t_non_zero_eqb : t_non_zero -> t_non_zero -> bool.
Hypothesis t_non_zeroP : Equality.axiom t_non_zero_eqb.
Hypothesis t_ge_refl : forall a, t_ge a a.
Hypothesis t_gt_t_ge : forall a b, (~~ t_gtb a b) = t_geb b a.
Hypothesis t_gtb_def : forall a b, t_gtb a b = t_geb a b && (a != b).
Hypothesis t_gt_weak : forall a b, t_gt a b -> t_ge a b.
Hypothesis t_ge_trans : forall a b c, t_ge a b -> t_ge b c -> t_ge a c.
Hypothesis t_gt_1 : forall n, t_gt (t_plus (nat2t 1) n) n.
End IntegralType.
Require Import Lists_ext.
Module IntegralType_Prop (X : IntegralType).
Import X.
Lemma t_inj_plus : forall n m : nat, nat2t (n + m) = t_plus (nat2t n) (nat2t m).
Proof.
elim=> [m|n IH m].
by rewrite t_plus_comm t_plus_0.
rewrite plus_Sn_m -(t_plus_1 n) -(t_plus_1 (_ + _)) -t_plus_assoc; f_equal.
by apply IH.
Qed.
Definition my_max (a b : t) := if t_geb a b then a else b.
Lemma le_my_max_r : forall a b, t_ge (my_max a b) b.
Proof.
move=> a b.
rewrite /my_max.
move H : (t_geb _ _) => [].
by apply t_geb_true.
by apply t_ge_refl.
Qed.
Lemma le_my_max_l : forall a b, t_ge (my_max b a) b.
Proof.
move=> a b.
rewrite /my_max.
move H : (t_geb _ _) => [].
by apply t_ge_refl.
move/negbT : H => H.
rewrite -t_gt_t_ge in H.
move/negPn : H => H.
apply t_gt_weak.
by apply t_gtb_true.
Qed.
Lemma my_ge_gt_dec : forall a b, t_ge a b \/ t_gt b a.
Proof.
move=> a b.
move H : (t_geb a b) => [|].
left.
by apply t_geb_true.
right.
apply t_gtb_true.
apply/negPn.
move/negbT : H.
apply contra.
move=> H.
apply t_geb_true'.
rewrite t_gt_t_ge in H.
by apply t_geb_true.
Qed.
Lemma t_gt_trans : forall a b c, t_gt a b -> t_gt b c -> t_gt a c.
Proof.
move=> a b c b_a.
move/t_gtb_true'.
move/negPn.
rewrite t_gt_t_ge => c_b.
apply t_gtb_true.
apply/negPn.
rewrite t_gt_t_ge.
move: c_b.
apply contra => c_a.
apply t_gt_weak in b_a.
apply t_geb_true'.
apply t_ge_trans with a => //.
by apply t_geb_true.
Qed.
Lemma my_max_assoc : forall a b c, my_max a (my_max b c) = my_max (my_max a b) c.
Proof.
move=> a b c.
rewrite /my_max.
move b_c : (t_geb b c) => [|].
move a_b : (t_geb a b) => [|].
move a_c : (t_geb a c) => [|] //.
apply t_geb_true in b_c.
apply t_geb_true in a_b.
move: (t_ge_trans _ _ _ a_b b_c).
move/t_geb_true'.
by rewrite a_c.
by rewrite b_c.
move a_c : (t_geb a c) => [|].
move a_b : (t_geb a b) => [|].
by rewrite a_c.
move/negbT : b_c.
rewrite -t_gt_t_ge.
move/negPn => c_b.
move/negbT : a_b.
rewrite -t_gt_t_ge.
move/negPn => b_a.
have a_c2 : t_gtb c a = true.
apply t_gtb_true'.
apply t_gt_trans with b => //.
by apply t_gtb_true.
by apply t_gtb_true.
rewrite -t_gt_t_ge in a_c.
by rewrite a_c2 in a_c.
move a_b : (t_geb a b) => [|].
by rewrite a_c.
by rewrite b_c.
Qed.
Definition my_max_list l def := List.fold_left my_max l def.
Lemma my_max_list_prop1 : forall tl def x, t_ge (my_max_list tl (my_max def x)) x.
Proof.
elim => [def x /= | hd tl IH def x /=].
by apply le_my_max_r.
case: (my_ge_gt_dec hd x) => X.
by apply t_ge_trans with hd.
rewrite -my_max_assoc.
apply t_ge_trans with (my_max x hd) => //.
by apply le_my_max_l.
Qed.
Lemma my_max_list_prop : forall l def x, List.In x l -> t_ge (my_max_list l def) x.
Proof.
elim=> // hd tl IH def x /= [-> | H]; by [apply my_max_list_prop1 | apply IH].
Qed.
Lemma my_max_list_disj : forall l, disj (t_plus (nat2t 1) (my_max_list l (nat2t O)) :: List.nil) l.
Proof.
move=> l.
apply disj_cons_L; first by apply disj_nil_L.
move/(my_max_list_prop _ (nat2t O)).
move/t_geb_true'.
rewrite -t_gt_t_ge.
move/negP.
apply.
apply t_gtb_true'.
by apply t_gt_1.
Qed.
Lemma t_geb_false : forall a b : t, ~~ t_geb a b -> ~ t_ge a b.
Proof. move=> a b. move/negP => H. by move/t_geb_true'. Qed.
Lemma t_gtb_false : forall a b : t, ~~ t_gtb a b -> ~ t_gt a b.
Proof. move=> a b. move/negP => H. by move/t_gtb_true'. Qed.
Lemma t_geb_false' : forall a b : t, ~ t_ge a b -> ~~ t_geb a b.
Proof. move=> a b H. apply/negP. contradict H. by apply t_geb_true. Qed.
Lemma t_gtb_false' : forall a b : t, ~ t_gt a b -> ~~ t_gtb a b.
Proof. move=> a b H. apply/negP. contradict H. by apply t_gtb_true. Qed.
End IntegralType_Prop.
Inductive negpos : Set :=
| neg : positive -> negpos
| pos : positive -> negpos.
Definition negpos_eqb a b :=
match (a, b) with
| (neg a', neg b') => Ndec.Peqb a' b'
| (pos a', pos b') => Ndec.Peqb a' b'
| _ => false
end.
Lemma negposP : Equality.axiom negpos_eqb.
Proof.
move=> x y.
apply: (iffP idP) => H.
destruct x; destruct y => //.
rewrite /negpos_eqb /= in H.
move/positiveP:H => H.
subst => //.
rewrite /negpos_eqb /= in H.
move/positiveP:H => H.
subst => //.
subst.
destruct y; rewrite /negpos_eqb => /=.
apply/positiveP => //.
apply/positiveP => //.
Qed.
Canonical Structure negpos_eqMixin := EqMixin negposP.
Canonical Structure negpos_eqType := Eval hnf in EqType _ negpos_eqMixin.
Module ZIT <: IntegralType.
Definition t : eqType := Z_eqType.
Lemma t_dec : forall (x y : t), {x = y} + {x <> y}.
Proof. exact Z_eq_dec. Qed.
Definition nat2t : nat -> t := Z_of_nat.
Definition t_plus : t -> t -> t := Zplus.
Lemma t_plus_assoc : forall a b c, t_plus a (t_plus b c) = t_plus (t_plus a b) c.
Proof. exact Zplus_assoc. Qed.
Lemma t_plus_comm : forall n m, t_plus n m = t_plus m n.
Proof. exact Zplus_comm. Qed.
Lemma t_plus_0 : forall a, t_plus a (nat2t 0) = a.
Proof. move=> a. rewrite /t_plus /nat2t /= Zplus_0_r //. Qed.
Lemma t_plus_1 : forall a, t_plus (nat2t 1) (nat2t a) = nat2t (S a).
Proof. move=> a. rewrite /t_plus /nat2t !Z_S [Z_of_nat 0]/= Zplus_0_l Zplus_comm; done. Qed.
Definition t_minus : t -> t -> t := Zminus.
Definition t_mult : t -> t -> t := Zmult.
Definition t_div : t -> t -> t := Zdiv.
Definition t_mod : t -> t -> t := Zmod.
Definition t_valabs : t -> t := Zabs.
Definition t_ge : t -> t -> Prop := Zge.
Definition t_gt : t -> t -> Prop := Zgt.
Definition t_geb : t -> t -> bool := Zge_bool.
Definition t_gtb : t -> t -> bool := Zgt_bool.
Lemma t_geb_true : forall a b : t, t_geb a b = true -> t_ge a b.
Proof. exact Zge_bool_true. Qed.
Lemma t_geb_true' : forall a b : t, t_ge a b -> t_geb a b = true.
Proof. exact Zge_bool_true'. Qed.
Lemma t_gtb_true : forall a b : t, t_gtb a b = true -> t_gt a b.
Proof. exact Zgt_bool_true. Qed.
Lemma t_gtb_true' : forall a b : t, t_gt a b -> t_gtb a b = true.
Proof. exact Zgt_bool_true'. Qed.
Definition t_eqb : t -> t -> bool := Zeq_bool.
Lemma t_eqb_eq : forall x y : t, t_eqb x y = true -> x = y.
Proof. exact Zeq_bool_eq. Qed.
Lemma t_eqb_refl : forall x : t, t_eqb x x = true.
Proof. exact Zeq_bool_refl. Qed.
Lemma t_eqb_false : forall x y : t, t_eqb x y = false <-> x <> y.
Proof. split. by apply Zeq_bool_neq. by apply Zeq_bool_neq'. Qed.
Lemma t_eqb_false' : forall x y : t, x <> y -> t_eqb x y = false.
Proof. exact Zeq_bool_neq'. Qed.
Lemma nat2t_inj : forall a b, nat2t a = nat2t b -> a = b.
Proof.
move=> a b.
by move/Z_of_nat_inj.
Qed.
Lemma tP : Equality.axiom t_eqb.
Proof. exact Zeq_boolP. Qed.
Definition t_non_zero : Set := negpos.
Definition t_non_zero2t (x : t_non_zero) : t :=
match x with neg p => Zneg p | pos p => Zpos p end.
Lemma t_non_zero2t_0 : forall x, t_non_zero2t x <> nat2t 0.
Proof. case=> p //=. Qed.
Definition t2t_non_zero (i : t) (H : i <> nat2t O) : t_non_zero.
Proof.
case:i H => // p H.
exact (pos p).
exact (neg p).
Defined.
Lemma t_non_zero2t_t2t_non_zero : forall z (H : z <> nat2t O), t_non_zero2t (t2t_non_zero z H) = z.
Proof. case=> //. Qed.
Lemma t_non_zero2t_inj : forall x y, t_non_zero2t x = t_non_zero2t y -> x = y.
Proof. case=> p; case=> p' //=; case=> -> //. Qed.
Definition t_non_zero_eqb : t_non_zero -> t_non_zero -> bool := negpos_eqb.
Lemma t_non_zeroP : Equality.axiom t_non_zero_eqb.
Proof. exact negposP. Qed.
Lemma t_ge_refl : forall a, t_ge a a.
Proof.
move=> a.
apply Zle_ge.
apply Zle_refl.
Qed.
Lemma t_gt_t_ge : forall a b, (~~ t_gtb a b) = t_geb b a.
Proof.
move=> a b.
by rewrite -Zge_bool_Zgt_bool.
Qed.
Lemma t_gtb_def a b : t_gtb a b = t_geb a b && (a != b).
Proof.
rewrite /t_gtb /t_geb.
apply/Zgt_boolP.
case: ifP.
case/andP.
move/Zge_boolP => X.
move/eqP => Y; omega.
move/negP.
move => X Y; apply X.
apply/andP; split.
apply/Zge_boolP; omega.
apply/eqP; omega.
Qed.
Lemma t_gt_weak : forall a b, t_gt a b -> t_ge a b.
Proof.
move=> a b.
rewrite /t_gt /t_ge; omega.
Qed.
Lemma t_ge_trans : forall a b c, t_ge a b -> t_ge b c -> t_ge a c.
exact Zge_trans.
Qed.
Lemma t_gt_1 : forall n, t_gt (t_plus (nat2t 1) n) n.
move=> n.
rewrite /t_gt /t_plus /nat2t [Z_of_nat _]/=.
omega.
Qed.
End ZIT.
Module Import ZIT_prop_m := IntegralType_Prop ZIT.
Ltac open_integral_type_hyp :=
match goal with
| |- is_true (ZIT.t_gtb _ _) => apply ZIT.t_gtb_true'; unfold ZIT.t_gt
| H : is_true (ZIT.t_gtb _ _) |- _ =>
move: {H}(ZIT.t_gtb_true _ _ H) => H; unfold ZIT.t_gt in H
| |- is_true (~~ ZIT.t_gtb _ _) => apply t_gtb_false'; unfold ZIT.t_gt
| H : is_true (~~ ZIT.t_gtb _ _) |- _ =>
move: {H}(t_gtb_false _ _ H) => H; unfold ZIT.t_gt in H
| |- is_true (~~ ZIT.t_geb _ _) => apply t_geb_false'; unfold ZIT.t_ge
| |- is_true (ZIT.t_geb _ _) => apply ZIT.t_geb_true'; unfold ZIT.t_ge
| H : is_true (ZIT.t_geb _ _) |- _ =>
move: {H}(ZIT.t_geb_true _ _ H) => H; unfold ZIT.t_ge in H
| H : is_true (~~ ZIT.t_geb _ _) |- _ =>
move: {H}(t_geb_false _ _ H) => H; unfold ZIT.t_ge in H
| |- is_true (ZIT.t_eqb _ _) => apply/ZIT.tP
| H : is_true (ZIT.t_eqb _ _) |- _ => move/ZIT.tP : H => H
| H : context [ZIT.t_plus _ _] |- _ => unfold ZIT.t_plus in H
| H : context [ZIT.t_minus _ _] |- _ => unfold ZIT.t_minus in H
| H : context [ZIT.t_mult _ _] |- _ => unfold ZIT.t_mult in H
| H : context [ZIT.t_gt _ _] |- _ => unfold ZIT.t_gt in H
| H : context [ZIT.t_ge _ _] |- _ => unfold ZIT.t_ge in H
| H : context [ZIT.nat2t _] |- _ => unfold ZIT.nat2t in H
end.
Ltac open_integral_type_goal :=
match goal with
| |- _ => unfold ZIT.t_plus, ZIT.t_minus, ZIT.t_mult, ZIT.t_gt, ZIT.t_ge, ZIT.nat2t
end.
Lemma ZIT_ring_theory : @ring_theory ZIT.t Z0 1%Z Zplus Zmult Zminus Zopp (@eq _).
Proof.
constructor.
exact Zplus_0_l.
exact Zplus_comm.
exact Zplus_assoc.
exact Zmult_1_l.
exact Zmult_comm.
exact Zmult_assoc.
exact Zmult_plus_distr_l.
move=> x [] //.
exact Zplus_opp_r.
Qed.
Add Ring ZIT_ring : ZIT_ring_theory.