From: Andrea Asperti Date: Thu, 19 Jul 2012 09:19:39 +0000 (+0000) Subject: adding tutorial X-Git-Tag: make_still_working~1606 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f0626b0315cb0ca51aacb40234f02edd970524c;p=helm.git adding tutorial --- diff --git a/matita/matita/lib/tutorial/chapter1.ma b/matita/matita/lib/tutorial/chapter1.ma new file mode 100644 index 000000000..e726eac07 --- /dev/null +++ b/matita/matita/lib/tutorial/chapter1.ma @@ -0,0 +1,372 @@ +(* +Data types, functions and theorems + +Matita is both a programming language and a theorem proving environment: +you define datatypes and programs, and then prove properties on them. +Very few things are built-in: not even booleans or logical connectives +(but you may of course use libraries, as in normal programming languages). +The main philosophy of the system is to let you define your own data-types +and functions using a powerful computational mechanism based on the +declaration of inductive types. + +Let us start this tutorial with a simple example based on the following well +known problem. + +The goat, the wolf and the cabbage +A farmer need to transfer a goat, a wolf and a cabbage across a river, but there +is only one place available on his boat. Furthermore, the goat will eat the +cabbage if they are left alone on the same bank, and similarly the wolf will eat +the goat. The problem consists in bringing all three items safely across the +river. + +Our first data type defines the two banks of the river, which will be named east +and west. It is a simple example of enumerated type, defined by explicitly +declaring all its elements. The type itself is called "bank". +Before giving its definition we "include" the file "logic.ma" that contains a +few preliminary notions not worth discussing for the moment. +*) + +include "basics/logic.ma". + +inductive bank: Type[0] ≝ +| east : bank +| west : bank. + +(* We can now define a simple function computing, for each bank of the river, the +opposite one. *) + +definition opposite ≝ λs. +match s with + [ east ⇒ west + | west ⇒ east + ]. + +(* Functions are live entities, and can be actually computed. To check this, let +us state the property that the opposite bank of east is west; every lemma needs a +name for further reference, and we call it "east_to_west". *) + +lemma east_to_west : opposite east = west. + +(* +The goal window + +If you stop the execution here you will see a new window on the right side +of the screen: it is the goal window, providing a sequent like representation of +the form + +B1 +B2 +.... +Bk +----------------------- +A + +for each open goal remaining to be solved. A is the conclusion of the goal and +B1, ..., Bk is its context, that is the set of current hypothesis and type +declarations. In this case, we have only one goal, and its context is empty. +The proof proceeds by typing commands to the system. In this case, we +want to evaluate the function, that can be done by invoking the "normalize" +command: +*) + +normalize + +(* By executing it - just type the advance command - you will see that the goal +has changed to west = west, by reducing the subexpression (opposite east). +You may use the retract bottom to undo the step, if you wish. + +The new goal west = west is trivial: it is just a consequence of reflexivity. +Such trivial steps can be just closed in Matita by typing a double slash. +We complete the proof by the qed command, that instructs the system to store the +lemma performing some book-keeping operations. +*) + +// qed. + +(* In exactly the same way, we can prove that the opposite side of west is east. +In this case, we avoid the unnecessary simplification step: // will take care of +it. *) + +lemma west_to_east : opposite west = east. +// qed. + +(* +Introduction + +A slightly more complex problem consists in proving that opposite is idempotent *) + +lemma idempotent_opposite : ∀x. opposite (opposite x) = x. + +(* we start the proof moving x from the conclusion into the context, that is a +(backward) introduction step. Matita syntax for an introduction step is simply +the sharp character followed by the name of the item to be moved into the +context. This also allows us to rename the item, if needed: for instance if we +wish to rename x into b (since it is a bank), we just type #b. *) + +#b + +(* See the effect of the execution in the goal window on the right: b has been +added to the context (replacing x in the conclusion); moreover its implicit type +"bank" has been made explicit. +*) + +(* +Case analysis + +But how are we supposed to proceed, now? Simplification cannot help us, since b +is a variable: just try to call normalize and you will see that it has no effect. +The point is that we must proceed by cases according to the possible values of b, +namely east and west. To this aim, you must invoke the cases command, followed by +the name of the hypothesis (more generally, an arbitrary expression) that must be +the object of the case analysis (in our case, b). +*) + +cases b + +(* Executing the previous command has the effect of opening two subgoals, +corresponding to the two cases b=east and b=west: you may switch from one to the +other by using the hyperlinks over the top of the goal window. +Both goals can be closed by trivial computations, so we may use // as usual. +If we had to treat each subgoal in a different way, we should focus on each of +them in turn, in a way that will be described at the end of this section. +*) + +// qed. + +(* +Predicates + +Instead of working with functions, it is sometimes convenient to work with +predicates. For instance, instead of defining a function computing the opposite +bank, we could declare a predicate stating when two banks are opposite to each +other. Only two cases are possible, leading naturally to the following +definition: +*) + +inductive opp : bank → bank → Prop ≝ +| east_west : opp east west +| west_east : opp west east. + +(* In precisely the same way as "bank" is the smallest type containing east and +west, opp is the smallest predicate containing the two sub-cases east_west and +weast_east. If you have some familiarity with Prolog, you may look at opp as the +predicate defined by the two clauses - in this case, the two facts - ast_west and +west_east. + +Between opp and opposite we have the following relation: + opp a b iff a = opposite b +Let us prove it, starting from the left to right implication, first *) + +lemma opp_to_opposite: ∀a,b. opp a b → a = opposite b. + +(* We start the proof introducing a, b and the hypothesis opp a b, that we +call oppab. *) +#a #b #oppab + +(* Now we proceed by cases on the possible proofs of (opp a b), that is on the +possible shapes of oppab. By definition, there are only two possibilities, +namely east_west or west_east. Both subcases are trivial, and can be closed by +automation *) + +cases oppab // qed. + +(* +Rewriting + +Let us come to the opposite direction. *) + +lemma opposite_to_opp: ∀a,b. a = opposite b → opp a b. + +(* As usual, we start introducing a, b and the hypothesis (a = opposite b), +that we call eqa. *) + +#a #b #eqa + +(* The right way to proceed, now, is by rewriting a into (opposite b). We do +this by typing ">eqa". If we wished to rewrite in the opposite direction, namely +opposite b into a, we would have typed "eqa + +(* We conclude the proof by cases on b. *) + +cases b // qed. + +(* +Records + +It is time to proceed with our formalization of the farmer's problem. +A state of the system is defined by the position of four items: the goat, the +wolf, the cabbage, and the boat. The simplest way to declare such a data type +is to use a record. +*) + +record state : Type[0] ≝ + {goat_pos : bank; + wolf_pos : bank; + cabbage_pos: bank; + boat_pos : bank}. + +(* When you define a record named foo, the system automatically defines a record +constructor named mk_foo. To construct a new record you pass as arguments to +mk_foo the values of the record fields *) + +definition start ≝ mk_state east east east east. +definition end ≝ mk_state west west west west. + +(* We must now define the possible moves. A natural way to do it is in the form +of a relation (a binary predicate) over states. *) + +inductive move : state → state → Prop ≝ +| move_goat: ∀g,g1,w,c. opp g g1 → move (mk_state g w c g) (mk_state g1 w c g1) + (* We can move the goat from a bank g to the opposite bank g1 if and only if the + boat is on the same bank g of the goat and we move the boat along with it. *) +| move_wolf: ∀g,w,w1,c. opp w w1 → move (mk_state g w c w) (mk_state g w1 c w1) +| move_cabbage: ∀g,w,c,c1.opp c c1 → move (mk_state g w c c) (mk_state g w c1 c1) +| move_boat: ∀g,w,c,b,b1. opp b b1 → move (mk_state g w c b) (mk_state g w c b1). + +(* A state is safe if either the goat is on the same bank of the boat, or both +the wolf and the cabbage are on the opposite bank of the goat. *) + +inductive safe_state : state → Prop ≝ +| with_boat : ∀g,w,c.safe_state (mk_state g w c g) +| opposite_side : ∀g,g1,b.opp g g1 → safe_state (mk_state g g1 g1 b). + +(* Finally, a state y is reachable from x if either there is a single move +leading from x to y, or there is a safe state z such that z is reachable from x +and there is a move leading from z to y *) + +inductive reachable : state → state → Prop ≝ +| one : ∀x,y.move x y → reachable x y +| more : ∀x,z,y. reachable x z → safe_state z → move z y → reachable x y. + +(* +Automation + +Remarkably, Matita is now able to solve the problem by itslef, provided +you allow automation to exploit more resources. The command /n/ is similar to +//, where n is a measure of this complexity: in particular it is a bound to +the depth of the expected proof tree (more precisely, to the number of nested +applicative nodes). In this case, there is a solution in six moves, and we +need a few more applications to handle reachability, and side conditions. +The magic number to let automation work is, in this case, 9. *) + +lemma problem: reachable start end. +normalize /9/ qed. + +(* +Application + +Let us now try to derive the proof in a more interactive way. Of course, we +expect to need several moves to transfer all items from a bank to the other, so +we should start our proof by applying "more". Matita syntax for invoking the +application of a property named foo is to write "@foo". In general, the philosophy +of Matita is to describe each proof of a property P as a structured collection of +objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining +the way it is actually used (e.g. for introduction, rewriting, in an applicative +step, and so on). +*) + +lemma problem1: reachable start end. +normalize @more + +(* +Focusing + +After performing the previous application, we have four open subgoals: + + X : STATE + Y : reachable [east,east,east,east] X + W : safe_state X + Z : move X [west,west,west,west] + +That is, we must guess a state X, such that this is reachable from start, it is +safe, and there is a move leading from X to end. All goals are active, that is +emphasized by the fact that they are all red. Any command typed by the user is +normally applied in parallel to all active goals, but clearly we must proceed +here is a different way for each of them. The way to do it, is by structuring +the script using the following syntax: [...|... |...|...] where we typically have +as many cells inside the brackets as the number of the active subgoals. The +interesting point is that we can associate with the three symbol "[", "|" and +"]" a small-step semantics that allow to execute them individually. In particular + +- the operator "[" opens a new focusing section for the currently active goals, + and focus on the first of them +- the operator "|" shift the focus to the next goal +- the operator "]" close the focusing section, falling back to the previous level + and adding to it all remaining goals not yet closed + +Let us see the effect of the "[" on our proof: +*) + + [ + +(* As you see, only the first goal has now the focus on. Moreover, all goals got +a progressive numerical label, to help designating them, if needed. +We can now proceed in several possible ways. The most straightforward way is to +provide the intermediate state, that is [east,west,west,east]. We can do it, by +just applying this term. *) + + @(mk_state east west west east) + +(* This application closes the goal; at present, no goal has the focus on. +In order to act on the next goal, we must focus on it using the "|" operator. In +this case, we would like to skip the next goal, and focus on the trivial third +subgoal: a simple way to do it, is by retyping "|". The proof that +[east,west,west,east] is safe is trivial and can be done with //.*) + + || // + +(* +We then advance to the next goal, namely the fact that there is a move from +[east,west,west,east] to [west,west,west,west]; this is trivial too, but it +requires /2/ since move_goat opens an additional subgoal. By applying "]" we +refocus on the skipped goal, going back to a situation similar to the one we +started with. *) + + | /2/ ] + +(* +Implicit arguments + +Let us perform the next step, namely moving back the boat, in a sligtly +different way. The more operation expects as second argument the new +intermediate state, hence instead of applying more we can apply this term +already instatated on the next intermediate state. As first argument, we +type a question mark that stands for an implicit argument to be guessed by +the system. *) + +@(more ? (mk_state east west west west)) + +(* We now get three independent subgoals, all actives, and two of them are +trivial. We can just apply automation to all of them, and it will close the two +trivial goals. *) + +/2/ + +(* Let us come to the next step, that consists in moving the wolf. Suppose that +instead of specifying the next intermediate state, we prefer to specify the next +move. In the spirit of the previous example, we can do it in the following way +*) + +@(more … (move_wolf … )) + +(* The dots stand here for an arbitrary number of implicit arguments, to be +guessed by the system. +Unfortunately, the previous move is not enough to fully instantiate the new +intermediate state: a bank B remains unknown. Automation cannot help here, +since all goals depend from this bank and automation refuses to close some +subgoals instantiating other subgoals remaining open (the instantiation could +be arbitrary). The simplest way to proceed is to focus on the bank, that is +the fourth subgoal, and explicitly instatiate it. Instead of repeatedly using "|", +we can perform focusing by typing "4:" as described by the following command. *) + +[4: @east] /2/ + +(* Alternatively, we can directly instantiate the bank into the move. Let +us complete the proof in this, very readable way. *) + +@(more … (move_goat west … )) /2/ +@(more … (move_cabbage ?? east … )) /2/ +@(more … (move_boat ??? west … )) /2/ +@one /2/ qed. \ No newline at end of file diff --git a/matita/matita/lib/tutorial/chapter2.ma b/matita/matita/lib/tutorial/chapter2.ma new file mode 100644 index 000000000..04a9999a2 --- /dev/null +++ b/matita/matita/lib/tutorial/chapter2.ma @@ -0,0 +1,313 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basics/types.ma". + +(* Most of the types we have seen so far are enumerated types, composed by a +finite set of alternatives, and records, composed by tuples of heteregoneous +elements. A more interesting case of type definition is when some of the rules +defining its elements are recursive, i.e. they allow the formation of more +elements of the type in terms of the already defined ones. The most typical case +is provided by the natural numbers, that can be defined as the smallest set +generated by a constant 0 and a successor function from natural numbers to natural +numbers *) + +inductive nat : Type[0] ≝ +| O :nat +| S: nat →nat. + +(* The two terms O and S are called constructors: they define the signature of the +type, whose objects are the elements freely generated by means of them. So, +examples of natural numbers are O, S O, S (S O), S (S (S O)) and so on. + +The language of Matita allows the definition of well founded recursive functions +over inductive types; in order to guarantee termination of recursion you are only +allowed to make recursive calls on structurally smaller arguments than the ones +you received in input. Most mathematical functions can be naturally defined in this +way. For instance, the sum of two natural numbers can be defined as follows *) + +let rec add n m ≝ +match n with +[ O ⇒ m +| S a ⇒ S (add a m) +]. + +(* +Elimination + +It is worth to observe that the previous algorithm works by recursion over the +first argument. This means that, for instance, (add O x) will reduce to x, as +expected, but (add x O) is stuck. +How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do +it is called induction. The induction principle states that, given a property P(n) +over natural numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), +than we can conclude P(n) for any n. + +The elim tactic, allow you to apply induction in a very simple way. If your goal is +P(n), the invocation of + elim n +will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m). + +Let us apply it to our case *) + +lemma add_0: ∀a. add a O = a. +#a elim a + +(* If you stop the computation here, you will see on the right the two subgoals + - add O O = O + - ∀x. add x 0 = x → add (S x) O = S x +After normalization, both goals are trivial. +*) + +normalize // qed. + +(* In a similar way, it is convenient to state a lemma about the behaviour of +add when the second argument is not zero. *) + +lemma add_S : ∀a,b. add a (S b) = S (add a b). + +(* In the same way as before, we proceed by induction over a. *) + +#a #b elim a normalize // +qed. + +(* We are now in the position to prove the commutativity of the sum *) + +theorem add_comm : ∀a,b. add a b = add b a. + +#a elim a normalize + +(* We have two sub goals: + G1: ∀b. b = add b O + G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x). +G1 is just our lemma add_O. For G2, we start introducing x and the induction +hypothesis IH; then, the goal is proved by rewriting using add_S and IH. +For Matita, the task is trivial and we can simply close the goal with // *) + +// qed. + +(* COERCIONS *) + +inductive bool : Type[0] ≝ +| tt : bool +| ff : bool. + +definition nat_of_bool ≝ λb. match b with +[ tt ⇒ S O +| ff ⇒ O +]. + +(* coercion nat_of_bool. ?? *) + +(* Let us now define the following function: *) + +definition twice ≝ λn.add n n. + +(* +Existential + +We are interested to prove that for any natural number n there exists a natural +number m that is the integer half of n. This will give us the opportunity to +introduce new connectives and quantifiers and, later on, to make some interesting +consideration on proofs and computations. *) + +theorem ex_half: ∀n.∃m. n = twice m ∨ n = S (twice m). +#n elim n normalize + +(* We proceed by induction on n, that breaks down to the following goals: + G1: ∃m.O = add O O ∨ O = S (add m m) + G2: ∀x.(∃m. x = add m m ∨ x = S (add m m))→ ∃m. S x = add m m ∨ S x = S (add m m) +The only way we have to prove an existential goal is by exhibiting the witness, +that in the case of first goal is O. We do it by apply the term called ex_intro +instantiated by the witness. Then, it is clear that we must follow the left branch +of the disjunction. One way to do it is by applying the term or_introl, that is +the first constructor of the disjunction. However, remembering the names of +constructors can be annyoing: we can invoke the application of the n-th +constructor of an inductive type (inferred by the current goal) by typing %n. At +this point we are left with the subgoal O = add O O, that is closed by +computation. It is worth to observe that invoking automation at depth /3/ would +also automatically close G1. +*) + + [@(ex_intro … O) %1 // + +(* +Destructuration + +The case of G2 is more complex. We should start introducing x and the +inductive hypothesis + IH: ∃m. x = add m m ∨ x = S (add m m) +At this point we should assume the existence of m enjoying the inductive +hypothesis. To eliminate the existential from the context we can just use the +case tactic. This situation where we introduce something into the context and +immediately eliminate it by case analysis is so frequent that Matita provides a +convenient shorthand: you can just type a single "*". +The star symbol should be reminiscent of an explosion: the idea is that you have +a structured hypothesis, and you ask to explode it into its constituents. In the +case of the existential, it allows to pass from a goal of the shape + (∃x.P x) → Q +to a goal of the shape + ∀x.P x → Q +*) + |#x * +(* At this point we are left with a new goal with the following shape + G3: ∀m. x = add m m ∨ x = S (add m m) → .... +We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and +then reason by cases on this hypothesis. It is the same situation as before: +we explode the disjunctive hypothesis into its possible consituents. In the case +of a disjunction, the * tactic allows to pass from a goal of the form + A∨B → Q +to two subgoals of the form + A → Q and B → Q +*) + #m * #eqx +(* In the first subgoal, we are under the assumption that x = add m m. The half +of (S x) is hence m, and we have to prove the right branch of the disjunction. +In the second subgoal, we are under the assumption that x = S (add m m). The halh +of (S x) is hence (S m), and have to follow the left branch of the disjunction. +*) + [@(ex_intro … m) /2/ | @(ex_intro … (S m)) normalize /2/ + ] +qed. + +(* +Computing vs. Proving + +Instead of proving the existence of a number corresponding to the half of n, +we could be interested in computing it. The best way to do it is to define this +division operation together with the remainder, that in our case is just a +boolean value: tt if the input term is even, and ff if the input term is odd. +Since we must return a pair, we could use a suitably defined record type, or +simply a product type nat × bool, defined in the basic library. The product type +is just a sort of general purpose record, with standard fields fst and snd, called +projections. +A pair of values n and m is written (pair … m n) or \langle n,m \rangle - visually +rendered as 〈n,m〉 + +We first write down the function, and then discuss it.*) + +let rec div2 n ≝ +match n with +[ O ⇒ 〈O,ff〉 +| S a ⇒ + let 〈q,r〉 ≝ (div2 a) in + match r with + [ tt ⇒ 〈S q,ff〉 + | ff ⇒ 〈q, tt〉 + ] +]. + +(* The function is computed by recursion over the input n. If n is 0, then the +quotient is 0 and the remainder is tt. If n = S a, we start computing the half +of a, say 〈q,b〉. Then we have two cases according to the possible values of b: +if b is tt, then we must return 〈q,ff〉, while if b = ff then we must return +〈S q,tt〉. + +It is important to point out the deep, substantial analogy between the algorithm +for computing div2 and the the proof of ex_half. In particular ex_half returns a +proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the +witness n and a boolean indicating which one between the two conditions A(n) and +B(n) is met. This is precisely the quotient-remainder pair returned by div2. +In both cases we proceed by recurrence (respectively, induction or recursion) over +the input argument n. In case n = 0, we conclude the proof in ex_half by providing +the witness O and a proof of A(O); this corresponds to returning the pair 〈O,ff〉 in +div2. Similarly, in the inductive case n = S a, we must exploit the inductive +hypothesis for a (i.e. the result of the recursive call), distinguishing two subcases +according to the the two possibilites A(a) or B(a) (i.e. the two possibile values of +the remainder for a). The reader is strongly invited to check all remaining details. + +Let us now prove that our div2 function has the expected behaviour. +*) + +lemma surjective_pairing: ∀A,B.∀p:A×B. p = 〈fst … p,\snd … p〉. +#A #B * // qed. + +lemma div2SO: ∀n,q. div2 n = 〈q,ff〉 → div2 (S n) = 〈q,tt〉. +#n #q #H normalize >H normalize // qed. + +lemma div2S1: ∀n,q. div2 n = 〈q,tt〉 → div2 (S n) = 〈S q,ff〉. +#n #q #H normalize >H normalize // qed. + +lemma div2_ok: ∀n,q,r. div2 n = 〈q,r〉 → n = add (twice q) (nat_of_bool r). +#n elim n + [#q #r normalize #H destruct // + |#a #Hind #q #r + cut (div2 a = 〈fst … (div2 a), snd … (div2 a)〉) [//] + cases (snd … (div2 a)) + [#H >(div2S1 … H) #H1 destruct + >add_0 normalize @eq_f + cut (∀n.add (twice n) (S O) = add n (S n)) + [|#Hcut add_S // + (* >add_S whd in ⊢ (???%); (div2SO … H) #H1 destruct >add_S @eq_f @(Hind … H) + ] +qed. + +(* +Mixing proofs and computations + +There is still another possibility, however, namely to mix the program and its +specification into a single entity. The idea is to refine the output type of the +div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a +specific pair satisfying the specification of the function. In other words, we need +the possibility to define, for a type A and a property P over A, the subset type +{a:A|P(a)} of all elements a of type A that satisfy the property P. Subset types +are just a particular case of the so called dependent types, that is types that +can depend over arguments (such as arrays of a specified length, taken as a +parameter).These kind of types are quite unusual in traditional programming +languages, and their study is one of the new frontiers of the current research on +type systems. + +There is nothing special in a subset type {a:A|P(a)}: it is just a record composed +by an element of a of type A and a proof of P(a). The crucial point is to have a +language reach enough to comprise proofs among its expressions. +*) + +record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝ + {witness: A; + proof: P witness}. + +definition qr_spec ≝ λn.λp.∀q,r. p = 〈q,r〉 → n = add (twice q) (nat_of_bool r). + +(* We can now construct a function from n to {p|qr_spec n p} by composing the objects +we already have *) + +definition div2P: ∀n. Sub (nat×bool) (qr_spec n) ≝ λn. + mk_Sub ?? (div2 n) (div2_ok n). + +(* But we can also try do directly build such an object *) + +definition div2Pagain : ∀n.Sub (nat×bool) (qr_spec n). +#n elim n + [@(mk_Sub … 〈O,ff〉) normalize #q #r #H destruct // + |#a * #p #qrspec + cut (p = 〈fst … p, snd … p〉) [//] + cases (snd … p) + [#H @(mk_Sub … 〈S (fst … p),ff〉) whd #q #r #H1 destruct @eq_f >add_S + whd in ⊢ (???%); add_S @eq_f @(qrspec … H) + ] +qed. + +example full7: (div2Pagain (S(S(S(S(S(S(S O)))))))) = ?. +[normalize +// qed. + +example quotient7: witness … (div2Pagain (S(S(S(S(S(S(S O)))))))) = ?. +normalize 〈S(S(S O)),tt〉. +normalize // qed. + +example quotient8: witness … (div2Pagain (twice (twice (twice (twice (S O)))))) + = 〈twice (twice (twice (S O))), ff〉. +// qed.