Beweren en bewijzen/het verhaal/6. Theorie/casus Stoplicht

Een aantal handige, doch niet noodzakelijke, commando's uit Coq wordt daarbij besproken. Dit voorbeeld is om je te helpen, het samenspel van notatie, definities en intervallen te begrijpen. Werk het door. Maar het is niet de bedoeling dat je in het werkstuk deze stapsgewijze opbouw volgt. In het werkstuk telt dat het zo overzichtelijk mogelijk is.

Getypeerde logica zonder definities en intervallen

Het verkeerslicht bestaat uit 4 onderdelen: 3 lampen van verschillende kleuren en een Schakelkast. We geven ze hier zonder domeinmodel. De function mod staat voor modulo.

Wie heeft zin om het domeinmodel toe te voegen?
Jasper Berendsen → BenB	Remove this comment when resolved!

Er zijn drie lampen:

Definition LampGroen := ∀t:T, Signaal t groen ↔ Licht t groen.

Definition LampOranje := ∀t:T, Signaal t oranje ↔ Licht t oranje.

Definition LampRood := ∀t:T, Signaal t rood ↔ Licht t rood.

De Schakelkast is wat complexer. In een periode van 20 seconden wordt: 5 seconden een signaal voor groen gegeven, dan 5 seconden een signaal voor oranje, en tenslotte 10 seconden een signaal voor rood. Vervolgens begint er een nieuwe periode. mod staat voor de modulo functie. (mod t 20) is dus een getal in het interval [0,20). De specificatie is:

Definition Schakelkast := ∀t:T,
  (0≤(mod t 20)∧(mod t 20)<5 ↔ Signaal t groen) ∧
  (5≤(mod t 20)∧(mod t 20)<10 ↔ Signaal t oranje) ∧
  (10≤(mod t 20)∧(mod t 20)<20 ↔ Signaal t rood).

Als specificatie voor het geheel concentreren we ons op een eenvoudige, maar belangrijke eigenschap:

¬(∃t:T. Licht t rood ∧ Licht t groen)

Dit is een wat flauwe specificatie die met veel simpelere onderdelen waar gemaakt zou kunnen worden, maar het gaat hier om het voorbeeld.

De correctheidsstelling wordt dan zonder gebruik van definities vrij lang:

LampGroen, LampOranje, LampRood, Schakelkast |- ¬(∃t:T. Licht t rood ∧ Licht t groen)

Water in de wijn

Met mod wordt het bewijs moeilijk. We kunnen mod wegwerken door de specificatie van de Schakelkast af te zwakken, door enkel nog over het tijdsinterval [0,20) te spreken. We schrijven dus in de inleiding dat we alleen dit tijdsinterval formeel beschouwen omdat de geschiedenis zich daarna precies herhaalt. De nieuwe specificatie wordt dan (ga na!):

Definition Schakelkast := ∀t:[0,20),
  (t∈[0,5) ↔ Signaal t groen) ∧
  (t∈[5,10) ↔ Signaal t oranje) ∧
  (t∈[10,20) ↔ Signaal t rood).

Om het bewijs rond te kunnen krijgen zullen we de specificatie van het geheel ook af moeten zwakken. In het Werkstuk noemden we dit: "water bij de wijn". De specificatie van het geheel zwakt af tot:

