Lvc.Infra.WithTop

Require Import Util MapBasics Infra.Lattice Infra.PartialOrder DecSolve Terminating.

Set Implicit Arguments.

Inductive withTop (A:Type) :=
| Top : withTop A
| wTA (a:A) : withTop A.

Arguments Top [A].
Arguments wTA [A] a.

Instance withTop_eq_dec A `{EqDec A eq} : EqDec (withTop A) eq.
Proof.
  hnf. destruct x,y; eauto; try dec_solve.
  destruct (H a a0); try dec_solve.
  hnf in e. subst. left; eauto.
Qed.

Inductive withTop_le A R `{EqDec A R} : withTop A withTop A Prop :=
| WithTopLe_refl a b : R a b withTop_le (wTA a) (wTA b)
| WithTopLe_top a : withTop_le a Top.

Instance withTop_le_dec A R `{EqDec A R} (a b:withTop A) : Computable (withTop_le a b).
Proof.
  destruct a,b; hnf; eauto using withTop_le.
  - dec_solve.
  - decide (a === a0); dec_solve.
Defined.

Inductive withTop_eq A R `{EqDec A R} : withTop A withTop A Prop :=
| WithTopEq_refl a b : R a b withTop_eq (wTA a) (wTA b)
| WithTopEq_top : withTop_eq Top Top.

Lemma withTopEq_refl_sym A R `{EqDec A R} a b
  : poEq a b withTop_eq (wTA b) (wTA a).
Proof.
  econstructor. symmetry. eauto.
Qed.

Hint Resolve withTopEq_refl_sym.

Instance withTop_eq_comp A R `{EqDec A R} (a b:withTop A)
  : Computable (withTop_eq a b).
Proof.
  destruct a,b; hnf; eauto using withTop_eq.
  - dec_solve.
  - dec_solve.
  - decide (a === a0); dec_solve.
Defined.

Instance withTop_eq_equiv A R `{EqDec A R} : Equivalence (withTop_eq (A:=A) (R:=R)).
Proof.
  constructor.
  - hnf; intros []; eauto using @withTop_eq.
    econstructor. reflexivity.
  - hnf; intros [] []; inversion 1; subst; eauto using @withTop_eq.
    econstructor. symmetry. eauto.
  - hnf; intros [] [] [] X Y; inv X; inv Y; eauto using @withTop_eq.
    econstructor. etransitivity; eauto.
Qed.

Lemma withTop_le_refl A R `{EqDec A R}
  : d d' : withTop A, withTop_eq d d' withTop_le d d'.
Proof.
  intros ? ? X; inv X; eauto using withTop_le.
Qed.

Instance withTop_le_Refl A R `{EqDec A R} : Reflexive (withTop_le (A:=A) (R:=R)).
Proof.
  hnf; intros.
  eapply withTop_le_refl. reflexivity.
Qed.

Instance withTop_le_trans A R `{EqDec A R}
  : Transitive (withTop_le (A:=A) (R:=R)).
Proof.
  hnf; intros [] [] [] X Y; inv X; inv Y; eauto using withTop_le.
  econstructor; etransitivity; eauto.
Qed.

Instance withTop_le_Trans A R `{EqDec A R} : Transitive (withTop_le (A:=A) (R:=R)).
Proof.
  hnf; intros.
  eapply withTop_le_trans. etransitivity; eauto. reflexivity.
Qed.

Instance withTop_le_anti A R `{EqDec A R}
  : Antisymmetric (withTop A) (withTop_eq (A:=A) (R:=R)) (withTop_le (A:=A) (R:=R)).
Proof.
  hnf; intros [] [] X Y; inv X; inv Y; eauto using withTop_eq.
Qed.

Instance withTop_PO A R `{EqDec A R} : PartialOrder (withTop A) :=
  {
    poLe := @withTop_le A R _ _;
    poEq := @withTop_eq A R _ _
  }.
Proof.
  - eapply withTop_le_refl.
Defined.

Lemma withTop_poLe_inv A R `{EqDec A R} (a b:A)
  : poLe (wTA a) (wTA b)
     a === b.
Proof.
  intros. inv H0. eapply H3.
Qed.

Smpl Add 100 match goal with
             | [ H : @poLe _ _ (wTA _) (wTA _) |- _ ] ⇒
               eapply withTop_poLe_inv in H
             | [ H : @poLe _ _ Top _ |- _ ] ⇒ invc H
             | [ H : @poLe _ _ _ (wTA _) |- _ ] ⇒ invc H
             | [ H : @poEq _ _ Top _ |- _ ] ⇒ invc H
             | [ H : @poEq _ _ _ Top |- _ ] ⇒ invc H
             | [ H : @poEq _ _ _ (wTA _) |- _ ] ⇒ invc H
             | [ H : @poEq _ _ (wTA _) _ |- _ ] ⇒ invc H
             | [ H : @withTop_le _ _ _ _ _ _ |- _ ] ⇒ invc H
             end : inv_trivial.

