How exactly to rewrite the work in Idris?
I wrote the following sentence in Idris:
total
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m)
plusOneCommutes Z k = Refl
plusOneCommutes (S k) j =
let inductiveHypothesis = plusOneCommutes k j in
rewrite inductiveHypothesis in Refl
Using inspiration from the source code Prelude.Nat
, I understand why it makes sense to use a recursive call (in the second case) as an induction hypothesis to prove it. However, looking through the details of the hole rewrite, I really don't understand what's going on and why it works.
If I write:
plusOneCommutes (S k) j = ?hole
I am getting the following from the compiler:
- + HolyGrail.hole [P]
`-- k : Nat
j : Nat
------------------------------------------------------
HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))
which doesn't really seem right. According to the signature, plusOneCommutes
this hole must be of type (plus (S k) (S j)) = (plus (S (S k)) j)
.
Following one more step and introducing the induction hypothesis if I write:
plusOneCommutes (S k) j =
let inductiveHypothesis = plusOneCommutes k j in
?hole
then the type hole
will become:
- + HolyGrail.hole [P]
`-- k : Nat
j : Nat
inductiveHypothesis : k + S j = S k + j
-------------------------------------------------------------------------
HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))
then using the rewrite rule given inductiveHypothesis
- + HolyGrail.hole [P]
`-- k : Nat
j : Nat
inductiveHypothesis : k + S j = S k + j
_rewrite_rule : k + S j = S k + j
-------------------------------------------------------------------------
HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j)
which results in S (plus (S k) j) = S (S (plus k j))
, which is the expected type, and Idris can complete the proof by automatically replacing ?hole
with Refl
.
What puzzles me is the unexpected difference in types between what I make from the signature and what the compiler outputs from the hole. If I voluntarily introduce an error:
I receive the following message:
- + Errors (1)
`-- HolyGrail.idr line 121 col 16:
When checking right hand side of plusOneCommutes with expected type
S k + S j = S (S k) + j
Type mismatch between
S (S (plus k j)) = S (S (plus k j)) (Type of Refl)
and
S (plus k (S j)) = S (S (plus k j)) (Expected type)
Specifically:
Type mismatch between
S (plus k j)
and
plus k (S j)
The part Type mismatch...
is consistent with the above steps, but not the part When checking ...
that gives the type I would expect.
source to share
The following from the compiler actually makes sense:
- + HolyGrail.hole [P]
`-- k : Nat
j : Nat
------------------------------------------------------
HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))
On the left =
in the type is n + S m
. After pattern matching on, n
you have (S k)
and should have S k + S j
in a type that is plus (S k) (S j)
. In this question, I have explained one important point: due to the way the function is written plus
and the fact that the compiler can do pattern matching on the types you see, S (plus k (S j))
which just applies plus
to (S k)
and (S j)
. A similar situation with S n + m
.
Now up rewrite
. In the Agda programming language rewrite
, it's just syntactic sugar for pattern matching in Refl
. And sometimes you can substitute rewrite
for pattern matching in Idris, but not in this case.
We can try to do something like this. Consider the following:
total
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m)
plusOneCommutes Z k = Refl
plusOneCommutes (S k) j = case plusOneCommutes k j of
prf => ?hole
The compiler says the following very reasonable things:
- + HolyGrail.hole [P]
`-- k : Nat
j : Nat
prf : k + S j = S k + j
------------------------------------------------------
HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))
prf
is what proves k + S j = S k + j
it makes sense. And after using rewrite
:
plusOneCommutes (S k) j = case plusOneCommutes k j of
prf => rewrite prf in ?hole
We got:
- + HolyGrail.hole [P]
`-- k : Nat
j : Nat
prf : k + S j = S k + j
_rewrite_rule : k + S j = S k + j
-------------------------------------------------------------------------
HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j)
rewrite
in Idris takes an object of type Refl
, searches the left side of =
the expression after, in
and replaces it with the right side of the =
given one Refl
. Therefore, rewrite
we had before as a result S (plus k (S j)) = S (S (plus k j))
. Your type inductiveHypothesis
is - k + S j = S k + j
and we k + S j
only got it in the form we want. You can see this part as replaced
in this lambda. After substituting S k + j
for, k + S j
you got S (plus (S k) j) = S (S (plus k j))
exactly as you correctly noted. But remember that Idris can do the pattern matching he does. And it S (plus (S k) j)
naturally becomes S (S (plus k j))
. Q.E.D.
source to share