ImpAlg.Theorems

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Export ImpAlg.Lattices.
Require Export ImpAlg.ImplicativeAlgebras.
Require Export ImpAlg.ParAlgebras.
Require Export ImpAlg.TensorAlgebras.

Zoology

This file is only there to sum up the connections we have established between the different notions of structures and algebras. Since

Theorem ParStructure_is_ImplicativeStructure `{CL:CompleteLattice}:
  ParStructure → (@ImplicativeStructure _ _ _ CL ).
Proof.
intros; apply PS_IS.
Qed.

Theorem ParAlgebra_is_ImpAlgebra `{PS:ParStructure}:
  ParAlgebra → (@ImplicativeAlgebra _ _ _ _ IS ).
Proof.
intros; apply PA_IA.
Qed.

Theorem Rev_ParStructure_is_TensorStructure `{CL:CompleteLattice}:
  ParStructure → (@TensorStructure _ _ _ RevCompleteLattice ).
Proof.
intros; apply PS_TS.
Qed.

Theorem Rev_ParAlgebra_is_TensorAlgebra `{PS:ParStructure}:
  ParAlgebra → (@TensorAlgebra _ _ _ _ TS ).
Proof.
intros; apply PA_TA.
Qed.

Theorem Rev_TensorStructure_is_ParStructure `{CL:CompleteLattice}:
  TensorStructure → (@ParStructure _ _ _ RevCompleteLattice ).
Proof.
intros; apply TS_PS.
Qed.

This is the main connection we are missing:
Theorem Rev_TensorAlgebra_is_ParAlgebra `{TS:TensorStructure}: TensorAlgebra → (@ParAlgebra _ PS ).
As for the the implication:
ImplicativeStructure → ParStructure
we should retrict to the ParStructure to the case where a⅋b is defined by a+b, and fromalize a counter-example. This might represent a lot of work...