From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 30 Nov 2008 21:00:04 +0000 (+0000)
Subject: natural deduction support for lemmas with premises
X-Git-Tag: make_still_working~4474
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2030cae5f1a588fa6bbea50927030f83a2156d67;p=helm.git

natural deduction support for lemmas with premises
---

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction.ma b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
index 7f941c118..1bc9717fd 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction.ma
@@ -173,7 +173,7 @@ apply rule (⇒_i [h2] ((D ⇒ A) ⇒ D ⇒ C));
 apply rule (⇒_i [h3] (D ⇒ C));
 apply rule (⇒_i [h4] (C));
 apply rule (∨_e (B∨¬B) [h5] (C) [h6] (C));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (⇒_e (B∧D⇒C) (B∧D));
 	    [ apply rule (discharge [h2]);
     	| apply rule (∧_i (B) (D));
@@ -234,9 +234,9 @@ apply rule (prove (¬(A∧B) ⇒ ¬A∨¬B));
 (*BEGIN*)
 apply rule (⇒_i [h1] (¬A∨¬B));
 apply rule (∨_e (A ∨ ¬A) [h2] ((¬A∨¬B)) [h3] ((¬A∨¬B)));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (∨_e (B ∨ ¬B) [h4] ((¬A∨¬B)) [h5] ((¬A∨¬B)));
-	    [ apply rule (lem EM);
+	    [ apply rule (lem 0 EM);
 	    | apply rule (⊥_e (⊥));
 	      apply rule (¬_e (¬(A∧B)) (A∧B));
 	        [ apply rule (discharge [h1]);
@@ -259,7 +259,7 @@ apply rule (prove (¬(A∨B) ⇒ (¬A ∧ ¬B)));
 (*BEGIN*)
 apply rule (⇒_i [h1] (¬A ∧ ¬B));
 apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (⊥_e (⊥));
     apply rule (¬_e (¬(A∨B)) (A∨B));
 	    [ apply rule (discharge [h1]);
@@ -267,7 +267,7 @@ apply rule (∨_e (A∨¬A) [h2] (¬A ∧ ¬B) [h3] (¬A ∧ ¬B));
         apply rule (discharge [h2]);
 	    ]
 	| apply rule (∨_e (B∨¬B) [h10] (¬A ∧ ¬B) [h11] (¬A ∧ ¬B));
-	    [ apply rule (lem EM);
+	    [ apply rule (lem 0 EM);
 	    | apply rule (⊥_e (⊥));
         apply rule (¬_e (¬(A∨B)) (A∨B));
 	        [ apply rule (discharge [h1]);
@@ -318,5 +318,5 @@ apply rule (⇒_e ((A⇒⊥)⇒⊥) (A⇒⊥));
 	    ]
 	]
 (*END*)
-qed. 
+qed.
 
diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
index 8f90dd67c..c2778fbc5 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction1.ma
@@ -54,7 +54,7 @@ apply rule (⇒_i [h1] ((G ∧ L ⇒ E) ⇒ F ∧ L ⇒ E));
 apply rule (⇒_i [h2] (F ∧ L ⇒ E));
 apply rule (⇒_i [h3] (E));
 apply rule (∨_e (G∨¬G) [h4] (E) [h4] (E));
-	[ apply rule (lem EM);
+	[ apply rule (lem 0 EM);
 	| apply rule (⇒_e (G∧L⇒E) (G∧L));
 	    [ apply rule (discharge [h2]);
 	    | apply rule (∧_i (G) (L));
@@ -123,7 +123,7 @@ apply rule (⇒_i [h2] ((¬G ⇒ ¬H) ⇒ H ⇒ E));
 apply rule (⇒_i [h3] (H ⇒ E));
 apply rule (⇒_i [h4] (E));
 apply rule (∨_e (G∨¬G) [h5] (E) [h5] (E));
-	[apply rule (lem EM);
+	[apply rule (lem 0 EM);
 	| apply rule (∨_e (E∨F) [h6] (E) [h6] (E));
 	   [ apply rule (⇒_e (H ⇒ E∨F) (H));
 	       [ apply rule (discharge [h2]);
diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index 84fbeee78..f5799b90e 100644
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -132,43 +132,6 @@ notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19
 for @{ 'leaf_ko $a $t }.
 interpretation "leaf KO" 'leaf_ko a t = (cast _ _ (show a t)).
 
-(* already proved lemma *)
-definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
-
-notation < "\infrule \nbsp p mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ko_1 $p $H }.
-interpretation "lemma_ko_1" 'lemma_ko_1 p H = 
-  (show p (cast _ _ (Lemma _ H))). 
-
-notation < "\infrule \nbsp mstyle color #ff0000 (p) mstyle color #ff0000 (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ko_2 $p $H }.
-interpretation "lemma_ko_2" 'lemma_ko_2 p H = 
-  (cast _ _ (show p (cast _ _ (Lemma _ H)))). 
-
-notation < "\infrule \nbsp p (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ok_1 $p $H }.
-interpretation "lemma_ok_1" 'lemma_ok_1 p H = 
-  (show p (Lemma _ H)). 
-interpretation "lemma_ok_11" 'lemma_ok_1 p H = 
-  (show p (Lemma _ H _)). 
-interpretation "lemma_ok_111" 'lemma_ok_1 p H = 
-  (show p (Lemma _ H _ _)). 
-
-notation < "\infrule \nbsp mstyle color #ff0000 (p) (\lem\emsp H)" non associative with precedence 19
-for @{ 'lemma_ok_2 $p $H }.
-interpretation "lemma_ok_2" 'lemma_ok_2 p H = 
-  (cast _ _ (show p (Lemma _ H))). 
-interpretation "lemma_ok_22" 'lemma_ok_2 p H = 
-  (cast _ _ (show p (Lemma _ H _))). 
-interpretation "lemma_ok_22" 'lemma_ok_2 p H = 
-  (cast _ _ (show p (Lemma _ H _ _))). 
-
-notation > "'lem' term 90 p" non associative with precedence 19
-for @{ 'Lemma $p  }.
-interpretation "lemma KO" 'Lemma p = (cast _ _ (Lemma _ p)).
-interpretation "lemma OK" 'Lemma p = (Lemma _ p).
-
-
 (* discharging *)
 notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 
 for @{ 'discharge_ko_1 $a $H }.
@@ -654,3 +617,230 @@ interpretation "Forall_elim KO" 'Forall_elim P t Px =
   (cast _ unit (Forall_elim sort P t (cast _ _ Px))). 
 interpretation "Forall_elim OK" 'Forall_elim P t Px =
   (Forall_elim sort P t Px). 
+
+(* already proved lemma *)
+definition hide_args : ∀A:Type.∀a:A.A := λA:Type.λa:A.a.
+notation < "t" non associative with precedence 90 for @{'hide_args $t}.
+interpretation "hide 0 args"  'hide_args t = (hide_args _ t).
+interpretation "hide 1 args"  'hide_args t = (hide_args _ t _).
+interpretation "hide 2 args"  'hide_args t = (hide_args _ t _ _).
+interpretation "hide 3 args"  'hide_args t = (hide_args _ t _ _ _).
+interpretation "hide 4 args"  'hide_args t = (hide_args _ t _ _ _ _). 
+interpretation "hide 5 args"  'hide_args t = (hide_args _ t _ _ _ _ _).
+interpretation "hide 6 args"  'hide_args t = (hide_args _ t _ _ _ _ _ _).
+interpretation "hide 7 args"  'hide_args t = (hide_args _ t _ _ _ _ _ _ _).
+
+(* more args crashes the pattern matcher *)
+
+(* already proved lemma, 0 assumptions *)
+definition Lemma : ΠA.A→A ≝ λA:CProp.λa:A.a.
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma_ko_1 $p ($H : $_) }.
+interpretation "lemma_ko_1" 'lemma_ko_1 p H = 
+  (show p (cast _ _ (Lemma _ (cast _ _ H)))). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+non associative with precedence 19
+for @{ 'lemma_ko_2 $p ($H : $_) }.
+interpretation "lemma_ko_2" 'lemma_ko_2 p H = 
+  (cast _ _ (show p (cast _ _ 
+    (Lemma _ (cast _ _ H))))). 
+
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma_ok_1 $p ($H : $_) }.
+interpretation "lemma_ok_1" 'lemma_ok_1 p H = 
+  (show p (Lemma _ H)). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+non associative with precedence 19
+for @{ 'lemma_ok_2 $p ($H : $_) }.
+interpretation "lemma_ok_2" 'lemma_ok_2 p H = 
+  (cast _ _ (show p (Lemma _ H))). 
+
+notation > "'lem' 0 term 90 l" non associative with precedence 19
+for @{ 'Lemma (hide_args ? $l : ?) }.
+interpretation "lemma KO" 'Lemma l = 
+  (cast _ _ (Lemma unit (cast unit _ l))). 
+interpretation "lemma OK" 'Lemma l = (Lemma _ l).
+
+
+(* already proved lemma, 1 assumption *)
+definition Lemma1 : ΠA,B. (A ⇒ B) → A → B ≝ 
+ λA,B:CProp.λf:A⇒B.λa:A.
+  Imply_elim A B f a.
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma1_ko_1 $a $p ($H : $_) }.
+interpretation "lemma1_ko_1" 'lemma1_ko_1 a p H = 
+  (show p (cast _ _ (Lemma1 _ _ (cast _ _ H) (cast _ _ a)))). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+non associative with precedence 19
+for @{ 'lemma1_ko_2 $a $p ($H : $_) }.
+interpretation "lemma1_ko_2" 'lemma1_ko_2 a p H = 
+  (cast _ _ (show p (cast _ _ 
+    (Lemma1 _ _ (cast _ _ H) (cast _ _ a))))). 
+
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma1_ok_1 $a $p ($H : $_) }.
+interpretation "lemma1_ok_1" 'lemma1_ok_1 a p H = 
+  (show p (Lemma1 _ _ H a)). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+non associative with precedence 19
+for @{ 'lemma1_ok_2 $a $p ($H : $_) }.
+interpretation "lemma1_ok_2" 'lemma1_ok_2 a p H = 
+  (cast _ _ (show p (Lemma1 _ _ H a))). 
+
+
+notation > "'lem' 1 term 90 l term 90 p" non associative with precedence 19
+for @{ 'Lemma1 (hide_args ? $l : ?) (show $p ?) }.
+interpretation "lemma 1 KO" 'Lemma1 l p = 
+  (cast _ _ (Lemma1 unit unit (cast (Imply unit unit) _ l) (cast unit _ p))). 
+interpretation "lemma 1 OK" 'Lemma1 l p = (Lemma1 _ _ l p).
+
+(* already proved lemma, 2 assumptions *)
+definition Lemma2 : ΠA,B,C. (A ⇒ B ⇒ C) → A → B → C ≝ 
+ λA,B,C:CProp.λf:A⇒B⇒C.λa:A.λb:B.
+  Imply_elim B C (Imply_elim A (B⇒C) f a) b.
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma2_ko_1 $a $b $p ($H : $_) }.
+interpretation "lemma2_ko_1" 'lemma2_ko_1 a b p H = 
+  (show p (cast _ _ (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b)))). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+non associative with precedence 19
+for @{ 'lemma2_ko_2 $a $b $p ($H : $_) }.
+interpretation "lemma2_ko_2" 'lemma2_ko_2 a b p H = 
+  (cast _ _ (show p (cast _ _ 
+    (Lemma2 _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b))))). 
+
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma2_ok_1 $a $b $p ($H : $_) }.
+interpretation "lemma2_ok_1" 'lemma2_ok_1 a b p H = 
+  (show p (Lemma2 _ _ _ H a b)). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+non associative with precedence 19
+for @{ 'lemma2_ok_2 $a $b $p ($H : $_) }.
+interpretation "lemma2_ok_2" 'lemma2_ok_2 a b p H = 
+  (cast _ _ (show p (Lemma2 _ _ _ H a b))). 
+
+notation > "'lem' 2 term 90 l term 90 p term 90 q" non associative with precedence 19
+for @{ 'Lemma2 (hide_args ? $l : ?) (show $p ?) (show $q ?) }.
+interpretation "lemma 2 KO" 'Lemma2 l p q = 
+  (cast _ _ (Lemma2 unit unit unit (cast (Imply unit (Imply unit unit)) _ l) (cast unit _ p) (cast unit _ q))). 
+interpretation "lemma 2 OK" 'Lemma2 l p q = (Lemma2 _ _ _ l p q).
+
+(* already proved lemma, 3 assumptions *)
+definition Lemma3 : ΠA,B,C,D. (A ⇒ B ⇒ C ⇒ D) → A → B → C → D ≝ 
+ λA,B,C,D:CProp.λf:A⇒B⇒C⇒D.λa:A.λb:B.λc:C.
+  Imply_elim C D (Imply_elim B (C⇒D) (Imply_elim A (B⇒C⇒D) f a) b) c.
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma3_ko_1 $a $b $c $p ($H : $_) }.
+interpretation "lemma3_ko_1" 'lemma3_ko_1 a b c p H = 
+  (show p (cast _ _ 
+   (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c)))). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
+             (╲ mstyle mathsize normal (mstyle color #ff0000 (H)) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+non associative with precedence 19
+for @{ 'lemma3_ko_2 $a $b $c $p ($H : $_) }.
+interpretation "lemma3_ko_2" 'lemma3_ko_2 a b c p H = 
+  (cast _ _ (show p (cast _ _ 
+    (Lemma3 _ _ _ _ (cast _ _ H) (cast _ _ a) (cast _ _ b) (cast _ _ c))))). 
+
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         p \nbsp" 
+non associative with precedence 19
+for @{ 'lemma3_ok_1 $a $b $c $p ($H : $_) }.
+interpretation "lemma3_ok_1" 'lemma3_ok_1 a b c p H = 
+  (show p (Lemma3 _ _ _ _ H a b c)). 
+
+notation < "\infrule 
+         (\infrule 
+             (\emsp a \emsp\emsp\emsp b \emsp\emsp\emsp c \emsp) 
+             (╲ mstyle mathsize normal (H) ╱) \nbsp) 
+         mstyle color #ff0000 (p) \nbsp" 
+non associative with precedence 19
+for @{ 'lemma3_ok_2 $a $b $c $p ($H : $_) }.
+interpretation "lemma3_ok_2" 'lemma3_ok_2 a b c p H = 
+  (cast _ _ (show p (Lemma3 _ _ _ _ H a b c))). 
+
+notation > "'lem' 3 term 90 l term 90 p term 90 q term 90 r" non associative with precedence 19
+for @{ 'Lemma3 (hide_args ? $l : ?) (show $p ?) (show $q ?) (show $r ?) }.
+interpretation "lemma 3 KO" 'Lemma3 l p q r = 
+  (cast _ _ (Lemma3 unit unit unit unit (cast (Imply unit (Imply unit (Imply unit unit))) _ l) (cast unit _ p) (cast unit _ q) (cast unit _ r))). 
+interpretation "lemma 3 OK" 'Lemma3 l p q r = (Lemma3 _ _ _ _ l p q r).
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 429bb6b2c..7f4571c55 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -801,7 +801,7 @@ class gui () =
       connect_button main#butRAA
         (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
       connect_button main#butUseLemma
-        (fun () -> source_buffer#insert "apply rule (lem …);\n");
+        (fun () -> source_buffer#insert "apply rule (lem #premises name …);\n");
       connect_button main#butDischarge
         (fun () -> source_buffer#insert "apply rule (discharge […]);\n");