WIP: Tactics

[clayrat]

I made this one against develop, as I assumed this will be the default working branch now?

[yurrriq]

Sounds good to me, yeah. We can use master for "releases," as in when we have significant enough changes to warrant pushing the PDF and updating the site. I'll make a note in CONTRIBUTING.md.

[clayrat]

Ok, I've finished the first pass over Tactics and wanted to consult.

Everything in there can be easily proven with rewrites and friends, but then the chapter kinda loses its point. So I've decided to use Pruviloj. There are several problems with that:

• it's an advanced feature. Do we want to introduce it so early?
• it's brittle. You have to build up a lot of intuition of how things work (TT vs Raw vs TTName, how quotes/unquotes work, etc), and debugging it is quite messy, error messages are super unhelpful, docs are sparse. You can also freeze the compiler, which mysteriously happens here in inversion_ex1.
• it's incomplete. I've managed to write symmetry and symmetryIn. I still have no idea how to write applyIn, how to use disjoint, and what are the equivalents of unfold/destruct, so I gave up in the second half and wrote things in the usual fashion.

So how do we proceed?

[david-christiansen]

I think that Idris and Coq are very different systems, and it doesn't necessarily make sense to grab Idris features that look similar to Coq features and use them in the same circumstances. I'd drop the chapter, or just give rewrites as examples.

[Melvar]

Or even not use rewrite when it’s not necessary and explain how useful this dependent pattern matching is that Coq doesn’t have.

[clayrat]

@david-christiansen Hm, now I'm confused about the purpose of Pruviloj. Given that it contains things like reflexivity and injective, I got the impression that it aims to support the same style of proving as Coq's tactics. What is its intended usage then?

[clayrat]

@Melvar PRs welcome I guess :) I'm not that proficient in Idris to figure out how to do without rewrites in the majority of the proofs. Or do you mean using replace instead?

[david-christiansen]

It was really a piece of exploratory design: "yes, we can do that too". But it's mostly intended for code generation and metaprogramming, which also benefits from many of these kinds of things. It never got quite polished enough to be the kind of thing that I'd promote as a replacement for writing the program directly, I'm afraid.

When you can do an Idris proof directly, that's the preferred style.

[yurrriq]

Would this be a good time to introduce %elab? 👍 for dropping the bulk of the chapter, showing a few examples and writing a sentence or two about how awesome Idris's pattern matching is.

[clayrat]

@david-christiansen So will Pruviloj be maintained and expanded in the future or is it going to deprecated and removed? I'm asking as I was planning to contribute the symmetry, symmetryIn and maybe applyIn (if I figure that one out) tactics, so would you accept those?

[Melvar]

@clayrat The first four uses of rewrite … in (in silly1, trans_eq_example, trans_eq, f_equal) can be replaced with pattern-matching each of the equality arguments and unifying previous pattern variables to match (the split-case functionality of the compiler will do this), and using Refl as the rhs. The subsequent three uses (in double_injective, beq_nat_true, and beq_id_true can have their rewrite … in Refl replaced with f_equal _ _ _ (…) (this is always possible with rewrite … in Refl, but if it’s not a constructor the function may need to be provided explicitly). For square_mult I’d really want a proper equational reasoning syntax, but barring that, writing out the various f_equal and trans_eq calls required is probably no clearer than the rewriting.

[david-christiansen]

It's in the distribution so that it doesn't break, but I don't know how much time I will have to improve it. It has to be either a free-time activity or a part of research, and I don't see the research connection right now. I do want other people to be able to improve it, though, so please feel free to contribute further tactics!

[clayrat]

Ok, I think I've translated all relevant examples here. We should probably keep the chapter, since it allows us to introduce things like absurd and with. But doing it with Pruviloj does look a bit overwhelming. Maybe we could use the first half to introduce the dependent pattern matching, and split out all the tacticy stuff into some kind of appendix chapter?

[yurrriq]

Thanks! Merging now and we can edit later as needed.