module prob1 where

open import Relation.Binary.PropositionalEquality 
open import Relation.Binary.Core
open import Data.Nat
open import Data.Nat.Properties
open import logic
open import nat
open import Data.Empty
open import Data.Product
open import Relation.Nullary
-- open import Relation.Binary.Definitions

-- All variables are positive integer
-- A = -M*n + i +k*M  - M
-- where n is in range (0,…,k-1) and i is in range(0,…,M-1)
-- Goal: Prove that A can take all values of (0,…,k*M-1)
-- A1 = -M*n1 + i1 +k*M  M, A2 = -M*n2 + i2 +k*M  - M
-- (1) If n1!=n2 or i1!=i2 then A1!=A2
-- Or its contraposition: (2) if A1=A2 then n1=n2 and i1=i2
-- Proof by contradiction: Suppose A1=A2 and (n1!=n2 or i1!=i2) becomes
-- contradiction
-- Induction on n and i

record Cond1 (A M k : ℕ )  : Set where
   field
      n : ℕ 
      i : ℕ 
      range-n : n < k 
      range-i : i < M 
      rule1 : i + k * M  ≡ M * (suc n) + A    -- A ≡ (i + k * M ) - (M * (suc n)) 

--   k = 1 → n = 0 →  ∀ M → A = i
--   k = 2 → n = 1 →
--   i + 2 * M = M * (suc n) + A    i = suc n → A = 0 

