Refl in agda: explanation of the congruence property
In the following definition of equality, we have refl as a constructor
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
and we can prove that the function is congruent on the equality
cong : ∀ { a b} { A : Set a } { B : Set b }
(f : A → B ) {m n} → m ≡ n → f m ≡ f n
cong f refl = refl
I'm not sure if I can make out what's going on here. I think we are matching refl patterns by hidden parameters: if we replace the first occurrence of a refl with a different identifier, we get a type error. after pattern matching, I assume that m and n are the same by the definition of refl. then the magic happens (does the definition of relationship functionality apply or is it built in?)
Is there an intuitive description of what's going on?
source to share
Yes, the arguments in curly braces {}
are implicit and only need to be supplied or matched if agda cannot understand them. You need to specify them as the dependent types must refer to the values they depend on, but dragging them around all the time would make the code rather clunky.
The expression cong f refl = refl
matches the explicit arguments ( A → B
) and ( m ≡ n
). If you want to match implicit arguments, you need to put the corresponding expression in {}
, but there is no need here. Then on the right-hand side this is really a construction ( f m ≡ f n
) with refl
, and it works "by magic". Agda has a built-in axiom that proves this to be true. This axiom is similar (but stronger) J
-axiom - an induction axiom: if something is C : (x y : A) → (x ≡ y) → Set
true for C x x refl
, then it is also true for any x y : A
and p : x ≡ y
.
J : forall {A : Set} {C : (x y : A) → (x ≡ y) → Set} →
(c : ∀ x → C x x refl) →
(x y : A) → (p : x ≡ y) → C x y p
-- this really is an axiom, but in Agda there is a stronger built-in,
-- which can be used to prove this
J c x .x refl = c x -- this _looks_ to only mean x ≡ x
-- but Agda built-in extends this proof to all cases
-- for which x ≡ y can be constructed - that the point
-- of having induction
cong : ∀ { a b} { A : Set a } { B : Set b }
(f : A → B ) {m n} → m ≡ n → f m ≡ f n
cong f {x} {y} p = J {C = \x y p → f x ≡ f y} -- the type of equality
-- of function results
(\_ → refl) -- f x ≡ f x is true indeed
x y p
(In this last line, we match the explicit arguments f
and p
, as well as the implicit arguments m=x
and n=y
. Then we go to J
one implicit argument, but this is not the first positional implicit, so we tell agda that this is the definition C
in the definition - without that Agda will not see that type means refl
c \_ → refl
)
source to share