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 let rec or_of_list l ≝
 167  match l with
 168   [ nil ⇒ FFalse
 169   | cons F l' ⇒ FOr F (or_of_list l')
 170   ].
 171
 172 definition formula_of_sequent ≝
 173  λs.match s with [pair l1 l2 ⇒ FOr (FNot (and_of_list l1)) (or_of_list l2)].
 174
 175 definition is_tautology ≝
 176  λF. ∀i. eval i F = true.
 177
 178 axiom assoc_orb: associative ? orb.
 179 axiom symm_orb: symmetric ? orb.
 180 axiom orb_not_b_b: ∀b:bool. (¬b ∨ b) = true.
 181 axiom distributive_orb_andb: distributive ? orb andb.
 182 axiom symm_andb: symmetric ? andb.
 183 axiom associative_andb: associative ? andb.
 184 axiom distributive_andb_orb: distributive ? andb orb.
 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     autobatch paramodulation
 248   | simplify in H2 ⊢ %;
 249     intros;
 250     lapply (H2 i); clear H2;
 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 t));
 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 ? ? (t::a));
 412        apply (ex_intro ? ? a1);
 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   | generalize in match H; clear H;
 426     elim f2;
 427      [1,2:
 428        simplify in H;
 429        destruct H
 430      | simplify in H;
 431        rewrite > (eqb_true_to_eq ? ? H);
 432        reflexivity
 433      |4,5:
 434        simplify in H2;
 435        destruct H2
 436      | simplify in H1;
 437        destruct H1
 438      ]
 439   |4,5:
 440     simplify in H2;
 441     destruct H2
 442   |6:
 443     simplify in H1;
 444     destruct H1
 445   ]
 446 qed.
 447
 448 lemma same_atom_to_exists: ∀f1,f2. same_atom f1 f2 = true → ∃n. f1 = FAtom n.
 449  intro;
 450  elim f1;
 451   [1,2:
 452     simplify in H;
 453     destruct H
 454   | autobatch
 455   |4,5:
 456     simplify in H2;
 457     destruct H2
 458   | simplify in H1;
 459     destruct H1
 460   ]
 461 qed.
 462
 463 lemma mem_same_atom_to_exists:
 464  ∀f,l. mem ? same_atom f l = true → ∃n. f = FAtom n.
 465  intros 2;
 466  elim l;
 467   [ simplify in H;
 468     destruct H
 469   | simplify in H1;
 470     apply (bool_elim ? (same_atom f t));
 471     intros;
 472      [ elim (same_atom_to_exists ? ? H2);
 473        autobatch
 474      | rewrite > H2 in H1;
 475        simplify in H1;
 476        elim (H H1);
 477        autobatch
 478      ]
 479   ]
 480 qed.
 481
 482 lemma look_for_axiom:
 483  ∀l1,l2.
 484   (∃n,ll1,ll2,lr1,lr2. l1 = ll1 @ (FAtom n :: ll2) ∧ l2 = lr1 @ (FAtom n :: lr2))
 485   ∨ ∀n1. (mem ? same_atom (FAtom n1) l1 ∧ mem ? same_atom (FAtom n1) l2) = false.
 486  intro;
 487  elim l1 1; clear l1;
 488   [ intros;
 489     right;
 490     intros;
 491     simplify;
 492     reflexivity
 493   | intros;
 494     generalize in match (refl_eq ? (mem ? same_atom t l2));
 495     elim (mem ? same_atom t l2) in ⊢ (? ? ? %→?);
 496      [ left;
 497        elim (mem_to_exists_l1_l2 ? ? ? ? same_atom_to_eq H1);
 498        elim H2; clear H2;
 499        elim (mem_same_atom_to_exists ? ? H1);
 500        rewrite > H2 in H3;
 501        apply (ex_intro ? ? a2);
 502        rewrite > H2;
 503        apply (ex_intro ? ? []);
 504        simplify;
 505        autobatch depth=5
 506      | elim (H l2);
 507         [ left;
 508           decompose;
 509           apply (ex_intro ? ? a);
 510           apply (ex_intro ? ? (t::a1));
 511           simplify;
 512           apply (ex_intro ? ? a2);
 513           apply (ex_intro ? ? a3);
 514           autobatch
 515         | right;
 516           intro;
 517           apply (bool_elim ? (same_atom t (FAtom n1)));
 518            [ intro;
 519              rewrite > (eq_to_eq_mem ? ? transitiveb_same_atom ? ? ? H3) in H1;
 520              rewrite > H1;
 521              autobatch
 522            | intro;
 523              change in ⊢ (? ? (? % ?) ?) with
 524               (match same_atom (FAtom n1) t with
 525                 [true ⇒ true
 526                 |false ⇒ mem ? same_atom (FAtom n1) l
 527                 ]);
 528              rewrite > symmetricb_same_atom;
 529              rewrite > H3;
 530              simplify;
 531              apply H2
 532            ]
 533         ]
 534      ]
 535   ]
 536 qed.
 537
 538 lemma eq_plus_n_m_O_to_eq_m_O: ∀n,m.n+m=0 → m=0.
 539  intros 2;
 540  elim n;
 541   [ assumption
 542   | simplify in H1;
 543     destruct H1
 544   ]
 545 qed.
 546
 547 lemma not_eq_nil_append_cons: ∀A.∀l1,l2.∀x:A.¬ [] = l1 @ (x :: l2).
 548  intros;
 549  elim l1;
 550  simplify;
 551  intro;
 552   [ destruct H
 553   | destruct H1
 554   ]
 555 qed.
 556
 557 (*lemma foo: ∀x,l.
 558  (¬eval
 559    (λn:nat
 560     .match eqb n x with
 561      [true⇒true|false⇒mem Formula same_atom (FAtom n) l]) (and_of_list l)) =
 562  (¬eval
 563    (λn:nat.mem Formula same_atom (FAtom n) l) (and_of_list l)).
 564  intros;
 565  elim l;
 566   [ reflexivity
 567   | simplify in ⊢ (? ? (? (? ? %)) ?);
 568     change in ⊢ (? ? (? %) ?) with
 569      (eval (λn:nat
 570       .match eqb n x in bool return λb:bool.bool with
 571        [true⇒true|false⇒mem Formula same_atom (FAtom n) (t::l1)]) t
 572       ∧
 573       eval (λn:nat
 574       .match eqb n x in bool return λb:bool.bool with
 575        [true⇒true|false⇒mem Formula same_atom (FAtom n) (t::l1)])
 576       (and_of_list l1));
 577
 578
 579   ]
 580 qed.*)
 581
 582 axiom daemon: False.
 583
 584 lemma sizel_0_no_axiom_is_tautology:
 585  ∀l1,l2. size_of_sequent 〈l1,l2〉 = 0 → is_tautology (formula_of_sequent 〈l1,l2〉) →
 586   (∀n. (mem ? same_atom (FAtom n) l1 ∧ mem ? same_atom (FAtom n) l2) = false) →
 587    (∃ll1,ll2. l1 = ll1 @ (FFalse :: ll2)) ∨ (∃ll1,ll2. l2 = ll1 @ (FTrue :: ll2)).
 588  intros;
 589  lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
 590  simplify in Hletin;
 591  generalize in match Hletin; clear Hletin;
 592  generalize in match H2; clear H2;
 593  generalize in match H; clear H;
 594  elim l1 0;
 595   [ intros;
 596     simplify in H2;
 597     generalize in match H2; clear H2;
 598     generalize in match H1; clear H1;
 599     generalize in match H; clear H;
 600     elim l2 0;
 601      [ intros;
 602        simplify in H2;
 603        destruct H2
 604      | simplify;
 605        intro;
 606        elim t;
 607         [ right;
 608           apply (ex_intro ? ? []);
 609           simplify;
 610           autobatch
 611         | simplify in H3;
 612           simplify in H1;
 613           elim H;
 614            [ elim H4;
 615              elim H5;
 616              elim (not_eq_nil_append_cons ? ? ? ? H6)
 617            | elim H4;
 618              right;
 619              apply (ex_intro ? ? (FFalse::a));
 620              simplify;
 621              elim H5;
 622              apply (ex_intro ? ? a1);
 623              autobatch
 624            |3,4: autobatch
 625            | assumption
 626            ]
 627         | simplify in H1 H3;
 628           elim (H H1 H2 H3); clear H;
 629            [ elim H4;
 630              elim H;
 631              elim (not_eq_nil_append_cons ? ? ? ? H5)
 632            | right;
 633              elim H4;
 634              apply (ex_intro ? ? (FAtom n::a));
 635              simplify;
 636              elim H;
 637              autobatch
 638            ]
 639         |4,5:
 640           simplify in H3;
 641           destruct H3
 642         | simplify in H2;
 643           destruct H2
 644         ]
 645      ]
 646   | intro;
 647     elim t;
 648      [ elim H;
 649         [ left;
 650           elim H4;
 651           apply (ex_intro ? ? (FTrue::a));
 652           simplify;
 653           elim H5;
 654           autobatch
 655         | right;
 656           assumption
 657         | assumption
 658         | lapply (H2 n); clear H2;
 659           simplify in Hletin;
 660           assumption
 661         | simplify in H3;
 662           assumption
 663         ]
 664      | left;
 665        apply (ex_intro ? ? []);
 666        simplify;
 667        autobatch
 668      | elim H;
 669         [ left;
 670           elim H4;
 671           apply (ex_intro ? ? (FAtom n::a));
 672           simplify;
 673           elim H5;
 674           autobatch
 675         | right;
 676           assumption
 677         | assumption
 678         | lapply (H2 n1); clear H2;
 679           simplify in Hletin;
 680           generalize in match Hletin; clear Hletin;
 681           elim (eqb n1 n);
 682            [ simplify in H2;
 683              rewrite > H2;
 684              autobatch
 685            | simplify in H2;
 686              assumption
 687            ]
 688         | simplify in H2;
 689           lapply (H2 n); clear H2;
 690           rewrite > eqb_n_n in Hletin;
 691           simplify in Hletin;
 692           simplify in H3;
 693           rewrite > eqb_n_n in H3;
 694           simplify in H3;
 695 (*
 696           generalize in match H3;
 697           generalize in match H1; clear H1;
 698           generalize in match H; clear H;
 699           elim l 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                  | generalize in match H4; clear H4;
 718                    generalize in match H2; clear H2;
 719                    elim t1;
 720                     [
 721                     |
 722                     |
 723                     |4,5:
 724                       simplify in H5;
 725                       destruct H5
 726                     | simplify in H4;
 727                       destruct H4
 728                     ]
 729                  ]
 730               ]
 731            |
 732            ]
 733 *) elim daemon
 734         ]
 735      |4,5:
 736        simplify in H3;
 737        destruct H3
 738      | simplify in H2;
 739        destruct H2
 740      ]
 741   ]
 742 qed.
 743
 744 lemma completeness_base:
 745  ∀S. size_of_sequent S = 0 → is_tautology (formula_of_sequent S) → derive S.
 746  intro;
 747  elim S 1; clear S;
 748  simplify in ⊢ (?→%→?);
 749  intros;
 750  elim (look_for_axiom t t1);
 751   [ decompose;
 752     rewrite > H2; clear H2;
 753     rewrite > H4; clear H4;
 754     apply (ExchangeL ? a1 a2 (FAtom a));
 755     apply (ExchangeR ? a3 a4 (FAtom a));
 756     apply Axiom
 757   | elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2);
 758      [ decompose;
 759        rewrite > H3;
 760        apply (ExchangeL ? a a1 FFalse);
 761        apply FalseL
 762      | decompose;
 763        rewrite > H3;
 764        apply (ExchangeR ? a a1 FTrue);
 765        apply TrueR
 766      ]
 767   ]
 768 qed.
 769
 770 (*
 771 lemma completeness_step:
 772  ∀l1,l2,n. size_of_sequent 〈l1,l2〉 = S n →
 773    (∃ll1,ll2,f. l1 = ll1 @ (f::ll2) ∧ size f > 0) ∨
 774    (∃ll1,ll2,f. l2 = ll1 @ (f::ll2) ∧ size f > 0).
 775  intros 3;
 776  elim l1 0;
 777   [ elim l2 0;
 778      [ intros;
 779        simplify in H;
 780        destruct H
 781      | intros 3;
 782        elim t;
 783         [ elim (H H1);
 784            [ left;
 785              assumption
 786            | right;
 787              decompose;
 788              apply (ex_intro ? ? (FTrue::a));
 789              simplify;
 790              autobatch depth=5
 791            ]
 792         | elim (H H1);
 793            [ left;
 794              assumption
 795            | right;
 796              decompose;
 797              apply (ex_intro ? ? (FFalse::a));
 798              simplify;
 799              autobatch depth=5
 800            ]
 801         | elim (H H1);
 802            [ left;
 803              assumption
 804            | right;
 805              decompose;
 806              apply (ex_intro ? ? (FAtom n1::a));
 807              simplify;
 808              autobatch depth=5
 809            ]
 810         | right;
 811           apply (ex_intro ? ? []);
 812           simplify;
 813           apply (ex_intro ? ? l);
 814           apply (ex_intro ? ? (FAnd f f1));
 815           simplify;
 816           split;
 817            [ reflexivity
 818            | unfold gt;
 819              autobatch
 820            ]
 821         | right;
 822           apply (ex_intro ? ? []);
 823           simplify;
 824           apply (ex_intro ? ? l);
 825           apply (ex_intro ? ? (FOr f f1));
 826           simplify;
 827           split;
 828            [ reflexivity
 829            | unfold gt;
 830              autobatch
 831            ]
 832         | right;
 833           apply (ex_intro ? ? []);
 834           simplify;
 835           apply (ex_intro ? ? l);
 836           apply (ex_intro ? ? (FNot f));
 837           simplify;
 838           split;
 839            [ reflexivity
 840            | unfold gt;
 841              autobatch
 842            ]
 843         ]
 844      ]
 845   | intros 2;
 846     elim t;
 847      [1,2:(*,2,3:*)
 848        elim (H H1);
 849        decompose;
 850         [ left;
 851           autobatch depth=5
 852         | right;
 853           autobatch depth=5
 854         ]
 855      | left;
 856        apply (ex_intro ? ? []);
 857        simplify;
 858        apply (ex_intro ? ? l);
 859        apply (ex_intro ? ? (FAnd f f1));
 860        unfold gt;
 861        simplify;
 862        autobatch
 863      | left;
 864        apply (ex_intro ? ? []);
 865        simplify;
 866        apply (ex_intro ? ? l);
 867        apply (ex_intro ? ? (FOr f f1));
 868        unfold gt;
 869        simplify;
 870        autobatch
 871      | left;
 872        apply (ex_intro ? ? []);
 873        simplify;
 874        apply (ex_intro ? ? l);
 875        apply (ex_intro ? ? (FNot f));
 876        unfold gt;
 877        simplify;
 878        autobatch
 879      ]
 880   ]
 881 qed.
 882
 883 theorem completeness: ∀S. is_tautology (formula_of_sequent S) → derive S.
 884  intro;
 885  generalize in match (refl_eq ? (size_of_sequent S));
 886  elim (size_of_sequent S) in ⊢ (? ? ? %→?);
 887   [ apply completeness_base;
 888     assumption
 889   |
 890   ]
 891 qed.
 892
 893  elim F;
 894   [ autobatch
 895   | simplify in H;
 896     lapply (H (λx.true));
 897     destruct Hletin
 898   | simplify in H;
 899     lapply (H (λx.false));
 900     destruct Hletin
 901   | apply AndR;
 902      [ apply H;
 903        intro;
 904        lapply (H2 i); clear H2;
 905        simplify in Hletin;
 906        autobatch
 907      | apply H1;
 908        intro;
 909        lapply (H2 i); clear H2;
 910        simplify in Hletin;
 911        autobatch
 912      ]
 913   | apply OrR;
 914     simplify in H2;
 915   | apply NotR;
 916     simplify in H1;
 917 *)