Require Export PropL. (** * 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). Instance eq_sform_dec S T : dec (S = T :> sform). Proof. unfold dec. repeat decide equality. Qed. Definition positive (S : sform) : Prop := match S with +s => True | -s => False end. Fixpoint pos (C : clause) : clause := match C with | nil => nil | + s :: C' => + s :: pos C' | - s :: C' => pos C' end. Lemma pos_iff S C : S el pos C <-> S el C /\ positive S. Proof. revert S. induction C as [|T C]. - simpl. tauto. - intros S. specialize (IHC S). destruct T as [t|t] ; split ; simpl. + intros [E|E] ; subst ; simpl ; tauto. + intros [[E|E] F] ; subst ; simpl ; tauto. + tauto. + intros [[E|E] F] ; subst ; simpl in F ; tauto. Qed. Lemma pos_mono C D : C <<= D -> pos C <<= pos D. Proof. intros E S F. apply pos_iff in F as [F F']. apply pos_iff. auto. Qed. Lemma pos_idempotent C : pos (pos C) = pos C. Proof. induction C as [|S C]. reflexivity. destruct S as [s|s] ; simpl ; congruence. Qed. Lemma pos_incl C : pos C <<= C. Proof. intros S F. apply pos_iff in F. apply F. Qed. Lemma pos_incl_pos A B : pos A <<= B -> pos A <<= pos B. Proof. intros E. intros S F. apply pos_iff. split. - auto. - apply pos_iff in F. apply F. Qed. (** * Models and satisfaction We consider finite Kripke models whose states are clauses. There is a transition from A to B iff all positive formulas in A are in B. A state is labelled with a variable x if it contains the signed formula +x. We will show that nd is sound and complete for this class of models. *) Definition state := clause. Definition model := list state. Section Model. Variable M : model. Implicit Types A B C : state. Definition before (A B : state) : Prop := A el M /\ B el M /\ pos A <<= B. Lemma before_refl A : A el M -> before A A. Proof. unfold before. intuition. apply pos_incl. Qed. Lemma before_tran A B C : before A B -> before B C -> before A C. Proof. intros [F [_ G]] [_ [H K]]. unfold before. intuition. setoid_rewrite <- K. apply pos_incl_pos, G. Qed. Lemma before_in s A B : before A B -> +s el A -> +s el B. Proof. intros [_ [_ E]] F. apply E. apply pos_iff. simpl. auto. Qed. Fixpoint satis (A : state) (s : form) : Prop := match s with | Var x => +Var x el A | Imp s t => forall B, before A B -> satis B s -> satis B t | Fal => False end. Lemma satis_not A s : A el M -> satis A (Not s) -> ~ satis A s. Proof. simpl. intros E F G. apply (F A (before_refl E) G). Qed. Lemma satis_mono A B s : before A B -> satis A s -> satis B s. Proof. intros F G. destruct s as [x|s1 s2|] ; simpl in *. - apply (before_in F G). - intros E H. apply G. apply (before_tran F H). - exact G. Qed. Fixpoint satis' (A : state) (C : clause) : Prop := match C with | nil => True | +s :: C' => satis A s /\ satis' A C' | -s :: C' => ~ satis A s /\ satis' A C' end. Lemma satis_iff A C : satis' A C <-> forall S, S el C -> match S with | +s => satis A s | -s => ~ satis A s end. Proof. induction C as [|S C] ; simpl. - firstorder. - split. + intros E T [F|F]. * subst T. destruct S ; tauto. * apply IHC ; [|exact F]. destruct S ; tauto. + intros E. assert (F : satis' A C). * apply IHC. intros T F. apply E. auto. * specialize (E S). destruct S ; subst ; tauto. Qed. Lemma satis_in A C S : satis' A C -> S el C -> match S with | +s => satis A s | -s => ~ satis A s end. Proof. intros E. apply satis_iff, E. Qed. Lemma satis_weak C D A : C <<= D -> satis' A D -> satis' A C. Proof. intros E F. apply satis_iff. intros S G. apply (satis_iff A D) ; auto. Qed. Global Instance before_forall_dec A p : (forall B, dec (p B)) -> dec (forall B, before A B -> p B). Proof. intros D. apply dec_prop_iff with (X:= forall B, B el M -> A el M -> pos A <<= B -> p B). - unfold before. firstorder. - decide claim. Qed. Global Instance satis_dec A s : dec (satis A s). Proof. revert A. induction s ; intros A ; simpl ; decide claim. Qed. End Model. (** * Semantic entailment and soundness *) Definition sem (A : context) (s : form) : Prop := forall M B, B el M -> (forall t, t el A -> satis M B t) -> satis M B s. Lemma nd_sem A s : nd A s -> sem A s. Proof. intros E M. induction E as [A s E|A s t _ IH|A s t _ IH _ IHs|A s _ IH] ; intros B F G ; simpl. - auto. - intros C H K. apply IH. now apply H. intros u [[]|L]. exact K. apply (satis_mono H). auto. - specialize (IH B F G). simpl in IH. apply IH. + apply before_refl, F. + auto. - contradiction (IH B F G). Qed. (** * Satisfiability *) Definition sat (C : clause) : Prop := exists M A, A el M /\ satis' M A C. Lemma sat_weak C D : C <<= D -> sat D -> sat C. Proof. intros E [ M [A [F G]]]. exists M. exists A. split. exact F. apply (satis_weak E G). Qed. Lemma sem_unsat A s : sem A s -> ~ sat (-s :: map Pos A). Proof. intros D [M [B [E [F G]]]]. apply F, D. exact E. intros t H. apply (satis_in (S:=+t) G). apply in_map, H. Qed. Lemma sem_iff_unsat A s : sem A s <-> ~ sat (-s :: map Pos A). Proof. split. now apply sem_unsat. intros D M B E F. decide (satis M B s) as [G|G]. exact G. exfalso. apply D. exists M, B. simpl. intuition. clear s D G. induction A as [|s A] ; simpl ; auto. Qed. (** * Demos A demo is a model satisfying certain consistency properties. We will show that every state A of a demo satifies every positive formula in A and dissatifies every negative formula in A. *) Definition demo' (M : model) (A : clause) (S : sform) : Prop := match S with | - Var x => ~ +Var x el A | + Imp s t => -s el A \/ +t el A | - Imp s t => exists B, before M A B /\ +s el B /\ -t el B | + Fal => False | _ => True end. Definition demo (M : model) : Prop := forall A, A el M -> forall S, S el A -> demo' M A S. Definition sign (b : bool) := if b then Pos else Neg. Lemma demo_satis M A b s : demo M -> A el M -> sign b s el A -> if b then satis M A s else ~ satis M A s. Proof. intros E. revert A b. induction s as [x|s IHs t IHt|] ; intros A [|] F G ; hnf ; simpl in G. - exact G. - intros H. simpl in H. exact (E A F (-Var x) G H). - intros B H K. apply (before_in H) in G. destruct H as [_ [H _]]. destruct (E B H _ G) as [L|L]. + exfalso. apply (IHs B false H) in L. tauto. + apply (IHt B true H) in L. exact L. - intros H. destruct (E A F _ G) as [B [K [L N]]]. hnf in H. specialize (H B K). destruct K as [_ [K _]]. apply (IHs B true K) in L. apply (IHt B false K) in N. tauto. - apply (E A F _ G). - simpl ; auto. Qed. Lemma demo_satis' M A : demo M -> A el M -> satis' M A A. Proof. intros E F. apply satis_iff. intros [s|s] G. - apply (demo_satis (b:=true) E F G). - apply (demo_satis (b:=false) E F G). Qed. (** * Intuitionistic ND cannot prove double negation *) Definition DN x := Imp (Not (Not (Var x))) (Var x). Section ND_not_DN. Variable x : var. Let A := [-DN x; + Not (Not (Var x)); - Not (Var x); -Var x]. Let B := [+ Not (Not (Var x)); - Not (Var x); +Var x; -Fal]. Let M := [A; B]. Let D : demo M. intros C E S F. destruct E as [E|E]. - subst C. repeat destruct F as [F|F] ; subst ; simpl in * ; auto ; try contradiction F. + exists A. firstorder. + exists B. firstorder. + intros F. repeat (destruct F as [F|F] ; [discriminate F|]). exact F. - apply in_sing in E ; subst C. repeat destruct F as [F|F] ; subst ; simpl in * ; auto ; try contradiction F. + exists B. firstorder. Qed. Lemma not_nd_DN : ~ nd nil (DN x). Proof. intros F. assert (G: A el M) by firstorder. assert (H: -DN x el A) by firstorder. apply (demo_satis (b:=false) D G H). apply (nd_sem F). exact G. intros t []. Qed. End ND_not_DN. (** * Tableaux *) Inductive tab : clause -> Prop := | tabF C : tab (+Fal :: C) | tabC (x : var) C : tab (-Var x :: +Var x :: C) | tabIP s t C : tab (-s :: C) -> tab (+ t :: C) -> tab (+Imp s t :: C) | tabIN s t C : tab (+s :: -t :: pos C) -> tab (-Imp s t :: C) | tabW C C' : C' <<= C -> tab C' -> tab C. Definition uns (S : sform) : form := match S with +s => s | -s => Not s end. Definition ndr (C : clause) : Prop := nd (map uns (pos C)) Fal \/ exists s, -s el C /\ nd (map uns (pos C)) s. Lemma tab_ndr C : tab C -> ndr C. Proof. intros E. induction E as [C|x C|s t C _ IH1 _ IH2|s t C _ IH|C C' F _ IH] ; simpl in *. - left. apply ndA. left. reflexivity. - right. exists (Var x). simpl. intuition. apply ndA. auto. - destruct IH1 as [E1|[u [E1 E1']]]. + left. apply ndW, E1. + destruct E1 as [E1|E1]. * { injection E1. clear E1. intros E1. subst. destruct IH2 as [E2|[v [[E2|E2] E2']]]. - left. simpl. apply ndIE_weak with (s:=t) (B:= map uns (pos C)). + apply ndII, E2. + auto. + apply ndapp1. apply ndW, E1'. - discriminate E2. - right. simpl in *. exists v. intuition. apply ndIE_weak with (s:=t) (B:= map uns (pos C)). + apply ndII, E2'. + auto. + apply ndapp1. apply ndW, E1'. } * right. exists u. split. now auto. apply ndW, E1'. - right. exists (Imp s t). simpl. split. now auto. apply ndII. unfold ndr in IH. simpl in IH. rewrite pos_idempotent in IH. destruct IH as [E|[u [[E|[E|E]] E']]]. + apply ndE, E. + discriminate E. + congruence. + apply pos_iff in E. destruct E as [_ []]. - assert (F' := incl_map (f := uns) (pos_mono F)). destruct IH as [E|[s [E E']]]. + left. apply (nd_weak F' E). + right. exists s. intuition. apply (nd_weak F' E'). Qed. Lemma uns_Pos A : map uns (map Pos A) = A. Proof. induction A ; simpl ; congruence. Qed. Lemma pos_map_Pos A : pos (map Pos A) = map Pos A. Proof. induction A ; simpl ; congruence. Qed. Lemma tab_nd A s : tab (-s :: map Pos A) -> nd A s. Proof. intros D. apply tab_ndr in D. unfold ndr in D. simpl in D. rewrite pos_map_Pos, uns_Pos in D. destruct D as [D|[t [D E]]]. + apply ndE, D. + destruct D as [D|D]. * injection D. congruence. * apply in_map_iff in D as [u [D _]]. discriminate D. Qed. (** * Main results assuming main lemma *) Section MainResults. Variable main : forall C, {sat C} + {tab C}. Lemma nd_plus_not_sem A s : {nd A s} + {~ sem A s}. Proof. destruct (main (-s :: map Pos A)) as [E|E]. - right. intros F. contradiction (sem_unsat F E). - left. apply tab_nd, E. Qed. Lemma nd_dec A s : dec (nd A s). Proof. destruct (nd_plus_not_sem A s) as [E|E]. - left. exact E. - right. intros B. apply E, nd_sem, B. Qed. Lemma nd_iff_sem A s : nd A s <-> sem A s. Proof. split. - apply nd_sem. - intros E. destruct (nd_plus_not_sem A s) as [F|F]. + exact F. + contradiction (F E). Qed. End MainResults.