Require Export Setoid Morphisms.
From mathcomp Require Import all_ssreflect.
Require Import edone preliminaries.
Require Export structures pttdom.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".

2p algebras, tests, initial algebra of terms

2p algebras (2pdom algebras with top)

(* 2p axioms *)
Structure ptt :=
  { ops:> ops_;
    dot_eqv_: Proper (eqv ==> eqv ==> eqv) (@dot ops);
    par_eqv_: Proper (eqv ==> eqv ==> eqv) (@par ops);
    cnv_eqv_: Proper (eqv ==> eqv) (@cnv ops);
    domE: forall x: ops, dom x 1 x·top;
    parA_: forall x y z: ops, x (y z) (x y) z;
    parC_: forall x y: ops, x y y x;
    dotA_: forall x y z: ops, x · (y · z) (x · y) · z;
    dotx1_: forall x: ops, x · 1 x;
    cnvI_: forall x: ops, x°° x;
    cnvpar_: forall x y: ops, (x y x° y°;
    cnvdot_: forall x y: ops, (x · y y° · x°;
    par11_: 1 1 @one ops;
    A10_: forall x y: ops, 1 x·y dom (x y°);
    A11: forall x: ops, x · top dom x · top;
    A12: forall x y: ops, (x1) · y (x1top y

basic derivable laws

Section derived.
 Variable X: ptt.
 Existing Instances dot_eqv_ par_eqv_ cnv_eqv_.

 Instance dom_eqv_: Proper (eqv ==> eqv) (@dom X).
 Proof. intros ?? H. by rewrite 2!domE H. Qed.

 Lemma A13_ (x y: X): dom(x·y) dom(x·dom y).
 Proof. by rewrite domE -dotA_ A11 dotA_ -domE. Qed.

 Lemma A14_ (x y z: X): dom x·(yz) dom x·y z.
 Proof. by rewrite domE parC_ A12 (A12 _ y) parA_. Qed.

 Canonical Structure pttdom_of: pttdom :=
    (@dot_eqv_ X)
    (@par_eqv_ X)
    (@cnv_eqv_ X)
    (@parA_ X)
    (@parC_ X)
    (@dotA_ X)
    (@dotx1_ X)
    (@cnvI_ X)
    (@cnvpar_ X)
    (@cnvdot_ X)
    (@par11_ X)
    (@A10_ X)

 Lemma parxtop (x: X): x top x.
   symmetry. generalize (A12 1 x).
   by rewrite par11 2!dot1x parC.

 Lemma partopx (x: X): top x x.
 Proof. by rewrite parC parxtop. Qed.

 Lemma cnvtop: top° @top X.
  rewrite -(parxtop top°) -{2}(cnvI top).
  by rewrite -cnvpar partopx cnvI.

End derived.

Section terms.
 Variable A: Type.
 Inductive term :=
 | tm_dot: term -> term -> term
 | tm_par: term -> term -> term
 | tm_cnv: term -> term
 | tm_dom: term -> term
 | tm_one: term
 | tm_top: term
 | tm_var: A -> term.
 Section e.
 Variable (X: ops_) (f: A -> X).
 Fixpoint eval (u: term): X :=
   match u with
   | tm_dot u v => eval u · eval v
   | tm_par u v => eval u eval v
   | tm_cnv u => (eval u) °
   | tm_dom u => dom (eval u)
   | tm_one => 1
   | tm_top => top
   | tm_var a => f a
 End e.
 Definition tm_eqv (u v: term): Prop :=
   forall (X: ptt) (f: A -> X), eval f u eval f v.
 Hint Unfold tm_eqv : core.
 Lemma tm_eqv_equivalence: Equivalence tm_eqv.
     now intro.
     intros ?? H X f. specialize (H X f). by symmetry.
     intros ??? H H' X f. specialize (H X f). specialize (H' X f). etransitivity. apply H. apply H'.
 Canonical Structure tm_setoid := Setoid tm_eqv_equivalence.
 Canonical Structure tm_ops_ :=
   {| setoid_of_ops := tm_setoid;
      dot := tm_dot;
      par := tm_par;
      cnv := tm_cnv;
      dom := tm_dom;
      one := tm_one;
      top := tm_top |}.

 (* quotiented terms indeed form a 2pdom algebra *)
 Definition tm_ptt: ptt.
  refine (@Build_ptt tm_ops_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
    abstract (repeat intro; simpl; by apply dot_eqv_).
    abstract (repeat intro; simpl; by apply par_eqv_).
    abstract (repeat intro; simpl; by apply cnv_eqv_).
    abstract (repeat intro; simpl; by apply domE).
    abstract (repeat intro; simpl; by apply parA_).
    abstract (repeat intro; simpl; by apply parC_).
    abstract (repeat intro; simpl; by apply dotA_).
    abstract (repeat intro; simpl; by apply dotx1_).
    abstract (repeat intro; simpl; by apply cnvI_).
    abstract (repeat intro; simpl; by apply cnvpar_).
    abstract (repeat intro; simpl; by apply cnvdot_).
    abstract (repeat intro; simpl; by apply par11_).
    abstract (repeat intro; simpl; by apply A10_).
    abstract (repeat intro; simpl; by apply A11).
    abstract (repeat intro; simpl; by apply A12).
 (* Canonical tm_ptt.  *)

End terms.
Bind Scope ptt_ops with term.