Search code examples
function-definitionagdaformal-verificationformal-semantics

Given a function in Agda, some argument, and a new value, how to generate new function where the result for this argument will be the new value

Let's suppose that I have some f : A -> B, a : A, b : B. I want new function, that is almost a copy of f, but it should produce b for an argument a.

I was trying something like this.

replace_f : ∀ {A B} (f : A -> B) (a : A) (b : B)
    -> (A -> B)
replace_f f a b = \ { a -> b ; attr -> f attr }

But the a in the lambda definition is not the same as a that I am trying to replace. Agda just considers it as a variable.

P. S. I have also tried to use Decideable and prop equality in replace_f f a b var = if ⌊ Dec (var ≡ a) ⌋ then b else (f var) . However, it errors with Set _p_391 !=< Dec _P_386 when checking that the expression Dec (var ≡ a) has type Dec _P_386

P. P. S. If you want to reproduce the Decidable solution, use these imports

open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Binary.Core
open import Data.Bool
Solution

  • Answer to the question given by my supervisor.

    He suggests to implement and provide the equality test for the A type.

    Overall, the replace_f will look like this:

    replace_f : ∀ {A B} (decide : (x : A) -> (y : A) -> Dec (x ≡ y)) (f : A -> B ) (a : A) (b : B ) -> (A -> B )
replace_f decide f a b var = if ⌊ decide var a ⌋ then b else (f var)

    where decide is an actual implementation for comparison

    Actually, you could derive Eq clause automatically in Agda, see Haskell Deriving Mechanism for Agda