X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpropositional_sequent_calculus.ma;h=42ae9682532ce8f65811f23944ec7e0f2a83cf0c;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=9bd89394d3fca58ed9579524a83566181231aae2;hpb=f5d8ab6a1c8bdf2d54e9961ac5899d9f001160c2;p=helm.git

diff --git a/helm/software/matita/library/demo/propositional_sequent_calculus.ma b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
index 9bd89394d..42ae96825 100644
--- a/helm/software/matita/library/demo/propositional_sequent_calculus.ma
+++ b/helm/software/matita/library/demo/propositional_sequent_calculus.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/demo/propositional_sequent_calculus/".
-
 include "nat/plus.ma".
 include "nat/compare.ma".
 include "list/sort.ma".
@@ -157,17 +155,16 @@ inductive derive: sequent → Prop ≝
  | NotL: ∀l1,l2,f.
     derive 〈l1,f::l2〉 → derive 〈FNot f :: l1,l2〉.
 
-alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)".
 let rec and_of_list l ≝
  match l with
-  [ Nil ⇒ FTrue
-  | Cons F l' ⇒ FAnd F (and_of_list l')
+  [ nil ⇒ FTrue
+  | cons F l' ⇒ FAnd F (and_of_list l')
   ].
 
 let rec or_of_list l ≝
  match l with
-  [ Nil ⇒ FFalse
-  | Cons F l' ⇒ FOr F (or_of_list l')
+  [ nil ⇒ FFalse
+  | cons F l' ⇒ FOr F (or_of_list l')
   ].
 
 definition formula_of_sequent ≝
@@ -184,6 +181,8 @@ axiom symm_andb: symmetric ? andb.
 axiom associative_andb: associative ? andb.
 axiom distributive_andb_orb: distributive ? andb orb.
 
+lemma andb_true: ∀x.(true ∧ x) = x. intro; reflexivity. qed. 
+
 lemma and_of_list_permut:
  ∀i,f,l1,l2. eval i (and_of_list (l1 @ (f::l2))) = eval i (and_of_list (f :: l1 @ l2)).
  intros;
@@ -245,11 +244,20 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
     lapply (H4 i); clear H4;
     rewrite > symm_orb in ⊢ (? ? (? ? %) ?);
     rewrite > distributive_orb_andb;
+    demodulate.
+    reflexivity.
+    (*
     autobatch paramodulation
+      by distributive_orb_andb,symm_orb,symm_orb, 
+         Hletin, Hletin1,andb_true.
+    *)
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
-    autobatch
+    pump 100. pump 100.
+    demodulate.
+    reflexivity. 
+    (* autobatch paramodulation by andb_assoc, Hletin. *) 
   | simplify in H2 H4 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
@@ -259,11 +267,13 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
     rewrite > demorgan2;
     rewrite > symm_orb;
     rewrite > distributive_orb_andb;
-    autobatch paramodulation
+    demodulate.
+    reflexivity.
+    (* autobatch paramodulation by symm_andb,symm_orb,andb_true,Hletin,Hletin1. *)
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
-    autobatch
+    autobatch paramodulation;
   | simplify in H2 ⊢ %;
     intros;
     lapply (H2 i); clear H2;
@@ -276,7 +286,6 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
 qed.
 
 alias num (instance 0) = "natural number".
