(* August 19, 1997 (after general overhaul) *) script "logic_tools"; script "tableau2"; script "algebra2"; (* induction proofs on even and odd numbers *) (* a proof partially set up by Holmes, mostly by Michael Parvin, with guidance *) (* EVENODD: forall @ [(even @ ?1) | odd @ ?1] = true ["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CONVIF","EQBOOL","EQUATION","FNDIST","FORSOMEDIST2","IF","IFF","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","SYM","TYPES","XOR","even","forall","forsome","odd"] *) initializecounter(); s "forall@[(even@?1)|odd@?1]"; right();right();left(); ri "even"; ex(); up(); right(); ri "odd"; ex(); top(); right();right(); ri "BIND@Nat:?1"; ex(); top(); ri "INDUCTION"; ex(); left(); ri "EVAL"; ex(); (* we are now looking at a disjunction whose left term is true *) left(); rri "DINSTANTIATE"; ex(); left(); assign "?x_4" "0";ri "EVAL"; ex(); ri "RIGHT@PLUSCOMP"; ex(); ri "REFLEX"; ex(); up(); ri "ALTORDEF"; ex(); ri "LEFT@REFLEX"; ex(); up(); ri "ALTORDEF"; ex(); ri "LEFT@REFLEX"; ex(); up(); ri "RL@EVAL"; ex(); ri "AND"; ex(); ri "LEFT@REFLEX"; ex(); rri "BOOLDEF"; ex(); rri "FORALLBOOL"; ex(); right();right(); ri "RL@EVAL";ex(); rri "3pt78";ex(); left(); rri "FORALL_IMP_FORSOME_EQ";ex(); right();right(); ri "IMPTOCOND";ex(); right();left(); ri "RIGHT@PLUSTYPE2";ex(); ri "SAMESUCC";ex(); ri "RIGHT@RIGHT@ \$PLUSTYPE2";ex(); up();right();left();right(); ri "DINSTANTIATEF1 @ ?2";ex(); left(); ri "EVAL"; ex(); ri "EQUATION"; ex(); ri "1|-|1"; ex(); up(); ri "ALTORDEF"; ex(); ri "LEFT@REFLEX"; ex(); up(); ri "DSYM";ex(); ri "ALTORDEF"; ex(); ri "LEFT@REFLEX"; ex(); up();up(); rri "CASEINTRO"; ex(); up(); ri "AT"; ex(); up();up(); ri "FORALLDROP**AT"; ex(); up(); ri "AND"; ex(); ri "LEFT@REFLEX"; ex(); rri "BOOLDEF"; ex(); ri "RIGHT@ \$FORALL_IMP_FORSOME_EQ";ex(); rri "FORALLBOOL"; ex(); right();right();left(); ri "RIGHT@(LEFT@ONENAT)**(RIGHT@PLUSTYPE2)**PLUSTYPE2";ex(); ri "SAMESUCC"; ex(); ri "RIGHT@RIGHT@(\$PLUSTYPE2)**(RIGHT@ \$PLUSTYPE2)**LEFT@ \$ONENAT";ex(); ri "RIGHT@(RIGHT@(\$PLUSASSOC)**PLUSCOMM)** \$PLUSASSOC"; ex(); up(); ri "IMPTOCOND";ex(); right();right();left();left(); ri "DINSTANTIATEF1 @ 1 + Nat: ?2";ex(); left(); ri "EVAL"; ex(); ri "EVERYWHERE@ONENAT"; ex(); ri "RIGHT@RL@ \$PLUSTYPE2"; ex(); ri "EVERYWHERE@ \$ONENAT"; ex(); ri "EQUATION"; ex(); ri "1|-|1"; ex(); up(); ri "ALTORDEF"; ex(); ri "LEFT@REFLEX"; ex(); up(); ri "ALTORDEF"; ex(); ri "LEFT@REFLEX"; ex(); up();up(); rri "CASEINTRO"; ex(); up(); ri "AT"; ex(); up();up(); ri "FORALLDROP**AT"; ex(); up();up(); ri "FORALLDROP**AT"; ex(); prove "EVENODD"; (* the full-strength theorem *) (* PARITY: forall @ [(forsome @ [(Nat : ?1) = (Nat : ?2) + Nat : ?2]) =/= forsome @ [(Nat : ?1) = (Nat : ?2) + (Nat : ?2) + 1]] = true ["AND","ASSERT","BOOLDEF","BUILTIN","CASEINTRO","CHOICE","CONVIF","EQBOOL","EQUATION","FNDIST","FORSOMEDIST2","IF","IFF","IGNOREFIRST","INDUCTION","NONTRIV","NOT","ODDCHOICE","OR","PLUSASSOC","PLUSCOMM","PLUSCOMP","PLUSID","PLUSTYPE","PLUSTYPE2","REFLEX","SAMESUCC","SUCCNOTZERO","SYM","TYPES","XOR","forall","forsome"] *) (* a tool *) initializecounter(); s "forall@[ (forsome@[(Nat:?1)=(Nat:?2)+Nat:?2]) =/= forsome@[(Nat:?1)=(Nat:?2)+(Nat:?2)+1]]"; ri "INDUCT_TAC"; ex(); left(); left(); ri "DINSTANTIATEF1@0"; ex(); left(); ri "EVAL"; ex(); ri "EVERYWHERE@ \$ZERONAT"; ex(); ri "(RIGHT@PLUSID**REALNUMERAL2)**REFLEX"; ex(); up(); ri "DSYM**DZER"; ex(); up();right(); right();right(); ri "(RIGHT@(GETPLUS@1)**RIGHT@PLUSTYPE2)**SUCCNOTZERO"; ex(); up();up(); ri "forsome**RIGHT@FORALLDROP**AF"; ex(); ri "NRULE2**DUBNEG2**AF";ex(); up(); ri "TAB_XOR"; ex(); up();right(); right();right(); ri "LEFT@XALTDEF"; ex(); rri "3pt78"; ex(); left(); rri "3pt65"; ex(); ri "IMPTOCOND"; ex(); right(); ri "TAB_NOT_2"; ex(); right();right(); rri "FORALL_IMP_FORSOME_EQ"; ex(); right();right(); ri "IMPTOCOND"; ex(); right();right();left(); right();right();right(); ri "(RIGHT@(GETPLUS@1)**RIGHT@PLUSTYPE2)** \$SAMESUCC"; ex(); ri "RIGHT@ \$PLUSTYPE2"; ex(); up();up(); ri "forsomecase**1|-|1";ex(); up();left(); ri "DINSTANTIATEF1@1+Nat:?2"; ex(); left(); ri "EVAL"; ex(); right(); ri "(EVERYWHERE@ONENAT)**EVERYWHERE@ \$PLUSTYPE2"; ex(); ri "GETPLUS@Nat:1"; ex(); right(); ri "GETPLUS@Nat:1";ex(); ri "PLUSCOMM**PLUSASSOC"; ex(); up(); ri "(LEFT@ \$BUILTIN)**RIGHT@EVERYWHERE@PLUSTYPE2"; ex(); up(); rri "SAMESUCC"; ex(); right(); ri "(\$PLUSTYPE2)** RIGHT@ \$PLUSTYPE2"; ex(); ri "EVERYWHERE@ \$ONENAT"; ex(); up(); ri "EQUATION**1|-|2"; ex(); up(); ri "TAB_OR"; ex(); up(); ri "TAB_XOR"; ex(); up();up();up(); ri "(EVERYWHERE@ \$CASEINTRO)**AT"; ex(); up();up(); ri "FORALLDROP**AT"; ex(); up();up(); rri "CASEINTRO"; ex(); up(); ri "AT"; ex(); up();right(); rri "3pt65"; ex(); rri "FORALL_IMP_FORSOME_EQ"; ex(); right();right(); ri "IMPTOCOND"; ex(); right();right();left(); ri "IMPTOCOND"; ex(); right(); ri "TAB_NOT_2"; ex(); right();right(); right(); ri "DINSTANTIATEF1@?2"; ex(); left(); ri "EVAL"; ex(); ri "RIGHT@GETPLUS@1"; ex(); ri "RIGHT@RIGHT@PLUSTYPE2"; ex(); rri "SAMESUCC"; ex(); ri "RIGHT@ \$PLUSTYPE2"; ex(); ri "EQUATION**1|-|1"; ex(); up(); ri "TAB_OR"; ex(); up();up();up(); right();right();left(); right();right(); ri "PCASEINTRO@(0=Nat:?3)|forsome@[(Nat:?3)=1+Nat:?4]";ex(); ri "TAB_OR_2"; ex(); right();left(); ri "EQSYMM"; ex(); ri "LEFT@(RL@ \$0|-|3)**PLUSID**REALNUMERAL2"; ex(); ri "SUCCNOTZERO"; ex(); up();right(); ri "LEFT@CHOICE_TAC";ex(); ri "BIND@ !!![(Nat : ?3) = 1 + Nat : ?4]";ex(); (* suppress the complex name of the witness *) left();right(); right();left(); ri "RIGHT@RL@0|-|4"; ex(); right(); ri "PLUSASSOC**RIGHT@GETPLUS@1"; ex(); ri "RIGHT@(LEFT@TYPENUMERAL)**(RIGHT@PLUSTYPE2)**PLUSTYPE2"; ex(); up(); rri "SAMESUCC"; ex(); ri "RIGHT@(\$PLUSTYPE2)**RIGHT@ \$PLUSTYPE2"; ex(); ri "EQUATION"; ex(); right();left(); rri "(2|-|2)@false"; ex(); left(); ri "DINSTANTIATEF1@?4"; ex(); ri "LEFT@EVAL"; ex(); ri "LEFT@RIGHT@(GETPLUS@1)**LEFT@ONENAT"; ex(); ri "(LEFT@EQUATION**1|-|5)**TAB_OR"; ex(); up();ex(); up();up(); rri "CASEINTRO"; ex(); up();up();up();up(); ri "EVAL"; ex(); ri "LEFT@ (BIND@ !!![(Nat : ?3) = 1 + Nat : ?4])** \$CHOICE"; ex(); up();up(); rri "TAB_OR_2"; ex(); ri "LEFT@9pt16a@?3,ZEROORSUCC"; ex(); (* it has its uses! *) up();up(); ri "FORSOMEDROP**AF"; ex(); up(); ri "TAB_XOR"; ex(); upto "[?P@?1]"; right(); ri "EVERYWHERE@ \$CASEINTRO"; ex(); ri "EVERYWHERE@AT"; ex(); ri "EVERYWHERE@ \$CASEINTRO"; ex(); ri "AT"; ex(); up();up(); ri "FORALLDROP**AT"; ex(); up(); ri "TAB_AND"; ex(); up();up(); ri "FORALLDROP**AT"; ex(); up(); ri "TAB_AND"; ex(); p "PARITY"; quit();