(* 命題論理 *) Require Import Bool List Arith Recdef Omega. Definition atom := nat. Definition atom_eq_dec : forall a b : atom, {a=b} + {a<>b} := eq_nat_dec. Notation "x == y" := (atom_eq_dec x y) (at level 70). Lemma atom_eq_refl : forall a, (a == a) = left eq_refl. Proof. induction a; simpl; auto. rewrite IHa. reflexivity. Qed. Inductive prop : Set := | Atom : atom -> prop | Neg : prop -> prop | Conj : prop -> prop -> prop | Disj : prop -> prop -> prop | Imp : prop -> prop -> prop. Definition valuation := atom -> bool. Fixpoint eval (v : valuation) (p : prop) : bool := match p with | Atom a => v a | Neg p1 => negb (eval v p1) | Conj p1 p2 => eval v p1 && eval v p2 | Disj p1 p2 => eval v p1 || eval v p2 | Imp p1 p2 => if eval v p1 then eval v p2 else true end. Definition tautology p := forall v, eval v p = true. Lemma imp_disj : forall p1 p2 v, eval v (Imp p1 p2) = eval v (Disj (Neg p1) p2). Proof. intros. simpl. destruct (eval v p1). reflexivity. reflexivity. Qed. Inductive is_nnf : prop -> Prop := | nnfAtom : forall a, is_nnf (Atom a) | nnfNegAtom : forall a, is_nnf (Neg (Atom a)) | nnfConj : forall p1 p2, is_nnf p1 -> is_nnf p2 -> is_nnf (Conj p1 p2) | nnfDisj : forall p1 p2, is_nnf p1 -> is_nnf p2 -> is_nnf (Disj p1 p2). Fixpoint nnf_sz (p : prop) := match p with | Atom a => 1 | Neg p1 => 1 + nnf_sz p1 + nnf_sz p1 | Conj p1 p2 => 2 + nnf_sz p1 + nnf_sz p2 | Disj p1 p2 => 2 + nnf_sz p1 + nnf_sz p2 | Imp p1 p2 => 3 + nnf_sz p1 + nnf_sz p1 + nnf_sz p2 (* Disj (Neg p1) p2 *) end. Function nnf (p : prop) {measure nnf_sz p} : prop := match p with | Atom a => Atom a | Neg (Atom a) => Neg (Atom a) | Neg (Neg p1) => nnf p1 | Neg (Conj p1 p2) => nnf (Disj (Neg p1) (Neg p2)) | Neg (Disj p1 p2) => nnf (Conj (Neg p1) (Neg p2)) | Neg (Imp p1 p2) => nnf (Conj p1 (Neg p2)) | Conj p1 p2 => Conj (nnf p1) (nnf p2) | Disj p1 p2 => Disj (nnf p1) (nnf p2) | Imp p1 p2 => Disj (nnf (Neg p1)) (nnf p2) end. simpl; intros; omega. simpl; intros; omega. simpl; intros; omega. simpl; intros; omega. simpl; intros; omega. simpl; intros; omega. simpl; intros; omega. simpl; intros; omega. simpl; intros; omega. simpl; intros; omega. Defined. Hint Constructors is_nnf. Theorem nnf_is_nnf : forall p, is_nnf (nnf p). Proof. intros. functional induction (nnf p); auto. Qed. Hint Resolve nnf_is_nnf. Theorem nnf_correct : forall p v, eval v (nnf p) = eval v p. Proof. intros. functional induction (nnf p); simpl; intros; try (rewrite IHp0; simpl); try (destruct (eval v p1)); auto. Qed. Inductive lit : Set := | Posi : atom -> lit | Nega : atom -> lit. Definition clause := list lit. Fixpoint eval_lit (v : valuation) l := match l with | Posi a => v a | Nega a => negb (v a) end. Check fold_left. Fixpoint eval_clause (v : valuation) (l : clause) : bool := match l with | nil => false | x :: l' => eval_lit v x || eval_clause v l' end. Fixpoint eval_cnf (v : valuation) (l : list clause) : bool := match l with | nil => true | d :: l' => eval_clause v d && eval_cnf v l' end. Fixpoint neg_lit x := match x with | Posi a => Nega a | Nega a => Posi a end. Fixpoint disj (l1 l2 : list clause) := match l1 with | nil => nil | c1 :: l => map (fun c2 => c1 ++ c2) l2 ++ disj l l2 end. Fixpoint cnf (p : prop) : list clause := match p with | Atom a => (Posi a :: nil) :: nil | Neg p1 => map (map neg_lit) (cnf p1) (* 一点集合のみ *) | Conj p1 p2 => cnf p1 ++ cnf p2 | Disj p1 p2 => disj (cnf p1) (cnf p2) | Imp p1 p2 => nil (* nnf にはない *) end. Lemma eval_clause_app : forall v c1 c2, eval_clause v (c1 ++ c2) = eval_clause v c1 || eval_clause v c2. Proof. intros; induction c1; simpl in *; auto. rewrite IHc1. rewrite orb_assoc; auto. Qed. Lemma eval_cnf_app : forall v l1 l2, eval_cnf v (l1 ++ l2) = eval_cnf v l1 && eval_cnf v l2. Proof. intros; induction l1; simpl in *; auto. rewrite IHl1. rewrite andb_assoc. auto. Qed. Lemma disj_correct : forall v l1 l2, eval_cnf v (disj l1 l2) = eval_cnf v l1 || eval_cnf v l2. Proof. intros. induction l1; simpl. reflexivity. rewrite eval_cnf_app. rewrite orb_andb_distrib_l. rewrite IHl1. replace (eval_cnf v (map (fun c2 : list lit => a ++ c2) l2)) with (eval_clause v a || eval_cnf v l2). reflexivity. clear. induction l2; simpl. destruct eval_clause; auto. rewrite orb_andb_distrib_r. rewrite IHl2. rewrite eval_clause_app. reflexivity. Qed. Theorem cnf_correct : forall v p, is_nnf p -> eval_cnf v (cnf p) = eval v p. Proof. induction 1; simpl. destruct (v a); reflexivity. destruct (v a); reflexivity. rewrite eval_cnf_app. congruence. rewrite disj_correct. congruence. Qed. Definition lit_eq_dec : forall a b : lit, {a=b}+{a<>b}. pose atom_eq_dec. decide equality. Defined. Print lit_eq_dec. Fixpoint tauto_clause (c : clause) := match c with | nil => false | a :: c' => if In_dec lit_eq_dec (neg_lit a) c then true else tauto_clause c' end. Fixpoint tauto_cnf (l : list clause) := match l with | nil => true | c :: l' => tauto_clause c && tauto_cnf l' end. Lemma eval_neg_lit : forall v a, eval_lit v (neg_lit a) = negb (eval_lit v a). Proof. intros. destruct a; simpl. auto. destruct (v a); auto. Qed. Lemma eval_clause_true : forall v a c, In a c -> eval_lit v a = true -> eval_clause v c = true. Proof. induction c; simpl; intros. elim H. case_eq (eval_lit v a0); intros. auto. destruct H. subst. rewrite H0 in H1; discriminate. simpl. auto. Qed. Definition atom_lit l := match l with | Posi a => a | Nega a => a end. Definition neg_val v a : {v' | eval_lit v' a = false /\ forall b, b <> atom_lit a -> v' b = v b}. destruct a; [ exists (fun x => if x == a then false else v x) | exists (fun x => if x == a then true else v x) ]; simpl; (split; intros; [destruct (a == a) | destruct (b == a)]; intuition). Restart. destruct a. exists (fun x => if x == a then false else v x). simpl; split; intros. destruct (a == a); intuition. destruct (b == a); intuition. exists (fun x => if x == a then true else v x). simpl; split; intros. destruct (a == a); intuition. destruct (b == a); intuition. Restart. Lemma atom_eq_cpl : forall a b (h: a <> b), a == b = right (match a == b with left _ => h | right h => h end). Proof. intros. destruct (a == b). elim h; auto. auto. Qed. destruct a; [ exists (fun x => if x == a then false else v x) | exists (fun x => if x == a then true else v x) ]; simpl; split; intros; try rewrite atom_eq_refl; try rewrite (atom_eq_cpl _ _ H); auto. Defined. Lemma tauto_clause_ok : forall c, tauto_clause c = true <-> (forall v, eval_clause v c = true). Proof. induction c; simpl. split; intros; auto. apply H. exact (fun x => true). destruct lit_eq_dec. destruct a; discriminate. destruct In_dec. split; intros; auto. case_eq (eval_lit v a); intros. auto. simpl. apply (eval_clause_true _ _ _ i). rewrite eval_neg_lit. rewrite H0. auto. split; intros. destruct (eval_lit v a); simpl; intuition. apply <- IHc. intros. destruct (neg_val v a) as [v' [v'_a v'_other]]. specialize (H v'). rewrite v'_a in H. simpl in H. clear IHc n. induction c; simpl in *; auto. case_eq (eval_lit v a0); intros. auto. apply IHc. intuition. destruct (atom_eq_dec (atom_lit a0) (atom_lit a)). destruct a0; destruct a; simpl in *; try discriminate; subst; try rewrite v'_a in *; auto. destruct a0; simpl in *; rewrite v'_other, H0 in H; auto. Qed. Lemma tauto_cnf_lem : forall l, tauto_cnf l = true <-> forall v, eval_cnf v l = true. Proof. induction l; simpl. split; auto. split. case_eq (tauto_clause a); simpl; intros. rewrite (proj1 (tauto_clause_ok _) H). simpl. apply -> IHl. auto. discriminate. intros. rewrite (proj2 (tauto_clause_ok _)). simpl. apply <- IHl. intros. specialize (H v). destruct (eval_clause v a); auto. discriminate. intros. specialize (H v). destruct eval_clause; auto. Qed. Theorem tauto_cnf_ok : forall p, tautology p <-> tauto_cnf (cnf (nnf p)) = true. Proof. unfold tautology. intros. destruct (tauto_cnf_lem (cnf (nnf p))). split; intros. apply H0. intros. rewrite cnf_correct, nnf_correct; auto. rewrite <- nnf_correct, <- cnf_correct; auto. Qed. (* 証明論 *) Definition hypotheses := list prop. Notation tt := (Disj (Atom 0) (Neg (Atom 0))). (* 透明な定義 *) Notation ff := (Conj (Atom 0) (Neg (Atom 0))). (* 証明の判定 *) Reserved Notation "h |- p" (at level 69). (* 証明の定義 *) Inductive provable : hypotheses -> prop -> Prop := | AxiomI : forall h p, In p h -> h |- p | ImpI : forall h p1 p2, p1 :: h |- p2 -> h |- (Imp p1 p2) | ImpE : forall p1 h p2, h |- p1 -> h |- Imp p1 p2 -> h |- p2 | ConjI : forall h p1 p2, h |- p1 -> h |- p2 -> h |- Conj p1 p2 | ConjE1 : forall p2 h p1, h |- Conj p1 p2 -> h |- p1 | ConjE2 : forall p1 h p2, h |- Conj p1 p2 -> h |- p2 | DisjI1 : forall h p1 p2, h |- p1 -> h |- Disj p1 p2 | DisjI2 : forall h p1 p2, h |- p2 -> h |- Disj p1 p2 | DisjE : forall p1 p2 h q, h |- Disj p1 p2 -> p1 :: h |- q -> p2 :: h |- q -> h |- q | NegI : forall q h p, p :: h |- q -> p :: h |- Neg q -> h |- Neg p | NegE : forall h p, h |- Neg (Neg p) -> h |- p where "h |- p" := (provable h p). (* 先に定義した記法を使う *) (* 仮定を満たす割り当て *) Definition validates v h := forall p, In p h -> eval v p = true. (* 論理的帰結 *) Definition consequence h p := forall v, validates v h -> eval v p = true. (* 証明論の健全性 *) Theorem soundness : forall p h, h |- p -> consequence h p. Proof. unfold consequence. unfold validates. intros. induction H. (* AxiomI *) auto. (* ImpI *) simpl. case_eq (eval v p1); intros. apply IHprovable. simpl; intros. destruct H2. subst; auto. auto. auto. (* ImpE *) simpl in *. rewrite IHprovable1 in IHprovable2; auto. (* ConjI *) simpl. rewrite IHprovable1; auto. (* ConjE1 *) simpl in *. specialize (IHprovable H0). destruct (eval v p1). auto. discriminate. (* ConjE2 *) simpl in *. specialize (IHprovable H0). destruct (eval v p1). auto. discriminate. (* DisjI1 *) simpl. rewrite IHprovable; auto. (* DisjI2 *) simpl. rewrite IHprovable; auto with bool. (* DisjE *) simpl in *. case_eq (eval v p1); intros. apply IHprovable2. intros. destruct H4; auto. subst. auto. rewrite H3 in IHprovable1. apply IHprovable3. intros. destruct H4; auto. subst. auto. (* NegI *) simpl in *. case_eq (eval v p); intros; auto. rewrite <- IHprovable1 at 1. apply IHprovable2. intros. destruct H3; auto. subst. auto. intros. destruct H3; auto. subst. auto. (* NegE *) simpl in *. destruct (eval v p); auto. Qed. (* 完全性も証明する *) (* provable をautoのヒントにする *) Hint Constructors provable. (* 特殊なヒント:ゴールが以下の形の時に、右の作戦で解こうとする *) Hint Extern 2 (_ :: _ |- _) => try solve [apply AxiomI; simpl; auto]. (* 前提を強くしても証明が可能 *) Theorem weakening : forall h1 h2 h3 p, h1++h2 |- p -> h1++h3++h2 |- p. Proof. intros. remember (h1++h2) as h. revert h1 h2 Heqh. induction H; intros; subst; auto. (* AxiomI *) apply AxiomI. apply in_or_app. destruct (in_app_or _ _ _ H); auto. right. apply in_or_app; auto. (* ImpI *) apply ImpI. apply (IHprovable (p1::h1) h2). reflexivity. (* ImpE *) eapply ImpE; try apply IHprovable1; auto. (* ConjE1 *) eapply ConjE1. apply IHprovable; auto. (* ConjE2 *) eapply ConjE2. apply IHprovable; auto. (* DisjE *) eapply DisjE. eauto. apply (IHprovable2 (p1::h1) h2); auto. apply (IHprovable3 (p2::h1) h2); auto. (* NegI *) eapply NegI. apply (IHprovable1 (p::h1) h2); auto. apply (IHprovable2 (p::h1) h2); auto. Qed. (* よく使う特殊な場合 *) Corollary weakening_head : forall p h p', h |- p' -> p::h |- p'. Proof. intros. apply (weakening nil h (p::nil) _ H). Qed. Hint Resolve weakening_head. (* tt と ff *) Lemma excluded_middle : forall h p, h |- Disj p (Neg p). Proof. intros. apply NegE. apply (NegI p). apply NegE. apply (NegI (Disj p (Neg p))); auto. apply (NegI (Disj p (Neg p))); auto. Qed. Hint Resolve excluded_middle. Lemma ex_falso : forall p q h, h |- Conj p (Neg p) -> h |- q. Proof. intros. apply NegE. apply (NegI p). apply (ConjE1 (Neg p)). auto. apply (ConjE2 p). auto. Qed. (* nnf への変換が証明可能性を保存する *) Lemma provable_nnf : forall p h, h |- p <-> h |- nnf p. Proof. intro. functional induction (nnf p); simpl; split; intros; auto; try apply -> IHp0; try apply <- IHp0 in H. (* 1 *) auto. (* 2 *) apply (NegI p1). destruct (IHp0 h); auto. auto. (* 3 *) apply NegE. apply (NegI (Conj p1 p2)); auto. apply ConjI. apply NegE. apply (NegI (Disj (Neg p1) (Neg p2))); auto. apply NegE. apply (NegI (Disj (Neg p1) (Neg p2))); auto. (* 4 *) apply (DisjE _ _ _ _ H). apply (NegI p1); auto. apply (ConjE1 p2); auto. apply (NegI p2); auto. apply (ConjE2 p1); auto. (* 5 *) apply ConjI. apply (NegI (Disj p1 p2)); auto. apply (NegI (Disj p1 p2)); auto. (* 6 *) apply (NegI (Conj (Neg p1) (Neg p2))); auto. apply (DisjE p1 p2); auto. apply (NegI p1); auto. apply (ConjE1 (Neg p2)); auto. apply (NegI p2); auto. apply (ConjE2 (Neg p1)); auto. (* 7 *) apply ConjI. apply NegE. apply (NegI (Imp p1 p2)); auto. apply ImpI. apply NegE. apply (NegI p1); auto. apply (NegI (Imp p1 p2)); auto. (* 8 *) apply (NegI p2). apply (ImpE p1); auto. apply (ConjE1 (Neg p2)); auto. apply (ConjE2 p1); auto. (* 9 *) apply ConjI. apply -> IHp0. apply (ConjE1 _ _ _ H). apply -> IHp1. apply (ConjE2 _ _ _ H). (* 10 *) apply ConjI. apply <- IHp0. apply (ConjE1 _ _ _ H). apply <- IHp1. apply (ConjE2 _ _ _ H). (* 11 *) apply (DisjE _ _ _ _ H). apply DisjI1. apply -> IHp0; auto. apply DisjI2. apply -> IHp1; auto. (* 12 *) apply (DisjE _ _ _ _ H). apply DisjI1. apply <- IHp0; auto. apply DisjI2. apply <- IHp1; auto. (* 13 *) apply NegE. apply (NegI p2). apply (ImpE p1); auto. apply NegE. apply (NegI (Disj (nnf (Neg p1)) (nnf p2))). apply DisjI1. apply -> IHp0; auto. auto. apply (NegI (Disj (nnf (Neg p1)) (nnf p2))). apply DisjI2. apply -> IHp1; auto. auto. (* 14 *) apply ImpI. apply (DisjE (nnf (Neg p1)) (nnf p2)). auto. apply NegE. apply (NegI p1). auto. apply <- IHp0; auto. apply <- IHp1; auto. Qed. (* Clause に関する完全性 *) Parameter true_clause : forall h, tauto_clause h = true -> exists b, In (Posi b) h /\ In (Nega b) h. Fixpoint prop_of_lit (l : lit) := match l with | Posi a => Atom a | Nega a => Neg (Atom a) end. Definition prop_of_clause := fold_right (fun x => Disj (prop_of_lit x)) ff. Definition prop_of_cnf := fold_right (fun x => Conj (prop_of_clause x)) tt. Theorem prop_of_cnf_ok : forall v c, eval_cnf v c = eval v (prop_of_cnf c). Admitted. Lemma provable_clause : forall a c h, In a c -> In (prop_of_lit a) h -> h |- prop_of_clause c. Admitted. (* CNF の clause 表記に関する完全性 *) Lemma completeness_cnf : forall p, (forall v, eval_cnf v p = true) -> nil |- prop_of_cnf p. Proof. intros p CSQ. induction p; simpl in *. admit. apply ConjI. destruct (true_clause a) as [b [Hb Hnegb]]. Admitted. (* 必要な補題 *) Parameter provable_clause_weaken_l : forall b a h, h |- prop_of_clause a -> h |- prop_of_clause (b ++ a). Parameter provable_clause_weaken_r : forall b a h, h |- prop_of_clause a -> h |- prop_of_clause (a ++ b). Parameter provable_cnf_app : forall c1 c2 h, h |- prop_of_cnf c1 -> h |- prop_of_cnf c2 -> h |- prop_of_cnf (c1 ++ c2). Parameter provable_cnf_app_inv : forall c1 c2 h, h |- prop_of_cnf (c1 ++ c2) -> h |- prop_of_cnf c1 /\ h |- prop_of_cnf c2. Parameter prop_of_clause_app_inv : forall c1 c2 h, h |- prop_of_clause (c1 ++ c2) -> h |- Disj (prop_of_clause c1) (prop_of_clause c2). Parameter provable_cnf_weaken_l : forall a h f, h |- prop_of_cnf f -> h |- prop_of_cnf (map (fun c => a ++ c) f). Parameter provable_cnf_weaken_r : forall a h f, h |- prop_of_cnf f -> h |- prop_of_cnf (map (fun c => c ++ a) f). Parameter provable_cnf_disj_l : forall c1 c2 h, h |- prop_of_cnf c1 -> h |- prop_of_cnf (disj c1 c2). Parameter provable_cnf_disj_r : forall c1 c2 h, h |- prop_of_cnf c2 -> h |- prop_of_cnf (disj c1 c2). Parameter provable_disj_conj : forall a b c h, h |- Conj (Disj a c) (Disj b c) <-> h |- Disj (Conj a b) c. Parameter provable_cnf_distr : forall a h f, h |- prop_of_cnf (map (fun c : list lit => a ++ c) f) -> h |- Disj (prop_of_clause a) (prop_of_cnf f). (* 論理和の証明の逆変換 *) Lemma provable_cnf_disj : forall c1 c2 h, h |- prop_of_cnf (disj c1 c2) -> h |- Disj (prop_of_cnf c1) (prop_of_cnf c2). Admitted. (* CNFでの証明の逆変換 *) Lemma provable_cnf : forall h p, is_nnf p -> h |- prop_of_cnf (cnf p) -> h |- p. Proof. intros h p Hnnf. revert h. induction Hnnf; simpl; intros. Admitted. (* 完全性 *) Theorem completeness : forall p, tautology p -> nil |- p. Proof. intros. apply <- provable_nnf. apply provable_cnf; auto. apply completeness_cnf. intros. rewrite cnf_correct, nnf_correct; auto. Qed. Corollary provable_dec : forall p, {nil |- p}+{~nil |- p}. Admitted.