Beweren en bewijzen/de zuilen/Zekerheid/6. Wiskunde/oefenstellingen

literatuur Speciale Coq commando's voor intervallen

Hier staan enkele oefenopgaven met predikaatlogica, getallen en intervallen. Je kunt zowel op papier oefenen als met Coq. Voor het werkstuk is het belangrijk dat je dit soort opgaven ook met Coq kunt maken. Bovendien heeft Coq als voordeel dat iedere fout wordt opgemerkt.

Coq kent speciale commando's om met getallen en intervallen te werken. Op deze pagina lees je hier meer over. Je zult ze zeker nodig hebben bij deze stellingen.

Op de bijbehorende discussiepagina kan men elkaar helpen, maar plaats geen uitwerkingen.

Oefenopgaven

<source lang="coq"> Require Import BenB.

Variable X: R->B. Variable Y: R->B. Variable Z: R->B.

Theorem getallen_001 :

 (forall t:R, t>=2 -> X t)

->

 (forall t:R, t>=3 -> X t).

Theorem getallen_002 :

 (X 2)

->

   (forall t:R, X t -> Y (t+3))
 ->
   (Y 5).

Theorem getallen_003 :

 (Y 0)

->

   (forall t:R, Y t -> (forall u:R, u>=t+2 -> X u))
 ->
   (forall t:R, t>=3 -> X t).

Theorem getallen_004 :

 (forall t:R, X t -> Y (t+1) \/ Y (t+2))

->

 (forall t:R, X t -> (exists u:R, u>=t+1 /\ Y u)).

Theorem getallen_005 :

 (forall t:R, (exists u:R, u<=t-5 /\ Y u) -> X t)

->

 (forall t:R, Y t -> X (t+5)).

Theorem getallen_006 :

 (forall t:R, X t -> Y (t+2))

->

   (forall t:R, Y t -> Z (t+3))
 ->
   (forall t:R, X t -> Z (t+5)).

Theorem getallen_007 :

 (forall t:R, X t -> (exists u:R, u in (t+2,t+5] /\ Y u))

->

 (forall t:R, X t -> (exists u:R, u in (t+1,t+6] /\ Y u)).

Theorem getallen_008 :

 (forall t:R, X t -> (exists u:R, u in (t+2,t+5] /\ Y u))

->

 (forall t:R, X t -> (exists u:R, u in (t,t+3] /\ Y (u+2))).

Theorem getallen_009 :

 (forall t:R, X t -> (exists u:R, u in [t+2,t+5) /\ Y u))

->

   (forall t:R, Y t -> Z (t+3))
 ->
   (forall t:R, X t -> (exists u:R, u in [t+5,t+8) /\ Z u)).

Theorem getallen_010 :

 (forall t:R, X t -> (forall u:R, u<t-5 -> Y u))

->

 (forall t:R, (exists u:R, t+5 Y t).

</source>

Voorbeelduitwerkingen

Hier vind je ter illustratie twee uitwerkingen van stelling 'getallen_007'. Een in de vorm van een echte boom zoals je het op het tentamen zou moeten kunnen maken en een in de vorm van een Coq script. (Voor het gemak is het script van commentaar voorzien waardoor het duidelijk zou moeten zijn waarom er op een bepaald moment een bepaalde regel wordt toegepast.)

Helaas vindt de werkplaats deze boom net iets te moeilijk om nog in zijn geheel weer te geven. Vandaar dat hij hier in een aantal stukken geknipt is.

Hier eerst het belangrijke begin van de boom.

... ... →E ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a ⊢ ∃ u:R, u ∈ (a+2, a+5] ∧ Q u ... ∃I ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ ∃ u:R, u ∈ (a+1, a+6] ∧ Q u ∃E ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a ⊢ ∃ u:R, u ∈ (a+1, a+6] ∧ Q u →I ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u) ⊢ P a → (∃ u:R, u ∈ (a+1, a+6] ∧ Q u) ∀I ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u) ⊢ ∀ t:R, P t → (∃ u:R, u ∈ (t+1, t+6] ∧ Q u)

→I

⊢ (∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u)) → (∀ t:R, P t → (∃ u:R, u ∈ (t+1, t+6] ∧ Q u))

Hier het linkerblok met de →E-regel.

hyp ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a ⊢ ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u) ∀E ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a ⊢ P a → ∃ u:R, u ∈ (a+2, a+5] ∧ Q u	hyp ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a ⊢ P a	→E
∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a ⊢ ∃ u:R, u ∈ (a+2, a+5] ∧ Q u

En daarna het rechterblok met de ∃I-regel.

... ... ∧I ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ a+1 < b ∧ b ≤ a+6 int ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ b ∈ (a+1, a+6]   hyp ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ b ∈ (a+2, a+5] ∧ Q b ∧2E ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ Q b ∧I ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ b ∈ (a+1, a+6] ∧ Q b

∃I

∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ ∃ u:R, u ∈ (a+1, a+6] ∧ Q u

Tenslotte maken we het stuk boven de ∧I af.

