steshaw (13) [Avatar] Offline
#1
I struggled with this exercise and would like to know if my answer is what's expected. In particular I had what I though to be a strange looking pattern of: rewrite x in Refl.

myPlusCommutative : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutative Z m = rewrite plusZeroRightNeutral m in Refl -- {x = m}
myPlusCommutative (S k) m = hmmm k m $ Refl {x = m + (S k)}
  where
    hmmm : (k : Nat) -> (m : Nat) -> ((m + (S k)) = (m + (S k))) -> S (plus k m) = plus m (S k)
    hmmm k m prf = rewrite myPlusCommutative k m in (rewrite plusSuccRightSucc m k in prf)

Can this code be improved?

Eric B (4) [Avatar] Offline
#2
For the first clause, check out sym:

??> :doc sym
sym : (left = right) -> right = left
    Symmetry of propositional equality
    
    The function is Total


As for the second, you've overcomplicated things a bit.

To describe the (read: my) process a bit, consider ?myPlusCommutative_rhs_2:

myPlusCommutative (S k) m = ?myPlusCommutative_rhs_2


Since we know we want to recurse toward our base case (n = Z):

myPlusCommutative (S k) m =
  let inductiveHypothesis = myPlusCommutative k m in
    rewrite inductiveHypothesis in
    ?myPlusCommutative_rhs_2


Now let's examine the type of myPlusCommutative_rhs_2:

??> :t myPlusCommutative_rhs_2
  k : Nat
  m : Nat
  inductiveHypothesis : plus k m = plus m k
  _rewrite_rule : plus k m = plus m k
--------------------------------------
myPlusCommutative_rhs_2 : S (plus m k) = plus m (S k)


The type of myPlusCommutative_rhs_2 should look familiar:

??> :t plusSuccRightSucc
plusSuccRightSucc : (left : Nat) ->
                    (right : Nat) -> S (left + right) = left + S right


Thus we know how to fill in the hole:

myPlusCommutative (S k) m =
  let inductiveHypothesis = myPlusCommutative k m in
    rewrite inductiveHypothesis in
            plusSuccRightSucc m k


As a matter of taste, I tend to avoid let-ing too many variables, so I like to rewrite such code as follows:

myPlusCommutative (S k) m =
  rewrite myPlusCommutative k m in
          plusSuccRightSucc m k


Hope that helps!
steshaw (13) [Avatar] Offline
#3
Thanks for the reply, Eric!

I don't see how to use sym in the first clause. My interactive developments always end up with:

myPlusCommutative' Z m = rewrite plusZeroRightNeutral m in Refl

Would you mind spelling it out?

I'm still working through your thoughts on the 2nd clause.
steshaw (13) [Avatar] Offline
#4
Thanks, this was very helpful!

I worked through your process for the 2nd clause. Originally I ended up with
myPlusCommutative' (S k) m = rewrite myPlusCommutative k m
                              in rewrite plusSuccRightSucc m k in
                              Refl

but I got to realise that I could trim that last rewrite x in Refl (which was precisely what I though was weird!).

I then tried the same with the first clause as it too was in the form rewrite x in Refl. It didn't work out but looking at the hole, I was able to realise what you meant by using sym. Now I have:

myPlusCommutative' : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutative' Z m = sym (plusZeroRightNeutral m)
myPlusCommutative' (S k) m = rewrite myPlusCommutative k m
                             in plusSuccRightSucc m k


Thanks again!
Eric B (4) [Avatar] Offline
#5
Great! I'm glad I could help.

I tried turning my reply into a blog post by the way:
http://blorg.ericb.me/2016/09/proving-addition-is-commutative-in-idris/
steshaw (13) [Avatar] Offline
#6
Nice one, Eric!