using the new by foo we proved semantics

diff --git a/helm/software/matita/contribs/didactic/depends b/helm/software/matita/contribs/didactic/depends
index a9d0243fb40c01cef5b14000bea366dbb58819f5..ae4b2462ac023521f38cd0816671aede59f7a1a5 100644 (file)
--- a/helm/software/matita/contribs/didactic/depends
+++ b/helm/software/matita/contribs/didactic/depends
@@ -1,2 +1,9 @@
+duality.ma nat/minus.ma
+exercise-induction.ma nat/minus.ma
+shannon.ma nat/minus.ma
+algebra.ma nat/compare.ma nat/times.ma
+exercise-duality.ma nat/minus.ma
 induction.ma nat/minus.ma
+nat/compare.ma 
 nat/minus.ma 
+nat/times.ma 

diff --git a/helm/software/matita/contribs/didactic/depends.png b/helm/software/matita/contribs/didactic/depends.png
index 0a48f0e8b07cb8717e7632ed2cac93bc2b224230..ed54ff73b2fc1a8cf2c3823aef3caeb82224659f 100644 (file)
Binary files a/helm/software/matita/contribs/didactic/depends.png and b/helm/software/matita/contribs/didactic/depends.png differ

diff --git a/helm/software/matita/contribs/didactic/duality.ma b/helm/software/matita/contribs/didactic/duality.ma
index 0138975b2fdd2fbebc3ffb1ce1b774912ff5a362..c04859bd142ea693521ba637ba6c017e979c5516 100644 (file)
--- a/helm/software/matita/contribs/didactic/duality.ma
+++ b/helm/software/matita/contribs/didactic/duality.ma
@@ -611,9 +611,9 @@ theorem duality: ∀F1,F2:Formula.F1 ≡ F2 → dualize F1 ≡ dualize F2.
  assume F2:Formula.
  suppose (F1 ≡ F2) (H).
  the thesis becomes (dualize F1 ≡ dualize F2).
- by (*BEGIN*)negate_fun(*END*) we proved (negate F1 ≡ negate F2) (H1).
+ by (*BEGIN*)negate_fun(*END*), H we proved (negate F1 ≡ negate F2) (H1).
  by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H1 we proved (FNot (dualize F1) ≡ negate F2) (H2).
  by (*BEGIN*)not_dualize_eq_negate(*END*), (*BEGIN*)equiv_rewrite(*END*), H2 we proved (FNot (dualize F1) ≡ FNot (dualize F2)) (H3).
  by (*BEGIN*)not_inj(*END*), H3 we proved (dualize F1 ≡ dualize F2) (H4).
- done.
+ by H4 done.
 qed.

diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma
index e2da2243ac90ede12b9d3be50969659b8fd71481..c4335ca3e313a15b55615084f12daa3f54a6a20c 100644 (file)
--- a/helm/software/matita/contribs/didactic/induction.ma
+++ b/helm/software/matita/contribs/didactic/induction.ma
@@ -440,7 +440,7 @@ case FAtom.
      if eqb n x then G2 else (FAtom n)).
   case true.
     the thesis becomes (G1 ≡ G2).
-    done.
+    by H done.
   case false.
     (*BEGIN*)
     the thesis becomes (FAtom n ≡ FAtom n).

diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma
index be31459eba4f78964e5672ff092dd13e93d322f2..d88f46ad76f45f2bdaa3f47a080901f05b6c0dd2 100644 (file)
--- a/helm/software/matita/contribs/didactic/shannon.ma
+++ b/helm/software/matita/contribs/didactic/shannon.ma
@@ -212,10 +212,10 @@ case FAnd.
   case Left.
     by H3, H we proved 
       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 0 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
@@ -230,10 +230,10 @@ case FAnd.
   case Right.
     by H3, H we proved 
       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 1 O then ((FAnd f f1)[ FBot/x ]) else ((FAnd f f1)[ FTop/x ]) ]]_v) by H3.
@@ -258,10 +258,10 @@ case FOr.
   case Left.
     by H3, H we proved 
       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 0 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
@@ -276,10 +276,10 @@ case FOr.
   case Right.
     by H3, H we proved 
       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 1 O then ((FOr f f1)[ FBot/x ]) else ((FOr f f1)[ FTop/x ]) ]]_v) by H3.
@@ -304,10 +304,10 @@ case FImpl.
   case Left.
     by H3, H we proved 
       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 0 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 0 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
@@ -322,10 +322,10 @@ case FImpl.
   case Right.
     by H3, H we proved 
       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
-    by H3, 1 we proved 
+    by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
+    by H3, H1 we proved 
       ([[ if eqb 1 O then f1[ FBot/x ] else (f1[ FTop/x ])  ]]_v = [[ f1 ]]_v) (H6).
-    using H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
+    by H6 we proved ([[ f1[FTop/x ] ]]_v = [[ f1 ]]_v) (H7).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v)
       = ([[ if eqb 1 O then ((FImpl f f1)[ FBot/x ]) else ((FImpl f f1)[ FTop/x ]) ]]_v) by H3.
@@ -348,7 +348,7 @@ case FNot.
   case Left.
     by H1, H we proved 
       ([[ if eqb 0 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
+    by H4 we proved ([[ f[FBot/x ] ]]_v = [[ f ]]_v) (H5).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
       = ([[ if eqb 0 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.
@@ -362,7 +362,7 @@ case FNot.
   case Right.
     by H1, H we proved 
       ([[ if eqb 1 O then f[ FBot/x ] else (f[ FTop/x ])  ]]_v = [[ f ]]_v) (H4).
-    using H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
+    by H4 we proved ([[ f[FTop/x ] ]]_v = [[ f ]]_v) (H5).
     conclude
         ([[ if eqb [[ FAtom x ]]_v O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v)
       = ([[ if eqb 1 O then ((FNot f)[ FBot/x ]) else ((FNot f)[ FTop/x ]) ]]_v) by H1.