As some might know, if inference fails on `foo`

in a statement, writing `foo : bar`

to help inference comes back to bite you. Could that be fixed?

I've just explained the pitfall to a colleague. What I (or a typical user) wants is "produce `foo`

but use `bar`

to help inference", but the result they get still contains the ascription. Hence _some_ tactics (IME, `rewrite`

) might fail to find occurrences of `foo : bar`

in the goal (because there are none!)

Does SSR's rewrite have this problem too?

not sure but I expect yes

and syntactic matching feels too common in Coq to live with casts

Not sure I understand you: are you saying that the type cast should be removed after successful inference or do you say that rewrite should be smarter? I guess you will need the cast during Qed time if you did need it during proof term construction.

what stdpp and Iris do (I suspect for this reason, but haven't confirmed) is write implicit arguments by hand — they even have dedicated syntax for _all_ operators.

it should be removed after inference

Won't you have issues during Qed then?

and I must have been unclear, because it seems clear you don't need these casts it at qed time

this is not in the proof but in statements

Ah ok, I see.

I mean, you could do the same in proofs, since these casts are about inference, not those produced by `simpl/compute/vm_compute/...`

an example of the disambiguation is https://gitlab.mpi-sws.org/iris/stdpp/-/blob/5843163bd51a5f1a7310ffb64bda3b4c6bb50c0c/theories/coGset.v#L192:

```
Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
x ∈@{C} coGset_to_top_set X ↔ x ∈ X.
```

instead of

```
Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
x ∈ (coGset_to_top_set X : C) ↔ x ∈ X.
```

where `∈@{C}`

is a variant of `∈`

to specify `C`

as an implicit argument

(I'll admit that this isn't enough to show problems with `rewrite`

or `auto`

; this felt like a known problem which I knew about, but if it isn't I can investigate)

I am still struggling to understand the connection: the @ variant of the ∈ infix operators is required to avoid the `: C `

type ascription because it would later make pattern matching for a rewrite more difficult?

@Paolo Giarrusso you can probably write a clever notation with tactic in terms to emulate a transparent cast.

We have already a bit of machinery to work around casts but it's fragile.

I believe that we should not try to hide this complexity from the user and clearly delineate "kind-of-proof-relevant" casts with mere type annotations.

(notwithstanding the fact casts are also heavily used in the legacy unification engine for horrible reasons)

If we want to introduce a language feature it might be yet another occasion to reuse the Program cast syntax

This might be naïve, but could it be possible to keep these kind of ascriptions around for typing purposes, but ignore them when comparing terms? I have used this trick on paper exactly to avoid the problem you describe of two terms not being considered equal/convertible because they have different casts in them.

define "comparing"

(ftr we already skip cast nodes in all equality functions I know of in the codebase)

Ah, that is what I meant

But then how come they can lead `rewrite`

astray if they are ignored when comparing terms?

because term equality is far to be pattern recognition

term equality is a somewhat *easy* problem, although we already have way too many ways to define it.

easy when compared to pattern recognition which has a crazy number of moving parts

Everything is simple in the marvelous world of paper :upside_down:

(pattern recognition contains unification so this gives you a lower bound)

my personal take on that is that the problem is not so much rewrite being sensitive to casts than the vast discrepancy we can observe in the handling of cast nodes

(hint: this reminds me of the primitive projection mess)

Naïve question: what is wrong with defining the identity function as an annotation gadget & using `unfold`

to magic it away when needed?

```
Definition Identity (A : Type) (a : A) : A := a.
Notation "A ∋ a" := (Identity A a) (at level 3).
Goal forall n, nat ∋ n = n + O.
intros. unfold Identity.
```

(disregard the random level, I couldn't be bothered to look up how to make it right associative)

It won't work for OP's use because he wants to pass such terms to tactics.

Right this seems to work

```
Definition Identity (A : Type) (a : A) : A := a.
Ltac Ann A a :=
let annotated := let h := fresh "H" in pose (h := Identity A a); exact a in
let val := eval cbn zeta in ltac:(annotated) in
exact val.
Notation "A ∋ a" := ltac:(Ann A a) (at level 3).
Goal forall n, n = n + O.
intro n. rewrite plus_n_O with (n := nat ∋ n).
```

But then again my example is super naïve and Coq already knew that `n`

was of type `nat`

so I don't know whether it'd work in OP's case.

No, unfortunately IIUC ltac quotations force to evaluate the term first, so you lose the typing constraint. You might be able to do that in Ltac2 because you have access to the untyped term in the quotation there.

I agree that the two casts should have different syntaxes — I think the new one should be the "default", but I can just tell colleagues

if it can be implemented in Coq itself, great, but I feel that it belongs in the stdlib and the manual...

Pierre-Marie Pédrot said:

you lose the typing constraint

I'm not sure I understand what you mean. If you put the wrong type annotation there (e.g. `list nat`

) you do get an error. So there is some checking.

What I mean is that the type of the term is first inferred without any use of the type cast, and *then* the result is checked for convertibility with the cast.

This is not what is asked in this thread, i.e. the type cast needs to be taken into account in the inference phase (e.g. to help resolving typeclasses and whatnot)

I see. I guess I don't know enough about Coq's internals to have a good feeling for what is going to work or not. Even with inference first, I would assume I'd get some evars if the problem is under-constrained and these would then be solved by unification when checking against the constraint.

@gallais yes, that would work, the only issue here is that you can't get a "partial term" or even an surface one to be passed to the tactic

Last updated: Jun 24 2024 at 01:01 UTC