This is the first concept in The Little Typer to give me quite a bit of trouble, and it appears I am not alone (1 2), so perhaps it would be beneficial to ask here. Hopefully this can be connected with more general concepts to expand the audience for this question beyond people reading the book.
The textbook The Little Typer is an introduction to dependent types using the Pie language. Chapter 8 introduces the concept of expressing statements with types, and constructing a value of that type being a proof of that statement being true.
In Pie, the type statement that two expressions are equal is
(= X from to) [docs], where
= is the type constructor,
X is a type, and both
to are values of type
X. For example
(= Nat (+ 6 6) (+ 8 4)).
The value constructor of
(same e) has type
(= X e e) if
e is an
X. So the value
(same 12) is a proof & instance of type
(= Nat (+ 6 6) (+ 8 4)) (that doesn't require induction to construct).
= type also has an eliminator called
cong (short for congruent) where
(cong target f) transforms a
target of type
(= X from to) to type
(= Y (f from) (f to)), where
f is of type
(→ X Y). For example
(λ(n) (cong (same n) (+ 1))) evaluates to
(λ(n) same (+ 1 n).
Here's where I have trouble: chapter 9 introduces a more general eliminator for
replace and claims
replace can do anything
cong can do, and more. The definition of
(replace target motive base) → (motive to) target : (= X from to) motive : (→ X U) base : (motive from)
Frankly I can't make heads nor tails of this operator. How would I parameterize it to mimic
cong? What is an example of something it can do that
cong cannot? The only clue I have to its workings is its name and the context in which it's presented, where I assume what we're doing is transforming one expression to look like something else.