Module Qcert.NRA.Typing.TNRAEq

Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import List.
Require Import String.
Require Import DataSystem.
Require Import NRA.
Require Import NRAEq.
Require Import TNRA.

Section TNRAEq.
  Local Open Scope nra_scope.


  Context {m:basic_model}.
  Definition typed_nra τc τin τout := {op:nra|op ▷ τin >=> τout ⊣ τc}.

  Definition tnra_eq {τc} {τin τout} (op1 op2:typed_nra τc τin τout) : Prop :=
    forall (x:data) c
           (dt_x:x ▹ τin)
           (dt_c:bindings_type c τc),
      brand_relation_brands ⊢ (proj1_sig op1) @ₐ x ⊣ c
                 = brand_relation_brands ⊢ (proj1_sig op2) @ₐ x ⊣ c.

  Global Instance tnra_equiv {τc} {τin τout:rtype} : Equivalence (@tnra_eq τc τin τout).

  Notation "t1 ⇝ t2 ⊣ τc" := (typed_nra τc t1 t2) (at level 80) : nra_scope.
  Notation "X ≡τ Y" := (tnra_eq X Y) (at level 80) : nra_scope.

  Local Hint Resolve data_type_normalized : qcert.
  Local Hint Resolve bindings_type_Forall_normalized : qcert.

  Lemma nra_eq_impl_tnra_eq {τc} {τin τout} (op1 op2: τin ⇝ τout ⊣ τc) :
    `op1 ≡ₐ `op2 -> op1 ≡τ op2.

  Lemma nra_eq_pf_irrel {op} {τc} {τin τout} (pf1 pf2: op ▷ τin >=> τout ⊣ τc) :
    tnra_eq (exist _ _ pf1) (exist _ _ pf2).


  Definition tnra_rewrites_to {τc} {τin τout} (op1 op2:nra) : Prop :=
    op1 ▷ τin >=> τout ⊣ τc ->
    (op2 ▷ τin >=> τout ⊣ τc) /\ (forall (x:data) c
                                         (dt_x:x ▹ τin)
                                         (dt_c:bindings_type c τc),
                                     brand_relation_brands ⊢ op1 @ₐ x ⊣ c = brand_relation_brands ⊢ op2 @ₐ x ⊣ c).
  
  Notation "A ↦ₐ B ⊣ C ⊧ op1 ⇒ op2" := (@tnra_rewrites_to C A B op1 op2) (at level 80) : nra_scope.

  Lemma rewrites_typed_and_untyped {τc} {τin τout} (op1 op2:nra):
    (op1 ▷ τin >=> τout ⊣ τc -> op2 ▷ τin >=> τout ⊣ τc) -> op1 ≡ₐ op2 -> τin ↦ₐ τout ⊣ τc ⊧ op1 ⇒ op2.

  Lemma tnra_rewrites_eq_is_typed_eq {τc} {τin τout:rtype} (op1 op2:typed_nra τc τin τout):
    (τin ↦ₐ τout ⊣ τc ⊧ `op1 ⇒ `op2) -> op1 ≡τ op2.

  Lemma tnra_typed_eq_and_type_propag {τc} {τin τout:rtype} (op1 op2:typed_nra τc τin τout):
    op1 ≡τ op2 ->
    ((`op1) ▷ τin >=> τout ⊣ τc -> (`op2) ▷ τin >=> τout ⊣ τc) -> τin ↦ₐ τout ⊣ τc ⊧ (`op1) ⇒ (`op2).

End TNRAEq.

Notation "m ⊢ₐ A ↦ B ⊣ C ⊧ op1 ⇒ op2" := (@tnra_rewrites_to m C A B op1 op2) (at level 80) : nra_scope.

Notation "t1 ⇝ t2 ⊣ tc" := (typed_nra tc t1 t2) (at level 80) : nra_scope.
Notation "X ≡τ Y" := (tnra_eq X Y) (at level 80) : nra_scope.
Notation "X ≡τ' Y" := (tnra_eq (exist _ _ X) (exist _ _ Y)) (at level 80) : nra_scope.