- destruct tactic: automatic simplification in case of failure removed

[helm.git] / matita / library / demo / propositional_sequent_calculus.ma

diff --git a/matita/library/demo/propositional_sequent_calculus.ma b/matita/library/demo/propositional_sequent_calculus.ma
index 9bd89394d3fca58ed9579524a83566181231aae2..f68cfd22cbba1a47ac928e4b417073bbc00d4924 100644 (file)
--- a/matita/library/demo/propositional_sequent_calculus.ma
+++ b/matita/library/demo/propositional_sequent_calculus.ma
@@ -157,17 +157,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 ≝
@@ -276,7 +275,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 +287,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 +309,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;
@@ -436,7 +433,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:
@@ -754,18 +751,18 @@ lemma completeness_base:
   [ decompose;
     rewrite > H2; clear H2;
     rewrite > H4; clear H4;
-    apply (exchangeL ? a1 a2 (FAtom a));
-    apply (exchangeR ? a3 a4 (FAtom a));
-    apply axiom 
+    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);
      [ decompose;
        rewrite > H3;
-       apply (exchangeL ? a a1 FFalse);
-       apply falseL
+       apply (ExchangeL ? a a1 FFalse);
+       apply FalseL
      | decompose;
        rewrite > H3;
-       apply (exchangeR ? a a1 FTrue);
-       apply trueR
+       apply (ExchangeR ? a a1 FTrue);
+       apply TrueR
      ]
   ]
 qed.
@@ -918,4 +915,3 @@ qed.
   | apply NotR;
     simplify in H1;
 *)
-*)