Use agree instead of dec_agree
This demonstrates that a list-based agreement could work, and form an OFE. I didn't bother to prove all the functor laws.
Man, this reasoning with about the lists is annoying^^.
What I don't like about this is that un-injection (agree_car) is only non-expansive for valid elements. I want to try using a different equivalence relation, maybe I can find one where this works.
Merge request reports
Activity
Hm.... I came to the conclusion that actually, we can't have a non-expansive uninjection that always works.
uninj (x * y)anduninj (y * x)would have to return the same thing no matter thexandy, which I don't think is actually possible.I'll go on doing the functor laws then. ;) I'm sure we can clean up that mess I did with
list_agreeslater.Nice to see that this works!
Any idea how much do we make use of the "uninjection" in the case of
dec_agree? I once tried reformulatingdec_agreein terms of thedraconstruction so as to get rid of the decidable equality constraint, and -- if I recall correctly -- not being able case on whether it is aDecAgreeorDecAgreeBotmade some uses of it quite annoying. However, I think the new auth construction made many occurrences of this kind of reasoning disappear, so it may be alright.-
Indeed the current definition just doesn't work. The mapped arrows are not non-expansive, they do not even preserve equivalence.
The trouble is as follows: Imagine we start with
agree nat, with the two non-empty lists[0,2]and[1,3]. These two are equal, since they are both invalid. Now we map this toagree boolthrougheven. The lists now read[true,true]and[false,false]-- that is, the lists are both valid, and unqeual. So we mapped two equal elements to two unequal elements. Ouch :/ Added 1 commit:
- 735ffa30 - WIP: use different equivalence relation for list_agree
-
I am now trying to use a different equivalence relation, one that doesn't "cheat" by just equating all invalid elements. (As usual, when you do stuff fully higher-order, cheating doesn't work.)
I am now stuck swapping a universal and an existential quantifier... but I actually believe that because of finiteness and the pigeon hole principle, this is legit. @jtassaro you proved the pigeon hole principle for the termination-preservation business, is there a part of that that's entirely independent from your application (much like the formulation you had in the paper), something we could copy to Iris proper?
@ralf, in an earlier email thread:
if it works -- should be able to replace both agree and dec_agree: It supports COFEs, but when used on a discrete COFE, it produces a discrete COFE; and when used on a COFE with decidable equality, its equality is decidable.
Note that one more property would be very desirable for it to be able to replace
dec_agree. To avoid reasoning with setoids, we would like the setoid equality ofagree Ato coincide with its Leibniz equality in case that happens forAtoo. In Coq terms:Instance agree_leibniz : LeibnizEquiv A → LeibnizEquiv (agree A).(We have similar instances for pretty much all RA constructions apart from STS)
However, this pretty much means we need canonical representations, which I don't believe is possible.
Edited by Robbert KrebbersAdded 1 commit:
- 38b6f264 - WIP: use different equivalence relation for list_agree
-
Right, we won't get Leibniz equality, just discrete decidable Setoid equality. How bad would that be? Isn't there some theorem that if you have decidable equality, you can take the quotient to get Leibniz equality?
I managed to prove that my desired construction forms an OFE, assuming the following lemma:
Context `(R : nat → A → Prop). Hypothesis R_le : forall m n a, m ≤ n → R n a → R m a. Lemma Forall_Exist_swap (l : list A) : (∀ n, Exists (R n) l) → Exists (λ x, ∀ n, R n x) l.I feel like this lemma ought to be in the prelude anyway, as part of our extensive List theory. Or is it (or some part of it) maybe even proven somewhere in Coq's stdlib or the prelude already? For now I just assumed it, to avoid proving the same thing again.
Right, we won't get Leibniz equality, just discrete decidable Setoid equality. How bad would that be?
Well, it means that whenever
agreeappears in one's RA construction, one has to use the setoid rewriter (which is less reliable) and declare all operations on that RA construction to be proper.Isn't there some theorem that if you have decidable equality, you can take the quotient to get Leibniz equality?
If only Coq had quotients! (Let's hope HITs give us those in our next life ;) )
I managed to prove that my desired construction forms an OFE, assuming the following lemma:
Context `(R : nat → A → Prop). Hypothesis R_le : forall m n a, m ≤ n → R n a → R m a. Lemma Forall_Exist_swap (l : list A) : (∀ n, Exists (R n) l) → Exists (λ x, ∀ n, R n x) l.Are you sure that is provable constructively? I have no intuition why it would be.
From your lemma you can prove:
Section scary. Context (P1 : nat → Prop) (P2 : nat → Prop). Context (P1_le : ∀ m n, m ≤ n → P1 n → P1 m). Context (P2_le : ∀ m n, m ≤ n → P2 n → P2 m). Lemma foo : (∀ n, P1 n ∨ P2 n) → (∀ n, P1 n) ∨ (∀ n, P2 n).Without the monotonicity requirements this surely does not hold constructively (take
P1 nto be Turing machinexterminates withinnsteps, andP2 nto be Turing machinexdoes not terminate withinnsteps).However, with the monotonicity requirements I am less sure.
Edited by Robbert KrebbersAdded 1 commit:
- 95d12e3f - WIP: use different equivalence relation for list_agree
-
This theorem is (if I made no typo) the core of how @jtassaro proved fair termination-presevration using Iris. See page 21 of the paper for more details.
Roughly speaking, the intuition is that in that family of existence proofs on the left, there are only finitely many choices for list elements -- so there has to be a list element that appears infinitely often. For that element, we have
R n xfor infinitely manyn, and thus, by down-closure, for alln.
