Information Technology Reference
In-Depth Information
Other rules can easily be added to our definition ('fsttrans') by simply adding a new
clause in its definition. Using the definition of closure, we can now calculate the list
of terms before and after the mapping, the composite_decorator and the compos-
ite_decorator' respectively. See Figure 11.
4.3 Proving Correctness of the Composition
To facilitate the proof of these theorems, we also need to define some customized
tactics. These tactics allow some automation in the proving process. Tactics are pow-
erful tools in Coq, which facilitate the proving process of the user. There is a language
for the definition of tactics in Coq. In the proofs-as-programs diagram, this language
is rather for the user to write down the proving process for their specific problems. In
our case, we should use this language to automate most of the task involved in prov-
ing the Theorems.
We now define the tactic not_add_tac for the proof of theorem (2) and not_lost_tac
for the proof of theorem (3). See Figure 12 and 13 for the definition of these tactics.
(* Define a function which calculate the transitive clouse of term t in list l *)
Fixpoint fsttrans (t:term) (l : list term) {struct l} : list term :=
match l with
(* if l is nil, return null *)
| nil => nil
| a::l' =>
(* match t and the first element in list l,if a and t can trigger the rule in (4), then
and the derived term the the resulting list *)
match a, t with
| Inherit f1 f2, Inherit s2 s3 =>
if ceqbool f2 s2 then Inherit f1 s3::(fsttrans t l') else
if ceqbool s3 f1 then Inherit s2 f2::(fsttrans t l') else
fsttrans t l'
(* if rule (4) cannot be applied, then check the next element in list l. *)
| _ , _ => fsttrans t l'
end
end.
(* Based on the definition of fsttrans, inductively calculate the deductive clouse of
list l. *)
Fixpoint closure (l :list term) { struct l } : list term:=
match l with
| nil => nil
| a::l' =>a::(fsttrans a l')++(closure l')
end.
Fig. 10. Definition of Closure
Search WWH ::




Custom Search