/prog/ - [coq] sigma inversion

Name: Anonymous 2017-01-27 0:04

Hey, how can I prove:

X : Set
Y : X -> Set
x: X
y, z: Y x
H: existT _ x y = existT _ x z
========================
y = z

why does inversion not give me y=z? Is there some reason why it is not true?

Name: Anonymous 2017-01-27 0:12

I was learning Coq, but then I realized it sounds like cock and would put me in awkward situations. What were they thinking with that name...?

My other option now is Isabelle, but I know nothing about it.

Name: Anonymous 2017-01-27 0:21

you cant because type theory is bullshit
you need an axiom called uniqueness of identity proofs
but the CIA nigger haskell gang decided to steer the entire type theory community down a wild goose chase of homotopy type theory, making their entire ethos about not being able to prove basic true equalities like this
rip coq, had so much potential before homos took over

Name: Anonymous 2017-01-27 0:28

>>2
Criton, nous devons un coq à Esculape. Payez cette dette, ne soyez pas négligents.

Name: Anonymous 2017-01-27 0:52

>>2
Wait, I got it.
https://coq.inria.fr/faq#htoc4

2 Did you really need to name it like that?

Some French computer scientists have a tradition of naming their software as animal species: Caml, Elan, Foc or Phox are examples of this tacit convention. In French, “coq” means rooster, and it sounds like the initials of the Calculus of Constructions CoC on which it is based.

Name: Anonymous 2017-01-27 0:57

>>3
ok, let's assume I have decidable eq for Y x (thus UIP for Y x), how would I proceed?

Name: Anonymous 2017-01-27 1:49

>>6
i think you can find example of this in the standard library

Name: Anonymous 2017-01-27 14:26

>>7
I could not, unfortunately.

Since "inversion H." just re-adds the same hypothesis, I'm inclined to believe that there's a reason why y = z is not true, I just can't imagine what that reason could be.

Name: Anonymous 2017-01-27 17:36

https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html

Name: Anonymous 2017-01-27 18:16

that's for getting UIP from dec, but how would I apply UIP to prove the original question?

Name: Anonymous 2017-01-27 23:50

https://coq.inria.fr/library/Coq.Logic.EqdepFacts.html

Name: Anonymous 2017-01-28 0:57

>>11
If I am not mistaken, the axiom required to prove inj_pair2 is this:

[code]Axiom eq_rect_eq :
forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
x = eq_rect p Q x p h.[code]

which I tried, and failed to prove (allowing for decidable equality on U and Q p). The other direction is already part of the library as EqdepTheory.UIP.

Any further pointers would be much appreciated!

Name: Anonymous 2017-01-28 6:57

https://coq.inria.fr/faq?som=5#htoc47

Name: Anonymous 2017-01-28 12:42

>>13
That looks promising, thanks!

Name: Anonymous 2017-01-28 17:07

>>13
Yes, that's what I was looking for, thanks.

Name: Anonymous 2017-01-28 18:13

>>13
virus dont click!!!!!!!!!!!!!!

Name: Anonymous 2017-01-29 17:16

https://sympa.inria.fr/sympa/arc/coq-club/2016-05/msg00158.html

This was discussed a few months ago on coq-club.

Name: Anonymous 2017-02-01 1:45

Just reading this made my head hurt

[coq] sigma inversion

1 Name: Anonymous 2017-01-27 0:04

2 Name: Anonymous 2017-01-27 0:12

3 Name: Anonymous 2017-01-27 0:21

4 Name: Anonymous 2017-01-27 0:28

5 Name: Anonymous 2017-01-27 0:52

6 Name: Anonymous 2017-01-27 0:57

7 Name: Anonymous 2017-01-27 1:49

8 Name: Anonymous 2017-01-27 14:26

9 Name: Anonymous 2017-01-27 17:36

10 Name: Anonymous 2017-01-27 18:16

11 Name: Anonymous 2017-01-27 23:50

12 Name: Anonymous 2017-01-28 0:57

13 Name: Anonymous 2017-01-28 6:57

14 Name: Anonymous 2017-01-28 12:42

15 Name: Anonymous 2017-01-28 17:07

16 Name: Anonymous 2017-01-28 18:13

17 Name: Anonymous 2017-01-29 17:16

18 Name: Anonymous 2017-02-01 1:45