Definition withTop_generic_join A R `{EqDec A R} (a b:withTop A) :=
  match a, b with
  | Top, _Top
  | _, TopTop
  | wTA a, wTA bif [ a === b ] then wTA a else Top
  end.

Lemma withTop_generic_join_bound A R `{EqDec A R}
  : a b : withTop A, a b withTop_generic_join a b b.
Proof.
  intros []; simpl; intros; repeat cases; eauto; econstructor; eauto.
Qed.

Lemma withTop_generic_join_sym A R `{EqDec A R}
  : a b : withTop A, withTop_generic_join a b withTop_generic_join b a.
Proof.
  intros [] []; simpl; try econstructor.
  repeat cases; try econstructor; eauto.
  - exfalso; eapply NOTCOND. symmetry. eauto.
Qed.

Lemma withTop_generic_join_assoc A R `{EqDec A R}
  : a b c : withTop A,
    withTop_generic_join (withTop_generic_join a b) c
                          withTop_generic_join a (withTop_generic_join b c).
Proof.
  intros [] [] []; simpl; repeat (cases; simpl); eauto.
  - exfalso. eapply NOTCOND. rewrite <- COND. eauto.
  - exfalso. eapply NOTCOND. rewrite COND. eauto.
  - exfalso. eapply NOTCOND. eauto.
Qed.

Lemma poLe_withTopLe_refl A R `{EqDec A R} (a b : A)
  : R a b
     poLe (wTA a) (wTA b).
Proof.
  econstructor; eauto.
Qed.

Lemma poEq_withTopEq_refl A R `{EqDec A R} (a b : A)
  : R a b
     poEq (wTA a) (wTA b).
Proof.
  econstructor; eauto.
Qed.

Lemma poLe_withTopLe_top A R `{EqDec A R} (x:withTop A)
  : poLe x Top.
Proof.
  econstructor 2.
Qed.

Hint Resolve poEq_withTopEq_refl poLe_withTopLe_refl poLe_withTopLe_top.

Lemma withTop_generic_join_exp A R `{EqDec A R}
  : a b : withTop A, a withTop_generic_join a b.
Proof.
  intros [] []; simpl; repeat (cases; simpl); eauto.
Qed.

Instance withTop_generic_join_poEq A R `{EqDec A R}
  : Proper (poEq ==> poEq ==> poEq) (withTop_generic_join (A:=A) (R:=R)).
Proof.
  unfold Proper, respectful; intros.
  destruct x,y,x0,y0; simpl;
    repeat (cases; simpl); eauto;
      clear_trivial_eqs.
  - exfalso. eapply NOTCOND.
    rewrite <- H3, <- H4. eauto.
  - exfalso. eapply NOTCOND. rewrite H4, H3. eauto.
Qed.

Instance withTop_generic_join_poLe A R `{EqDec A R}
  : Proper (poLe ==> poLe ==> poLe) (withTop_generic_join (A:=A) (R:=R)).
Proof.
  unfold Proper, respectful; intros.
  destruct x,y,x0,y0; simpl; eauto using withTop_le;
    repeat (cases; simpl); eauto using withTop_le.
  - exfalso. eapply NOTCOND. rewrite H0, H1. eauto.
Qed.

Instance withTop_JSL A R `{EqDec A R} : JoinSemiLattice (withTop A) :=
  {
    join := @withTop_generic_join A R _ _
  }.
Proof.
  - eapply withTop_generic_join_bound.
  - eapply withTop_generic_join_sym.
  - eapply withTop_generic_join_assoc.
  - eapply withTop_generic_join_exp.
Defined.

Inductive withUnknown (A:Type) :=
| Known (a:A) : withUnknown A
| Unknown : withUnknown A.

Arguments Unknown [A].
Arguments Known [A] a.

Instance withUnknown_eq_dec A `{EqDec A eq} : EqDec (withUnknown A) eq.
Proof.
  hnf. destruct x,y; eauto; try dec_solve.
  destruct (H a a0); try dec_solve.
  hnf in e. subst. left; eauto.
Qed.

Inductive withUnknown_eq A R `{EqDec A R} : withUnknown A withUnknown A Prop :=
| WithUnknownEq_refl a b : R a b withUnknown_eq (Known a) (Known b)
| WithUnknownEq_top : withUnknown_eq Unknown Unknown.

Smpl Add 100 match goal with
             | [ H : Known _ === Known _ |- _ ] ⇒ invc H
             | [ H : withUnknown_eq _ _ |- _ ] ⇒ invc H
             end : inv_trivial.

Lemma withUnknownEq_refl_sym A `{PartialOrder A} a b
  : poEq a b withUnknown_eq (Known b) (Known a).
Proof.
  econstructor. symmetry. eauto.
Qed.

Hint Resolve withUnknownEq_refl_sym.

Instance withUnknown_eq_comp A R `{EqDec A R} (a b:withUnknown A)
  : Computable (withUnknown_eq a b).
Proof.
  destruct a,b; hnf; eauto using withUnknown_eq.
  - decide (a === a0); dec_solve.
  - dec_solve.
  - dec_solve.
Defined.

Instance withUnknown_eq_equiv A R `{EqDec A R}
  : Equivalence (withUnknown_eq (A:=A) (R:=R)).
