Adapt w.r.t. coq/coq#12512.
This removes the reliance on auto using clauses being arbitrary terms. In theory, should be backwards compatible.
Merge request reports
Activity
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. @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 becomesauto with @lem
in current Coq, I will see if I can make that to work.If
auto with lem
basically becomesauto 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 thateauto
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 thetypeclass_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 thateauto
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 thateauto
is unable to use (as it does not do TC resolution).
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 asusing
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
).mentioned in merge request !166 (merged)
Here's an alternative for this MR without
epose
: !166 (merged)let's see what @jung thinks.
I have a slight preference for !166 (merged), but really I hardly care.
Then let's go for !166 (merged). I think the pose style has some serious issues:
- If you don't specify the implicit arguments, it suffers from the same issue as the current setup: it picks an arbitrary type class instance.
- If you do stuff like
pose ...; split; [by auto|]
the posed lemma remains in the second goal too.
mentioned in merge request iris!464 (closed)
BTW, do not hesitate to comment on the Coq PR about the expected semantics of the
using
clause forauto
, and of the whole tactic more generally. It's actually a bit strange that typeclasses are never resolved when applying hints, regardless of theusing
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].
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 addingHint 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.