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.
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
constructor.
Here, having 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: Oct 03 2023 at 19:01 UTC