[Agda] sym in Agda 2.5.1

[John Leo]

I've enjoyed playing with the 2.5.1 RC so far.  The new library management
seems very nice, sections have proven to be immediately valuable, and I'm
looking forward to playing with the new reflection and other features.

I've been going through Software Foundations and doing the exercises in
Agda in a "pure functional" style with no tactics (not even Agda's
rewrite); so far I far prefer the results I've been able to obtain to Coq's
tactics--I feel the functional style is simpler and clearer.  This may
change as the proofs get more complicated.  I'm about midway through the
"More Coq" chapter now and so far I only miss the unfold and inversion
tactics, but I've been able to work around them with a little effort.

I have noticed one "regression" of sorts regarding sym of propositional
equality--when goals are shown with C-c C-, sym is represented as
"Function.flip" whereas before the flip was done explicitly.  As a simple
example, in the following (I've written it to show two calls to sym):

n+0=n : (n : ℕ) → n + 0 ≡ n
n+0=n zero    = refl
n+0=n (suc n) = cong suc (n+0=n (n))

m+Sn : (m n : ℕ) → m + suc n ≡ suc (m + n)
m+Sn zero    n = refl
m+Sn (suc m) n = cong suc (m+Sn m n)

+comm : (m n : ℕ) → m + n ≡ n + m
+comm zero    n =
  let a = sym (n+0=n n)
  in {!!}
+comm (suc m) n =
  let a = cong suc (+comm m n)
      b = sym (m+Sn n m)
  in {!!}

In the first hole we get

Goal: n ≡ n + zero
————————————————————————————————————————————————————————————
a : Function.flip _≡_ (n + 0) n
n : ℕ

and in the second hole

Goal: suc (m + n) ≡ n + suc m
————————————————————————————————————————————————————————————
b : Function.flip _≡_ (n + suc m) (suc (n + m))
a : suc (m + n) ≡ suc (n + m)
n : ℕ
m : ℕ

In the previous version these would have been

a : n ≡ (n + 0)

and

b : suc (n + m) ≡ (n + suc m)

respectively, which are certainly easier to read.

I can still read the Function.flip notation but it was easier to read in
the previous version, so if this is viewed as a regression I'm happy to
file an issue for it.

John
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160213/08ce74e1/attachment.html