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


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

_-_ : ℕ -> ℕ -> ℕ
x - zero  = x
zero - _  = zero
(suc x) - (suc y)  = x - y

lt : ℕ -> ℕ -> Bool
lt x y with suc x  ≤? y
lt x y | yes p = true
lt x y | no ¬p = false

Equal : ℕ -> ℕ -> Bool
Equal x y with x ≟ y
Equal x y | yes p = true
Equal x y | no ¬p = false

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

implies : Bool → Bool → Bool
implies false _ = true
implies true true = true
implies true false = false

impl-1 : {x : Bool} → implies x true  ≡ true
impl-1 {x} with x
impl-1 {x} | false = refl
impl-1 {x} | true = refl

impl-2 : {x : Bool} → implies false x  ≡ true
impl-2 {x} with x
impl-2 {x} | false = refl
impl-2 {x} | true = refl

and-lemma-1 : { x y : Bool } → x  ∧  y  ≡ true  → x  ≡ true
and-lemma-1 {x} {y} eq with x | y | eq
and-lemma-1 {x} {y} eq | false | b | ()
and-lemma-1 {x} {y} eq | true | false | ()
and-lemma-1 {x} {y} eq | true | true | refl = refl

and-lemma-2 : { x y : Bool } →  x  ∧  y  ≡ true  → y  ≡ true
and-lemma-2 {x} {y} eq with x | y | eq
and-lemma-2 {x} {y} eq | false | b | ()
and-lemma-2 {x} {y} eq | true | false | ()
and-lemma-2 {x} {y} eq | true | true | refl = refl

bool-case : ( x : Bool ) { p : Set } → ( x ≡ true  → p ) → ( x ≡ false  → p ) → p
bool-case x T F with x
bool-case x T F | false = F refl
bool-case x T F | true = T refl

impl :  {x y : Bool} → (x  ≡ true → y  ≡ true ) → implies x y  ≡ true
impl {x} {y} p = bool-case x (λ x=t →   let open ≡-Reasoning  in
          begin
            implies x y
          ≡⟨  cong ( \ z -> implies x z ) (p x=t ) ⟩
            implies x true
          ≡⟨ impl-1 ⟩
            true
          ∎
    ) ( λ x=f →  let open ≡-Reasoning  in
          begin
            implies x y
          ≡⟨  cong ( \ z -> implies z y ) x=f ⟩
            true
          ∎
  )
 
eqlemma : { x y : ℕ } →  Equal x y ≡ true → x ≡ y
eqlemma {x} {y} eq with x ≟ y
eqlemma {x} {y} refl | yes refl = refl
eqlemma {x} {y} () | no ¬p 

eqlemma1 : { x y : ℕ } →  Equal x y ≡ Equal (suc x) (suc y)
eqlemma1 {x} {y} with  x ≟ y
eqlemma1 {x} {.x} | yes refl = refl
eqlemma1 {x} {y} | no ¬p = refl

add-lemma1 : { x : ℕ } → x + 1 ≡ suc x
add-lemma1 {zero} = refl
add-lemma1 {suc x} = cong ( \ z -> suc z ) ( add-lemma1 {x} )

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

program : Comm
program = 
    Seq ( PComm (λ env → record env {varn = 10}))
    $ 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 = 
    Seq ( PComm (λ env → record env {varn = 10}))
    $  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

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

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


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


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

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

_/\_ :  Cond -> Cond -> Cond
x /\ 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 /\ b) cmThen bPost ->
           HTProof (bPre /\ neg b) cmElse bPost ->
           HTProof bPre (If b cmThen cmElse) bPost
  WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
              HTProof (bInv /\ b) cm bInv ->
              HTProof bInv (While b cm) (bInv /\ neg b)

initCond : Cond
initCond env = true

stmt1Cond : Cond
stmt1Cond env = Equal (varn env) 10

stmt2Cond : Cond
stmt2Cond env = (Equal (varn env) 10) ∧ (Equal (vari env) 0)

