Dear All,

I have formula of the shape `~ exists n, P n`

and I would like to use `not_ex_all_not`

to make it `forall n, ~ P n`

.

When I specialize `not_ex_all_not`

and fold the necessary type aliases, I still can't apply the resulting hypothesis to the `~ exists `

one.

Upon further inspection with Set Printing All, it seems the two things are subtly different, but I don't know how to make them converge:

```
COMP : forall
_ : @ex nat
(fun n : nat =>
incompatible_n (@edge tile t1 t2) n
(@pair cgraph tgraph
(@pair (list cell) (list (@iedge cell)) cells cedges)
(@pair (list tile) (list (@iedge tile)) tiles edges))),
False
EXALL : forall
(_ : forall
_ : @ex nat
(fun n : nat =>
incompatible_n (@edge tile t1 t2) n
(@pair cgraph tgraph
(@pair (list cell) (list (@iedge cell)) cells
cedges)
(@pair (list tile) (list (@iedge tile)) tiles
edges))), False) (n : nat),
not
(incompatible_n (@edge tile t1 t2) n
(@pair cgraph tgraph
(@pair (list cell) (list (@iedge cell)) cells cedges)
(@pair (list tile) (list (@iedge tile)) tiles edges)))
```

In the EXALL, the property with the existential is wrapped in `(_ : forall _: .... ) (n : nat)`

Do you know of a way to fix this ?

Best.

The lemma does match. The issue is `apply`

tries to instantiate all the parameters of the given lemma, including `n`

.

One way out is `assert (myH := not_ex_all_not _ _ COMP).`

The `assert`

complains that the output does not have the right type. However by doing `specialize _ _ COMP`

I get something close to what I wanted to I'll go with that.

Last updated: Sep 23 2023 at 07:01 UTC