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 Relation.Nullary

minus : (a b : ℕ ) →  ℕ
minus a zero = a
minus zero (suc b) = zero
minus (suc a) (suc b) = minus a b

m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
m+= {i} {j} {zero} refl = refl
m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )

+m= : {i j  m : ℕ } → i + m ≡ j + m → i ≡ j
+m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )

less-1 :  { n m : ℕ } → suc n < m → n < m
less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)

sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
sa=b→a<b {0} {suc zero} refl = s≤s z≤n
sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)

minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
minus+n {zero} {suc y} (s≤s ())
minus+n {suc x} {suc y} (s≤s lt) = begin
           minus (suc x) (suc y) + suc y
        ≡⟨ +-comm _ (suc y)    ⟩
           suc y + minus x y 
        ≡⟨ cong ( λ k → suc k ) (
           begin
                 y + minus x y 
              ≡⟨ +-comm y  _ ⟩
                 minus x y + y
              ≡⟨ minus+n {x} {y} lt ⟩
                 x 
           ∎  
           ) ⟩
           suc x
        ∎  where open ≡-Reasoning

<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
<-minus-0 {x} {suc _} {zero} lt = lt
<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt

<-minus : {x y z : ℕ } → x + z < y + z → x < y
<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )

<-plus : {x y z : ℕ } → x < y → x + z < y + z 
<-plus = {!!}

distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) 
distr-minus-* = {!!}

minus- : {x y z : ℕ } → minus (minus x y) z ≡ minus x (y + z)
minus- = {!!}

minus-* : {M k n : ℕ } → minus k (suc n) * M ≡ minus (minus k n * M ) M
minus-* {M} {k} {n} = begin
           minus k (suc n) * M
        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
           minus (k * M ) ((suc n) * M)
        ≡⟨⟩
           minus (k * M ) (M + n * M  )
        ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
           minus (k * M ) ((n * M) + M )
        ≡⟨ sym ( minus- {k * M} {n * M} ) ⟩
           minus (minus (k * M ) (n * M)) M
        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
           minus (minus k n * M ) M
        ∎  where open ≡-Reasoning

-- 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 

open import Data.Product

problem : ( A M k : ℕ ) → Set 
problem A M k =  (suc A <  k * M ) → Cond1 A M k

