A very nice experiment using notation: we define the notation for natural

language derivations so that, when looking at the proof, we see it as a
natural deduction tree! Useful to teach logic to first year students, but
much work still need to be done (expecially to give derivation trees to
the system in some way).

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
new file mode 100644 (file)
index 0000000..a75d0cb
--- /dev/null
+++ b/helm/software/matita/library/demo/natural_deduction.ma
@@ -0,0 +1,145 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+definition cast ≝ λA:CProp.λa:A.a.
+
+notation < "[ a ] \sup H" with precedence 19 for @{ 'ass $a $H }.
+interpretation "assumption" 'ass a H = (cast a H).
+
+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).
+
+notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i) " with precedence 19 for @{ 'Imply_intro $ab (λ${ident H}:$p.$b) }.
+interpretation "Imply_intro" 'Imply_intro ab \eta.b = (cast ab (Imply_intro _ _ b)).
+
+definition Imply_elim ≝ λA,B.λf:Imply A B.λa:A.match f with [ Imply_intro g ⇒ g 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)).
+
+inductive And (A,B:CProp) : CProp ≝
+ And_intro: A → B → And A B.
+
+interpretation "constructive and" 'and x y = (And x y).
+
+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\sup\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)).
+
+definition And_elim_r ≝
+ λA,B.λc:A∧B.match c with [ And_intro a b ⇒ b ].
+
+notation < "\infrule hbox(\emsp ab \emsp) b (∧\sub\e\sup\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)).
+
+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 < "\infrule hbox(\emsp a \emsp) ab (∨\sub\i\sup\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 < "\infrule hbox(\emsp b \emsp) ab (∨\sub\i\sup\l)" with precedence 19 for @{ 'Or_intro_r $b $ab }.
+interpretation "Or_intro_l" 'Or_intro_r b ab = (cast ab (Or_intro_r _ _ 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 ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e)" with precedence 19 for @{ 'Or_elim $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
+interpretation "Or_elim" 'Or_elim ab ac bc c = (cast c (Or_elim _ _ _ ab ac bc)).
+
+inductive Exists (A:Type) (P:A→CProp) : CProp ≝
+  Exists_intro: ∀w:A. P w → Exists A P.
+
+interpretation "constructive ex" 'exists \eta.x = (Exists _ x).
+
+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)).
+
+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 < "\infrule hbox(\emsp ExPx \emsp\emsp\emsp Pc \emsp) c (∃\sub\e)" 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)).
+
+inductive Forall (A:Type) (P:A→CProp) : CProp ≝
+ Forall_intro: (∀n:A. P n) → Forall A P.
+
+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 Px \emsp) Pn (∀\sub\i)" 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)).
+
+axiom A: CProp.
+axiom B: CProp.
+axiom C: CProp.
+axiom D: CProp.
+axiom E: CProp.
+
+lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
+repeat (apply cast; constructor 1; intro);
+apply cast; apply (Or_elim (A ⇒ E) B (E∧C∨B)); try intro;
+[ apply cast; assumption
+| apply cast; apply Or_intro_l;
+  apply cast; constructor 1;
+  [ apply cast; apply (Imply_elim A E);
+    [ apply cast; assumption
+    | apply cast; apply (And_elim_l A C);
+      apply cast; assumption
+    ]
+  | apply cast; apply (And_elim_r A C);
+    apply cast; assumption
+  ]
+| apply cast; apply Or_intro_r;
+  apply cast; assumption
+]
+qed.
+
+axiom N: Type.
+axiom R: N → N → CProp.
+
+lemma ex2: (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
+ apply cast; apply Imply_intro; intro;
+ apply cast; apply Forall_intro; intro z;
+ apply cast; apply Imply_intro; intro;
+ apply cast; apply (Exists_elim N (λy.R y z)); try intros (n);
+  [ apply cast; assumption
+  | apply cast; apply (Exists_intro ? ? n);
+    apply cast; apply (Imply_elim (R n z) (R z n));
+     [ apply cast; apply (Forall_elim N (λb:N.R n b ⇒ R b n) z);
+       apply cast; apply (Forall_elim N (λa:N.∀b:N.R a b ⇒ R b a) n);
+       apply cast; assumption
+     | apply cast; assumption
+     ]
+  ]
+qed.
\ No newline at end of file