Stream: Coq users

Topic: decompose type pairs


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yu Zhang (Jan 18 2022 at 13:48):

I see. Thank you both.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC