The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

I don't think so. This has to do with the parametrization of Iris with 
higher-order user-defined resources.

I feel that this is getting off-topic, so if you want to know more, 
please ask me in private.

On 10/10/2020 22.55, Bas Spitters wrote:
> Robbert, is that related to the issues with later-s and equality, as
> we have addressed in guarded cubical type theory?
> https://arxiv.org/abs/1611.09263
>
> On Sat, Oct 10, 2020 at 10:38 PM Robbert Krebbers
> <mailinglists AT robbertkrebbers.nl> wrote:
> > Test subject volunteers.
> >
> > Also Iris got infected with homotopy type theory lately :) We're
> > transporting equalities over our resource algebras.
> >
> > See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/530#note_57508
> >
> > On 10/10/2020 19.36, Xavier Leroy wrote:
> > > At any rate, Talia's message gave me an idea for a paper:
> > >
> > > " Q.e.d. or starve?  On the feeding habits of homotopy type theorists"
> > >
> > > I still need a few more test subjects, though :-)
> > >
> > > - Xavier
> > >
> > > On Sat, Oct 10, 2020 at 7:24 PM Derek Dreyer <dreyer AT mpi-sws.org
> > > <mailto:dreyer AT mpi-sws.org>> wrote:
> > >
> > >      FYI: I don't think Talia was complaining: nerd sniping is fun.  I
> > >      sometimes nerd-snipe myself.
> > >
> > >      https://www.urbandictionary.com/define.php?term=Nerd%20Sniping
> > >
> > >
> > >      Derek
> > >
> > >      On Sat, Oct 10, 2020 at 7:19 PM Larry Lee <llee454 AT gmail.com
> > >      <mailto:llee454 AT gmail.com>> wrote:
> > >       >
> > >       > Hey Talia,
> > >       >
> > >       > Sorry to hear that you were "nerd sniped" over this. It's possible to
> > >       > prove the lemma you presented below:
> > >       >
> > >       > 1   Require Import ProofIrrelevance.
> > >       >   1 Require Import FunctionalExtensionality.
> > >       >   2
> > >       >   3 Parameter A : Type.
> > >       >   4 Parameter B : Type.
> > >       >   5 Parameter f : A -> B.
> > >       >   6 Parameter g : B -> A.
> > >       >   7 Axiom section : forall a, g (f a) = a.
> > >       >   8 Axiom retraction : forall b, f (g b) = b.
> > >       >   9
> > >       >  10 Goal
> > >       >  11   forall (P : B -> Type) (a : A) (f0 : forall a : A, P (f a)),
> > >       >  12   eq_rect
> > >       >  13     (f (g (f a)))
> > >       >  14     P
> > >       >  15     (f0 (g (f a)))
> > >       >  16     (f a)
> > >       >  17     (retraction (f a)) =
> > >       >  18   f0 a.
> > >       >  19 Proof.
> > >       >  20   intros P a f0.
> > >       >  21   rewrite <- (f_equal_dep (fun a => P (f a)) f0 (section a)).
> > >       >  22   rewrite (proof_irrelevance (f (g (f a)) = (f a)) (retraction (f
> > >       > a)) (f_equal f (section a))).
> > >       >  23   set (b := f a).
> > >       >  24   set (a0 := g b).
> > >       >  25   set (b0 := f a0).
> > >       >  26   assert (a0 = a).
> > >       >  27   + exact (section a).
> > >       >  28   + assert (b0 = b).
> > >       >  29     - exact (retraction b).
> > >       >  30     - exact (eq_sym (rew_map P f (section a) (f0 a0))).
> > >       >  31 Qed.
> > >       >
> > >       > I don't drink, but a pizza would be nice.
> > >       >
> > >       > - Larry Lee
> > >       > (http://larrylee.tech)
> > >       >
> > >       > On 10/10/20, Talia Ringer <tringer AT cs.washington.edu
> > >      <mailto:tringer AT cs.washington.edu>> wrote:
> > >       > > Thanks all, love the thought processes too, and happy to ship
> > >      some beer or
> > >       > > dessert or get it next conference :)
> > >       > >
> > >       > > On Sat, Oct 10, 2020, 7:53 AM Jason Gross
> > >      <jasongross9 AT gmail.com <mailto:jasongross9 AT gmail.com>> wrote:
> > >       > >
> > >       > >> I have not yet looked at Gaëtan's proof, but here is the
> > >      intuition:
> > >       > >> What you have is a sort of incoherent equivalence.  What would
> > >      make
> > >       > >> your proof easier is having some version of [section] such that
> > >       > >> [forall a, f_equal f (section a) = retraction (f a)], so that
> > >      you were
> > >       > >> dealing with a coherent equivalence instead.  Since your proof
> > >      goal
> > >       > >> only uses [retraction], it should be possible to "adjust"
> > >      [section] so
> > >       > >> that it satisfies this equation; I suspect that this is what
> > >      most of
> > >       > >> Gaëtan's proof is about.  Once you have this additional lemma,
> > >      your
> > >       > >> goal is quite straight forward: supposing you have this lemma
> > >      as [H],
> > >       > >> you can solve your goal with [rewrite <- H; generalize
> > >      (section a);
> > >       > >> generalize (g (f a)); intros; subst; reflexivity.]
> > >       > >>
> > >       > >> The underlying intuition that I had here is that the thing
> > >      getting in
> > >       > >> the way of the "naive proof" is that you can't just destruct an
> > >       > >> equality [e] of type [f a0 = f a], because you can't
> > >      generalize over
> > >       > >> the two sides.  But since f is an equivalence, HoTT tells us
> > >      that we
> > >       > >> can get that [e = ap f <something>] (i.e., [e = f_equal f
> > >       > >> <something>], where <something> is going to be [ap g e]
> > >      adjusted so
> > >       > >> the endpoints line up.  Once you get this, you can just
> > >      destruct the
> > >       > >> <something>, and you're golden.
> > >       > >>
> > >       > >> (Note that if your goal also mentioned [section], then you'd
> > >      almost
> > >       > >> surely be sunk without having an extra hypothesis which related
> > >       > >> [section] and [retraction].)
> > >       > >>
> > >       > >> On Sat, Oct 10, 2020 at 4:00 AM Gaëtan Gilbert
> > >       > >> <gaetan.gilbert AT skyskimmer.net
> > >      <mailto:gaetan.gilbert AT skyskimmer.net>> wrote:
> > >       > >> >
> > >       > >> > It's proved. HoTT is the only place I know to get lemmas
> > >      about equality
> > >       > >> from so that's what I used, but this is axiom less so can be
> > >      done without
> > >       > >> HoTT too.
> > >       > >> >
> > >       > >> > Thought process:
> > >       > >> > - eq_rect is complicated, let's turn it into transport to
> > >      simplify the
> > >       > >> goal
> > >       > >> >    this worked but is not actually useful in the end
> > >       > >> > - maybe there's a fancy destruct which will work (simple
> > >      proofs about
> > >       > >> equality are all about the well chosen destruct)
> > >       > >> >    this went nowhere fast
> > >       > >> > - maybe I can construct a counterexample using univalence on
> > >      boolean
> > >       > >> negation
> > >       > >> >    obviously this couldn't work
> > >       > >> > - this looks like the incomplete IsEquiv from HoTT where we can
> > >       > >> construct some fancy equality proofs to get the full IsEquiv stuff
> > >       > >> >    let's look at the construction to see if I get any ideas
> > >       > >> >    a bit of messing about then leads to the solution
> > >       > >> >
> > >       > >> > Gaëtan Gilbert
> > >       > >> >
> > >       > >> > On 10/10/2020 08:11, Talia Ringer wrote:
> > >       > >> > > Hello friends,
> > >       > >> > >
> > >       > >> > > I got nerd sniped this morning on a proof task I've been
> > >      at for like
> > >       > >> 11 hours. Most of the proof obligations are done now, but I
> > >      ended up
> > >       > >> stuck
> > >       > >> at one particular proof obligation that I'm not sure how to
> > >      solve, or if
> > >       > >> it
> > >       > >> is solvable in general. But also I need to work on job
> > >      applications and
> > >       > >> normal last year of grad school things, and I haven't eaten
> > >      dinner. So if
> > >       > >> you help me out with this one proof obligation, I'll give you
> > >      appropriate
> > >       > >> credit and also get you a beer or dessert.
> > >       > >> > >
> > >       > >> > > For real. I don't have technical mentors or local expertise to
> > >       > >> > > consult.
> > >       > >> > >
> > >       > >> > > Essentially, I have two types:
> > >       > >> > >
> > >       > >> > >     A : Type
> > >       > >> > >
> > >       > >> > >     B : Type
> > >       > >> > >
> > >       > >> > > that are equivalent:
> > >       > >> > >
> > >       > >> > >     f : A -> B
> > >       > >> > >
> > >       > >> > >     g : B -> A
> > >       > >> > >     section : forall a, g (f a) = a.
> > >       > >> > >     retraction : forall b, f (g b) = b.
> > >       > >> > >
> > >       > >> > >
> > >       > >> > > I know literally nothing else about my types or my
> > >      equivalence. *I
> > >       > >> want to know if it is possible to solve this proof obligation:*
> > >       > >> > >
> > >       > >> > >     *P : B -> Type
> > >       > >> > >     a : A
> > >       > >> > >     f0 : forall a : A, P (f a)
> > >       > >> > >     ______________________________________(1/1)
> > >       > >> > >     eq_rect (f (g (f a))) P (f0 (g (f a))) (f a)
> > >      (retraction (f a)) =
> > >       > >> f0 a*
> > >       > >> > >
> > >       > >> > >
> > >       > >> > > (I have already solved this proof obligation:
> > >       > >> > >
> > >       > >> > >     a : A
> > >       > >> > >     ______________________________________(1/1)
> > >       > >> > >     eq_rect (f (g (f a))) (fun _ : B => A) (g (f a)) (f a)
> > >       > >> > > (retraction
> > >       > >> (f a)) = a
> > >       > >> > >
> > >       > >> > > Literally just "rewrite retraction. apply section." works.
> > >      But that
> > >       > >> didn't help me, and I also couldn't get Coq to use the same
> > >      tactics.)
> > >       > >> > >
> > >       > >> > > I can't figure out whether this is me being really bad at
> > >      equalities
> > >       > >> of equalities and dependent rewrites, or whether there is
> > >      something we
> > >       > >> must
> > >       > >> know about A, B, or our equivalence for this to hold, or
> > >      whether there is
> > >       > >> an additional axiom we must assume for this to hold in
> > >      general. And it's
> > >       > >> 11:00 PM and I haven't eaten dinner, so time to ask you all:
> > >       > >> > >
> > >       > >> > >   * Is this provable? If so, how? (And why am I so bad at
> > >      equalities
> > >       > >> of equalities?)
> > >       > >> > >   * If it is not, can you explain why?
> > >       > >> > >   * Is there anything I could assume about A and B to make it
> > >       > >> > > provable?
> > >       > >> > >   * Is there anything I could assume about f, g, section, or
> > >       > >> retraction to make it provable?
> > >       > >> > >
> > >       > >> > > Hopefully someone else finds this fun, too. Or really
> > >      likes beer.
> > >       > >> > >
> > >       > >> > > Talia
> > >       > >> > >
> > >       > >> > >
> > >       > >> > >
> > >       > >>
> > >       > >