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