Module DecidableTypeEquality

Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.

-------------------------------------------------------------------------

In general, an equality between two tensors cannot be decomposed. It can, however, be decomposed if these tensors are inert. We prove this fact for approximate equality first, then transport it to equality.

Lemma tyapproxeq_decompose_inert_tensor_1:
  forall T1,
  inert T1 ->
  forall T2,
  inert T2 ->
  forall k U1 U2,
  tyapproxeq (S k) (TyTensor T1 U1) (TyTensor T2 U2) ->
  tyapproxeq (S k) T1 T2.

Proof.

  induction 1; introv i1 i2; dependent destruction i1; dependent destruction i2;
  try solve [ false; eauto using tyred_inert ];
  eassumption.
Qed.

Lemma tyapproxeq_decompose_inert_tensor_2:
  forall T1,
  inert T1 ->
  forall T2,
  inert T2 ->
  forall k U1 U2,
  tyapproxeq (S k) (TyTensor T1 U1) (TyTensor T2 U2) ->
  tyapproxeq k U1 U2.

Proof.

  induction 1; introv i1 i2; dependent destruction i1; dependent destruction i2;
  try solve [ false; eauto using tyred_inert ];
  eassumption.
Qed.

Lemma tyeq_decompose_inert_tensor_1:
  forall T1 T2 U1 U2,
  inert T1 ->
  inert T2 ->
  tyeq (TyTensor T1 U1) (TyTensor T2 U2) ->
  tyeq T1 T2.

Proof.

  introv i1 i2 h. intro k.
  tyapproxeqrr_increment.
  eauto using tyapproxeq_decompose_inert_tensor_1.
Qed.

Lemma tyeq_decompose_inert_tensor_2:
  forall T1 T2 U1 U2,
  inert T1 ->
  inert T2 ->
  tyeq (TyTensor T1 U1) (TyTensor T2 U2) ->
  tyeq U1 U2.

Proof.

introv i1 i2 h. intro k.
eapply (tyapproxeq_decompose_inert_tensor_2 i1 i2). eauto.
Qed.