CODEWITHSUNDEEP
agda
ajayv
ajayv

Reputation: 703

why this code is not working in agda?

I am trying to prove commutative property over natural number on multiplication operation.

--proving comm over *
*comm : ∀ a b → (a * b) ≡ (b * a)
*comm zero b = sym (rightId* b)
*comm (suc a) b = {!!}

when i check goal I found that it is b + a * b ≡ b * suc a. So i proved this. 

lemma*-swap : ∀ a b → a + a * b ≡ a * suc b

Now when i tried : 

*comm : ∀ a b → (a * b) ≡ (b * a)
*comm zero b = sym (rightId* b)
*comm (suc a) b = lemma*-swap b a

This should work as it satisfied the goal but why this is not working?? Please suggest me where I am wrong.

Upvotes: 1

Views: 72

Answers (1)

gallais
gallais

Reputation: 12103

b + a * b (the expression in the goal) and a + a * b (the expression in lemma*-swap) are distinct so applying lemma*-swap does not satisfy the goal.

You need to rewrite the induction hypothesis *comm a b to turn a * b into b * a in the goal so that the expression lemma*-swap b a can be used to discharge the goal.

Upvotes: 4

Related Questions