From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 15 Nov 2008 12:52:22 +0000 (+0000)
Subject: natural deduction palette
X-Git-Tag: make_still_working~4563
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88f24d23df67d88bf98c2ca32ac0d9854f3d9b00;p=helm.git

natural deduction palette
---

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
index ba0f565e4..64b3daccb 100644
--- a/helm/software/matita/library/demo/natural_deduction.ma
+++ b/helm/software/matita/library/demo/natural_deduction.ma
@@ -14,16 +14,68 @@
 
 include "demo/natural_deduction_support.ma".
 
-lemma ex1 : ΠA,B,C,E: CProp.
+lemma RAA_to_EM : A ∨ ¬ A.
 
-   (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
+  apply (prove (A ∨ ¬ A));
+  
+  apply (RAA [H] ⊥);
+  apply (¬_e (¬A) A);
+    [ apply (¬_i [H1] ⊥);
+      apply (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply [H];
+      | apply (∨_i_l A);
+        apply [H1];
+      ]
+    | apply (RAA [H2] ⊥);
+      apply (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply [H];
+      | apply (∨_i_r (¬A));
+        apply [H2];
+      ]
+    ]
+qed.
+
+lemma RA_to_EM1 : A ∨ ¬ A.
+
+  apply (prove (A ∨ ¬ A));
+  
+  apply (RAA [H] ⊥);
+  apply (¬_e (¬¬A) (¬A));
+    [ apply (¬_i [H2] ⊥);
+      apply (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply [H];
+      | apply (∨_i_r (¬A));
+        apply [H2];
+      ]
+    | apply (¬_i [H1] ⊥);
+      apply (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply [H];
+      | apply (∨_i_l A);
+        apply [H1];
+      ]
+    ]
+qed.
 
- intros 4 (A B C E);apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
+lemma ex0 : (A ⇒ ⊥) ⇒ A ⇒ B ∧ ⊤. 
  
- (*NICE: TRY THIS ERROR! 
- apply (⇒_i [H] (A∧C⇒E∧E∧C∨B));
- apply (⇒_i [K] (E∧E∧C∨B));
-  OR DO THE RIGHT THING *)
+  apply (prove ((A ⇒ ⊥) ⇒ A ⇒ B∧⊤));
+  
+  apply (⇒_i [H] (A ⇒ B∧⊤));
+  apply (⇒_i [H1] (B∧⊤));
+  apply (∧_i B ⊤);
+  [ apply (⊥_e ⊥);
+    apply (⇒_e (A ⇒ ⊥) A); 
+    [ apply [H];
+    | apply [H1];
+    ]
+  | apply (⊤_i);
+  ]
+qed.
+
+lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
+
+ apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
+   
  apply (⇒_i [H] (A∧C⇒E∧C∨B));
  apply (⇒_i [K] (E∧C∨B));
  apply (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
@@ -40,6 +92,17 @@ lemma ex1 : ΠA,B,C,E: CProp.
 ]
 qed.
 
+lemma dmg : ¬(A ∨ B) ⇒ ¬A ∧ ¬B.
+
+  apply (prove (¬(A ∨ B) ⇒ ¬A ∧ ¬B));
+  apply (⇒_i [H] (¬A ∧ ¬B));
+  
+  apply (¬_e (¬A) A);
+  
+  
+
+
+(*
 lemma ex2: ΠN:Type.ΠR:N→N→CProp.
 
    (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
@@ -60,3 +123,4 @@ lemma ex2: ΠN:Type.ΠR:N→N→CProp.
      ]
   ]
 qed.
+*)
\ No newline at end of file
diff --git a/helm/software/matita/library/demo/natural_deduction_support.ma b/helm/software/matita/library/demo/natural_deduction_support.ma
index a3613e51d..3969197e9 100644
--- a/helm/software/matita/library/demo/natural_deduction_support.ma
+++ b/helm/software/matita/library/demo/natural_deduction_support.ma
@@ -1,158 +1,438 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
+(* Logic system *)
 
-axiom cast: ∀A,B:CProp.B → A.
-
-notation > "'prove' p" non associative with precedence 19 for @{ cast ? $p}. 
+inductive Imply (A,B:CProp) : CProp ≝
+| Imply_intro: (A → B) → Imply A B.
+ 
+definition Imply_elim ≝ λA,B.λf:Imply A B. λa:A.
+  match f with [ Imply_intro g ⇒ g a].
 
-notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (b) (? \ERROR)" with precedence 19
-for @{ 'caste $a $b $t }.
+inductive And (A,B:CProp) : CProp ≝
+| And_intro: A → B → And A B.
 
-interpretation "cast ERR" 'caste a b t = (cast a b t).
+definition And_elim_l ≝ λA,B.λc:And A B.
+  match c with [ And_intro a b ⇒ a ].
 
-notation < "\infrule (t\atop ⋮) a ?" with precedence 19 for @{ 'cast $a $t }.
+definition And_elim_r ≝ λA,B.λc:And A B.
+  match c with [ And_intro a b ⇒ b ].
 
-interpretation "cast OK" 'cast a t = (cast a a t).
+inductive Or (A,B:CProp) : CProp ≝
+| Or_intro_l: A → Or A B
+| Or_intro_r: B → Or A B. 
+ 
+definition Or_elim ≝ λA,B,C:CProp.λc:Or A B.λfa: A → C.λfb: B → C.
+  match c with 
+  [ Or_intro_l a ⇒ fa a 
+  | Or_intro_r b ⇒ fb b].
 
-definition assumpt ≝ λA:CProp.λa:A.a.
+inductive Top : CProp := 
+| Top_intro : Top.
 
-notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 for @{ 'asse $a $H }.
-interpretation "assumption" 'asse a H = (cast _ _ (assumpt a (cast _ _ H))).
+inductive Bot : CProp := .
 
-notation < "[ a ] \sup H" with precedence 19 for @{ 'ass $a $H }.
-interpretation "assumption" 'ass a H = (cast a a  (assumpt a (cast a a H))).
+definition Bot_elim ≝ λP:CProp.λx:Bot.
+  match x in Bot return λx.P with []. 
 
-inductive Imply (A,B:CProp) : CProp ≝
- Imply_intro: (A → B) → Imply A B.
- 
-notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
-interpretation "Imply" 'Imply a b = (Imply a b).
+definition Not := λA:CProp.Imply A Bot.
 
-notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000(ab) (⇒\sub\i \emsp ident H \ERROR) " with precedence 19
-for @{ 'Imply_introe $xxx $ab (λ${ident H}:$p.$b) }.
-interpretation "Imply_intro" 'Imply_introe xxx ab \eta.b = (cast xxx ab (Imply_intro _ _ b)).
+definition Not_intro : ∀A.(A → Bot) → Not A ≝  λA. 
+  Imply_intro A Bot.
 
-notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
-for @{ 'Imply_intro $ab (λ${ident H}:$p.$b) }.
-interpretation "Imply_intro" 'Imply_intro ab \eta.b = (cast ab ab (Imply_intro _ _ b)).
+definition Not_elim : ∀A.Not A → A → Bot ≝ λA. 
+  Imply_elim ? Bot.  
 
-definition Imply_elim ≝ λA,B.λf:Imply A B.λa:A.match f with [ Imply_intro g ⇒ g a].
+definition assumpt := λA:CProp.λa:A.
+  a.
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim $ab $a $b }.
-interpretation "Imply_elim" 'Imply_elim ab a b = (cast _ b (Imply_elim _ _ ab a)).
+axiom Raa : ∀A.(Not A → Bot) → A.
 
-inductive And (A,B:CProp) : CProp ≝
- And_intro: A → B → And A B.
+(* Dummy proposition *)
+axiom unit : CProp.
 
+(* Notations *)
+notation "hbox(a break ⇒ b)" right associative with precedence 20 
+for @{ 'Imply $a $b }.
+interpretation "Imply" 'Imply a b = (Imply a b).
+interpretation "constructive or" 'or x y = (Or x y).
 interpretation "constructive and" 'and x y = (And x y).
+notation "⊤" non associative with precedence 90 for @{'Top}.
+interpretation "Top" 'Top = Top.
+notation "⊥" non associative with precedence 90 for @{'Bot}.
+interpretation "Bot" 'Bot = Bot.
+interpretation "Not" 'not a = (Not a).
+notation "✶" non associative with precedence 90 for @{'unit}.
+interpretation "dummy prop" 'unit = unit.
+
+(* Variables *)
+axiom A : CProp.
+axiom B : CProp.
+axiom C : CProp.
+axiom D : CProp.
+axiom E : CProp.
+axiom F : CProp.
+axiom G : CProp.
+axiom H : CProp.
+axiom I : CProp.
+axiom J : CProp.
+axiom K : CProp.
+axiom L : CProp.
+axiom M : CProp.
+axiom N : CProp.
+axiom O : CProp.
+axiom P : CProp.
+axiom Q : CProp.
+axiom R : CProp.
+axiom S : CProp.
+axiom T : CProp.
+axiom U : CProp.
+axiom V : CProp.
+axiom W : CProp.
+axiom X : CProp.
+axiom Y : CProp.
+axiom Z : CProp.
+
+(* Every formula user provided annotates its proof A becomes (show A ?) *)
+definition show : ∀A.A→A ≝ λA:CProp.λa:A.a.
+
+(* When something does not fit, this daemon is used *)
+axiom cast: ∀A,B:CProp.B → A.
 
-notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19 for @{ 'And_intro $a $b $ab }.
-interpretation "And_intro" 'And_intro a b ab = (cast _ ab (And_intro _ _ a b)).
-
-definition And_elim_l ≝
- λA,B.λc:A∧B.match c with [ And_intro a b ⇒ a ].
 
-notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19 for @{ 'And_elim_l $ab $a }.
-interpretation "And_elim_l" 'And_elim_l ab a = (cast _ a (And_elim_l _ _ ab)).
+notation > "'prove' p" non associative with precedence 19 
+for @{ 'prove $p }.
+interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
+interpretation "prove OK" 'prove p = (show p _).
 
-definition And_elim_r ≝
- λA,B.λc:A∧B.match c with [ And_intro a b ⇒ b ].
+notation < "\infrule (t\atop ⋮) a ?" with precedence 19 for @{ 'leaf_ok $a $t }.
+interpretation "leaf OK" 'leaf_ok a t = (show a t).
+notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 for @{ 'leaf_ko $a $t }.
+interpretation "leaf KO" 'leaf_ko a t = (cast _ a (show _ t)).
 
-notation < "\infrule hbox(\emsp ab \emsp) b (∧\sub(\e_\r))" with precedence 19 for @{ 'And_elim_r $ab $b }.
-interpretation "And_elim_r" 'And_elim_r ab b = (cast _ b (And_elim_r _ _ ab)).
+notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 for @{ 'assumpt_ko $a $H }.
+interpretation "assumption_ko 1" 'assumpt_ko a H = (show a (cast _ _ (assumpt _ H))).
+interpretation "assumption_ko 2" 'assumpt_ko a H = (cast _ _ (show a (cast _ _ (assumpt _ H)))).
 
-inductive Or (A,B:CProp) : CProp ≝
- | Or_intro_l: A → Or A B
- | Or_intro_r: B → Or A B. 
- 
-interpretation "constructive or" 'or x y = (Or x y).
+notation < "[ a ] \sup H" with precedence 19 for @{ 'assumpt_ok $a $H }.
+interpretation "assumption_ok 1" 'assumpt_ok a H = (show a (assumpt a H)).
+notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 for @{ 'assumpt_ok_2 $a $H }.
+interpretation "assumption_ok 2" 'assumpt_ok_2 a H = (cast _ _ (show a (assumpt a H))).
 
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19 for @{ 'Or_intro_l $a $ab }.
-interpretation "Or_intro_l" 'Or_intro_l a ab = (cast _ ab (Or_intro_l _ _ a)).
+notation > "[H]" with precedence 90 for @{ 'assumpt $H }.
+interpretation "assumpt KO" 'assumpt H = (cast _ _ (assumpt _ H)).
+interpretation "assumpt OK" 'assumpt H = (assumpt _ H).
 
-notation < "\infrule hbox(\emsp b \emsp) ab (∨\sub(\i_\r))" with precedence 19 for @{ 'Or_intro_r $b $ab }.
-interpretation "Or_intro_r" 'Or_intro_r b ab = (cast _ ab (Or_intro_r _ _ b)).
+notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
+for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
+interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = 
+  (show ab (cast _ _ (Imply_intro _ _ b))).
 
-definition Or_elim ≝
- λA,B,C:CProp.λc:A∨B.λfa: A → C.λfb: B → C.
-  match c with [ Or_intro_l a ⇒ fa a | Or_intro_r b ⇒ fb b].
+notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
+for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
+interpretation "Imply_intro_ko_1" 'Imply_intro_ko_2 ab \eta.b = 
+  (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
-for @{ 'Or_elim $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
-interpretation "Or_elim" 'Or_elim ab \eta.ac \eta.bc c = (cast _ c (Or_elim _ _ _ ab ac bc)).
+notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
+for @{ 'Imply_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
+interpretation "Imply_intro_ok_1" 'Imply_intro_ok_1 ab \eta.b = 
+  (show ab (Imply_intro _ _ b)).
 
-inductive Exists (A:Type) (P:A→CProp) : CProp ≝
-  Exists_intro: ∀w:A. P w → Exists A P.
+notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (⇒\sub\i \emsp ident H) " with precedence 19
+for @{ 'Imply_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
+interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b = 
+  (cast _ _ (show ab (Imply_intro _ _ b))).
 
-interpretation "constructive ex" 'exists \eta.x = (Exists _ x).
+notation > "⇒_'i' [ident H] term 90 b" with precedence 19
+for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
+interpretation "Imply_intro KO" 'Imply_intro b pb = (cast _ (Imply unit b) (Imply_intro _ b pb)).
+interpretation "Imply_intro OK" 'Imply_intro b pb = (Imply_intro _ b pb).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_1 $ab $a $b }.
+interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b = 
+  (show b (cast _ _ (Imply_elim _ _ ab a))).
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_2 $ab $a $b }.
+interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b = 
+  (cast _ _ (show b (cast _ _ (Imply_elim _ _ ab a)))).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19 
+for @{ 'Imply_elim_ok_1 $ab $a $b }.
+interpretation "Imply_elim_ok_1" 'Imply_elim_ok_1 ab a b = 
+  (show b (Imply_elim _ _ ab a)).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (⇒\sub\e) " with precedence 19 
+for @{ 'Imply_elim_ok_2 $ab $a $b }.
+interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b = 
+  (cast _ _ (show b (Imply_elim _ _ ab a))).
+
+notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
+interpretation "Imply_elim KO" 'Imply_elim ab a = (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
+interpretation "Imply_elim OK" 'Imply_elim ab a = (Imply_elim _ _ ab a). 
+
+notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_1 $a $b $ab }.
+interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab = 
+  (show ab (cast _ _ (And_intro _ _ a b))).
+notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_2 $a $b $ab }.
+interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab = 
+  (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
+
+notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab (∧\sub\i)" with precedence 19 
+for @{ 'And_intro_ok_1 $a $b $ab }.
+interpretation "And_intro_ok_1" 'And_intro_ok_1 a b ab = 
+  (show ab (And_intro _ _ a b)).
+
+notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) (∧\sub\i)" with precedence 19 
+for @{ 'And_intro_ok_2 $a $b $ab }.
+interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab = 
+  (cast _ _ (show ab (And_intro _ _ a b))).
+
+notation > "∧_'i' term 90 a term 90 b" with precedence 19 for @{ 'And_intro (show $a ?) (show $b ?) }.
+interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)).
+interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b).
+
+notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 
+for @{ 'And_elim_l_ko_1 $ab $a }.
+interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a = 
+  (show a (cast _ _ (And_elim_l _ _ ab))).
+
+notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 
+for @{ 'And_elim_l_ko_2 $ab $a }.
+interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a = 
+  (cast _ _ (show a (cast _ _ (And_elim_l _ _ ab)))).
+
+notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19 
+for @{ 'And_elim_l_ok_1 $ab $a }.
+interpretation "And_elim_l_ok_1" 'And_elim_l_ok_1 ab a = 
+  (show a (And_elim_l _ _ ab)).
+
+notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\l))" with precedence 19 
+for @{ 'And_elim_l_ok_2 $ab $a }.
+interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a = 
+  (cast _ _ (show a (And_elim_l _ _ ab))).
 
-notation < "\infrule hbox(\emsp Pn \emsp) Px (∃\sub\i)" with precedence 19
-for @{ 'Exists_intro $Pn $Px }.
-interpretation "Exists_intro" 'Exists_intro Pn Px = (cast _ Px (Exists_intro _ _ _ Pn)).
+notation > "∧_'e_l' term 90 ab" with precedence 19
+for @{ 'And_elim_l (show $ab ?) }.
+interpretation "And_elim_l KO" 'And_elim_l a = (And_elim_l _ _ (cast (And _ unit) _ a)).
+interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a).
+
+notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 
+for @{ 'And_elim_r_ko_1 $ab $a }.
+interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a = 
+  (show a (cast _ _ (And_elim_r _ _ ab))).
+
+notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 
+for @{ 'And_elim_r_ko_2 $ab $a }.
+interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a = 
+  (cast _ _ (show a (cast _ _ (And_elim_r _ _ ab)))).
+
+notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19 
+for @{ 'And_elim_r_ok_1 $ab $a }.
+interpretation "And_elim_r_ok_1" 'And_elim_r_ok_1 ab a = 
+  (show a (And_elim_r _ _ ab)).
+
+notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) (∧\sub(\e_\r))" with precedence 19 
+for @{ 'And_elim_r_ok_2 $ab $a }.
+interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a = 
+  (cast _ _ (show a (And_elim_r _ _ ab))).
 
-definition Exists_elim ≝
-  λA:Type.λP:A→CProp.λC:CProp.λc:∃x:A.P x.λH:(∀x.P x → C).
-   match c with [ Exists_intro w p ⇒ H w p ].
+notation > "∧_'e_r' term 90 ab" with precedence 19
+for @{ 'And_elim_r (show $ab ?) }.
+interpretation "And_elim_r KO" 'And_elim_r a = (And_elim_r _ _ (cast (And unit _) _ a)).
+interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a).
+
+notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19 
+for @{ 'Or_intro_l_ok_1 $a $ab }.
+interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = 
+  (show ab (Or_intro_l _ _ a)).
+
+notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 
+for @{ 'Or_intro_l_ok_1 $a $ab }.
+interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = 
+  (cast _ _ (show ab (Or_intro_l _ _ a))).
+
+notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 
+for @{ 'Or_intro_l_ko_1 $a $ab }.
+interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab = 
+  (show ab (cast _ _ (Or_intro_l _ _ a))).
+
+notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 
+for @{ 'Or_intro_l_ko_2 $a $ab }.
+interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab = 
+  (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
 
-notation < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e \emsp ident n \emsp ident HPn)" with precedence 19
-for @{ 'Exists_elim $ExPx (λ${ident n}:$tn.λ${ident HPn}:$Pn.$Pc) $c }.
-interpretation "Exists_elim" 'Exists_elim ExPx Pc c = (cast _ c (Exists_elim _ _ _ ExPx Pc)).
+notation > "∨_'i_l' term 90 a" with precedence 19
+for @{ 'Or_intro_l (show $a ?) }.
+interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)).
+interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a). 
+  
+notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19 
+for @{ 'Or_intro_r_ok_1 $a $ab }.
+interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab = 
+  (show ab (Or_intro_r _ _ a)).
+
+notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 
+for @{ 'Or_intro_r_ok_1 $a $ab }.
+interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = 
+  (cast _ _ (show ab (Or_intro_r _ _ a))).
+
+notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 
+for @{ 'Or_intro_r_ko_1 $a $ab }.
+interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab = 
+  (show ab (cast _ _ (Or_intro_r _ _ a))).
+
+notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 
+for @{ 'Or_intro_r_ko_2 $a $ab }.
+interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab = 
+  (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
 
-inductive Forall (A:Type) (P:A→CProp) : CProp ≝
- Forall_intro: (∀n:A. P n) → Forall A P.
+notation > "∨_'i_r' term 90 a" with precedence 19
+for @{ 'Or_intro_r (show $a ?) }.
+interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)).
+interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a). 
 
-notation "\forall ident x:A.break term 19 Px" with precedence 20
-for @{ 'Forall (λ${ident x}:$A.$Px) }.
-interpretation "Forall" 'Forall \eta.Px = (Forall _ Px).
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
+for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
+interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c = 
+  (show c (Or_elim _ _ _ ab ac bc)).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
+for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
+interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c = 
+  (cast _ _ (show c (Or_elim _ _ _ ab ac bc))).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19
+for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
+interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = 
+  (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc)))).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19
+for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
+interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = 
+  (cast _ _ (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc))))).
+
+definition unit_to ≝ λx:CProp.unit → x.
+
+notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
+for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) $cl $cr }.
+interpretation "Or_elim KO" 'Or_elim ab ac bc c1 c2 = 
+  (cast _ _ (Or_elim _ _ _ (cast (Or unit unit) _ ab) (cast (unit_to unit) (unit_to _) ac) (cast (unit_to unit) (unit_to _) bc))).
+interpretation "Or_elim OK" 'Or_elim ab ac bc c1 c2 = (Or_elim _ _ _ ab ac bc).
+
+notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19 
+for @{'Top_intro_ko_1}.
+interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = (show _ (cast _ _ Top_intro)).
+
+notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 
+for @{'Top_intro_ok_1}.
+interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
+
+notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }.
+interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro).
+interpretation "Top_intro OK" 'Top_intro = Top_intro.
+
+notation < "\infrule b a (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ok_1 $a $b}.
+interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = 
+  (show a (Bot_elim a b)).
+
+notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ko_1 $a $b}.
+interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = 
+  (show a (Bot_elim a (cast _ _ b))).
+
+notation > "⊥_'e' term 90 b" with precedence 19 
+for @{ 'Bot_elim (show $b ?) }.
+interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).  
+interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
+
+notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
+for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
+interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = 
+  (show ab (cast _ _ (Not_intro _ (cast _ _ b)))).
+
+notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
+for @{ 'Not_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
+interpretation "Not_intro_ko_2" 'Not_intro_ko_2 ab \eta.b = 
+  (cast _ _ (show ab (cast _ _ (Not_intro _ (cast _ _ b))))).
+
+notation < "\infrule hbox(\emsp b \emsp) ab (\lnot\sub\i \emsp ident H) " with precedence 19
+for @{ 'Not_intro_ok_1 $ab (λ${ident H}:$p.$b) }.
+interpretation "Not_intro_ok_1" 'Not_intro_ok_1 ab \eta.b = 
+  (show ab (Not_intro _ b)).
+
+notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (\lnot\sub\i \emsp ident H) " with precedence 19
+for @{ 'Not_intro_ok_2 $ab (λ${ident H}:$p.$b) }.
+interpretation "Not_intro_ok_2" 'Not_intro_ok_2 ab \eta.b = 
+  (cast _ _ (show ab (Not_intro _ b))).
+
+notation > "¬_'i' [ident H] term 90 b" with precedence 19
+for @{ 'Not_intro (λ${ident H}.show $b ?) }.
+interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))).
+interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\e) " with precedence 19 
+for @{ 'Not_elim_ok_1 $ab $a $b }.
+interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b = 
+  (show b (Not_elim _ ab a)).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) (\lnot\sub\e) " with precedence 19 
+for @{ 'Not_elim_ok_2 $ab $a $b }.
+interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b = 
+  (cast _ _ (show b (Not_elim _ ab a))).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
+for @{ 'Not_elim_ko_1 $ab $a $b }.
+interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = 
+  (show b (Not_elim _ (cast _ _ ab) a)).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
+for @{ 'Not_elim_ko_2 $ab $a $b }.
+interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = 
+  (cast _ _ (show b (Not_elim _ (cast _ _ ab) a))).
+
+notation > "¬_'e' term 90 ab term 90 a" with precedence 19
+for @{ 'Not_elim (show $ab ?) (show $a ?) }.
+interpretation "Not_elim KO" 'Not_elim ab a = (Not_elim _ (cast _ _ ab) a).
+interpretation "Not_elim OK" 'Not_elim ab a = (Not_elim _ ab a).
+
+notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19
+for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
+interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = 
+  (show Pn (Raa _ Px)).
+
+notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (\RAA \emsp ident x)" with precedence 19
+for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
+interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn = 
+  (cast _ _ (show Pn (Raa _ Px))).
+
+notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
+for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
+interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = 
+  (show Pn (Raa _ (cast _ _ Px))).
+
+notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
+for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
+interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = 
+  (cast _ _ (show Pn (Raa _ (cast _ _ Px)))).
+
+notation > "'RAA' [ident H] term 90 b" with precedence 19 
+for @{ 'Raa (λ${ident H}.show $b ?) }. 
+interpretation "RAA KO" 'Raa p = (Raa _ (cast _ (unit_to _) p)).
+interpretation "RAA OK" 'Raa p = (Raa _ p).
+
+(*DOCBEGIN
+Templates for rules
+⇒_i […] (…)
+∧_i (…) (…)
+∨_i_l (…)
+∨_i_r (…)
+¬_i […] (…)
+⊤_i
+⇒_e (…) (…)
+∧_e_l (…)
+∧_e_r (…)
+∨_e (…) […] (…) […] (…)
+¬_e (…) (…)
+⊥_e (…)
+prove (…)
+RAA […] (…)
+DOCEND*)
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i \emsp ident x)" with precedence 19
-for @{ 'Forall_intro (λ${ident x}:$tx.$Px) $Pn }.
-interpretation "Forall_intro" 'Forall_intro Px Pn = (cast _ Pn (Forall_intro _ _ Px)).
 
-definition Forall_elim ≝
- λA:Type.λP:A→CProp.λn:A.λf:∀x:A.P x.match f with [ Forall_intro g ⇒ g n ].
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (∀\sub\i)" with precedence 19 for @{ 'Forall_elim $Px $Pn }.
-interpretation "Forall_elim" 'Forall_elim Px Pn = (cast _ Pn (Forall_elim _ _ _ Px)).
 
-notation > "[H]" with precedence 90
-for @{ assumpt ? (cast ? ? $H)}.
-notation > "⇒_'i' [ident H] term 90 b" with precedence 19
-for @{ Imply_intro ?? (λ${ident H}.cast ? $b ?) }.
-notation > "⇒_'e' term 90 ab term 90 a" with precedence 19
-for @{ Imply_elim ?? (cast ? $ab ?) (cast $a $a ?) }.
-notation > "∧_'i' term 90 a term 90 b" with precedence 19
-for @{ And_intro ?? (cast ? $a ?) (cast ? $b ?) }.
-(*notation > "∧_'e_l' term 90 ab" with precedence 19
-for @{ And_elim_l ?? (cast (? ∧ False) $ab ?) }.
-notation > "∧_'e_l' term 90 a ∧ term 90 b" with precedence 19
-for @{ And_elim_l ?? (cast (? ∧ $b) ($a ∧ $b) ?) }. *)
-notation > "∧_'e_l' term 90 ab" with precedence 19
-for @{ And_elim_l ?? (cast $ab $ab ?) }. (* CSC: WRONG *)
-notation > "∧_'e_r' term 90 ab" with precedence 19
-for @{ And_elim_r ?? (cast $ab $ab ?) }. (* CSC: WRONG *)
-notation > "∨_'i_l' term 90 a" with precedence 19
-for @{ Or_intro_l ?? (cast ? $a ?) }.
-notation > "∨_'i_r' term 90 a" with precedence 19
-for @{ Or_intro_r ?? (cast ? $a ?) }.
-notation > "∨_'e' term 90 ab [ident Ha] term 90 c1 [ident Hb] term 90 c2" with precedence 19
-for @{ Or_elim ??? (cast $ab $ab ?) (λ${ident Ha}.cast ? $c1 ?) (λ${ident Hb}.cast ? $c2 ?) }.
-notation > "∀_'i' [ident z] term 90 a" with precedence 19
-for @{ Forall_intro ?? (λ${ident z}.cast ? $a ?) }.
-notation > "∀_'e' term 90 ab term 90 a" with precedence 19
-for @{ Forall_elim ?? $a (cast $ab $ab ?) }. 
-notation > "∃_'e' term 90 enpn [ident z] [ident pz] term 90 c" with precedence 19
-for @{ Exists_elim ??? (cast $enpn $enpn ?) (λ${ident z}.λ${ident pz}.cast ? $c ?) }.
-notation > "∃_'i' term 90 n term 90 pn" with precedence 19
-for @{ Exists_intro ? (λ_.?) $n (cast ? $pn ?) }.
diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 5e39120a9..2b239b4e5 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1160,15 +1160,6 @@
                         <property name="use_underline">True</property>
                         <child>
                           <widget class="GtkMenu" id="viewMenu_menu">
-                            <child>
-                              <widget class="GtkCheckMenuItem" id="tacticsBarMenuItem">
-                                <property name="visible">True</property>
-                                <property name="label" translatable="yes">Show _tactics bar</property>
-                                <property name="use_underline">True</property>
-                                <property name="active">True</property>
-                                <accelerator key="F2" modifiers="" signal="activate"/>
-                              </widget>
-                            </child>
                             <child>
                               <widget class="GtkMenuItem" id="newCicBrowserMenuItem">
                                 <property name="visible">True</property>
@@ -1190,6 +1181,15 @@
                                 <accelerator key="F11" modifiers="" signal="activate"/>
                               </widget>
                             </child>
+                            <child>
+                              <widget class="GtkCheckMenuItem" id="menuitemPalette">
+                                <property name="visible">True</property>
+                                <property name="tooltip" translatable="yes">Shows a palette with natural deduction rules</property>
+                                <property name="label" translatable="yes">Natural deduction palette</property>
+                                <property name="use_underline">True</property>
+                                <accelerator key="F2" modifiers="" signal="activate"/>
+                              </widget>
+                            </child>
                             <child>
                               <widget class="GtkSeparatorMenuItem" id="separator1">
                                 <property name="visible">True</property>
@@ -1396,13 +1396,234 @@
                               <widget class="GtkVBox" id="vboxTacticsPalette">
                                 <property name="visible">True</property>
                                 <child>
-                                  <placeholder/>
+                                  <widget class="GtkExpander" id="expander1">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <widget class="GtkVBox" id="vbox1">
+                                        <property name="visible">True</property>
+                                        <child>
+                                          <widget class="GtkButton" id="butImpl_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Implication (⇒_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butAnd_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Conjunction (∧_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butOr_intro_left">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Disjunction left (∨_i_l)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butOr_intro_right">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Disjunction right (∨_i_r)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">3</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butNot_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Negaton (¬_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">4</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butTop_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Top (⊤_i)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">5</property>
+                                          </packing>
+                                        </child>
+                                      </widget>
+                                    </child>
+                                    <child>
+                                      <widget class="GtkLabel" id="label4">
+                                        <property name="visible">True</property>
+                                        <property name="label" translatable="yes">Introduction rules</property>
+                                      </widget>
+                                      <packing>
+                                        <property name="type">label_item</property>
+                                      </packing>
+                                    </child>
+                                  </widget>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                  </packing>
                                 </child>
                                 <child>
-                                  <placeholder/>
+                                  <widget class="GtkExpander" id="expander2">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <widget class="GtkVBox" id="vbox3">
+                                        <property name="visible">True</property>
+                                        <child>
+                                          <widget class="GtkButton" id="butImpl_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Implication (⇒_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butAnd_elim_left">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Conjunction left (∧_e_l)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butAnd_elim_right">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Conjunction right (∧_e_r)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butOr_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Disjunction (∨_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">3</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butNot_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Negaton (¬_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">4</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butBot_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Bottom (⊥_e)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">5</property>
+                                          </packing>
+                                        </child>
+                                      </widget>
+                                    </child>
+                                    <child>
+                                      <widget class="GtkLabel" id="label5">
+                                        <property name="visible">True</property>
+                                        <property name="label" translatable="yes">Elimination rules</property>
+                                      </widget>
+                                      <packing>
+                                        <property name="type">label_item</property>
+                                      </packing>
+                                    </child>
+                                  </widget>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                    <property name="position">1</property>
+                                  </packing>
                                 </child>
                                 <child>
-                                  <placeholder/>
+                                  <widget class="GtkExpander" id="expander3">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <widget class="GtkVBox" id="vbox4">
+                                        <property name="visible">True</property>
+                                        <child>
+                                          <widget class="GtkButton" id="butRAA">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Reduction to Absurdity (RAA)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                        </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butStart">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Prove (to start)</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
+                                      </widget>
+                                    </child>
+                                    <child>
+                                      <widget class="GtkLabel" id="label6">
+                                        <property name="visible">True</property>
+                                        <property name="label" translatable="yes">Misc rules</property>
+                                      </widget>
+                                      <packing>
+                                        <property name="type">label_item</property>
+                                      </packing>
+                                    </child>
+                                  </widget>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                    <property name="position">2</property>
+                                  </packing>
                                 </child>
                               </widget>
                             </child>
@@ -2116,59 +2337,6 @@
         <property name="n_rows">3</property>
         <property name="n_columns">2</property>
         <property name="row_spacing">5</property>
-        <child>
-          <widget class="GtkLabel" id="label17">
-            <property name="visible">True</property>
-            <property name="xalign">0</property>
-            <property name="label" translatable="yes">Find:</property>
-          </widget>
-          <packing>
-            <property name="x_options"></property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkLabel" id="label18">
-            <property name="visible">True</property>
-            <property name="xalign">0</property>
-            <property name="label" translatable="yes">Replace with: </property>
-          </widget>
-          <packing>
-            <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="x_options"></property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkEntry" id="findEntry">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="has_focus">True</property>
-            <property name="can_default">True</property>
-            <property name="has_default">True</property>
-            <property name="invisible_char">*</property>
-          </widget>
-          <packing>
-            <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkEntry" id="replaceEntry">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="invisible_char">*</property>
-          </widget>
-          <packing>
-            <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
         <child>
           <widget class="GtkHBox" id="hbox19">
             <property name="visible">True</property>
@@ -2267,6 +2435,59 @@
             <property name="y_padding">5</property>
           </packing>
         </child>
+        <child>
+          <widget class="GtkEntry" id="replaceEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="invisible_char">*</property>
+          </widget>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkEntry" id="findEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="has_focus">True</property>
+            <property name="can_default">True</property>
+            <property name="has_default">True</property>
+            <property name="invisible_char">*</property>
+          </widget>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkLabel" id="label18">
+            <property name="visible">True</property>
+            <property name="xalign">0</property>
+            <property name="label" translatable="yes">Replace with: </property>
+          </widget>
+          <packing>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="x_options"></property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkLabel" id="label17">
+            <property name="visible">True</property>
+            <property name="xalign">0</property>
+            <property name="label" translatable="yes">Find:</property>
+          </widget>
+          <packing>
+            <property name="x_options"></property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
       </widget>
     </child>
   </widget>
diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index 6c0f4c8dc..c76046c75 100644
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -158,6 +158,7 @@
     <keyword>obtain</keyword>	    	 
     <keyword>conclude</keyword>	    	 
     <keyword>done</keyword>	    	 
+    <keyword>rule</keyword>	    	 
 </keyword-list>
 
   <keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index fa9a0d393..d0e1c1acb 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -35,7 +35,7 @@ let disambiguate_tactic text prefix_len lexicon_status_ref grafite_status goal t
   GrafiteDisambiguate.disambiguate_tactic
    lexicon_status_ref
    (GrafiteTypes.get_proof_context grafite_status goal)
-   (GrafiteTypes.get_proof_metasenv grafite_status)
+   (GrafiteTypes.get_proof_metasenv grafite_status) (Some goal)
    tac
  in
   GrafiteTypes.set_metasenv metasenv grafite_status,tac
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 1fe78046e..393da7cef 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -754,9 +754,47 @@ class gui () =
         ignore (adj#connect#changed
                 (fun _ -> adj#set_value (adj#upper -. adj#page_size)));
       console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version);
-      (* TO BE REMOVED *)
+        (* natural deduction palette *)
       main#tacticsButtonsHandlebox#misc#hide ();
-      main#tacticsBarMenuItem#misc#hide ();
+      MatitaGtkMisc.toggle_callback
+        ~callback:(fun b -> 
+          if b then main#tacticsButtonsHandlebox#misc#show ()
+          else main#tacticsButtonsHandlebox#misc#hide ())
+        ~check:main#menuitemPalette;
+      connect_button main#butImpl_intro
+        (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
+      connect_button main#butAnd_intro
+        (fun () -> source_buffer#insert 
+          "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n");
+      connect_button main#butOr_intro_left
+        (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n");
+      connect_button main#butOr_intro_right
+        (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
+      connect_button main#butNot_intro
+        (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
+      connect_button main#butTop_intro
+        (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
+      connect_button main#butImpl_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n");
+      connect_button main#butAnd_elim_left
+        (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n");
+      connect_button main#butAnd_elim_right
+        (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
+      connect_button main#butOr_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
+      connect_button main#butNot_elim
+        (fun () -> source_buffer#insert 
+          "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n");
+      connect_button main#butBot_elim
+        (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
+      connect_button main#butRAA
+        (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
+      connect_button main#butStart
+        (fun () -> source_buffer#insert "apply rule (prove (…));\n");
+    
+      (* TO BE REMOVED *)
       main#scriptNotebook#remove_page 1;
       main#scriptNotebook#set_show_tabs false;
       (* / TO BE REMOVED *)