How to write a tactic contradiction with Ltac2 #105
Conversation
thomas-lamiaux
force-pushed
the
how_to_ltac2_contradiction
branch
from
954c5d6 to
16aed5d
Compare
Co-authored-by: Pierre Rousselin <[email protected]>
…x/platform-docs into how_to_ltac2_contradiction
|
|
||
| (** - [multi_match! goal with] is more complex and subtle. It basically behaves | ||
| like [match!] except that it will further backtrack if the choice of a | ||
| branch leads to a subsequent failure when linked with another tactic. |
There was a problem hiding this comment.
I don't think the term "linked" is clear enough here. Personally, I find examples clearer than specifications, so giving a code sample where there is a difference between match! goal with (...) end; t () and multi_match! goal with (...) end; t () would be most helpful for me.
There was a problem hiding this comment.
It is not supposed to be an intro on match but I have added a bit of text, it can always be moved to a tuto when we will write one
src/How_to_Ltac2_contradiction.v
Outdated
| In contrast, if we had a deep embedding, the arguments of [Unsafe.App] would be | ||
| recursively converted to [kind], resulting in the type [kind -> kind array -> kind]. | ||
| The reason for using a shallow embedding is that it is much faster than fully | ||
| converting terms to the interal syntax, yet sufficient for most applications. |
There was a problem hiding this comment.
interal -> internal
I honestly don't think this paragraph is necessary. The distinction between shallow embeddings and deep embeddings doesn't seem relevant to me here.
I don't think you need to call it an "embedding" at all, you can say that it returns the head of the term.
There was a problem hiding this comment.
One of the goal of this how-to is to get that, I would rather like to move all the match content in a real tuto. It should not be in a how-to but I kinda need it as there is no tuto yet.
|
@patrick-nicodemus thanks. Overall what do you think, it is clear / useful ? |
|
I think it's good overall. In 2019 in the original Ltac2 paper, Pierre Marie-Pedrot writes:
It seems to me we are still in that stage in 2025 - by using it to write tutorials, you are hitting the need for functions to count the number of constructors and do conversion between terms, and expose more in the Rocq API. This tension will continue to exist for a while but I think the tension is necessary for the language to develop. |
|
@patrick-nicodemus I agree but also if you check out the current dev, a lot have been added since Rocq 9, and there are less and less API missing. Like, it is far from being bad with the shallow embedding etc... |
|
Thank you very much @patrick-nicodemus. @thomas-lamiaux, I will wait for comments to be resolved and write a quick review afterwards. |
There was a problem hiding this comment.
Thanks for the review @patrick-nicodemus
Sorry for the typos, clearly AI do not catch them all.
To fix typos could use "code suggestion" next time.
It is the +- button in a comment.
It saves me a lot of times, as I can just merge all the typos from the interface rather than having to go back and forth with my file.
|
|
||
| (** - [multi_match! goal with] is more complex and subtle. It basically behaves | ||
| like [match!] except that it will further backtrack if the choice of a | ||
| branch leads to a subsequent failure when linked with another tactic. |
There was a problem hiding this comment.
It is not supposed to be an intro on match but I have added a bit of text, it can always be moved to a tuto when we will write one
|
|
||
| (** Checking terms up to syntax is not a good notion of equality in type theory. | ||
| For instance, [4 + 1] is not syntactically equal to [1]. | ||
| What we really want here is to compare type semantically, i.e. up to |
There was a problem hiding this comment.
you do too much categories, the semantics of a PL language is its operational semantics 😅
Joke aside, I see your point, I'll see what I can do
src/How_to_Ltac2_contradiction.v
Outdated
| In contrast, if we had a deep embedding, the arguments of [Unsafe.App] would be | ||
| recursively converted to [kind], resulting in the type [kind -> kind array -> kind]. | ||
| The reason for using a shallow embedding is that it is much faster than fully | ||
| converting terms to the interal syntax, yet sufficient for most applications. |
There was a problem hiding this comment.
One of the goal of this how-to is to get that, I would rather like to move all the match content in a real tuto. It should not be in a how-to but I kinda need it as there is no tuto yet.
|
@Villetaneuse I have fixed the issues |
|
@Villetaneuse I'll merge this during the week-end so you have until then. If you don't have time it is fine |
@thomas-lamiaux Actually, the linked post only discusses "Allow edits from maintainers." Since I am not an official Rocq maintainer, it's not clear that I can do this. |
|
@patrick-nicodemus do you not see this button ?
|
|
@thomas-lamiaux yes, it generates a markdown box: I guess whatever I put in there is clickable, I see. |
No description provided.