Qcert.NRA.Typing.TNRAEq

Section TNRAEq.

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

  Definition tnra_eq {τin τout} (op1 op2:typed_nra τin τ out) : Prop :=
    ∀ x:data, x ▹ τin → brand_relation_brands ⊢ (proj1_sig op1 ) @ₐ x = brand_relation_brands ⊢ (proj1_sig op2 ) @ₐ x.

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

  Notation "t1 ⇝ t2" := (typed_nra t1 t2) (at level 80).   Notation "X ≡τ Y" := (tnra_eq X Y) (at level 80).
  Lemma nra_eq_impl_tnra_eq {τin τout} (op1 op2: τin ⇝ τ out) :
    `op1 ≡ₐ `op2 → op1 ≡τ op2.

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

  Definition tnra_rewrites_to {τin τout} (op1 op2:nra) : Prop :=
    op1 ▷ τin >=> τ out →
    (op2 ▷ τin >=> τ out ) ∧ (∀ x:data, x ▹ τin → brand_relation_brands ⊢ op1 @ₐ x = brand_relation_brands ⊢ op2 @ₐ x ).

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

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

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

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

End TNRAEq.

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

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