Library Field
The record of operations
Structure fparams: Type := {
K:> Set;
v0: K;
v1: K;
eqK: K -> K -> bool;
oppK: K -> K;
addK : K -> K -> K;
multK : K -> K -> K;
invK : K -> K
}.
Recover the usual mathematical notations
Delimit Scope field_scope with f.
Notation "x ?= y" := (eqK _ x y) (at level 70) : field_scope.
Notation "x + y" := (addK _ x y) : field_scope.
Notation "- x" := (oppK _ x) : field_scope.
Notation "x ^-1" := (invK _ x) (at level 25) : field_scope.
Notation "x * y" := (multK _ x y) : field_scope.
Notation "0" := (v0 _) : field_scope.
Notation "1" := (v1 _) : field_scope.
Section ParamsProp.
Variable p: fparams.
Open Scope field_scope.
Structure fparamsProp: Type := {
eqK_dec: forall x y: p, if x ?= y then x = y else x <> y;
addK_assoc: forall x y z: p, (x + y) + z = x + (y + z);
addK_com: forall x y: p, x + y = y + x;
addK0l: forall x: p, 0 + x = x;
oppKr: forall x: p, x + - x = 0;
multK_assoc: forall x y z: p, (x * y) * z = x * (y * z);
multK_com: forall x y: p, x * y = y * x;
multK1l: forall x: p, 1 * x = x;
add_multKl: forall x y z: p, (x + y) * z = x * z + y * z;
one_diff_zero: 1 <> 0 :> p;
invKl: forall x: p, x <> 0 -> x * x^-1 = 1
}.
Notation "x ^ k" := (expK x k) : field_scope.
Derived properties
Variable Hp: fparamsProp.
Implicit Types x y z: p.
Lemma eqKI: forall x, x ?= x = true.
Lemma eqK_spec x y: eq_Spec x y (x ?= y).
Left oppositive for +
Cancelation rule for +
Lemma addK_cancel x y z: x + y = x + z -> y = z.
Lemma addK_eq_opp: forall x y, x + (-y) = 0 -> x = y.
Lemma addK_eq_opp: forall x y, x + (-y) = 0 -> x = y.
Right neutral for +
Oppositive involutive
Right neutral for *
Right distributivity of + over *
0 is its own opposite
Distributivity of - over +
Right absorbent for *
Left absorbent for *
Left distributivity of - over *
Right distributivity of - over *
Lemma opp_multKr x y: - (x * y) = x * - y.
Lemma opp_multK1l x: - x = (-(1)) * x.
Lemma opp_multK1r x: - x = x * (-(1)).
Lemma multK_m1_m1: -(1) * -(1) = 1 :>p.
Lemma expKS n: (-(1)) ^n.+1 = -(-(1)) ^n.
Lemma expK2m1 n: (-(1)) ^ n * (- (1)) ^ n =1.
Lemma expK_add n1 n2 a: a ^ (n1 + n2) = a ^n1 * a ^ n2.
Lemma expKm1_even n: even n -> (-(1))^ n = 1
with expKm1_odd n: odd n -> (-(1))^ n = -(1).
Lemma expKm1_sub m n: m <= n -> (-(1))^ (n - m) = (-(1))^ (n + m).
Lemma expKm1_2 n: (-(1))^ (2 * n) = 1.
Lemma expKm1_2E n m: (-(1))^ (2 * n + m) = (-(1))^ m.
Lemma invKr x: x <> 0 -> x^-1 * x = 1.
Lemma opp_multK1l x: - x = (-(1)) * x.
Lemma opp_multK1r x: - x = x * (-(1)).
Lemma multK_m1_m1: -(1) * -(1) = 1 :>p.
Lemma expKS n: (-(1)) ^n.+1 = -(-(1)) ^n.
Lemma expK2m1 n: (-(1)) ^ n * (- (1)) ^ n =1.
Lemma expK_add n1 n2 a: a ^ (n1 + n2) = a ^n1 * a ^ n2.
Lemma expKm1_even n: even n -> (-(1))^ n = 1
with expKm1_odd n: odd n -> (-(1))^ n = -(1).
Lemma expKm1_sub m n: m <= n -> (-(1))^ (n - m) = (-(1))^ (n + m).
Lemma expKm1_2 n: (-(1))^ (2 * n) = 1.
Lemma expKm1_2E n m: (-(1))^ (2 * n + m) = (-(1))^ m.
Lemma invKr x: x <> 0 -> x^-1 * x = 1.
Cancelation rule for *
Lemma multK_cancel x y z: x <> 0 -> x * y = x * z -> y = z.
Lemma multK_swap x y z: x * (y * z) = y * (x * z).
Lemma multK_swap x y z: x * (y * z) = y * (x * z).
a field is integral
Lemma multK_integral x y : x * y = 0 -> x = 0 \/ y = 0.
Lemma expK_integral x n : x^n = 0 -> x = 0.
Lemma expKm1_n0 n : (-(1))^n <> 0.
Fixpoint n_to_K n :=
match n with O => 0: p | S n => (1 + n_to_K n) end.
Lemma n_to_K0: n_to_K 0 = 0.
Lemma n_to_K1: n_to_K 1 = 1.
Lemma n_to_K_add m n : n_to_K (m + n) = n_to_K m + n_to_K n.
Lemma n_to_K_minus m n : n <= m -> n_to_K (m - n) = n_to_K m + -n_to_K n.
Lemma n_to_K_mult m n : n_to_K (m * n) = n_to_K m * n_to_K n.
Definition Z_to_K (z: Z) :=
match z with
| Z0 => 0
| Zpos _ => n_to_K (Zabs_nat z)
| Zneg _ => - (n_to_K (Zabs_nat z))
end.
Lemma Z_to_K_opp (z: Z): Z_to_K (-z)%Z = - Z_to_K z.
Lemma Z_to_K_pos (z: Z): (0 <= z)%Z -> Z_to_K z = n_to_K (Zabs_nat z).
Lemma Z_to_K_add (z1 z2: Z):
Z_to_K (z1 + z2)%Z = Z_to_K z1 + Z_to_K z2.
Lemma Z_to_K_minus (z1 z2: Z):
Z_to_K (z1 - z2)%Z = Z_to_K z1 + - Z_to_K z2.
Lemma Z_to_K_mult (z1 z2: Z):
Z_to_K (z1 * z2)%Z = Z_to_K z1 * Z_to_K z2.
End ParamsProp.
Notation "x ^ k" := (expK _ x%f k) : field_scope.
Ltac Krm0 :=
repeat ((rewrite multK0l || rewrite multK0r || rewrite oppK0 ||
rewrite addK0l || rewrite addK0r)); auto.
Ltac Krm1 :=
Krm0;
repeat (rewrite multK1l || rewrite multK1r || rewrite <- opp_multKr ||
rewrite expK2m1 || rewrite <- opp_multKl || rewrite opp_oppK); auto.
Lemma expK_integral x n : x^n = 0 -> x = 0.
Lemma expKm1_n0 n : (-(1))^n <> 0.
Fixpoint n_to_K n :=
match n with O => 0: p | S n => (1 + n_to_K n) end.
Lemma n_to_K0: n_to_K 0 = 0.
Lemma n_to_K1: n_to_K 1 = 1.
Lemma n_to_K_add m n : n_to_K (m + n) = n_to_K m + n_to_K n.
Lemma n_to_K_minus m n : n <= m -> n_to_K (m - n) = n_to_K m + -n_to_K n.
Lemma n_to_K_mult m n : n_to_K (m * n) = n_to_K m * n_to_K n.
Definition Z_to_K (z: Z) :=
match z with
| Z0 => 0
| Zpos _ => n_to_K (Zabs_nat z)
| Zneg _ => - (n_to_K (Zabs_nat z))
end.
Lemma Z_to_K_opp (z: Z): Z_to_K (-z)%Z = - Z_to_K z.
Lemma Z_to_K_pos (z: Z): (0 <= z)%Z -> Z_to_K z = n_to_K (Zabs_nat z).
Lemma Z_to_K_add (z1 z2: Z):
Z_to_K (z1 + z2)%Z = Z_to_K z1 + Z_to_K z2.
Lemma Z_to_K_minus (z1 z2: Z):
Z_to_K (z1 - z2)%Z = Z_to_K z1 + - Z_to_K z2.
Lemma Z_to_K_mult (z1 z2: Z):
Z_to_K (z1 * z2)%Z = Z_to_K z1 * Z_to_K z2.
End ParamsProp.
Notation "x ^ k" := (expK _ x%f k) : field_scope.
Ltac Krm0 :=
repeat ((rewrite multK0l || rewrite multK0r || rewrite oppK0 ||
rewrite addK0l || rewrite addK0r)); auto.
Ltac Krm1 :=
Krm0;
repeat (rewrite multK1l || rewrite multK1r || rewrite <- opp_multKr ||
rewrite expK2m1 || rewrite <- opp_multKl || rewrite opp_oppK); auto.