Require Import Base.

Definition Var := nat.

Inductive Exp := top | bot | var (x: Var) | neg (s: Exp)
               | con (s t: Exp) | dis (s t: Exp).

Implicit Types x y z : Var.
Implicit Types s t u v : Exp.

Notation "s && t" := (con s t) (at level 40, left associativity).
Notation "s || t" := (dis s t) (at level 50, left associativity).
Notation "-- s" := (neg s) (at level 35, right associativity).

Instance Exp_eq_dec :
  eq_dec Exp.
Proof.
  unfold dec. decide equality. apply nat_eq_dec.
Qed.

Fixpoint subst s x t : Exp :=
  match s with
    | top => top
    | bot => bot
    | var y => if Dec (x=y) then t else var y
    | -- s => -- subst s x t
    | s && s' => subst s x t && subst s' x t
    | s || s' => subst s x t || subst s' x t
  end.

Fixpoint vars s : list nat :=
  match s with
    | top => nil
    | bot => nil
    | var x => [x]
    | -- s => vars s
    | s && t => vars s ++ vars t
    | s || t => vars s ++ vars t
end.

Definition Assn := Var -> bool.

Implicit Types alpha : Assn.

Definition tau : Assn := fun x => true.

Fixpoint eva alpha s : bool :=
  match s with
    | top => true
    | bot => false
    | var x => alpha x
    | --s => negb (eva alpha s)
    | s && t => andb (eva alpha s) (eva alpha t)
    | s || t => orb (eva alpha s) (eva alpha t)
  end.

Definition beq s t := forall alpha, eva alpha s = eva alpha t.

Notation "s =~= t" := (beq s t) (at level 70).

Definition sat s := exists alpha, eva alpha s = true.

Reserved Notation "s == t " (at level 70, no associativity).

Inductive aeq : Exp -> Exp -> Prop :=
| Comm s t : s && t == t && s
| Comm' s t : s || t == t || s
| Iden s : s && top == s
| Iden' s : s || bot == s
| Nega s : s && --s == bot
| Nega' s : s || --s == top
| Dist s t u : s && (t || u) == s && t || s && u
| Dist' s t u : s || t && u == (s || t) && (s || u)
| Symm s t : s == t -> t == s
| Tran s t u: s == t -> t == u -> s == u
| CompN s s' : s == s' -> --s == --s'
| CompC s s' t : s == s' -> s && t == s' && t
| CompD s s' t : s == s' -> s || t == s' || t
where "s == t" := (aeq s t).

Fact Refl s :
  s == s.
Proof.
  apply Tran with (t:= s&&top).
  - apply Symm, Iden.
  - apply Iden.
Qed.

Instance aeq_Equivalence :
  Equivalence aeq.
Proof.
  constructor; hnf.
  - apply Refl.
  - apply Symm.
  - apply Tran.
Qed.

Instance neg_aeq_proper :
  Proper (aeq ==> aeq) neg.
Proof.
  cbv. auto using CompN.
Qed.

Fact comp_con s s' t t' :
  s == s' -> t == t' -> s && t == s' && t'.
