From c775f53f9aae44897fb13342cd9f2e7ec5e394f7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 16 Oct 2008 16:04:25 +0000 Subject: [PATCH] ex for students about induction --- .../matita/contribs/didactic/Makefile | 21 +++ .../software/matita/contribs/didactic/depends | 2 + .../matita/contribs/didactic/depends.png | Bin 0 -> 10835 bytes .../matita/contribs/didactic/induction.ma | 169 ++++++++++++++++++ .../contribs/didactic/induction_support.ma | 25 +++ helm/software/matita/contribs/didactic/root | 1 + 6 files changed, 218 insertions(+) create mode 100644 helm/software/matita/contribs/didactic/Makefile create mode 100644 helm/software/matita/contribs/didactic/depends create mode 100644 helm/software/matita/contribs/didactic/depends.png create mode 100644 helm/software/matita/contribs/didactic/induction.ma create mode 100644 helm/software/matita/contribs/didactic/induction_support.ma create mode 100644 helm/software/matita/contribs/didactic/root diff --git a/helm/software/matita/contribs/didactic/Makefile b/helm/software/matita/contribs/didactic/Makefile new file mode 100644 index 000000000..a904aaef4 --- /dev/null +++ b/helm/software/matita/contribs/didactic/Makefile @@ -0,0 +1,21 @@ +include ../Makefile.defs + +DIR=$(shell basename $$PWD) + +$(DIR) all: + $(BIN)matitac +$(DIR).opt opt all.opt: + $(BIN)matitac.opt +clean: + $(BIN)matitaclean +clean.opt: + $(BIN)matitaclean.opt +depend: + $(BIN)matitadep -dot && rm depends.dot +depend.opt: + $(BIN)matitadep.opt -dot && rm depends.dot +exercise: + rm -rf ex/ + mkdir ex/ + cp *.ma root depends ex/ + for X in ex/*.ma; do perl -ne 'undef $$/;s/\(\*BEGIN.*?END\*\)/.../msg;print' -i $$X; done diff --git a/helm/software/matita/contribs/didactic/depends b/helm/software/matita/contribs/didactic/depends new file mode 100644 index 000000000..6234ee807 --- /dev/null +++ b/helm/software/matita/contribs/didactic/depends @@ -0,0 +1,2 @@ +induction_support.ma +induction.ma induction_support.ma diff --git a/helm/software/matita/contribs/didactic/depends.png b/helm/software/matita/contribs/didactic/depends.png new file mode 100644 index 0000000000000000000000000000000000000000..3b6104659a0445c661f5a90af70ea60f5d1330aa GIT binary patch literal 10835 zcmd6tWmHw|*Y39ng3^jeml)`#q?ObSQqn3VsemAjfOLm+x0HxTNJ>ddgMdg#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 literal 0 HcmV?d00001 diff --git a/helm/software/matita/contribs/didactic/induction.ma b/helm/software/matita/contribs/didactic/induction.ma new file mode 100644 index 000000000..4bfe88a8b --- /dev/null +++ b/helm/software/matita/contribs/didactic/induction.ma @@ -0,0 +1,169 @@ +include "induction_support.ma". + +inductive Formula : Type ≝ +| FBot: Formula +| FTop: (*BEGIN*)Formula(*END*) +| FAtom: nat → Formula +| FNot: Formula → Formula +| FAnd: (*BEGIN*)Formula → Formula → Formula(*END*) +| FOr: (*BEGIN*)Formula → Formula → Formula(*END*) +| FImpl: (*BEGIN*)Formula → Formula → Formula(*END*) +. + +let rec sem (v: nat -> nat) (F: formula) on F ≝ + match F with + [ FBot ⇒ 0 + | FTop ⇒ (*BEGIN*)1(*END*) + | FAtom n ⇒ v n + | FNot F1 ⇒ 1 - sem v F1 + | FAnd F1 F2 ⇒ min (sem v F1) (sem v F2) + (*BEGIN*) + | FOr F1 F2 ⇒ max (sem v F1) (sem v F2) + | FImpl F1 F2 ⇒ max (1 - sem v F1) (sem v F2) + (*END*) + ] +. + +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 }. + +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 }. + +interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else e t 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) + (*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*) + ]. + +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 }. + +notation > "a ≡_ term 90 v b" non associative with precedence 50 +for @{ equiv $v $a $b }. + +interpretation "equivalence for Formulas" 'equivF v a b = (equiv v 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. +assume F : Formula. +assume x : ℕ. +assume v : (ℕ → ℕ). +assume H : (F1 ≡_v F2). +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). + the thesis becomes (0 = 0). + done. +case Top. + (*BEGIN*) + the thesis becomes (FTop ≡_v FTop). + the thesis becomes (sem v FTop = sem v FTop). + the thesis becomes (1 = 1). + (*END*) + done. +case Atom. + 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). + done. + case False. + the thesis becomes (FAtom n ≡_v FAtom n). + the thesis becomes (sem v (FAtom n) = sem v (FAtom n)). + the thesis becomes (v n = v n). + 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). + 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))). + 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))). + 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*). + 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). + 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))). + 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))). + 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). + 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). + 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. + done. +(*END*) +qed. + + + diff --git a/helm/software/matita/contribs/didactic/induction_support.ma b/helm/software/matita/contribs/didactic/induction_support.ma new file mode 100644 index 000000000..b8fc7ffc8 --- /dev/null +++ b/helm/software/matita/contribs/didactic/induction_support.ma @@ -0,0 +1,25 @@ +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 diff --git a/helm/software/matita/contribs/didactic/root b/helm/software/matita/contribs/didactic/root new file mode 100644 index 000000000..8f72072f4 --- /dev/null +++ b/helm/software/matita/contribs/didactic/root @@ -0,0 +1 @@ +baseuri=cic:/matita/didactic -- 2.39.2