------------------------------------------------------------------------
-- A theorem related to pointwise equality
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Chi            χ-ℕ-atoms
open import Coding         χ-ℕ-atoms
open import Free-variables χ-ℕ-atoms

import Coding.Instances.Nat

-- The results are stated and proved under the assumption that a
-- correct self-interpreter can be implemented.

module Pointwise-equality
  (eval : Exp)
  (cl-eval : Closed eval)
  (eval-correct₁ :  p v  Closed p  p  v  apply eval  p    v )
  where

open import Bag-equivalence
open import Equality.Propositional
open import Prelude hiding (const; Decidable)

open import Equality.Decision-procedures equality-with-J
open import H-level.Closure equality-with-J

open import Computability χ-ℕ-atoms
open import Constants     χ-ℕ-atoms
open import Reasoning     χ-ℕ-atoms
open import Values        χ-ℕ-atoms

open Computable-function
open χ-atoms χ-ℕ-atoms

open import Combinators hiding (if_then_else_)

-- Pointwise equality of computable functions to Bool.

Pointwise-equal :
   {a} (A : Set a)  rA : Rep A Consts  
  let F = Computable-function A Bool Bool-set in
  (F × F) →Bool
Pointwise-equal _ =
  as-function-to-Bool₁
     { (f , g)   x  function f x  function g x })

-- Pointwise equality of computable functions from Bool to Bool is
-- decidable.

