Beweren en bewijzen/supplement/assistentie/taak 09

Hier wat informatie over Leertaak 9.

Opgave 1

• Bij deze opgave moeten er verschillende aannames gemaakt worden in verband met het beperkte domeinmodel.
• Zo is er bijvoorbeeld geen predikaat voor scheiden. Bij isWeduwe is het feitelijk natuurlijk niet genoeg als de partner waarmee een vrouw ooit getrouwd is inmiddels is overleden. Als ze namelijk al weer gescheiden zijn, is ze vast geen weduwe.
• Ook over tweelingen kunnen veel keuzes gemaakt worden. Volgens Van Dale is het van belang dat ze tegelijk geboren zijn uit dezelfde moeder, maar er zijn ook definities die kijken naar het moment van bevruchten. Maar daar kunnen we natuurlijk niets mee met dit domeinmodel.
• Verder kunnen veel hulppredikaten extra ingewikkeld gemaakt worden door bijvoorbeeld voor momenten waarop er getrouwd wordt ook expliciet te eisen dat die mensen leven. Dat is niet fout, maar ik denk dat er weinig mogelijkheden zijn om te trouwen als beide personen niet in leven zijn, dus het is een beetje overdreven.
• Iets soortgelijks gebeurt ook met reïncarnaties: sommige studenten willen expliciet aangeven dat iemand die op tijdstip x is overleden, daarna nooit meer geboren worden...
• Bij deze opgave is het niet verplicht om de systematische methode te gebruiken, maar als je ziet dat er echt rare dingen staan, kun je wel vragen of ze die methode gebruikt hebben om tot hun formule te komen. Meestal was dat dan niet zo.
• Hieronder een voorbeelduitwerking (die hopelijk goed is).

Require Import BenB.


Variable M: Set.
(* Verzameling van alle levende en overleden mensen. *)

Definition T:= R.
(* Verzameling tijdstippen in minuten. *)

Variable isMan: M -> B.
(* isMan x: x is een man *)

Variable ouderVan: M -> M -> B.
(* ouderVan x y: x is ouder van y *)

Variable wordtGeboren: M -> T -> B.
(* wordtGeboren x t: x wordt geboren op tijdstip t *)

Variable overlijdt: M -> T -> B.
(* overlijdt x t: x overlijdt op tijdstip t *)

Variable trouwtMet: M -> M -> T -> B.
(* trouwtMet x y t: x trouwt met y op tijdstip t *)

(* Hulppredikaten *)

Definition leeft (x:M) (t:T) :=
(* Er is een moment t0 waarvoor geldt dat
     t0 komt voor t en
     x wordt geboren op t0 en
     tussen t0 en t overlijft x niet. *)
exists t0:T,
    t0 < t
  /\
    wordtGeboren x t0
  /\
    (
      forall t1:T,
          t1 in (t0,t) 
        ->
          ~overlijdt x t1
    )
.

Definition isWeduwe (x:M) (t:T) :=
(* x leeft op moment t en
   x is vrouw en
   er is een mens m waarvoor geldt dat
     er is een moment t0 waarvoor geldt dat
       t0 < t en
       x trouwt met m op tijdstip t0 en
       er is een moment t1 waarvoor geldt dat
         t0 < t1 en
         t1 < t en
         m overlijdt op tijdstip t1. *)
(* Merk op dat we geen 'gescheiden' hebben, dus eens getrouwd
   blijft getrouwd. *)
(* En eigenlijk ontbreekt hier natuurlijk dat
   de vrouw na het overlijden van haar partner
   niet opnieuw is getrouwd. *)

  leeft x t
/\
  ~isMan x
/\
  (
     exists m:M,
       exists t0:T,
           t0 < t
         /\
           trouwtMet x m t0
         /\ 
           (
              exists t1:T,
                  t0 < t1
                /\
                  t1 < t
                /\
                  overlijdt m t1
           )
  )         
.

Definition tweeling (x:M) (y:M) :=
(* x en y hebben dezelfde moeder en
   x en y zijn even oud. *)