record UCond1 (A M k : ℕ )  : Set where
   field
      c1 : Cond1 A M k
      unique-i : {j : ℕ} {m1  : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.i c1 ≡ j
      unique-n : {j : ℕ} {m1  : ℕ} → j < M → m1 < k → j + k * M ≡ M * suc m1 + A → Cond1.n c1 ≡ m1
      maxA : A ≤ ( k * M ) - 1

problem1-0 : (k A M : ℕ )  → (A<kM : suc A <  k * M )
    → UCond1 A M k 
problem1-0 zero A M () 
problem1-0 (suc k) A zero A<kM = ⊥-elim ( nat-<> A<kM (subst (λ x → x < suc A) (*-comm _ k ) 0<s ))
problem1-0 (suc k) A (suc m) A<kM = cc k a<sa (start-range k) where
     M = suc m
     cck :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M →  Cond1 A M (suc k)
     cck n n<k gt lt =  record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = lt ; rule1 = lemma2 }  where
        lemma2 :   A - ((k - n) * M) + suc k * M ≡ M * suc n + A
        lemma2 = begin
           A - ((k - n) * M) + suc k * M                           ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩
           A - ((k - n) * M) + (suc (((k - n) ) + n )) * M         ≡⟨ cong ( λ x → A - ((k - n) * M) + suc x * M ) (+-comm _ n) ⟩
           A - ((k - n) * M) + (suc (n + ((k - n) ) )) * M         ≡⟨⟩
           A - ((k - n) * M) + (suc n + ((k - n) ) ) * M           ≡⟨ cong ( λ x → A - ((k - n) * M) + x * M ) (+-comm (suc n) _) ⟩
           A - ((k - n) * M) + (((k - n) ) + suc n ) * M           ≡⟨ cong ( λ x → A - ((k - n) * M) + x  ) (((proj₂ *-distrib-+)) M ((k - n))  _  ) ⟩
           A - ((k - n) * M) + (((k - n) * M) + (suc n) * M)       ≡⟨ sym (+-assoc (A - ((k - n) * M)) _ ((suc n) * M)) ⟩
           A - ((k - n) * M) + ((k - n) * M) + (suc n) * M         ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {(k - n) * M}  gt ) ⟩
           A + (suc n) * M                                         ≡⟨ cong ( λ k → A + k ) (*-comm (suc n)  _ )  ⟩
           A + M * (suc n)                                         ≡⟨ +-comm A _ ⟩
           M * (suc n) + A
          ∎  where open ≡-Reasoning
     cck-u :  ( n : ℕ ) →  n < suc k  → (suc A >  ((k - n) ) * M )  → A - ((k - n) * M) < M → UCond1 A M (suc k)
     cck-u n n<k k<A i<M = c0 where
        c1 : Cond1 A M (suc k) 
        c1 = cck n n<k k<A i<M 
        lemma4 : {i j x y z : ℕ} → j + x ≡ y → i + x ≡ z → j < i → y < z
        lemma4 {i} {j} {x} refl refl (s≤s z≤n) = s≤s (subst (λ k → x ≤ k ) (+-comm x _) x≤x+y)
        lemma4 refl refl (s≤s (s≤s lt)) = s≤s (lemma4 refl refl (s≤s lt) )
        lemma5 : {m1 n : ℕ} →      M * suc m1 + A  < M * suc n + A
                           → M + (M * suc m1 + A) ≤ M * suc n + A  
        lemma5 {m1} {n} lt with <-cmp m1 n
        lemma5 {m1} {n} lt | tri< a ¬b ¬c = begin
                   M + (M * suc m1 + A)
               ≡⟨ sym (+-assoc M _ _ ) ⟩
                   (M + M * suc m1) + A
               ≡⟨ sym ( cong (λ k → (k + M * suc m1) + A) ((proj₂ *-identity) M )) ⟩
                   (M * suc zero + M * suc m1) + A
               ≡⟨  sym ( cong (λ k → k + A) (( proj₁ *-distrib-+  )  M (suc zero) _ )) ⟩
                   M * suc (suc m1) + A
               ≤⟨ ≤-plus {_} {_} {A} (subst₂ (λ x y → x ≤ y ) (*-comm _ M ) (*-comm _ M )  (*≤ (s≤s a))) ⟩
                   M * suc n + A
               ∎ where open ≤-Reasoning
        lemma5 {m1} {n} lt | tri≈ ¬a refl ¬c = ⊥-elim ( nat-<≡ lt )
        lemma5 {m1} {n} lt | tri> ¬a ¬b c = ⊥-elim ( nat-<> lt (<-plus {_} {_} {A} (<≤+ (s≤s c)
                (subst₂ (λ x y → x ≤ y ) (*-comm _ m ) (*-comm _ m ) (*≤ (s≤s (≤to< c)))))))
        lemma6 : {i j x : ℕ} → M + (j + x ) ≤ i + x → M ≤ i
        lemma6 {i} {j} {x} lt = ≤-minus {M} {i} {x} (x+y≤z→x≤z ( begin 
                 M + x + j 
               ≡⟨ +-assoc M _ _ ⟩
                 M + (x + j )
               ≡⟨ cong (λ k → M + k  ) (+-comm x _ ) ⟩
                 M + (j + x)
               ≤⟨ lt  ⟩
                 i + x 
               ∎ )) where open ≤-Reasoning
        i : ℕ
        i = A - ((k - n) * M)
        lemma-u1 : {j : ℕ} {m1 : ℕ} → j < i → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
        lemma-u1 {j} {m1} j<akM m1<k eq with <-cmp j M
        lemma-u1 {j} {m1} j<akM m1<k eq | tri< a ¬b ¬c =
            ⊥-elim (nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym eq) (sym (Cond1.rule1 c1 )) lemma3) ) i<M ) where
             lemma3 : M + (M * suc m1 + A) ≤ M * suc n + A   -- M + j ≤ i
             lemma3 = lemma5 (lemma4  eq (Cond1.rule1 c1) j<akM)
        lemma-u1 {j} {m1} j<akM m1<k eq | tri≈ ¬a b ¬c = ⊥-elim (nat-≡< b ( (≤-trans j<akM (≤-trans refl-≤s i<M )))) 
        lemma-u1 {j} {m1} j<akM m1<k eq | tri> ¬a ¬b c = ⊥-elim (nat-<> (≤-trans i<M (less-1 c)) j<akM ) 
        lemma-u2 : {j : ℕ} {m1  : ℕ} → (A - ((k - n) * M)) < j →
            j < M → m1 < suc k → ¬ j + suc k * M ≡ M * suc m1 + A
        lemma-u2 {j} {m1} i<j j<M m1<k eq = ⊥-elim ( nat-≤> (lemma6 (subst₂ (λ x y → M + x ≤ y) (sym (Cond1.rule1 c1)) (sym eq) lemma3-2)) j<M ) where
             lemma3-2 : M + (M * suc n + A) ≤ M * suc m1 + A -- M + i ≤ j
             lemma3-2 = lemma5 (lemma4 (Cond1.rule1 c1) eq i<j)
        unique-i : {j : ℕ} {m1  : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → i ≡ j
        unique-i {j} {m1} j<M m1<k eq with <-cmp i j
        unique-i {j} {m1} j<M m1<k eq | tri< a ¬b ¬c = ⊥-elim ( lemma-u2 a j<M m1<k eq  )
        unique-i {j} {m1} j<M m1<k eq | tri≈ ¬a b ¬c = b
        unique-i {j} {m1} j<M m1<k eq | tri> ¬a ¬b c = ⊥-elim ( lemma-u1 c m1<k eq  )
        lemma7 : {n m1 m A  : ℕ} → n < m1   → suc (n + m * suc n + A) < suc (m1 + m * suc m1 + A)
        lemma7 {n} {m1} {m} {A} n<m1 = begin
                  suc (suc (n + m * suc n + A))
               ≡⟨ +-assoc _ (m * suc n)  A ⟩
                  suc (suc n + (m * suc n + A))
               ≤⟨ s≤s (<-plus n<m1) ⟩
                  suc (m1 + (m * suc n + A))
               ≡⟨ sym ( +-assoc _ (m * suc n)  A) ⟩
                  suc (m1 + m * suc n + A)
               ≤⟨ ≤-plus {_} {_} {A} (≤-plus-0 {_} {_} {suc m1} (≤* {suc n} {suc m1} {m} (s≤s (≤to< n<m1 )))) ⟩ 
                  suc (m1 + m * suc m1 + A)
               ∎ where open ≤-Reasoning
        unique-m : {i j : ℕ} {n m1  : ℕ}  → i ≡ j → i + suc k * M ≡ M * suc n + A → j + suc k * M ≡ M * suc m1 + A → n ≡ m1
        unique-m {i} {_} {n} {m1} refl eqn eqm with <-cmp n m1
        unique-m {i} {_} {n} {m1} refl eqn eqm | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (sym (trans (sym eqm) eqn )) (lemma7 {n} {m1} {m} {A} a ))
        unique-m {i} {_} {n} {m1} refl eqn eqm | tri≈ ¬a b ¬c = b
        unique-m {i} {_} {n} {m1} refl eqn eqm | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (trans (sym eqm) eqn ) (lemma7 {m1} {n} {m} {A} c ))
        unique-n :  {j m1 : ℕ} → j < M → m1 < suc k → j + suc k * M ≡ M * suc m1 + A → n ≡ m1
        unique-n {j} {m1} j<M m1<k eq = unique-m (unique-i j<M m1<k eq ) (Cond1.rule1 c1) eq 
        --   A < M + ((k - n) * M)
        --   A < suc k * M - n * M  < suc k * M - n * M
        lemma8 : A - ((k - n) * M) < M  → A < M + ((k - n) * M) 
        lemma8 i<M with <-cmp (suc (suc A)) ( (k - n) * M )
        lemma8 i<M | tri< a ¬b ¬c = {!!}
        lemma8 i<M | tri≈ ¬a b ¬c = {!!}
        lemma8 i<M | tri> ¬a ¬b c = begin
                  suc A
               ≡⟨ sym ( minus+n {suc A} {(k - n) * M} c )  ⟩
                  (suc A - ((k - n) * M)) + (k - n) * M
               ≡⟨ {!!}  ⟩
                  suc ( (A - ((k - n) * M)) + ((k - n) * M) )
               ≤⟨  ≤-plus i<M  ⟩ 
                   M + ((k - n) * M)
               ∎ where open ≤-Reasoning
        lemma9 : {x y : ℕ } → suc x ≤ y → x ≤ y - 1
        lemma9 {zero} {zero} ()
        lemma9 {suc x} {zero} ()
        lemma9 {x} {suc y} (s≤s lt) = lt
        maxA : A - ((k - n) * M) < M  → A ≤ (suc k * M ) - 1
        maxA i<M = begin
                  A
               ≤⟨ lemma9 (lemma8 i<M ) ⟩ 
                  (M + ((k - n) * M)) - 1
               ≡⟨ cong (λ k → (M + k ) - 1 ) (distr-minus-* {k} {n} {M} ) ⟩ 
                  (M + ((k * M) - ( n * M))) - 1
               ≡⟨ {!!} ⟩ 
                  ((M + (k * M) )- ( n * M)) - 1
               ≡⟨⟩ 
                  ((suc k * M )- ( n * M)) - 1
               ≡⟨ {!!} ⟩ 
                  (suc k * M) - ((n * M) + 1)
               ≤⟨ {!!}  ⟩ 
                  (suc k * M ) - 1
               ∎ where open ≤-Reasoning
        c0  =  record { c1 = record { n = n ; i = A - (((k - n)) * M ) ; range-n = n<k   ; range-i = i<M; rule1 = Cond1.rule1 c1 }
            ; unique-i = unique-i 
            ; unique-n = unique-n
            ; maxA = maxA i<M
            }
     --  loop on  range  of A : ((k - n) ) * M ≤ A < ((k - n) ) * M + M
     nextc : (n : ℕ ) → (suc n < suc k) → M < suc ((k - n) * M) 
     nextc n n<k with k - n | inspect (_-_ k) n
     nextc n n<k | 0 | record { eq = e } = ⊥-elim ( nat-≡< (sym e) (minus>0 n<k) )
     nextc n n<k | suc n0 | _ = s≤s (s≤s lemma) where
        lemma : m ≤ m + n0 * suc m
        lemma = x≤x+y
     cc : (n : ℕ) → n < suc k → suc A > (k - n) * M → UCond1 A M (suc k)
     cc zero n<k k<A = cck-u 0 n<k k<A lemma where
        a<m : suc A < M + k * M 
        a<m = A<kM
        lemma : A - ((k - 0) * M) < M
        lemma = <-minus {_} {_} {k * M} (subst (λ x → x < M + k * M) (sym (minus+n {A} {k * M} k<A )) (less-1 a<m) )
     cc (suc n) n<k k<A with <-cmp (A - ((k - (suc n)) * M))  M
     cc (suc n) n<k k<A | tri< a ¬b ¬c = cck-u (suc n) n<k k<A a
     cc (suc n) n<k k<A | tri≈ ¬a b ¬c = 
        cc n (less-1 n<k) (lemma1 b)  where
        a=mk0 :  (A - ((k - (suc n)) * M)) ≡  M → A ≡ (k - n) * M
        a=mk0 a=mk = sym ( begin
           (k - n) * M 
         ≡⟨ sym ( minus+n {(k - n) * M} {M} (nextc n n<k )) ⟩
           ((k - n) * M ) - M + M
         ≡⟨ +-comm _ M ⟩
           M + (((k - n) * M ) - M)
         ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k} (<-minus-0 n<k ))) ⟩
           M + (k - (suc n) * M) 
         ≡⟨ cong (λ x → x + (k - (suc n)) * M) (sym a=mk) ⟩
           A - ((k - (suc n)) * M) + ((k - (suc n)) * M) 
         ≡⟨ minus+n {A} {(k - (suc n)) * M} k<A ⟩
           A
         ∎ ) where open ≡-Reasoning
        lemma1 : (A - ((k - (suc n)) * M)) ≡  M → suc A > (k - n) * M
        lemma1 a=mk = subst (λ x → (k - n) * M < suc x ) (sym (a=mk0 a=mk )) a<sa
     cc (suc n) n<k k<A | tri> ¬a ¬b c = 
        cc n (less-1 n<k) (lemma3 c) where
        lemma3 : (A - ((k - (suc n)) * M)) > M  → suc A > (k - n) * M
        lemma3 mk<a = <-trans lemma5 a<sa where
            lemma6 :  M + (k - (suc n)) * M ≡ (k - n) * M
            lemma6 = begin
                  M + (k - (suc n)) * M 
               ≡⟨ cong (λ x → M + x) (minus-* {M} {k} (<-minus-0 n<k))  ⟩
                  M + (((k - n) * M ) - M )
               ≡⟨ +-comm M _ ⟩
                  ((k - n) * M ) - M + M
               ≡⟨ minus+n {_} {M} (nextc n n<k ) ⟩
                  (k - n) * M
               ∎  where open ≡-Reasoning
            lemma4 : (M + (k - (suc n)) * M) < A
            lemma4 = subst (λ x → (M + (k - (suc n)) * M)  < x ) (minus+n {A}{(k - (suc n)) * M} k<A ) ( <-plus mk<a )
            lemma5 : (k - n) * M < A
            lemma5 = subst (λ x → x < A ) lemma6 lemma4
     start-range : (k : ℕ ) → suc A > (k - k) * M
     start-range zero = s≤s z≤n
     start-range (suc k) = start-range k