Mathieu Dehouck (Feb 14 2022 at 08:13): 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: Sep 23 2023 at 07:01 UTC