¬(∃t:[0,20). Licht t rood ∧ Licht t groen

Merk op dat het eigenlijk wel mee valt met de afzwakking, met methoden uit de wiskunde als natuurlijke inductie zouden uit datgene wat we nu bewijzen het orginele bewijs best rond kunnen krijgen.

Definities en intervallen

Omdat iedere lamp vrijwel hetzelfde is gebruiken we een geparametriseerde specificatie. Hiertoe gebruiken we een eigen type Kleur dat de kleuren {groen, oranje, rood} heeft.

Definition Lamp (k:Kleur) := ∀t:T. Signaal t k ↔ Licht t k.

Dit omdat de specificaties van de lampen zich alleen onderscheiden in kleur. De correctheidsstelling wordt nu heel compact:

Schakelkast, (forall k:Kleur, Lamp(k)) |- ¬(&exists;t:[0,20). Licht t rood ∧ Licht t groen

In Coq-notatie

De delen hieronder vormen samen het gehele bewijs in Coq. Daar waar nieuwe dingen worden gebruikt staat een toelichting. Om de toelichting te begrijpen is het uitvoeren van het bewijs in Coq onontbeerlijk.

Require Import BenB.

Definition T := R.

Variable Kleur : Set.
Variable groen : Kleur. Variable oranje : Kleur. Variable rood : Kleur.

Kleur wordt als type/verzameling gedefinieerd en groen, oranje, rood als elementen daarvan.

Variable signaal : T -> Kleur -> Prop. Variable licht : T -> Kleur -> Prop.

Definition Lamp(k : Kleur) := forall t:T, (signaal t k -> licht t k ) /\ 
(licht t k -> signaal t k).
Definition Schakelkast := forall t:T,
(t in [0, 5) -> signaal t groen) /\ (signaal t groen -> t in [0, 5)) /\
(t in [5, 10) -> signaal t oranje) /\ (signaal t oranje -> t in [5, 10)) /\
(t in [10, 20) -> signaal t rood) /\ (signaal t rood -> t in [10, 20)).

Theorem correctheidsstelling : 
Schakelkast -> (forall k:Kleur, Lamp k) ->
~exists t:T, t in [0,20) /\ licht t rood /\ licht t groen.

We schrijven in de correctheidsstelling allemaal implicaties zoals uitgelegd op Beweren_en_bewijzen/de_opzet/gereedschap/Coq#Natuurlijke deductie voor propositielogica.

Bewijzen

Het bewijs is gegeven in Gentzen notatie. Hoe men tot dit bewijs komt in Coq wordt hieronder uitgelegd.

imp_i H_Schakelkast.
imp_i K_Lampen.
neg_i (exists t : T, t in  [0, 20) /\ licht t rood /\ licht t groen) H1.
exi_e (exists t : T, t in  [0, 20) /\ licht t rood /\ licht t groen) m H2.
assumption.
clear H1.

Men mag clear gebruiken om aannames weg te gooien, het hoeft niet.

neg_i (10<=m) H3.
clear H3.
imp_e (m<5).
imp_i H4.
neg_i True H5.

True is een propositie die altijd waar is.

lin_solve.

lin_solve is in staat het doel ~True te bewijzen doordat de aannames elkaar tegenspreken, er is geen enkele oplossing mogelijk.

lin_solve.

Het doel True kan men zonder aannames bewijzen en kan ook opgelost worden m.b.v. lin_solve.

con_e2 (0<=m).
unfold Schakelkast in H_Schakelkast.

Met unfold kan men aangeven welke definitie men wil ontvouwen en in welke aanname dat moet gebeuren. unfold is geen noodzakelijk commando (het wordt in dit bewijs ter illustratie maar 1 keer gebruikt), maar kan zaken wat overzichtelijker maken.

imp_e (signaal m groen).
con_e1 (
(m in  [5, 10) -> signaal m oranje) /\ (signaal m oranje -> m in  [5, 10)) /\
(m in  [10, 20) -> signaal m rood) /\ (signaal m rood -> m in  [10, 20))
).
con_e2 (m in [0,5) -> signaal m groen). 
all_e (
forall t:T,
(t in [0, 5) -> signaal t groen) /\ (signaal t groen -> t in [0, 5)) /\
(t in [5, 10) -> signaal t oranje) /\ (signaal t oranje -> t in [5, 10)) /\
(t in [10, 20) -> signaal t rood) /\ (signaal t rood -> t in [10, 20))
) m.
assumption.
imp_e (licht m groen).
con_e2 (signaal m groen -> licht m groen).
all_e (forall t:T, (signaal t groen -> licht t groen) /\ (licht t groen -> signaal t groen)) m.
all_e (forall k:Kleur, forall t:T, (signaal t k -> licht t k) /\ (licht t k -> signaal t k)) groen.
assumption.
con_e2 (licht m rood).
con_e2 (m in [0,20)).
assumption.
clear H3.
con_e1 (m<20).
imp_e (signaal m rood).
con_e2 (m in [10,20) -> signaal m rood).
con_e2 (signaal m oranje -> m in [5,10)).
con_e2 (m in [5,10) -> signaal m oranje).
con_e2 (signaal m groen -> m in [0,5)).
con_e2 (m in [0,5) -> signaal m groen).
all_e (
forall t:T,
(t in [0, 5) -> signaal t groen) /\ (signaal t groen -> t in [0, 5)) /\
(t in [5, 10) -> signaal t oranje) /\ (signaal t oranje -> t in [5, 10)) /\
(t in [10, 20) -> signaal t rood) /\ (signaal t rood -> t in [10, 20))
) m.
assumption.
imp_e (licht m rood).
con_e2 (signaal m rood -> licht m rood).
all_e (forall t:T, (signaal t rood -> licht t rood) /\ (licht t rood -> signaal t rood)) m.
all_e (forall k:Kleur, forall t:T, (signaal t k -> licht t k) /\ (licht t k -> signaal t k)) rood.
assumption.
con_e1 (licht m groen).
con_e2 (m in [0,20)).
assumption.
assumption.

Qed.