1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "nat/plus.ma".
16 include "nat/compare.ma".
17 include "list/sort.ma".
18 include "datatypes/constructors.ma".
20 inductive Formula : Type ≝
23 | FAtom: nat → Formula
24 | FAnd: Formula → Formula → Formula
25 | FOr: Formula → Formula → Formula
26 | FNot: Formula → Formula.
28 definition interp ≝ nat → bool.
30 let rec eval (interp:interp) F on F : bool ≝
35 | FAnd f1 f2 ⇒ eval interp f1 ∧ eval interp f2
36 | FOr f1 f2 ⇒ eval interp f1 ∨ eval interp f2
37 | FNot f ⇒ ¬ eval interp f
40 inductive not_nf : Formula → Prop ≝
42 | NFalse: not_nf FFalse
43 | NAtom: ∀n. not_nf (FAtom n)
44 | NAnd: ∀f1,f2. not_nf f1 → not_nf f2 → not_nf (FAnd f1 f2)
45 | NOr: ∀f1,f2. not_nf f1 → not_nf f2 → not_nf (FOr f1 f2)
46 | NNot: ∀n.not_nf (FNot (FAtom n)).
52 | FAtom n ⇒ FNot (FAtom n)
53 | FAnd f1 f2 ⇒ FOr (negate f1) (negate f2)
54 | FOr f1 f2 ⇒ FAnd (negate f1) (negate f2)
55 | FNot f ⇒ elim_not f]
61 | FAnd f1 f2 ⇒ FAnd (elim_not f1) (elim_not f2)
62 | FOr f1 f2 ⇒ FOr (elim_not f1) (elim_not f2)
66 theorem not_nf_elim_not: ∀F.not_nf (elim_not F) ∧ not_nf (negate F).
69 [1,2,3: simplify; autobatch
84 theorem demorgan1: ∀b1,b2:bool. (¬ (b1 ∧ b2)) = ¬ b1 ∨ ¬ b2.
91 theorem demorgan2: ∀b1,b2:bool. (¬ (b1 ∨ b2)) = ¬ b1 ∧ ¬ b2.
98 theorem eq_notb_notb_b_b: ∀b:bool. (¬ ¬ b) = b.
104 theorem eq_eval_elim_not_eval:
105 ∀i,F. eval i (elim_not F) = eval i F ∧ eval i (negate F) = eval i (FNot F).
108 [1,2,3: split; reflexivity
115 |replace with ((eval i (FNot f) ∨ eval i (FNot f1)) = ¬ (eval i f ∧ eval i f1));
120 |replace with ((eval i (FNot f) ∧ eval i (FNot f1)) = ¬ (eval i f ∨ eval i f1));
129 | change with (eval i (elim_not f) = ¬ ¬ eval i f);
135 definition sequent ≝ (list Formula) × (list Formula).
137 inductive derive: sequent → Prop ≝
138 ExchangeL: ∀l,l1,l2,f. derive 〈f::l1@l2,l〉 → derive 〈l1 @ [f] @ l2,l〉
139 | ExchangeR: ∀l,l1,l2,f. derive 〈l,f::l1@l2〉 → derive 〈l,l1 @ [f] @ l2〉
140 | Axiom: ∀l1,l2,f. derive 〈f::l1, f::l2〉
141 | TrueR: ∀l1,l2. derive 〈l1,FTrue::l2〉
142 | FalseL: ∀l1,l2. derive 〈FFalse::l1,l2〉
143 | AndR: ∀l1,l2,f1,f2.
144 derive 〈l1,f1::l2〉 → derive 〈l1,f2::l2〉 →
145 derive 〈l1,FAnd f1 f2::l2〉
146 | AndL: ∀l1,l2,f1,f2.
147 derive 〈f1 :: f2 :: l1,l2〉 → derive 〈FAnd f1 f2 :: l1,l2〉
149 derive 〈f1::l1,l2〉 → derive 〈f2::l1,l2〉 →
150 derive 〈FOr f1 f2 :: l1,l2〉
152 derive 〈l1,f1 :: f2 :: l2〉 → derive 〈l1,FOr f1 f2 :: l2〉
154 derive 〈f::l1,l2〉 → derive 〈l1,FNot f :: l2〉
156 derive 〈l1,f::l2〉 → derive 〈FNot f :: l1,l2〉.
158 let rec and_of_list l ≝
161 | cons F l' ⇒ FAnd F (and_of_list l')
164 let rec or_of_list l ≝
167 | cons F l' ⇒ FOr F (or_of_list l')
170 definition formula_of_sequent ≝
171 λs.match s with [pair l1 l2 ⇒ FOr (FNot (and_of_list l1)) (or_of_list l2)].
173 definition is_tautology ≝
174 λF. ∀i. eval i F = true.
176 axiom assoc_orb: associative ? orb.
177 axiom symm_orb: symmetric ? orb.
178 axiom orb_not_b_b: ∀b:bool. (¬b ∨ b) = true.
179 axiom distributive_orb_andb: distributive ? orb andb.
180 axiom symm_andb: symmetric ? andb.
181 axiom associative_andb: associative ? andb.
182 axiom distributive_andb_orb: distributive ? andb orb.
184 lemma andb_true: ∀x.(true ∧ x) = x. intro; reflexivity. qed.
186 lemma and_of_list_permut:
187 ∀i,f,l1,l2. eval i (and_of_list (l1 @ (f::l2))) = eval i (and_of_list (f :: l1 @ l2)).
194 autobatch paramodulation
198 lemma or_of_list_permut:
199 ∀i,f,l1,l2. eval i (or_of_list (l1 @ (f::l2))) = eval i (or_of_list (f :: l1 @ l2)).
206 autobatch paramodulation
210 theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
213 [ simplify in H2 ⊢ %;
215 lapply (H2 i); clear H2;
216 rewrite > and_of_list_permut;
219 | simplify in H2 ⊢ %;
221 lapply (H2 i); clear H2;
222 rewrite > or_of_list_permut;
229 rewrite > assoc_orb in ⊢ (? ? (? % ?) ?);
230 rewrite > symm_orb in ⊢ (? ? (? (? ? %) ?) ?);
232 rewrite > orb_not_b_b;
241 | simplify in H2 H4 ⊢ %;
243 lapply (H2 i); clear H2;
244 lapply (H4 i); clear H4;
245 rewrite > symm_orb in ⊢ (? ? (? ? %) ?);
246 rewrite > distributive_orb_andb;
250 autobatch paramodulation
251 by distributive_orb_andb,symm_orb,symm_orb,
252 Hletin, Hletin1,andb_true.
254 | simplify in H2 ⊢ %;
256 lapply (H2 i); clear H2;
260 (* autobatch paramodulation by andb_assoc, Hletin. *)
261 | simplify in H2 H4 ⊢ %;
263 lapply (H2 i); clear H2;
264 lapply (H4 i); clear H4;
266 rewrite > distributive_andb_orb;
269 rewrite > distributive_orb_andb;
272 (* autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1. *)
273 | simplify in H2 ⊢ %;
275 lapply (H2 i); clear H2;
276 autobatch paramodulation;
277 | simplify in H2 ⊢ %;
279 lapply (H2 i); clear H2;
280 autobatch paramodulation
281 | simplify in H2 ⊢ %;
283 lapply (H2 i); clear H2;
284 autobatch paramodulation
288 alias num (instance 0) = "natural number".
294 | FAnd f1 f2 ⇒ S (size f1 + size f2)
295 | FOr f1 f2 ⇒ S (size f1 + size f2)
296 | FNot f ⇒ S (size f)
302 | cons F l' ⇒ size F + sizel l'
305 definition size_of_sequent ≝
306 λS.match S with [ pair l r ⇒ sizel l + sizel r].
309 ∀l1,l2,F. derive 〈l1,l2〉 → derive 〈l1,F::l2〉.
311 definition same_atom : Formula → Formula → bool.
322 definition symmetricb ≝
323 λA:Type.λeq:A → A → bool. ∀x,y. eq x y = eq y x.
325 theorem symmetricb_eqb: symmetricb ? eqb.
335 theorem symmetricb_same_atom: symmetricb ? same_atom.
345 |*: elim y; reflexivity
349 definition transitiveb ≝
350 λA:Type.λeq:A → A → bool.
351 ∀x,y,z. eq x y = true → eq y z = eq x z.
353 theorem transitiveb_same_atom: transitiveb ? same_atom.
362 rewrite > (eqb_true_to_eq ? ? H);
390 theorem eq_to_eq_mem:
391 ∀A.∀eq: A → A → bool.transitiveb ? eq →
392 ∀x,y,l.eq x y = true → mem ? eq x l = mem ? eq y l.
397 rewrite > (H ? ? ? H1);
403 theorem mem_to_exists_l1_l2:
404 ∀A,eq,n,l. (∀x,y. eq x y = true → x = y) → mem A eq n l = true → ∃l1,l2. l = l1 @ (n :: l2).
410 apply (bool_elim ? (eq n a));
412 [ apply (ex_intro ? ? []);
413 apply (ex_intro ? ? l1);
415 rewrite > (H1 ? ? H3);
417 | rewrite > H3 in H2;
422 apply (ex_intro ? ? (a::a1));
423 apply (ex_intro ? ? a2);
430 lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
441 rewrite > (eqb_true_to_eq ? ? H);
458 lemma same_atom_to_exists: ∀f1,f2. same_atom f1 f2 = true → ∃n. f1 = FAtom n.
473 lemma mem_same_atom_to_exists:
474 ∀f,l. mem ? same_atom f l = true → ∃n. f = FAtom n.
480 apply (bool_elim ? (same_atom f a));
482 [ elim (same_atom_to_exists ? ? H2);
484 | rewrite > H2 in H1;
492 lemma look_for_axiom:
494 (∃n,ll1,ll2,lr1,lr2. l1 = ll1 @ (FAtom n :: ll2) ∧ l2 = lr1 @ (FAtom n :: lr2))
495 ∨ ∀n1. (mem ? same_atom (FAtom n1) l1 ∧ mem ? same_atom (FAtom n1) l2) = false.
504 generalize in match (refl_eq ? (mem ? same_atom a l2));
505 elim (mem ? same_atom a l2) in ⊢ (? ? ? %→?);
507 elim (mem_to_exists_l1_l2 ? ? ? ? same_atom_to_eq H1);
509 elim (mem_same_atom_to_exists ? ? H1);
511 apply (ex_intro ? ? a3);
513 apply (ex_intro ? ? []);
519 apply (ex_intro ? ? a1);
520 apply (ex_intro ? ? (a::a2));
522 apply (ex_intro ? ? a3);
523 apply (ex_intro ? ? a4);
527 apply (bool_elim ? (same_atom a (FAtom n1)));
529 rewrite > (eq_to_eq_mem ? ? transitiveb_same_atom ? ? ? H3) in H1;
533 change in ⊢ (? ? (? % ?) ?) with
534 (match same_atom (FAtom n1) a with
536 |false ⇒ mem ? same_atom (FAtom n1) l
538 rewrite > symmetricb_same_atom;
548 lemma eq_plus_n_m_O_to_eq_m_O: ∀n,m.n+m=0 → m=0.
557 lemma not_eq_nil_append_cons: ∀A.∀l1,l2.∀x:A.¬ [] = l1 @ (x :: l2).
571 [true⇒true|false⇒mem Formula same_atom (FAtom n) l]) (and_of_list l)) =
573 (λn:nat.mem Formula same_atom (FAtom n) l) (and_of_list l)).
577 | simplify in ⊢ (? ? (? (? ? %)) ?);
578 change in ⊢ (? ? (? %) ?) with
580 .match eqb n x in bool return λb:bool.bool with
581 [true⇒true|false⇒mem Formula same_atom (FAtom n) (t::l1)]) t
584 .match eqb n x in bool return λb:bool.bool with
585 [true⇒true|false⇒mem Formula same_atom (FAtom n) (t::l1)])
594 lemma sizel_0_no_axiom_is_tautology:
595 ∀l1,l2. size_of_sequent 〈l1,l2〉 = 0 → is_tautology (formula_of_sequent 〈l1,l2〉) →
596 (∀n. (mem ? same_atom (FAtom n) l1 ∧ mem ? same_atom (FAtom n) l2) = false) →
597 (∃ll1,ll2. l1 = ll1 @ (FFalse :: ll2)) ∨ (∃ll1,ll2. l2 = ll1 @ (FTrue :: ll2)).
599 lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
601 elim l1 in Hletin H2 H ⊢ % 0;
604 elim l2 in H2 H1 H ⊢ % 0;
612 apply (ex_intro ? ? []);
620 elim (not_eq_nil_append_cons ? ? ? ? H6)
623 apply (ex_intro ? ? (FFalse::a1));
626 apply (ex_intro ? ? a2);
632 elim (H H1 H2 H3); clear H;
635 elim (not_eq_nil_append_cons ? ? ? ? H5)
638 apply (ex_intro ? ? (FAtom n::a1));
655 apply (ex_intro ? ? (FTrue::a1));
662 | lapply (H2 n); clear H2;
669 apply (ex_intro ? ? []);
675 apply (ex_intro ? ? (FAtom n::a1));
682 | lapply (H2 n1); clear H2;
684 elim (eqb n1 n) in Hletin ⊢ %;
692 lapply (H2 n); clear H2;
693 rewrite > eqb_n_n in Hletin;
696 rewrite > eqb_n_n in H3;
699 elim l in H3 H1 H ⊢ % 0;
712 apply (eq_plus_n_m_O_to_eq_m_O ? ? H2)
717 | elim t1 in H4 H2 ⊢ %;
742 lemma completeness_base:
743 ∀S. size_of_sequent S = 0 → is_tautology (formula_of_sequent S) → derive S.
746 simplify in ⊢ (?→%→?);
748 elim (look_for_axiom a b);
750 rewrite > H2; clear H2;
751 rewrite > H4; clear H4;
752 apply (ExchangeL ? a2 a3 (FAtom a1));
753 apply (ExchangeR ? a4 a5 (FAtom a1));
755 | elim (sizel_0_no_axiom_is_tautology a b H H1 H2);
758 apply (ExchangeL ? a1 a2 FFalse);
762 apply (ExchangeR ? a1 a2 FTrue);
769 lemma completeness_step:
770 ∀l1,l2,n. size_of_sequent 〈l1,l2〉 = S n →
771 (∃ll1,ll2,f. l1 = ll1 @ (f::ll2) ∧ size f > 0) ∨
772 (∃ll1,ll2,f. l2 = ll1 @ (f::ll2) ∧ size f > 0).
786 apply (ex_intro ? ? (FTrue::a));
795 apply (ex_intro ? ? (FFalse::a));
804 apply (ex_intro ? ? (FAtom n1::a));
809 apply (ex_intro ? ? []);
811 apply (ex_intro ? ? l);
812 apply (ex_intro ? ? (FAnd f f1));
820 apply (ex_intro ? ? []);
822 apply (ex_intro ? ? l);
823 apply (ex_intro ? ? (FOr f f1));
831 apply (ex_intro ? ? []);
833 apply (ex_intro ? ? l);
834 apply (ex_intro ? ? (FNot f));
854 apply (ex_intro ? ? []);
856 apply (ex_intro ? ? l);
857 apply (ex_intro ? ? (FAnd f f1));
862 apply (ex_intro ? ? []);
864 apply (ex_intro ? ? l);
865 apply (ex_intro ? ? (FOr f f1));
870 apply (ex_intro ? ? []);
872 apply (ex_intro ? ? l);
873 apply (ex_intro ? ? (FNot f));
881 theorem completeness: ∀S. is_tautology (formula_of_sequent S) → derive S.
883 generalize in match (refl_eq ? (size_of_sequent S));
884 elim (size_of_sequent S) in ⊢ (? ? ? %→?);
885 [ apply completeness_base;
894 lapply (H (λx.true));
897 lapply (H (λx.false));
902 lapply (H2 i); clear H2;
907 lapply (H2 i); clear H2;