File CoMoNum.Z
Require Import Arith Relations.
Inductive diffeq : (nat×nat) → (nat×nat) → Prop :=
| diffeq_1 : ∀ a b c d, a + d = b + c → diffeq (a,b) (c,d).
Infix "=Z" := diffeq (at level 80).
Theorem diffeq_reflexive : reflexive _ diffeq.
Proof.
intros [a b];
constructor;
apply Nat.add_comm.
Qed.
Theorem diffeq_symmetric : symmetric _ diffeq.
Proof.
intros ab cd [a b c d H1];
constructor;
symmetry.
rewrite (Nat.add_comm d a);
rewrite (Nat.add_comm c b);
exact H1.
Qed.
Theorem diffeq_transitive : transitive _ diffeq.
Proof.
Admitted.
Corollary diffeq_equivalence : equivalence _ diffeq.
Proof.
split.
-
exact diffeq_reflexive.
-
exact diffeq_transitive.
-
exact diffeq_symmetric.
Qed.
Definition Z : Set := nat×nat.
Theorem name_missing : ∀ a b k, diffeq (a,b) (a+k,b+k).
Proof.
intros a b k;
constructor.
rewrite Nat.add_assoc.
rewrite (Nat.add_comm a b).
rewrite <- Nat.add_assoc.
reflexivity.
Qed.
Definition addZ (x y : Z) : Z :=
let (a,b) := x in
let (c,d) := y in
(a+c,b+d).
Infix "+Z" := addZ (at level 10).
Theorem addZ_comm : ∀ x y, x +Z y =Z y +Z x.
Proof.
intros [a b] [c d];
constructor.
Admitted.
Theorem addZ_assoc : ∀ x y z, x +Z (y +Z z) =Z (x +Z y) +Z z.
Proof.
intros [a b] [c d] [e f];
constructor.
Admitted.
Definition mulZ (x y : Z) : Z :=
let (a,b) := x in
let (c,d) := y in
(a×c+b×d,a×d+b×c).
Infix "*Z" := mulZ (at level 9).
Theorem mulZ_comm : ∀ x y, x ×Z y =Z y ×Z x.
Proof.
intros [a b] [c d];
constructor.
Admitted.
Theorem mulZ_assoc : ∀ x y z, x ×Z (y ×Z z) =Z (x ×Z y) ×Z z.
Proof.
intros [a b] [c d] [e f];
constructor.
Admitted.
Theorem addZ_mulZ_distr : ∀ x y z, x ×Z (y +Z z) =Z x ×Z y +Z x ×Z z.
Proof.
intros [a b] [c d] [e f];
constructor.
Admitted.
Definition emb (x : nat) : Z := (x,0).
Theorem emb_add : ∀ x y, emb (x + y) =Z emb x +Z (emb y).
Proof.
intros x y;
constructor;
cbn.
apply Nat.add_0_r.
Qed.
Theorem emb_mul : ∀ x y, emb (x × y) =Z (emb x) ×Z (emb y).
Proof.
intros x y;
constructor;
cbn.
rewrite Nat.add_0_r.
rewrite Nat.mul_0_r.
reflexivity.
Qed.
Example minus_mul_minus_eq_plus : (0,1) ×Z (0,1) =Z (1,0).
Proof.
constructor;
reflexivity.
Qed.
Inductive diffeq : (nat×nat) → (nat×nat) → Prop :=
| diffeq_1 : ∀ a b c d, a + d = b + c → diffeq (a,b) (c,d).
Infix "=Z" := diffeq (at level 80).
Theorem diffeq_reflexive : reflexive _ diffeq.
Proof.
intros [a b];
constructor;
apply Nat.add_comm.
Qed.
Theorem diffeq_symmetric : symmetric _ diffeq.
Proof.
intros ab cd [a b c d H1];
constructor;
symmetry.
rewrite (Nat.add_comm d a);
rewrite (Nat.add_comm c b);
exact H1.
Qed.
Theorem diffeq_transitive : transitive _ diffeq.
Proof.
Admitted.
Corollary diffeq_equivalence : equivalence _ diffeq.
Proof.
split.
-
exact diffeq_reflexive.
-
exact diffeq_transitive.
-
exact diffeq_symmetric.
Qed.
Definition Z : Set := nat×nat.
Theorem name_missing : ∀ a b k, diffeq (a,b) (a+k,b+k).
Proof.
intros a b k;
constructor.
rewrite Nat.add_assoc.
rewrite (Nat.add_comm a b).
rewrite <- Nat.add_assoc.
reflexivity.
Qed.
Definition addZ (x y : Z) : Z :=
let (a,b) := x in
let (c,d) := y in
(a+c,b+d).
Infix "+Z" := addZ (at level 10).
Theorem addZ_comm : ∀ x y, x +Z y =Z y +Z x.
Proof.
intros [a b] [c d];
constructor.
Admitted.
Theorem addZ_assoc : ∀ x y z, x +Z (y +Z z) =Z (x +Z y) +Z z.
Proof.
intros [a b] [c d] [e f];
constructor.
Admitted.
Definition mulZ (x y : Z) : Z :=
let (a,b) := x in
let (c,d) := y in
(a×c+b×d,a×d+b×c).
Infix "*Z" := mulZ (at level 9).
Theorem mulZ_comm : ∀ x y, x ×Z y =Z y ×Z x.
Proof.
intros [a b] [c d];
constructor.
Admitted.
Theorem mulZ_assoc : ∀ x y z, x ×Z (y ×Z z) =Z (x ×Z y) ×Z z.
Proof.
intros [a b] [c d] [e f];
constructor.
Admitted.
Theorem addZ_mulZ_distr : ∀ x y z, x ×Z (y +Z z) =Z x ×Z y +Z x ×Z z.
Proof.
intros [a b] [c d] [e f];
constructor.
Admitted.
Definition emb (x : nat) : Z := (x,0).
Theorem emb_add : ∀ x y, emb (x + y) =Z emb x +Z (emb y).
Proof.
intros x y;
constructor;
cbn.
apply Nat.add_0_r.
Qed.
Theorem emb_mul : ∀ x y, emb (x × y) =Z (emb x) ×Z (emb y).
Proof.
intros x y;
constructor;
cbn.
rewrite Nat.add_0_r.
rewrite Nat.mul_0_r.
reflexivity.
Qed.
Example minus_mul_minus_eq_plus : (0,1) ×Z (0,1) =Z (1,0).
Proof.
constructor;
reflexivity.
Qed.