Proof.
  constructor.
  - hnf; intros []; eauto using @withUnknown_eq.
    econstructor. reflexivity.
  - hnf; intros [] []; inversion 1; subst; eauto using @withUnknown_eq.
    econstructor. symmetry. eauto.
  - hnf; intros [] [] [] X Y; inv X; inv Y; eauto using @withUnknown_eq.
    econstructor. etransitivity; eauto.
Qed.

Instance withUnknown_PO A R `{EqDec A R} : PartialOrder (withUnknown A) :=
  {
    poLe := @withUnknown_eq A R _ _ ;
    poEq := @withUnknown_eq A R _ _
  }.
Proof.
  - eauto.
  - hnf; intros; eauto.
Defined.

Instance withUnknown_EqDec A R `{EqDec A R}
  : EqDec (withUnknown A) (@withUnknown_eq _ _ _ _).
Proof.
  hnf. eapply withUnknown_eq_comp.
Defined.

Inductive withBot (A:Type) :=
| Bot : withBot A
| WBElt (a:A) : withBot A.

Arguments Bot [A].
Arguments WBElt [A] a.

Instance withBot_eq_dec A `{EqDec A eq} : EqDec (withBot A) eq.
Proof.
  hnf. destruct x,y; eauto; try dec_solve.
  destruct (H a a0); try dec_solve.
  hnf in e. subst. left; eauto.
Qed.

Inductive withBot_le A `{PartialOrder A} : withBot A withBot A Prop :=
| WithBotLe_refl a b : poLe a b withBot_le (WBElt a) (WBElt b)
| WithBotLe_bot a : withBot_le Bot a.

Instance withBot_le_dec A `{PartialOrder A} (a b:withBot A) : Computable (withBot_le a b).
Proof.
  destruct a,b; hnf; eauto using withBot_le.
  - dec_solve.
  - decide (poLe a a0); dec_solve.
Defined.

Inductive withBot_eq A `{PartialOrder A} : withBot A withBot A Prop :=
| WithBotEq_refl a b : poEq a b withBot_eq (WBElt a) (WBElt b)
| WithBotEq_bot : withBot_eq Bot Bot.

Lemma withBotEq_refl_sym A `{PartialOrder A} a b
  : poEq a b withBot_eq (WBElt b) (WBElt a).
Proof.
  econstructor. symmetry. eauto.
Qed.

Hint Resolve withBotEq_refl_sym.

Instance withBot_eq_comp A `{PartialOrder A} (a b:withBot A)
  : Computable (withBot_eq a b).
Proof.
  destruct a,b; hnf; eauto using withBot_eq.
  - dec_solve.
  - dec_solve.
  - decide (poEq a a0); dec_solve.
Defined.

Instance withBot_eq_equiv A `{PartialOrder A} : Equivalence (withBot_eq (A:=A)).
Proof.
  constructor.
  - hnf; intros []; eauto using @withBot_eq.
  - hnf; intros [] []; inversion 1; subst; eauto using @withBot_eq.
  - hnf; intros [] [] [] X Y; inv X; inv Y; eauto using @withBot_eq.
    econstructor. etransitivity; eauto.
Qed.

Lemma withBotLe_refl A `{PartialOrder A}
  : d d' : withBot A, withBot_eq d d' withBot_le d d'.
Proof.
  intros ? ? X; inv X; eauto using withBot_le.
Qed.

Instance withBot_le_trans A `{PartialOrder A}
  : Transitive (withBot_le (A:=A)).
Proof.
  hnf; intros [] [] [] X Y; inv X; inv Y; eauto using withBot_le.
Qed.

Instance withBot_le_anti A `{PartialOrder A}
  : Antisymmetric (withBot A) (withBot_eq (A:=A)) (withBot_le (A:=A)).
Proof.
  hnf; intros [] [] X Y; inv X; inv Y; eauto using withBot_eq.
  exploit poLe_antisymmetric; eauto.
Qed.

Instance withBot_PO A `{PartialOrder A} : PartialOrder (withBot A) :=
  {
    poLe := @withBot_le A _;
    poEq := @withBot_eq A _
  }.
Proof.
  - eapply withBotLe_refl.
Defined.

Instance withBot_lower_bounded A `{PartialOrder A} : LowerBounded (withBot A) :=
  {
    bottom := Bot
  }.
Proof.
  intros. destruct a; econstructor.
Qed.

Instance terminating_withTop X R `{EqDec X R}
  : Terminating (withTop X) poLt.
Proof.
  hnf; intros.
  destruct x.
  - econstructor; intros. exfalso.
    destruct H0; clear_trivial_eqs. eauto.
  - econstructor; intros.
    destruct H0. invc H0.
    + exfalso. eapply H1. econstructor. symmetry. eauto.
    + econstructor; intros. exfalso.
      destruct H0; clear_trivial_eqs. eauto.
Qed.