Created
April 25, 2020 13:13
-
-
Save kendfrey/5a58c29715b5e102b24df5bc6a5ddccd to your computer and use it in GitHub Desktop.
Peano numbers are a semiring
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Setoid. | |
Declare Scope peano_scope. | |
Delimit Scope peano_scope with peano. | |
Open Scope peano_scope. | |
Axiom peano : Type -> Prop. | |
Axiom O : Type. | |
Axiom o_peano : peano O. | |
Hint Resolve o_peano : peano. | |
Axiom S : Type -> Type. | |
Axiom s_closed : forall x : Type, peano x -> peano (S x). | |
Hint Resolve s_closed : peano. | |
Axiom eq : Type -> Type -> Prop. | |
Infix ".=" := eq (at level 70, no associativity) : peano_scope. | |
Axiom eq_sym : forall x y : Type, peano x -> peano y -> x .= y -> y .= x. | |
Axiom eq_trans : forall x y z : Type, peano x -> peano y -> peano z -> x .= y -> y .= z -> x .= z. | |
Axiom s_inj : forall x y : Type, peano x -> peano y -> S x .= S y <-> x .= y. | |
Axiom s_neq_o : forall x : Type, peano x -> ~S x .= O. | |
Hint Resolve eq_sym : peano. | |
Hint Resolve eq_trans : peano. | |
Hint Extern 1 => rewrite s_inj : peano. | |
Hint Resolve s_neq_o : peano. | |
Axiom peano_ind : forall P : Type -> Prop, P O -> (forall x, peano x -> P x -> P (S x)) -> forall x, peano x -> P x. | |
Axiom add : Type -> Type -> Type. | |
Infix ".+" := add (at level 50, left associativity) : peano_scope. | |
Axiom add_closed : forall x y : Type, peano x -> peano y -> peano (x .+ y). | |
Axiom add_o : forall x : Type, peano x -> O .+ x .= x. | |
Axiom add_s : forall x y : Type, peano x -> peano y -> S x .+ y .= S (x .+ y). | |
Hint Resolve add_closed : peano. | |
Hint Resolve add_o : peano. | |
Hint Resolve add_s : peano. | |
Theorem add_o_r : forall x : Type, peano x -> x .+ O .= x. | |
Proof with auto with peano. | |
intros x x_peano. | |
apply (peano_ind (fun x => x .+ O .= x))... | |
clear dependent x. | |
intros x x_peano IHx. | |
apply (eq_trans _ (S (x .+ O)))... | |
Qed. | |
Hint Resolve add_o_r : peano. | |
Theorem add_comm : forall x y : Type, peano x -> peano y -> x .+ y .= y .+ x. | |
Proof with auto with peano. | |
intros x y x_peano y_peano. | |
generalize dependent y. | |
apply (peano_ind (fun x => forall y : Type, peano y -> x .+ y .= y .+ x))... | |
{ | |
intros y y_peano. | |
apply (eq_trans _ y)... | |
} | |
clear dependent x. | |
intros x x_peano IHx y y_peano. | |
apply (eq_trans _ (S (x .+ y)))... | |
apply (eq_trans _ (S (y .+ x)))... | |
apply (peano_ind (fun y => S (y .+ x) .= y .+ S x))... | |
{ | |
apply (eq_trans _ (S x))... | |
} | |
clear dependent y. | |
intros y y_peano IHy. | |
apply (eq_trans _ (S (S (y .+ x))))... | |
apply (eq_trans _ (S (y .+ S x)))... | |
Qed. | |
Hint Resolve add_comm : peano. | |
Theorem add_cancel : forall x y z : Type, peano x -> peano y -> peano z -> x .+ y .= x .+ z <-> y .= z. | |
Proof with auto with peano. | |
intros x y z x_peano y_peano z_peano. | |
split. | |
- apply (peano_ind (fun x => x .+ y .= x .+ z -> y .= z))... | |
{ | |
intros H. | |
apply (eq_trans _ (O .+ y))... | |
apply (eq_trans _ (O .+ z))... | |
} | |
clear dependent x. | |
intros x x_peano IHx H. | |
apply IHx. | |
rewrite <- s_inj... | |
apply (eq_trans _ (S x .+ y))... | |
apply (eq_trans _ (S x .+ z))... | |
- apply (peano_ind (fun x => y .= z -> x .+ y .= x .+ z))... | |
{ | |
intros H. | |
apply (eq_trans _ y)... | |
apply (eq_trans _ z)... | |
} | |
clear dependent x. | |
intros x x_peano IHx H. | |
apply (eq_trans _ (S (x .+ y)))... | |
apply (eq_trans _ (S (x .+ z)))... | |
Qed. | |
Hint Extern 1 => rewrite add_cancel : peano. | |
Theorem add_cancel_r : forall x y z : Type, peano x -> peano y -> peano z -> x .+ z .= y .+ z <-> x .= y. | |
Proof with auto with peano. | |
intros x y z x_peano y_peano z_peano. | |
split. | |
- intros H. | |
apply (add_cancel z)... | |
apply (eq_trans _ (x .+ z))... | |
apply (eq_trans _ (y .+ z))... | |
- intros H. | |
apply (eq_trans _ (z .+ x))... | |
apply (eq_trans _ (z .+ y))... | |
Qed. | |
Hint Extern 1 => rewrite add_cancel_r : peano. | |
Theorem add_assoc : forall x y z : Type, peano x -> peano y -> peano z -> x .+ (y .+ z) .= x .+ y .+ z. | |
Proof with auto with peano. | |
intros x y z x_peano y_peano z_peano. | |
apply (peano_ind (fun x => x .+ (y .+ z) .= x .+ y .+ z))... | |
{ | |
apply (eq_trans _ (y .+ z))... | |
} | |
clear dependent x. | |
intros x x_peano IHx. | |
apply (eq_trans _ (S (x .+ (y .+ z))))... | |
apply (eq_trans _ (S (x .+ y .+ z)))... | |
apply (eq_trans _ (S (x .+ y) .+ z))... | |
Qed. | |
Hint Resolve add_assoc : peano. | |
Axiom mul : Type -> Type -> Type. | |
Infix ".*" := mul (at level 40, left associativity) : peano_scope. | |
Axiom mul_closed : forall x y : Type, peano x -> peano y -> peano (x .* y). | |
Axiom mul_o : forall x : Type, peano x -> O .* x .= O. | |
Axiom mul_s : forall x y : Type, peano x -> peano y -> S x .* y .= y .+ x .* y. | |
Hint Resolve mul_closed : peano. | |
Hint Resolve mul_o : peano. | |
Hint Resolve mul_s : peano. | |
Theorem mul_o_r : forall x : Type, peano x -> x .* O .= O. | |
Proof with auto with peano. | |
intros x x_peano. | |
apply (peano_ind (fun x => x .* O .= O))... | |
clear dependent x. | |
intros x x_peano IHx. | |
apply (eq_trans _ (O .+ x .* O))... | |
apply (eq_trans _ (x .* O))... | |
Qed. | |
Hint Resolve mul_o_r : peano. | |
Theorem mul_s_r : forall x y : Type, peano x -> peano y -> x .* S y .= x .+ x .* y. | |
Proof with auto with peano. | |
intros x y x_peano y_peano. | |
apply (peano_ind (fun x => x .* S y .= x .+ x .* y))... | |
{ | |
apply (eq_trans _ O)... | |
apply (eq_trans _ (O .* y))... | |
} | |
clear dependent x. | |
intros x x_peano IHx. | |
apply (eq_trans _ (S y .+ x .* S y))... | |
apply (eq_trans _ (S (y .+ x .* S y)))... | |
apply eq_sym... | |
apply (eq_trans _ (S (x .+ S x .* y)))... | |
rewrite s_inj... | |
apply (eq_trans _ (x .+ (y .+ x .* y)))... | |
apply (eq_trans _ (x .+ y .+ x .* y))... | |
apply (eq_trans _ (y .+ x .+ x .* y))... | |
apply (eq_trans _ (y .+ (x .+ x .* y)))... | |
Qed. | |
Hint Resolve mul_s_r : peano. | |
Theorem mul_comm : forall x y : Type, peano x -> peano y -> x .* y .= y .* x. | |
Proof with auto with peano. | |
intros x y x_peano y_peano. | |
apply (peano_ind (fun x => x .* y .= y .* x))... | |
{ | |
apply (eq_trans _ O)... | |
} | |
clear dependent x. | |
intros x x_peano IHx. | |
apply (eq_trans _ (y .+ x .* y))... | |
apply (eq_trans _ (y .+ y .* x))... | |
Qed. | |
Hint Resolve mul_comm : peano. | |
Theorem mul_cancel : forall x y z : Type, peano x -> peano y -> peano z -> x .* y .= x .* z <-> (~x .= O -> y .= z). | |
Proof with auto with peano. | |
intros x y z x_peano y_peano z_peano. | |
split. | |
- apply (peano_ind (fun x => x .* y .= x .* z -> ~ x .= O -> y .= z))... | |
{ | |
intros _ contra. | |
contradict contra. | |
apply (eq_trans _ (O .+ O))... | |
} | |
clear dependent x. | |
intros x x_peano _ H _. | |
generalize dependent z. | |
apply (peano_ind (fun y => forall z : Type, peano z -> S x .* y .= S x .* z -> y .= z))... | |
{ | |
intros z z_peano H. | |
apply (eq_trans (O .+ x .* O)) in H... | |
apply (eq_trans (x .* O)) in H... | |
apply (eq_trans O) in H... | |
generalize dependent H. | |
apply (peano_ind (fun z => O .= S x .* z -> O .= z))... | |
{ | |
intros H. | |
apply (eq_trans _ _ O) in H... | |
} | |
clear dependent z. | |
intros z z_peano _ H. | |
exfalso. | |
apply (eq_trans _ _ (S z .+ x .* S z)) in H... | |
apply (eq_trans _ _ (S (z .+ x .* S z))) in H... | |
apply eq_sym in H... | |
apply s_neq_o in H... | |
} | |
clear dependent y. | |
intros y y_peano IHy z z_peano. | |
apply (peano_ind (fun z => S x .* S y .= S x .* z -> S y .= z))... | |
{ | |
intros H. | |
exfalso. | |
apply (eq_trans _ _ O) in H... | |
apply (eq_trans (S y .+ x .* S y)) in H... | |
apply (eq_trans (S (y .+ x .* S y))) in H... | |
- apply s_neq_o in H... | |
- apply eq_sym... | |
} | |
clear dependent z. | |
intros z z_peano _ H. | |
rewrite s_inj... | |
apply IHy... | |
rewrite <- (add_cancel (S x))... | |
apply (eq_trans (S x .+ S x .* y)) in H... | |
apply (eq_trans _ _ (S x .+ S x .* z)) in H... | |
- apply (peano_ind (fun x => (~ x .= O -> y .= z) -> x .* y .= x .* z))... | |
{ | |
intros _. | |
apply (eq_trans _ O)... | |
} | |
clear dependent x. | |
intros x x_peano IHx H. | |
apply (eq_trans _ (y .+ x .* y))... | |
apply (eq_trans _ (z .+ x .* z))... | |
apply (eq_trans _ (z .+ x .* y))... | |
Qed. | |
Hint Extern 1 => rewrite mul_cancel : peano. | |
Theorem mul_cancel_r : forall x y z : Type, peano x -> peano y -> peano z -> x .* z .= y .* z <-> (~z .= O -> x .= y). | |
Proof with auto with peano. | |
intros x y z x_peano y_peano z_peano. | |
split. | |
- intros H z_pos. | |
apply (mul_cancel z)... | |
apply (eq_trans _ (x .* z))... | |
apply (eq_trans _ (y .* z))... | |
- intros H. | |
apply (eq_trans _ (z .* x))... | |
apply (eq_trans _ (z .* y))... | |
Qed. | |
Hint Extern 1 => rewrite mul_cancel_r : peano. | |
Theorem mul_distr : forall x y z : Type, peano x -> peano y -> peano z -> x .* y .+ x .* z .= x .* (y .+ z). | |
Proof with auto with peano. | |
intros x y z x_peano y_peano z_peano. | |
apply (peano_ind (fun x => x .* y .+ x .* z .= x .* (y .+ z)))... | |
{ | |
apply (eq_trans _ (O .+ O .* z))... | |
apply (eq_trans _ (O .+ O))... | |
apply (eq_trans _ O)... | |
} | |
clear dependent x. | |
intros x x_peano IHx. | |
apply (eq_trans _ (y .+ z .+ x .* (y .+ z)))... | |
apply (eq_trans _ (y .+ x .* y .+ S x .* z))... | |
apply (eq_trans _ (y .+ x .* y .+ (z .+ x .* z)))... | |
apply eq_sym... | |
apply (eq_trans _ (y .+ (x .* y .+ (z .+ x .* z))))... | |
apply (eq_trans _ (y .+ (z .+ x .* z .+ x .* y)))... | |
apply (eq_trans _ (y .+ (z .+ (x .* z .+ x .* y))))... | |
apply eq_sym... | |
apply (eq_trans _ (y .+ (z .+ x .* z .+ x .* y)))... | |
apply (eq_trans _ (y .+ (z .+ x .* (y .+ z))))... | |
apply add_cancel... | |
apply (eq_trans _ (z .+ (x .* z .+ x .* y)))... | |
apply add_cancel... | |
apply (eq_trans _ (x .* y .+ x .* z))... | |
Qed. | |
Hint Resolve mul_distr : peano. | |
Theorem mul_distr_r : forall x y z : Type, peano x -> peano y -> peano z -> x .* z .+ y .* z .= (x .+ y) .* z. | |
Proof with auto with peano. | |
intros x y z x_peano y_peano z_peano. | |
apply (eq_trans _ (z .* (x .+ y)))... | |
apply (eq_trans _ (z .* x .+ y .* z))... | |
apply (eq_trans _ (z .* x .+ z .* y))... | |
Qed. | |
Hint Resolve mul_distr_r : peano. | |
Theorem mul_assoc : forall x y z : Type, peano x -> peano y -> peano z -> x .* (y .* z) .= x .* y .* z. | |
Proof with auto with peano. | |
intros x y z x_peano y_peano z_peano. | |
generalize dependent z. | |
generalize dependent y. | |
apply (peano_ind (fun x => forall y : Type, peano y -> forall z : Type, peano z -> x .* (y .* z) .= x .* y .* z))... | |
{ | |
intros y y_peano z z_peano. | |
apply (eq_trans _ O)... | |
apply (peano_ind (fun z => O .= O .* y .* z))... | |
clear dependent z. | |
intros z z_peano IHz. | |
apply (eq_trans _ (O .* y .+ O .* y .* z))... | |
apply (eq_trans _ (O .+ O .* y .* z))... | |
apply (eq_trans _ (O .* y .* z))... | |
} | |
clear dependent x. | |
intros x x_peano IHx y y_peano z z_peano. | |
apply (eq_trans _ (y .* z .+ x .* (y .* z)))... | |
apply (eq_trans _ ((y .+ x .* y) .* z))... | |
apply (eq_trans _ (y .* z .+ x .* y .* z))... | |
Qed. | |
Hint Resolve mul_assoc : peano. | |
Theorem mul_i : forall x : Type, peano x -> S O .* x .= x. | |
Proof with auto with peano. | |
intros x x_peano. | |
apply (eq_trans _ (x .+ O .* x))... | |
apply (eq_trans _ (x .+ O))... | |
Qed. | |
Theorem mul_i_r : forall x : Type, peano x -> x .* S O .= x. | |
Proof with auto with peano. | |
intros x x_peano. | |
apply (eq_trans _ (S O .* x))... | |
apply mul_i... | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment