[Agda] Matching problem at end of equational reasoning proof

[Liang-Ting Chen]

Hi,

On Wed, May 27, 2009 at 11:26 PM, Christoph Herrmann <ch at cs.st-andrews.ac.uk
> wrote:

> Hi,
>
> I have attached an inductive proof (attempt) of Gauss' summation formula.
>
> The problem is that at the end of the equational reasoning the matching
> with the right-hand side of the type does not seem to work, namely:
>
> (suc n) * ((suc n) + 1) against (a * (a + 1)) in the case that a=(suc n)
>
> I am wondering whether Agda still knows that it is in the case a=(suc n)
> or whether this information is available only for matching the left-hand
> side.

You pass "refl" as the proof term that tells agda that

((suc n) + 1) * (suc n)

is computaionally equal to

(suc n) * ((suc n) + 1), but it is not so trivial to know this fact. It
doesn't complain that a != (suc n) but some terms are different.

Here is my proof, and I leave an unsolved hole as a practice. It might be
more compact, but I don't want to modify your proof too much.

module Gauss where

open import Algebra
open import Data.Nat
open import Data.Nat.Properties
import Relation.Binary.EqReasoning
open Relation.Binary.EqReasoning (Data.Nat.setoid)
open import Relation.Binary.PropositionalEquality using (cong; cong₂)
open Algebra.CommutativeSemiring commutativeSemiring
        hiding (_+_; _*_)
        renaming (zero to *-zero)
open import Data.Product
sum : ℕ -> ℕ
sum 0 = 0
sum (suc n) = suc n + sum n

gauss-formula : (a : ℕ) -> 2 * sum a ≈ a * (a + 1)
gauss-formula 0 = refl
gauss-formula (suc n) =
 begin
 2 * sum (suc n)
 ≈⟨ refl ⟩
 2 * (suc n + sum n)
 ≈⟨ proj₁ distrib 2 (suc n) (sum n) ⟩
 (2 * suc n) + 2 * sum n
 ≈⟨ cong (λ p -> 2 * suc n + p) (gauss-formula n) ⟩
 (2 * suc n) + (n * (n + 1))
 ≈⟨ cong (λ p → 2 * p + n * (n + 1)) (+-comm 1 n) ⟩
 2 * (n + 1) + n * (n + 1)
 ≈⟨ {!!} ⟩
 (2 + n) * (n + 1)
 ≈⟨ cong₂ _*_ (cong (λ p → 1 + p) (+-comm 1 n)) (+-comm n 1)⟩
 ((suc n) + 1) * (suc n)
 ≈⟨ *-comm ((suc n) + 1) (suc n)⟩
 (suc n) * ((suc n) + 1)
 ∎


-- 
sincerely,
Liang-Ting
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090528/483857ee/attachment.html