[Agda] Matching problem at end of equational reasoning proof

[Christoph Herrmann]

Hi,

the missing part is
 
2 * (n + 1) + n * (n + 1)
 ≈⟨ sym (proj₂ distrib (n + 1) 2 n) ⟩
  (2 + n) * (n + 1)

I was confused by the error message; since the error location
given was the last line including the \qed box, I assumed
that all equations before had been checked correct.

If it is the case as it appears now that the equations are
checked from bottom to top, then I would of course write them
in the same order to check them on the fly.

Cheers
 
Liang-Ting Chen wrote:
> Hi,
>
> On Wed, May 27, 2009 at 11:26 PM, Christoph Herrmann 
> <ch at cs.st-andrews.ac.uk <mailto: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


-- 
  Dr. Christoph Herrmann
  University of St Andrews, Scotland/UK
  phone: office: +44 1334 461629, home: +44 1334 478648
  email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
  URL:   http://www.cs.st-andrews.ac.uk/~ch
 
  The University of St Andrews is a charity registered in Scotland: No SC013532