lins ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b, a+2 < b ⊢ a+1 < b →I ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ a+2 < b → a+1 < b   hyp ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ a+2 < b ∧ b ≤ a+5 ∧1E ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ a+2 < b →E ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ a+1 < b	lins ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b, b ≤ a+5 ⊢ b ≤ a+6 →I ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ b ≤ a+5 → b ≤ a+6   hyp ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ a+2 < b ∧ b ≤ a+5 ∧2E ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ b ≤ a+5 →E ∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ b ≤ a+6	∧I
∀ t:R, P t → (∃ u:R, u ∈ (t+2, t+5] ∧ Q u), P a, b ∈ (a+2, a+5] ∧ Q b ⊢ a+1 < b ∧ b ≤ a+6

Met name in het laatste stuk moeten we trucs uithalen door een →E te doen en direct te laten volgen door een →I om de gewenste informatie voor de lins-regel in de aannames te krijgen.

Vergelijk deze boom en in het bijzonder de plaatsen waar er lins- en int-regels zijn toegepast eens met onderstaand Coq-script!

Coq script getallen_007

Require Import BenB. Variable X: R->B. Variable Y: R->B. Theorem getallen_007 : (forall t:R, X t -> (exists u:R, u in (t+2,t+5] /\ Y u)) -> (forall t:R, X t -> (exists u:R, u in (t+1,t+6] /\ Y u)). Proof. (* Opening *) (* De bewijsverplichting is een implicatie, dus imp_i. *) imp_i a1. (* De bewijsverplichting is een voor-alle-bewering, dus een all_i met een onbesproken variabele a. *) all_i a. (* De bewijsverplichting is een implicatie, dus imp_i. *) imp_i a2. (* Middenspel *) (* Er staat (een beetje verstopt) een existentiele bewering in aanname a1. Die is niet altijd waar, maar wel als X t voor een geschikte t waar is. En we weten al dat X a waar is, dus als we hier voor t de waarde a nemen, moet dat existentiele deel wel te bewijzen zijn. *) exi_e (exists u : R, u in (a + 2, a + 5] /\ Y u) b a3. (* Eindspel voor deze tak. *) (* We willen naar aanname a1 toe, dus modus ponens. *) imp_e (X a). (* De bewijsverplichting is een exacte instantie van a1, dus all_e. *) all_e (forall t : R, X t -> exists u : R, u in (t + 2, t + 5] /\ Y u) a. (* De bewijsverplichting is precies a1, dus hyp. *) hyp a1. (* De bewijsverplichting is precies a2, dus hyp. *) hyp a2. (* De bewijsverplichting vraagt om een u aan te wijzen die in een bepaald interval zit en die voldoet aan Y u. Over dat interval denken we voorlopig niet na, maar we zien in aanname a3 wel duidelijk staan dat Y b geldt. Dus proberen we een exi_i met die b. *) exi_i b. (* De bewijsverplichting is een conjunctie, dus con_i. *) con_i. (* De bewijsverplichting is laten zien dat b in een bepaald interval zit. In aanname a3 zien we dat b zelfs in een subinterval van dat interval zit, dus het moet te bewijzen zijn. Hier zijn alleen wat technieken (trucs) voor nodig om het Coq ook te laten snappen. Het begint er mee dat we de bewering met het commando interval gaan splitsen in simpelere beweringen. *) interval. (* De bewijsverplichting is een conjunctie, dus con_i. *) con_i. (* In aanname a3 staat onder meer dat a+2 < b, maar dat staat gecombineerd met de bewering b <= a+5 en Y b. Het commando lin_solve is alleen maar te overtuigen als die deelbeweringen als losse aannames aanwezig zijn. Dus passen we nu een truc toe om die a+2 < b expliciet als aanname te krijgen, door eerst een imp_e en dan meteen een imp_i te doen. *) imp_e (a+2 < b). imp_i a4. (* Nu hebben we a+2 < b als aanname a4 en snapt lin_solve het ook. *) lin_solve. (* De truc met imp_e en imp_i heeft natuurlijk een nieuwe bewijsverplichting opgeleverd, maar die is met conjunctie-eliminaties eenvoudig uit aanname a3 te bewijzen. *) con_e1 (b<=a+5). con_e1 (Y b). (* Bedenk dat de intervalnotatie een afkorting is, dus ondanks dat het er anders uit ziet, is het eigenlijk toch hetzelfde. *) hyp a3. (* Nu de rechterkant van het interval. Ook hier staat de informatie al samengesteld in aanname a3 en ook hier gebruiken we dezelfde truc om de noodzakelijke aanname b <= a+5 expliciet te krijgen. *) imp_e (b <= a+5). imp_i a4. lin_solve. (* En op dezelfde manier is die extra bewijsverplichting weer af te leiden uit a3 met conjunctie-eliminaties. *) con_e2 (a+2<b). con_e1 (Y b). hyp a3. (* Tenslotte moeten we nog bewijzen dat Y b waar is, maar dat volgt natuurlijk ook op eenvoudige manier uit a3. *) con_e2 (b in (a + 2, a + 5]). hyp a3. Qed.