Beweren en bewijzen/het verhaal/6. Theorie/casus Iets met tijdsintervallen
Deze pagina beschrijft een bewijs zoals dat in 2006-2007 een keer tijdens het responsiecollege is beschreven. Het geeft een voorbeeld van een bewijs met tijd en in het bijzonder tijdsintervallen.
De stelling waar we naar kijken ziet er in Coq zo uit:
( (forall t:T, (forall d:T, d in (t,t+3] -> s d) -> h(t+3)) /\ (forall t:T, (h t /\ (forall d:T, d in (t, t+2] -> s d)) -> x (t+2)) ) -> (forall t:T, (forall d:T, d in (t,t+6]->s d)->x (t+6)).
Merk op dat er hier overdreven veel haakjes staan. En waar de predicaten voor staan is helaas niet meer bekend, maar aangezien het hier in feite alleen een formeel spel is, is dat niet erg.
Bij dit soort bewijzen krijg je op een gegeven moment te maken met uitspraken als 'a+4+2 = a+6' en 'a>3 => a>2'. De vraag is hoe je die 'triviale' beweringen netjes in je bewijs kunt stoppen. Nou, tegenwoordig kan dat vrij simpel met het lin_solve commando.
Eerst zorgen dat we met reële getallen kunnen werken en dat de predicaten allemaal gedefinieerd zijn.
(* Iets met tijdsintervallen (versie 07-08) *) Require Import BenB. Definition T := R. Variables s h x: T->Prop.
Nu de stelling en het bewijs zelf.
Theorem iets_met_tijdsintervallen : ( (forall t:T, (forall d:T, d in (t,t+3] -> s d) -> h(t+3)) /\ (forall t:T, (h t /\ (forall d:T, d in (t, t+2] -> s d)) -> x (t+2)) ) -> (forall t:T, (forall d:T, d in (t,t+6]->s d)->x (t+6)). Proof. imp_i H1. all_i a. imp_i H2. imp_e ( h(a+4) /\ (forall d:T, d in (a+4,a+6]-> s d)).
Tot nu toe ging het allemaal heel vanzelfsprekend. In de volgende stap willen we echter een ∀-E toepassen waarbij we nu eens een keer niet een simpele variabele willen gebruiken, maar een iets complexere term. We proberen toe te werken naar iets wat dezelfde conclusie heeft als het tweede deel van aanname H1. Als x(t+2) moet matchen met x(a+6), moeten we dus de term t=a+4 als specifiek geval nemen. Op papier kunnen we dat zonder problemen doen omdat wij wel weten dat a+4+2 hetzelfde is als a+6. Coq weet dat op zich ook wel (via lin_solve), maar bij de instantiatie wil Coq dat in de huidige goal exact die term staat die we willen gaan invullen voor t. Dus moeten we Coq expliciet vertellen dat a+6=a+4+2. Dat kan met 'replace'. Je ziet dat de instantiatie nu lukt en dat deze tak vervolgens eenvoudig is af te sluiten.
replace (a+6) with ((a+4)+2). all_e ( forall t:T, h t /\ (forall d:T, d in (t, t+2] -> s d) -> x(t+2) ) (a+4). con_e2 (forall t:T, (forall d:T, d in (t, t+3] -> s d) -> h (t+3)). assumption. lin_solve.
Nu zijn we bij een goal uitgekomen waarvan de linkerhelft uit H1 moet worden bewezen en de rechterhelft uit H2.
con_i. imp_e (forall d : T, d in (a+1, a+4] -> s d).
Hier gebruiken we dezelfde methode als zostraks: als h(t+3) moet matchen met h(a+4), betekent dat dat we als term t=a+1 moeten nemen en dus moeten we de a+4 die er nu staat weer omschrijven tot een voor Coq bruikbare (a+1)+3. De rest van deze tak en de extra bewijsverplichting a+4=(a+1)+3 zijn eenvoudig af te sluiten.
replace (a+4) with ((a+1)+3).
all_e ( forall t:T, (forall d:T, d in (t, t+3] -> s(d))->h(t+3)) (a+1).
con_e1 (forall t : T,
h t /\ (forall d : T, d in (t, t + 2] -> s d) -> x (t + 2)).
assumption.
lin_solve.
De goal die we nu hebben, is duidelijk af te leiden uit H2. In H2 staat namelijk dat s d geldt voor het hele interval (a, a+6]. En omdat het interval (a+1, a+4] uit onze goal geheel binnen (a, a+6] ligt, moeten we deze goal echt uit H2 kunnen afleiden. Eerst instantiëren we d met z, zodat we vervolgens weer op de standaardmanier kunnen bewerkstelligen dat onze goal exact wordt omgeschreven naar H2.
all_in z. imp_in H3. imp_e (z in (a,a+6]). all_el (forall d : T, d in (a, a + 6] -> s d) z. assumption.
Dit levert alleen de extra bewijsverplichting op dat 'z in (a, a + 6]' terwijl we als aanname al weten dat 'z in (a+1, a + 4]. Helaas is een lin_solve hier niet toereikend. We moeten dan ook de intervalnotatie in de goal gaan uitschrijven als een conjunctie. En die vervolgens opsplitsen.
interval. con_i.
Onze goal a<z volgt natuurlijk uit het feit dat we al weten dat a+1<z, wat impliciet zit in H3. Om lin_solve te kunnen laten werken, moet deze bewering echter expliciet als aanname zijn opgenomen. Dat kunnen we voor elkaar krijgen door eerst een →E uit te voeren, gevolgd door een →-I. (Daar waar je die meestal precies andersom uitvoert.)
imp_e (a+1<z). imp_i H4. lin_solve.
De goal waar we nu mee zitten is a+1<z. Omdat dit precies ëën van de grenzen is uit H3, gaan we gebruikmaken van het feit dat H3 eigenlijk een conjunctie is. Merk op dat hier geen interval of zo hoeft te worden gebruikt. Het commando assumption snapt al dat H3 hetzelfde is als onze goal, ondanks dat ze er anders uitzien.
con_e1 (z<=a+4). assumption.
Om de volgende goal z<=a+6 te bewijzen doen we nog een keer hetzelfde als in de vorige twee blokjes.
imp_e (z<=a+4). imp_i H5. lin_solve. con_e2 (a+1 < z). assumption.
Nu krijgen we weer een soortgelijk probleem. We moeten bewijzen dat s d waar is op (a+4, a+6] terwijl in aanname H2 al staat dat s d geldt op het grotere domein (a, a+6]. Het bewijs gaat dan ook volkomen analoog aan wat we net gezien hebben.
all_i z. imp_i H6. imp_e (z in (a, a+6]). all_e (forall d : T, d in (a, a + 6] -> s d) z. assumption. interval. con_i. imp_e (a+4<z). imp_i H7. lin_solve. con_e1 (z<=a+6). assumption. con_e2 (a+4<z). assumption. Qed.
Omdat de hierboven gegeven commandolijst natuurlijk geen bewijs is, geven we hier het echte bewijs in Fitch notatie.
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 1 │ H1: (∀t:T, (∀d:T, d∈(t, t+3] → s d) → h (t+3)) ∧ (∀t:T, h t ∧ (∀d:T, d∈(t, t+2] → s d) → x (t+2)) assumption │┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 2 ││ a: T assumption ││┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 3 │││ H2: ∀d:T, d∈(a, a+6] → s d assumption 4 │││ (∀t:T, (∀d:T, d∈(t, t+3] → s d) → h (t+3)) ∧ (∀t:T, h t ∧ (∀d:T, d∈(t, t+2] → s d) → x (t+2)) assumption 5 │││ ∀t:T, h t ∧ (∀d:T, d∈(t, t+2] → s d) → x (t+2) ∧e₂ 4 6 │││ h (a+4) ∧ (∀d:T, d∈(a+4, a+4+2] → s d) → x (a+4+2) ∀e 5 7 │││ a+4+2 = a+6 lin_solve 8 │││ h (a+4) ∧ (∀d:T, d∈(a+4, a+6] → s d) → x (a+6) [replace,(a,+,6),with,(a,+,4,+,2)] 6,7 9 │││ (∀t:T, (∀d:T, d∈(t, t+3] → s d) → h (t+3)) ∧ (∀t:T, h t ∧ (∀d:T, d∈(t, t+2] → s d) → x (t+2)) assumption 10 │││ ∀t:T, (∀d:T, d∈(t, t+3] → s d) → h (t+3) ∧e₁ 9 11 │││ (∀d:T, d∈(a+1, a+1+3] → s d) → h (a+1+3) ∀e 10 12 │││ a+1+3 = a+4 lin_solve 13 │││ (∀d:T, d∈(a+1, a+4] → s d) → h (a+4) [replace,(a,+,4),with,(a,+,1,+,3)] 11,12 │││┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 14 ││││ z: T assumption ││││┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 15 │││││ H3: z∈(a+1, a+4] assumption 16 │││││ ∀d:T, d∈(a, a+6] → s d assumption 17 │││││ z∈(a, a+6] → s z ∀e 16 │││││┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 18 ││││││H4: a+1 < z assumption 19 ││││││ a < z lin_solve │││││└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 20 │││││ a+1 < z → a < z →i 18-19 21 │││││ a+1 < z ∧ z <= a+4 assumption 22 │││││ a+1 < z ∧e₁ 21 23 │││││ a < z →e 20,22 │││││┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 24 ││││││H5: z <= a+4 assumption 25 ││││││ z <= a+6 lin_solve │││││└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 26 │││││ z <= a+4 → z <= a+6 →i 24-25 27 │││││ a+1 < z ∧ z <= a+4 assumption 28 │││││ z <= a+4 ∧e₂ 27 29 │││││ z <= a+6 →e 26,28 30 │││││ a < z ∧ z <= a+6 ∧i 23,29 31 │││││ z∈(a, a+6] interval 30 32 │││││ s z →e 17,31 ││││└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 33 ││││ z∈(a+1, a+4] → s z →i 15-32 │││└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 34 │││ ∀d:T, d∈(a+1, a+4] → s d ∀i 14-33 35 │││ h (a+4) →e 13,34 │││┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 36 ││││z: T assumption ││││┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 37 │││││H6: z∈(a+4, a+6] assumption 38 │││││ ∀d:T, d∈(a, a+6] → s d assumption 39 │││││ z∈(a, a+6] → s z ∀e 38 │││││┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 40 ││││││H7: a+4 < z assumption 41 ││││││ a < z lin_solve │││││└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 42 │││││ a+4 < z → a < z →i 40-41 43 │││││ a+4 < z ∧ z <= a+6 assumption 44 │││││ a+4 < z ∧e₁ 43 45 │││││ a < z →e 42,44 46 │││││ a+4 < z ∧ z <= a+6 assumption 47 │││││ z <= a+6 ∧e₂ 46 48 │││││ a < z ∧ z <= a+6 ∧i 45,47 49 │││││ z∈(a, a+6] interval 48 50 │││││ s z →e 39,49 ││││└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 51 ││││ z∈(a+4, a+6] → s z →i 37-50 │││└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 52 │││ ∀d:T, d∈(a+4, a+6] → s d ∀i 36-51 53 │││ h (a+4) ∧ (∀d:T, d∈(a+4, a+6] → s d) ∧i 35,52 54 │││ x (a+6) →e 8,53 ││└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 55 ││ (∀d:T, d∈(a, a+6] → s d) → x (a+6) →i 3-54 │└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 56 │ ∀t:T, (∀d:T, d∈(t, t+6] → s d) → x (t+6) ∀i 2-55 └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── 57 (∀t:T, (∀d:T, d∈(t, t+3] → s d) → h (t+3)) ∧ (∀t:T, h t ∧ (∀d:T, d∈(t, t+2] → s d) → x (t+2)) → ∀t:T, (∀d:T, d∈(t, t+6] → s d) → x (t+6) →i 1-56
