Beweren en bewijzen/supplement/assistentie/taak 05

Hier wat extra informatie over de leertaak.

Opmerking vooraf

• Voor alle duidelijkheid: er is een nieuwe versie van de tableauregels gemaakt! Zie Bestand:Tableauregels.pdf.
• De regels voor de logische operatoren zijn uiteraard hetzelfde gebleven.
• Er zijn drie regels toegevoegd voor de boekhouding;
  • clear_L om aan de linkerkant van het bolletje dubbele voorkomens van formules weg te halen.
  • clear_R om dat aan de rechterkant te kunnen doen.
  • unfold om (net als in Coq) een Definition uit te schrijven als de formules die er onder zitten. Op het moment dat er een correctheidsstelling bewezen moet worden is het waarschijnlijk handig om eerst wat simpele dingen te doen met de definities op het niveau van onderdelen en als er dan geen voegtekens meer zijn via deze unfold de definities open te klappen.
• Die clear-regels ondervangen eigenlijk ook de terugkerende vraag waarom het nodig is om formules dubbel op te schrijven. Het oude andtwoord was dat dat nodig was om te kunnen zien of de uitgevoerde regel precies goed is toegepast. Dat antwoord geldt nog steeds, maar nu komt er bij dat er niet voor niets van die clear regels zijn om dingen op te ruimen die dubbel zijn.

Opgave 1

• Hier is weinig commentaar te geven.
• Maar let er wel op dat er niet alleen maar wordt gezegd welke beweringen geprobeerd zijn, maar ook welke beweringen wel of juist niet gelukt zijn.
• Indien hier vragen staan als het niet gelukt is, probeer die dan zo goed mogelijk te beantwoorden.

Opgave 2

• In de leesbare varianten van de correctheidsstelling zie ik al een paar keer dat er geen haakjes meer staan, bijvoorbeeld als de definities van de onderdelen zijn uitgeschreven, waardoor er door de hogere prioriteit van de ∧ opeens andere formules staan. Graag opmerkingen over maken.
• Sommige mensen hadden wel een stelling die door Coq werd goedgekeurd, maar het was toch geen correctheidsstelling omdat de koppeling zo gemaakt was dat een van de onderdelen niet nodig was. (Typisch als een input van een onderdeel is gekoppeld aan de invoer van een ander onderdeel. Zie de slides van afgelopen maandag in Blackboard.)
• Een andere fout was dat er interne fenomenen in de spec van het geheel waren opgenomen.
• Zie je een stelling die wel waar is, maar waar toch twijfels over zijn, zet daar dan commentaar bij.

Opgave 3

• De redenering zou ongeveer van hetzelfde niveau moeten zijn als de redeneringen over de deurbel eerder dit semester.
• Dus kleine stappen en liefst verwijzingen naar welke eigenschappen er precies gebruikt worden om tot een deelconclusie te komen.