Stream: Coq users

Topic: Identical surface form but different with Print All

Mathieu Dehouck (Feb 14 2022 at 08:13):

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.

Li-yao (Feb 14 2022 at 08:22):

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).`

Mathieu Dehouck (Feb 14 2022 at 08:32):

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: Jun 25 2024 at 14:01 UTC