pointwise-equal-Bool : Decidable (Pointwise-equal Bool)
pointwise-equal-Bool =
  total→almost-computable→computable
    id
    id
    (proj₁ (Pointwise-equal Bool))
    total
    ( pointwise-equal
    , closed
    , correct
    )
  where
  F = Computable-function Bool Bool Bool-set

  pointwise-equal′ : F × F  Bool
  pointwise-equal′ (f , g) =
    (if function f true  Bool.≟ function g true  then true else false)
      
    (if function f false Bool.≟ function g false then true else false)

  total : Total id (proj₁ (Pointwise-equal Bool))
  total p@(f , g) = result , true-lemma , false-lemma
    where
    result = pointwise-equal′ p

    true-lemma : (∀ b  function f b  function g b)  result  true
    true-lemma hyp
      with function f true Bool.≟ function g true | hyp true
    ... | no  f≢g | f≡g = ⊥-elim (f≢g f≡g)
    ... | yes _   | _
      with function f false Bool.≟ function g false | hyp false
    ... | no  f≢g | f≡g = ⊥-elim (f≢g f≡g)
    ... | yes _   | _   = refl

    false-lemma : ¬ (∀ b  function f b  function g b)  result  false
    false-lemma hyp
      with function f true  Bool.≟ function g true
         | function f false Bool.≟ function g false
    ... | yes ft≡gt | yes ff≡gf = ⊥-elim $ hyp Prelude.[  _  ft≡gt)
                                                       ,  _  ff≡gf)
                                                       ]
    ... | yes _     | no  _     = refl
    ... | no  _     | yes _     = refl
    ... | no  _     | no  _     = refl

  infix 10 _at_

  _at_ : Exp  Bool  Exp
  f at b =
    decode-Bool
      (apply eval (const c-apply (f    b   Exp   [])))

  test : Bool  Exp
  test b = equal-Bool (var v-f at b) (var v-g at b)

  pointwise-equal : Exp
  pointwise-equal =
    lambda v-p (case (var v-p) (
      branch c-pair (v-f  v-g  [])
        (and (test true) (test false))  []))

  -- This proof could have been simplified if eval had been a concrete
  -- implementation, rather than a variable.

  closed : Closed pointwise-equal
  closed =
    Closed′-closed-under-lambda $
    Closed′-closed-under-case
      (Closed′-closed-under-var (inj₁ refl))
       where
        (inj₁ refl)  and-closed (test-closed true) (test-closed false)
        (inj₂ ()))
    where
    variables = v-f  v-g  v-p  []

    at-closed :  f b  f  variables  Closed′ variables (var f at b)
    at-closed f b f∈ =
      decode-Bool-closed $
      Closed′-closed-under-apply
        (Closed→Closed′ cl-eval)
        (Closed′-closed-under-const λ where
           _ (inj₁ refl)         Closed′-closed-under-var f∈
           _ (inj₂ (inj₁ refl))  Closed→Closed′ $
                                  rep-closed ( b   Exp)
           _ (inj₂ (inj₂ ())))

    test-closed :  b  Closed′ variables (test b)
    test-closed b =
      equal-Bool-closed
        (at-closed v-f b (from-⊎ (V.member v-f variables)))
        (at-closed v-g b (from-⊎ (V.member v-g variables)))

  at-correct :
     (f : F) b   f  at b   function f b 
  at-correct f b = decode-Bool-correct (function f b) (
    apply eval  apply (proj₁ (computable f))  b   Exp   ⇓⟨ eval-correct₁
                                                                  (apply (proj₁ $ computable f)  b )
                                                                   function f b 
                                                                  (Closed′-closed-under-apply
                                                                     (proj₁ $ proj₂ $ computable f)
                                                                     (rep-closed b))
                                                                  (proj₁ (proj₂ $ proj₂ $ computable f)
                                                                     b
                                                                     (function f b)
                                                                     (lift refl)) ⟩■
      function f b   Exp )

  test-correct :
     b (f g : F) 
    test b [ v-g   g  ] [ v-f   f  ] 
     if function f b Bool.≟ function g b then true else false 
  test-correct b f g =
    equal-Bool-correct (function f b) (function g b)

      (var v-f at b [ v-g   g  ] [ v-f   f  ]  ≡⟨ lemma  f  ⟩⟶
        f  at b                                    ⇓⟨ at-correct f b ⟩■
        function f b )

      (var v-g at b [ v-g   g  ] [ v-f   f  ]  ≡⟨ lemma ( g  [ v-f   f  ]) ⟩⟶
       ( g  [ v-f   f  ]) at b                  ≡⟨ cong (_at b) (subst-rep g) ⟩⟶
        g  at b                                    ⇓⟨ at-correct g b ⟩■
        function g b )
    where
    ss = (v-f ,  f )  (v-g ,  g )  []

    lemma = λ e 
      cong₂  e₁ e₂  decode-Bool (apply e₁ (const _ (e  e₂  []))))
        (substs-closed eval cl-eval ss)
        (substs-rep ( b   Exp) ss)

  correct :
     p b 
    proj₁ (Pointwise-equal Bool) [ p ]= b 
    apply pointwise-equal  p    b 
  correct p@(f , g) b [p]=b =
    apply pointwise-equal  p                                ⟶⟨ apply lambda (rep⇓rep p) 

    case  p  (
      branch c-pair (v-f  v-g  [])
        (and (test true) (test false) [ v-p   p  ])  [])  ≡⟨ cong₂  e₁ e₂  case  p  (branch c-pair (v-f  v-g  []) (and e₁ e₂)  []))
                                                                   (test-lemma true)
                                                                   (test-lemma false) ⟩⟶
    case  p  (
      branch c-pair (v-f  v-g  [])
        (and (test true) (test false))  [])                  ⟶⟨ case (rep⇓rep p) here (  []) 

    and (test true  [ v-g   g  ] [ v-f   f  ])
        (test false [ v-g   g  ] [ v-f   f  ])          ⇓⟨ and-correct (if function f true  Bool.≟ function g true  then true else false)
                                                                             (if function f false Bool.≟ function g false then true else false)
                                                                             (test-correct true f g) (test-correct false f g) 

     pointwise-equal′ p                                     ≡⟨ cong ⌜_⌝ (_⇀_.deterministic (proj₁ (Pointwise-equal Bool)) {a = p}
                                                                                             (proj₂ (total p)) [p]=b) ⟩⟶
     b                                                      ■⟨ rep-value b 

    where

    at-lemma :
       b f  v-p  f  var f at b [ v-p   p  ]  var f at b
    at-lemma b f p≢f =
      var f at b [ v-p   p  ]                                          ≡⟨⟩

      decode-Bool (apply (eval [ v-p   p  ]) (const c-apply
        (var f [ v-p   p  ]    b   Exp  [ v-p   p  ]  [])))  ≡⟨ cong  e  decode-Bool (apply e (const _
                                                                                          (var f [ v-p   p  ] 
                                                                                             b   Exp  [ v-p   p  ]  []))))
                                                                               (subst-closed v-p  p  cl-eval) 
      decode-Bool (apply eval (const c-apply
        (var f [ v-p   p  ]    b   Exp  [ v-p   p  ]  [])))  ≡⟨ cong  e  decode-Bool (apply _ (const _ (e  _))))
                                                                               (subst-∉ v-p (var f) λ { (var p≡f)  p≢f p≡f }) 
      decode-Bool (apply eval (const c-apply
        (var f    b   Exp  [ v-p   p  ]  [])))                  ≡⟨ cong  e  decode-Bool (apply _ (const _ (_  e  _))))
                                                                               (subst-rep ( b   Exp)) 
      decode-Bool (apply eval (const c-apply
        (var f    b   Exp   [])))                                  ≡⟨⟩

      var f at b                                                          

    test-lemma :  b  test b [ v-p   p  ]  test b
    test-lemma b =
      cong₂ equal-Bool (at-lemma b v-f  ())) (at-lemma b v-g  ()))