ICL.ctab

Require Export PropL.

Implicit Types x y z : var.
Implicit Types s t : form.
Implicit Types alpha beta : assn.
Implicit Types A B : context.
Implicit Types m n k : nat.

Boolean satisfaction

Fixpoint eval alpha s : bool :=
  match s with
    | Var x => alpha x
    | Imp s t => if eval alpha s then eval alpha t else true
    | Fal => false
  end.

Fixpoint satis alpha s : Prop :=
  match s with
    | Var x => if alpha x then True else False
    | Imp s1 s2 => satis alpha s1 -> satis alpha s2
    | Fal => False
  end.

Lemma satis_eval alpha s :
  satis alpha s <-> eval alpha s = true.
Proof.
  induction s as [x|s1 IH1 s2 IH2|]; simpl.
  - destruct (alpha x); intuition.
  - destruct (eval alpha s1); intuition.
  - intuition.
Qed.

Instance satis_dec alpha s : dec (satis alpha s).
Proof.
  eapply dec_prop_iff.
  - symmetry. apply satis_eval.
  - auto.
Qed.

Lemma satis_pos_imp alpha s t :
  satis alpha (Imp s t) <-> ~ satis alpha s \/ satis alpha t.
Proof.
  simpl. decide (satis alpha s) ; tauto.
Qed.

Lemma satis_neg_imp alpha s t :
  ~ satis alpha (Imp s t) <-> satis alpha s /\ ~ satis alpha t.
Proof.
  simpl. decide (satis alpha s) ; tauto.
Qed.

Validity and boolean entailment

Definition valid s : Prop :=
  forall alpha, satis alpha s.

Lemma valid_unsat s :
  valid s <-> ~ exists alpha, satis alpha (Not s).
Proof.
  rewrite DM_exists.
  split.
  - intros F alpha G. apply G, F.
  - intros F alpha. apply dec_DN; auto. apply F.
Qed.

Definition bent A s : Prop :=
  forall alpha, (forall t, t el A -> satis alpha t) -> satis alpha s.

Lemma ndc_bent A s :
  ndc A s -> bent A s.

Proof.
  intros E alpha F.
  induction E as [A s E|A s t _ IH|A s t _ IHs _ IHt|A s _ IH] ; simpl in *.
  - apply F, E.
  - intros G. apply IH. intros u [[]|H]; auto.
  - apply (IHs F), (IHt F).
  - decide (satis alpha s) as [G|G]. exact G.
    exfalso ; apply IH. intros t [[]|H]; auto.
Qed.

Signed formulas and clauses

Inductive sform : Type :=
| Pos : form -> sform
| Neg : form -> sform.

Definition clause := list sform.

Notation "+ s" := (Pos s) (at level 35).
Notation "- s" := (Neg s).

Implicit Types S T : sform.
Implicit Types C D : clause.

Instance sform_eq_dec S T : dec (S = T).
Proof.
  unfold dec. repeat decide equality.
Qed.

Definition uns S : form :=
  match S with +s => s | -s => Not s end.

Fixpoint satis' alpha C : Prop :=
  match C with
    | nil => True
    | T::C' => satis alpha (uns T) /\ satis' alpha C'
  end.

Definition sat C := exists alpha, satis' alpha C.

Lemma satis_iff alpha C :
  satis' alpha C <-> forall S, S el C -> satis alpha (uns S).
Proof.
  induction C; simpl; intuition; subst; auto.
Qed.

Lemma satis_in alpha C S :
  satis' alpha C -> S el C -> satis alpha (uns S).
Proof.
  intros E. apply satis_iff, E.
Qed.

Lemma satis_weak alpha C C' :
  C <<= C' -> satis' alpha C' -> satis' alpha C.
Proof.
  rewrite !satis_iff. auto.
Qed.

Lemma sat_weak C C' :
  C <<= C' -> sat C' -> sat C.
Proof.
  intros E [alpha F]. exists alpha. eauto using satis_weak.
Qed.

Entailment of clauses

Definition cent C D : Prop :=
  forall alpha, satis' alpha C -> satis' alpha D.

Lemma cent_weak C D D' :
  D <<= D' -> cent C D' -> cent C D.
Proof.
  intros F G alpha K. apply (satis_weak F),G, K.
Qed.

Lemma cent_sat C D :
  cent C D -> sat C -> sat D.
Proof.
  intros F [alpha G]. exists alpha. apply F, G.
Qed.

Solved Clauses

Definition svar S : Prop :=
  match S with
    | +Var _ | -Var _ => True
    | _ => False
  end.

Definition solved C : Prop :=
  (forall S, S el C -> svar S ) /\ forall x, +Var x el C -> ~ -Var x el C.

Definition phi C x := if decision (+Var x el C) then true else false.

Lemma solved_phi C :
  solved C -> satis' (phi C) C.
Proof.
  intros [F G]. apply satis_iff.
  intros S K. assert (L := F S K).
  destruct S as [[x| |]|[x| |]];
    inv L; simpl; unfold phi;
    decide (+Var x el C) as [L|L]; auto.
  apply G in L. auto.
