I played around with Ltac to define a Lean/mathlib handy tactics known as `push_neg`

, along with `by_contradiction`

, `by_cases`

and `by_contraposition`

.

I'm not an expert in Ltac, and I think such a tactic would be useful (maybe to add in the stdlib ?), it's probably very naive.

What do you think of this?

EssaiClassique.v

`Tactic Notation "push_neg" "in" constr(H) :=`

shouldn't this be `hyp(H)`

?

I second the need to have such tactic in the stdlib!

I was unaware of the `push_neg`

tactic in Lean, and your approach looks very nice.

A while back I wrote a similar tactic, see `solve_by_manipulating_negation_in`

in https://github.com/impermeable/coq-waterproof/blob/main/theories/Libs/Negation.v

Its tries to reduce implications like $\neg \forall x, \exists y, x \leq y ~~\implies~~ \exists x, \forall y, x >y$ to the domain specific part $\forall x y, \neg x \leq y \implies x > y$, working through the quantifiers of both formula's in sequence untill you get to the domain specific part.

My tactic was designed around doing Coq proofs using lots of `assert`

and `enough`

s, whereas your `push_neg`

seems very usefull for the direct manipulation of hypotheses and goals.

- This is Ltac2, this looks nice. I would like to learn how to use it. Do you have any pointers to some friendly documentation or tutorial ?
- Then do you suggest to extend it with domain specific lemmas ? Like
`(not a < b) <-> a >= b`

?

I spent a little bit of time learning Ltac2 and I found it pretty confusing. I had never programmed in an ML language before.

Here is the documentation.

https://coq.inria.fr/refman/proof-engine/ltac2.html

Personally I found this line very difficult to decipher and I hope the writers flesh that out at some point:

One way to think about this is that thunks are isomorphic to this type: (unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a))) i.e. thunks can produce a lazy list of results where each tail is waiting for a continuation exception.

I think it's helpful to find some general course notes on functional programming that treat programming in continuation-passing-style or CPS.

I learned a bit by following this https://github.com/tchajed/ltac2-tutorial

And there is this https://github.com/yiyunliu/ltac2-tutorial

Lastly I will say that I was initially confused by the difference between the types `() -> int`

and `int`

. The difference is that an element of type `() -> int`

(called a "thunk") represents a suspended computation to construct an integer which has not yet been evaluated and will only be evaluated once you trigger it by feeding a trivial input, whereas an element of `int`

is an actual integer with a definite value. Importantly, evaluating the computation `() -> int`

may fail, or produce side effects, or its behavior may be dependent on the existing proof context, or raise exceptions which must be handled by the calling function which tried to evaluate it. Exactly when and where you try to evaluate the "thunked" integer `()-> int`

is a question of the control flow of the program, if this computation fails, and raises an exception, or causes state changes to the global proof context, what are you going to do next?

We also have in this zulip a global Ltac2 stream which you can enable by going into the Stream settings.

Pierre Rousselin said:

- This is Ltac2, this looks nice. I would like to learn how to use it. Do you have any pointers to some friendly documentation or tutorial ?

For me personally rummaging through the Ltac2 test suite https://github.com/coq/coq/tree/master/test-suite/ltac2 was the best way to get started. Then I was able to make sense of the official documentation.

Thank you @k32 and @Patrick Nicodemus for the pointers. I will try to translate this first `push_neg`

attempt into Ltac2. Maybe we can now get back to `push_neg`

(I know I made the thread diverge...)?

Here are the docs in mathlib (lean3 and lean4) for reference :

https://leanprover-community.github.io/mathlib_docs/tactic/push_neg.html

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/PushNeg.html#Mathlib.Tactic.PushNeg.tacticPush_neg_

It looks like there are typeclasses involved for the negation of orders.

Isn't Ltac2 incompatible with mathcomp?

I have fought with some goals where I wanted to push things down ; the result looked more like "under ... do ...".

Ltac2 should be compatible with anything as long as you keep Ltac1 as the default?

but if you use ssreflect inside `Ltac`

reusable scripts (which math-comp doesn't do much), https://github.com/coq/coq/issues/6687 is likely to make your life harder.

To be back with `push_neg`

. Does anyone know how to be able to use intro patterns with the `in`

form as in something like

```
push_neg in H as [p H'].
```

Julien Puydt said:

Isn't Ltac2 incompatible with mathcomp?

I have fought with some goals where I wanted to push things down ; the result looked more like "under ... do ...".

Last time I checked Ltac2 lacks proper access to SSR internals. I mean, you can call SSR tactics via the ltac1 bridge, but that is all

@Enrico Tassi I think that's right. What ssr internals are there that Ltac2 might want to access?

The pattern matching routine, the coercion from open constr to constr, the intro pattern language and interpreter...

@Pierre Rousselin To get back to your earlier question: if you would like to add `push_neg`

to the stdlib it could indeed be nice to extend it with domain specific lemmas like `(not a < b) <-> a >= b`

to make it compatible with the other components in the library. Otherwise these steps can probably be left to the end-user.

Unfortunately I don't have experience with intropatterns..

But then it probably needs some abstraction mechanism (typeclasses? canonical structures?) and I'm

- not really knowledgeable about them
- not optimistic that there will be a consensus here... (or maybe some notion of totally ordered type already exists?)

Last updated: Jun 22 2024 at 15:01 UTC