Stream: Coq users

Topic: RFC: a push_neg tactic for Coq


view this post on Zulip Pierre Rousselin (Sep 06 2023 at 17:51):

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

view this post on Zulip Gaëtan Gilbert (Sep 06 2023 at 18:08):

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

shouldn't this be hyp(H)?

view this post on Zulip Jelle Wemmenhove (Sep 07 2023 at 12:46):

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 ¬x,y,xy        x,y,x>y \neg \forall x, \exists y, x \leq y ~~\implies~~ \exists x, \forall y, x >y to the domain specific part xy,¬xy    x>y\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 enoughs, whereas your push_neg seems very usefull for the direct manipulation of hypotheses and goals.

view this post on Zulip Pierre Rousselin (Sep 07 2023 at 14:33):

  1. 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 ?
  2. Then do you suggest to extend it with domain specific lemmas ? Like (not a < b) <-> a >= b ?

view this post on Zulip Patrick Nicodemus (Sep 07 2023 at 14:45):

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?

view this post on Zulip Patrick Nicodemus (Sep 07 2023 at 14:47):

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

view this post on Zulip k32 (Sep 07 2023 at 20:27):

Pierre Rousselin said:

  1. 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.

view this post on Zulip Pierre Rousselin (Sep 08 2023 at 05:57):

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.

view this post on Zulip Julien Puydt (Sep 08 2023 at 10:19):

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 ...".

view this post on Zulip Paolo Giarrusso (Sep 08 2023 at 12:40):

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

view this post on Zulip Paolo Giarrusso (Sep 08 2023 at 12:42):

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.

view this post on Zulip Pierre Rousselin (Sep 08 2023 at 14:56):

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'].

view this post on Zulip Enrico Tassi (Sep 08 2023 at 17:28):

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

view this post on Zulip Jason Gross (Sep 08 2023 at 21:45):

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

view this post on Zulip Enrico Tassi (Sep 08 2023 at 21:59):

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

view this post on Zulip Jelle Wemmenhove (Sep 14 2023 at 09:42):

@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..

view this post on Zulip Pierre Rousselin (Sep 14 2023 at 10:25):

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

  1. not really knowledgeable about them
  2. 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