(* Deze definitie komt uit Van Dale. Er zijn ook
   definities die uitgaan naar bevruchting op hetzelfde
   moment, maar daar kunnen we niets mee in dit domeinmodel. *)
(* Even oud betekent in dit domeinmodel dat de baby's in
   dezelfde minuut geboren moeten zijn. Dat is niet erg realistisch,
   dus daarom geven we aan dat er maximaal een uur tussen mag zitten.
   En ook dat is natuurlijk arbitrair. *)
(* Er is een mens m waarvoor geldt dat
     m is vrouw en
     m is moeder van x en
     m is moeder van y en
     er is een moment tx waarvoor geldt dat
       x wordt geboren op tx en
       er is een moment ty waarvoor geldt dat
         y wordt geboren op ty en
         ty ligt in het interval [tx-60, tx+60]. *)

exists m:M,
    ~isMan m
  /\
    ouderVan m x
  /\
    ouderVan m y
  /\
    (
      exists tx:T,
          wordtGeboren x tx
        /\
          (
            exists ty:T,
                wordtGeboren y ty
              /\
                ty in [tx-60, tx+60]
          )
    )
.
  
Definition oudsteKindVan (x:M) (y:M) :=
(* y is ouder van x en
   voor alle mensen z geldt dat
     als y ouder van z is
     dan geldt dat
       z is x of
       x wordt eerder geboren dan z. *)

  ouderVan y x
/\
  (
    forall z:M,
        ouderVan y z
      ->
          z=x
        \/
          (
            forall tx:T,
                wordtGeboren x tx
              ->
                (
                  forall tz:T,
                      wordtGeboren z tz
                    ->
                      tx < tz
                )
          )
  )
.

Klopt het dat in deze definitie van tweeling iedereen een tweeling is met zichzelf?
Tom Evers → Beweren en bewijzen	Remove this comment when resolved!

(tweeling tom tom) is inderdaad waar volgens deze definitie.
Rick Erkens → Tom Evers	Remove this comment when resolved!

Opgave 2

• Dingen die beter hadden gekund:
  • Verzameling tijdstippen in plaats van tijd.
  • Het is onduidelijk of de noodstopknop en de veiligheidsknop nu ook onderdeel van S, de knoppen van het bedieningspaneel zijn.
  • En waarom is ruimteAanwezig als een functie genoemd? Dat zou toch ook als een predikaat kunnen? Maar dan moet er wel een meting bij.
  • Bij de betekenis worden wel parametes t, s en k gebruikt (soms de types T en K), maar eigenlijk moet er dan wel eerst iets staan als knopGedrukt t s.
  • De metingen zijn onduidelijk. Wat is bijvoorbeeld het verschil tussen een drukmeter en een druksensor?
  • Wat is een ODU? In de betekenis van "obstructieGedetecteerd".
• Indien jullie fouten zien die ik hier nog niet had genoemd, voeg ze dan toe.
• Zie onderstaand script voor de hulppredikaten en de specificaties van het geheel.

Require Import BenB.


Definition T := R.
(* De verzameling tijdstippen in seconden. *)
Variable K: Set.
(* De verzameling van verschillende kasten. *)
Variable S: Set.
(* De verzameling van knoppen op het besturingspaneel. *)

(* Functies *)
Variable ruimteAanwezig: T -> K -> B.
(* Geeft aan of er op tijdstip T rechts van kast K voldoende ruimte 
   aanwezig is. *)
Variable knopKast: S -> K.
(* Geeft een kast k bij een knop s. *)


(* Predikaten *)

Variable obstructieGedetecteerd: T-> B.
(* obstructieGedetecteerd t: Geeft aan of op tijdstip t een obstructie 
   gedetecteerd is door de ODU. *)
Variable noodstop: T -> B.
(* noodstop t: Geeft aan of op tijdstip t een noodstop knop ingedrukt is. *)
Variable isVeiligknop: T -> B.
(* isVeiligknop t: Geeft aan of op tijdstip t de veiligheidsknop ingedrukt
   is. *)	
