4.8 場合分け

次に場合に分けて証明するときの話をします．証明したいのは A and B という命題で，この命題は場合分けすれば証明できるとします．例えば x=1 の場合と，x=2 の場合と， x がその他の値を取る場合とに分けて証明したいとします. x=1,2 で特異点になっているということです．このときには次のような証明の構造をとります．



  L:( x=1 or x=2 or not ( x=1 & x=2 ))



   now per cases by L;



    suppose LA:x=1;



     ......



    thus A and B;


    


    suppose LB:x=2;



     ......



    thus A and B;


    


    suppose LC:not (x=1 & x=2);



     ......



    thus A and B;



   end;

now per cases 〜 end の中で，それぞれの場合について suppose して証明します. suppose x=1 から最初の thus A and B までで x=1 のときの証明をします．同様に，x=2 の時，その他の場合についても証明します. now から end までの文は全体で1つの A and B とみなします．例えば now 〜 end の後に then とすれば，then は now 〜 end 全体を受けるわけです. suppose でそれぞれの場合に分けられていますが，それぞれの場合の帰結の部分を最後に渡すわけです．ですから，これ全体を引用したときには suppose に分かれたということは忘れてしまって，結論だけが全部同じということがチェックされるわけです．だからこれは1つの式だということです．

4.8.1 場合分けの前提

ここで注意があります．この場合は， x=1 or x=2 or not (x=1 & x=2) という式を場合分けするときに前提として使っています．この場合分けがすべての場合を覆っているということをいっているわけです．このように場合分けするときは，すべての場合についていっていることを言わなければなりません．

4.8.2 場合分けでのラベル

当然ながら場合分けをして証明するときには，それぞれの場合の証明でのラベルは，その場合の証明の中でのみ有効です．もし，その場合の証明以外でその証明のラベルを使おうとすると，ラベルがないというエラーとなります．

4.8.3 ラベルについての注意

それから，ここでラベルの注意をしておきます．Mizarでは，同じラベルを使ってもかまいませんが，直前のものが優先されます．

例えば，



　L1:......;



  　 ......



  L1:......;



     ...... by L1;　ここでは直前のL1が引用される

この例で何か証明したときに by L1 とすると，下の L1 の文が引用されます．

このことは間違いやすく L1,L2,L3,...... とラベルをつけていって，とどこまでラベルを使ったのかを忘れてしまい，また L3 とつけたとします．そして， by L3 とすると，自分では前の \verb| L3| のつもりで必ず \verb| L3| から推論できると思っても，いくらやってもエラーがでてきてしまうわけです．このようなことを最初のうちによくやります．このときはよく捜すと，同じラベルが１つ隠れているのです．もうひとつ別のところにあることがあります．これがラベルについての注意です．