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