The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

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