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
  | Add : ExpressionExpressionExpression
  | 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;
    destruct_head_hnf @eq;
    reflexivity.
  Defined.
  Definition ArithmeticGroupoid : Groupoid.
    refine {| GroupoidCategory := ArithmeticCategory |}.
    constructor.
    intros s d m.
     (eq_sym m);
      simpl in *;
      destruct_head_hnf @eq;
      reflexivity.
  Defined.
End Exercise_4_2_3_12.