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     STOP
 246     autobatch paramodulation
 247   | simplify in H2 ⊢ %;
 248     intros;
 249     lapply (H2 i); clear H2;
 250     pump 98.
 251     autobatch.
 252   | simplify in H2 H4 ⊢ %;
 253     intros;
 254     lapply (H2 i); clear H2;
 255     lapply (H4 i); clear H4;
 256     rewrite > symm_andb;
 257     rewrite > distributive_andb_orb;
 258     rewrite > demorgan2;
 259     rewrite > symm_orb;
 260     rewrite > distributive_orb_andb;
 261     autobatch paramodulation
 262   | simplify in H2 ⊢ %;
 263     intros;
 264     lapply (H2 i); clear H2;
 265     autobatch
 266   | simplify in H2 ⊢ %;
 267     intros;
 268     lapply (H2 i); clear H2;
 269     autobatch paramodulation
 270   | simplify in H2 ⊢ %;
 271     intros;
 272     lapply (H2 i); clear H2;
 273     autobatch paramodulation
 274   ]
 275 qed.
 276
 277 alias num (instance 0) = "natural number".
 278 let rec size F ≝
 279  match F with
 280   [ FTrue ⇒ 0
 281   | FFalse ⇒ 0
 282   | FAtom n ⇒ 0
 283   | FAnd f1 f2 ⇒ S (size f1 + size f2)
 284   | FOr f1 f2 ⇒ S (size f1 + size f2)
 285   | FNot f ⇒ S (size f)
 286   ].
 287
 288 let rec sizel l ≝
 289  match l with
 290   [ nil ⇒ 0
 291   | cons F l' ⇒ size F + sizel l'
 292   ].
 293
 294 definition size_of_sequent ≝
 295  λS.match S with [ pair l r ⇒ sizel l + sizel r].
 296
 297 axiom weakeningR:
 298  ∀l1,l2,F. derive 〈l1,l2〉 → derive 〈l1,F::l2〉.
 299
 300 definition same_atom : Formula → Formula → bool.
 301  intros;
 302  elim f;
 303   [3: elim f1;
 304        [3: apply (eqb n n1)
 305        |*: apply false
 306        ]
 307   |*: apply false
 308   ]
 309 qed.
 310
 311 definition symmetricb ≝
 312  λA:Type.λeq:A → A → bool. ∀x,y. eq x y = eq y x.
 313
 314 theorem symmetricb_eqb: symmetricb ? eqb.
 315  intro;
 316  elim x;
 317  elim y;
 318   [1,2,3: reflexivity
 319   | simplify;
 320     autobatch
 321   ]
 322 qed.
 323
 324 theorem symmetricb_same_atom: symmetricb ? same_atom.
 325  intro;
 326  elim x;
 327   [3:
 328     elim y;
 329      [3:
 330        simplify;
 331        apply symmetricb_eqb
 332      |*: reflexivity
 333      ]
 334   |*: elim y; reflexivity
 335   ]
 336 qed.
 337
 338 definition transitiveb ≝
 339  λA:Type.λeq:A → A → bool.
 340   ∀x,y,z. eq x y = true → eq y z = eq x z.
 341
 342 theorem transitiveb_same_atom: transitiveb ? same_atom.
 343  intro;
 344  elim x 0;
 345   [3:
 346     intros 2;
 347     elim y 0;
 348      [3:
 349        intros 3;
 350        simplify in H;
 351        rewrite > (eqb_true_to_eq ? ? H);
 352        reflexivity
 353      |1,2:
 354        intros;
 355        simplify in H;
 356        destruct H
 357      |4,5:
 358        intros;
 359        simplify in H2;
 360        destruct H2
 361      | intros;
 362        simplify in H1;
 363        destruct H1
 364      ]
 365   |1,2:
 366     intros;
 367     simplify in H;
 368     destruct H
 369   |4,5:
 370     intros;
 371     simplify in H2;
 372     destruct H2
 373   | intros;
 374     simplify in H1;
 375     destruct H1
 376   ]
 377 qed.
 378
 379 theorem eq_to_eq_mem:
 380  ∀A.∀eq: A → A → bool.transitiveb ? eq →
 381   ∀x,y,l.eq x y = true → mem ? eq x l = mem ? eq y l.
 382  intros;
 383  elim l;
 384   [ reflexivity
 385   | simplify;
 386     rewrite > (H ? ? ? H1);
 387     rewrite > H2;
 388     reflexivity
 389   ]
 390 qed.
 391
 392 theorem mem_to_exists_l1_l2:
 393  ∀A,eq,n,l. (∀x,y. eq x y = true → x = y) → mem A eq n l = true → ∃l1,l2. l = l1 @ (n :: l2).
 394  intros 4;
 395  elim l;
 396   [ simplify in H1;
 397     destruct H1
 398   | simplify in H2;
 399     apply (bool_elim ? (eq n a));
 400     intro;
 401      [ apply (ex_intro ? ? []);
 402        apply (ex_intro ? ? l1);
 403        simplify;
 404        rewrite > (H1 ? ? H3);
 405        reflexivity
 406      | rewrite > H3 in H2;
 407        simplify in H2;
 408        elim (H H1 H2);
 409        elim H4;
 410        rewrite > H5;
 411        apply (ex_intro ? ? (a::a1));
 412        apply (ex_intro ? ? a2);
 413        simplify;
 414        reflexivity
 415      ]
 416   ]
 417 qed.
 418
 419 lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
 420  intro;
 421  elim f1;
 422   [1,2:
 423     simplify in H;
 424     destruct H
 425   | elim f2 in H ⊢ %;
 426      [1,2:
 427        simplify in H;
 428        destruct H
 429      | simplify in H;
 430        rewrite > (eqb_true_to_eq ? ? H);
 431        reflexivity
 432      |4,5:
 433        simplify in H2;
 434        destruct H2
 435      | simplify in H1;
 436        destruct H1
 437      ]
 438   |4,5:
 439     simplify in H2;
 440     destruct H2
 441   |6:
 442     simplify in H1;
 443     destruct H1
 444   ]
 445 qed.
 446
 447 lemma same_atom_to_exists: ∀f1,f2. same_atom f1 f2 = true → ∃n. f1 = FAtom n.
 448  intro;
 449  elim f1;
 450   [1,2:
 451     simplify in H;
 452     destruct H
 453   | autobatch
 454   |4,5:
 455     simplify in H2;
 456     destruct H2
 457   | simplify in H1;
 458     destruct H1
 459   ]
 460 qed.
 461
 462 lemma mem_same_atom_to_exists:
 463  ∀f,l. mem ? same_atom f l = true → ∃n. f = FAtom n.
 464  intros 2;
 465  elim l;
 466   [ simplify in H;
 467     destruct H
 468   | simplify in H1;
 469     apply (bool_elim ? (same_atom f a));
 470     intros;
 471      [ elim (same_atom_to_exists ? ? H2);
 472        autobatch
 473      | rewrite > H2 in H1;
 474        simplify in H1;
 475        elim (H H1);
 476        autobatch
 477      ]
 478   ]
 479 qed.
 480
 481 lemma look_for_axiom:
 482  ∀l1,l2.
 483   (∃n,ll1,ll2,lr1,lr2. l1 = ll1 @ (FAtom n :: ll2) ∧ l2 = lr1 @ (FAtom n :: lr2))
 484   ∨ ∀n1. (mem ? same_atom (FAtom n1) l1 ∧ mem ? same_atom (FAtom n1) l2) = false.
 485  intro;
 486  elim l1 1; clear l1;
 487   [ intros;
 488     right;
 489     intros;
 490     simplify;
 491     reflexivity
 492   | intros;
 493     generalize in match (refl_eq ? (mem ? same_atom a l2));
 494     elim (mem ? same_atom a l2) in ⊢ (? ? ? %→?);
 495      [ left;
 496        elim (mem_to_exists_l1_l2 ? ? ? ? same_atom_to_eq H1);
 497        elim H2; clear H2;
 498        elim (mem_same_atom_to_exists ? ? H1);
 499        rewrite > H2 in H3;
 500        apply (ex_intro ? ? a3);
 501        rewrite > H2;
 502        apply (ex_intro ? ? []);
 503        simplify;
 504        autobatch depth=5
 505      | elim (H l2);
 506         [ left;
 507           decompose;
 508           apply (ex_intro ? ? a1);
 509           apply (ex_intro ? ? (a::a2));
 510           simplify;
 511           apply (ex_intro ? ? a3);
 512           apply (ex_intro ? ? a4);
 513           autobatch depth=4
 514         | right;
 515           intro;
 516           apply (bool_elim ? (same_atom a (FAtom n1)));
 517            [ intro;
 518              rewrite > (eq_to_eq_mem ? ? transitiveb_same_atom ? ? ? H3) in H1;
 519              rewrite > H1;
 520              autobatch
 521            | intro;
 522              change in ⊢ (? ? (? % ?) ?) with
 523               (match same_atom (FAtom n1) a with
 524                 [true ⇒ true
 525                 |false ⇒ mem ? same_atom (FAtom n1) l
 526                 ]);
 527              rewrite > symmetricb_same_atom;
 528              rewrite > H3;
 529              simplify;
 530              apply H2
 531            ]
 532         ]
 533      ]
 534   ]
 535 qed.
 536
 537 lemma eq_plus_n_m_O_to_eq_m_O: ∀n,m.n+m=0 → m=0.
 538  intros 2;
 539  elim n;
 540   [ assumption
 541   | simplify in H1;
 542     destruct H1
 543   ]
 544 qed.
 545
 546 lemma not_eq_nil_append_cons: ∀A.∀l1,l2.∀x:A.¬ [] = l1 @ (x :: l2).
 547  intros;
 548  elim l1;
 549  simplify;
 550  intro;
 551   [ destruct H
 552   | destruct H1
 553   ]
 554 qed.
 555
 556 (*lemma foo: ∀x,l.
 557  (¬eval
 558    (λn:nat
 559     .match eqb n x with
 560      [true⇒true|false⇒mem Formula same_atom (FAtom n) l]) (and_of_list l)) =
 561  (¬eval
 562    (λn:nat.mem Formula same_atom (FAtom n) l) (and_of_list l)).
 563  intros;
 564  elim l;
 565   [ reflexivity
 566   | simplify in ⊢ (? ? (? (? ? %)) ?);
 567     change in ⊢ (? ? (? %) ?) with
 568      (eval (λn:nat
 569       .match eqb n x in bool return λb:bool.bool with
 570        [true⇒true|false⇒mem Formula same_atom (FAtom n) (t::l1)]) t
 571       ∧
 572       eval (λn:nat
 573       .match eqb n x in bool return λb:bool.bool with
 574        [true⇒true|false⇒mem Formula same_atom (FAtom n) (t::l1)])
 575       (and_of_list l1));
 576
 577
 578   ]
 579 qed.*)
 580
 581 axiom daemon: False.
 582
 583 lemma sizel_0_no_axiom_is_tautology:
 584  ∀l1,l2. size_of_sequent 〈l1,l2〉 = 0 → is_tautology (formula_of_sequent 〈l1,l2〉) →
 585   (∀n. (mem ? same_atom (FAtom n) l1 ∧ mem ? same_atom (FAtom n) l2) = false) →
 586    (∃ll1,ll2. l1 = ll1 @ (FFalse :: ll2)) ∨ (∃ll1,ll2. l2 = ll1 @ (FTrue :: ll2)).
 587  intros;
 588  lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
 589  simplify in Hletin;
 590  elim l1 in Hletin H2 H ⊢ % 0;
 591   [ intros;
 592     simplify in H2;
 593     elim l2 in H2 H1 H ⊢ % 0;
 594      [ intros;
 595        simplify in H2;
 596        destruct H2
 597      | simplify;
 598        intro;
 599        elim a;
 600         [ right;
 601           apply (ex_intro ? ? []);
 602           simplify;
 603           autobatch
 604         | simplify in H3;
 605           simplify in H1;
 606           elim H;
 607            [ elim H4;
 608              elim H5;
 609              elim (not_eq_nil_append_cons ? ? ? ? H6)
 610            | elim H4;
 611              right;
 612              apply (ex_intro ? ? (FFalse::a1));
 613              simplify;
 614              elim H5;
 615              apply (ex_intro ? ? a2);
 616              autobatch
 617            |3,4: autobatch
 618            | assumption
 619            ]
 620         | simplify in H1 H3;
 621           elim (H H1 H2 H3); clear H;
 622            [ elim H4;
 623              elim H;
 624              elim (not_eq_nil_append_cons ? ? ? ? H5)
 625            | right;
 626              elim H4;
 627              apply (ex_intro ? ? (FAtom n::a1));
 628              simplify;
 629              elim H;
 630              autobatch
 631            ]
 632         |4,5:
 633           simplify in H3;
 634           destruct H3
 635         | simplify in H2;
 636           destruct H2
 637         ]
 638      ]
 639   | intro;
 640      elim a;
 641      [ elim H;
 642         [ left;
 643           elim H4;
 644           apply (ex_intro ? ? (FTrue::a1));
 645           simplify;
 646           elim H5;
 647           autobatch
 648         | right;
 649           assumption
 650         | assumption
 651         | lapply (H2 n); clear H2;
 652           simplify in Hletin;
 653           assumption
 654         | simplify in H3;
 655           assumption
 656         ]
 657      | left;
 658        apply (ex_intro ? ? []);
 659        simplify;
 660        autobatch
 661      | elim H;
 662         [ left;
 663           elim H4;
 664           apply (ex_intro ? ? (FAtom n::a1));
 665           simplify;
 666           elim H5;
 667           autobatch
 668         | right;
 669           assumption
 670         | assumption
 671         | lapply (H2 n1); clear H2;
 672           simplify in Hletin;
 673           elim (eqb n1 n) in Hletin ⊢ %;
 674            [ simplify in H2;
 675              rewrite > H2;
 676              autobatch
 677            | simplify in H2;
 678              assumption
 679            ]
 680         | simplify in H2;
 681           lapply (H2 n); clear H2;
 682           rewrite > eqb_n_n in Hletin;
 683           simplify in Hletin;
 684           simplify in H3;
 685           rewrite > eqb_n_n in H3;
 686           simplify in H3;
 687 (*
 688           elim l in H3 H1 H ⊢ % 0;
 689            [ elim l2 0;
 690               [ intros;
 691                 simplify in H2;
 692                 destruct H2
 693               | intros;
 694                 simplify in H4 ⊢ %;
 695                 simplify in H;
 696                 rewrite > H;
 697                  [ autobatch
 698                  | intros;
 699                    apply H1;
 700                  | simplify in H2;
 701                    apply (eq_plus_n_m_O_to_eq_m_O ? ? H2)
 702                  |
 703                  ]
 704
 705                  [ autobatch
 706                  | elim t1 in H4 H2 ⊢ %;
 707                     [
 708                     |
 709                     |
 710                     |4,5:
 711                       simplify in H5;
 712                       destruct H5
 713                     | simplify in H4;
 714                       destruct H4
 715                     ]
 716                  ]
 717               ]
 718            |
 719            ]
 720 *) elim daemon
 721         ]
 722      |4,5:
 723        simplify in H3;
 724        destruct H3
 725      | simplify in H2;
 726        destruct H2
 727      ]
 728   ]
 729 qed.
 730
 731 lemma completeness_base:
 732  ∀S. size_of_sequent S = 0 → is_tautology (formula_of_sequent S) → derive S.
 733  intro;
 734  elim S 1; clear S;
 735  simplify in ⊢ (?→%→?);
 736  intros;
 737  elim (look_for_axiom a b);
 738   [ decompose;
 739     rewrite > H2; clear H2;
 740     rewrite > H4; clear H4;
 741     apply (ExchangeL ? a2 a3 (FAtom a1));
 742     apply (ExchangeR ? a4 a5 (FAtom a1));
 743     apply Axiom
 744   | elim (sizel_0_no_axiom_is_tautology a b H H1 H2);
 745      [ decompose;
 746        rewrite > H3;
 747        apply (ExchangeL ? a1 a2 FFalse);
 748        apply FalseL
 749      | decompose;
 750        rewrite > H3;
 751        apply (ExchangeR ? a1 a2 FTrue);
 752        apply TrueR
 753      ]
 754   ]
 755 qed.
 756
 757 (*
 758 lemma completeness_step:
 759  ∀l1,l2,n. size_of_sequent 〈l1,l2〉 = S n →
 760    (∃ll1,ll2,f. l1 = ll1 @ (f::ll2) ∧ size f > 0) ∨
 761    (∃ll1,ll2,f. l2 = ll1 @ (f::ll2) ∧ size f > 0).
 762  intros 3;
 763  elim l1 0;
 764   [ elim l2 0;
 765      [ intros;
 766        simplify in H;
 767        destruct H
 768      | intros 3;
 769        elim t;
 770         [ elim (H H1);
 771            [ left;
 772              assumption
 773            | right;
 774              decompose;
 775              apply (ex_intro ? ? (FTrue::a));
 776              simplify;
 777              autobatch depth=5
 778            ]
 779         | elim (H H1);
 780            [ left;
 781              assumption
 782            | right;
 783              decompose;
 784              apply (ex_intro ? ? (FFalse::a));
 785              simplify;
 786              autobatch depth=5
 787            ]
 788         | elim (H H1);
 789            [ left;
 790              assumption
 791            | right;
 792              decompose;
 793              apply (ex_intro ? ? (FAtom n1::a));
 794              simplify;
 795              autobatch depth=5
 796            ]
 797         | right;
 798           apply (ex_intro ? ? []);
 799           simplify;
 800           apply (ex_intro ? ? l);
 801           apply (ex_intro ? ? (FAnd f f1));
 802           simplify;
 803           split;
 804            [ reflexivity
 805            | unfold gt;
 806              autobatch
 807            ]
 808         | right;
 809           apply (ex_intro ? ? []);
 810           simplify;
 811           apply (ex_intro ? ? l);
 812           apply (ex_intro ? ? (FOr f f1));
 813           simplify;
 814           split;
 815            [ reflexivity
 816            | unfold gt;
 817              autobatch
 818            ]
 819         | right;
 820           apply (ex_intro ? ? []);
 821           simplify;
 822           apply (ex_intro ? ? l);
 823           apply (ex_intro ? ? (FNot f));
 824           simplify;
 825           split;
 826            [ reflexivity
 827            | unfold gt;
 828              autobatch
 829            ]
 830         ]
 831      ]
 832   | intros 2;
 833     elim t;
 834      [1,2:(*,2,3:*)
 835        elim (H H1);
 836        decompose;
 837         [ left;
 838           autobatch depth=5
 839         | right;
 840           autobatch depth=5
 841         ]
 842      | left;
 843        apply (ex_intro ? ? []);
 844        simplify;
 845        apply (ex_intro ? ? l);
 846        apply (ex_intro ? ? (FAnd f f1));
 847        unfold gt;
 848        simplify;
 849        autobatch
 850      | left;
 851        apply (ex_intro ? ? []);
 852        simplify;
 853        apply (ex_intro ? ? l);
 854        apply (ex_intro ? ? (FOr f f1));
 855        unfold gt;
 856        simplify;
 857        autobatch
 858      | left;
 859        apply (ex_intro ? ? []);
 860        simplify;
 861        apply (ex_intro ? ? l);
 862        apply (ex_intro ? ? (FNot f));
 863        unfold gt;
 864        simplify;
 865        autobatch
 866      ]
 867   ]
 868 qed.
 869
 870 theorem completeness: ∀S. is_tautology (formula_of_sequent S) → derive S.
 871  intro;
 872  generalize in match (refl_eq ? (size_of_sequent S));
 873  elim (size_of_sequent S) in ⊢ (? ? ? %→?);
 874   [ apply completeness_base;
 875     assumption
 876   |
 877   ]
 878 qed.
 879
 880  elim F;
 881   [ autobatch
 882   | simplify in H;
 883     lapply (H (λx.true));
 884     destruct Hletin
 885   | simplify in H;
 886     lapply (H (λx.false));
 887     destruct Hletin
 888   | apply AndR;
 889      [ apply H;
 890        intro;
 891        lapply (H2 i); clear H2;
 892        simplify in Hletin;
 893        autobatch
 894      | apply H1;
 895        intro;
 896        lapply (H2 i); clear H2;
 897        simplify in Hletin;
 898        autobatch
 899      ]
 900   | apply OrR;
 901     simplify in H2;
 902   | apply NotR;
 903     simplify in H1;
 904 *)