Tutorial about Intro patterns

[thomas-lamiaux]

A completion of #32

[Matafou]

inteRest

[thomas-lamiaux]

Thanks. Btw, if you have never used it you should check out the code suggestion functionality. It enables to suggest a modification that I can later commit if I want. It is great to fix typos. It is this button

[Matafou]

Nice tuto!

[Tragicus]

Nice work indeed. As a small optimization, you do not need cbn before reflexivity, since reflexivity unifies both sides of the equality, which reduces the terms as needed. I mostly checked for typos, should I also check the writing style?

[thomas-lamiaux]

@Tragicus Thanks for checking for typos. Most comes from refactoring. After staring at the code for so long you start not seeing them anymore and basic spell checker don't catch them.

Concerning cbnI know it is not needed but for introductory contents I think it is important that people see the simplification to get what is going on.

[Villetaneuse]

Nice work. I have some minor suggestions and a longer one (about nat).

[LyesSaadi]

Very good explanations which are easy to understand, and very pertinent examples. I frequently found myself asking for "hey, would we be able to combine this and that", only for an example of that to be given just afterward.

[thomas-lamiaux]

@Villetaneuse All is solved for one detail. In your suggestion you have introduced the as ... notation which uses intro patterns itself but without explanation, so I feel there is a bit of a loop. What do you think ?

[Villetaneuse]

@Villetaneuse All is solved for one detail. In your suggestion you have introduced the as ... notation which uses intro patterns itself but without explanation, so I feel there is a bit of a loop. What do you think ?

That's indeed an issue. However, I was thinking that the reader was already familiar with these forms for the destruct and injection tactics (even though she may ignore that there is an intro pattern after as).
That's what I do in my course.

As I see it, we can go in two directions:

• remove as in the beginning of this tutorial, use case instead of destruct to avoid auto names, or as you did before use destruct and do not use the auto names, and progressively introduce the as (almost) "tactical"
• rely on some previous experience with destruct as; we still can explain that in general as takes an intro pattern

What do you think?

Would you like that I extract from my course a tutorial about basic proofs of logical statements which could be a prerequisite, in order to have a clearer view?

[thomas-lamiaux]

I think it is best to suppose people know destruct as and want to know about intro patterns, and to just add a comment.

Would you like that I extract from my course a tutorial about basic proofs of logical statements which could be a prerequisite, in order to have a clearer view?

@Villetaneuse Sth that is a bit urgent to do, would be a learning game for Coq, an adaptation of the natural number game or sth else so that people can try it out and learn the base.

[Villetaneuse]

I think it is best to suppose people know destruct as and want to know about intro patterns, and to just add a comment.

All right, I will add a remark and a list of tactics which allow as intro_pattern in the end.

Would you like that I extract from my course a tutorial about basic proofs of logical statements which could be a prerequisite, in order to have a clearer view?

@Villetaneuse Sth that is a bit urgent to do, would be a learning game for Coq, an adaptation of the natural number game or sth else so that people can try it out and learn the base.

If you really want something which resembles the natural number game, it's very difficult at this point, I'm afraid. We would first need a stable javascript backend and, to some extent, frontend.