Peano numbers are a semiring

peano.v

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.