-alias symbol "plus" = "natural plus".
 let rec size F ≝
  match F with
   [ FTrue ⇒ 0
@@ -289,8 +298,8 @@ let rec size F ≝
 
 let rec sizel l ≝
  match l with
-  [ Nil ⇒ 0
-  | Cons F l' ⇒ size F + sizel l'
+  [ nil ⇒ 0
+  | cons F l' ⇒ size F + sizel l'
   ].
 
 definition size_of_sequent ≝
@@ -311,8 +320,7 @@ definition same_atom : Formula → Formula → bool.
 qed.
 
 definition symmetricb ≝
- λA:Type.λeq:A → A → bool.
-  ∀x,y. eq x y = eq y x.
+ λA:Type.λeq:A → A → bool. ∀x,y. eq x y = eq y x.
 
 theorem symmetricb_eqb: symmetricb ? eqb.
  intro;
@@ -399,7 +407,7 @@ theorem mem_to_exists_l1_l2:
   [ simplify in H1;
     destruct H1
   | simplify in H2;
-    apply (bool_elim ? (eq n t));
+    apply (bool_elim ? (eq n a));
     intro;
      [ apply (ex_intro ? ? []);
        apply (ex_intro ? ? l1);
@@ -411,8 +419,8 @@ theorem mem_to_exists_l1_l2:
        elim (H H1 H2);
        elim H4;
        rewrite > H5;
-       apply (ex_intro ? ? (t::a));
-       apply (ex_intro ? ? a1);
+       apply (ex_intro ? ? (a::a1));
+       apply (ex_intro ? ? a2);
        simplify;
        reflexivity
      ]
@@ -425,8 +433,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
   [1,2:
     simplify in H;
     destruct H
-  | generalize in match H; clear H;
-    elim f2;
+  | elim f2 in H ⊢ %;
      [1,2:
        simplify in H;
        destruct H
@@ -436,7 +443,7 @@ lemma same_atom_to_eq: ∀f1,f2. same_atom f1 f2 = true → f1=f2.
      |4,5:
        simplify in H2;
        destruct H2
-     | simplify in H2;
+     | simplify in H1;
        destruct H1
      ]
   |4,5:
@@ -470,7 +477,7 @@ lemma mem_same_atom_to_exists:
   [ simplify in H;
     destruct H
   | simplify in H1;
-    apply (bool_elim ? (same_atom f t));
+    apply (bool_elim ? (same_atom f a));
     intros;
      [ elim (same_atom_to_exists ? ? H2);
        autobatch
@@ -494,14 +501,14 @@ lemma look_for_axiom:
     simplify;
     reflexivity
   | intros;
-    generalize in match (refl_eq ? (mem ? same_atom t l2));
-    elim (mem ? same_atom t l2) in ⊢ (? ? ? %→?);
+    generalize in match (refl_eq ? (mem ? same_atom a l2));
+    elim (mem ? same_atom a l2) in ⊢ (? ? ? %→?);
      [ left;
        elim (mem_to_exists_l1_l2 ? ? ? ? same_atom_to_eq H1);
        elim H2; clear H2;
        elim (mem_same_atom_to_exists ? ? H1);
        rewrite > H2 in H3;
-       apply (ex_intro ? ? a2);
+       apply (ex_intro ? ? a3);
        rewrite > H2;
        apply (ex_intro ? ? []);
        simplify;
@@ -509,22 +516,22 @@ lemma look_for_axiom:
      | elim (H l2);
         [ left;
           decompose;
-          apply (ex_intro ? ? a);
-          apply (ex_intro ? ? (t::a1));
+          apply (ex_intro ? ? a1);
+          apply (ex_intro ? ? (a::a2));
           simplify;
-          apply (ex_intro ? ? a2);
           apply (ex_intro ? ? a3);
-          autobatch
+          apply (ex_intro ? ? a4);
+          autobatch depth=4
         | right;
           intro;
-          apply (bool_elim ? (same_atom t (FAtom n1)));
+          apply (bool_elim ? (same_atom a (FAtom n1)));
            [ intro;
              rewrite > (eq_to_eq_mem ? ? transitiveb_same_atom ? ? ? H3) in H1;
              rewrite > H1;
              autobatch
            | intro;
              change in ⊢ (? ? (? % ?) ?) with
-              (match same_atom (FAtom n1) t with
+              (match same_atom (FAtom n1) a with
                 [true ⇒ true
                 |false ⇒ mem ? same_atom (FAtom n1) l
                 ]);
@@ -591,22 +598,16 @@ lemma sizel_0_no_axiom_is_tautology:
  intros;
  lapply (H1 (λn.mem ? same_atom (FAtom n) l1)); clear H1;
  simplify in Hletin;  
- generalize in match Hletin; clear Hletin;
- generalize in match H2; clear H2;
- generalize in match H; clear H;
- elim l1 0;
+ elim l1 in Hletin H2 H ⊢ % 0;
   [ intros;
     simplify in H2;
-    generalize in match H2; clear H2;
-    generalize in match H1; clear H1;
-    generalize in match H; clear H;
-    elim l2 0;
+    elim l2 in H2 H1 H ⊢ % 0;
      [ intros;
        simplify in H2;
        destruct H2
      | simplify;
        intro;
-       elim t;
+       elim a;
         [ right;
           apply (ex_intro ? ? []);
           simplify;
@@ -619,10 +620,10 @@ lemma sizel_0_no_axiom_is_tautology:
              elim (not_eq_nil_append_cons ? ? ? ? H6)
            | elim H4;
              right;
-             apply (ex_intro ? ? (FFalse::a));
+             apply (ex_intro ? ? (FFalse::a1));
              simplify;
              elim H5;
-             apply (ex_intro ? ? a1);
+             apply (ex_intro ? ? a2);
              autobatch
            |3,4: autobatch
            | assumption
@@ -634,7 +635,7 @@ lemma sizel_0_no_axiom_is_tautology:
              elim (not_eq_nil_append_cons ? ? ? ? H5)
            | right;
              elim H4;
-             apply (ex_intro ? ? (FAtom n::a));
+             apply (ex_intro ? ? (FAtom n::a1));
              simplify;
              elim H;
              autobatch
@@ -647,11 +648,11 @@ lemma sizel_0_no_axiom_is_tautology:
         ]
      ]
   | intro;
-    elim t;
+     elim a;
      [ elim H;
         [ left;
           elim H4;
-          apply (ex_intro ? ? (FTrue::a));
+          apply (ex_intro ? ? (FTrue::a1));
           simplify;
           elim H5;
           autobatch
@@ -671,7 +672,7 @@ lemma sizel_0_no_axiom_is_tautology:
      | elim H;
         [ left;
           elim H4;
-          apply (ex_intro ? ? (FAtom n::a));
+          apply (ex_intro ? ? (FAtom n::a1));
           simplify;
           elim H5;
           autobatch
@@ -680,8 +681,7 @@ lemma sizel_0_no_axiom_is_tautology:
         | assumption
         | lapply (H2 n1); clear H2;
           simplify in Hletin;
-          generalize in match Hletin; clear Hletin;
-          elim (eqb n1 n);
+          elim (eqb n1 n) in Hletin ⊢ %;
            [ simplify in H2;
              rewrite > H2;
              autobatch
@@ -696,10 +696,7 @@ lemma sizel_0_no_axiom_is_tautology:
           rewrite > eqb_n_n in H3;
           simplify in H3;
 (*
-          generalize in match H3;
-          generalize in match H1; clear H1;
-          generalize in match H; clear H;
-          elim l 0;
+          elim l in H3 H1 H ⊢ % 0;
            [ elim l2 0;
               [ intros;
                 simplify in H2;
@@ -717,9 +714,7 @@ lemma sizel_0_no_axiom_is_tautology:
                  ]
                     
                  [ autobatch
-                 | generalize in match H4; clear H4;
-                   generalize in match H2; clear H2;
-                   elim t1;
+                 | elim t1 in H4 H2 ⊢ %;
                     [
                     |
                     |
@@ -750,22 +745,22 @@ lemma completeness_base:
  elim S 1; clear S;
  simplify in ⊢ (?→%→?);
  intros;
- elim (look_for_axiom t t1);
+ elim (look_for_axiom a b);
   [ decompose;
     rewrite > H2; clear H2;
     rewrite > H4; clear H4;
-    apply (exchangeL ? a1 a2 (FAtom a));
-    apply (exchangeR ? a3 a4 (FAtom a));
-    apply axiom 
-  | elim (sizel_0_no_axiom_is_tautology t t1 H H1 H2);
+    apply (ExchangeL ? a2 a3 (FAtom a1));
+    apply (ExchangeR ? a4 a5 (FAtom a1));
+    apply Axiom 
+  | elim (sizel_0_no_axiom_is_tautology a b H H1 H2);
      [ decompose;
        rewrite > H3;
-       apply (exchangeL ? a a1 FFalse);
-       apply falseL
+       apply (ExchangeL ? a1 a2 FFalse);
+       apply FalseL
      | decompose;
        rewrite > H3;
-       apply (exchangeR ? a a1 FTrue);
-       apply trueR
+       apply (ExchangeR ? a1 a2 FTrue);
+       apply TrueR
      ]
   ]
 qed.
@@ -918,4 +913,3 @@ qed.
   | apply NotR;
     simplify in H1;
 *)
-*)