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_eqc} {τ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) @ₐ xc
                 = brand_relation_brands ⊢ (proj1_sig op2) @ₐ xc.

  Global Instance tnra_equivc} {τin τout:rtype} : Equivalence (@tnra_eq τc τin τout).
Proof.
    constructor.
    - unfold Reflexive, tnra_eq.
      intros; reflexivity.
    - unfold Symmetric, tnra_eq.
      intros; rewrite (H x0 c dt_x dt_c); reflexivity.
    - unfold Transitive, tnra_eq.
      intros; rewrite (H x0 c dt_x dt_c); rewrite (H0 x0 c dt_x dt_c); reflexivity.
  Qed.

  Notation "t1t2 ⊣ τ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_eqc} {τin τout} (op1 op2: τin ⇝ τout ⊣ τc) :
    `op1 ≡ₐ `op2 -> op1 ≡τ op2.
Proof.
    unfold tnra_eq, nra_eq; intros.
    eapply H; eauto with qcert.
  Qed.

  Lemma nra_eq_pf_irrel {op} {τc} {τin τout} (pf1 pf2: op ▷ τin >=> τout ⊣ τc) :
    tnra_eq (exist _ _ pf1) (exist _ _ pf2).
Proof.
    red; intros; simpl.
    reflexivity.
  Qed.


  Definition tnra_rewrites_toc} {τ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_brandsop1 @ₐ xc = brand_relation_brandsop2 @ₐ xc).
  
  Notation "A ↦ₐ BCop1op2" := (@tnra_rewrites_to C A B op1 op2) (at level 80) : nra_scope.

  Lemma rewrites_typed_and_untypedc} {τin τout} (op1 op2:nra):
    (op1 ▷ τin >=> τout ⊣ τc -> op2 ▷ τin >=> τout ⊣ τc) -> op1 ≡ₐ op2 -> τin ↦ₐ τout ⊣ τcop1op2.
Proof.
    intros.
    unfold tnra_rewrites_to; simpl; intros.
    split; eauto with qcert.
  Qed.

  Lemma tnra_rewrites_eq_is_typed_eqc} {τin τout:rtype} (op1 op2:typed_nra τc τin τout):
    (τin ↦ₐ τout ⊣ τc ⊧ `op1 ⇒ `op2) -> op1 ≡τ op2.
Proof.
    unfold tnra_rewrites_to, tnra_eq; intros.
    elim H; clear H; intros.
    apply (H0 x c dt_x dt_c).
    dependent induction op1; simpl.
    assumption.
  Qed.

  Lemma tnra_typed_eq_and_type_propagc} {τ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).
Proof.
    unfold tnra_rewrites_to, tnra_eq; intros.
    split.
    apply H0; assumption.
    assumption.
  Qed.

End TNRAEq.

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

Notation "t1t2tc" := (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.