From: Enrico Tassi Date: Wed, 5 Nov 2008 21:31:01 +0000 (+0000) Subject: using the new by foo we proved semantics X-Git-Tag: make_still_working~4597 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4257ad7d31bc2db6c40ad55878f190963e51c1ec;p=helm.git 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 a9d0243fb..ae4b2462a 100644 --- 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 0a48f0e8b..ed54ff73b 100644 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 0138975b2..c04859bd1 100644 --- 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 e2da2243a..c4335ca3e 100644 --- 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 be31459eb..d88f46ad7 100644 --- 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.