1
$\begingroup$

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.

$\endgroup$
3
  • 1
    $\begingroup$ I suspect the aproach you are taking is not the best one for the problem that you are really trying to solve. Please explain a concrete example of what you're trying to accomplish. Where precisely in group theory do you feel the need to define a function by distinguishing cases? The pattern you've come up with makes sense if you're a classically trained mathematician who is doing this on a whiteboard, but for Coq there will be a much better way. We just have to find out what it is you're actually doing. $\endgroup$ Jan 25 at 11:47
  • 1
    $\begingroup$ For instance, can you suggest a concrete theorem that you would like to prove, and in whose proof you encounter the problem you're trying to solve? $\endgroup$ Jan 25 at 11:50
  • 1
    $\begingroup$ A site dedicated to Proof Assistants will be created soon. If you want an invitation to the Private Beta when it is launched, then click here, then "sign up" and it should automatically link to your Stack Exchange account. I hope to see you there! $\endgroup$ Jan 26 at 5:35

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ The example is a way of stating the existence of a non-trivial function on a non-inductive domain (which is Type in my example, but could be A as in yours) which seemingly isn't possible in a meaningful way without LEM. This proof of existence of a function is one half of the most direct way to prove a homomorphism, The crux of the question is whether defining a function in this way will cause difficulties down the road when trying to supply the second half, proving properties about the function, such as whether it preserves operations. $\endgroup$
    – Ene
    Jan 21 at 17:02
  • $\begingroup$ While it's clear that having proofs of some statements about the domain is one way of defining functions, I suppose there's also an implicit question (implied by the statement that I'm proving that the existence of one homomorphism implies the existence of another) about whether this goes the other way: can information about a mostly unknown domain be inferred from the existence of a hypothesized function on that domain, such that the information can then be used to define a new function? I'd think this would require case analysis on function types, which seems to not be informative. $\endgroup$
    – Ene
    Jan 21 at 17:10
  • $\begingroup$ I think the discussion is too vague to give an affirmative answer. What I can only say is that practice seems to suggest you don’t need the LEM to define interesting functions: the Mathematical Components library for instance develops a lot of advanced group theory without ever needing it, for instance. But maybe the use cases you have in mind are different. What is sure is that if you’ve used the LEM to define a function, you should not hope it to compute too well. This might prove annoying because you will have to do more equational reasoning, but it should not be completely intractable. $\endgroup$ Jan 28 at 10:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.