Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
Require Import fintype finfun bigop ssralg poly.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Delimit Scope int_scope with Z.
Local Open Scope int_scope.
Import GRing.Theory.

(* This is a definition of signed intergers as two copies of nat *)
Inductive int : Set := Posz of nat | Negz of nat.

(* We introduce a notation to interpret natural numbers as positive *)
(* numbers *)

Notation "n %:Z" := (Posz n : int)
  (at level 2, left associativity, format "n %:Z")  : int_scope.

(* And here we equip this type with various combinatorial structures using *)
(* the subType infrastructure *)

Definition natsum_of_int (m : int) : nat + nat :=
  match m with Posz p => inl _ p | Negz n => inr _ n end.

Definition int_of_natsum (m : nat + nat) :=
  match m with inl p => Posz p | inr n => Negz n end.

Lemma natsum_of_intK : cancel natsum_of_int int_of_natsum.
Proof. by case. Qed.

Definition int_eqMixin := CanEqMixin natsum_of_intK.
Definition int_countMixin := CanCountMixin natsum_of_intK.
Definition int_choiceMixin := CountChoiceMixin int_countMixin.
Canonical int_eqType := Eval hnf in EqType int int_eqMixin.
Canonical int_choiceType := Eval hnf in ChoiceType int int_choiceMixin.
Canonical int_countType := Eval hnf in CountType int int_countMixin.

(* Prove: *)
Lemma eqz_nat (m n : nat) : (Posz m == Posz n :> int) = (m == n :> nat).
Proof. 
Admitted.


Section intZmod.

Definition addz (m n : int) :=
  match m, n with
    | Posz m', Posz n' => Posz (m' + n')
    | Negz m', Negz n' => Negz (m' + n').+1
    | Posz m', Negz n' => if n' < m' then Posz (m' - n'.+1) else Negz (n' - m')
    | Negz n', Posz m' => if n' < m' then Posz (m' - n'.+1) else Negz (n' - m')
  end.

Definition oppz m := nosimpl
  match m with
    | Posz n => if n is (n'.+1)%N then Negz n' else Posz 0
    | Negz n => Posz (n.+1)%N
  end.

(* We cannot yet benefit from generic notations, since we are in the process of proving the required results. Hence we define temporary notations that will be subsumed by the generic ones when we will have defined the appropriate instances*)

Local Notation "0" := (0 : int) : int_scope.
Local Notation "-%Z" := (@oppz) : int_scope.
Local Notation "- x" := (oppz x) : int_scope.
Local Notation "+%Z" := (@addz) : int_scope.
Local Notation "x + y" := (addz x y) : int_scope.
Local Notation "x - y" := (x + - y) : int_scope.

Lemma PoszD : {morph Posz : m n / (m + n)%N >-> m + n}. Proof. done. Qed.

Local Coercion Posz : nat >-> int.

Lemma NegzE (n : nat) : Negz n = - n.+1. Proof. done. Qed.

(* Prouve the following induction scheme *)
Lemma new_int_rect (P : int -> Type) :
  P 0 -> (forall n : nat, P n -> P (n.+1))
  -> (forall n : nat, P (- n) -> P (- (n.+1)))
  -> forall n : int, P n.
Proof.
Admitted.

(* This is a way to obtain a tool for a more appropriate case analysis on *)
(* ints than the one provided by the structure of the type *)
CoInductive int_spec (x : int) : int -> Type :=
| ZintNull of x = 0 : int_spec x 0
| ZintPos n of x = n.+1 : int_spec x n.+1
| ZintNeg n of x = - (n.+1)%:Z : int_spec x (- n.+1).

(* We will use this lemma shortly after, when indicated by a comment *)
Lemma intP x : int_spec x x. Proof. by move: x=> [] []; constructor. Qed.


(* Prove the following lemmas when they are admitted*)
Lemma addzC : commutative addz.
Proof.
Admitted.

Lemma add0z : left_id 0 addz. 
Proof.
Admitted.

Lemma oppzK : involutive oppz. 
Proof.
Admitted.

(* This expresses that opposite distributes over the sum. Prove it *)
Lemma oppz_add : {morph oppz : m n / m + n}.
Proof.
Admitted.

Lemma add1Pz (n : int) : 1 + (n - 1) = n.
Proof.
(* Observe the effect of:*)
case: (intP n).
(* finish the proof *)
Admitted.

Lemma subSz1 (n : int) : 1 + n - 1 = n.
Proof.
Admitted.

Lemma addSnz (m : nat) (n : int) : (m.+1%N) + n = 1 + (m + n).
Proof.
Admitted.

Lemma addSz (m n : int) : (1 + m) + n = 1 + (m + n).
Proof.
case: m => [] m; first by rewrite -PoszD add1n addSnz.
rewrite !NegzE; apply: (inv_inj oppzK).
rewrite !oppz_add !oppzK addSnz [-1%:Z + _]addzC addSnz add1Pz.
by rewrite [-1%:Z + _]addzC subSz1.
Qed.

Lemma addPz (m n : int) : (m - 1) + n = (m + n) - 1.
Proof.
by apply: (inv_inj oppzK); rewrite !oppz_add oppzK [_ + 1]addzC addSz addzC.
Qed.

Lemma addzA : associative addz.
Proof.
Admitted.

Lemma addNz : left_inverse (0:int) oppz addz. Proof. by do 3?elim. Qed.

Lemma predn_int (n : nat) : 0 < n -> n.-1%:Z = n - 1.
Proof. by case: n=> // n _ /=; rewrite subn1. Qed.

(* And now we can define the mixin of commutative group *)
Definition int_zmodTypeMixin := ZmodMixin addzA addzC add0z addNz.

End intZmod.


Canonical int_ZmodType := ZmodType int int_zmodTypeMixin.

Open Scope ring_scope.

(* Now we benefit from the notations and theory of the structure of commutative group, because we have declared the canonical instance, and opened the appropriate notation scope *)

Lemma test : forall (F : nat -> int)(m n : nat), 
  \sum_(i < n | odd i) F i *+ m = (\sum_(i < n | odd i) F i) *+ m.
Proof. Admitted.