problem0-k=k : ( k A M : ℕ ) → problem A M k
problem0-k=k zero A M ()
problem0-k=k (suc k) A M A<kM = cc k a<sa (start-range k) where
     cck :  ( n : ℕ ) →  n < suc k  → (suc A >  (minus k n ) * M )  → minus A (minus k n * M) < M →  Cond1 A M (suc k)
     cck n n<k gt lt =  record { n = n ; i = minus A ((minus k n) * M ) ; range-n = n<k   ; range-i = lt ; rule1 = lemma2 }  where
        lemma2 :   minus A (minus k n * M) + suc k * M ≡ M * suc n + A
        lemma2 = begin
           minus A (minus k n * M) + suc k * M                 ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (sym (minus+n {k} {n} n<k )) ⟩
           minus A (minus k n * M) + (suc ((minus k n ) + n )) * M ≡⟨ cong ( λ x → minus A (minus k n * M) + suc x * M ) (+-comm _ n) ⟩
           minus A (minus k n * M) + (suc (n + (minus k n ) )) * M ≡⟨⟩
           minus A (minus k n * M) + (suc n + (minus k n ) ) * M   ≡⟨ cong ( λ x → minus A (minus k n * M) + x * M ) (+-comm (suc n) _) ⟩
           minus A (minus k n * M) + ((minus k n ) + suc n ) * M   ≡⟨ cong ( λ x → minus A (minus k n * M) + x  ) (((proj₂ *-distrib-+)) M (minus k n)  _  ) ⟩
           minus A (minus k n * M) + ((minus k n * M) + (suc n) * M) ≡⟨ sym (+-assoc (minus A (minus k n * M)) _ ((suc n) * M)) ⟩
           minus A (minus k n * M) + (minus k n * M) + (suc n) * M ≡⟨ cong ( λ x → x + (suc n) * M ) ( minus+n {A} {minus 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
     --  loop on  range  of A : (minus k n ) * M ≤ A < (minus k n ) * M + M
     cc : (n : ℕ) → n < suc k → suc A > minus k n * M → Cond1 A M (suc k)
     cc zero n<k k<A = cck 0 n<k k<A lemma where
        a<m : suc A < M + k * M 
        a<m = A<kM
        lemma : minus A (minus 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 (minus A (minus k (suc n) * M))  M
     cc (suc n) n<k k<A | tri< a ¬b ¬c = cck (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
        lemma2 : suc (minus k n * M) > M
        lemma2 = {!!}
        a=mk0 :  (minus A (minus k (suc n) * M)) ≡  M → A ≡ minus k n * M
        a=mk0 a=mk = sym ( begin
           minus k n * M 
         ≡⟨ sym ( minus+n {minus k n * M} {M} lemma2 ) ⟩
           minus (minus k n * M ) M + M
         ≡⟨ +-comm _ M ⟩
           M + minus (minus k n * M ) M
         ≡⟨ cong (λ x → M + x ) (sym (minus-* {M} {k}  )) ⟩
           M + (minus k (suc n) * M) 
         ≡⟨ cong (λ x → x + minus k (suc n) * M) (sym a=mk) ⟩
           minus A (minus k (suc n) * M) + (minus k (suc n) * M) 
         ≡⟨ minus+n {A} {minus k (suc n) * M} k<A ⟩
           A
         ∎ ) where open ≡-Reasoning
        lemma1 : (minus A (minus k (suc n) * M)) ≡  M → suc A > minus k n * M
        lemma1 a=mk = subst (λ x → minus 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
        -- A > M + minus k (suc n) * M → A > M + minus k n - M → A >  minus k n
        lemma3 : (minus A (minus k (suc n) * M)) > M  → suc A > minus k n * M
        lemma3 mk<a = <-trans lemma5 a<sa where
            lemma4 : (M + minus k (suc n) * M) < A
            lemma4 = subst (λ x → (M + minus k (suc n) * M)  < x ) (minus+n {A}{minus k (suc n) * M} {!!} ) ( <-plus mk<a )
            lemma5 : minus k n * M < A
            lemma5 = subst (λ x → x < A ) {!!} lemma4
     start-range : (k : ℕ ) → suc A > minus k k * M
     start-range zero = s≤s z≤n
     start-range (suc k) = start-range k

problem0 : ( A M k : ℕ ) → M > 0 → k > 0 → (suc A <  k * M ) → Cond1 A M k
problem0 A (suc M) (suc k) 0<M 0<k A<kM = lemma1 k M A<kM a<sa a<sa where
    --- i loop in n loop
    lemma1-i : ( n i : ℕ ) → (suc A <  suc k * suc M ) → n < suc k → i < suc M →  Dec ( Cond1 A (suc M) (suc k) )
    lemma1-i n zero A<kM _ _ with <-cmp (1 + suc k * suc M ) (  suc M * suc n + A)
    lemma1-i n zero A<kM _ _ | tri< a ¬b ¬c = no {!!}
    lemma1-i n zero A<kM n<k i<M | tri≈ ¬a b ¬c = yes record { n = n ; i = suc zero ; range-n = n<k ; range-i = {!!} ; rule1 = b }
    lemma1-i n zero A<kM _ _ | tri> ¬a ¬b c = no {!!}
    lemma1-i n (suc i) A<kM _ _ with <-cmp (suc i + suc k * suc M ) (  suc M * suc n + A)
    lemma1-i n (suc i) A<kM n<k i<M | tri≈ ¬a b ¬c = yes record { n = n ; i = suc i ; range-n = n<k ; range-i = i<M ; rule1 = b }
    lemma1-i n (suc i) A<kM n<k i<M | tri< a ¬b ¬c = lemma1-i n i A<kM n<k (less-1 i<M)
    lemma1-i n (suc i) A<kM n<k i<M | tri> ¬a ¬b c = no {!!}
    --- n loop
    lemma1 : ( n i : ℕ ) → (suc A <  suc k * suc M ) → n < suc k → i < suc M →  Cond1 A (suc M) (suc k)
    lemma1 n i A<kM _ _ with <-cmp (i + suc k * suc M ) (  suc M * suc n + A)
    lemma1 n i A<kM n<k i<M | tri≈ ¬a b ¬c = record { n = n ; i = i ; range-n = n<k ; range-i = i<M ; rule1 = b }
    lemma1 zero i A<kM n<k i<M | tri< a ¬b ¬c = lemma2 i A<kM i<M where
         --- i + k * M ≡ M + A case
         lemma2 : (  i : ℕ ) → (suc A <  suc k * suc M ) → i < suc M →  Cond1 A (suc M) (suc k) 
         lemma2 zero A<kM i<M = {!!} -- A = A = k * M
         lemma2 (suc i) A<kM i<M with <-cmp ( suc i + suc k * suc M ) ( suc M * 1 + A)
         lemma2 (suc i) A<kM i<M | tri≈ ¬a b ¬c = record { n = zero ; i = suc i ; range-n = n<k ; range-i = i<M ; rule1 = b }
         lemma2 (suc i) A<kM i<M | tri< a ¬b ¬c = lemma2 i A<kM (less-1 i<M)
         lemma2 (suc i) A<kM i<M | tri> ¬a ¬b c = {!!}  -- can't happen
    lemma1 (suc n) i A<kM n<k i<M | tri< a ¬b ¬c with lemma1-i (suc n) i A<kM n<k i<M
    lemma1 (suc n) i A<kM n<k i<M | tri< a ¬b ¬c | yes p = p
    lemma1 (suc n) i A<kM n<k i<M | tri< a ¬b ¬c | no ¬p = lemma1 n i A<kM (less-1 n<k) i<M
    lemma1 n i A<kM n<k i<M | tri> ¬a ¬b c =  {!!}  where -- can't happen
         cannot1 :  { n k M i A : ℕ } → n < suc k → i < suc M →  (i + suc k * suc M ) > (  suc M * suc n + A)  → ¬ ( suc A <  suc k * suc M )
         cannot1 = {!!}

problem1 : (A1 A2 M k : ℕ ) 
    → (c1 : Cond1 A1 M k ) → (c2 : Cond1 A2 M k )
    → ( A1 ≡ A2 ) → (  Cond1.n c1  ≡ Cond1.n c2 ) ∧ ( Cond1.i c1  ≡ Cond1.i c2 )
problem1 = {!!}