helm/software/matita/library/demo/propositional_sequent_calculus.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/plus.ma".
  16 include "nat/compare.ma".
  17 include "list/sort.ma".
  18 include "datatypes/constructors.ma".
  19
  20 inductive Formula : Type ≝
  21    FTrue: Formula
  22  | FFalse: Formula
  23  | FAtom: nat → Formula
  24  | FAnd: Formula → Formula → Formula
  25  | FOr: Formula → Formula → Formula
  26  | FNot: Formula → Formula.
  27
  28 definition interp ≝ nat → bool.
  29
  30 let rec eval (interp:interp) F on F : bool ≝
  31  match F with
  32   [ FTrue ⇒ true
  33   | FFalse ⇒ false
  34   | FAtom n ⇒ interp n
  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
  38   ].
  39
  40 inductive not_nf : Formula → Prop ≝
  41    NTrue: not_nf FTrue
  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)).
  47
  48 let rec negate F ≝
  49  match F with
  50   [ FTrue ⇒ FFalse
  51   | FFalse ⇒ FTrue
  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]
  56 and elim_not F ≝
  57  match F with
  58   [ FTrue ⇒ FTrue
  59   | FFalse ⇒ FFalse
  60   | FAtom n ⇒ FAtom n
  61   | FAnd f1 f2 ⇒ FAnd (elim_not f1) (elim_not f2)
  62   | FOr f1 f2 ⇒ FOr (elim_not f1) (elim_not f2)
  63   | FNot f ⇒ negate f
  64   ].
  65
  66 theorem not_nf_elim_not: ∀F.not_nf (elim_not F) ∧ not_nf (negate F).
  67  intros;
  68  elim F;
  69   [1,2,3: simplify; autobatch
  70   |4,5:
  71    simplify;
  72    elim H; clear H;
  73    elim H1; clear H1;
  74    split;
  75    autobatch
  76   |elim H; clear H;
  77    split;
  78    [ assumption
  79    | assumption
  80    ]
  81   ]
  82 qed.
  83
  84 theorem demorgan1: ∀b1,b2:bool. (¬ (b1 ∧ b2)) = ¬ b1 ∨ ¬ b2.
  85  intros;
  86  elim b1;
  87  simplify;
  88  reflexivity.
  89 qed.
  90
  91 theorem demorgan2: ∀b1,b2:bool. (¬ (b1 ∨ b2)) = ¬ b1 ∧ ¬ b2.
  92  intros;
  93  elim b1;
  94  simplify;
  95  reflexivity.
  96 qed.
  97
  98 theorem eq_notb_notb_b_b: ∀b:bool. (¬ ¬ b) = b.
  99  intro;
 100  elim b;
 101  reflexivity.
 102 qed.
 103
 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).
 106  intros;
 107  elim F;
 108   [1,2,3: split; reflexivity
 109   |4,5:
 110    simplify;
 111    elim H; clear H;
 112    elim H1; clear H1;
 113    split;
 114     [1,3: autobatch
 115     |replace with ((eval i (FNot f) ∨ eval i (FNot f1)) = ¬ (eval i f ∧ eval i f1));
 116      [ simplify;
 117        autobatch
 118      | autobatch
 119      ]
 120     |replace with ((eval i (FNot f) ∧ eval i (FNot f1)) = ¬ (eval i f ∨ eval i f1));
 121      [ simplify;
 122        autobatch
 123      | autobatch
 124      ]
 125     ]
 126   |elim H; clear H;
 127    split;
 128     [ assumption
 129     | change with (eval i (elim_not f) = ¬ ¬ eval i f);
 130       autobatch
 131     ]
 132   ]
 133 qed.
 134
 135 definition sequent ≝ (list Formula) × (list Formula).
 136
 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〉
 148  | OrL: ∀l1,l2,f1,f2.
 149     derive 〈f1::l1,l2〉 → derive 〈f2::l1,l2〉 →
 150      derive 〈FOr f1 f2 :: l1,l2〉
 151  | OrR: ∀l1,l2,f1,f2.
 152     derive 〈l1,f1 :: f2 :: l2〉 → derive 〈l1,FOr f1 f2 :: l2〉
 153  | NotR: ∀l1,l2,f.
 154     derive 〈f::l1,l2〉 → derive 〈l1,FNot f :: l2〉
 155  | NotL: ∀l1,l2,f.
 156     derive 〈l1,f::l2〉 → derive 〈FNot f :: l1,l2〉.
 157
 158 let rec and_of_list l ≝
 159  match l with
 160   [ nil ⇒ FTrue
 161   | cons F l' ⇒ FAnd F (and_of_list l')
 162   ].
 163
 164 let rec or_of_list l ≝
 165  match l with
 166   [ nil ⇒ FFalse
 167   | cons F l' ⇒ FOr F (or_of_list l')
 168   ].
 169
 170 definition formula_of_sequent ≝
 171  λs.match s with [pair l1 l2 ⇒ FOr (FNot (and_of_list l1)) (or_of_list l2)].
 172
 173 definition is_tautology ≝
 174  λF. ∀i. eval i F = true.
 175
 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.
 183
 184 lemma and_of_list_permut:
 185  ∀i,f,l1,l2. eval i (and_of_list (l1 @ (f::l2))) = eval i (and_of_list (f :: l1 @ l2)).
 186  intros;
 187  elim l1;
 188   [ simplify;
 189     reflexivity
 190   | simplify in H ⊢ %;
 191     rewrite > H;
 192     autobatch paramodulation
 193   ]
 194 qed.
 195
 196 lemma or_of_list_permut:
 197  ∀i,f,l1,l2. eval i (or_of_list (l1 @ (f::l2))) = eval i (or_of_list (f :: l1 @ l2)).
 198  intros;
 199  elim l1;
 200   [ simplify;
 201     reflexivity
 202   | simplify in H ⊢ %;
 203     rewrite > H;
 204     autobatch paramodulation
 205   ]
 206 qed.
 207
 208 theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
 209  intros;
 210  elim H;
 211   [ simplify in H2 ⊢ %;
 212     intros;
 213     lapply (H2 i); clear H2;
 214     rewrite > and_of_list_permut;
 215     simplify;
 216     autobatch
 217   | simplify in H2 ⊢ %;
 218     intros;
 219     lapply (H2 i); clear H2;
 220     rewrite > or_of_list_permut;
 221     simplify;
 222     autobatch
 223   | simplify;
 224     intro;
 225     rewrite > demorgan1;
 226     rewrite < assoc_orb;
 227     rewrite > assoc_orb in ⊢ (? ? (? % ?) ?);
 228     rewrite > symm_orb in ⊢ (? ? (? (? ? %) ?) ?);
 229     rewrite < assoc_orb;
 230     rewrite > orb_not_b_b;
 231     reflexivity
 232   | simplify;
 233     intros;
 234     rewrite > symm_orb;
 235     reflexivity
 236   | simplify;
 237     intros;
 238     reflexivity
 239   | simplify in H2 H4 ⊢ %;
 240     intros;
 241     lapply (H2 i); clear H2;
 242     lapply (H4 i); clear H4;
 243     rewrite > symm_orb in ⊢ (? ? (? ? %) ?);
 244     rewrite > distributive_orb_andb;
 245     autobatch paramodulation
 246   | simplify in H2 ⊢ %;
 247     intros;
 248     lapply (H2 i); clear H2;
 249     autobatch
 250   | simplify in H2 H4 ⊢ %;
 251     intros;
 252     lapply (H2 i); clear H2;
 253     lapply (H4 i); clear H4;
 254     rewrite > symm_andb;
 255     rewrite > distributive_andb_orb;
 256     rewrite > demorgan2;
 257     rewrite > symm_orb;
 258     rewrite > distributive_orb_andb;
 259     autobatch paramodulation
 260   | simplify in H2 ⊢ %;
 261     intros;
 262     lapply (H2 i); clear H2;
 263     autobatch
 264   | simplify in H2 ⊢ %;
 265     intros;
 266     lapply (H2 i); clear H2;
 267     autobatch paramodulation
 268   | simplify in H2 ⊢ %;
 269     intros;
 270     lapply (H2 i); clear H2;
 271     autobatch paramodulation
 272   ]
 273 qed.
 274
 275 alias num (instance 0) = "natural number".
 276 let rec size F ≝
 277  match F with
 278   [ FTrue ⇒ 0
 279   | FFalse ⇒ 0
 280   | FAtom n ⇒ 0
 281   | FAnd f1 f2 ⇒ S (size f1 + size f2)
 282   | FOr f1 f2 ⇒ S (size f1 + size f2)
 283   | FNot f ⇒ S (size f)
 284   ].
 285
 286 let rec sizel l ≝
 287  match l with
 288   [ nil ⇒ 0
 289   | cons F l' ⇒ size F + sizel l'
 290   ].
 291
 292 definition size_of_sequent ≝
 293  λS.match S with [ pair l r ⇒ sizel l + sizel r].
 294
 295 axiom weakeningR:
 296  ∀l1,l2,F. derive 〈l1,l2〉 → derive 〈l1,F::l2〉.
 297
 298 definition same_atom : Formula → Formula → bool.
 299  intros;
 300  elim f;
 301   [3: elim f1;
 302        [3: apply (eqb n n1)
 303        |*: apply false
 304        ]
 305   |*: apply false
 306   ]
 307 qed.
 308
 309 definition symmetricb ≝
 310  λA:Type.λeq:A → A → bool. ∀x,y. eq x y = eq y x.
 311
 312 theorem symmetricb_eqb: symmetricb ? eqb.
 313  intro;
 314  elim x;
 315  elim y;
 316   [1,2,3: reflexivity
 317   | simplify;
 318     autobatch
 319   ]
 320 qed.
 321
 322 theorem symmetricb_same_atom: symmetricb ? same_atom.
 323  intro;
 324  elim x;
 325   [3:
 326     elim y;
 327      [3:
 328        simplify;
 329        apply symmetricb_eqb
 330      |*: reflexivity
 331      ]
 332   |*: elim y; reflexivity
 333   ]
 334 qed.
 335
 336 definition transitiveb ≝
 337  λA:Type.λeq:A → A → bool.
 338   ∀x,y,z. eq x y = true → eq y z = eq x z.
 339
 340 theorem transitiveb_same_atom: transitiveb ? same_atom.
 341  intro;
 342  elim x 0;
 343   [3:
 344     intros 2;
 345     elim y 0;
 346      [3:
 347        intros 3;
 348        simplify in H;
 349        rewrite > (eqb_true_to_eq ? ? H);
 350        reflexivity
 351      |1,2:
 352        intros;
 353        simplify in H;
 354        destruct H
 355      |4,5:
 356        intros;
 357        simplify in H2;
 358        destruct H2
 359      | intros;
 360        simplify in H1;
 361        destruct H1
 362      ]
 363   |1,2:
 364     intros;
 365     simplify in H;
 366     destruct H
 367   |4,5:
 368     intros;
 369     simplify in H2;
 370     destruct H2
 371   | intros;
 372     simplify in H1;
 373     destruct H1
 374   ]
 375 qed.
 376
 377 theorem eq_to_eq_mem:
 378  ∀A.∀eq: A → A → bool.transitiveb ? eq →
 379   ∀x,y,l.eq x y = true → mem ? eq x l = mem ? eq y l.
 380  intros;
 381  elim l;
 382   [ reflexivity
 383   | simplify;
 384     rewrite > (H ? ? ? H1);
 385     rewrite > H2;
 386     reflexivity
 387   ]
 388 qed.
 389
 390 theorem mem_to_exists_l1_l2:
 391  ∀A,eq,n,l. (∀x,y. eq x y = true → x = y) → mem A eq n l = true → ∃l1,l2. l = l1 @ (n :: l2).
 392  intros 4;
 393  elim l;
 394   [ simplify in H1;
 395     destruct H1
 396   | simplify in H2;
 397     apply (bool_elim ? (eq n a));
 398     intro;
 399      [ apply (ex_intro ? ? []);
 400        apply (ex_intro ? ? l1);
 401        simplify;
 402        rewrite > (H1 ? ? H3);
 403        reflexivity
 404      | rewrite > H3 in H2;
 405        simplify in H2;
 406        elim (H H1 H2);
 407        elim H4;
 408        rewrite > H5;
 409        apply (ex_intro ? ? (a::a1));
 410        apply (ex_intro ? ? a2);
 411        simplify;
 412        reflexivity
 413      ]
 414   ]
 415 qed.
 416
 417 lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
 418  intro;
 419  elim f1;
 420   [1,2:
 421     simplify in H;
 422     destruct H
 423   | elim f2 in H ⊢ %;
 424      [1,2:
 425        simplify in H;
 426        destruct H
 427      | simplify in H;
 428        rewrite > (eqb_true_to_eq ? ? H);
 429        reflexivity
 430      |4,5:
 431        simplify in H2;
 432        destruct H2
 433      | simplify in H1;
 434        destruct H1
 435      ]
 436   |4,5:
 437     simplify in H2;
 438     destruct H2
 439   |6:
 440     simplify in H1;
 441     destruct H1
 442   ]
 443 qed.
 444
 445 lemma same_atom_to_exists: ∀f1,f2. same_atom f1 f2 = true → ∃n. f1 = FAtom n.
 446  intro;
 447  elim f1;
 448   [1,2:
 449     simplify in H;
 450     destruct H
 451   | autobatch
 452   |4,5:
 453     simplify in H2;
 454     destruct H2
 455   | simplify in H1;
 456     destruct H1
 457   ]
 458 qed.
 459
 460 lemma mem_same_atom_to_exists:
 461  ∀f,l. mem ? same_atom f l = true → ∃n. f = FAtom n.
 462  intros 2;
 463  elim l;
 464   [ simplify in H;
 465     destruct H
 466   | simplify in H1;
 467     apply (bool_elim ? (same_atom f a));
 468     intros;
 469      [ elim (same_atom_to_exists ? ? H2);
 470        autobatch
 471      | rewrite > H2 in H1;
 472        simplify in H1;
 473        elim (H H1);
 474        autobatch
 475      ]
 476   ]
 477 qed.
 478
 479 lemma look_for_axiom:
 480  ∀l1,l2.
 481   (∃n,ll1,ll2,lr1,lr2. l1 = ll1 @ (FAtom n :: ll2) ∧ l2 = lr1 @ (FAtom n :: lr2))
 482   ∨ ∀n1. (mem ? same_atom (FAtom n1) l1 ∧ mem ? same_atom (FAtom n1) l2) = false.
 483  intro;
 484  elim l1 1; clear l1;
 485   [ intros;
 486     right;
 487     intros;
 488     simplify;
 489     reflexivity
 490   | intros;
 491     generalize in match (refl_eq ? (mem ? same_atom a l2));
 492     elim (mem ? same_atom a l2) in ⊢ (? ? ? %→?);
 493      [ left;
 494        elim (mem_to_exists_l1_l2 ? ? ? ? same_atom_to_eq H1);
 495        elim H2; clear H2;
 496        elim (mem_same_atom_to_exists ? ? H1);
 497        rewrite > H2 in H3;
 498        apply (ex_intro ? ? a3);
 499        rewrite > H2;
 500        apply (ex_intro ? ? []);
 501        simplify;
 502        autobatch depth=5
 503      | elim (H l2);
 504         [ left;
 505           decompose;
 506           apply (ex_intro ? ? a1);
 507           apply (ex_intro ? ? (a::a2));
 508           simplify;
 509           apply (ex_intro ? ? a3);
 510           apply (ex_intro ? ? a4);
 511           autobatch depth=4
 512         | right;
 513           intro;
 514           apply (bool_elim ? (same_atom a (FAtom n1)));
 515            [ intro;
 516              rewrite > (eq_to_eq_mem ? ? transitiveb_same_atom ? ? ? H3) in H1;
 517              rewrite > H1;
 518              autobatch
 519            | intro;
 520              change in ⊢ (? ? (? % ?) ?) with
 521               (match same_atom (FAtom n1) a with
 522                 [true ⇒ true
 523                 |false ⇒ mem ? same_atom (FAtom n1) l
 524                 ]);
 525              rewrite > symmetricb_same_atom;
 526              rewrite > H3;
 527              simplify;
 528              apply H2
 529            ]
 530         ]
 531      ]
 532   ]
 533 qed.
 534
 535 lemma eq_plus_n_m_O_to_eq_m_O: ∀n,m.n+m=0 → m=0.
 536  intros 2;
 537  elim n;
 538   [ assumption
 539   | simplify in H1;
 540     destruct H1
 541   ]
 542 qed.
 543
 544 lemma not_eq_nil_append_cons: ∀A.∀l1,l2.∀x:A.¬ [] = l1 @ (x :: l2).
 545  intros;
 546  elim l1;
 547  simplify;
 548  intro;
 549   [ destruct H
 550   | destruct H1
 551   ]
 552 qed.
 553
 554 (*lemma foo: ∀x,l.
 555  (¬eval
 556    (λn:nat
 557     .match eqb n x with
 558      [true⇒true|false⇒mem Formula same_atom (FAtom n) l]) (and_of_list l)) =
 559  (¬eval
 560    (λn:nat.mem Formula same_atom (FAtom n) l) (and_of_list l)).
 561  intros;
 562  elim l;
 563   [ reflexivity
 564   | simplify in ⊢ (? ? (? (? ? %)) ?);
 565     change in ⊢ (? ? (? %) ?) with
 566      (eval (λn:nat
 567       .match eqb n x in bool return λb:bool.bool with
 568        [true⇒true|false⇒mem Formula same_atom (FAtom n) (t::l1)]) t
 569       ∧
 570       eval (λn:nat
 571       .match eqb n x in bool return λb:bool.bool with
 572        [true⇒true|false⇒mem Formula same_atom (FAtom n) (t::l1)])
 573       (and_of_list l1));
 574
 575
 576   ]
 577 qed.*)
 578
 579 axiom daemon: False.
 580
 581 lemma sizel_0_no_axiom_is_tautology:
 582  ∀l1,l2. size_of_sequent 〈l1,l2〉 = 0 → is_tautology (formula_of_sequent 〈l1,l2〉) →
 583   (∀n. (mem ? same_atom (FAtom n) l1 ∧ mem ? same_atom (FAtom n) l2) = false) →
 584    (∃ll1,ll2. l1 = ll1 @ (FFalse :: ll2)) ∨ (∃ll1,ll2. l2 = ll1 @ (FTrue :: ll2)).
 585  intros;
 586  lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
 587  simplify in Hletin;
 588  elim l1 in Hletin H2 H ⊢ % 0;
 589   [ intros;
 590     simplify in H2;
 591     elim l2 in H2 H1 H ⊢ % 0;
 592      [ intros;
 593        simplify in H2;
 594        destruct H2
 595      | simplify;
 596        intro;
 597        elim a;
 598         [ right;
 599           apply (ex_intro ? ? []);
 600           simplify;
 601           autobatch
 602         | simplify in H3;
 603           simplify in H1;
 604           elim H;
 605            [ elim H4;
 606              elim H5;
 607              elim (not_eq_nil_append_cons ? ? ? ? H6)
 608            | elim H4;
 609              right;
 610              apply (ex_intro ? ? (FFalse::a1));
 611              simplify;
 612              elim H5;
 613              apply (ex_intro ? ? a2);
 614              autobatch
 615            |3,4: autobatch
 616            | assumption
 617            ]
 618         | simplify in H1 H3;
 619           elim (H H1 H2 H3); clear H;
 620            [ elim H4;
 621              elim H;
 622              elim (not_eq_nil_append_cons ? ? ? ? H5)
 623            | right;
 624              elim H4;
 625              apply (ex_intro ? ? (FAtom n::a1));
 626              simplify;
 627              elim H;
 628              autobatch
 629            ]
 630         |4,5:
 631           simplify in H3;
 632           destruct H3
 633         | simplify in H2;
 634           destruct H2
 635         ]
 636      ]
 637   | intro;
 638      elim a;
 639      [ elim H;
 640         [ left;
 641           elim H4;
 642           apply (ex_intro ? ? (FTrue::a1));
 643           simplify;
 644           elim H5;
 645           autobatch
 646         | right;
 647           assumption
 648         | assumption
 649         | lapply (H2 n); clear H2;
 650           simplify in Hletin;
 651           assumption
 652         | simplify in H3;
 653           assumption
 654         ]
 655      | left;
 656        apply (ex_intro ? ? []);
 657        simplify;
 658        autobatch
 659      | elim H;
 660         [ left;
 661           elim H4;
 662           apply (ex_intro ? ? (FAtom n::a1));
 663           simplify;
 664           elim H5;
 665           autobatch
 666         | right;
 667           assumption
 668         | assumption
 669         | lapply (H2 n1); clear H2;
 670           simplify in Hletin;
 671           elim (eqb n1 n) in Hletin ⊢ %;
 672            [ simplify in H2;
 673              rewrite > H2;
 674              autobatch
 675            | simplify in H2;
 676              assumption
 677            ]
 678         | simplify in H2;
 679           lapply (H2 n); clear H2;
 680           rewrite > eqb_n_n in Hletin;
 681           simplify in Hletin;
 682           simplify in H3;
 683           rewrite > eqb_n_n in H3;
 684           simplify in H3;
 685 (*
 686           elim l in H3 H1 H ⊢ % 0;
 687            [ elim l2 0;
 688               [ intros;
 689                 simplify in H2;
 690                 destruct H2
 691               | intros;
 692                 simplify in H4 ⊢ %;
 693                 simplify in H;
 694                 rewrite > H;
 695                  [ autobatch
 696                  | intros;
 697                    apply H1;
 698                  | simplify in H2;
 699                    apply (eq_plus_n_m_O_to_eq_m_O ? ? H2)
 700                  |
 701                  ]
 702
 703                  [ autobatch
 704                  | elim t1 in H4 H2 ⊢ %;
 705                     [
 706                     |
 707                     |
 708                     |4,5:
 709                       simplify in H5;
 710                       destruct H5
 711                     | simplify in H4;
 712                       destruct H4
 713                     ]
 714                  ]
 715               ]
 716            |
 717            ]
 718 *) elim daemon
 719         ]
 720      |4,5:
 721        simplify in H3;
 722        destruct H3
 723      | simplify in H2;
 724        destruct H2
 725      ]
 726   ]
 727 qed.
 728
 729 lemma completeness_base:
 730  ∀S. size_of_sequent S = 0 → is_tautology (formula_of_sequent S) → derive S.
 731  intro;
 732  elim S 1; clear S;
 733  simplify in ⊢ (?→%→?);
 734  intros;
 735  elim (look_for_axiom a b);
 736   [ decompose;
 737     rewrite > H2; clear H2;
 738     rewrite > H4; clear H4;
 739     apply (ExchangeL ? a2 a3 (FAtom a1));
 740     apply (ExchangeR ? a4 a5 (FAtom a1));
 741     apply Axiom
 742   | elim (sizel_0_no_axiom_is_tautology a b H H1 H2);
 743      [ decompose;
 744        rewrite > H3;
 745        apply (ExchangeL ? a1 a2 FFalse);
 746        apply FalseL
 747      | decompose;
 748        rewrite > H3;
 749        apply (ExchangeR ? a1 a2 FTrue);
 750        apply TrueR
 751      ]
 752   ]
 753 qed.
 754
 755 (*
 756 lemma completeness_step:
 757  ∀l1,l2,n. size_of_sequent 〈l1,l2〉 = S n →
 758    (∃ll1,ll2,f. l1 = ll1 @ (f::ll2) ∧ size f > 0) ∨
 759    (∃ll1,ll2,f. l2 = ll1 @ (f::ll2) ∧ size f > 0).
 760  intros 3;
 761  elim l1 0;
 762   [ elim l2 0;
 763      [ intros;
 764        simplify in H;
 765        destruct H
 766      | intros 3;
 767        elim t;
 768         [ elim (H H1);
 769            [ left;
 770              assumption
 771            | right;
 772              decompose;
 773              apply (ex_intro ? ? (FTrue::a));
 774              simplify;
 775              autobatch depth=5
 776            ]
 777         | elim (H H1);
 778            [ left;
 779              assumption
 780            | right;
 781              decompose;
 782              apply (ex_intro ? ? (FFalse::a));
 783              simplify;
 784              autobatch depth=5
 785            ]
 786         | elim (H H1);
 787            [ left;
 788              assumption
 789            | right;
 790              decompose;
 791              apply (ex_intro ? ? (FAtom n1::a));
 792              simplify;
 793              autobatch depth=5
 794            ]
 795         | right;
 796           apply (ex_intro ? ? []);
 797           simplify;
 798           apply (ex_intro ? ? l);
 799           apply (ex_intro ? ? (FAnd f f1));
 800           simplify;
 801           split;
 802            [ reflexivity
 803            | unfold gt;
 804              autobatch
 805            ]
 806         | right;
 807           apply (ex_intro ? ? []);
 808           simplify;
 809           apply (ex_intro ? ? l);
 810           apply (ex_intro ? ? (FOr f f1));
 811           simplify;
 812           split;
 813            [ reflexivity
 814            | unfold gt;
 815              autobatch
 816            ]
 817         | right;
 818           apply (ex_intro ? ? []);
 819           simplify;
 820           apply (ex_intro ? ? l);
 821           apply (ex_intro ? ? (FNot f));
 822           simplify;
 823           split;
 824            [ reflexivity
 825            | unfold gt;
 826              autobatch
 827            ]
 828         ]
 829      ]
 830   | intros 2;
 831     elim t;
 832      [1,2:(*,2,3:*)
 833        elim (H H1);
 834        decompose;
 835         [ left;
 836           autobatch depth=5
 837         | right;
 838           autobatch depth=5
 839         ]
 840      | left;
 841        apply (ex_intro ? ? []);
 842        simplify;
 843        apply (ex_intro ? ? l);
 844        apply (ex_intro ? ? (FAnd f f1));
 845        unfold gt;
 846        simplify;
 847        autobatch
 848      | left;
 849        apply (ex_intro ? ? []);
 850        simplify;
 851        apply (ex_intro ? ? l);
 852        apply (ex_intro ? ? (FOr f f1));
 853        unfold gt;
 854        simplify;
 855        autobatch
 856      | left;
 857        apply (ex_intro ? ? []);
 858        simplify;
 859        apply (ex_intro ? ? l);
 860        apply (ex_intro ? ? (FNot f));
 861        unfold gt;
 862        simplify;
 863        autobatch
 864      ]
 865   ]
 866 qed.
 867
 868 theorem completeness: ∀S. is_tautology (formula_of_sequent S) → derive S.
 869  intro;
 870  generalize in match (refl_eq ? (size_of_sequent S));
 871  elim (size_of_sequent S) in ⊢ (? ? ? %→?);
 872   [ apply completeness_base;
 873     assumption
 874   |
 875   ]
 876 qed.
 877
 878  elim F;
 879   [ autobatch
 880   | simplify in H;
 881     lapply (H (λx.true));
 882     destruct Hletin
 883   | simplify in H;
 884     lapply (H (λx.false));
 885     destruct Hletin
 886   | apply AndR;
 887      [ apply H;
 888        intro;
 889        lapply (H2 i); clear H2;
 890        simplify in Hletin;
 891        autobatch
 892      | apply H1;
 893        intro;
 894        lapply (H2 i); clear H2;
 895        simplify in Hletin;
 896        autobatch
 897      ]
 898   | apply OrR;
 899     simplify in H2;
 900   | apply NotR;
 901     simplify in H1;
 902 *)