open import Level renaming ( suc to Suc ; zero to Zero )
module hoare where

open import Data.Nat
open import Data.Nat.Properties
-- open import Data.Bool hiding (_≤?_ ; _≤_)
-- open import Data.Product renaming ( _×_ to _/\_ )
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_; Dec; yes; no)
open import logic

record Env : Set (Suc Zero) where
   field
        varn : ℕ
        vari : ℕ
open Env

Statement : Set (Suc Zero)
Statement = {t : Set} → Env → (Env → t ) → t

Cond : Set (Suc Zero)
Cond = Env → Set

whileTest :  {t : Set (Suc Zero) }  → (c10 : ℕ) → (Env → t) → t
whileTest c10 next = next ( record {varn = c10 ; vari = 0 } )

lt :  ℕ → ℕ → Bool
lt zero zero = false
lt (suc _) zero = false
lt zero (suc _) = true
lt (suc x) (suc y) = lt x y

open import nat 
-- _-_ : ℕ → ℕ → ℕ
-- zero - zero = zero
-- zero - suc y = zero
-- suc x - zero = suc x
-- suc x - suc y = x - y

{-# TERMINATING #-}
whileLoop : {t : Set (Suc Zero)} → Env → (Env → t) → t
whileLoop env next with lt 0 (varn env)
whileLoop env next | false = next env
whileLoop env next | true =
   whileLoop (record env {varn = (varn env) - 1 ; vari = (vari env) + 1}) next

test1 : Env
test1 = whileTest 10 (λ env → whileLoop env (λ env1 → env1 ))

assert1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
assert1 = refl

-- proof1 : (n : ℕ ) → whileTest n (λ env → whileLoop env (λ e → (vari e) ≡ n ))
-- proof1 = {!!}

{-# TERMINATING #-}
whileLoop' : {l : Level} {t : Set l} → (env : Env ) → {c10 :  ℕ } → ((varn env) + (vari env) ≡ c10) → (Code : Env  → t) → t
whileLoop' env proof next with  ( suc zero  ≤? (varn  env) )
whileLoop' env proof next       | no p = next env
whileLoop' env {c10} proof next | yes p = whileLoop' record env {varn = (varn  env) - 1 ; vari = (vari env) + 1} (proof3 proof p ) next
    where
          env1 = record env {varn = (varn  env) - 1 ; vari = (vari env) + 1}
          proof3 : varn env + vari env ≡ c10 → (suc zero  ≤ (varn  env))  → varn env1 + vari env1 ≡ c10
          proof3 n+i=c 0<n = begin
              varn env1 + vari env1 ≡⟨⟩
              (varn env - 1) + (vari env + 1) ≡⟨ cong (λ k → (varn env - 1 ) + k ) (+-comm _ 1 ) ⟩
              (varn env - 1) + (1 + vari env ) ≡⟨ sym (+-assoc _ 1 _) ⟩ -- 1 ≤ varn env
              ((varn env - 1) + 1 )+ vari env  ≡⟨ cong (λ k → k + vari env) (minus+n {_} {1} (s≤s p)) ⟩
              varn env + vari env ≡⟨ proof ⟩
              c10
            ∎ where open ≡-Reasoning  

open _∧_

-- Condition to Invariant
conversion1 : {l : Level} {t : Set l } → (env : Env ) → {c10 :  ℕ } → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10)
               → (Code : (env1 : Env ) → (varn env1 + vari env1 ≡ c10) → t) → t
conversion1 env {c10} p1 next = next env proof4
   where
      proof4 : varn env + vari env ≡ c10
      proof4 = let open ≡-Reasoning  in
          begin
            varn env + vari env
          ≡⟨ cong ( λ n → n + vari env ) (proj2 p1) ⟩
            c10 + vari env
          ≡⟨ cong ( λ n → c10 + n ) (proj1 p1) ⟩
            c10 + 0
          ≡⟨ +-comm _ 0 ⟩
            c10
          ∎

whileTest' : {l : Level} {t : Set l}  →  {c10 :  ℕ } → (Code : (env : Env )  → ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) → t) → t
whileTest' {_} {_}  {c10} next = next env proof2
  where
    env : Env
    env = record {vari = 0 ; varn = c10 }
    proof2 : ((vari env) ≡ 0) ∧ ((varn env) ≡ c10) -- PostCondition
    proof2 = record { proj1 = refl ; proj2 =  refl }

-- all proofs are connected
proofGears : {c10 :  ℕ } → Set
proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 ))))

-- proof2 : {c10 :  ℕ } → proofGears  {c10}
-- proof2 {c10} = {!!}

data _implies_ {l m : Level}  (A : Set l ) (B : Set m)  : Set (l Level.⊔  m) where
    proof : ( A → B ) → A implies B

--    ind1 : {Inv : ℕ → Set l} → A →  (∀(i : ℕ) → Inv i) → B  → A implies B

-- step : {l m n : Level} {t : Set l} {A : Set l } {B : Set m} {C : Set n} (F : A → (B → t) → t ) →  
-- step = ?

data WhileTestState (c10 : ℕ) (env : Env)  : Set where
  S1 : (vari env ≡ 0) ∧ (varn env ≡ c10 ) → WhileTestState c10 env
  S2 : varn env + vari env ≡ c10 → WhileTestState c10 env
  Sf : vari env ≡ c10 → WhileTestState c10 env

proofGears1 : {c10 : ℕ } →
    whileTest' {_} {_} {c10} (λ n p1 →
    conversion1 n p1 (λ n1 p2 →
    whileLoop' n1 p2 (λ n2 →  vari n2 ≡ c10 )))
proofGears1 {c10} = {!!} where
     lemma2 : whileTest' {Level.suc Level.zero} {_} {c10} (λ n p1 → (vari n ≡ 0) ∧ (varn n ≡ c10 ))
     lemma2 = record { proj1 = refl ; proj2 =  refl }
     lemma4 : {n : Env} → (p2 : ((varn n) + (vari n) ≡ c10)) → whileLoop' n p2 (λ n2 →  vari n2 ≡ c10)
     lemma4 {record { varn = zero ; vari = i }} p2 = p2
     lemma4 {record { varn = suc n ; vari = i }} p2 with lemma4 {record { varn = n - 0; vari = i + 1 }} {!!} 
     ... | t = {!!}