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.
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.
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.
This would contradict some strong equality principles such as univalence so it will not be provable.
I see. Thank you both.
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?
In general you cannot inspect types so inverting equalities about them is not going to work.
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 a b = prod c d you can deduce
a = c and
b = d.
But this is somehow stronger than only having
decode (prod a b) = decode (prod c d) which corresponds roughly to your original goal.
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!
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