Variable opdrachtGegeven: T -> K -> B.
(* opdrachtGegeven t k: Geeft aan of op tijdstip t de opdracht is gegeven 
   om rechts van kast k ruimte te maken. *)
Variable kastBeweegt: T -> K -> B.
(* kastBeweegt t k: Geeft aan of op tijdstip t kast k beweegt. *)
Variable knopGedrukt: T -> S -> B.	
(* knopGedrukt t s: Geeft aan of op tijdstip t op knop s is gedrukt. *)

Definition ruimteBespaard := 
forall t:T,
    (
       forall k:K,
         ~ruimteAanwezig t k
    )
  \/
    (
       exists k:K,
           ruimteAanwezig t k
         /\
           (
             forall k1:K,
                 ruimteAanwezig t k1
               ->
                 k1 = k
           )
    )
.

Definition magBewegen (t:T) :=
exists t1:T,
    isVeiligknop (t-t1)
  /\
    (
      forall t2:T,
          t2 in (t-t1, t]
        ->
            ~obstructieGedetecteerd t2
          /\
            ~noodstop t2
    )
.

Definition isVeilig := 
forall t:T,
    magBewegen t
  \/
    (
      forall k:K,
        ~kastBeweegt t k
    )
.

Definition allesBereikbaar :=
forall s:S,
  forall t:T,
        knopGedrukt t s
      /\
        (
          forall t1:T,
              t1 in (t,t+30]
            ->
              magBewegen t1
        )
    ->
      ruimteAanwezig (t+30) (knopKast s)
.

(* Specificaties van het geheel *)

(* Als op een willekeurig moment op een of andere knop wordt gedrukt, 
   dan is er een zekere tijd later ruimte aanwezig bij de bijbehorende 
   kast. *)
Definition spec1 :=
forall t:T,
  forall s:S,
      knopGedrukt t s
    ->
       (
         exists t1:T,
             t1 > t
           /\
             ruimteAanwezig t1 (knopKast s)
       )
.

(* Als op een willekeurig moment op de veiligheidsknop wordt gedrukt en 
   als er dan 5 seconden later op een of andere knop wordt gedrukt en 
   gedurende een minuut na het indrukken van de veiligheidsknop wordt 
   er geen obstructie gedetecteerd en ook niet op de noodknop gedrukt, 
   dan is er 35 seconden na het indrukken van de veiligheidsknop ruimte 
   bij de bijbehorende kast. *)

(* Met 'een of andere knop' is hier waarschijnlijk bedoeld dat het om
   een keuzeknop gaat en niet om de noodstopknop of juist weer de
   veiligheidsknop. *)

(* Bij deze uitwerking is alles wat niet afhankelijk is van de knop s
   naar voren gehaald. *)
Definition spec2a :=
forall t:T,
      isVeiligknop t
    /\
      (
        forall t1:T,
            t1 in (t, t+60]
          ->
              ~obstructieGedetecteerd t1
            /\
              ~noodstop t1
      )
  ->
    (
      forall s:S,
          knopGedrukt (t+5) s
        ->
          ruimteAanwezig (t+35) (knopKast s)   
    )
.

(* Bij deze uitwerking is juist de forall s:S naar voren gehaald. Dit
   zorgt ervoor dat de rest van de formule meer overeenkomt qua structuur
   met de natuurlijke taal, maar is in feite wel in tegenspraak met
   de systematische methode. *)

Definition spec2b :=
forall t:T,
  forall s:S,
        isVeiligknop t
      /\
        knopGedrukt (t+5) s
      /\ 
        (
          forall t1:T,
              t1 in (t, t+60]
            ->
                ~obstructieGedetecteerd t1
              /\
                ~noodstop t1
        )
    ->
      ruimteAanwezig (t+35) (knopKast s)
.​

Opgave 3

• Deze opgave staat bijna letterlijk in het lesmateriaal (vakje Tijdslogica) en is dus een klein testje of men de stof op de werkplaats een beetje doorleest.