Methodology for user-friendly types without UIP on the index #39
Comments
|
Cyrill Cohen thinks the fold intuition may be right here. We are going to play with this tomorrow. |
|
Also, generating the equivalence between { l : list T | length l = n } and vector T n and implementing lifting along that as well may be another way around this. There is an issue open for that, too. |
|
I think generally showing the latter equivalence directly from the former relies on UIP over the index. But maybe I can get that from something else, like from the fact that length is a fold that projects the first element of ltv. |
|
If we Going to see if I can derive the whole equivalence without relying on UIP over |
What is "the former" here, and what is "the latter equivalence"? |
|
I tried playing with However, I think using this type instead of Inductive tlist (A : Type) : Type -> Type :=
| tnil : tlist A Empty_set
| tcons (a : A) {T} (xs : tlist A T) : tlist A (option T).(Note that, with this type, |
|
Are these the other definitions you're looking for, re proving the equivalence? Fixpoint ltv_u' (A : Type) (n : nat) (v : vector A n)
: { l : list A & ltv_index A l = n}
:= match v in vector _ n return { l : list A & ltv_index A l = n} with
| Vector.nil _ => existT _ nil eq_refl
| Vector.cons _ x _ xs => existT _ (cons x (projT1 (ltv_u' A _ xs)))
(f_equal S (projT2 (ltv_u' A _ xs)))
end.
Lemma ltv_u'u {A n x} : ltv_u' A n (ltv_u A n x) = x.
Proof.
destruct x as [l H].
cbv [ltv_coh ltv_u]; subst n; cbn [eq_rect projT1 projT2].
cbv [ltv].
cbn.
induction l as [|x xs IHxs]; [ reflexivity | ].
cbn.
rewrite IHxs; clear IHxs; cbn; reflexivity.
Qed.
Lemma ltv_uu' {A n x} : ltv_u A n (ltv_u' A n x) = x.
Proof.
induction x; cbn; [ reflexivity | ].
cbv [ltv_u] in *.
cbn.
generalize dependent (ltv_u' A n x); intros [x' H]; intros; subst; cbn.
reflexivity.
Qed. |
|
Not quite. That's what I mean by showing that equivalence directly in the tool; we don't do that yet. I want to figure out if I can avoid doing that. So I want that equivalence, but I want to see if it's possible to show it via functions: that form an equivalence, but without relying on UIP on the index, even implicitly. So defining the functions in is not very hard: But to show section and retraction this way, I think you have to show that all proofs of: lift to eq_refl. I basically don't want to depend on anything other than the ltv, ltv_inv, section, retraction, coherence, the fact that ltv_index is a fold, and the constructors and eliminators for eq and sigT. |
|
It's probably not a good idea to try to solve this without playing around with the Example.v file or you lose context. You can: To get section, retraction, and coherence over sigma if you do that. If I can't show it generally, I want to see if I can construct my user-friendly functions such a way that I can avoid relying on the index, and instead this will reduce nicely. |
|
I also don't want to change the type of list and vector; they're important because they are just two easy examples of a broader class of types with nice properties the tool can automate. This is why I want to see if I can avoid relying on any facts other than the ones I mentioned before. |
|
Is |
You need one more property (at least): you need that the section and retraction form an half-adjoint-equivalence: ltv_adjuction : forall A x, ltv_retraction A (ltv A x) = f_equal (ltv A) (ltv_section A x)If you have this, then (at least in cases where Lemma ltv_ltv_inv : forall A n v, ltv_u A n (ltv_inv_u A n v) = v.
Proof.
cbv [ltv_u ltv_inv_u].
cbn [projT1 projT2].
intros.
set (p := ltv_retraction _ _).
set (q := ltv_coh _ _).
clearbody p q.
cbv beta in *.
generalize dependent (ltv A (ltv_inv A (existT [eta vector A] n v))).
intros [x y] p q.
cbn [projT1 projT2] in *.
subst x.
inversion_sigma.
repeat match goal with H : _ = ?v |- _ => is_var v; destruct H end.
reflexivity.
Qed.
Lemma ltv_inv_ltv : forall A n v, ltv_inv_u A n (ltv_u A n v) = v.
Proof.
intros A n [l H]; apply eq_sigT_uncurried; subst n.
cbv [ltv_u ltv_inv_u ltv_coh].
cbn [projT1 projT2 eq_rect].
change (existT [eta vector A] (ltv_index A l) (projT2 (ltv A l))) with (ltv A l).
exists (ltv_section _ _).
rewrite ltv_adjuction.
destruct (ltv_section A l).
reflexivity.
Qed.(These proofs are a bit messy, sorry.) Is this what you're looking for? |
|
Neat! Adjunction should always follow from section and retraction, according at least to the proof from EFF. Next we need to derive the proof of adjunction (#57) and figure out how to use it to port proofs as in Example.v. |
|
Adjunction (credit to Jasper) with few dependencies: https://github.com/jashug/IWTypes/blob/master/Adjointification.v I think we should start by generating applications of this automatically, and then using that to manually write some unfolded equivalences. Then, once we understand what those proofs look like, we can automatically generate the unfolded equivalence with an option. Doing that would build the groundwork necessary to understand how to repeat the same process for other functions and proofs. We can then do those manually, then work on automating those. But even generating the other version of the equivalence means we can already provide a very powerful tool for hooking into tools like EFF. |
|
I will likely not get to this myself, but I still am super curious!! |
|
My student @cosmoviola may look at this a bit, which is cool! The language in this issue is a bit out-of-date. Note that adjunction has been proven, but we're still trying to figure out whether we can get interesting proofs for Example.v without relying on UIP on the index. There should be a corresponding comment in Example.v that mentions this issue. |
|
Still stuck on the more general question about UIP. Have a Tweet thread going: https://twitter.com/TaliaRinger/status/1475897510342594560 |
|
Conor McBride has refined this question---we need UIP to hold locally on the elements in the range of the function in the return datatype. But such datatypes should exist. Remains to be seen whether this is at all consequential for making proofs of equalities between equalities easier though |
As I said at https://twitter.com/diagram_chaser/status/1475941698739965955, probably the way you want to state this is that, if your indexing function is |
In
Example.v, the current methodology for deriving the user-friendly type of the proof uses the fact that nat is an hSet, and so the auxiliary rewrites we apply are irrelevant. It would be nice to have a methodology that does not rely on this fact. While many indices have types that are hSet, and while UIP can safely be assumed in Coq in general, it's still not great.Without UIP, the way the rewrites for the other user-friendly types are derived should be relevant. Thus the methodology should instruct the user to write the auxiliary lemma proofs in such a way that proofs of equalities between rewrites using the auxiliary lemmas will go through easily (and eventually, automation should help with this).
I think more generally that even when the index type itself isn't an hSet, there's something about the structure of an algebraic ornament here that is useful: the new index must fully determined by a fold over the old type. So my guess is that this forces some structure on the indices themselves that makes this possible without relying on any properties of the type. The intuition is fuzzy, though, and I don't know how to reify it into the code yet. (Please comment if you do!)
The text was updated successfully, but these errors were encountered: