I'm trying to prove statements about homomorphisms in Coq. Specifically, about in which cases the existence of some set of homomorphisms implies the existence of a specific other homomorphism. I'm aware that most functions are defined by applying a match
statement to a term of an inductive type. However, many algebraic objects (such as any group) don't seem to have an inductive definition as there are often multiple ways to construct a given element (e.g. in a group the constructor trees 0
and 0 + 0
need to be equal, which is not allowed).
In my attempt to define a function between the carrier sets of groups, I came up with the following pattern to define a function mapping arbitrary terms a
to a
and b
to c
:
Axiom em : forall p : Prop, {p} + {~ p}.
Section LEMExample.
Variable a : Type.
Variable b : Type.
Variable c : Type.
Variable distinct : b = a -> False.
(* Define the function using LEM *)
Theorem fn : Type -> Type.
Proof.
intros x.
destruct (em (x = a)).
- exact a.
- exact c.
Defined.
(* Can't directly compute the function *)
Compute fn. (* fun x : Type => if em (x = a) then a else c *)
Compute (fn a). (* if em (a = a) then a else c *)
Compute (fn b). (* if em (b = a) then a else c *)
(* But can prove the value of its output *)
Theorem fnValueA : fn a = a.
Proof using Type.
- unfold fn.
destruct (em (a = a)) as [H | H].
+ exact H.
+ contradiction (H (eq_refl a)).
Qed.
Theorem fnValueB : fn b = c.
Proof using distinct.
- unfold fn.
destruct (em (b = a)) as [H | H].
+ contradiction (distinct H).
+ exact (eq_refl c).
Qed.
End LEMExample.
From a logical standpoint I'm fine with accepting the law of excluded middle. It appears that I can also prove the value of the function on a
and b
, which means I should be able to manually rewrite applications of the function.
Is there some hidden opacity that I will run into with defining functions in this way? I can't destruct them, which seems like a problem, but destructing functions doesn't usually seem to provide much information in Coq anyway. I'd think a better approach to my problem might involve handling sub-objects rather than raw functions via the fundamental theorem on homomorphisms, but there's some theory I haven't worked through yet so I'm not sure if that's a strong enough representation.
Additionally, is there a cleaner way to get the same effect of defining a function on a non-inductive type? I almost feel like I'm missing something elementary, but the function documentation I've looked through so far seems entirely centered on inductive types.
Also, if this is something that would be easier in UniMath/HoTT (since it deals with abusing identity types) I'd be interested in hearing about that.