whileInv : Cond
whileInv env = Equal ((varn env) + (vari env)) 10

whileInv' : Cond
whileInv' env = Equal ((varn env) + (vari env)) 11

termCond : Cond
termCond env = Equal (vari env) 10

proofs : HTProof initCond simple stmt2Cond
proofs =
      SeqRule {initCond} ( PrimRule empty-case )
    $ PrimRule {stmt1Cond} {_} {stmt2Cond} lemma
  where
     lemma : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
     lemma env with stmt1Cond env
     lemma env | false = refl
     lemma env | true = refl

open import Data.Empty

open import Data.Nat.Properties

proof1 : HTProof initCond program termCond
proof1 =
      SeqRule {λ e → true} ( PrimRule empty-case )
    $ SeqRule {λ e →  Equal (varn e) 10} ( PrimRule lemma1   )
    $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)}  lemma2 (
            WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
            $ SeqRule (PrimRule {λ e →  whileInv e  ∧ lt zero (varn e) } lemma3 )
                     $ PrimRule {whileInv'} {_} {whileInv}  lemma4 ) lemma5
  where
     lemma1 : Axiom stmt1Cond (λ env → record { varn = varn env ; vari = 0 }) stmt2Cond
     lemma1 env with stmt1Cond env
     lemma1 env | false = refl
     lemma1 env | true = refl
     lemma21 : {env : Env } → stmt2Cond env ≡ true → varn env ≡ 10
     lemma21 eq = eqlemma (and-lemma-1 eq)
     lemma22 : {env : Env } → stmt2Cond env ≡ true → vari env ≡ 0
     lemma22 eq = eqlemma (and-lemma-2 eq)
     lemma23 :  {env : Env } → stmt2Cond env ≡ true → varn env + vari env ≡ 10
     lemma23 {env} eq = let open ≡-Reasoning  in
          begin
            varn env + vari env
          ≡⟨ cong ( \ x -> x + vari env ) (lemma21 eq  ) ⟩
            10 + vari env
          ≡⟨ cong ( \ x -> 10 + x) (lemma22 eq  ) ⟩
            10
          ∎
     lemma2 :  Tautology stmt2Cond whileInv
     lemma2 env = bool-case (stmt2Cond env) (
        λ eq → let open ≡-Reasoning  in
          begin
            implies (stmt2Cond env) (whileInv env)
          ≡⟨⟩
            implies (stmt2Cond env) ( Equal (varn env + vari env) 10 )
          ≡⟨  cong ( \ x -> implies (stmt2Cond env) ( Equal x 10 ) ) ( lemma23 {env} eq ) ⟩
            implies (stmt2Cond env) (Equal 10 10)
          ≡⟨⟩
            implies (stmt2Cond env) true
          ≡⟨ impl-1 ⟩
            true
          ∎
        ) (
         λ ne → let open ≡-Reasoning  in
          begin
            implies (stmt2Cond env) (whileInv env)
          ≡⟨ cong ( \ x -> implies x (whileInv env) ) ne ⟩
             implies false (whileInv env)
          ≡⟨ impl-2 {whileInv 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)) 11
          ≡⟨ cong ( \ x -> Equal x 11 ) (sym (+-assoc (varn env) (vari env) 1)) ⟩
            Equal ((varn env + vari env) + 1) 11
          ≡⟨ cong ( \ x -> Equal x 11 ) add-lemma1 ⟩
            Equal (suc (varn env + vari env)) 11
          ≡⟨ sym eqlemma1 ⟩
            Equal ((varn env + vari env) ) 10
          ≡⟨ and-lemma-1 cond ⟩
            true
          ∎ )
     lemma4 :  Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv
     lemma4 env = {!!}
     lemma5 :  Tautology ((λ e → Equal (varn e + vari e) 10) /\ neg (λ z → lt zero (varn z))) termCond
     lemma5 env = {!!}