Stream: math-comp users

Topic: How to discharge annoying dis-equality patterns

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 ?

Julien Puydt (Nov 10 2022 at 16:31):

@walker: use simplification items?

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

Julien Puydt (Nov 10 2022 at 17:54):

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

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

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

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.

walker (Nov 11 2022 at 08:52):

What is a cyclic hint ?

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.

Paolo Giarrusso (Nov 11 2022 at 11:20):

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

Paolo Giarrusso (Nov 11 2022 at 11:20):

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

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.

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