module whileTestPrim where

open import Function
open import Data.Nat
open import Data.Bool hiding ( _≟_ )
open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality

open import utilities

record Env : Set where
  field
    varn : ℕ
    vari : ℕ
open Env

PrimComm : Set
PrimComm = Env → Env

Cond : Set
Cond = (Env → Bool) 

data Comm : Set where
  Skip  : Comm
  Abort : Comm
  PComm : PrimComm -> Comm
  Seq   : Comm -> Comm -> Comm
  If    : Cond -> Comm -> Comm -> Comm
  While : Cond -> Comm -> Comm

---------------------------

program : ℕ → Comm
program c10 = 
    Seq ( PComm (λ env → record env {varn = c10}))
    $ Seq ( PComm (λ env → record env {vari = 0}))
    $ While (λ env → lt zero (varn env ) )
      (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
        $ PComm (λ env → record env {varn = ((varn env) - 1)} ))

simple : ℕ → Comm
simple c10 = 
    Seq ( PComm (λ env → record env {varn = c10}))
    $  PComm (λ env → record env {vari = 0})

{-# TERMINATING #-}
interpret : Env → Comm → Env
interpret env Skip = env
interpret env Abort = env
interpret env (PComm x) = x env
interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
interpret env (If x then else) with x env
... | true = interpret env then
... | false = interpret env else
interpret env (While x comm) with x env
... | true = interpret (interpret env comm) (While x comm)
... | false = env

test1 : Env
test1 =  interpret ( record { vari = 0  ; varn = 0 } ) (program 10)

eval-proof : vari test1 ≡ 10
eval-proof = refl

tests : Env
tests =  interpret ( record { vari = 0  ; varn = 0 } ) (simple 10)


empty-case : (env : Env) → (( λ e → true ) env ) ≡ true 
empty-case _ = refl


Axiom : Cond -> PrimComm -> Cond -> Set
Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true

Tautology : Cond -> Cond -> Set
Tautology pre post = ∀ (env : Env) →  (pre env)  ⇒ (post env) ≡ true

_and_ :  Cond -> Cond -> Cond
x and y =  λ env → x env ∧ y env 

neg :  Cond -> Cond 
neg x  =  λ env → not ( x env )

data HTProof : Cond -> Comm -> Cond -> Set where
  PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
             (pr : Axiom bPre pcm bPost) ->
             HTProof bPre (PComm pcm) bPost
  SkipRule : (b : Cond) -> HTProof b Skip b
  AbortRule : (bPre : Cond) -> (bPost : Cond) ->
              HTProof bPre Abort bPost
  WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
                {bPost' : Cond} -> {bPost : Cond} ->
                Tautology bPre bPre' ->
                HTProof bPre' cm bPost' ->
                Tautology bPost' bPost ->
                HTProof bPre cm bPost
  SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
            {cm2 : Comm} -> {bPost : Cond} ->
            HTProof bPre cm1 bMid ->
            HTProof bMid cm2 bPost ->
            HTProof bPre (Seq cm1 cm2) bPost
  IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
           {bPre : Cond} -> {bPost : Cond} ->
           {b : Cond} ->
           HTProof (bPre and b) cmThen bPost ->
           HTProof (bPre and neg b) cmElse bPost ->
           HTProof bPre (If b cmThen cmElse) bPost
  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
              HTProof (bInv and b) cm bInv ->
              HTProof bInv (While b cm) (bInv and neg b)

initCond : Cond
initCond env = true

stmt1Cond : {c10 : ℕ} → Cond
stmt1Cond {c10} env = Equal (varn env) c10

init-case : {c10 :  ℕ} → (env : Env) → (( λ e → true  ⇒ stmt1Cond {c10} e ) (record { varn = c10 ; vari = vari env }) ) ≡ true 
init-case {c10} _ = impl⇒ ( λ cond → ≡→Equal refl )

init-type : {c10 :  ℕ} → Axiom (λ env → true) (λ env → record { varn = c10 ; vari = vari env }) (stmt1Cond {c10})
init-type {c10} env = init-case env

stmt2Cond : {c10 : ℕ} → Cond
stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0)

whileInv : {c10 : ℕ} → Cond
whileInv {c10} env = Equal ((varn env) + (vari env)) c10

whileInv' : {c10 : ℕ} → Cond
whileInv'{c10}  env = Equal ((varn env) + (vari env)) (suc c10) ∧ lt zero (varn env)

termCond : {c10 : ℕ} → Cond
termCond {c10} env = Equal (vari env) c10

lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
  begin
    (Equal (varn env) c10 ) ∧ true
  ≡⟨ ∧true ⟩
    Equal (varn env) c10 
  ≡⟨ cond ⟩
    true
  ∎ )

proofs : (c10 : ℕ) → HTProof initCond (simple c10) (stmt2Cond {c10})
proofs c10 =
      SeqRule {initCond} ( PrimRule (init-case {c10} ))
    $ PrimRule {stmt1Cond} {_} {stmt2Cond} (lemma1 {c10})

open import Data.Empty

open import Data.Nat.Properties

proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
proof1 c10 =
      SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
    $ SeqRule {λ e →  Equal (varn e) c10} ( PrimRule lemma1   )
    $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)}  lemma2 (
            WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10}
            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
                     $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
  where
     lemma21 : {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env ≡ c10
     lemma21 eq = Equal→≡ (∧-pi1 eq)
     lemma22 : {env : Env } → {c10 : ℕ} → stmt2Cond {c10} env ≡ true → vari env ≡ 0
     lemma22 eq = Equal→≡ (∧-pi2 eq)
     lemma23 :  {env : Env } → {c10 : ℕ} → stmt2Cond env ≡ true → varn env + vari env ≡ c10
     lemma23 {env} {c10} eq = let open ≡-Reasoning  in
          begin
            varn env + vari env
          ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq  ) ⟩
            c10 + vari env
          ≡⟨ cong ( \ x -> c10 + x) (lemma22 {env} {c10} eq ) ⟩
            c10 + 0
          ≡⟨ +-sym {c10} {0} ⟩
            0 + c10 
          ≡⟨⟩
            c10 
          ∎
     lemma2 :  {c10 : ℕ} → Tautology stmt2Cond whileInv
     lemma2 {c10} env = bool-case (stmt2Cond env) (
        λ eq → let open ≡-Reasoning  in
          begin
            (stmt2Cond env)  ⇒  (whileInv env)
          ≡⟨⟩
            (stmt2Cond env)  ⇒ ( Equal (varn env + vari env) c10 )
          ≡⟨  cong ( \ x -> (stmt2Cond  {c10} env)  ⇒ ( Equal x c10 ) ) ( lemma23 {env} eq ) ⟩
            (stmt2Cond env)  ⇒ (Equal c10 c10)
          ≡⟨ cong ( \ x -> (stmt2Cond {c10} env) ⇒ x ) (≡→Equal refl )  ⟩
            (stmt2Cond {c10} env)  ⇒  true
          ≡⟨ ⇒t ⟩
            true
          ∎
        ) (
         λ ne → let open ≡-Reasoning  in
          begin
            (stmt2Cond env)  ⇒  (whileInv env)
          ≡⟨ cong ( \ x -> x  ⇒  (whileInv env) ) ne ⟩
             false  ⇒  (whileInv {c10} env)
          ≡⟨ f⇒ {whileInv {c10} env} ⟩
            true
          ∎
        ) 
     lemma3 :   Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv'
     lemma3 env = impl⇒ ( λ cond →  let open ≡-Reasoning  in
          begin
            whileInv' (record { varn = varn env ; vari = vari env + 1 }) 
          ≡⟨⟩
             Equal (varn env + (vari env + 1)) (suc c10) ∧ (lt 0 (varn env) )
          ≡⟨ cong ( λ z → Equal (varn env + (vari env + 1)) (suc c10) ∧ z ) (∧-pi2 cond )  ⟩
             Equal (varn env + (vari env + 1)) (suc c10) ∧ true
          ≡⟨ ∧true ⟩
            Equal (varn env + (vari env + 1)) (suc c10)
          ≡⟨ cong ( \ x -> Equal x (suc c10) ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
            Equal ((varn env + vari env) + 1) (suc c10)
          ≡⟨ cong ( \ x -> Equal x (suc c10) ) +1≡suc ⟩
            Equal (suc (varn env + vari env)) (suc c10)
          ≡⟨ sym Equal+1 ⟩
            Equal ((varn env + vari env) ) c10
          ≡⟨ ∧-pi1  cond ⟩
            true
          ∎ )
     lemma41 : (env : Env ) → {c10 : ℕ} → (varn env + vari env) ≡ (suc c10) → lt 0 (varn env) ≡ true  → Equal ((varn env - 1) + vari env) c10 ≡ true
     lemma41 env {c10} c1 c2 =  let open ≡-Reasoning  in
          begin
            Equal ((varn env - 1) + vari env) c10
          ≡⟨ cong ( λ z → Equal ((z - 1 ) +  vari env ) c10 ) (sym (suc-predℕ=n c2) )  ⟩
            Equal ((suc (predℕ {varn env} c2 ) - 1) + vari env) c10
          ≡⟨⟩
            Equal ((predℕ {varn env} c2 ) + vari env) c10
          ≡⟨  Equal+1 ⟩
            Equal ((suc (predℕ {varn env} c2 )) + vari env) (suc c10)
          ≡⟨ cong ( λ z → Equal (z  +  vari env ) (suc c10) ) (suc-predℕ=n c2 )  ⟩
            Equal (varn env + vari env) (suc c10)
          ≡⟨ cong ( λ z → (Equal z (suc c10) )) c1 ⟩
            Equal (suc c10) (suc c10)
          ≡⟨ ≡→Equal refl ⟩
            true
          ∎
     lemma4 :  {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
     lemma4 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
          begin
            whileInv (record { varn = varn env - 1 ; vari = vari env })
          ≡⟨⟩
            Equal ((varn env - 1) + vari env) c10
          ≡⟨ lemma41 env (Equal→≡ (∧-pi1  cond)) (∧-pi2  cond) ⟩
            true
          ∎
        )
     lemma51 : (z : Env ) → neg (λ z → lt zero (varn z)) z ≡ true → varn z ≡ zero
     lemma51 z cond with lt zero (varn z) | (suc zero) ≤? (varn z)
     lemma51 z () | false | yes p
     lemma51 z () | true | yes p
     lemma51 z refl | _ | no ¬p with varn z
     lemma51 z refl | _ | no ¬p | zero = refl
     lemma51 z refl | _ | no ¬p | suc x = ⊥-elim ( ¬p (s≤s z≤n ) )
     lemma5 : {c10 : ℕ} →  Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond
     lemma5 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning  in
         begin
            termCond env
          ≡⟨⟩
             Equal (vari env) c10 
          ≡⟨⟩
             Equal (zero + vari env) c10 
          ≡⟨ cong ( λ z →  Equal (z + vari env) c10 )  (sym ( lemma51 env ( ∧-pi2  cond ) )) ⟩
             Equal (varn env + vari env) c10 
          ≡⟨ ∧-pi1  cond  ⟩
             true
          ∎
        )