Cylindrical decomposition #3
Conversation
cylinder.v
Outdated
| rewrite -ball_normE inE/= [normr _]mx_normrE => /bigmax_ltP[_]. | ||
| move=> /(_ (ord0, ord0) isT)/=; rewrite !mxE -opprB normrN => /ltr_normlW. | ||
| by rewrite -subr_lt0 -addrA subrr addr0 mem_setE inSAset_itv in_itv/=. | ||
| mp. |
There was a problem hiding this comment.
That is a tactic I have defined earlier that turns a goal (A -> B) -> C into goals A and B -> C. It may disappear during cleanup if we want to, although it has been pervasively useful, so unless you know a hack that does it without copying large terms, we may want to keep it.
There was a problem hiding this comment.
the typical hack is move=> /(_ _)/wrap[]
Lemma test A B C : (A -> B) -> C.
Proof.
move=> /(_ _)/wrap[].
Abort.There was a problem hiding this comment.
could be a good idea to turn it into a dedicated intro pattern tactic to use e.g. move=> /(fill 1) (that would fill for example the nth hole in the top of the stack).
There was a problem hiding this comment.
Ah, another one I did not know. It is not in the refman?
There was a problem hiding this comment.
Ah, another one I did not know. It is not in the refman?
No... do you think it should be put there, or isn't a bit too advanced?
There was a problem hiding this comment.
Should not a reference manual be exhaustive?
There was a problem hiding this comment.
Well one cannot document every single program or sequence of tactics... But we could add this one... though I still believe it may be nicer packaged as a dedicated intropattern tactic view...
There was a problem hiding this comment.
The fact that move=> /(_ _)/wrap[] and move=> /(_ _) => /wrap[] are not equivalent triggers me a lot makes me feel like this needs some documentation. But maybe I just have a completely wrong model of what ssreflect does and I could have been able to guess what the combination does otherwise (although I have never seen wrap either).
|
@CohenCyril It looks like |
|
Where is topology.v ? |
|
Here ! |
- add generic makefile - add multinomials and analysis as dependencies
|
Should be fixed now |
|
@Tragicus this is a real error (in Coq 8.20+rc1) |
|
CI passes for Coq 8.18 and 8.19 🎉 |
Adds a definition of cylindrical decomposition and the required definitions and lemmas.