## Stream: Coq users

### Topic: decompose type pairs

#### Yu Zhang (Jan 18 2022 at 13:42):

I'm stuck with proving the following

``````  Goal forall a b c d, (a * b)%type = (c * d)%type -> a = c /\ b = d.
intros * H.
``````

I tried `destruct H` or `inversion H` but neither works. So I am skeptical about whether this can be proved or not. I'd appreciate if anyone can give suggestions about which tactic can be used here or how to re-formulate it to make it provable.

#### Meven Lennon-Bertrand (Jan 18 2022 at 13:46):

What you are trying to prove corresponds to the injectivity of the `*` type constructor, which is not derivable in CIC. Indeed there are models where this is not true, for instance in homotopy type theory.

#### Théo Winterhalter (Jan 18 2022 at 13:47):

This would contradict some strong equality principles such as univalence so it will not be provable.

#### Yu Zhang (Jan 18 2022 at 13:48):

I see. Thank you both.

#### Meven Lennon-Bertrand (Jan 18 2022 at 13:48):

There are usually ways to go around these unprovable things, but it depends widely upon what you want to do with it. What is your context?

#### Théo Winterhalter (Jan 18 2022 at 13:48):

In general you cannot inspect types so inverting equalities about them is not going to work.

#### Meven Lennon-Bertrand (Jan 18 2022 at 13:50):

But a typical solution might be to replace types with codes, eg. have an inductive

``````Inductive code : Type :=
| prod : code -> code -> code
…
``````

and a function `decode : code -> Type` mapping `prod co1 co1` to `(decode co1) * (decode co2)`, so that you can use injectivity of the `prod` constructor.

#### Meven Lennon-Bertrand (Jan 18 2022 at 13:52):

Here, having `prod a b = prod c d` you can deduce `a = c` and `b = d`.

#### Meven Lennon-Bertrand (Jan 18 2022 at 13:53):

But this is somehow stronger than only having `decode (prod a b) = decode (prod c d)` which corresponds roughly to your original goal.

#### Yu Zhang (Jan 18 2022 at 14:02):

I'm trying to define the product on type constructors

``````Inductive tycon_prod (E F: Type -> Type): Type -> Type :=
| tycon_prod_intro s t :
E s -> F t -> tycon_prod E F (s * t)%type.
``````

So sometimes I got type level equalities like in my original question. Let me try to replace (s * t) with what you suggested. Thank you so much!

#### Paolo Giarrusso (Jan 18 2022 at 15:21):

Fwiw if you just need a product it's enough to do `Definition hprod (E F : Type -> Type) (T : Type) : Type := E T * F T.`, but codes make sense for metaprogramming tasks

Last updated: Oct 03 2023 at 19:01 UTC