Lvc.Eqn

Require Import CSet Le.

Require Import Plus Util AllInRel Map.
Require Import CSet Val Var Env EnvTy Equiv.Sim IL Fresh Annotation MoreExp Coherence.

Require Import SetOperations Filter.

Set Implicit Arguments.

Inductive eqn :=
  | EqnEq (e e´:exp)
  | EqnApx (e e´:exp)
  | EqnBot.

Definition satisfies (E:onv val) (gamma:eqn) : Prop :=
match gamma with
| EqnEq e e´ ⇒ option_R eq (exp_eval E e) (exp_eval E e´)
| EqnApx e e´ ⇒ fstNoneOrR eq (exp_eval E e) (exp_eval E e´)
| EqnBot ⇒ False
end.

Inductive eqnLt : eqn → eqn → Prop :=
| EqnLtBotEq e e´
  : eqnLt EqnBot (EqnEq e e´)
| EqnLtBotApx e e´
  : eqnLt EqnBot (EqnApx e e´)
| EqnLtEqApx e1 e1´ e2 e2´
  : eqnLt (EqnEq e1 e2) (EqnApx e1´ e2´)
| EqnLtEqEq1 e1 e1´ e2 e2´
  : expLt e1 e1´
    → eqnLt (EqnEq e1 e2) (EqnEq e1´ e2´)
| EqnLtEqEq2 e1 e2 e2´
  : expLt e2 e2´
    → eqnLt (EqnEq e1 e2) (EqnEq e1 e2´)
| EqnLtApxApx1 e1 e1´ e2 e2´
  : expLt e1 e1´
    → eqnLt (EqnApx e1 e2) (EqnApx e1´ e2´)
| EqnLtApxApx2 e1 e2 e2´
  : expLt e2 e2´
    → eqnLt (EqnApx e1 e2) (EqnApx e1 e2´).

Instance eqnLt_irr : Irreflexive eqnLt.
Qed.

Instance eqnLt_trans : Transitive eqnLt.
Qed.

Instance StrictOrder_eqnLt : OrderedType.StrictOrder eqnLt eq.
Qed.

Local Notation "´Compare´ x ´next´ y" :=
  (match x with
    | Eq ⇒ y
    | z ⇒ z
  end) (at level 100).

Fixpoint eqn_cmp (e e´:eqn) :=
  match e, e´ with
    | EqnBot, EqnBot ⇒ Eq
    | EqnBot, _ ⇒ Lt
    | EqnEq _ _, EqnBot ⇒ Gt
    | EqnEq _ _, EqnApx _ _ ⇒ Lt
    | EqnEq e1 e2, EqnEq e1´ e2´ ⇒
      Compare _cmp e1 e1´ next
      Compare _cmp e2 e2´ next Eq
    | EqnApx e1 e2, EqnApx e1´ e2´ ⇒
      Compare _cmp e1 e1´ next
      Compare _cmp e2 e2´ next Eq
    | EqnApx _ _, _ ⇒ Gt
  end.

Instance OrderedType_eqn : OrderedType eqn :=
 { _eq := eq;
  _lt := eqnLt;
  _cmp := eqn_cmp}.
Defined.

Definition eqns := set eqn.

Definition satisfiesAll (E:onv val) (Gamma:eqns) :=
  ∀ gamma, gamma ∈ Gamma → satisfies E gamma.

Definition freeVars (gamma:eqn) :=
  match gamma with
    | EqnEq e e´ ⇒ Exp.freeVars e ∪ Exp.freeVars e´
    | EqnApx e e´ ⇒ Exp.freeVars e ∪ Exp.freeVars e´
    | EqnBot ⇒ ∅
  end.

Definition eqns_freeVars (Gamma:eqns) := fold union (map freeVars Gamma) ∅.

Definition entails Gamma Γ´ := ∀ E, satisfiesAll E Gamma → satisfiesAll E Γ´.

Definition not_entails Gamma gamma := ∃ E, satisfiesAll E Gamma ∧ ¬ satisfies E gamma.

Definition onvLe X (E E´:onv X)
:= ∀ x v, E x = Some v → E´ x = Some v.


Lemma exp_eval_onvLe e E E´ v
: onvLe E E´
  → exp_eval E e = Some v
  → exp_eval E´ e = Some v.

Definition list_EqnApx Y Y´ :=
  of_list (zip (fun e e´ ⇒ EqnApx e e´) Y Y´).

Definition subst_eqn (ϱ : env exp) (gamma: eqn) :=
  match gamma with
    | EqnEq e e´ ⇒ EqnEq (subst_exp ϱ e) (subst_exp ϱ e´)
    | EqnApx e e´ ⇒ EqnApx (subst_exp ϱ e) (subst_exp ϱ e´)
    | EqnBot ⇒ EqnBot
  end.

Definition subst_eqns (ϱ : env exp) (G:eqns) : eqns :=
  map (subst_eqn ϱ) G.

Definition sid := fun x ⇒ Var x.

Definition unsatisfiable (Gamma:eqns) :=
  ∀ E, ¬ satisfiesAll E Gamma.