From e74a2893a14da614919420a9661462b23dbfd9f6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 17 Oct 2008 10:56:02 +0000 Subject: [PATCH] ... --- .../matita/contribs/didactic/Makefile | 3 +- .../software/matita/contribs/didactic/depends | 4 +- .../matita/contribs/didactic/depends.png | Bin 10835 -> 7964 bytes .../matita/contribs/didactic/induction.ma | 379 +++++++++++++----- .../contribs/didactic/induction_support.ma | 25 -- 5 files changed, 278 insertions(+), 133 deletions(-) delete mode 100644 helm/software/matita/contribs/didactic/induction_support.ma diff --git a/helm/software/matita/contribs/didactic/Makefile b/helm/software/matita/contribs/didactic/Makefile index a904aaef4..bc35339e7 100644 --- a/helm/software/matita/contribs/didactic/Makefile +++ b/helm/software/matita/contribs/didactic/Makefile @@ -17,5 +17,6 @@ depend.opt: exercise: rm -rf ex/ mkdir ex/ - cp *.ma root depends ex/ + cp *.ma depends ex/ for X in ex/*.ma; do perl -ne 'undef $$/;s/\(\*BEGIN.*?END\*\)/.../msg;print' -i $$X; done + echo 'baseuri=cic:/matita/didactic/student' > ex/root diff --git a/helm/software/matita/contribs/didactic/depends b/helm/software/matita/contribs/didactic/depends index 6234ee807..a9d0243fb 100644 --- a/helm/software/matita/contribs/didactic/depends +++ b/helm/software/matita/contribs/didactic/depends @@ -1,2 +1,2 @@ -induction_support.ma -induction.ma induction_support.ma +induction.ma nat/minus.ma +nat/minus.ma diff --git a/helm/software/matita/contribs/didactic/depends.png b/helm/software/matita/contribs/didactic/depends.png index 3b6104659a0445c661f5a90af70ea60f5d1330aa..0a48f0e8b07cb8717e7632ed2cac93bc2b224230 100644 GIT binary patch literal 7964 zcmch61zS~7xAmc=6p&6y0TqyL5RsNp1Vkj1?(UTCl#~(yk(L&uQ(6S1IZ`4a-NK#c zeZS{>?k~8ofpggVtiASHbB;O2nBnTG@`QNQcnAc7P*Fkl3H+^qpNwnR@VkAMxETIm zzfzW$MO>l2bG{ZP!hdj_6(2vs`H4r2CnQu8@JXudem%&AJfw8eSI$zyqA;G=)_piqq4GnE}VPr%-C?uqP zZf=focaY6}^3@$#HMJW*ECt{g%9e_S5&4CL@@i_xN=r-4?d%v#r0nL!Rf)9iNWw8+ zRZ{M+4hAZ)ywSNE0)xvk5yNrfEx9_FA@nV~u~Dq4sYz~YY~zp;zG}+r>L@xoI(R4v zc+ymUudfHR8TyZ!%i7s-A9zX}cz*4oQO+C9sjG8KYRSpD6%-V7i=Uqqi9}u_Bz)xT z%ukAk1&6n{w{>cN6-El#&d3PSP?kjG^t3KNKmX$9RF$ybr8vx6R7?!*g6%_C*frD` z;^MSMMn>0gaRc2HRe?vz$d>e?d>g|q{Iq$pPik3=PfYS!HQWjZmIG7c{tqs$M|?|Z7q4B zT6V~&d5}8$a&uffx0!Kb{|eW6*UyODTt>Yn_joU+Xlt|KtYF>J?#0DhuuLR3Z^plS z7xm!-3;SE8S?~S9oueaH*ONrv4NP%y@hCpCp~W5sKUohC5hZ2i(VsuVU?9}dgbxGG{}V~@Z^U%rT<=2K9BT~kw2@4QX|GmcA54Xdu^w~dU9 z#E9*2a{ZZ?N``*9l478)uI|6o6T7tBm-u^YD_E2Bk)8PPE6&B%C|!BoE**AIb57Lkdl(-zzRNi z@St~Ss5^mGIW9RlBq#`T=d>ivQ;-LqDB$HAA!2#?b|qtii%a+yPXvT#JOcGzFlNZYxx7(*{tcXcTmn#f6J+ zZmo#wx@`I6Q(IduiIc^^<)x*Ea1rX-M%S(PkTQ)~GhFCgoSg5YX@n9KSeU|PWnv}I z*y$uZlg`f1w;V*f@4jzo$&R6yP|6UpV}sL7@nM2C)3RM%U9KY8gP5}m3u+8L2gLB6 z81bY?v)XK!{<~#OtteJU7p!Hq*RieA>4Juav@G8<3zEn#Qc6k%xKBZDZmz|7MzVi#aj|0llX&S{IZ~Iq zu|MYLCASciPKgkNo~vnQ3b%;VJv~LAX=|(X4<})Y3kxd@OI?ZMVxoT=7%+Z@)g4t- zRFoSPML=>5^PnA{J8sH4>-(-2zE0k#x~r?8A`8iMmDvr#8#mNMbg(-}Anj2PytlXa zesk0M&*o{6TlaP?G zNtk|b)~(Tv&R0%hVq?Q5BO_BKwv&^?=H=xzU0zyj3ykYuS=@EMzOh^NXx0fg|4Dd6 z1fHzCJTt_LWsT?e*KDK}s)ZeyZu8;G%f_@4o}|9MzJmC!oI1O4sY!%1f{PH8~PGHN)8{Jdu6Murky=K zu~ZB_sq|mJepPtiVl!@c#W9I6FQ$8EeI78)G+J9iGf>V4Kofl3!UF4^V@43t`Ng#(w{PJR(koEe`|d zy1JGYxre9c6UdmAwY6B$%k#f2g^wc1<5N;7aD!zcqN0{DXUE68T)bkhl~-3Mz0b>& z-=fL=^eJMye(CzQ37MatpOT^?W3=4Ex>-kjw}IZH^LoEwp#|@UX=!OJhgtQfY2(MrA=GmLORfd3)~~>=G|^ zbhX`rB)T-f?4tFzZ{HNyNuTKH(F*YMLrAej%khM;H z2cg5x#%8MI+kAED^=tpM8sZ4z>O*a6gqAJl7K0c_ z|I=aoo`#b07NT=)zrn|9vWykse6oY&IQ?90_wVcw(?5n*g!h~6+EC`xJttVbn}|=J zKK(j^KqW@#HaM=pG{k-VO5lMIolCoSeQSdR1Yf+?|l-OV6ugvk$5eZ`N_&7U(+iIy|)w8sL z+-!7YL>lq2tZeAjmoC%l)>df*C7<7$JEP;{SO`Ijvqr}iJj8%|??A8k^_J{hd8YU% zB`54>&z{vEPP{-aE%9v>P}X~&^7>y{>{;H$6TWo|G5OMs&i4d~bN|m5M4v%UiRg|ZLSGA zG1oYqyQ?w(d}bXR-br3vI59Dax^7YyX>#rz9I#aCs6fh-&jj3VlzgispwucMA(0dp z*E-eJ**PNiw~6o1{tLUWT|P09k$EvO*O{268{N1)yu6+o8s6IaSs9p+m?*yz&&Ph} z4zrt^+u5&3Zno--1HqXl4?ZkROm!QZ(!n>cdDz|;6oeS_Qc0Zs&P$wD^%&ilr<<9ZI~M4oywyZWrR7fHGqOy$X!?uG9mwFb4TGz1`le<--yxAk zXZ;43GEk#yZRacxdsjHde@LAyVvyhkS6ff<0w|fqvVZ)&EC19{p{SF1^oZV^t32*wxC6+EkMxLOdSftAU8eN^HUT`wPxA{mZ+sm zwZbut5hoSZdzcnZcu#HVjkSNM^cDQjLLbEYzAy=8e+12$|Z#;AF z;NT-8BSu(Ehq1>(DBdO_BGNlB5EL33n%8cmf|1x4^!@u26kW{8K}h{OxCyoJ^XJbM zFt3uAjT5<6X~H(~6oGC2zka>qVutO#MG}tUk_QLQwnizt^B5+=*wJ!%P}A^W#Tn>4*sL(7@Q(OLHyGUlBs$&@QDFTatQ znfZHjleXsfaqpL2lq9mSXamAke;AL2j>g2qBv%^mJ?Ap{AXohsC#U5E;jed`T-=M{ zl(e+V+a$`N-uFdwxanD$tAXbjs=L){scFG!^Uy zy_m&C!=T{c=;tGPTq(n!9BgY>)5$Apemjdo^vUFn+P|Wj0!3M^d(T;v4q^gczyU9W z-s_Z4I+9I^GvkQ}DQeYub$bS;n^=jLc z+CvFyS?j`r-^7G69q!EvI*-Kw90cO(^0+0Fwyy^NMN}&C`~R2n9hd|57ODPJT!c4y zI`WOsP3!qpS_x7@aQ|;FdTejQ+IGBp)G zUaZ|QGvlRqo?-h1cYJ(&si1h=va_=@YAQQD9S<>L&VK^%-6L@c&W1WW=~BUh)35|e zg~M(NN=ZqboS#2rOEf~Z2Rj{Mr`|;OMFvx-18xBWh6QUis0N_*ATx-n#5%*1CAQZ^^NDn>Y6f%1+FEJE~8W_YL zZcH*WF}>28Nip!Hf)D;bBgWpI2W7<2(ppb4Xa@!cB6yJal6?6vxTK_H-gIWU98 z`Q$@(QW>t4hq>y~06QT4K>hcA`}Wx#;|n?$<6?KW9Lh^*Zl-r}arszU8Z4KGhJajM zgo4`oJzqJKc4ZSaB=GW%2B)T6&8XB71$&K7`%QXM3zFM1^ohh?yMn*<7@KjI; z8lRMe3Hs6BA7K`{_Fb>R5er1iQo-@T!Q!CMLXcAa8#wg1+zg!)mz>cI>h00k5-r;6 zssU*_U+o6PDu(!&TU&SjJ6?!AJM$zUBxDp8rc_S8`#@Fo`sb>u+a+H_&_nTcipPI7 z{%!8qUFvaw(gbB@)@{M(XNzA8bBCb{@mKv=NW$>geQz`Z&;nkD8puW@ae83ncpWv<6ib&3`MbyQe1;GjoT9gRpEX9UWa* zM1%~;b5PfzV%zl?VDrounhc=(UY?q3cL~RtdBi6B`>99(FDN1aES86v3GxU?zTkQrj(8zFys(hC0z> zjR{l)%1yBMI-na-dsLmV&rJcquxU>(<=4u4Ks{bi6hFco}L#fG|YoE5C ztrEi^rHTL=9;-;RU%I-wN`l~}B)E=i%UgE&1P2@Y8UhqZNZX6rVa^Q&|6v4hW8o2fB&B8`^Mqx@7+HF zz6E}kmMm{FbdB)#oHwMJ^Lt&wsaO$q5!NggX<-pSY&qOL<@kpL;R^9K| zD>V|G_-FboKK(d>gGM~fU{YWb-W1hu2W~5 znaP|%W#GMwwcWI@3b-PEF!B(U^bQV{FNXv&#hppFwzh}Jz{$pZ8Tr8Lwe zPdkThU~l-7#ZE(g)o|%59=ms{prCLoZ&Y~wv}D(WJA*hqBV&Eu>o0hgKuy`^$R~N8 z(~BmewhKnMqg@uISVf79AiKjZATYii@H|k!pgJRi1}&$p?Lp+awqIFE$pGfuBBcLQMwcGPyn;3hor*Dx>yOQISQ|;7v900EjRG0)kuI z+&5Z(Ka+aK`F1emw@Py8(62-_$p+4AR zJOr3iApm`u8rch;8~3)IAa=HLmbvs@`_WASY2kV8| z37VWMzqZ%cbAjliq&7rgx{w_`tV0NwUVUp<$&(^>@E+tQM@B~<$nsmziv~gsOi;={ zI9ZAXAMy5=1gbK5NJ-nKT{+msMR4|khE$jftr@Hu4X6Sbpdb@Uy`SDLy3?`=eRoZN zlJa7DIyLktM(HbgD4&{sL-##hNr{K1f#1avLoLnBu%SvK2fi?9L++*>bbY^nF2Lq~ z8C;!F2*vXS8r{Rdz&L^Xqx_%Yfl=oSVc&m;+Mdht^5Eqq=y4Thin$G?Q}|O>QGC@` zgGiC&=8(kI#XjGj(30ySJ_XmvQ#FZ4V4-`}CAZb5!&7+zg!lFIghIy(1y5Z1 zO~S8R1g(OhXVBByifHfXutCN+5IPJ?954RY0(Rf5?5VJs5!}wNO#3xr$}jkEWp)`( z?HnF<0UNN9>~HSCwC14%zJvZ&DY(XJ@>N#^8DxiJXAzZaw;@l|^UhHX;gZ`i!)vc6 z%U*(BafkRIqN5`WmI<(#sYL>)%bJ-L=E)ch5P|ySZn+?tskM2iqC&9!^;o~K>sL}% zJ*c+}SPfx^Uzm7!c=li>-PLcR1e+%2daw}|s&e}rl6~v%*8rPrtWd3EaF7tJbe%8G z99kth0Rsang`I+Tz9gKVoxvvGM>-ZmJBo)oIxHpz8=5zU&IFmNq0k;#Xx>j}ivmkbf$jQ5dY*=Mcob8>66E<|K zqo+60W6)7FgC$>jyeWYdqZ}fqd+GrX<=DyddgMdg#htl0r z`^@z`{}1mtAKr1!`{^BS-457$t#!wo^SXZX4pdTjNPL0j0t$s9mXXG&pipNB;r~el z=iuMhnA$9OJ7*yG5QD-Zf6{8Qqu?j_b~2A7@rN&v5z`Q_saY(dP)sNpjD(tF^6K~- zrD%sl{0&ZCf$?tQN25#iZsE7UN9JXl6a4Hq|B4nvMh7kX}_Wp3>(jpH6^`DA)}gA@(T^nT8g*Z#`9 zYxU&%(Vnv=Ik~4km61)>U~GYhethd$LP9@%`Nl>seX6Ko^(vH+QAlubT6Q-6t(Xfm zA?IppYET|)YZk#1&-i$GeQIk(z4i0+^QUKK40^wR|4ssbr#2nQF8EGu|FyER@=&^& z{5Mb^{noeH&?|r`uCs4s*|Jm_;9_n ztW4s16ui=FYR2^%9PI4q%27+$d3cJ~uYIGUF457^Rbc7q=_}dsJjGG8Np<+@@PXk&v*KvXo9)ZN`3 ztyxN7P(*cldb+W_{Xj{H%*)G*DMDKB#S6YmCCLeiDwLEZc{Mfkj~_p-u%11)w7gvT zR8EdiN=gdlp=GjTrYj~U7SL>P@b|BNUxp-EAjZnZrg$S-_->ZU`AY53*jP#!OnO!p z9?YwWxw)jREl*-nQe~d|6)qkgGb<~uva)hOK!8U{Nr`Xva|wNYZdE@&Kda?I z_UO1c+i9!W7GgU)I~3~p z3cq}j($iy#<pijt0l7inl|l^;L${q*UU+LI?4pFUl1SQ~4AiKArK^f@?i zWMyTY%E^9rUtXSwj-HQF{CsPc$_wI-25rR+j$iNErb!ahY907$GHPRG(>CTYGy$j%s#zOpNdM?+R$$ zS~^9s6JF%@$;m|c`1o>h?eWqaaaV8Lz=shDx}OSyyC#O~uLtQL?i*J3Eh*7?Ymtes(Xj(}*qJXq*`- zGm8!n7e_7pGEU9<`c+si?pv3&W`3;b>4BlsOyG^S!NJ(mX~t8}XxXf+&P4NTgmV{n zA@Qt?mXmI7ZWfl8w+`e!-E1NiV-gbj^&^YhHo2xoWN+n{_dSQTsowMlZCza$6O)^@ z2Q!4;w;kq1u&x?RFsrl;^yYAu=(>A9@2W7 z9}TS#GR1A|3j)OYRIoUBitJaL>)ahUr3+egHCkBOI;LPka=mZNiJZk#$94-ZfJ z(W7RFi9*wXTXJzc=8*fx#`C*QlxubewGLn{YYO)kdJ4VqNoS7M>mELSJm6AoVd9pu zCUWPF*TRBH-m_}T^*U^ARwp+h%go^3-0??AX8^ga`H_4vN}dK3)YFHYBu8oR}b zHCVLidI{e?fi(^H_CEXC&Q85FbZg6Iq|RNeva&M7>`9KA-BkUVix+$;$jHRwICc4{ zzLb^4*slyrtgWrFUJP7l^d-dg*uXxl+{GIHRJJr+4G4g+SRF3%9vd5j;0@$|H7w4~ z&W^#9+AXShPdf@vR8;M1YHFGs?X9ws5lAzUDLFaa9T*s(PMPq3G>O@k$sPF7;EgYH zlj29@HMyIdoMBbf)h~w%o_(9&X5-@Oox-hZX^|R%DL#*jV`FFc{_^c7O8WZKYN8*g zZ5Mi(w{~_|L!=BBRgkeY{O!2?xwoW8)NJvNG)n{(`fFyA*um6UQ%lS2+19X2sJ8(D zQ+}$qVvzAcfl<@Ykh$RNrQ^KH=WTtNf+CpE&vyQMh}n&}P8pU6B?AMNveHr|EiKwW z49nZV!0AKkdtJj-yL{|AU*iWq>nh4-MP48zY#$hiadB~}*d~-uscoO@Pk-Pqovs8S z;!l9W!^iJ;UaxrwcPTC|CP4Z6`dT;1W~tza!yMSnby4GpGcz-*p5_^OspPPlnVEHb z|Ng~}ZH~9Dk%gZ>)@`pORilb%X>E;PeZk4eslq7#i5v!V_Uzd)nrG|z4HvP48g#H(%<7+`8@N`Qi7A^-BQC9%WmQpoaHrEPR{^iJ=7qIpC_#Ljjq zcI?NC`2OR&-m0t@B{<@=s)DVJ0}`EDOjK1bp{SBo8)i2da?bhQKZ6=$-+iQ?r{MaC z*Yt*oxH!rKf1f$Uq~f8gm}-vNtyjN_@kYxnTg6WL#YDCojXG+a_otSZVUu*3>i9Ny z#N1X^Qqo(z!;kr6sB!bWo-JVJ45Kr)NLSzTNSPu~-w7 zDXZfH>-X8&T6rXfFq+=JKJIl6mE@=TMP@@BYL6eMXJj;HybgAo8Ek7K0Qo?ac&3T3 ztTyEo^R7Qz(RTdYxpNiRUFHn;$oSf%C%N=Pin6j7P*dX$laf%6P-#$tA@^M$A{G{8 zBSO`l>}eHfJ$puvnu45%kBZ9fiQcCbNj`NqoW1L`^RdD1`!#=3#+E2W(epWKrVtRF zkz!s(jo(x5vGMW6`1$*@KY0MTYoGQI%CVZddK+I{T-+scWl2fAp@P!V=zxH?K|$?M z7POx|W4nDj=E+1vA{2wHoAk|aR6?vFe0Yy>72)YiUB zPEMX1jUdbT`^7sdU}2)h`S;wM6!vr-Yf(hAqq`EQ({k9?+1{T1@#D?nva&3At8zQJ zTUk-j`%c8U;wmkOmKz{7XSV;AI`3Pk|lw# z?}{BRT!qh4(9+6*>bW$irllpfJeYsg*w`47WvT0ty?1Bvqm)_@NV4+s$y-(}Bd&k{ z#A&ZWkR#Rm%$YNG(~Z6_-JHS{vQ+xE{&cckz1n2J*OeCe=JmPkiTz3UFk)K%DS^7b z#3T&DCW|)lc;cCTdb2Gd2g|zHw~>(-E2^uts#tArr#wAE?+g|^3+fR)BElYoVFLsv zUHYfWxtrpXPEg-`vlC zGMnNsAz^BID>5p|`cKE@AO_iY#M^h#D5hJtE@Wk8Aq5RePN9C&Id9u@R7Rg5=aDfm zgo22pV01fRR!9~+BbsWtSZp-*m6Q;*v9VEqMc2i1Y)qS%pP%Kj1pNZ5%%s*61XZPL=96pT<4DUs?1*YA|R{*Ap!A)Q+ND_b2F~)7!N{oxZIKv zG%|dd$N$go-+H@C1L|d_m(StjTW`)t(%rLvHIefDgp2SN8dX0yNNM?X^BmO6jcI?z z8PH@8q@@YISWbo}C)3$qr8I3Pj%klfkyICM}M(<(}ljx!O=3^rW5ZwU_)Kdky|+pZ2C~4NJ9jq5Yjg|G=k85}O z)A|>cKo)g%$s?Z#2?+tgEh!~+?u*6vThI`4ae`Nh3LU9Z6#PN;PXBI?5_CP}rMQ4c z$*B`uTFQ&4bkOq~TU*6;30)7ys$LWRNAPp#)&`%Rx?v#?;~E78MOt1Sk*lk#m4m}W7$ri*o`xg;~2a^eg>Z+(H!};^))k{qxvO3=>s;hVL#>o1D3;x%#y*ci?_zUs`T% z=af4zf-+5FuU#4P-DF?W_{w14W}N+5Ml6-Lw|CSY&>*55wYzecxos~K2H|lC3)7L4lNS~j-x(Q) z%nR8u`Ol~L$^c(H@05EEUahm#tNajMjM#(L5^ZuG$VhsH=A-0%U%c>*kEa5@ zqM3Hfr~sx~Z*!(uy~qGBFQ2%MM3{k;vt}pK_mjaK4XlU}P-?(FQO)zzgg z7m(r@dTt0((Xt-aSy)&g`?;iq2N&mz&wXYH#_8X`ai2bY3jP*0zQj$6#_n!n@O6+% zA!ZAASlL;#&}fFf-d?i1ckiYt-Rzy1Ao0EL`EOj=y?$-&$yN0xqwMH8;aj*YT(Dt& z8^9zExE2E6`x}nJf_LvWHZ(Not%`n0dRJS+edtSx0+GAXgFWs!=(cogdOhSH#jTl7 zNfY8{wzj(342*`Ch8XfYsMEgDQL|Ez!M>XL{A^siTB4c1hKK9N$5RNy`y^)O=FWkH zJUBRj1#IZ-BxH#ofDuNy=5>8jR}ba`4Fg=S?fD&E0fEf2vdiFpyzi%bXmhlJ)CXaX z48j|)t)bzJj*bq<4yt{;J>*|sdt2Mt!D!nM*({ig%IYNq_T3scMkj7ZgLH*4KMnWroko5OzX_{Wp*I{``rXAa7K7|D}b6l(F#*5B#BSsEG*cym^xV%E}m4 zLP7$NGUYp(66dc?8AV0p8qq+S8|*RaG>AdLaOCQ1Hw? z{{B$yk*fpi1Igh+_e9&46aCYa5B!CarY545qhn)dpqMkU00u@L1%&1F^fXdB8yg$v zX0J2y^gt@4euek+@#E>e)luX*pk4u>4TVhet+|<*pPv%s5WU0YLSGG0G~nTgq@*Cw z!kO>i z9jsNahbJTif?PiXEeS-+lv~iNsH$oRa&_@S7C@LU!d?OOB_<}4QBei#?AW~;DLoH- z_0qfid&F~ugdtMipX*L(bX_*_KqeAtX=#CuL{J~CfQ3(adAZPppME@dfo@$W=+fse zULZ;yGSM(l9)!ifUWi{d|G-H3;>8O=o8JVdJK18;FkpcTaMm8MymLEzx#o1%Pv7Vv zaQ{0zJe#dzr{wTi^(s3yGqeg7T`Mot<;lBz3@pFVnJra9;zj=NAf z|1J}VmMT8`n*}z5@$vEDB13$Bi?M*=VfCMbgEQrIC+x?^#~-$jj9Xxh^+B}uGbn;d z-&>y)Gn?N^%C+!IkOvQDV{2=@x1upt>q@JVLy_usm?P7qKtow>Ioa~|@@>Sdloc>;5Q%fnZ%y%k3If0X9rl$nlCZeq9wfOO*abJ4ZF)j)&K$N z1g%g|STB}puKqszsI=P}dLO{CGk~wE+@zTMb z(R1=JBn^G2c0J-(QBeUV&N)?wJ*o@YH8}2FtaUw-z7-Rxng1@3DT({fpFgGUST~ph z+Mzs^oP~PNv#b;s*qE3+V8gxQdIb{pA1XOMF2j1U4^R%#7xWG=OU(}Tdn_yo@>2Kg zSC|9@1Z-?9 zS4|;>Ee`Ghlb)VlYSc}Wxjho!x2^o&^UrXY^9p^?2rv6TJOY5)*4G#DBu{;Fn1LD1 z!EqfTtD~n!VDQaxUpSPw;_~wB_1Ytgxm+HeK#al0ANuj*27E>(XXktLVs6POB@6~v zAXz2nJpdRmAK8!xU@><_%sx{G=cc9UjWyb=ja6E&LY0AO1C;R|rU5L@)d*<}zz}UQ z1R<8!erOK5(to(SER&j-v`# zu(0H)$)Y}1RV98;7J7iX$;$e?W81A@xYG7UzHZ%wdiJLN=DZj-;gz}hOA`~5x!XJ? z(BAOoY+X1Zfj&q8L$VUTJ^S{cmL)mr5D-a)J=p7WvrxKe_M2({XACtp2ZX``@I>wH z1$IK!4|SQD-e!Y~cG~Vh=B}e))f3rvjh9>&R#*SDIP9-I^L}~f8d|Cc3n`q1MI}c~ z``*dAV~T=+#RP2QWJ3HC;o_pAgq@SQVgz(NH#BVO_E&E4Z*FCDmj@+NqMDEZ8j;FH z=>G<!c*4k<;+i&~{>|;0(&((>VB#Vi! ze|xK1za)KpH#qnNNBn-emFx-mBTG?vwQY6Pgs@8?>;J*CZ7|75EAdPkSf-+s7Jo^A zbY~o2DUQ2EHJm^~NsWUM9-+q(D zFM=dI61Nak_c;Q5fA-j<-CWc2)kljx(e}`@j*f^x+75PyJBzKNXwj1$RT~i5gD+jw zK~qOcvm&YdyUPonDP>A4Phh?u%gY@`W+7f!PzZ{QGUFZmJ~R~PfnVplyOVU1>3(Ug zRkjL+I=_gV1xVsS2LynbT-dL}ib!HGWT?aHx}$2gnz$mjyZ7#$NBR2sDOA=icKNrD zB>hNbTish5mqRVUB&a&oRhm41?lUtpvk)RM!3DuboeX^35qq+~X^Gvl1pGiV`bMFD zQiIxY<7+^AIYRV?&MLH>P$+O!b5$X3=(JOzj6-Luh3XK|K*`DfU-k<;;mOC` z+$La2*4uNBTmUz=b$9=%O1g96bf`6VRvc)Q2R^9|!?ONK!X3sBJl!6ff5n`V53wON zJ$;!E&m6DXx+kA(#noXRJUBb?W}bdlL_Ye?=oj;=fV@9_`ji+*mPCF?Z-ZL+uei9+ zyUG609#9` z%66Uv)+-VSL4zWX>JiTiQRrb?&sMu*Ya4h&Qid>?z`#IgE_~Zn)zq1BxN) zOTW7Uv<0uDqEk{HA!+OO?b|pT!}O1i7c#@zMn)2APY;&^oe~c27khf1aoYQ39N06j z$nPa2iIq^;xic811HEraNy&)(e0F&2gX-Dd-0TZ|(kA*}h#dQSbaW}TCmT8lQJVSJ z!G4WYJA7{F3j^c|9VO;__wK=4Iy9$ffBx-z$Vd*K1tDN+ViI5YVPr&86U3L$y?aqg zH{U~V(bk{vMq+GW%ZsIBz=|J?Q(a?MR#z7jjNeUvC*^*9xVwG?QYZqNQEk6|CGcBL z2(NivQ$0#ra-niA=oo(U2t&ch*n`)qHkVmsuj}^rn!qWbDOnkrbSMZ_R@05qb2V8e zyfh;<&H@@*TK#YXevQvjy01Th7=jXu>j5Z4{}m})6BQTVdxmRWRNJ?1-b~Aqi;Dzm z=6bYRPP**6m8)R>>eWW|!gx1XMv+?s1`b@b&~j4rc)9NMHbPb>Pxs1|atHc3k`u%% z#;cl7+yRik+;5G43R_sm{p2++K0cz*p`-r|kUDahq+g0_;L#PR_hKiDitR8dK%5q` z#ZK79E36HdM#a1G>L2XQ)(4B>%hS)xe-$uHR>;nT?u;sQDZzg#!SR!mX;Sz2m8Bnn zRCP-~Dd30;B1uKD$F`u>SeTj5RNJpM265J!EZ(@m-Q@)1It!`}Xqw|(g7F6Q zB&R_2Isa_MmB+44V0>WhkwXQr-B4kzO;xX#3*T%TA>CYvr+#V?07}S)R!9{M0eK7? zxdDLJ=i0+t_G@D=4;4cK6ZV-Oz`2rx!{yJ`hdVDpXy}1eU}Iw&Yf|h|;%ef;T0Vb{ zi<~AgGP(}>SXou|Y>|3!2(5qtC_I4leDh5)#%r6tAnbD8wz$58ov3qX zM8R<>@V1@+hhZ|r!H$Bk#qq3fe9RM^4&@V}ki(d3kf8Z?NwFS)%8x%h+iGCj|2gUe z9YAdf>%)W-N8e@)I5VYZ&q9&}ETI8M2?`q&kca&B zv*gHATnzlign^Sw)ARHA5F!VMhc^4Bdhtczq2YT>QSI=uLd1zxuUJ6G!~_EX0sIYy1!!q57K~pvX zEt!~@0Q6eALBTyYI52<*XVd^Kfs!sQEft4TWpEq|yi$1k^K$|V)7yWM+d=5 zSm1@An(=XZgmT&18fx99OnZ{sH!y%4E`l~#2Am=T!UHdJbMu9Tg?a=QO-z8UA@RPK zAtWeR4}o_v&}Ve%=V#%a+mUYyeK$T*TByeZkB5GAW`2IiQR8Br3(%(7L1~-Hu>~Gw z-}}sP6k=*_t_81cxDIePC?YF+d%xV=+y6mu=}H9YN(Ue3H^pKBe!*ccCuirrp&|Sj z*=F`*h)CqP9vRiq=)eHq+M5)ZPnbIBzj(n2;attvnwrXdNuW?LI>2G|qobquRZrFR z^z}IaJu2O#h;oZ~SiZcnf&sAv`i5vNODGmZ-WAq=(L2JSfOX{kbEXgnrCmt1{9%4( z=FYUy7G@ks94}2spMHxyEdzrT@J0{(?9(uq^vpi-+yR=^4=OnoWWD7{0dU~&z~!`} zFa;d|4t9EVwVNUM6$2VQ=LJ>LoA0A$zLc&mBOF+O`37Lw+u!f~FAD`?1P1{0OiTi* zl?&YTc?OBOw8L8y^Jv3by_IhA=8P_QfZr-CD&nTmIkZqvP(bGHpN_)sFNNCL+AZeR zMR*f4|Dg8BA8)FcWA&-F4gL#$r$xoYa(L;-3$4#!&)}b7Bvv_=Gk`OpC>cowOu>CU Gum1zdxGwep diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma index fd1cc9057..c9c165218 100644 --- a/helm/software/matita/contribs/didactic/induction.ma +++ b/helm/software/matita/contribs/didactic/induction.ma @@ -1,169 +1,338 @@ -include "induction_support.ma". +(* Esercitazione di logica 22/10/2008. + + Esercizio 0: compilare i seguenti campi + + Nome1: ... + Cognome1: ... + Matricola1: ... + Account1: ... + + Nome2: ... + Cognome2: ... + Matricola2: ... + Account2: ... + Prima di abbandonare la postazione: + + * compilare il questionario in fondo al file + + * salvare il file (menu 'File ▹ Save as ...') nella directory (cartella) + /public/ con nome linguaggi_Account1.ma, ad esempio Mario Rossi, il cui + account è mrossi deve salvare il file in /public/linguaggi_mrossi.ma +*) + +(*DOCBEGIN + + Come scrivere i simboli + ======================= + + Per inserire i simboli matematici è necessario digitare il loro nome + e poi premere CTRL-L. In generale i nomi dei simboli sono della forma + '\nome', ad esempio '\equiv'. Alcuni simboli molto frequenti hanno + dei sinonimi più comodi da digitare, per esemio ⇒ ha sia il nome + '\Rightarrow' sia '=>'. + + Segue un elenco dei simboli più comuni e i loro nomi separati da virgola, + Se sono necessari dei simboli non riportati di seguito si può visualizzare + l'intera lista dal menù a tendina 'View ▹ TeX/UTF8 table'. + + * → : \to, -> + * ⇒ : \Rightarrow, => + * ℕ : \naturals + * ≝ : \def, := + * ≡ : \equiv + * ∀ : \forall + + La sintassi '∀v.P' significa "per tutti i 'v' vale 'P'". + + La sintassi 'F → G' dove 'F' e 'G' sono proposizioni nel metalinguaggio + significa "'F' implica 'G'". Attenzione, il simbolo '⇒' (usato a lezione) + non ha lo stesso significato in Matita. + + La sintassi 'ℕ → ℕ' è il tipo delle funzioni che preso un numero naturale + restituiscono un numero naturale. + + LA sintassi .. + ============== + * applicazione + * match + * min/max a b + * sottrazione + + I comandi per le definizioni + ============================ + + Esistono due tipi di definizioni: definizioni ricorsive tramite sintassi + simile a BNF, definizione di funzioni per ricorsione strutturale. + + Definire una nuova sintassi astratta + ------------------------------------ + + Definizione + +DOCEND*) + +(* non modificare le seguenti tre righe *) +include "nat/minus.ma". +definition max : nat → nat → nat ≝ λa,b:nat.let rec max n m on n ≝ match n with [ O ⇒ b | S n ⇒ match m with [ O ⇒ a | S m ⇒ max n m]] in max a b. +definition min : nat → nat → nat ≝ λa,b:nat.let rec min n m on n ≝ match n with [ O ⇒ a | S n ⇒ match m with [ O ⇒ b | S m ⇒ min n m]] in min a b. + +(* Esercizio 1: Definire l'albero di sintassi astratta delle formule *) inductive Formula : Type ≝ | FBot: Formula | FTop: (*BEGIN*)Formula(*END*) -| FAtom: nat → Formula -| FNot: Formula → Formula -| FAnd: (*BEGIN*)Formula → Formula → Formula(*END*) +| FAtom: nat → Formula (* usiamo i naturali al posto delle lettere *) +| FAnd: Formula → Formula → Formula | FOr: (*BEGIN*)Formula → Formula → Formula(*END*) | FImpl: (*BEGIN*)Formula → Formula → Formula(*END*) +| FNot: (*BEGIN*)Formula → Formula(*END*) . -let rec sem (v: nat -> nat) (F: Formula) on F ≝ +(* Esercizio 2: Data la funzione di valutazione per gli atomi 'v', definire la + funzione 'sem' per una generica formula 'F' che vi associa la semantica + (o denotazione) *) +let rec sem (v: nat → nat) (F: Formula) on F ≝ match F with [ FBot ⇒ 0 | FTop ⇒ (*BEGIN*)1(*END*) + (*BEGIN*) | FAtom n ⇒ v n - | FNot F1 ⇒ 1 - sem v F1 - | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2) + (*END*) + | FAnd F1 F2 ⇒ (*BEGIN*)min (sem v F1) (sem v F2)(*END*) (*BEGIN*) | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) (*END*) + | FNot F1 ⇒ 1 - (sem v F1) ] . -definition if_then_else ≝ - λe,t,f.match e return λ_.Formula with [ true ⇒ t | false ⇒ f]. - -notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" -non associative with precedence 19 -for @{ 'if_then_else $e $t $f }. +(* I comandi che seguono definiscono la seguente notazione: -notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" -non associative with precedence 19 -for @{ 'if_then_else $e $t $f }. + if e then risultato1 else risultato2 + + Questa notazione permette di valutare l'espressione 'e'. Se questa + è vera restituisce 'risultato1', altrimenti restituisce 'risultato2'. + + Un esempio di espressione è 'eqb n m', che confronta i due numeri naturali + 'n' ed 'm'. + + * [[ formula ]]_v + + Questa notazione utilizza la funzione 'sem' precedentemente definita, in + particolare '[[ f ]]_v' è una abbreviazione per 'sem v f'. + Non modificare le linee seguenti, saltare all'esercizio 3 +*) +definition if_then_else ≝ λe,t,f.match e return λ_.Formula with [ true ⇒ t | false ⇒ f]. +notation > "'if' term 19 e 'then' term 19 t 'else' term 90 f" non associative with precedence 90 for @{ 'if_then_else $e $t $f }. +notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 90 f \nbsp" non associative with precedence 90 for @{ 'if_then_else $e $t $f }. interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else e t f). +notation < "[[ \nbsp term 19 a \nbsp ]] \nbsp \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. +notation > "[[ term 19 a ]] \sub term 90 v" non associative with precedence 90 for @{ 'semantics $v $a }. +notation > "[[ term 19 a ]]_ term 90 v" non associative with precedence 90 for @{ sem $v $a }. +interpretation "Semantic of Formula" 'semantics v a = (sem v a). + +(* Esercizio 3: Definire la funzione di sostituzione di una formula 'G' al posto + degli atomi uguali a 'x' in una formula 'F'. *) let rec subst (x:nat) (G: Formula) (F: Formula) on F ≝ match F with [ FBot ⇒ FBot | FTop ⇒ (*BEGIN*)FTop(*END*) - | FAtom n ⇒ if eqb n x then G else (*BEGIN*)(FAtom n)(*END*) - | FNot F ⇒ FNot (subst x G F) + | FAtom n ⇒ if (*BEGIN*)eqb n x(*END*) then (*BEGIN*)G(*END*) else (*BEGIN*)(FAtom n)(*END*) (*BEGIN*) | FAnd F1 F2 ⇒ FAnd (subst x G F1) (subst x G F2) | FOr F1 F2 ⇒ FOr (subst x G F1) (subst x G F2) | FImpl F1 F2 ⇒ FImpl (subst x G F1) (subst x G F2) (*END*) + | FNot F ⇒ FNot (subst x G F) ]. -definition equiv ≝ λv,F1,F2. sem v F1 = sem v F2. - -notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \sub v \nbsp b)" -non associative with precedence 45 -for @{ 'equivF $v $a $b }. +(* I comandi che seguono definiscono la seguente notazione: -notation > "a ≡_ term 90 v b" non associative with precedence 50 -for @{ equiv $v $a $b }. + * F [ G / x ] + + Questa notazione utilizza la funzione 'subst' appena definita, in particolare + la scrittura 'F [ G /x ]' è una abbreviazione per 'subst x G F'. + + * F ≡ G + + Questa notazione è una abbreviazione per '∀v.[[ f ]]_v = [[ g ]]_v'. + Asserisce che for ogni funzione di valutazione 'v', la semantica di 'f' + in 'v' è uguale alla semantica di 'g' in 'v'. -interpretation "equivalence for Formulas" 'equivF v a b = (equiv v a b). + Non modificare le linee seguenti, saltare all'esercizio 4 +*) +notation < "t [ \nbsp term 19 a / term 19 b \nbsp ]" non associative with precedence 90 for @{ 'substitution $b $a $t }. +notation > "t [ term 90 a / term 90 b]" non associative with precedence 90 for @{ 'substitution $b $a $t }. +interpretation "Substitution for Formula" 'substitution b a t = (subst b a t). +definition equiv ≝ λF1,F2. ∀v.[[ F1 ]]_v = [[ F2 ]]_v. +notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }. +notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }. +interpretation "equivalence for Formulas" 'equivF a b = (equiv a b). -theorem substitution: - ∀F1,F2,F,x,v. equiv v F1 F2 → equiv v (subst x F1 F) (subst x F2 F). -assume F1 : Formula. -assume F2 : Formula. +(* Esercizio 4: Prove the substitution theorem *) +theorem substitution: ∀G1,G2,F,x. G1 ≡ G2 → F[G1/x] ≡ F[G2/x]. +assume G1 : Formula. +assume G2 : Formula. +(*BEGIN*) assume F : Formula. assume x : ℕ. -assume v : (ℕ → ℕ). -suppose (F1 ≡_v F2) (H). -we proceed by induction on F to prove (subst x F1 F ≡_v subst x F2 F). -case Bot. - the thesis becomes (FBot ≡_v (subst x F2 FBot)). - the thesis becomes (FBot ≡_v FBot). - the thesis becomes (sem v FBot = sem v FBot). - the thesis becomes (0 = sem v FBot). +(*END*) +suppose (G1 ≡ G2) (H). +we proceed by induction on F to prove (F[ G1/x ] ≡ F[ G2/x ]). +case FBot. + the thesis becomes (FBot ≡ FBot[ G2/x ]). + the thesis becomes (FBot ≡ FBot). + the thesis becomes (∀v.[[FBot]]_v = [[FBot]]_v). + assume v : (ℕ → ℕ). + the thesis becomes (0 = [[FBot]]_v). the thesis becomes (0 = 0). done. -case Top. +case FTop. (*BEGIN*) - the thesis becomes (FTop ≡_v FTop). - the thesis becomes (sem v FTop = sem v FTop). + the thesis becomes (FTop ≡ FTop). + the thesis becomes (∀v. [[FTop]]_v = [[FTop]]_v). + assume v : (ℕ → ℕ). the thesis becomes (1 = 1). (*END*) done. -case Atom. +case FAtom. assume n : ℕ. the thesis becomes - (if eqb n x then F1 else (FAtom n) ≡_v subst x F2 (FAtom n)). - the thesis becomes - (if eqb n x then F1 else (FAtom n) ≡_v - if eqb n x then F2 else (FAtom n)). - we proceed by cases on (eqb n x) to prove True. (*CSC*) - case True. - the thesis becomes (F1 ≡_v F2). + (if eqb n x then G1 else (FAtom n) ≡ (FAtom n)[ G2/x ]). + the thesis becomes + (if eqb n x then G1 else (FAtom n) ≡ + if eqb n x then G2 else (FAtom n)). + we proceed by cases on (eqb n x) to prove + (if eqb n x then G1 else (FAtom n) ≡ + if eqb n x then G2 else (FAtom n)). + case true. + the thesis becomes (G1 ≡ G2). done. - case False. - the thesis becomes (FAtom n ≡_v FAtom n). - the thesis becomes (sem v (FAtom n) = sem v (FAtom n)). + case false. + (*BEGIN*) + the thesis becomes (FAtom n ≡ FAtom n). + the thesis becomes (∀v. [[FAtom n]]_v = [[FAtom n]]_v). + assume v : (ℕ → ℕ). the thesis becomes (v n = v n). + (*END*) done. -case Not. - assume (*BEGIN*)f : Formula.(*END*) - by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH). - the thesis becomes (FNot (subst x F1 f) ≡_v FNot (subst x F2 f)). - the thesis becomes (sem v (FNot (subst x F1 f)) = sem v (FNot (subst x F2 f))). - the thesis becomes (1 - sem v (subst x F1 f) = sem v (FNot (subst x F2 f))). - the thesis becomes (1 - sem v (subst x F1 f) = 1 - sem v (subst x F2 f)). - by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH1). - conclude (1-sem v (subst x F1 f)) = (1-sem v (subst x F2 f)) by IH1. - done. -case And. - assume f : Formula. - by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH). - assume f1 : Formula. - by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1). - by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2). - by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3). +case FAnd. + assume F1 : Formula. + by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). + assume F2 : Formula. + by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). the thesis becomes - (sem v (FAnd (subst x F1 f) (subst x F1 f1)) = - sem v (FAnd (subst x F2 f) (subst x F2 f1))). + (∀v.[[ (FAnd F1 F2)[ G1/x ] ]]_v = [[ (FAnd F1 F2)[ G2/x ] ]]_v). + assume v : (ℕ → ℕ). the thesis becomes - (min (sem v (subst x F1 f)) (sem v (subst x F1 f1)) = - min (sem v (subst x F2 f)) (sem v (subst x F2 f1))). + (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = + min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). + by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11). + by (*BEGIN*)IH2(*END*) we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22). + by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111). + by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222). conclude - (min (sem v (subst x F1 f)) (sem v (subst x F1 f1))) - = (min (sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2. - = (*BEGIN*)(min (sem v (subst x F2 f)) (sem v (subst x F2 f1)))(*END*) by (*BEGIN*)IH3(*END*). + (min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) + = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222. + = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*). + (*END*) done. -(*BEGIN*) -case Or. - assume f : Formula. - by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH). - assume f1 : Formula. - by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1). - by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2). - by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3). +case FOr. + (*BEGIN*) + assume F1 : Formula. + by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). + assume F2 : Formula. + by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). the thesis becomes - (sem v (FOr (subst x F1 f) (subst x F1 f1)) = - sem v (FOr (subst x F2 f) (subst x F2 f1))). + (∀v.[[ (FOr F1 F2)[ G1/x ] ]]_v = [[ (FOr F1 F2)[ G2/x ] ]]_v). + assume v : (ℕ → ℕ). the thesis becomes - (max (sem v (subst x F1 f)) (sem v (subst x F1 f1)) = - max (sem v (subst x F2 f)) (sem v (subst x F2 f1))). + (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = + max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). + by IH1 we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH11). + by IH2 we proved (∀v2.[[ F2[ G1/x ] ]]_v2 = [[ F2[ G2/x ] ]]_v2) (IH22). + by IH11 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH111). + by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222). conclude - (max (sem v (subst x F1 f)) (sem v (subst x F1 f1))) - = (max (sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2. - = (max (sem v (subst x F2 f)) (sem v (subst x F2 f1))) by IH3. - done. -case Implication. - assume f : Formula. - by induction hypothesis we know (subst x F1 f ≡_v subst x F2 f) (IH). - assume f1 : Formula. - by induction hypothesis we know (subst x F1 f1 ≡_v subst x F2 f1) (IH1). + (max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) + = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222. + = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111. + (*END*) + done. +case FImpl. + (*BEGIN*) + assume F1 : Formula. + by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH1). + assume F2 : Formula. + by induction hypothesis we know (F2[ G1/x ] ≡ F2[ G2/x ]) (IH2). the thesis becomes - (max (1 - sem v (subst x F1 f)) (sem v (subst x F1 f1)) = - max (1 - sem v (subst x F2 f)) (sem v (subst x F2 f1))). - by IH we proved (sem v (subst x F1 f) = sem v (subst x F2 f)) (IH2). - by IH1 we proved (sem v (subst x F1 f1) = sem v (subst x F2 f1)) (IH3). + (∀v.max (1 - [[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v) = + max (1 - [[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)). + assume v : (ℕ → ℕ). + by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH11). + by IH2 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH22). conclude - (max (1-sem v (subst x F1 f)) (sem v (subst x F1 f1))) - = (max (1-sem v (subst x F2 f)) (sem v (subst x F1 f1))) by IH2. - = (max (1-sem v (subst x F2 f)) (sem v (subst x F2 f1))) by IH3. + (max (1-[[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) + = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH11. + = (max (1-[[ F1[ G2/x ] ]]_v) ([[ F2[ G2/x ] ]]_v)) by IH22. done. -(*END*) +case FNot. + (*BEGIN*) + assume F1 : Formula. + by induction hypothesis we know (F1[ G1/x ] ≡ F1[ G2/x ]) (IH). + the thesis becomes (FNot (F1[ G1/x ]) ≡ FNot (F1[ G2/x ])). + the thesis becomes (∀v.[[FNot (F1[ G1/x ])]]_v = [[FNot (F1[ G2/x ])]]_v). + assume v : (ℕ → ℕ). + the thesis becomes (1 - [[F1[ G1/x ]]]_v = [[FNot (F1[ G2/x ])]]_v). + the thesis becomes (1 - [[ F1[ G1/x ] ]]_v = 1 - [[ F1[ G2/x ] ]]_v). + by IH we proved (∀v1.[[ F1[ G1/x ] ]]_v1 = [[ F1[ G2/x ] ]]_v1) (IH1). + by IH1 we proved ([[ F1[ G1/x ] ]]_v = [[ F1[ G2/x ] ]]_v) (IH2). + conclude + (1-[[ F1[ G1/x ] ]]_v) + = (1-[[ F1[ G2/x ] ]]_v) by IH2. + (*END*) + done. qed. + +(* Questionario + + Compilare mettendo una X nella risposta scelta. + + 1) Pensi che sia utile l'integrazione del corso con una attività di + laboratorio? + + [ ] per niente [ ] poco [ ] molto + 2) Pensi che gli esercizi proposti ti siano stati utili a capire meglio + quanto visto a lezione? + + [ ] per niente [ ] poco [ ] molto + + + 3) Gli esercizi erano + + [ ] troppo facili [ ] alla tua portata [ ] impossibili + + + 4) Il tempo a disposizione è stato + + [ ] poco [ ] giusto [ ] troppo + + + 5) Cose che miglioreresti nel software Matita + + ......... + + 6) Suggerimenti sullo svolgimento delle attività in laboratorio + + ......... + + +*) + + diff --git a/helm/software/matita/contribs/didactic/induction_support.ma b/helm/software/matita/contribs/didactic/induction_support.ma deleted file mode 100644 index b8fc7ffc8..000000000 --- a/helm/software/matita/contribs/didactic/induction_support.ma +++ /dev/null @@ -1,25 +0,0 @@ -include "nat/minus.ma". - -definition max : nat → nat → nat ≝ - λa,b:nat. - let rec max n m on n ≝ - match n with - [ O ⇒ b - | S n ⇒ - match m with - [ O ⇒ a - | S m ⇒ max n m]] - in - max a b. - -definition min : nat → nat → nat ≝ - λa,b:nat. - let rec min n m on n ≝ - match n with - [ O ⇒ a - | S n ⇒ - match m with - [ O ⇒ b - | S m ⇒ min n m]] - in - min a b. \ No newline at end of file -- 2.39.2