-- Implementation of finite maps using functions, including proofs of required properties

--#include "FiniteMaps2.alfa"

--#include "Alfa/Bool.alfa"

--#include "Alfa/Identity.alfa"

--#include "Alfa/Propositions.alfa"

--#include "Alfa/BoolProp.alfa"

package FunFM where
  open FiniteMaps  use  FiniteMap
  open Identity
   use  (==),  refl,  subst,  substSym,  sym,  trans,  cong,  cong2,
        cong1
  open Propositions
   use  Prop,  Absurdity,  AbsurdityElim,  Triviality,  TrivialityIntro,
        Pred,  IsTrue
  open BoolProp  use  ifPropD,  ifProp,  ifTrueProp,  ifFalseProp
  open Booleans  use  Bool,  if
  FM (K::Set)(V::Set) :: Set
    = K -> V
  -- To use functions as finite maps, we require an equality test for keys:
  KeyEq (K::Set) :: Type
    = sig{eqK :: K -> K -> Bool;
          eqRefl :: (k::K) -> IsTrue (eqK k k);
          eqId :: (k::K) -> (k'::K) -> IsTrue (eqK k k') -> (==) K k k';}
  funFM (K::Set)(domK::KeyEq K) :: FiniteMap (FM K) K
    = open domK use  eqK,  eqRefl,  eqId in 
      struct {
        empty (V::Set)(v::V) :: FM K V
          = \(k::K) -> v;
        lookup (V::Set)(f::FM K V) :: K -> V
          = f;
        update (V::Set)(k::K)(r::V)(f::FM K V) :: FM K V
          = \(k'::K) -> if V (eqK k' k) r (f k');
        updateProp (V::Set)
                   (k::K)
                   (k'::K)
                   (v::V)
                   (fm1::FM K V)
                   (fm2::FM K V)
                   (p::(==) V (lookup V fm1 k) (lookup V fm2 k))
          :: (==)
               V
               (lookup V (update V k' v fm1) k)
               (lookup V (update V k' v fm2) k)
          = subst
              V
              (lookup V fm1 k)
              (lookup V fm2 k)
              (\(h::V) ->
               (==)
                 V
                 (lookup V (update V k' v fm1) k)
                 (lookup V (\(d'::K) -> if V (eqK d' k') v h) k))
              p
              (refl V (lookup V (update V k' v fm1) k));
        updateSame (V::Set)(k::K)(v::V)(fm::FM K V)
          :: (==) V (lookup V (update V k v fm) k) v
          = ifTrueProp
              V
              (eqK k k)
              v
              (fm k)
              (\(h::V) -> (==) V h v)
              (eqRefl k)
              (refl V v);
        updateOther (V::Set)
                    (k::K)
                    (k'::K)
                    (v::V)
                    (fm::FM K V)
                    (p::(==) K k k' -> Absurdity)
          :: (==) V (lookup V (update V k' v fm) k) (lookup V fm k)
          = ifFalseProp
              V
              (eqK k k')
              v
              (fm k)
              (\(h::V) -> (==) V h (lookup V fm k))
              (\(h::Propositions.IsTrue (eqK k k')) -> p (eqId k k' h))
              (refl V (fm k));}
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
var "empty" hide 1
var "lookup" hide 1
var "update" hide 1
var "updateSame" hide 1
var "updateOther" hide 1
 #-}