I thought about it a bit and reinvented Ralf's conclusion #473 (comment 83164), so should you just pick another delimiter, maybe non-ASCII?

I'm not 100% certain this is ambiguous but it seems to be, at least since Coq is restricted to onr token of lookahead (LL(1)): the `>>`

token has different meanings in `<< f >> g >>`

and `<< f >> g <<`

(it can be infix in the first, it can be a bracket in the second — and there might be more ways to complete these expressions), but looking at `g`

isn't enough to tell — we must get to the last token to distinguish the two, but LL(1) parsers don't look so far ahead. Splitting `>>`

in two tokens would make this even harder, since lookahead is still just one token.

FWIW, these axioms can now be implemented via an auth_frag on the monotone camera - start would use the auth, while finished would be persistent. Not sure if that'd be a simpler sketch?

I misspoke; IME these break so often to be bad style, hence worth avoiding in a style guide — but iris is different enough such tradeoffs can vary. ~~Closing.~~ (Can't resolve this thread, but you can pretend I did).

That seems pretty ambiguous if `component`

exists in multiple libraries; this will only import one `component`

.

This assumes that `SolveProperSubrelation`

is "reflexive" — that `SolveProperSubrelation R R`

is provable for any `R`

. That'll fail if `R`

has evars (and that's fine), but what about evar-free closed `R`

s? Maybe worth a unit test?

` LeibnizEquiv A → Discrete a → @IntoPure PROP (a ≡ b) (a = b) | 10.`

would ensure `Discrete a`

is only searched once.

**Paolo G. Giarrusso**
(d3f6c7e2)
*
at
03 Aug 15:54
*

Good idea but that's a potential breaking change because `Proper`

instances must "match `Params`

arity" or they're ignored. Does this mean the existing instances were never used?

Yes.

No I have not found out honestly.

Nice change overall! I'm curious if this is invertible (guess yes), but at the same time I can't imagine much use for the converse direction. If that's true, maybe

```
(* Invertible, but the converse doesn't seem useful. *)
```

(I'm trying not to delay this nice refactoring).

I think it is best if we remove the ofe section at the bottom of the file

Mostly agree, I've just used "principal is injective wrt `eq`

" so that kind-of thing might be useful. Sorry I didn't get to revise the MR, but I hope to do it this weekend.

Overall, it seems Ralf agrees with me the current `dist`

theory can be taken out even more completely, and that should help the next revision.

Okay — I'll keep the `S := eq`

instance and add `S := equiv`

one.

I'm not sure how to preserve the structure without a step-indexed preorder, do you have an idea?
I was claiming that's impossible, but maybe what you want is equivalent to *constructing* a (free?) step-indexed preorder — sth like `free_si_extension`

:

```
Program Definition free_si_extension {A : ofe} (R : A -> A -> Prop) : A -> A -> siProp :=
λ a d, {| siProp_holds n := ∃ b c, a ≡{n}≡ b ∧ R a b ∧ c ≡{n}≡ d |}.
Next Obligation.
intros * (b & c & ?) ?. exists b, c; naive_solver eauto using dist_le.
Qed.
```

No idea if proving extension is any easier.

Is there a reason why this would not work here, or is it just a bunch of work?

TLDR: AFAIK, ~~we~~ I don't even know. (EDIT: "we" might be too strong).

The construction doesn't need OFEs — it has no reason to use `equiv`

or `dist`

, it only uses the preorder. You want the preorder to respect `equiv`

and `dist`

appropriately, but that's only used in side lemmas like `principal_inj`

/`principal_ne`

.

But what I suspect it should do is support (some presentation of) preorders in `siProp`

: if `A`

is not discrete, non-constant relations on `A`

seem likely to violate non-expansiveness on `A`

.

After your comment, I tried to generalize to siProp orders naively: many proofs generalize easily, but I don't see how to prove the extension axiom for the adapted camera. @amintimany did you already try?

I was thinking of `principal_includedN`

even if I use a synonym, but we should probably remove the theory for `dist`

.

The concern is that applying this "forward" (`apply inj in H`

) would have to pick `S`

by TC search on `AntiSymm`

, which lacks any mode. That's a regression in this MR.

The options are:

- make it export so that people must opt-in to this by importing the nested module.
- just make it a lemma, like Iris does today for other problematic instances.

If your concern stands I'd prefer option 2.

They do: we're defining a discrete OFE with `discreteO`

, and that requires instances for `Equiv`

and `Equivalence equiv`

.

Note on locker: all existing releases lack https://github.com/LPCIC/coq-elpi/pull/450; so `mlock Definition id {A} (a : A) := a.`

will only mark `A`

implicit locally.

More in general, that bug doesn't apply in math-comp's context because of `Set Implicit Arguments`

, and coq-elpi is much less tested outside of math-comp — we in Bedrock might be the main other user. But we're overall pretty happy with elpi maintenance :-).