(* week-10_formalizing-two-by-two-matrices.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 28 Mar 2025 *)

(* ********** *)

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

Require Import Arith.

(* ********** *)

Inductive m22 : Type := M22 : nat -> nat -> nat -> nat -> m22.

Property componential_equality_m22 :
  forall x11 x12 x21 x22 y11 y12 y21 y22 : nat,
    M22 x11 x12
        x21 x22 =
    M22 y11 y12
        y21 y22
    <->
    x11 = y11 /\ x12 = y12 /\ x21 = y21 /\ x22 = y22.
Proof.
  intros x11 x12
         x21 x22.
  intros y11 y12
         y21 y22.
  split.

  - intro H_tmp.
    injection H_tmp as H11 H12 H21 H22.
    rewrite -> H11.
    rewrite -> H12.
    rewrite -> H21.
    rewrite -> H22.
    split; [reflexivity | split; [reflexivity | split; [reflexivity | reflexivity]]].

  - intros [H11 [H12 [H21 H22]]].
    rewrite -> H11.
    rewrite -> H12.
    rewrite -> H21.
    rewrite -> H22.
    reflexivity.
Qed.

(* ***** *)

Definition zero_m22 := M22 0 0
                           0 0.

Definition add_m22 (x y : m22) : m22 :=
  match (x, y) with
    (M22 x11 x12
         x21 x22,
     M22 y11 y12
         y21 y22) =>
    M22 (x11 + y11) (x12 + y12)
        (x21 + y21) (x22 + y22)
  end.

Lemma add_m22_assoc :
  forall x y z : m22,
    add_m22 x (add_m22 y z) =
    add_m22 (add_m22 x y) z.
Proof.
  intros [x11 x12
          x21 x22]
         [y11 y12
          y21 y22]
         [z11 z12
          z21 z22].
  unfold add_m22.
  rewrite ->4 Nat.add_assoc.
  reflexivity.
Qed.

Lemma add_m22_0_l :
  forall x : m22,
    add_m22 zero_m22 x = 
    x.
Proof.
  intros [x11 x12
          x21 x22].
  unfold add_m22, zero_m22.
  rewrite ->4 Nat.add_0_l.
  reflexivity.
Qed.

Lemma add_m22_0_r :
  forall x : m22,
    add_m22 x zero_m22 =
    x.
Proof.
  intros [x11 x12
          x21 x22].
  unfold add_m22, zero_m22.
  rewrite ->4 Nat.add_0_r.
  reflexivity.
Qed.

(* ********** *)

Inductive mm22 : Type := MM22 : m22 -> m22 -> m22 -> m22 -> mm22.

(* ********** *)

(* week-10_formalizing-two-by-two-matrices.v *)