The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Beware that proof_irrelevance is an axiom

On Sat, Oct 10, 2020, 12:21 Larry Lee <llee454 AT gmail.com> wrote:

Sorry for the cruft in the last snippet:

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   exact (eq_sym (rew_map P f (section a) (f0 (g (f a))))).
 24 Qed.

On 10/10/20, Larry Lee <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> 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> 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> 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
>>> > >
>>> > >
>>> > >
>>>
>>
>