Methodology for user-friendly types without UIP on the index

[tlringer]

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!)

[tlringer]

Cyrill Cohen thinks the fold intuition may be right here. We are going to play with this tomorrow.

[tlringer]

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.

[tlringer]

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.

[tlringer]

If we Set DEVOID search prove coherence, then it's easy to get ltv_u:

Definition ltv_u (A : Type) (n : nat) (ll : { l : list A & ltv_index A l = n}) :=
  @eq_rect 
    nat
    (ltv_index _ (projT1 ll))
    (vector A)
    (@eq_rect 
      nat
      (projT1 (ltv _ (projT1 ll))) 
      (vector A)
      (projT2 (ltv _ (projT1 ll)))
      (ltv_index _ (projT1 ll))
      (ltv_coh _ (projT1 ll)))
    n
    (projT2 ll).

Going to see if I can derive the whole equivalence without relying on UIP over nat, though.

[JasonGross]

I think generally showing the latter equivalence directly from the former relies on UIP over the index

What is "the former" here, and what is "the latter equivalence"?

[JasonGross]

I tried playing with Example.v a bit, but I think I don't have enough context here to do anything.

However, I think using this type instead of vector will be informative in trying to drive things:

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, zip_index' and zip_with_index' are highly non-trivial, though still true. (They are true because forall x : tlist A T, T = option^(length x) Empty_set.))

[JasonGross]

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.

[tlringer]

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:

ltv : list A -> sigT (vector A)
ltv_inv : sigT (vector A) -> list A

that form an equivalence, but without relying on UIP on the index, even implicitly.

So defining the functions in is not very hard:

Definition ltv_u (A : Type) (n : nat) (ll : { l : list A & ltv_index A l = n}) : vector A n :=
  eq_rect
    (ltv_index _ (projT1 ll))
    (vector A)
    (eq_rect
      (projT1 (ltv _ (projT1 ll))) 
      (vector A)
      (projT2 (ltv _ (projT1 ll)))
      (ltv_index _ (projT1 ll))
      (ltv_coh _ (projT1 ll))) 
    n
    (projT2 ll). (* ltv_index A l = n *)

Definition ltv_inv_u (A : Type) (n : nat) (v : vector A n) : { l : list A & ltv_index A l = n} :=
  existT 
    (fun (l : list A) => ltv_index _ l = n)
    (ltv_inv _ (existT _ n v)) 
    (eq_rect
      (projT1 (ltv A (ltv_inv A (existT _ n v))))
      (fun n0 : nat => n0 = n)
      (eq_rect
        (existT _ n v)
        (fun s : sigT (vector A) => projT1 s = n)
        (eq_refl (projT1 (existT _ n v)))
        (ltv A (ltv_inv A (existT _ n v)))
        (eq_sym (ltv_retraction _ (existT _ n v))))
      (ltv_index _ (ltv_inv _ (existT _ n v)))
      (ltv_coh _ (ltv_inv _ (existT _ n v)))).

But to show section and retraction this way, I think you have to show that all proofs of:

ltv_index A l = n

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.

[tlringer]

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:

Set DEVOID search prove coherence.
Set DEVOID search prove equivalence.

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.

[tlringer]

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.

[JasonGross]

Is Find ornament supposed to error with Set DEVOID search prove equivalence. on exotic indices?

[JasonGross]

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.

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 coh is refl), you can prove your equivalence:

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?

[tlringer]

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.

[tlringer]

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.

[tlringer]

I will likely not get to this myself, but I still am super curious!!

[tlringer]

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.

[tlringer]

Still stuck on the more general question about UIP. Have a Tweet thread going: https://twitter.com/TaliaRinger/status/1475897510342594560

[tlringer]

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

https://twitter.com/PTOOP/status/1475920399749763083

[tlringer]

https://cubical.1lab.dev/wip.maximal-set.html

[JasonGross]

we need UIP to hold locally on the elements in the range of the function in the return datatype

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 fold f init data you need UIP for the base case(s) (i.e., forall p q : init = init, p = q), and you need that ap (uncurry f) is a retraction, i.e., forall x, exists (g : uncurried_f x = uncurried_f x -> x = x), forall (p : uncurried_f x = uncurried_f x), f_equal uncurried_f (g p) = p (or maybe you want the more concise forall x, IsEquiv (@f_equal _ _ uncurried_f x x)).