Stream: Coq users

Topic: Tactic fails, but not its definition


view this post on Zulip Théo Winterhalter (Dec 16 2020 at 13:35):

Hi, I'm having a problem I can't really understand (with coq 8.12.1).
I have a goal (using extructures but it's probably irrelevant):

0 \in [fset 0]

and a tactic in scope which prints to

in_fset_auto := rewrite in_fset; auto

but in_fset_auto fails with

Found no subterm matching (...)

while

rewrite in_fset; auto.

works and solves the goal.
Am I missing something stupid?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 13:37):

Isn't that a problem with auto printing? Like, it used to evaluate as auto with * or something?

view this post on Zulip Gaëtan Gilbert (Dec 16 2020 at 13:37):

if you do Ltac in_fset_auto_2 := rewrite in_fset; auto. and use that does it work?

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 13:56):

Gaëtan Gilbert said:

if you do Ltac in_fset_auto_2 := rewrite in_fset; auto. and use that does it work?

Yes it does.

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 13:59):

Pierre-Marie Pédrot said:

Isn't that a problem with auto printing? Like, it used to evaluate as auto with * or something?

No, it's not that. I just changed auto with reflexivity and it has the exact same resutl.

view this post on Zulip Gaëtan Gilbert (Dec 16 2020 at 14:02):

so what's the real definition of in_fset_auto?

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:43):

That's the real one…

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:44):

Now it's

Ltac in_fset_auto :=
  rewrite in_fset ; reflexivity.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:44):

Is it the same in_fset?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:44):

Have you tried printing all?

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:45):

It could have resolved typeclasses differently.

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:46):

It's the same in_fset I checked the default interpretation is the same in both locations.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:48):

Really really? Like, you diffed the output of printing all?

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:48):

With Set Printing All I still get

Ltac Foo.Bar.tactics.in_fset_auto := rewrite in_fset; reflexivity

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:48):

Don't trust Ltac printing.

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:49):

Go to the file defining the tactic and print it there.

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:49):

Then which printing should I check

view this post on Zulip Pierre-Marie Pédrot (Dec 16 2020 at 14:49):

Like, Definition foo := in_fet. Print foo.

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:49):

Ltac tactics.in_fset_auto := rewrite in_fset; reflexivity

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:51):

From the terminal, the output is literally the same.

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:51):

(Using Set Printing All in both)

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:53):

I used a fully qualified name for in_fset:

rewrite extructures.fset.in_fset ; reflexivity.

But no change.

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:53):

Ok found it…

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:53):

I forgot about one thing… rewrite is not the same in both files…

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:54):

This is really terrible that they are both bearing the same name and that printing also doesn't differentiate them.

view this post on Zulip Théo Winterhalter (Dec 16 2020 at 14:57):

Thanks for your help!


Last updated: Feb 08 2023 at 23:03 UTC