Qed.

Lemma solved_sat C :
  solved C -> sat C.
Proof.
  intros F. exists (phi C). apply solved_phi, F.
Qed.

Lemma solved_nil :
  solved nil.
Proof.
  firstorder.
Qed.

Lemma solved_pos_var x C :
  solved C -> ~ -Var x el C -> solved (+Var x :: C).
Proof.
  intros F G. split.
  - intros S [K|K].
    + subst S. simpl; auto.
    + apply F, K.
  - intros y [K|K] [L|L]; try inv K; try inv L; auto.
    eapply F; eauto.
Qed.

Lemma solved_neg_var x C :
  solved C -> ~ +Var x el C -> solved (-Var x :: C).
Proof.
  intros F G. split.
  - intros S [K|K].
    + subst S. simpl; auto.
    + apply F, K.
  - intros y [K|K] [L|L]; try inv K; try inv L; auto.
    eapply F; eauto.
Qed.

Lemma cent_solved_sat C D :
  cent C D -> solved C -> sat D.
Proof.
  intros G F. apply (cent_sat G), solved_sat, F.
Qed.

Refutation predicates

Record ref_pred (rho : clause -> Prop) :=
  { ref_Fal : forall C, +Fal el C -> rho C;
    ref_weak : forall C C', C <<= C' -> rho C -> rho C';
    ref_clash : forall x C, +Var x el C -> -Var x el C -> rho C;
    ref_pos_imp : forall s t C, rho (-s ::C) -> rho (+t ::C) -> rho (+Imp s t ::C);
    ref_neg_imp : forall s t C, rho (+s ::-t ::C) -> rho (-Imp s t ::C);
    ref_sound : forall C, rho C -> ~ sat C }.

Lemma ref_unsat :
  ref_pred (fun C => ~ sat C).
Proof.
  split.
  - intros C E [alpha F]. apply (satis_in F E).
  - intros C C' A E F. apply E. revert A F. apply sat_weak.
  - intros s C A B [alpha E]. apply (satis_in E B), (satis_in E A).
  - intros s t C A B [alpha [E F]]. apply satis_pos_imp in E as [E|E].
    + apply A. exists alpha. simpl. auto.
    + apply B. exists alpha. simpl. auto.
  - intros s t C A [alpha [E F]]. apply A. exists alpha. simpl in *.
    apply satis_neg_imp in E as [E G]. auto.
  - auto.
Qed.

Lemma ref_ndc :
  ref_pred (fun C => ndc (map uns C) Fal).
Proof.
  split; simpl.
  - intros C A. apply ndcA. exact (in_map uns _ _ A).
  - intros C C' A. apply ndc_weak. apply incl_map, A.
  - intros x C A B. apply ndcIE with (s:=Var x) ; apply ndcA.
    + exact (in_map uns _ _ B).
    + exact (in_map uns _ _ A).
  - intros s t C A B. apply ndcIE with (s:= Not s).
    + apply ndcW, ndcII, A.
    + apply ndcII. apply ndcIE with (s:=t).
      * apply ndcW, ndcW, ndcII, B.
      * apply ndcIE with (s:=s) ; apply ndcA ; auto.
  - intros s t C A. apply ndcIE with (s:= Imp s t).
    + apply ndcA ; auto.
    + apply ndcII, ndcE. apply ndcIE with (s:= Not t).
      * { apply ndcIE with (s:= s).
          - apply ndcW, ndcW, ndcII, ndcII. revert A. apply ndc_weak. firstorder.
          - apply ndcA ; auto. }
      * { apply ndcII. apply ndcIE with (s:= Imp s t).
          - apply ndcA ; auto.
          - apply ndcII, ndcA ; auto. }
  - intros C F [alpha G].
    apply ndc_bent in F. apply (F alpha).
    intros t K.
    apply in_map_iff in K as [[u|u] [K1 K2]];
      subst t; revert K2; apply satis_in, G.
Qed.

Decision trees

Inductive rec C : clause -> Type :=
| recNil : rec C nil
| recPF D : rec C (+Fal :: D)
| recNF D : rec C D -> rec C (-Fal ::D)
| recPV D x : -Var x el C -> rec C (+Var x :: D)
| recPV' D x : ~ -Var x el C -> rec (+Var x :: C) D -> rec C (+Var x :: D)
| recNV D x : +Var x el C -> rec C (-Var x :: D)
| recNV' D x : ~ +Var x el C -> rec (-Var x :: C) D -> rec C (-Var x :: D)
| recPI D s t : rec C (-s :: D) -> rec C (+t :: D) -> rec C (+Imp s t :: D)
| recNI D s t : rec C (+s :: -t :: D) -> rec C (-Imp s t :: D).

Fixpoint sizeF s : nat :=
  match s with
    | Imp s1 s2 => 1 + sizeF s1 + sizeF s2
    | _ => 1
  end.

Fixpoint size C : nat :=
  match C with
    | nil => 0
    | +s::C' => sizeF s + size C'
    | -s::C' => sizeF s + size C'
  end.

