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: Apr 19 2024 at 20:01 UTC