Beweren en bewijzen/het verhaal/6. Theorie/casus Drieminutenlicht
Een drieminutenlicht moet na druk op de knop drie minuten branden, maar het mag niet ongewenst branden. Het dient tenslotte ter energiebesparing.
Inhoud
Specificaties
Een mogelijke specificatie is de volgende:
(∀t:T, Dr t → (∀t':(t,t+3], Li t')) ∧ (∀t:T, Li t → (∃t':[t-3,t), Dr t'))
met domeinmodel
| type | betekenis (verzameling) | ||
|---|---|---|---|
| T | de tijd: reële getallen, eenheid min | ||
| predikaat | type | betekenis | meting |
| Dr | T→B | Dr t: op moment t wordt op de knop gedrukt | kijken |
| Li | T→B | Li t: op moment t schijnt er licht | kijken |
Men kan dit ook korter opschrijven, maar het voor de hand liggende veranderen van de eerste implicatie in een dubbele implicatie leidt tot een verkeerde specificatie.
Veranderen van de tweede implicatie in een dubbele implicatie leidt tot:
∀t:T, Li t ↔ (∃t':[t-3,t), Dr t')
Deze specificatie is wél equivalent aan de eerste, twee keer zo lange specificatie. Dit komt omdat
∀t:T. Dr t → (∀t':(t,t+3]. Li t')
logisch equivalent is aan:
∀t:T, (∃t':[t-3,t), Dr t') → Li t
Om dit te bewijzen moeten we aantonen:
∀t:T, Dr t → (∀t':(t,t+3], Li t') |- ∀t:T, (∃t':[t-3,t), Dr t') → Li t
En:
∀t:T, (∃t':[t-3,t), Dr t') → Li t |- ∀t:T, Dr t → (∀t':(t,t+3], Li t')
Voorbeelden voor bewijzen
Dit zijn twee interessante bewijzen, omdat tijd een rol speelt en het interval als het ware omklapt van gesloten naar open en vice versa. De bewijzen zijn bovendien uitgevoerd m.b.v. Coq.
- 3-minlicht.v geeft de bewijzen.
- Gentzen-bewijs1 en Gentzen-bewijs2 geven de Gentzen-bewijs bomen.
- Fitch-bewijs1 en Fitch-bewijs2 geven de Fitch style box proofs.
Redeneren in natuurlijke taal
Als illustratie beredeneren we de eerste eigenschap in natuurlijke taal, dat wil zeggen als een lopende tekst. Hieronder doen we dat vrij uitgebreid, om de toepassingen van de deductieregels goed zichtbaar te maken. Als je het mechanisme eenmaal doorhebt, ligt het voor de hand waar je compacter kunt formuleren. We nummeren de aannamen en tussenconclusies om er gemakkelijk naar te kunnen verwijzen. Tijdens het construeren van een bewijs is een lijstje van zulke 'te gebruiken resultaten' erg handig!
Voor een redenering in natuurlijke taal is het nodig een precieze definitie van de gebruikte begrippen achter de hand te hebben. In dit geval lezen we die af in de formele specificatie hierboven.
Bijvoorbeeld: "het licht brandt even na t gedurende 3 minuten" betekent dat het licht brandt op elk tijdstip in het interval (t,t+3].
Op naar het bewijs. We schrijven op wat we moeten bewijzen, en gaan systematisch aan het werk via de logische structuur (kwantoren, voegtekens) van de uitspraken.
We nemen aan: voor elk tijdstip t: als er op t op de knop gedrukt wordt, dan brandt het licht even daarna gedurende 3 minuten (1).
We moeten bewijzen: voor elk tijdstip t: als er in de 3 minuten voorafgaand aan t op de knop gedrukt is, dan brandt het licht op t.
BEWIJS
Laat t een willekeurig tijdstip zijn.
Stel: er is in de 3 minuten voorafgaand aan t op de knop gedrukt (2). (We gaan bewijzen: het licht brandt op t.)
Gebruik (2): noem het tijdstip van knopdrukken even x. Dan: t-3 <= x (3), x < t (4) en er wordt op x op de knop gedrukt (5).
Met (1) hebben we in het bijzonder: als er op x op de knop gedrukt wordt, dan brandt het licht even daarna gedurende 3 minuten (6).
Uit (5) en (6) volgt: het licht brandt even na x gedurende 3 minuten, dat wil zeggen gedurende het interval (x,x+3] (7).
We laten zien dat t in dit interval zit, dat wil zeggen x < t en t <= x+3. Het eerste geldt volgens (4). We hebben volgens (3): t-3 <= x, dus t-3+3 <= x+3, met andere woorden: t <= x+3. Dus t zit inderdaad in het interval (x,x+3].
Dus, met behulp van (7): het licht brandt op t.
We hebben over x verder geen aannamen gemaakt, dus in elk geval: het licht brandt op t.
We concluderen: als er in de 3 minuten voorafgaand aan t op de knop gedrukt is, dan brandt het licht op t.
Het tijdstip t was willekeurig, dus dit geldt voor elke t, hetgeen we moesten bewijzen.
Correctheidsstelling
Deze casus laat zien hoe een drieminutenlicht gebouwd kan worden met twee onderdelen: een tijdschakelaar en een lamp die met een signaal uit dan wel aan gaat.
Definition DRIEMINL := (∀t:T, Dr t → (∀t':(t,t+3], Li t')) ∧ (∀t:T, Li t → (∃t':[t-3,t), Dr t')) .
Het domeinmodel is
| type | betekenis (verzameling) | ||
|---|---|---|---|
| T | de tijd: reële getallen, eenheid min | ||
| predikaat | type | betekenis | meting |
| Dr | T→B | Dr t: op moment t wordt op de knop gedrukt | kijken |
| Li | T→B | Li t: op moment t schijnt er licht | kijken |
| RL | T→B | RL t: op moment t is er een elektrisch signaal op de ResetLatch poort van de lamp | voltmeter |
Onderdeel Tijdschakelaar
Dan en slechts dan wanneer er op de knop wordt gedrukt dan komt er 3 minuten later een elektrisch signaal op de ResetLatch poort. In Coq notatie:
Definition TIJDSCHAKELAAR := forall t:T, (Dr t /\ (forall u:T, u in [t,t+3) -> ~Dr u) -> RL (t+3)) /\ (RL (t+3) -> Dr t /\ (forall u:T, u in [t,t+3) -> ~Dr u)).
Onderdeel Lamp
Het onderdeel is eigenlijk een samentrekking van twee dingen: een normale lamp die licht produceert en een SR Latch. Het drukken op de knop heeft een Set tot gevolg.
Als op een tijdstip t op de knop wordt gedrukt, dan brandt het licht d minuten later, mits er gedurende die d minuten geen signaal op de ResetLatch poort is. Bovendien als het licht schijnt op een tijdstip t, dan was er d minuten eerder op de knop gedrukt en was er gedurende die d minuten geen signaal op de ResetLatch poort en werd er ook niet op de knop gedrukt. Merk op dat dit betekent dat op tijdstip (t-d) de laatste keer voor t op de knop werd gedrukt. Merkop: door toe te voegen dat het de laatste keer was dat op de knop werd gedrukt is er iets meer informatie beschikbaar en wordt het bewijs eenvoudiger wat wel mag aangezien het al niet eenvoudig is. Kernpunt: hoe men de specificaties op stelt is van wezenlijk belang voor de moeilijkheid van het bewijs. Soms kan een ietwat andere formulering helpen terwijl het voor het onderdeel wel op hetzelfde neerkomt.
In Coq notatie:
Definition LAMP := forall t:T, (forall d:D, d>0 -> Dr t /\ (forall u:T, u in (t,t+d] -> ~RL u) -> Li (t+d)) /\ (Li t -> exists d:D, d>0 /\ Dr (t-d) /\ forall u:T, u in [t-d,t) -> ~RL u /\ ~Dr u).
Bewijs
De correctheidsstelling is simpelweg TIJDSCHAKELAAR, LAMP |= DRIEMINL. Het volledige bewijs is te vinden op [1]. Het volledige Coq script is te vinden op [2]. Om dit verhaal te kunnen volgen moet het Coq-script uitgevoerd worden. Het bewijs in Coq heeft een extra aanname nodig die verder voor de hand ligt. We doen dat in de vorm van een hypothese en wel als volgt:
Hypothesis hypo1 : forall d:D, ~ d <= 3 -> d > 3.
Kernpunt: als je iets triviaals niet kunt bewijzen met Coq, neem het dan op als hypothese.
We zullen nu het bewijs bespreken aan de hand van het Coq script. Onder ieder stukje script staat uitleg wat er gebeurt. Bekende dingen als toewerken naar aannames worden niet uitgelegd.
imp_i H1. imp_i H2. unfold DRIEMINL. con_i.
Eerste deel
We gaan nu eerst bewijzen dat het licht wel zal schijnen. Later komt het andere deel: dat het licht niet zomaar schijnt.
all_i a. imp_i H3. all_i b. imp_i H4. unfold LAMP in H2. replace b with (a+(b-a)).
We willen de conclusie bewijzen m.b.v. LAMP vandaar dat we de definitie uitvouwen om hem te kunnen bekijken. We vervangen b door (a+(b-a)), omdat we zo naar de vorm die LAMP heeft kunnen toewerken, in het achterhoofd houdende dat we Dr a hebben in onze aannames.
imp_e (Dr a /\ (forall u:T, u in (a,a+(b-a)] -> ~RL u)). imp_e (b-a>0). all_e (forall d:D, d>0 -> Dr a /\ (forall u:T,u in (a,a+d] -> ~RL u) -> Li (a+d)) (b-a). con_e1 (Li a -> (exists d:D, d>0 /\ Dr (a-d) /\ (forall u:T, u in [a-d,a) -> ~RL u /\ ~Dr u))). all_e (forall t:T, (forall d:D, d>0 -> Dr t /\ (forall u:T, u in (t,t+d] -> ~RL u) -> Li (t+d)) /\ (Li t -> exists d:D, d>0 /\ Dr (t-d) /\ forall u:T, u in [t-d,t) -> ~RL u /\ ~Dr u) ) a. assumption.
Naar aanname toewerken.
imp_e (a<b). imp_i H5. lin_solve.
Uit (a<b) kunnen we met wat rekenen uiteraard de conclusie trekken, en (a<b) staat in een conjunctie in de aannames, namelijk in b in (a, a + 3], want dat is niets anders dan een conjunctie.
con_e1 (b<=a+3). assumption. clear H2.
Maak het rechterdeel van de conjunctie compleet. Ruim een nutteloze aanname op.
con_i. assumption.
Dat was makkelijk, maar daarom hadden we ook (a+(b-a)) gekozen.
unfold TIJDSCHAKELAAR in H1. all_i c. imp_i H5. neg_i (Dr a) H6.
Uit aanname H1 zien we dat als RL (t+3) geldt er tussen t en t+3 niet op de knop gedrukt was. Dus als we voor t invulllen c-3 dan wordt tussen c-3 en c niet op de knop gedrukt Uit de ongelijkheden valt af te leiden dat dan ondermeer niet op a op de knop wordt gedrukt. Tegenspraak met Dr a!
imp_e (a in [c-3,c-3+3)). all_e (forall t':T, t' in [c-3,c-3+3) -> ~Dr t') a. con_e2 (Dr (c-3)). imp_e (RL (c-3+3)). con_e2 (Dr (c-3) /\ (forall t':T, t' in [c-3,c-3+3) -> ~Dr t') -> RL (c-3+3)). all_e (forall t:T, (Dr t /\ (forall t':T, t' in [t,t+3) -> ~Dr t') -> RL (t+3)) /\ (RL (t+3) -> Dr t /\ (forall t':T, t' in [t,t+3) -> ~Dr t'))) (c-3). assumption.
Naar aaname toewerken.
replace (c-3+3) with c. assumption. lin_solve.
Wat simpel rekenwerk.
interval. con_i.
Dit is standaard: om een interval te bewijzen moet je een conjunctie bewijzen.
imp_e (c <= a+3). imp_i H7. lin_solve.
Vervang de conclusie c-3 <= a met c <= a+3.
imp_e (b<=a+3). imp_i H8. lin_solve. con_e2 (a<b). assumption. replace b with (a+(b-a)). con_e2 (a<c). assumption. lin_solve. imp_e (a<c). imp_i H7. lin_solve. con_e1 (c<=a+(b-a)). assumption. assumption. lin_solve.
c<=b en b<=a+3 staan in de aannames als intervallen. Uit deze twee formules volgt uiteraard de conclusie c<=a+3.
Tweede deel
Het tweede deel bewijst dat het licht niet zomaar schijnt. Het is een stuk moeilijker.
all_i a. imp_i H3. unfold LAMP in H2. exi_e (exists d:D, d>0 /\ Dr (a-d) /\ forall u:T, u in [a-d,a) -> ~RL u /\ ~Dr u) e H4.
Uit Li a en de formule voor de lamp kunnen we eenvoudig het volgende concluderen:
(exists d:D, d>0 /\ Dr (a-d) /\ forall u:T, u in [a-d,a) -> ~RL u /\ ~Dr u) e H4.
Hierop doen we een existentie eliminatie.
imp_e (Li a). con_e2 (forall d:D, d>0 -> Dr a /\ (forall u:T, u in (a,a+d] -> ~RL u) -> Li (a+d)). all_e ( forall t:T, (forall d:D, d>0 -> Dr t /\ (forall u:T, u in (t,t+d] -> ~RL u) -> Li (t+d)) /\ (Li t -> exists d:D, d>0 /\ Dr (t-d) /\ forall u:T, u in [t-d,t) -> ~RL u /\ ~Dr u) ) a. assumption. assumption.
Werk naar de twee aannames toe.
exi_i (a-e).
Het licht brandt op tijdstip a. De variabele e representeert hoe lang het geleden is dat voor het laatst op de knop werd gedrukt. We zullen bewijzen dat er hooguit 3 minuten geleden op de knop werd gedrukt.
con_i. interval. con_i. imp_e (e<=3). imp_i H5. lin_solve.
Eenvoudig rekenwerk.
neg_e' (RL (a-e+3)) H5.
Bewijs uit het ongerijmde! Door aan te nemen dat ~(a<=3), wat door de hypothese overeenkomt met a>3, zullen we bewijzen ~RL (a-e+3), terwijl uit aanname H4 eenvoudig valt te bewijzen dat dit juist wel het geval is.
con_e1 (~Dr (a-e+3)). imp_e ((a-e+3) in [a-e,a)). all_e (forall u:T, u in [a-e,a) -> ~RL u /\ ~Dr u) (a-e+3). con_e2 (Dr (a-e)). con_e2 (e>0). assumption. interval. con_i. lin_solve. imp_e (e>3). imp_i H6. lin_solve. imp_e (~e<=3). all_e (forall d:D, ~d<=3 -> d>3) e. exact hypo1. assumption.
Dit bewijst ~RL (a-e+3).
clear H2. unfold TIJDSCHAKELAAR in H1. imp_e (Dr (a-e) /\ (forall u:T, u in [a-e,a-e+3) -> ~Dr u)). con_e1 (RL (a-e+3) -> Dr (a-e) /\ (forall u:T, u in [a-e,a-e+3) -> ~Dr u)). all_e (forall t:T, (Dr t /\ (forall u:T, u in [t,t+3) -> ~Dr u) -> RL (t+3)) /\ (RL (t+3) -> Dr t /\ (forall u:T, u in [t,t+3) -> ~Dr u)) ) (a-e). assumption. con_i. con_e1 (forall u:T, u in [a-e, a) -> ~RL u /\ ~Dr u). con_e2 (e>0). assumption. all_i b. imp_i H6. con_e2 (~RL b). imp_e (b in [a-e,a)). all_e (forall u:T, u in [a-e,a) -> ~RL u /\ ~Dr u) b. con_e2 (Dr (a-e)). con_e2 (e>0). assumption. interval. con_i. con_e1 (b<a-e+3). assumption. imp_e (b<a-e+3). imp_i H7. imp_e (e>3). imp_i H8. lin_solve. imp_e (~e<=3). all_e (forall d:D, ~d<=3 -> d>3) e. exact hypo1. assumption. con_e2 (a-e<=b). assumption. imp_e (e>0). imp_i H5. lin_solve. con_e1 (Dr (a-e) /\ (forall u:T, u in [a-e,a) -> ~RL u /\ ~Dr u)). assumption. con_e1 (forall u:T, u in [a-e,a) -> ~RL u /\ ~Dr u). con_e2 (e>0). assumption. Qed.
