Skip to content
Snippets Groups Projects

Adapt w.r.t. coq/coq#12512.

Closed Ghost User requested to merge (removed):globref-in-auto-using into master
3 unresolved threads

This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.

https://github.com/coq/coq/pull/12512

Edited by Ralf Jung

Merge request reports

Closed by avatar (May 2, 2025 2:12pm UTC)

Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
182 182 intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
183 183 induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
184 184 repeat case_decide;
185 constructor; eauto using HdRel_list_merge, HdRel_cons, total_not.
185 constructor; epose proof total_not; eauto using HdRel_list_merge, HdRel_cons.
  • Why does this make any sense? Is total_not not an identifier?

  • Author Contributor

    No, the current implementation handles it as a term and thus resolves typeclasses, infers implicit arguments and whatnot. The linked Coq PR changes the behaviour, but if you want backwards compatibility you need to do this kind of gymnastic.

  • So the new behavior is that total_not here basically becomes @total_not, and for some reason that does not work? Why not?

  • Author Contributor

    Before the Coq PR, there is a broken heuristic to try to reabstract over evars, so you can get strange results sometimes. For simple cases it does work though.

  • That doesn't answer the question of why this epose horribleness is needed after the Coq PR.

  • Although I agree that the old behavior was broken, I'm not sure I like this eposs horribleness any better, and I'm wondering how much fall-out this is going to cause for Iris and our reverse dependencies.

  • Author Contributor

    @jung what's your expected behaviour then? I don't understand whether you complain about the use of epose vs. pose or that you'd like something completely different.

    @robbertkrebbers I am trying to assess it with the Coq CI. The changes are limited, most of the big developments pass after a handful of systematic changes.

  • Ok, I would like to see the impact on Iris and RustBelt before merging this MR. Also, I would be in favor to see if we can refactor the code to avoid these epose commands, which are horrible. To understand what's going on, can you answer @jung's question about:

    So the new behavior is that total_not here basically becomes @total_not, and for some reason that does not work? Why not?

    If auto with lem basically becomes auto with @lem in current Coq, I will see if I can make that to work.

  • Author Contributor

    If auto with lem basically becomes auto with @lem in current Coq, I will see if I can make that to work.

    This is the new semantics indeed. It doesn't work in the above example because when intepreting total_not as a term typeclass resolution kicks in and fills in the missing instances. If you were to call @total_not instead you'd get a more general term that eauto doesn't know what to do with.

  • Right, so the problem is that the lemma then has a TC premise, and eauto won't solve that because it doesn't use the typeclass_instances database by default.

    I have experienced that problem many times before, and "fixed" it in some occasions in a rather ad hoc way by re-declaring some type class instances in the core hint data base. See https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/base_logic/bi.v#L158 for an example.

    This is truly horrible, and IMHO we need a more structural fix for this. Any idea?

  • This is the new semantics indeed. It doesn't work in the above example because when intepreting total_not as a term typeclass resolution kicks in and fills in the missing instances. If you were to call @total_not instead you'd get a more general term that eauto doesn't know what to do with.

    Thanks, that information is what I was trying to acquire twice but I clearly failed to express myself. :)

    And indeed, it it rather problematic that there are lemmas that eapply can use just fine (through TC resolution) but that eauto is unable to use (as it does not do TC resolution).

  • Please register or sign in to reply
  • Ralf Jung changed the description

    changed the description

  • Author Contributor

    FTR, the Coq PR is only motivated by cleaning up of the hint database implementation. I guess I could emulate the old behaviour by automatically pose-ing the terms passed as using arguments. This would be good enough for my purposes, but that means that there is still a magical phase of resolution that the user has no control over, even less since she cannot write arbitrary terms anymore (in particular @foo).

  • I am very sympathetic to cleaning up the code. However, what I would like to point out that it's useful to use lemmas that are polymorphic in a type class as hints to eauto. The current behavior is unreliable, but does sometime work. I think we should find a principle solution for this.

  • Robbert Krebbers mentioned in merge request !166 (merged)

    mentioned in merge request !166 (merged)

  • Here's an alternative for this MR without epose: !166 (merged)

  • Author Contributor

    Should I close this PR in favour of the other one? I confirm that the other one is working with the corresponding Coq PR.

  • Author Contributor

    I also have this PR's little sister for Iris. It's quite short (18 line diff) but uses the pose tricks, if you want to use it as a stub for a cleaner variant I can submit it there.

  • Ghost User mentioned in merge request iris!464 (closed)

    mentioned in merge request iris!464 (closed)

    • Author Contributor

      BTW, do not hesitate to comment on the Coq PR about the expected semantics of the using clause for auto, and of the whole tactic more generally. It's actually a bit strange that typeclasses are never resolved when applying hints, regardless of the using clause. I don't use typeclasses regularly, but the following snipped looks like a bug to me. (This is the point where you can start screaming that fixing this would be nonsense.)

      Class Foo.
      
      Instance foo : Foo := {}.
      
      Axiom bar : Foo -> False.
      
      Arguments bar {_}.
      
      Hint Resolve bar : mydb.
      
      Goal False.
      Proof.
      Fail solve [eauto with mydb].
    • Has this already been reported as a Coq bug?

    • Please register or sign in to reply
  • I agree that's a bug. I think auto/eauto should solve type class goals during search too, then this example would work. Note that it can be fixed in an adhoc way by adding Hint Resolve foo : mydb. However, that approach clearly doesn't scale, because you obviously don't want to duplicate the whole TC hint database into your own hint database manually.

  • Since !166 (merged) superseded this MR, I'm closing it. Thanks @ppedrot.

  • closed

  • Please register or sign in to reply
    Loading