[Agda] A new rewrite 'tactic'.

[Victor Miraldo]

Hello Agda Community!

My name is Victor and I'm writing to introduce you guys to
something that came out of my (ongoing) MSc project.
We wrote a library to perform rewrites, similar to "setoid_rewrite" in Coq.

The library is available at https://github.com/VictorCMiraldo/agda-rw .

There are a few examples here and there (a 2 min reading of the repo
top-page
should direct you where you want to go), but here's a preview of list
concatenation
associativity, using the tactic 'by':


open import Data.List
open import RW.Strategy.PropEq
open import RW.RW (≡-strat ∷ [])

++-assoc : ∀{a}{A : Set a}(xs ys zs : List A)
         → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs       = refl
++-assoc (x ∷ xs) ys zs = tactic (by (quote ++-assoc))

The term produced by 'by' is

cong (_::_ x) (++-assoc xs ys zs)

Feel free to experiment with it, note that this is still work-in-progress,
though.

I hope you'll enjoy it.
Best,
Victor
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150210/dafe4f64/attachment.html