Stream: Coq users

Topic: Identical surface form but different with Print All


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC