Defining functions on non-inductive types using LEM in Coq

Question

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.

Answer 1

I’m not sure I get what you are trying to do – or, rather, how your example corresponds to your goal. Indeed, in your code you postulate those three types a, b and c, but these are not really "arbitrary terms", rather they are types (this is just what you have postulated!). If you wanted to work with unspecified carriers, what you could do instead would be to postulate two types and then elements of those types, something like

Variables (A B : Type) (a : A) (b b' : B).

Then you can define the function you wish, something like

Definition fn (x : A) : B :=
  match (em (x = a)) with
    | left _ => b
    | right _ => b'
  end.

But indeed it will not compute as it is stuck on your use of the axiom. This is why the law of excluded middle is used with care in Coq, as it breaks computation.

As for the need for this excluded middle, if your carrier types are completely abstract, indeed you cannot do much with them – but this is similar to math: if I give you two sets without any other info, it would be quite difficult for you to define any map between them. However, usually when we try to define functions, we know some things on the carrier sets, and then we can use that to define them! For instance, if you know that there is some e in B, because it’s a group so it has a unit, then you can define the trivial group isomorphism from A to B (the constant function to e). Of course the more things you know about your types A and B, the more interesting maps you can define.

As for HoTT/Unimath, in the context of group theory they might interest you because they give you a good notion of quotients – something vanilla Coq lacks. But if you are unfamiliar with higher mathematics, I would advise against going this way at first, as there is a non-negligible price to pay before you can get the best out of it.