From PCF2 Require Import pcf_2_system pcf_2_contexts.
From PCF2.external.Synthetic Require Import Definitions.
From PCF2.Autosubst Require Import pcf_2.

Definition cont_equiv Γ A s t :=
  forall (ctxt: pctxt), ctxt_typed ctxt Γ A nil Base -> forall v, (fill ctxt s) ⇓ v <-> (fill ctxt t) ⇓ v.

Notation "Γ ⊢ x ≡c y : A" := (cont_equiv Γ A x y) (at level 50, x, y, A at next level).

Definition CE := fun a => match a with (p, A) => nil ⊢ (fst p) ≡c (snd p): A end.

Definition CE_open := fun a => match a with (Γ, p, A) => Γ ⊢ (fst p) ≡c (snd p): A end.

Inductive obs_preorder_base: tm -> tm -> Prop :=
  |norm_bot_min x y: x ≻* bot -> obs_preorder_base x y
  |norm_comp x y z: x ⇓ z -> y ⇓ z -> obs_preorder_base x y.

Hint Constructors obs_preorder_base : core.

Fixpoint obs_preorder_closed (A: ty): tm -> tm -> Prop :=
  fun x y =>
  match A with
  | Base => obs_preorder_base x y
  | Fun A B => forall a b, nil ⊢ a: A -> nil ⊢ b: A -> obs_preorder_closed A a b -> obs_preorder_closed B (app x a) (app y b)
  end.

Definition obs_preorder (Γ: context) (A: ty): tm -> tm -> Prop :=
  fun x y => forall σ, subst_well_typed nil Γ σ -> obs_preorder_closed A (Subst_tm σ x) (Subst_tm σ y).

Definition obs_equiv Γ A x y := obs_preorder Γ A x y /\ obs_preorder Γ A y x.

Notation "x ≤b y" := (obs_preorder_base x y) (at level 50, y at next level).
Notation "x ≤c y : A" := (obs_preorder_closed A x y) (at level 50, y, A at next level).
Notation "Γ ⊢ x ≤ y : A" := (obs_preorder Γ A x y) (at level 50, x, y, A at next level).
Notation "Γ ⊢ x ≡ y : A" := (obs_equiv Γ A x y) (at level 50, x, y, A at next level).