comparison src/Match.v @ 329:d7178fb77321

Two exercises for Match
author Adam Chlipala <adam@chlipala.net>
date Tue, 27 Sep 2011 11:39:46 -0400
parents cbeccef45f4e
children 49c6aa7d2148
comparison
equal deleted inserted replaced
328:cbeccef45f4e 329:d7178fb77321
994 Theorem t9 : exists p : nat * nat, fst p = 3. 994 Theorem t9 : exists p : nat * nat, fst p = 3.
995 econstructor; match goal with 995 econstructor; match goal with
996 | [ |- fst ?x = 3 ] => equate x (3, 2) 996 | [ |- fst ?x = 3 ] => equate x (3, 2)
997 end; reflexivity. 997 end; reflexivity.
998 Qed. 998 Qed.
999
1000
1001 (** * Exercises *)
1002
1003 (** %\begin{enumerate}%#<ol>#
1004
1005 %\item%#<li># An anonymous Coq fan from the Internet was excited to come up with this tactic definition shortly after getting started learning Ltac: *)
1006
1007 Ltac deSome :=
1008 match goal with
1009 | [ H : Some _ = Some _ |- _ ] => injection H; clear H; intros; subst; deSome
1010 | _ => reflexivity
1011 end.
1012
1013 (** Without lifting a finger, exciting theorems can be proved: *)
1014
1015 Theorem test : forall (a b c d e f g : nat),
1016 Some a = Some b
1017 -> Some b = Some c
1018 -> Some e = Some c
1019 -> Some f = Some g
1020 -> c = a.
1021 intros; deSome.
1022 Qed.
1023
1024 (** Unfortunately, this tactic exhibits some degenerate behavior. Consider the following example: *)
1025
1026 Theorem test2 : forall (a x1 y1 x2 y2 x3 y3 x4 y4 x5 y5 x6 y6 : nat),
1027 Some x1 = Some y1
1028 -> Some x2 = Some y2
1029 -> Some x3 = Some y3
1030 -> Some x4 = Some y4
1031 -> Some x5 = Some y5
1032 -> Some x6 = Some y6
1033 -> Some a = Some a
1034 -> x1 = x2.
1035 intros.
1036 Time try deSome.
1037 Abort.
1038
1039 (* begin hide *)
1040 Reset test.
1041 (* end hide *)
1042
1043 (** This (failed) proof already takes about one second on my workstation. I hope a pattern in the theorem statement is clear; this is a representative of a class of theorems, where we may add more matched pairs of [x] and [y] variables, with equality hypotheses between them. The running time of [deSome] is exponential in the number of such hypotheses.
1044
1045 The task in this exercise is twofold. First, figure out why [deSome] exhibits exponential behavior for this class of examples and record your explanation in a comment. Second, write an improved version of [deSome] that runs in polynomial time.#</li>#
1046
1047 %\item%#<li># Some theorems involving existential quantifiers are easy to prove with [eauto]. *)
1048
1049 Theorem test1 : exists x, x = 0.
1050 eauto.
1051 Qed.
1052
1053 (** Others are harder. The problem with the next theorem is that the existentially quantified variable does not appear in the rest of the theorem, so [eauto] has no way to deduce its value. However, we know that we had might as well instantiate that variable to [tt], the only value of type [unit]. *)
1054
1055 Theorem test2 : exists x : unit, 0 = 0.
1056 (* begin hide *)
1057 eauto.
1058 Abort.
1059 (* end hide *)
1060
1061 (** We also run into trouble in the next theorem, because [eauto] does not understand the [fst] and [snd] projection functions for pairs. *)
1062
1063 Theorem test3 : exists x : nat * nat, fst x = 7 /\ snd x = 2 + fst x.
1064 (* begin hide *)
1065 eauto.
1066 Abort.
1067 (* end hide *)
1068
1069 (** Both problems show up in this monster example. *)
1070
1071 Theorem test4 : exists x : (unit * nat) * (nat * bool),
1072 snd (fst x) = 7 /\ fst (snd x) = 2 + snd (fst x) /\ snd (snd x) = true.
1073 (* begin hide *)
1074 eauto.
1075 Abort.
1076 (* end hide *)
1077
1078 (** The task in this problem is to write a tactic that preprocesses such goals so that [eauto] can finish them. Your tactic should serve as a complete proof of each of the above examples, along with the wide class of similar examples. The key smarts that your tactic will bring are: first, it introduces separate unification variables for all the %``%#"#leaf types#"#%''% of compound types built out of pairs; and second, leaf unification variables of type [unit] are simply replaced by [tt].
1079
1080 A few hints: The following tactic is more convenient than direct use of the built-in tactic [evar], for generation of new unification variables: *)
1081
1082 Ltac makeEvar T k := let x := fresh in
1083 evar (x : T); let y := eval unfold x in x in clear x; k y.
1084
1085 (** remove printing exists *)
1086
1087 (** This is a continuation-passing style tactic. For instance, when the goal begins with existential quantification over a type [T], the following tactic invocation will create a new unification variable to use as the quantifier instantiation:
1088
1089 [makeEvar T ltac:(][fun x => exists x)] *)
1090
1091 (** printing exists $\exists$ *)
1092
1093 (** Recall that [exists] formulas are desugared to uses of the [ex] inductive family. In particular, a pattern like the following can be used to extract the domain of an [exists] quantifier into variable [T]:
1094
1095 [| [ |- ex ( A := ?T) _ ] => ...]
1096
1097 The [equate] tactic used as an example in this chapter will probably be useful, to unify two terms, for instance if the first is a unification variable whose value you want to set.
1098 [[
1099 Ltac equate E1 E2 := let H := fresh in
1100 assert (H : E1 = E2) by reflexivity; clear H.
1101 ]]
1102
1103 Finally, there are some minor complications surrounding overloading of the [*] operator for both numeric multiplication and Cartesian product for sets (i.e., pair types). To ensure that an Ltac pattern is using the type version, write it like this:
1104
1105 [| (?T1 * ?T2)%type => ...]
1106
1107 #</ol>#%\end{enumerate}% *)