Proof.
  intros H1 H2.
  rewrite (CompC _ H1).
  rewrite (Comm s' t), (Comm s' t').
  now apply CompC.
Qed.

Instance con_aeq_proper :
  Proper (aeq ==> aeq ==> aeq) con.
Proof.
  cbv. auto using comp_con.
Qed.

Fact comp_dis s s' t t' :
  s == s' -> t == t' -> s || t == s' || t'.
Proof.
  intros H1 H2.
  rewrite (CompD _ H1).
  rewrite (Comm' s' t), (Comm' s' t').
  now apply CompD.
Qed.

Instance dis_aeq_proper :
  Proper (aeq ==> aeq ==> aeq) dis.
Proof.
  cbv. auto using comp_dis.
Qed.

Lemma soundness s t :
  s == t -> s =~= t.
Proof.
  intros H alpha.
  induction H; cbn;
  try congruence;
  destruct (eva alpha s); auto;
  destruct (eva alpha t); auto.
Qed.

Lemma consistency :
  ~ top == bot.
Proof.
  intros H % soundness.
  discriminate (H tau).
Qed.

Fact substitutivity s t x u :
  s == t -> subst s x u == subst t x u.
Proof.
  induction 1; cbn; eauto using aeq.
Qed.

Fixpoint dual s : Exp :=
  match s with
    | top => bot
    | bot => top
    | var x => var x
    | --s => --dual s
    | s && t => dual s || dual t
    | s || t => dual s && dual t
  end.

Lemma dual_involutive s :
  dual (dual s) = s.
Proof.
  induction s; cbn; congruence.
Qed.

Lemma dualize s t :
  s == t -> dual s == dual t.
Proof.
  induction 1; eauto using aeq.
Qed.

Lemma dualize' s t :
  dual s == dual t -> s == t.
Proof.
  intros A.
  apply dualize in A.
  rewrite !dual_involutive in A.
  exact A.
Qed.

Lemma neg_top :
  --top == bot.
Proof.
  rewrite <- Iden at 1.
  rewrite Comm.
  apply Nega.
Qed.

Lemma neg_bot :
  --bot == top.
Proof.
  apply dualize', neg_top.
Qed.

Lemma Idem s :
  s && s == s.
Proof.
  rewrite <- (Iden s) at 3.
  rewrite <- (Nega' s).
  rewrite Dist.
  rewrite Nega.
  rewrite Iden'.
  reflexivity.
Qed.

Lemma Idem' s :
  s || s == s.
Proof.
  apply dualize', Idem.
Qed.

Lemma Annu s :
  s && bot == bot.
Proof.
  symmetry.
  rewrite <- (Nega s) at 1.
  rewrite <- (Iden'(--s)).
  rewrite Dist at 1.
  now rewrite Nega, Comm', Iden'.
Qed.

Lemma Annu' s :
  s || top == top.
Proof.
  apply dualize', Annu.
Qed.

Lemma Absorp s t :
  s && (s || t) == s.
Proof.
  rewrite <- (Iden' s) at 1. rewrite <- Dist'.
  now rewrite Comm, Annu, Iden'.
Qed.

Lemma Absorp' s t :
  s || (s && t) == s.
Proof.
  apply dualize', Absorp.
Qed.

Lemma Expa t s :
  s == (t || s) && (--t || s).
Proof.
  symmetry.
  rewrite !(Comm' _ s).
  rewrite <- Dist'.
  rewrite Nega.
  apply Iden'.
Qed.

Lemma Expa' t s :
  s == (t && s) || (--t && s).
Proof.
  apply dualize', Expa.
Qed.

Lemma expa u s t :
  u || s == u || t ->
  --u || s == --u || t ->
  s == t.
Proof.
  intros A B.
  rewrite (Expa u s), (Expa u t).
  auto using comp_con.
Qed.

Lemma Asso s t u :
  s && (t && u) == (s && t) && u.
Proof.
  apply expa with (u:=s).
  - rewrite Absorp'. rewrite Dist'. rewrite Absorp'. now rewrite Absorp.
  - rewrite !Dist'. rewrite !(Comm' _ s), !Nega'.
    rewrite !(Comm top). now rewrite !Iden.
Qed.

Lemma Asso' s t u :
  s || (t || u) == (s || t) || u.
Proof.
  apply dualize', Asso.
Qed.

Fact reduce_aeq s t :
  s == t <-> s && --t || --s && t == bot.
Proof.
  split; intros H.
  - rewrite !H. rewrite Nega.
    rewrite Comm, Nega. apply Iden'.
  - enough (s == s || t /\ t == t || s) as [H1 H2].
    { rewrite H2. rewrite Comm'. exact H1. }
    split.
    + rewrite <-(Iden' s) at 1. rewrite <-H. clear H.
      rewrite Asso', Absorp'. rewrite Comm at 1.
      rewrite Dist', Nega'. apply Iden.
    + rewrite <-(Iden' t) at 1. rewrite <-H. clear H.
      rewrite (Comm' (s&&_)). rewrite Asso'. rewrite Comm at 1.
      rewrite Absorp'. rewrite Dist', Nega'. apply Iden.
Qed.

Lemma UoC s t :
  s && t == bot -> s || t == top -> --s == t.
Proof.
  intros A B.
  rewrite <- (Iden (-- s)). rewrite <- B. rewrite Dist.
  rewrite Comm. rewrite Nega. rewrite Comm'. rewrite Iden'.
  rewrite <- (Iden t) at 2. rewrite <- (Nega' s).
  rewrite Dist. rewrite (Comm t s). rewrite A.
  rewrite Comm'. rewrite Iden'. apply Comm.
Qed.

Lemma DN s :
  -- -- s == s.
Proof.
  apply UoC.
  - rewrite Comm. apply Nega.
  - rewrite Comm'. apply Nega'.
Qed.

Lemma deMorgan s t :
  -- (s && t) == -- s || -- t.
Proof.
  apply UoC.
  - rewrite Dist.
    rewrite <- !Asso.
    rewrite Nega. rewrite Annu. rewrite Iden'.
    rewrite (Comm t). rewrite Asso. rewrite Nega.
    rewrite Comm. apply Annu.
  - rewrite Comm'. rewrite Dist'.
    rewrite <- !Asso'.
    rewrite (Comm' _ t).
    rewrite Nega'. rewrite Annu'. rewrite Iden.
    rewrite Comm'. rewrite <- Asso'. rewrite Nega'.
    apply Annu'.
Qed.

Lemma deMorgan' s t :
  -- (s || t) == -- s && -- t.
Proof.
  apply dualize', deMorgan.
Qed.

Lemma propagate_neg s t :
  s && --t == s && --(s && t).
Proof.
  rewrite deMorgan.
  rewrite Dist.
  rewrite Nega.
  rewrite Comm'.
  now rewrite Iden'.
Qed.

Lemma propagate_con s t u :
  s && (t && u) == (s && t) && (s && u).
Proof.
  rewrite <- (Idem s) at 1.
  rewrite <- Asso.
  rewrite (Comm s (t&&u)).
  rewrite (Comm s u).
  now rewrite !Asso.
Qed.

Lemma expansion_top s x :
  var x && s == var x && subst s x top.
Proof.
  induction s as [ | |y|s|s1 IH1 s2 IH2|s1 IH1 s2 IH2]; cbn.
  - reflexivity.
  - reflexivity.
  - decide (x = y) as [<-|A].
    + now rewrite Idem, Iden.
    + reflexivity.
  - rewrite propagate_neg.
    rewrite IHs.
    now rewrite <- propagate_neg.
  - rewrite propagate_con.
    rewrite IH1. rewrite IH2.
    now rewrite <- propagate_con.
  - rewrite Dist.
    rewrite IH1. rewrite IH2.
    now rewrite <- Dist.
Qed.

Lemma expansion_bot s x :
  --var x && s == --var x && subst s x bot.
Proof.
  induction s as [ | |y|s|s1 IH1 s2 IH2|s1 IH1 s2 IH2]; cbn.
  - reflexivity.
  - reflexivity.
  - decide (x = y) as [<-|A].
    + rewrite Annu. rewrite Comm. apply Nega.
    + reflexivity.
  - rewrite propagate_neg.
    rewrite IHs.
    now rewrite <- propagate_neg.
  - rewrite propagate_con.
    rewrite IH1. rewrite IH2.
    now rewrite <- propagate_con.
  - rewrite Dist.
    rewrite IH1. rewrite IH2.
    now rewrite <- Dist.
Qed.

Notation cond x s t := (var x && s || --var x && t).

Lemma expansion s x :
  s == cond x (subst s x top) (subst s x bot).
Proof.
  rewrite (Expa' (var x)) at 1.
  now rewrite expansion_top, expansion_bot.
Qed.

Lemma reduce x s :
  cond x s s == s.
Proof.
  rewrite (Comm (var x)), (Comm (--var x)).
  rewrite <-Dist, Nega', Iden. reflexivity.
Qed.

Inductive ground : Exp -> Prop :=
| groundT : ground top
| groundB : ground bot
| groundN s : ground s -> ground (--s)
| groundC s t : ground s -> ground t -> ground (s && t)
| groundD s t : ground s -> ground t -> ground (s || t).

Lemma ground_eval s alpha :
  ground s -> s == if eva alpha s then top else bot.
Proof.
  intros A.
  induction A; cbn.
  - reflexivity.
  - reflexivity.
  - rewrite IHA at 1.
    destruct (eva alpha s); cbn;
    apply neg_top || apply neg_bot.
  - rewrite IHA1, IHA2 at 1.
    destruct (eva alpha s), (eva alpha t); cbn;
    apply Iden || apply Annu.
  - rewrite IHA1, IHA2 at 1.
    destruct (eva alpha s), (eva alpha t); cbn;
    apply Iden' || apply Annu'.
Qed.

Lemma vars_ground s :
  vars s <<= nil -> ground s.
Proof.
  induction s; cbn; intros A; auto using ground.
  - apply incl_nil_eq in A. discriminate A.
  - apply incl_app_left in A as [A1 A2]; auto using ground.
  - apply incl_app_left in A as [A1 A2]; auto using ground.
Qed.

Lemma agreement :
  (forall s, sat s \/ s == bot) ->
  forall s t, s == t <-> s =~= t.
Proof.
  intros H s t. split.
  - apply soundness.
  - intros H1.
    specialize (H (s && --t || --s && t)).
    destruct H as [[alpha H]|H].
    + exfalso. revert H. cbn. rewrite H1.
      destruct (eva alpha t); cbn; auto.
    + apply reduce_aeq, H.
Qed.

Definition update alpha x b : Assn :=
  fun y => if Dec (x=y) then b else alpha y.

Implicit Types A B : list Var.

Fixpoint solve A s : option Assn :=
  match A with
  | nil => if eva tau s then Some tau else None
  | x::A' => match solve A' (subst s x bot), solve A' (subst s x top) with
            | Some alpha, _ => Some (update alpha x false)
            | _, Some alpha => Some (update alpha x true)
            | None, None => None
            end
  end.

Lemma shift alpha s x t :
  eva alpha (subst s x t) = eva (update alpha x (eva alpha t)) s.
Proof.
  induction s as [| |y|s IH|s1 IH1 s2 IH2|s1 IH1 s2 IH2];
    cbn; try congruence.
  unfold update. now decide (x=y).
Qed.

Lemma subst_vars_ground s x A t :
  vars t <<= nil -> vars s <<= x::A -> vars (subst s x t) <<= A.
Proof.
  intros H1 H2.
  induction s as [| |y|s IH|s1 IH1 s2 IH2|s1 IH1 s2 IH2]; cbn in *.
  - auto.
  - auto.
  - decide (x=y) as [<-|H3];cbn.
    + rewrite H1. auto.
    + assert (y el x::A) as H4 by auto. cbn in *; intuition.
  - auto.
  - apply incl_app_left in H2 as [H2 H3]. auto.
  - apply incl_app_left in H2 as [H2 H3]. auto.
Qed.

Lemma solve_correct s A :
  vars s <<= A ->
  match solve A s with
  | Some alpha => eva alpha s = true
  | None => s == bot
  end.
Proof.
  revert s. induction A as [|x A IH]; cbn; intros s H.
  - destruct (eva tau s) as [alpha|] eqn:E.
    + exact E.
    + apply vars_ground, (ground_eval tau) in H.
      now rewrite H, E.
  - destruct (solve A (subst s x bot)) as [alpha|] eqn:E.
    + specialize (IH (subst s x bot)).
      rewrite E, shift in IH. apply IH.
      apply subst_vars_ground; cbn; auto.
    + destruct (solve A (subst s x top)) as [alpha|] eqn:E'.
      * specialize (IH (subst s x top)).
        rewrite E', shift in IH. apply IH.
        apply subst_vars_ground; cbn; auto.
      * assert (vars (subst s x top) <<= A) as H1 % IH.
        { apply subst_vars_ground; cbn; auto. }
        rewrite E' in H1.
        assert (vars (subst s x bot) <<= A) as H2 % IH.
        { apply subst_vars_ground; cbn; auto. }
        rewrite E in H2.
        rewrite (expansion s x), H1, H2. apply reduce.
Qed.

Lemma Solve s :
  { alpha | eva alpha s = true} + { s == bot }.
Proof.
  assert (vars s <<= vars s) as H % solve_correct by auto.
  destruct (solve _ _); eauto.
Qed.

Theorem Agreement s t :
  s == t <-> s =~= t.
Proof.
  revert s t. apply agreement.
  intros s.
  destruct (Solve s) as [[alpha H]|H];
    unfold sat; eauto.
Qed.

Lemma aeq_dec_bot s :
  dec (s == bot).
Proof.
  destruct (Solve s) as [[alpha H]|H].
  - right. intros H1 % soundness.
    rewrite H1 in H. discriminate H.
  - unfold dec. auto.
Qed.

Theorem decidability s t :
  dec (s == t).
Proof.
  apply dec_transfer with (P := s && --t || --s && t == bot).
  - symmetry. apply reduce_aeq.
  - apply aeq_dec_bot.
Qed.