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

Hier wordt een klein artefact als voorbeeld uitgewerkt. In het bijzonder laat deze casus zien hoe je met een natuurkunde grootheden als snelheid en positie kunt omgaan.

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.

Focus

Het artefact is een heistelling [1]. Het gaat hier om het dynamische gedrag van een heistelling. We kijken naar het geval dat het heiblok bovenaan wordt losgelaten en door de zwaartekracht de heipaal raakt welke in de grond wordt gedreven.

Functioneel netwerk

Wie heeft zin om het bijbehorende functionele netwerk te tekenen. Het volgt zoals altijd het geval is bij functionele netwerken direct uit de definities.
Jasper Berendsen → BenB	Remove this comment when resolved!

Domeinmodel

type		betekenis (verzameling)
T		de tijd, d.w.z. de verzameling van momenten. In dit voorbeeld reële getallen, eenheid: sec.
m		afstand, eenheid: meter.
mPs		snelheid, eenheid: m/s
predikaat	type	betekenis
blok	T→m→mPs→B	blok t h v: het blok heeft op tijdstip t een afstand h t.o.v. de paal en snelheid v
inGrond	T→B	inGrond t: op tijdstip t zit de paal in de grond
gefixeerd	T→B	gefixeerd t: op tijdstip t is het blok gefixeerd
knop	T→B	knop t: op tijdstip t wordt op de knop gedrukt

Onderdelen

Besturing

Als op de knop wordt gedrukt is het blok niet gefixeerd.

<source lang="coq"> Definition BESTURING := forall t:T, knop t -> ~gefixeerd t. </source>

Zwaartekracht

Strikt genomen kan men zwaartekracht niet een onderdeel noemen. Dit artefact werkt echter niet zonder zwaartekracht en zwaartekracht is een aanname in de correctheidsstelling net als de overige onderdelen. Merkop dat Zwaartekracht het blok beïnvloedt.

Als het blok niet gefixeerd is en op hoogte h stilstaat, dan is d seconden later het blok op hoogte (h-5*d*d) met snelheid (10*d).

De formules zijn gebaseerd op een valversnelling van 10 m/s^2. De hoogte neemt dan kwadratisch af met 1/2*10*d*d.

<source lang="coq"> Definition ZWAARTEKRACHT :=

forall t:T, forall h:m, ~gefixeerd t /\ blok t h 0
 -> 
(forall d:T, d>=0 -> blok (t+d) (h-5*d*d) (10*d)).

</source>

Paal

De heipaal is hetgene wat in de grond wordt gedreven. We hebben voor onze situatie maar 1 heipaal. Bovendien modelleren we deze paal als onderdeel.

Als het blok met een snelheid van meer dan 50 m/s op een hoogte 0 of lager van de paal is verwijderd, dan zit de paal 1 seconde later de rest van de tijd in de grond.

Merkop: we gebruiken hoogte 0 of lager. Dat is handig want we hoeven dan niet te bewijzen dat het precies 0 is. Deze extra vrijheid zorgt dat we in het bewijs geen wiskundige wortels nodig hebben, iets wat met Coq erg moeilijk zal gaan. <source lang="coq"> Definition PAAL :=

forall t:T, (exists v:mPs, exists h:m, v>=50 /\ h<=0 /\ blok t h v) -> (forall u:T, u>=t+1 -> inGrond u).

</source>

Specificatie van het Geheel

Als op de knop wordt gedrukt en op dat moment het blok 7 meter boven de paal stilstaat, dan zit 10 seconden later de paal de rest van de tijd in de grond.

<source lang="coq"> Definition HEIMACHINE :=

forall t:T, knop t /\ blok t 7 0
 -> (forall u:T, u>=t+10 -> inGrond u).

</source>

Correctheidsstelling

<source lang="coq"> Theorem th1 : PAAL -> ZWAARTEKRACHT -> BESTURING -> HEIMACHINE. </source>

Bewijs

We gaan hier niet verder in op het bewijs maar geven het wel. Uit de overige stof is op te maken hoe men een dergelijk bewijs doet. Ook kun je met Coq het hieronder gegeven bewijs nog eens stap voor stap doorlopen om te zien wat er gebeurt.

Require Import BenB.

Definition T:=R.
Definition m:=R. (* hoogte in meters *)
Definition mPs:=R. (* snelheid in meters per seconde *)

Variable blok : T -> m -> mPs -> B.
Variable inGrond : T -> B.
Variable gefixeerd : T -> B.
Variable knop : T -> B.

Definition PAAL := 
 forall t:T, (exists v:mPs, exists h:m, v>=50 /\ h<=0 /\ blok t h v) -> (forall u:T, u>=t+1 -> inGrond u).

Definition ZWAARTEKRACHT := 
 forall t:T, forall h:m, ~gefixeerd t /\ blok t h 0
  -> 
 (forall d:T, d>=0 -> blok (t+d) (h-5*d*d) (10*d)).

Definition BESTURING := forall t:T, knop t -> ~gefixeerd t.

Definition HEIMACHINE := 
 forall t:T, knop t /\ blok t 7 0
  -> (forall u:T, u>=t+10 -> inGrond u).

Theorem th1 : PAAL -> ZWAARTEKRACHT -> BESTURING -> HEIMACHINE.
imp_i H1.
imp_i H2.
imp_i H3.
unfold HEIMACHINE.
all_i a.
imp_i H4.
all_i b.
imp_i H5.
unfold PAAL in H1.
imp_e (b >= a+9+1).
all_e (forall u : T, u >= a+9+1 -> inGrond u) b.
imp_e (exists v:mPs, exists h:m, v>=50 /\ h<=0 /\ blok (a+9) h v).
all_e (forall t : T,
       (exists v : mPs, exists h : m, v >= 50 /\ h <= 0 /\ blok t h v) ->
       forall u : T, u >= t + 1 -> inGrond u
) (a+9).
assumption.
clear H1.
unfold ZWAARTEKRACHT in H2.
exi_i (10 * 9).
exi_i (7 - 5 * 9 * 9).
con_i.
lin_solve.
con_i.
lin_solve.
imp_e (9>=0).
all_e (forall d : T, d >= 0 -> blok (a + d) (7 - 5 * d * d) (10 * d)) 9.
imp_e (~gefixeerd a /\ blok a 7 0).
all_e (forall h : m,
       ~ gefixeerd a /\ blok a h 0 ->
       forall d : T, d >= 0 -> blok (a + d) (h - 5 * d * d) (10 * d)
) 7.
all_e (
forall t : T, forall h : m,
       ~ gefixeerd t /\ blok t h 0 ->
       forall d : T, d >= 0 -> blok (t + d) (h - 5 * d * d) (10 * d)
) a.
assumption.
clear H2.
unfold BESTURING in H3.
con_i.
imp_e (knop a).
all_e (forall t:T, knop t -> ~gefixeerd t) a.
assumption.
clear H3.
con_e1 (blok a 7 0).
assumption.
con_e2 (knop a).
assumption.
lin_solve.
lin_solve.
Qed.