Beweren en bewijzen/supplement/assistentie/taak 06

Hier wat informatie over Leertaak 6.

Opgave 1

• Er hoort in de uitwerkingen niet alleen te staan wat de conclusie van het tableau was, maar ook wat de eerste impressie was. En daarbij hoort natuurlijk ook een korte redenering waarom het dan wel of niet een tautologie lijkt.
• Idealiter wordt een gevonden tegenvoorbeeld expliciet gegeven. Ik zie dat dat niet formeel bij het product hoort, maar vraag er gerust om als je ziet dat er alleen maar gezegd wordt dat er een tegenvoorbeeld is.
• Uit mijn hoofd zijn de stellingen 1, 2, 3, 6 en 10 waar en de andere dus niet.
• Tegenvoorbeelden:
  • 4: A onwaar, B onwaar, C onwaar.
  • 5: A waar, B waar, C onwaar.
  • 7: A waar, B waar, C waar of A waar, B waar, C onwaar of A onwaar, B waar, C onwaar of A onwaar, B onwaar, C onwaar
  • 8: A waar, B onwaar, C onwaar of A onwaar, B waar, C onwaar.
  • 9: A onwaar, B onwaar, C onwaar.

Opgave 2

• Wat er zoal mis is:
  • Een ':' in plaats van een ':='.
  • Geen punt aan het einde.
  • Een '<=>' in plaats van '<->'.
  • Matchende haakjes staan niet netjes onder elkaar.
  • Suggestieve layout waardoor het een conjunctie lijkt terwijl het een equivalentie is.
  • De haakjes bij het hele eerste stuk, (audio_stekker_in /\ microfoon_stekker_in) en (geluid_aan /\ microfoon_aan) zijn overbodig, maar niet fout. Voor het maken van de constructieboom is het echter verstandig om ze weg te halen, want dat scheelt een hoop werk.
• Bij twijfel over syntax en overbodige haakjes: laat ze de definitie in Coq invoeren. Door op een slimme manier Theorem en unfold te gebruiken, krijg je gratis welke haakjes essentieel zijn en welke niet. Dus als studenten vragen stellen over welke haakjes overbodig zijn, kun je ze deze tip geven.
• Helemaal uitgewerkt tot op het niveau van enkele proposities (overbodige haakjes laten staan):

Definition headset :=
  (
      (   computer_aan 
        <-> 
          (
              audio_stekker_in 
            /\ 
              microfoon_stekker_in
          )
      ) 
    /\ 
      geluidsknop_aan 
    /\ 
      microfoonknop_aan
  ) 
<-> 
  (
      geluid_aan 
    /\ 
      microfoon_aan
  )
.

• Of iets minder ver uitgewerkt, maar wel goed leesbaar. (Misschien wel beter leesbaar dan de volledig uitgeklapte variant.)

Definition headset :=
  (
      (computer_aan <-> (audio_stekker_in /\ microfoon_stekker_in)) 
    /\ 
      geluidsknop_aan 
    /\ 
      microfoonknop_aan
  ) 
<-> 
  (geluid_aan /\ microfoon_aan)
.

• De laatste variant met een minimaal aantal haakjes wordt:

Definition headset :=
    (computer_aan <-> audio_stekker_in /\ microfoon_stekker_in)
  /\ 
    geluidsknop_aan 
  /\ 
    microfoonknop_aan 
<-> 
  geluid_aan /\ microfoon_aan
.

• In mijn uitwerkingen ga ik uit van telkens twee spaties inspringen per niveau. Dat is natuurlijk geen wet.
• Ook zet ik de afsluitende punt bij voorkeur vooraan, maar ook dat is geen wet.

Opgave 3

• Een voorbeelduitwerking:

(** Basistypes **)
Variable PN: Set. (* perceelnummer *)
Inductive BT: Set := wonen | bedrijventerrein | horeca | groenvoorziening. (* bebouwingstype *)
Variable BP: Set. (* bouwplan *)

(** Basisfuncties en -predikaten, met betekenis en meting: **)
Variable BestemmingsplanVanPerceel: PN -> BT. (* Wat zegt het gemeentelijke bestemmingsplan over dit perceel? Meting: In gemeentearchief nakijken. *)
Variable AlBebouwd: PN -> B. (* Is een perceel al bebouwd? Meting: kijken *)
Variable IsVerbouwing: BP -> B. (* Is het een verbouwing? Meting: architect vragen *)
Variable PerceelnummerVanBouwplan: BP -> PN. (* Wat is het perceelnummer van het bouwplan? Meting: architect vragen *)
Variable BebouwingstypeVanBouwplan: BP -> BT. (* Wat is het gewenste bebouwingstype van het bouwplan? Meting: architect vragen *)

(** Hulpdefinitie **)
Definition PastInBestemmingsplan (plan:BP) :=
    BestemmingsplanVanPerceel (PerceelnummerVanBouwplan plan)
=
    BebouwingstypeVanBouwplan plan
.

(** Verlangde definitie **)
Definition vergunningWordtAfgegegeven (plan:BP) :=
        PastInBestemmingsplan plan
    \/
            IsVerbouwing plan
        /\
            AlBebouwd (PerceelnummerVanBouwplan plan)
.

• Het is niet nodig om deze opgave als een Coq-script in te voeren, maar de uiteindelijke definitie en eventuele hulpdefinities moeten wel volgens de grammatica met 'Definition' en zo worden weergegeven.
• Bij de basisdefinities wordt Inductive gebruikt. Die constructie is genoemd in de slides van David. Maar indien men een gewone tabel maakt met het domeinmodel, mag dit natuurlijk gewoon als een verzameling worden weergegeven.
• Let er op dat er metingen staan bij de basispredikaten. Bij de basisfuncties hoeft dat niet volgens de theorie (maar David heeft het hierboven wel gedaan). De betekenis moet natuurlijk zowel bij de basispredikaten als de basisfuncties worden gegeven.