Description and Verification of Pattern-Based Composition in Coq - Advances in Computational Science and Engineering - page 241

(* The composite_decorator pattern before the composition *)
Definition composite_decorator :=
closure (union composite_pattern decorator_pattern).
(* The composite_decorator' pattern after the composition *)
Definition composite_decorator' :=
closure (union composite_pattern' decorator_pattern').
Fig. 11. Defintion of patterns before and after the composition
(* This tactic takes list l1 and l2 as parameters, which means it is suitable for
any patterns, as long as they are modeled in our way---as a list of 'terms' *)
Ltac not_add_tac l1 l2 :=
(* First use the atom tactic intro provided by the Coq system. This also allows us
to use all the conditions available to the theorem. *)
intro t;
(* The atom tactic simpl automatically simplify the theorem according to the defi-
nitions in the user's environment. *)
simpl;
(* Intuition is a powerful tactic in Coq, it analyzes the current situation and provide
subgoals whenever necessary. *)
intuition;
match goal with
(* Match the form of the current goal, according our definition of Mapping func-
tions, we can automate the proof of theorem (2). *)
| [id1 : Mcmp ?x =t |- _ ] => exists x
| [id2 : Mdcr ?x=t |- _ ] => exists x
| [id3 : Mcmp_dcr ?x = t |- _ ]=> exists x
| [id4 : _ |- _ ] => auto
end;
auto.
Fig. 12. Definition of the not_add_tac tactic
After these general definitions of tactics, we are now ready for the proof of theo-
rem (2) and (3). Figure 14 and 15 are the details of the proving processes. Note in
Figure 14, theorem (2) is done with only one tactic: the not_lost_tac. We only need to
pass the correct actual parameters to the not_lose_tac tactic and then the Coq system
will automatically search the solution to the goal based on the user's definitions in the
current environment.