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