Stream: math-comp users

Topic: How to discharge annoying dis-equality patterns


view this post on Zulip walker (Nov 10 2022 at 16:14):

So many times I am faced with a situation where hypthesis s (k <> k') and goal is (k' <> k) note that both k and k' are eqType.

Is there a way to automatically discharge those quickly without having to do a move + by apply maneuver ?

view this post on Zulip Julien Puydt (Nov 10 2022 at 16:31):

@walker: use simplification items?

view this post on Zulip walker (Nov 10 2022 at 17:38):

so basically unless I misunderstood you are advising me to use // but this simplification does not match a <> b with b <> a

view this post on Zulip Julien Puydt (Nov 10 2022 at 17:54):

No, I misunderstood your question because I hadn't seen the reversal: sorry.

view this post on Zulip Paolo Giarrusso (Nov 10 2022 at 20:17):

Stdpp's done handles this via a lemma (called not_symmetry); I suspect you could add a Hint to the core database for this

view this post on Zulip Pierre Jouvelot (Nov 10 2022 at 20:33):

walker said:

So many times I am faced with a situation where hypthesis s (k <> k') and goal is (k' <> k) note that both k and k' are eqType.

Is there a way to automatically discharge those quickly without having to do a move + by apply maneuver ?

Not automatic but a bit shorter would be, if h is the hypothesis, to use by apply: (contra_not _ _ _ h).

view this post on Zulip Michael Soegtrop (Nov 11 2022 at 07:44):

@Paolo Giarrusso : I am in general not a fan of cyclic hints in the core database unless they are gated to ensure they make sense.

view this post on Zulip walker (Nov 11 2022 at 08:52):

What is a cyclic hint ?

view this post on Zulip Ana de Almeida Borges (Nov 11 2022 at 09:54):

A hint that can be applied ad infinitum. Here if you have a <> b you can apply the rule to obtain b <> a, and then again to obtain a <> b, and so on.

view this post on Zulip Paolo Giarrusso (Nov 11 2022 at 11:20):

Good point; would Hint Immediate help, and still let trivial use it?

view this post on Zulip Paolo Giarrusso (Nov 11 2022 at 11:20):

stdpp mentions it explicitly in the body of done but that seems excessively invasive.

view this post on Zulip Michael Soegtrop (Nov 11 2022 at 12:27):

@Paolo Giarrusso : yes, using Hint Immediate would solve this - it requires that the premises of the application can be solved by trivial. trivial is like auto - so it again uses core, but it uses only hints which don't produce additional hypothesis.

view this post on Zulip Michael Soegtrop (Nov 11 2022 at 14:03):

@Paolo Giarrusso : sorry I didn't read your question properly. As far as I understand this trivial wouldn't use it anyway, because trivial uses only 0-cost hints, that is (again afaik) hints which don't produce new premises.


Last updated: Feb 08 2023 at 04:04 UTC