Path induction meant
This is the next question Getting induction to work at Agda
I wonder when this design could be more expressive. It seems to me that we can always express the same thing:
f : forall {A} -> {x y : A} -> x == y -> "some type"
f refl = instance of "some type" for p == refl
Here Agda will do path induction, given an example that is the same as c : (x : A) -> C refl
from this question:
pathInd : forall {A} -> (C : {x y : A} -> x == y -> Set)
-> (c : (x : A) -> C refl)
-> {x y : A} -> (p : x == y) -> C p
This function seems to be isomorphic:
f' : forall {A} -> {x y : A} -> x == y -> "some type"
f' = pathInd (\p -> "some type") (\x -> f {x} refl)
Are these two ways ( f
vs pathInd
) the same in terms of power?
source to share
pathInd
is just a dependent rectifier. Here's an isomorphic definition:
J : ∀ {α β} {A : Set α} {x y : A}
-> (C : {x y : A} {p : x ≡ y} -> Set β)
-> ({x : A} -> C {x} {x})
-> (p : x ≡ y) -> C {p = p}
J _ b refl = b
That being said, you can define various functions on _≡_
without pattern matching, for example:
sym : ∀ {α} {A : Set α} {x y : A}
-> x ≡ y
-> y ≡ x
sym = J (_ ≡ _) refl
trans : ∀ {α} {A : Set α} {x y z : A}
-> x ≡ y
-> y ≡ z -> x ≡ z
trans = J (_ ≡ _ -> _ ≡ _) id
cong : ∀ {α β} {A : Set α} {B : Set β} {x y : A}
-> (f : A -> B)
-> x ≡ y
-> f x ≡ f y
cong f = J (f _ ≡ f _) refl
subst : ∀ {α β} {A : Set α} {x y : A}
-> (C : A -> Set β)
-> x ≡ y
-> C x -> C y
subst C = J (C _ -> C _) id
But you cannot prove the uniqueness of proofs of identity from J
, as described in [1]:
uip : ∀ {α} {A : Set α} {x y : A} -> (p q : x ≡ y) -> p ≡ q
uip refl refl = refl
So you can express more with Agda pattern matching than with just a dependent rectifier for _≡_
. But you can use the option --without-K
:
{-# OPTIONS --without-K #-}
open import Relation.Binary.PropositionalEquality
uip : ∀ {α} {A : Set α} {x y : A} -> (p q : x ≡ y) -> p ≡ q
uip refl refl = refl
uip
now does not check the typecheck, throwing this error:
Cannot eliminate reflexive equation x = x of type A because K has
been disabled.
when checking that the pattern refl has type x ≡ x
source to share
To give the short answer: you're right, Agda pattern matching implies the existence of a path induction primitive. In fact, it has been shown that in unit type theory, dependent pattern matching is equivalent to the existence of inductive primitives for inductive types and the so-called K-axiom:
http://link.springer.com/chapter/10.1007/11780274_27
Recently, it has been shown that the (latest implementation) of Agda's --without-K option restricts pattern matching to be only equivalent to having inductive primitives for inductive types:
http://dl.acm.org/citation.cfm?id=2628136.2628139
Full disclosure: I am a co-author of the latest work.
source to share