Stream: Coq users

Topic: Tactic fails, but not its definition

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?

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?

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?

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.

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.

Gaëtan Gilbert (Dec 16 2020 at 14:02):

so what's the real definition of in_fset_auto?

Théo Winterhalter (Dec 16 2020 at 14:43):

That's the real one…

Théo Winterhalter (Dec 16 2020 at 14:44):

Now it's

Ltac in_fset_auto :=
  rewrite in_fset ; reflexivity.

Pierre-Marie Pédrot (Dec 16 2020 at 14:44):

Is it the same in_fset?

Pierre-Marie Pédrot (Dec 16 2020 at 14:44):

Have you tried printing all?

Pierre-Marie Pédrot (Dec 16 2020 at 14:45):

It could have resolved typeclasses differently.

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.

Pierre-Marie Pédrot (Dec 16 2020 at 14:48):

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

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

Pierre-Marie Pédrot (Dec 16 2020 at 14:48):

Don't trust Ltac printing.

Pierre-Marie Pédrot (Dec 16 2020 at 14:49):

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

Théo Winterhalter (Dec 16 2020 at 14:49):

Then which printing should I check

Pierre-Marie Pédrot (Dec 16 2020 at 14:49):

Like, Definition foo := in_fet. Print foo.

Théo Winterhalter (Dec 16 2020 at 14:49):

Ltac tactics.in_fset_auto := rewrite in_fset; reflexivity

Théo Winterhalter (Dec 16 2020 at 14:51):

From the terminal, the output is literally the same.

Théo Winterhalter (Dec 16 2020 at 14:51):

(Using Set Printing All in both)

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.

Théo Winterhalter (Dec 16 2020 at 14:53):

Ok found it…

Théo Winterhalter (Dec 16 2020 at 14:53):

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

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.

Théo Winterhalter (Dec 16 2020 at 14:57):

Thanks for your help!

Last updated: Sep 23 2023 at 14:01 UTC