Definition provider C D : rec C D.
Proof.
  revert D C.
  refine (size_recursion size _).
  intros [|[[x|s t|]|[x|s t|]] D] IH C.
  - constructor.
  - decide (-Var x el C) as [E|E].
    + apply (recPV _ E).
    + apply (recPV' E). apply IH. simpl ; omega.
  - constructor ; apply IH ; simpl ; omega.
  - constructor ; apply IH ; simpl ; omega.
  - decide (+Var x el C) as [E|E].
    + apply (recNV _ E).
    + apply (recNV' E). apply IH. simpl ; omega.
  - constructor ; apply IH ; simpl ; omega.
  - constructor ; apply IH ; simpl ; omega.
Qed.

Refutation lemma

Section RL.
  Variable rho : clause -> Prop.
  Variable Rho : ref_pred rho.

  Definition decider C D :
    rec C D -> solved C ->
    {E | solved E /\ cent E (D ++ C)} + {rho (D ++ C)}.
  Proof.
    intros F G.
    induction F as [C|C D|C D _ IH|C D x F|C D x F _ IH|C D x F|C D x F _ IH|
                    C D s t _ IHs _ IHt|C D s t _ IH] ; simpl.
    - left. exists C. firstorder.
    - right. apply ref_Fal; auto.
    - destruct (IH G) as [[E [F1 F2]]|F].
      + left. exists E. split. exact F1.
        revert F2. unfold cent. simpl. auto.
      + right. revert F. apply ref_weak; auto.
    - right. apply ref_clash with (x:=x); auto.
    - destruct IH as [[E [K1 K2]]|K].
      + apply solved_pos_var; auto.
      + left. exists E. split. exact K1.
        revert K2. apply cent_weak; auto.
      + right. revert K. apply ref_weak; auto.
    - right. apply ref_clash with (x:=x); auto.
    - destruct IH as [[E [K1 K2]]|K].
      + apply solved_neg_var; auto.
      + left. exists E. split. exact K1.
        revert K2. apply cent_weak; auto.
      + right. revert K. apply ref_weak; auto.
    - destruct (IHs G) as [[E [K1 K2]]|K].
      + left. exists E. split. exact K1.
        intros alpha L. apply K2 in L. simpl in *; tauto.
      + destruct (IHt G) as [[E [L1 L2]]|L].
        * left. exists E. split. exact L1.
          intros alpha L. apply L2 in L. simpl in *; tauto.
        * right. apply ref_pos_imp; auto.
    - destruct (IH G) as [[E [K1 K2]]|K].
      + left. exists E. split. exact K1.
        intros alpha L. apply K2 in L. simpl in *. tauto.
      + right. apply ref_neg_imp; auto.
  Qed.

  Lemma solved_ref C :
    {D| solved D /\ cent D C } + {rho C }.
  Proof.
    destruct (decider (provider nil C)) as [[E [F1 F2]]|F].
    - apply solved_nil.
    - left. exists E. revert F2. simpl_list. auto.
    - right. revert F. simpl_list. auto.
  Qed.

  Lemma refutation C :
    {sat C } + {rho C }.
  Proof.
    destruct (solved_ref C) as [[D [F1 F2]]|F];
    eauto using cent_solved_sat.
  Qed.

  Lemma ref_iff_unsat C :
    rho C <-> ~ sat C.
  Proof.
    generalize (ref_sound Rho (C:=C)), (refutation C); tauto.
  Qed.

  Lemma ref_dec C :
    dec (rho C).
  Proof.
    unfold dec.
    generalize (refutation C), (ref_iff_unsat C); tauto.
  Qed.

End RL.

Decidability of classical ND entailment

Lemma satis_pos f A :
  satis' f (map Pos A) <-> forall s, s el A -> satis f s.
Proof.
  induction A; simpl; firstorder; subst; auto.
Qed.

Lemma uns_pos A :
  map uns (map Pos A) = A.
Proof.
  induction A; simpl; congruence.
Qed.

Instance ndc_dec A s :
  dec (ndc A s).
Proof.
  generalize (ref_dec ref_ndc (-s :: map Pos A)).
  simpl. rewrite uns_pos. apply dec_prop_iff.
  symmetry. apply ndc_refute.
Qed.

Agreement of classical ND entailment with boolean entailment

Lemma bent_iff_unsat A s :
  bent A s <-> ~ sat (-s :: map Pos A).
Proof.
  split.
  - intros D [f [E F]]. apply E, (D f). apply satis_pos, F.
  - intros D f E. decide (satis f s) as [F|F]. exact F. exfalso.
    apply D. exists f. split. exact F. apply satis_pos, E.
Qed.

Lemma ndc_iff_sem A s :
  ndc A s <-> bent A s.
Proof.
  rewrite bent_iff_unsat.
  rewrite ndc_refute.
  generalize (ref_iff_unsat ref_ndc (-s :: map Pos A)).
  simpl. rewrite uns_pos.
  auto.
Qed.