# Library Exercise_4_2_3_12

Require Import Utf8 ZArith.
Require Import Common Notations Groupoid CategoryIsomorphisms.

Set Implicit Arguments.

Generalizable All Variables.

Local Notation := Z.

Local Open Scope Z_scope.

# Exercise 4.2.3.12

## Problem

Consider the set A of all (well-formed) arithmetic expressions in the symbols {0, ..., 9, +, -, *, (, )}. For example, here are some elements of A:
[52, 52 - 7, 50 + 3 × (6 - 2).]
We can say that an equivalence between two arithmetic expressions is a justification that they give the same "final answer", e.g. 52 + 60 is equivalent to 10 × (5 + 6) + (2 + ), which is equivalent to 10 × 11 + 2. I’ve basically described a groupoid. What are its objects and what are its morphisms?
Lemma eq_trans_id : T x y (pf : @eq T x y),
eq_trans (eq_sym pf) pf = eq_refl.
compute.
intros.
destruct pf.
reflexivity.
Qed.
Inductive Expression :=
| Constant : Expression
| Pos : ExpressionExpression
| Negate : ExpressionExpression
| Subtract : ExpressionExpressionExpression
| Multiply : ExpressionExpressionExpression.
Fixpoint DenoteExpression (e : Expression) : :=
match e with
| Constant zz
| Pos zDenoteExpression z
| Negate z-DenoteExpression z
| Add a b(DenoteExpression a) + (DenoteExpression b)
| Subtract a b(DenoteExpression a) - (DenoteExpression b)
| Multiply a b(DenoteExpression a) × (DenoteExpression b)
end.
Definition ArithmeticCategory : @Category Expression.
refine {| Morphism := (fun x y DenoteExpression x = DenoteExpression y);
Identity := (fun x eq_refl);
Compose := (fun _ _ _ p q eq_trans q p) |};
repeat intro;