Beweren en bewijzen/de zuilen/Zekerheid/8. Hulpstellingen
| literatuur
... |
De correctheidsstelling van een serieus artefact (zeg maar op werkstukniveau) zal vaak behoorlijk ingewikkeld zijn. Daar waar een bewijs met papier en pen dan al snel ondoenlijk is, heeft Coq geen enkel probleem met het correct bijhouden van alle aannames en openstaande (sub)goals. Echter, naast de standaard afleidingsregels voor de natuurlijke deductie heeft Coq ook nog een ander mechanisme dat kan helpen bij het maken van grote bewijzen. Coq kan namelijk hulpstellingen gebruiken. Dit zijn lemma's die je eerst als een aparte simpele stelling bewijst en die je daarna simpelweg kunt toepassen in het grote bewijs. Dit kan bijvoorbeeld handig zijn als je ziet dat een bepaald deel van het bewijs in een grote stelling telkens op hetzelfde neer komt. In plaats van telkens alle stappen uit te schrijven, kun je een lemma bewijzen dat precies die gemeenschappelijke goal oplevert en dat lemma vervolgens een paar keer gebruiken. Ook kun je zo'n lemma gebruiken als je weet dat P(x) geldt voor alle x in (a, a+d) en je moet bewijzen dat P(y) geldt voor alle y in (a,a+d-1) en P(z) voor alle z in (a,a+d-2). Je zou dan in een lemma kunnen bewijzen dat P(s) geldt voor alle s in (a,a+e) voor alle e in (0,d) en dat lemma telkens met een andere e toepassen.
Voorbeeld in propositielogica
Bij een tentamen is ooit gevraagd om een simpele AHOB spoorwegovergang te modelleren. Het idee was dat de correctheidsstelling aangaf dat als er een trein op het kritieke traject aanwezig is, dat er een bel rinkelt, er rode lampen knipperen en er een slagboom dicht is. Hier het domeinmodel:
| propositie | betekenis | meting |
|---|---|---|
| T | Er bevindt zich een trein op het kritieke traject. | Kijken naar het kritieke traject. |
| SC | Er staat spanning op de ingang van de besturingskast . | Kijken of een voltmeter op die ingang een spanning detecteert. |
| SB | Er staat spanning op het aansluitpunt van de bel. | Kijken of een voltmeter op dat aansluitpunt een spanning detecteert. |
| SL | Er staat spanning op het aansluitpunt van de lichtunit. | Kijken of een voltmeter op dat aansluitpunt een spanning detecteert. |
| SS | Er staat spanning op het aansluitpunt van de slagboom. | Kijken of een voltmeter op dat aansluitpunt een spanning detecteert. |
| B | De bel rinkelt. | Luisteren. |
| R | De rode lampen in de lichtunit knipperen. | Kijken naar de lichtunit. |
| D | De slagboom is dicht. | Voelen of je wordt tegengehouden als je probeert de overgang te passeren. |
In Coq kan dit alsvolgt worden ingevoerd:
Require Import "BenB". Variable T SC SB SL SS B R D: Prop. Definition railsensor := T->SC. Definition besturingskast := SC -> SB /\ SL /\ SS. Definition bel := SB -> B. Definition slagboom := SS -> D. Definition lichtunit := SL -> R.
En de bijbehorende correctheidsstelling is:
Theorem ahob : railsensor -> besturingskast -> bel -> slagboom -> lichtunit -> T -> B /\ R /\ D.
We geven hier niet de commando's die je kunt gebruiken om deze stelling te bewijzen, maar alleen het uiteindelijke bewijs in Fitch notatie: zie Bestand:Ahob.pdf. (Aangezien het niet gelukt is om de uitvoer van Coq met de essentiële blokken erin te kopiëren is het bewijs hier alleen als .pdf beschikbaar.)
Als je goed kijkt, zie je dat hier drie keer dezelfde subgoal SB /\ SL /\ SS uit dezelfde aannames is bewezen (regel 12, 20 en 29). Het bewijs is dan ook drie keer precies hetzelfde. Dit kan dus mooi aangepakt worden met een lemma.
Theorem lemma1 : railsensor -> besturingskast -> T -> SB /\ SL /\ SS.
In feite maak je hier een correctheidssteling van een subsysteem: als er een trein op het kritieke traject aanwezig is, dan staat er spanning op de aansluitpunten van de bel, de lichtunit en de slagboom. Het bewijs is triviaal. Na afloop zal Coq zeggen:
lemma1 is defined
Als we nu de ahob-stelling gaan bewijzen, mogen we gebruik maken van deze bewezen hulpstelling. Als de hulpstelling nog niet bewezen is, geeft Coq een foutmelding op het moment dat je hem probeert toe te passen!
Eerst wat triviale stappen om de aannames mooi als losse aannames te krijgen.
Proof. imp_i rs. imp_i bk. imp_i bl. imp_i sb. imp_i lu. imp_i tr.
Nu de splitsing van de conjunctie.
con_i.
Om B te kunnen bewijzen, willen we lemma1 gaan gebruiken en dus moeten we zorgen dat we daarvoor de juiste subgoal SB /\ SL /\ SS krijgen.
imp_e SB. assumption. con_e1 (SL /\ SS).
Nu passen we lemma1 toe.
apply lemma1.
Dit levert precies de drie aannames uit lemma1 als bewijsverplichting op. Gelukkig zijn dat ook allemaal aannames binnen de ahob-stelling en zijn ze dus triviaal te bewijzen.
assumption. assumption. assumption.
De andere twee subgoals R en D gaan op precies dezelfde manier.
con_i. imp_e SL. assumption. con_e1 SS. con_e2 SB. apply lemma1. assumption. assumption. assumption. imp_e SS. assumption. con_e2 SL. con_e2 SB. apply lemma1. assumption. assumption. assumption. Qed.
In dit specifieke voorbeeld is de uiteindelijke winst maar klein, maar dat is natuurlijk een direct gevolg van het feit dat lemma1 zo eenvoudig te bewijzen was. Als hier iets ingewikkelders had gestaan of als lemma1 zes keer in plaats van drie keer toegepast had moeten worden is de winst natuurlijk veel groter.
In Fitch notatie wordt door Coq netjes opgeschreven welk lemma op welke plaats is toegepast: zie Bestand:Ahob-lemma.pdf
Voorbeeld in predikaatlogica
We gaan een voorbeeld behandelen dat nog iets anders is dan het in de inleiding genoemde geval. Merk op dat het geen zin heeft om dit bewijs hier simpelweg te lezen: voer het zelf uit in Coq en zie wat er gebeurt. Dit is de stelling die we willen bewijzen:
Definition T:= R. Variable P : T -> B. Theorem beperkenmag: forall a:T, (forall x:T, x in [a+3, a+37] -> P x) -> ((forall y:T, y in [a+7, a+7] -> P y) /\ (forall z:T, z in (a+9, a+12)-> P z)).
Deze stelling zegt dat als we weten dat P x waar is voor alle x in het gesloten interval [a+3, a+37], dan weten we ook dat P y waar is voor alle x in het gesloten interval [a+7,a+7] (wat natuurlijk eigenlijk niets anders is dan zeggen dat P (a+7) geldt) en dat P z waar is voor alle z in het open interval (a+9, a+12).
We gaan dit bewijzen met behulp van het volgende lemma:
Theorem lemma2: forall a:T, forall b:T, forall c:T, (b <= c /\ (forall x:T, x in [a+b, a+c] -> P x)) -> forall d:T, forall e:T, (b <= d/\ e <=c /\ d<=e -> (forall x:T, x in [a+d, a+e] -> P x)).
Overtuig jezelf dat dit lemma aangeeft dat als je weet dat P x geldt voor een bepaald gesloten interval [a+b,a+c], dan weet je ook dat P x geldt voor elk gesloten deelinterval [a+d,a+e] van [a+b,a+c]. In het bijzonder doen we hier dus geen uitspraken over open intervallen.
Nu eerst het bewijs van het lemma. Dit bewijs gaat redelijk vanzelf. Eerst doen we zoals gebruikelijk een aantal voor-alle-introducties en implicatie-introducties om een zo simpel mogelijke goal te krijgen.
Proof. all_i a1. all_i b1. all_i c1. imp_i h1. all_i d1. all_i e1. imp_i h2. all_i x1. imp_i h3.
Nu is het zaak om te zorgen dat onze goal gaat lijken op onze aanname h1 door een implicatie-eliminatie, een voor-alle-eliminatie en een conjunctie-eliminatie te doen.
imp_e (x1 in [a1 + b1, a1 + c1]). all_e (forall x : T, x in [a1 + b1, a1 + c1] -> P x) x1. con_e2 (b1 <= c1). assumption.
De goal die we nu moeten bewijzen volgt uit h2 en h3. Helaas snapt Coq dat niet meteen. Voordat we lin_solve kunnen gebruiken om elementaire vergelijkingen te kunnen oplossen, moeten we die zoveel mogelijk splitsen in kleine delen. Daartoe schrijven we eerst de intervalnotatie uit en splitsen vervolgens de conjunctie.
interval. con_i.
Nu gaan we een truc toepassen die je vaker kunt gebruiken. We gaan een impliciet gevolg van de aanname h3, namelijk dat a1+d1 <=x, expliciet als aanname genereren door eerst een implicatie-eliminatie te doen en dan een implicatie-introductie. (Daar waar je normaal gesproken eerst vooral implicatie-introducties doet.)
imp_e (a1+d1 <= x1). imp_i h4.
Dezelfde truc gebruiken we nu om de b1 <= d1 uit h2 expliciet te krijgen.
imp_e (b1 <= d1). imp_i h5.
Op dit moment hebben we nog steeds dezelfde subgoal a1+b1<=x als een aantal stappen geleden, maar doordat enkele aannames nu expliciet zijn opgeschreven kan Coq dit nu wel zelf bewijzen:
lin_solve.
De extra aannames die we hadden gegenereerd kunnen eenvoudig uit h2 en h3 worden bewezen.
con_e1 (e1<= c1 /\ d1<= e1). assumption. con_e1 (x1 <= a1+ e1). assumption.
Vervolgens kunnen we dezelfde strategie ook gebruiken voor de rechterkant van het interval.
imp_e (x1 <= a1 + e1). imp_i h6. imp_e (e1 <= c1). imp_i h7. lin_solve. con_e1 (d1 <= e1). con_e2 (b1 <= d1). assumption. con_e2 (a1+d1<=x1). assumption. Qed.
En het verlossende lemma2 is defined verschijnt.
Nu kunnen we de stelling zelf gaan bewijzen.
Proof. all_i a1. imp_i h1. con_i.
Op dit moment hebben we een goal die al sterk lijkt op de conclusie van lemma2, maar het is nog niet precies goed: we moeten eerst nog een aantal beweringen toevoegen via een implicatie-eliminatie. Vervolgens kunnen we lemma2 toepassen. Merk op dat Coq zelf precies ziet wat de a, b, c, d en e uit de formulering van lemma2 zijn. Hier respectievelijk a1, 3, 37, 7 en 7.
imp_e (3 <= 7 /\ 7 <= 37 /\ 7 <= 7). apply lemma2.
Vervolgens krijgen we een aantal triviale goals te bewijzen.
con_i. lin_solve. assumption. con_i. lin_solve. con_i. lin_solve. lin_solve.
Op dit moment hebben we de bewering over het gesloten interval [a+7,a+7] dus bewezen. Nu nog de bewering over het open interval. Dat vergt iets meer werk omdat we lemma2 alleen maar kunnen toepassen voor beweringen over gesloten intervallen. We gaan nu dan ook eerst de sterkere eis over het gesloten interval [a+9,a+12] bewijzen en vervolgens laten zien dat uit z in (a+9,a+12) direct volgt dat ook z in [a+9,a+12]. Die sterkere eis volgt weer uit ons lemma2. Vervolgens moeten we nog een paar triviale lin_solve's doen om aan alle bewijsverplichtingen te voldoen.
all_i z1. imp_i h2. imp_e (z1 in [a1+9, a1+12]). all_e (forall z:T, z in [a1+9,a1+12]-> P z) z1. imp_e (3 <=9 /\ 12 <=37 /\ 9 <= 12). apply lemma2. con_i. lin_solve. assumption. con_i. lin_solve. con_i. lin_solve. lin_solve.
Nu komen we op het punt waar we moeten laten zien dat voor alle z in (a+9,a+12) ook geldt z in [a+9,a+12]. (Natuurlijk hadden we daar ook weer een algemeen lemma voor kunnen bewijzen, maar we doen het hier nu gewoon in dit grotere bewijs.) De truc is om de juiste implicatie-eliminaties toe te passen en vervolgens lin_solve het triviale werk op te laten knappen.
interval. con_i. imp_e (a1+9 < z1). imp_i h3. lin_solve. con_e1 (z1 < a1 + 12). assumption. imp_e ( z1 < a1 + 12). imp_i h4. lin_solve. con_e2 (a1 +9 < z1). assumption. Qed.
Hier het bewijs in Fitch notatie: Bestand:Interval-lemma.pdf
