AltAutoA Streamlined Treatment of Automation
- tacticals, which allow tactics to be combined;
- new tactics that make dealing with hypothesis names less fussy
and more maintainable;
- automatic solvers that can prove limited classes of theorems
without any human assistance;
- proof search with the auto tactic; and
- the Ltac language for writing tactics.
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality,-deprecated-syntactic-definition,-deprecated]".
From Coq Require Import Arith List.
From LF Require Import IndProp.
From Coq Require Import Arith List.
From LF Require Import IndProp.
As a simple illustration of the benefits of automation,
let's consider another problem on regular expressions, which we
formalized in IndProp. A given set of strings can be
denoted by many different regular expressions. For example, App
EmptyString re matches exactly the same strings as re. We can
write a function that "optimizes" any regular expression into a
potentially simpler one by applying this fact throughout the r.e.
(Note that, for simplicity, the function does not optimize
expressions that arise as the result of other optimizations.)
Fixpoint re_opt_e {T:Type} (re: reg_exp T) : reg_exp T :=
match re with
| App EmptyStr re2 ⇒ re_opt_e re2
| App re1 re2 ⇒ App (re_opt_e re1) (re_opt_e re2)
| Union re1 re2 ⇒ Union (re_opt_e re1) (re_opt_e re2)
| Star re ⇒ Star (re_opt_e re)
| _ ⇒ re
end.
match re with
| App EmptyStr re2 ⇒ re_opt_e re2
| App re1 re2 ⇒ App (re_opt_e re1) (re_opt_e re2)
| Union re1 re2 ⇒ Union (re_opt_e re1) (re_opt_e re2)
| Star re ⇒ Star (re_opt_e re)
| _ ⇒ re
end.
We would like to show the equivalence of re's with their
"optimized" form. One direction of this equivalence looks like
this (the other is similar).
Lemma re_opt_e_match : ∀ T (re: reg_exp T) s,
s =~ re → s =~ re_opt_e re.
Proof.
intros T re s M.
induction M
as [| x'
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
- (* MEmpty *) simpl. apply MEmpty.
- (* MChar *) simpl. apply MChar.
- (* MApp *) simpl.
destruct re1.
+ apply MApp.
× apply IH1.
× apply IH2.
+ inversion Hmatch1. simpl. apply IH2.
+ apply MApp.
× apply IH1.
× apply IH2.
+ apply MApp.
× apply IH1.
× apply IH2.
+ apply MApp.
× apply IH1.
× apply IH2.
+ apply MApp.
× apply IH1.
× apply IH2.
- (* MUnionL *) simpl. apply MUnionL. apply IH.
- (* MUnionR *) simpl. apply MUnionR. apply IH.
- (* MStar0 *) simpl. apply MStar0.
- (* MStarApp *) simpl. apply MStarApp.
× apply IH1.
× apply IH2.
Qed.
s =~ re → s =~ re_opt_e re.
Proof.
intros T re s M.
induction M
as [| x'
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
- (* MEmpty *) simpl. apply MEmpty.
- (* MChar *) simpl. apply MChar.
- (* MApp *) simpl.
destruct re1.
+ apply MApp.
× apply IH1.
× apply IH2.
+ inversion Hmatch1. simpl. apply IH2.
+ apply MApp.
× apply IH1.
× apply IH2.
+ apply MApp.
× apply IH1.
× apply IH2.
+ apply MApp.
× apply IH1.
× apply IH2.
+ apply MApp.
× apply IH1.
× apply IH2.
- (* MUnionL *) simpl. apply MUnionL. apply IH.
- (* MUnionR *) simpl. apply MUnionR. apply IH.
- (* MStar0 *) simpl. apply MStar0.
- (* MStarApp *) simpl. apply MStarApp.
× apply IH1.
× apply IH2.
Qed.
The amount of repetition in that proof is annoying. And if
we wanted to extend the optimization function to handle other,
similar, rewriting opportunities, it would start to be a real
problem. We can streamline the proof with tacticals, which we
turn to, next.
Tacticals
The try Tactical
Theorem silly1 : ∀ n, 1 + n = S n.
Proof. try reflexivity. (* this just does reflexivity *) Qed.
Theorem silly2 : ∀ (P : Prop), P → P.
Proof.
intros P HP.
Fail reflexivity.
try reflexivity. (* proof state is unchanged *)
apply HP.
Qed.
Proof. try reflexivity. (* this just does reflexivity *) Qed.
Theorem silly2 : ∀ (P : Prop), P → P.
Proof.
intros P HP.
Fail reflexivity.
try reflexivity. (* proof state is unchanged *)
apply HP.
Qed.
There is no real reason to use try in completely manual
proofs like these, but it is very useful for doing automated
proofs in conjunction with the ; tactical, which we show
next.
The Sequence Tactical ; (Simple Form)
Lemma simple_semi : ∀ n, (n + 1 =? 0) = false.
Proof.
intros n.
destruct n eqn:E.
(* Leaves two subgoals, which are discharged identically... *)
- (* n=0 *) simpl. reflexivity.
- (* n=Sn' *) simpl. reflexivity.
Qed.
Proof.
intros n.
destruct n eqn:E.
(* Leaves two subgoals, which are discharged identically... *)
- (* n=0 *) simpl. reflexivity.
- (* n=Sn' *) simpl. reflexivity.
Qed.
We can simplify this proof using the ; tactical:
Lemma simple_semi' : ∀ n, (n + 1 =? 0) = false.
Proof.
intros n.
(* destruct the current goal *)
destruct n;
(* then simpl each resulting subgoal *)
simpl;
(* and do reflexivity on each resulting subgoal *)
reflexivity.
Qed.
Proof.
intros n.
(* destruct the current goal *)
destruct n;
(* then simpl each resulting subgoal *)
simpl;
(* and do reflexivity on each resulting subgoal *)
reflexivity.
Qed.
Or even more tersely, destruct can do the intro, and simpl
can be omitted:
Exercise: 3 stars, standard (try_sequence)
Theorem andb_eq_orb :
∀ (b c : bool),
(andb b c = orb b c) →
b = c.
Proof. (* FILL IN HERE *) Admitted.
Theorem add_assoc : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof. (* FILL IN HERE *) Admitted.
Fixpoint nonzeros (lst : list nat) :=
match lst with
| [] ⇒ []
| 0 :: t ⇒ nonzeros t
| h :: t ⇒ h :: nonzeros t
end.
Lemma nonzeros_app : ∀ lst1 lst2 : list nat,
nonzeros (lst1 ++ lst2) = (nonzeros lst1) ++ (nonzeros lst2).
Proof. (* FILL IN HERE *) Admitted.
☐
∀ (b c : bool),
(andb b c = orb b c) →
b = c.
Proof. (* FILL IN HERE *) Admitted.
Theorem add_assoc : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof. (* FILL IN HERE *) Admitted.
Fixpoint nonzeros (lst : list nat) :=
match lst with
| [] ⇒ []
| 0 :: t ⇒ nonzeros t
| h :: t ⇒ h :: nonzeros t
end.
Lemma nonzeros_app : ∀ lst1 lst2 : list nat,
nonzeros (lst1 ++ lst2) = (nonzeros lst1) ++ (nonzeros lst2).
Proof. (* FILL IN HERE *) Admitted.
☐
Lemma re_opt_e_match' : ∀ T (re: reg_exp T) s,
s =~ re → s =~ re_opt_e re.
Proof.
intros T re s M.
induction M
as [| x'
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2];
(* Do the simpl for every case here: *)
simpl.
- (* MEmpty *) apply MEmpty.
- (* MChar *) apply MChar.
- (* MApp *)
destruct re1;
(* Most cases follow by the same formula. Notice that apply MApp gives two subgoals: try apply IH1 is run on _both_ of
them and succeeds on the first but not the second; apply IH2
is then run on this remaining goal. *)
try (apply MApp; try apply IH1; apply IH2).
(* The interesting case, on which try... does nothing, is when
re1 = EmptyStr. In this case, we have to appeal to the fact
that re1 matches only the empty string: *)
inversion Hmatch1. simpl. apply IH2.
- (* MUnionL *) apply MUnionL. apply IH.
- (* MUnionR *) apply MUnionR. apply IH.
- (* MStar0 *) apply MStar0.
- (* MStarApp *) apply MStarApp. apply IH1. apply IH2.
Qed.
s =~ re → s =~ re_opt_e re.
Proof.
intros T re s M.
induction M
as [| x'
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2];
(* Do the simpl for every case here: *)
simpl.
- (* MEmpty *) apply MEmpty.
- (* MChar *) apply MChar.
- (* MApp *)
destruct re1;
(* Most cases follow by the same formula. Notice that apply MApp gives two subgoals: try apply IH1 is run on _both_ of
them and succeeds on the first but not the second; apply IH2
is then run on this remaining goal. *)
try (apply MApp; try apply IH1; apply IH2).
(* The interesting case, on which try... does nothing, is when
re1 = EmptyStr. In this case, we have to appeal to the fact
that re1 matches only the empty string: *)
inversion Hmatch1. simpl. apply IH2.
- (* MUnionL *) apply MUnionL. apply IH.
- (* MUnionR *) apply MUnionR. apply IH.
- (* MStar0 *) apply MStar0.
- (* MStarApp *) apply MStarApp. apply IH1. apply IH2.
Qed.
The Sequence Tactical ; (Local Form)
T; [T' | T' | ... | T']
Theorem app_length : ∀ (X : Type) (lst1 lst2 : list X),
length (lst1 ++ lst2) = (length lst1) + (length lst2).
Proof.
intros; induction lst1;
[reflexivity | simpl; rewrite IHlst1; reflexivity].
Qed.
length (lst1 ++ lst2) = (length lst1) + (length lst2).
Proof.
intros; induction lst1;
[reflexivity | simpl; rewrite IHlst1; reflexivity].
Qed.
The identity tactic idtac always succeeds without changing the
proof state. We can use it to factor out reflexivity in the
previous proof.
Theorem app_length' : ∀ (X : Type) (lst1 lst2 : list X),
length (lst1 ++ lst2) = (length lst1) + (length lst2).
Proof.
intros; induction lst1;
[idtac | simpl; rewrite IHlst1];
reflexivity.
Qed.
length (lst1 ++ lst2) = (length lst1) + (length lst2).
Proof.
intros; induction lst1;
[idtac | simpl; rewrite IHlst1];
reflexivity.
Qed.
Exercise: 1 star, standard (notry_sequence)
Theorem add_assoc' : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof. (* FILL IN HERE *) Admitted.
☐
n + (m + p) = (n + m) + p.
Proof. (* FILL IN HERE *) Admitted.
☐
Lemma re_opt_e_match'' : ∀ T (re: reg_exp T) s,
s =~ re → s =~ re_opt_e re.
Proof.
intros T re s M.
induction M
as [| x'
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2];
(* Do the simpl for every case here: *)
simpl.
- (* MEmpty *) apply MEmpty.
- (* MChar *) apply MChar.
- (* MApp *)
destruct re1;
try (apply MApp; [apply IH1 | apply IH2]). (* <=== *)
inversion Hmatch1. simpl. apply IH2.
- (* MUnionL *) apply MUnionL. apply IH.
- (* MUnionR *) apply MUnionR. apply IH.
- (* MStar0 *) apply MStar0.
- (* MStarApp *) apply MStarApp; [apply IH1 | apply IH2]. (* <=== *)
Qed.
s =~ re → s =~ re_opt_e re.
Proof.
intros T re s M.
induction M
as [| x'
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2];
(* Do the simpl for every case here: *)
simpl.
- (* MEmpty *) apply MEmpty.
- (* MChar *) apply MChar.
- (* MApp *)
destruct re1;
try (apply MApp; [apply IH1 | apply IH2]). (* <=== *)
inversion Hmatch1. simpl. apply IH2.
- (* MUnionL *) apply MUnionL. apply IH.
- (* MUnionR *) apply MUnionR. apply IH.
- (* MStar0 *) apply MStar0.
- (* MStarApp *) apply MStarApp; [apply IH1 | apply IH2]. (* <=== *)
Qed.
The repeat Tactical
The tactic repeat T never fails: if the tactic T doesn't apply
to the original goal, then repeat still succeeds without
changing the original goal (i.e., it repeats zero times).
Theorem In10' : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
repeat (left; reflexivity).
repeat (right; try (left; reflexivity)).
Qed.
Proof.
repeat (left; reflexivity).
repeat (right; try (left; reflexivity)).
Qed.
The tactic repeat T also does not have any upper bound on the
number of times it applies T. If T is a tactic that always
succeeds, then repeat T will loop forever (e.g., repeat simpl
loops, since simpl always succeeds). Evaluation in Coq's term
language, Gallina, is guaranteed to terminate, but tactic
evaluation is not. This does not affect Coq's logical consistency,
however, since the job of repeat and other tactics is to guide
Coq in constructing proofs. If the construction process diverges,
it simply means that we have failed to construct a proof, not that
we have constructed an incorrect proof.
Exercise: 1 star, standard (ev100)
Prove that 100 is even. Your proof script should be quite short.An Optimization Exercise
Exercise: 4 stars, standard (re_opt)
Fixpoint re_opt {T:Type} (re: reg_exp T) : reg_exp T :=
match re with
| App _ EmptySet ⇒ EmptySet
| App EmptyStr re2 ⇒ re_opt re2
| App re1 EmptyStr ⇒ re_opt re1
| App re1 re2 ⇒ App (re_opt re1) (re_opt re2)
| Union EmptySet re2 ⇒ re_opt re2
| Union re1 EmptySet ⇒ re_opt re1
| Union re1 re2 ⇒ Union (re_opt re1) (re_opt re2)
| Star EmptySet ⇒ EmptyStr
| Star EmptyStr ⇒ EmptyStr
| Star re ⇒ Star (re_opt re)
| EmptySet ⇒ EmptySet
| EmptyStr ⇒ EmptyStr
| Char x ⇒ Char x
end.
(* Here is an incredibly tedious manual proof of (one direction of)
its correctness: *)
Lemma re_opt_match : ∀ T (re: reg_exp T) s,
s =~ re → s =~ re_opt re.
(* Use the tacticals described so far to shorten the proof. The proof
above is about 200 lines. Reduce it to 50 or fewer lines of similar
density. Solve each of the seven top-level bullets with a one-shot
proof.
Hint: use a bottom-up approach. First copy-paste the entire proof
below. Then automate the innermost bullets first, proceeding
outwards. Frequently double-check that the entire proof still
compiles. If it doesn't, undo the most recent changes you made
until you get back to a compiling proof. *)
Lemma re_opt_match' : ∀ T (re: reg_exp T) s,
s =~ re → s =~ re_opt re.
Proof.
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_re_opt : option (nat×string) := None.
☐
match re with
| App _ EmptySet ⇒ EmptySet
| App EmptyStr re2 ⇒ re_opt re2
| App re1 EmptyStr ⇒ re_opt re1
| App re1 re2 ⇒ App (re_opt re1) (re_opt re2)
| Union EmptySet re2 ⇒ re_opt re2
| Union re1 EmptySet ⇒ re_opt re1
| Union re1 re2 ⇒ Union (re_opt re1) (re_opt re2)
| Star EmptySet ⇒ EmptyStr
| Star EmptyStr ⇒ EmptyStr
| Star re ⇒ Star (re_opt re)
| EmptySet ⇒ EmptySet
| EmptyStr ⇒ EmptyStr
| Char x ⇒ Char x
end.
(* Here is an incredibly tedious manual proof of (one direction of)
its correctness: *)
Lemma re_opt_match : ∀ T (re: reg_exp T) s,
s =~ re → s =~ re_opt re.
Proof.
intros T re s M.
induction M
as [| x'
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
- (* MEmpty *) simpl. apply MEmpty.
- (* MChar *) simpl. apply MChar.
- (* MApp *) simpl.
destruct re1.
+ inversion IH1.
+ inversion IH1. simpl. destruct re2.
× apply IH2.
× apply IH2.
× apply IH2.
× apply IH2.
× apply IH2.
× apply IH2.
+ destruct re2.
× inversion IH2.
× inversion IH2. rewrite app_nil_r. apply IH1.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
+ destruct re2.
× inversion IH2.
× inversion IH2. rewrite app_nil_r. apply IH1.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
+ destruct re2.
× inversion IH2.
× inversion IH2. rewrite app_nil_r. apply IH1.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
+ destruct re2.
× inversion IH2.
× inversion IH2. rewrite app_nil_r. apply IH1.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
- (* MUnionL *) simpl.
destruct re1.
+ inversion IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
- (* MUnionR *) simpl.
destruct re1.
+ apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
- (* MStar0 *) simpl.
destruct re.
+ apply MEmpty.
+ apply MEmpty.
+ apply MStar0.
+ apply MStar0.
+ apply MStar0.
+ simpl.
destruct re.
× apply MStar0.
× apply MStar0.
× apply MStar0.
× apply MStar0.
× apply MStar0.
× apply MStar0.
- (* MStarApp *) simpl.
destruct re.
+ inversion IH1.
+ inversion IH1. inversion IH2. apply MEmpty.
+ apply star_app.
× apply MStar1. apply IH1.
× apply IH2.
+ apply star_app.
× apply MStar1. apply IH1.
× apply IH2.
+ apply star_app.
× apply MStar1. apply IH1.
× apply IH2.
+ apply star_app.
× apply MStar1. apply IH1.
× apply IH2.
Qed.
intros T re s M.
induction M
as [| x'
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
- (* MEmpty *) simpl. apply MEmpty.
- (* MChar *) simpl. apply MChar.
- (* MApp *) simpl.
destruct re1.
+ inversion IH1.
+ inversion IH1. simpl. destruct re2.
× apply IH2.
× apply IH2.
× apply IH2.
× apply IH2.
× apply IH2.
× apply IH2.
+ destruct re2.
× inversion IH2.
× inversion IH2. rewrite app_nil_r. apply IH1.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
+ destruct re2.
× inversion IH2.
× inversion IH2. rewrite app_nil_r. apply IH1.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
+ destruct re2.
× inversion IH2.
× inversion IH2. rewrite app_nil_r. apply IH1.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
+ destruct re2.
× inversion IH2.
× inversion IH2. rewrite app_nil_r. apply IH1.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
× apply MApp.
-- apply IH1.
-- apply IH2.
- (* MUnionL *) simpl.
destruct re1.
+ inversion IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
+ destruct re2.
× apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
× apply MUnionL. apply IH.
- (* MUnionR *) simpl.
destruct re1.
+ apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
+ destruct re2.
× inversion IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
× apply MUnionR. apply IH.
- (* MStar0 *) simpl.
destruct re.
+ apply MEmpty.
+ apply MEmpty.
+ apply MStar0.
+ apply MStar0.
+ apply MStar0.
+ simpl.
destruct re.
× apply MStar0.
× apply MStar0.
× apply MStar0.
× apply MStar0.
× apply MStar0.
× apply MStar0.
- (* MStarApp *) simpl.
destruct re.
+ inversion IH1.
+ inversion IH1. inversion IH2. apply MEmpty.
+ apply star_app.
× apply MStar1. apply IH1.
× apply IH2.
+ apply star_app.
× apply MStar1. apply IH1.
× apply IH2.
+ apply star_app.
× apply MStar1. apply IH1.
× apply IH2.
+ apply star_app.
× apply MStar1. apply IH1.
× apply IH2.
Qed.
(* Use the tacticals described so far to shorten the proof. The proof
above is about 200 lines. Reduce it to 50 or fewer lines of similar
density. Solve each of the seven top-level bullets with a one-shot
proof.
Hint: use a bottom-up approach. First copy-paste the entire proof
below. Then automate the innermost bullets first, proceeding
outwards. Frequently double-check that the entire proof still
compiles. If it doesn't, undo the most recent changes you made
until you get back to a compiling proof. *)
Lemma re_opt_match' : ∀ T (re: reg_exp T) s,
s =~ re → s =~ re_opt re.
Proof.
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_re_opt : option (nat×string) := None.
☐
Tactics that Make Mentioning Names Unnecessary
We took the trouble to invent a name for HP, then we had
to remember that name. If we later change the name in one place,
we have to change it everywhere. Likewise, if we were to add new
arguments to the theorem, we would have to adjust the intros
list. That makes it challenging to maintain large proofs. So, Coq
provides several tactics that make it possible to write proof
scripts that do not hardcode names.
The assumption tactic
Some might argue to the contrary that hypothesis names
improve self-documention of proof scripts. Maybe they do,
sometimes. But in the case of the two proofs above, the first
mentions unnecessary detail, whereas the second could be
paraphrased simply as "the conclusion follows from the
assumptions."
Anyway, unlike informal (good) mathematical proofs, Coq proof
scripts are generally not that illuminating to readers. Worries
about rich, self-documenting names for hypotheses might be
misplaced.
The contradiction tactic
Theorem false_assumed : False → 0 = 1.
Proof.
intros H. destruct H.
Qed.
Theorem false_assumed' : False → 0 = 1.
Proof.
intros. contradiction.
Qed.
Theorem contras : ∀ (P : Prop), P → ¬P → 0 = 1.
Proof.
intros P HP HNP. exfalso. apply HNP. apply HP.
Qed.
Theorem contras' : ∀ (P : Prop), P → ¬P → 0 = 1.
Proof.
intros. contradiction.
Qed.
Proof.
intros H. destruct H.
Qed.
Theorem false_assumed' : False → 0 = 1.
Proof.
intros. contradiction.
Qed.
Theorem contras : ∀ (P : Prop), P → ¬P → 0 = 1.
Proof.
intros P HP HNP. exfalso. apply HNP. apply HP.
Qed.
Theorem contras' : ∀ (P : Prop), P → ¬P → 0 = 1.
Proof.
intros. contradiction.
Qed.
The subst tactic
Theorem many_eq : ∀ (n m o p : nat),
n = m →
o = p →
[n; o] = [m; p].
Proof.
intros n m o p Hnm Hop. rewrite Hnm. rewrite Hop. reflexivity.
Qed.
Theorem many_eq' : ∀ (n m o p : nat),
n = m →
o = p →
[n; o] = [m; p].
Proof.
intros. subst. reflexivity.
Qed.
n = m →
o = p →
[n; o] = [m; p].
Proof.
intros n m o p Hnm Hop. rewrite Hnm. rewrite Hop. reflexivity.
Qed.
Theorem many_eq' : ∀ (n m o p : nat),
n = m →
o = p →
[n; o] = [m; p].
Proof.
intros. subst. reflexivity.
Qed.
Actually there are two forms of this tactic.
- subst x finds an assumption x = e or e = x in the
context, replaces x with e throughout the context and
current goal, and removes the assumption from the context.
- subst substitutes away all assumptions of the form x = e or e = x.
The constructor tactic
Check ev_0 : ev 0.
Check ev_SS : ∀ n : nat, ev n → ev (S (S n)).
Example constructor_example: ∀ (n:nat),
ev (n + n).
Proof.
induction n; simpl.
- constructor. (* applies ev_0 *)
- rewrite add_comm. simpl. constructor. (* applies ev_SS *)
assumption.
Qed.
Check ev_SS : ∀ n : nat, ev n → ev (S (S n)).
Example constructor_example: ∀ (n:nat),
ev (n + n).
Proof.
induction n; simpl.
- constructor. (* applies ev_0 *)
- rewrite add_comm. simpl. constructor. (* applies ev_SS *)
assumption.
Qed.
Warning: if more than one constructor can apply,
constructor picks the first one, in the order in which they were
defined in the Inductive definition. That might not be the one
you want.
Automatic Solvers
Linear Integer Arithmetic: The lia Tactic
- variables and constants of type nat, Z, and other integer
types;
- arithmetic operators +, -, ×, and ^;
- equality = and ordering <, >, ≤, ≥; and
- the logical connectives ∧, ∨, ¬, →, and ↔; and constants True and False.
- For linear goals, lia will either solve the goal or fail,
meaning that the goal is actually invalid.
- For non-linear goals, lia will also either solve the goal or fail. But in this case, the failure does not necessarily mean that the goal is invalid -- it might just be beyond lia's reach to prove because of non-linearity.
From Coq Require Import Lia.
Theorem lia_succeed1 : ∀ (n : nat),
n > 0 → n × 2 > n.
Proof. lia. Qed.
Theorem lia_succeed2 : ∀ (n m : nat),
n × m = m × n.
Proof.
lia. (* solvable though non-linear *)
Qed.
Theorem lia_fail1 : 0 = 1.
Proof.
Fail lia. (* goal is invalid *)
Abort.
Theorem lia_fail2 : ∀ (n : nat),
n ≥ 1 → 2 ^ n = 2 × 2 ^ (n - 1).
Proof.
Fail lia. (*goal is non-linear, valid, but unsolvable by lia *)
Abort.
Theorem lia_succeed1 : ∀ (n : nat),
n > 0 → n × 2 > n.
Proof. lia. Qed.
Theorem lia_succeed2 : ∀ (n m : nat),
n × m = m × n.
Proof.
lia. (* solvable though non-linear *)
Qed.
Theorem lia_fail1 : 0 = 1.
Proof.
Fail lia. (* goal is invalid *)
Abort.
Theorem lia_fail2 : ∀ (n : nat),
n ≥ 1 → 2 ^ n = 2 × 2 ^ (n - 1).
Proof.
Fail lia. (*goal is non-linear, valid, but unsolvable by lia *)
Abort.
There are other tactics that can solve arithmetic goals. The
ring and field tactics, for example, can solve equations over
the algebraic structures of rings and fields, from which the
tactics get their names. These tactics do not do intros.
Require Import Ring.
Theorem mult_comm : ∀ (n m : nat),
n × m = m × n.
Proof.
intros n m. ring.
Qed.
Theorem mult_comm : ∀ (n m : nat),
n × m = m × n.
Proof.
intros n m. ring.
Qed.
Equalities: The congruence Tactic
Theorem eq_example1 :
∀ (A B C : Type) (f : A → B) (g : B → C) (x : A) (y : B),
y = f x → g y = g (f x).
Proof.
intros. rewrite H. reflexivity.
Qed.
∀ (A B C : Type) (f : A → B) (g : B → C) (x : A) (y : B),
y = f x → g y = g (f x).
Proof.
intros. rewrite H. reflexivity.
Qed.
The essential properties of equality are that it is:
It is that congruence property that we're using when we
rewrite in the proof above: if a = b then f a = f b. (The
ProofObjects chapter explores this idea further under the
name "Leibniz equality".)
The congruence tactic is a decision procedure for equality with
uninterpreted functions and other symbols.
- reflexive
- symmetric
- transitive
- a congruence: it respects function and predicate application.
Theorem eq_example1' :
∀ (A B C : Type) (f : A → B) (g : B → C) (x : A) (y : B),
y = f x → g y = g (f x).
Proof.
congruence.
Qed.
∀ (A B C : Type) (f : A → B) (g : B → C) (x : A) (y : B),
y = f x → g y = g (f x).
Proof.
congruence.
Qed.
The congruence tactic is able to work with constructors,
even taking advantage of their injectivity and distinctness.
Theorem eq_example2 : ∀ (n m o p : nat),
n = m →
o = p →
(n, o) = (m, p).
Proof.
congruence.
Qed.
Theorem eq_example3 : ∀ (X : Type) (h : X) (t : list X),
[] ≠ h :: t.
Proof.
congruence.
Qed.
n = m →
o = p →
(n, o) = (m, p).
Proof.
congruence.
Qed.
Theorem eq_example3 : ∀ (X : Type) (h : X) (t : list X),
[] ≠ h :: t.
Proof.
congruence.
Qed.
Propositions: The intuition Tactic
Theorem intuition_succeed1 : ∀ (P : Prop),
P → P.
Proof. intuition. Qed.
Theorem intuition_succeed2 : ∀ (P Q : Prop),
¬ (P ∨ Q) → ¬P ∧ ¬Q.
Proof. intuition. Qed.
Theorem intuition_simplify1 : ∀ (P : Prop),
~~P → P.
Proof.
intuition. (* not a constructively valid formula *)
Abort.
Theorem intuition_simplify2 : ∀ (x y : nat) (P Q : nat → Prop),
x = y ∧ (P x → Q x) ∧ P x → Q y.
Proof.
Fail congruence. (* the propositions stump it *)
intuition. (* the = stumps it, but it simplifies the propositions *)
congruence.
Qed.
P → P.
Proof. intuition. Qed.
Theorem intuition_succeed2 : ∀ (P Q : Prop),
¬ (P ∨ Q) → ¬P ∧ ¬Q.
Proof. intuition. Qed.
Theorem intuition_simplify1 : ∀ (P : Prop),
~~P → P.
Proof.
intuition. (* not a constructively valid formula *)
Abort.
Theorem intuition_simplify2 : ∀ (x y : nat) (P Q : nat → Prop),
x = y ∧ (P x → Q x) ∧ P x → Q y.
Proof.
Fail congruence. (* the propositions stump it *)
intuition. (* the = stumps it, but it simplifies the propositions *)
congruence.
Qed.
In the previous example, neither congruence nor
intuition alone can solve the goal. But after intuition
simplifies the propositions involved in the goal, congruence can
succeed. For situations like this, intuition takes an optional
argument, which is a tactic to apply to all the unsolved goals
that intuition generated. Using that we can offer a shorter
proof:
Theorem intuition_simplify2' : ∀ (x y : nat) (P Q : nat → Prop),
x = y ∧ (P x → Q x) ∧ P x → Q y.
Proof.
intuition congruence.
Qed.
x = y ∧ (P x → Q x) ∧ P x → Q y.
Proof.
intuition congruence.
Qed.
Exercises with Automatic Solvers
Exercise: 2 stars, standard (automatic_solvers)
The exercises below are gleaned from previous chapters, where they were proved with (relatively) long proof scripts. Each should now be provable with just a single invocation of an automatic solver.
Theorem plus_id_exercise_from_basics : ∀ n m o : nat,
n = m → m = o → n + m = m + o.
Proof. (* FILL IN HERE *) Admitted.
Theorem add_assoc_from_induction : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof. (* FILL IN HERE *) Admitted.
Theorem S_injective_from_tactics : ∀ (n m : nat),
S n = S m →
n = m.
Proof. (* FILL IN HERE *) Admitted.
Theorem or_distributes_over_and_from_logic : ∀ P Q R : Prop,
P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R).
Proof. (* FILL IN HERE *) Admitted.
☐
n = m → m = o → n + m = m + o.
Proof. (* FILL IN HERE *) Admitted.
Theorem add_assoc_from_induction : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof. (* FILL IN HERE *) Admitted.
Theorem S_injective_from_tactics : ∀ (n m : nat),
S n = S m →
n = m.
Proof. (* FILL IN HERE *) Admitted.
Theorem or_distributes_over_and_from_logic : ∀ P Q R : Prop,
P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R).
Proof. (* FILL IN HERE *) Admitted.
☐
Search Tactics
The auto Tactic
Example auto_example_1 : ∀ (P Q R: Prop),
(P → Q) → (Q → R) → P → R.
Proof.
intros P Q R H1 H2 H3.
apply H2. apply H1. apply H3.
Qed.
(P → Q) → (Q → R) → P → R.
Proof.
intros P Q R H1 H2 H3.
apply H2. apply H1. apply H3.
Qed.
The auto tactic frees us from this drudgery by searching for a
sequence of applications that will prove the goal:
The auto tactic solves goals that are solvable by any combination of
Using auto is always "safe" in the sense that it will
never fail and will never change the proof state: either it
completely solves the current goal, or it does nothing.
Here is a more interesting example showing auto's power:
- intros and
- apply (of hypotheses from the local context, by default).
Example auto_example_2 : ∀ P Q R S T U : Prop,
(P → Q) →
(P → R) →
(T → R) →
(S → T → U) →
((P → Q) → (P → S)) →
T →
P →
U.
Proof. auto. Qed.
(P → Q) →
(P → R) →
(T → R) →
(S → T → U) →
((P → Q) → (P → S)) →
T →
P →
U.
Proof. auto. Qed.
Proof search could, in principle, take an arbitrarily long time,
so there are limits to how far auto will search by default.
Example auto_example_3 : ∀ (P Q R S T U: Prop),
(P → Q) →
(Q → R) →
(R → S) →
(S → T) →
(T → U) →
P →
U.
Proof.
(* When it cannot solve the goal, auto does nothing *)
auto.
(* Optional argument says how deep to search (default is 5) *)
auto 6.
Qed.
(P → Q) →
(Q → R) →
(R → S) →
(S → T) →
(T → U) →
P →
U.
Proof.
(* When it cannot solve the goal, auto does nothing *)
auto.
(* Optional argument says how deep to search (default is 5) *)
auto 6.
Qed.
The auto tactic considers the hypotheses in the current context
together with a hint database of other lemmas and constructors.
Some common facts about equality and logical operators are
installed in the hint database by default.
If we want to see which facts auto is using, we can use
info_auto instead.
Example auto_example_5 : 2 = 2.
Proof.
(* auto subsumes reflexivity because eq_refl is in the hint
database. *)
info_auto.
Qed.
Proof.
(* auto subsumes reflexivity because eq_refl is in the hint
database. *)
info_auto.
Qed.
We can extend the hint database with theorem t just for the
purposes of one application of auto by writing auto using
t.
Lemma le_antisym : ∀ n m: nat, (n ≤ m ∧ m ≤ n) → n = m.
Proof. intros. lia. Qed.
Example auto_example_6 : ∀ n m p : nat,
(n ≤ p → (n ≤ m ∧ m ≤ n)) →
n ≤ p →
n = m.
Proof.
auto using le_antisym.
Qed.
Proof. intros. lia. Qed.
Example auto_example_6 : ∀ n m p : nat,
(n ≤ p → (n ≤ m ∧ m ≤ n)) →
n ≤ p →
n = m.
Proof.
auto using le_antisym.
Qed.
Of course, in any given development there will probably be
some specific constructors and lemmas that are used very often in
proofs. We can add these to a hint database named db by writing
Create HintDb db. to create the database, then
Hint Resolve T : db. to add T to the database, where T is a top-level theorem or a constructor of an inductively defined proposition (i.e., anything whose type is an implication). We tell auto to use that database by writing auto with db. Technically creation of the database is optional; Coq will create it automatically the first time we use Hint.
Create HintDb db. to create the database, then
Hint Resolve T : db. to add T to the database, where T is a top-level theorem or a constructor of an inductively defined proposition (i.e., anything whose type is an implication). We tell auto to use that database by writing auto with db. Technically creation of the database is optional; Coq will create it automatically the first time we use Hint.
Create HintDb le_db.
Hint Resolve le_antisym : le_db.
Example auto_example_6' : ∀ n m p : nat,
(n ≤ p → (n ≤ m ∧ m ≤ n)) →
n ≤ p →
n = m.
Proof.
auto with le_db.
Qed.
Hint Resolve le_antisym : le_db.
Example auto_example_6' : ∀ n m p : nat,
(n ≤ p → (n ≤ m ∧ m ≤ n)) →
n ≤ p →
n = m.
Proof.
auto with le_db.
Qed.
As a shorthand, we can write
Hint Constructors c : db. to tell Coq to do a Hint Resolve for all of the constructors from the inductive definition of c.
It is also sometimes necessary to add
Hint Unfold d : db. where d is a defined symbol, so that auto knows to expand uses of d, thus enabling further possibilities for applying lemmas that it knows about.
Hint Constructors c : db. to tell Coq to do a Hint Resolve for all of the constructors from the inductive definition of c.
Hint Unfold d : db. where d is a defined symbol, so that auto knows to expand uses of d, thus enabling further possibilities for applying lemmas that it knows about.
Definition is_fortytwo x := (x = 42).
Example auto_example_7: ∀ x,
(x ≤ 42 ∧ 42 ≤ x) → is_fortytwo x.
Proof.
auto. (* does nothing *)
Abort.
Hint Unfold is_fortytwo : le_db.
Example auto_example_7' : ∀ x,
(x ≤ 42 ∧ 42 ≤ x) → is_fortytwo x.
Proof. info_auto with le_db. Qed.
Example auto_example_7: ∀ x,
(x ≤ 42 ∧ 42 ≤ x) → is_fortytwo x.
Proof.
auto. (* does nothing *)
Abort.
Hint Unfold is_fortytwo : le_db.
Example auto_example_7' : ∀ x,
(x ≤ 42 ∧ 42 ≤ x) → is_fortytwo x.
Proof. info_auto with le_db. Qed.
The "global" database that auto always uses is named core.
You can add your own hints to it, but the Coq manual discourages
that, preferring instead to have specialized databases for
specific developments. Many of the important libraries have their
own hint databases that you can tag in: arith, bool, datatypes
(including lists), etc.
Example auto_example_8 : ∀ (n m : nat),
n + m = m + n.
Proof.
auto. (* no progress *)
info_auto with arith. (* uses Nat.add_comm *)
Qed.
n + m = m + n.
Proof.
auto. (* no progress *)
info_auto with arith. (* uses Nat.add_comm *)
Qed.
Exercise: 3 stars, standard (re_opt_match_auto)
Lemma re_opt_match'' : ∀ T (re: reg_exp T) s,
s =~ re → s =~ re_opt re.
Proof.
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_re_opt_match'' : option (nat×string) := None.
☐
s =~ re → s =~ re_opt re.
Proof.
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_re_opt_match'' : option (nat×string) := None.
☐
Exercise: 3 stars, advanced, optional (pumping_redux)
Use auto, lia, and any other useful tactics from this chapter to shorten your proof (or the "official" solution proof) of the weak Pumping Lemma exercise from IndProp.
Import Pumping.
Lemma weak_pumping : ∀ T (re : reg_exp T) s,
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_pumping_redux : option (nat×string) := None.
☐
Lemma weak_pumping : ∀ T (re : reg_exp T) s,
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_pumping_redux : option (nat×string) := None.
☐
Exercise: 3 stars, advanced, optional (pumping_redux_strong)
Use auto, lia, and any other useful tactics from this chapter to shorten your proof (or the "official" solution proof) of the stronger Pumping Lemma exercise from IndProp.
Lemma pumping : ∀ T (re : reg_exp T) s,
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
length s1 + length s2 ≤ pumping_constant re ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
intros T re s Hmatch.
induction Hmatch
as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ];
simpl; try lia;
intros Hlen.
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_pumping_redux_strong : option (nat×string) := None.
☐
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
length s1 + length s2 ≤ pumping_constant re ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
intros T re s Hmatch.
induction Hmatch
as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ];
simpl; try lia;
intros Hlen.
(* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_pumping_redux_strong : option (nat×string) := None.
☐
The eauto variant
Example trans_example1: ∀ a b c d,
a ≤ b + b × c →
(1 + c) × b ≤ d →
a ≤ d.
Proof.
intros a b c d H1 H2.
apply Nat.le_trans with (b + b × c).
(* ^ We must supply the intermediate value *)
- apply H1.
- simpl in H2. rewrite mul_comm. apply H2.
Qed.
a ≤ b + b × c →
(1 + c) × b ≤ d →
a ≤ d.
Proof.
intros a b c d H1 H2.
apply Nat.le_trans with (b + b × c).
(* ^ We must supply the intermediate value *)
- apply H1.
- simpl in H2. rewrite mul_comm. apply H2.
Qed.
In the first step of the proof, we had to explicitly provide a
longish expression to help Coq instantiate a "hidden" argument to
the le_trans constructor. This was needed because the definition
of le_trans...
le_trans : ∀ m n o : nat, m ≤ n → n ≤ o → m ≤ o is quantified over a variable, n, that does not appear in its conclusion, so unifying its conclusion with the goal state doesn't help Coq find a suitable value for this variable. If we leave out the with, this step fails ("Error: Unable to find an instance for the variable n").
We already know one way to avoid an explicit with clause, namely
to provide H1 as the (first) explicit argument to le_trans.
But here's another way, using the eapply tactic:
le_trans : ∀ m n o : nat, m ≤ n → n ≤ o → m ≤ o is quantified over a variable, n, that does not appear in its conclusion, so unifying its conclusion with the goal state doesn't help Coq find a suitable value for this variable. If we leave out the with, this step fails ("Error: Unable to find an instance for the variable n").
Example trans_example1': ∀ a b c d,
a ≤ b + b × c →
(1 + c) × b ≤ d →
a ≤ d.
Proof.
intros a b c d H1 H2.
eapply Nat.le_trans. (* 1 *)
- apply H1. (* 2 *)
- simpl in H2. rewrite mul_comm. apply H2.
Qed.
a ≤ b + b × c →
(1 + c) × b ≤ d →
a ≤ d.
Proof.
intros a b c d H1 H2.
eapply Nat.le_trans. (* 1 *)
- apply H1. (* 2 *)
- simpl in H2. rewrite mul_comm. apply H2.
Qed.
The eapply H tactic behaves just like apply H except
that, after it finishes unifying the goal state with the
conclusion of H, it does not bother to check whether all the
variables that were introduced in the process have been given
concrete values during unification.
If you step through the proof above, you'll see that the goal
state at position 1 mentions the existential variable ?n in
both of the generated subgoals. The next step (which gets us to
position 2) replaces ?n with a concrete value. When we start
working on the second subgoal (position 3), we observe that the
occurrence of ?n in this subgoal has been replaced by the value
that it was given during the first subgoal.
Several of the tactics that we've seen so far, including
∃, constructor, and auto, have e... variants. For
example, here's a proof using eauto:
Example trans_example2: ∀ a b c d,
a ≤ b + b × c →
b + b × c ≤ d →
a ≤ d.
Proof.
intros a b c d H1 H2.
info_eauto using Nat.le_trans.
Qed.
a ≤ b + b × c →
b + b × c ≤ d →
a ≤ d.
Proof.
intros a b c d H1 H2.
info_eauto using Nat.le_trans.
Qed.
The eauto tactic works just like auto, except that it
uses eapply instead of apply.
Pro tip: One might think that, since eapply and eauto are more
powerful than apply and auto, it would be a good idea to use
them all the time. Unfortunately, they are also significantly
slower -- especially eauto. Coq experts tend to use apply and
auto most of the time, only switching to the e variants when
the ordinary variants don't do the job.
Ltac: The Tactic Language
Ltac Functions
Ltac simpl_and_try tac := simpl; try tac.
This defines a new tactic called simpl_and_try that takes one
tactic tac as an argument and is defined to be equivalent to
simpl; try tac. Now writing "simpl_and_try reflexivity." in a
proof will be the same as writing "simpl; try reflexivity."
Example sat_ex1 : 1 + 1 = 2.
Proof. simpl_and_try reflexivity. Qed.
Example sat_ex2 : ∀ (n : nat), 1 - 1 + n + 1 = 1 + n.
Proof. simpl_and_try reflexivity. lia. Qed.
Proof. simpl_and_try reflexivity. Qed.
Example sat_ex2 : ∀ (n : nat), 1 - 1 + n + 1 = 1 + n.
Proof. simpl_and_try reflexivity. lia. Qed.
Of course, that little tactic is not so useful. But it
demonstrates that we can parameterize Ltac-defined tactics, and
that their bodies are themselves tactics that will be run in the
context of a proof. So Ltac can be used to create functions on
tactics.
For a more useful tactic, consider these three proofs from
Basics, and how structurally similar they all are:
Theorem plus_1_neq_0 : ∀ n : nat,
(n + 1) =? 0 = false.
Proof.
intros n. destruct n.
- reflexivity.
- reflexivity.
Qed.
Theorem negb_involutive : ∀ b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b.
- reflexivity.
- reflexivity.
Qed.
Theorem andb_commutative : ∀ b c, andb b c = andb c b.
Proof.
intros b c. destruct b.
- destruct c.
+ reflexivity.
+ reflexivity.
- destruct c.
+ reflexivity.
+ reflexivity.
Qed.
(n + 1) =? 0 = false.
Proof.
intros n. destruct n.
- reflexivity.
- reflexivity.
Qed.
Theorem negb_involutive : ∀ b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b.
- reflexivity.
- reflexivity.
Qed.
Theorem andb_commutative : ∀ b c, andb b c = andb c b.
Proof.
intros b c. destruct b.
- destruct c.
+ reflexivity.
+ reflexivity.
- destruct c.
+ reflexivity.
+ reflexivity.
Qed.
We can factor out the common structure:
- Do a destruct.
- For each branch, finish with reflexivity -- if possible.
Ltac destructpf x :=
destruct x; try reflexivity.
Theorem plus_1_neq_0' : ∀ n : nat,
(n + 1) =? 0 = false.
Proof. intros n; destructpf n. Qed.
Theorem negb_involutive' : ∀ b : bool,
negb (negb b) = b.
Proof. intros b; destructpf b. Qed.
Theorem andb_commutative' : ∀ b c, andb b c = andb c b.
Proof.
intros b c; destructpf b; destructpf c.
Qed.
destruct x; try reflexivity.
Theorem plus_1_neq_0' : ∀ n : nat,
(n + 1) =? 0 = false.
Proof. intros n; destructpf n. Qed.
Theorem negb_involutive' : ∀ b : bool,
negb (negb b) = b.
Proof. intros b; destructpf b. Qed.
Theorem andb_commutative' : ∀ b c, andb b c = andb c b.
Proof.
intros b c; destructpf b; destructpf c.
Qed.
Exercise: 1 star, standard (andb3_exchange)
Re-prove the following theorem from Basics, using only intros and destructpf. You should have a one-shot proof.
Theorem andb3_exchange :
∀ b c d, andb (andb b c) d = andb (andb b d) c.
Proof. (* FILL IN HERE *) Admitted.
☐
∀ b c d, andb (andb b c) d = andb (andb b d) c.
Proof. (* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (andb_true_elim2)
The following theorem from Basics can't be proved with destructpf.
Theorem andb_true_elim2 : ∀ b c : bool,
andb b c = true → c = true.
Proof.
intros b c. destruct b eqn:Eb.
- simpl. intros H. rewrite H. reflexivity.
- simpl. intros H. destruct c eqn:Ec.
+ reflexivity.
+ rewrite H. reflexivity.
Qed.
andb b c = true → c = true.
Proof.
intros b c. destruct b eqn:Eb.
- simpl. intros H. rewrite H. reflexivity.
- simpl. intros H. destruct c eqn:Ec.
+ reflexivity.
+ rewrite H. reflexivity.
Qed.
Uncomment the definition of destructpf', below, and define your
own, improved version of destructpf. Use it to prove the
theorem.
(*
Ltac destructpf' x := ...
*)
Ltac destructpf' x := ...
*)
Your one-shot proof should need only intros and
destructpf'.
Theorem andb_true_elim2' : ∀ b c : bool,
andb b c = true → c = true.
Proof. (* FILL IN HERE *) Admitted.
andb b c = true → c = true.
Proof. (* FILL IN HERE *) Admitted.
Double-check that intros and your new destructpf' still
suffice to prove this earlier theorem -- i.e., that your improved
tactic is general enough to still prove it in one shot:
Theorem andb3_exchange' :
∀ b c d, andb (andb b c) d = andb (andb b d) c.
Proof. (* FILL IN HERE *) Admitted.
☐
∀ b c d, andb (andb b c) d = andb (andb b d) c.
Proof. (* FILL IN HERE *) Admitted.
☐
Ltac Pattern Matching
Theorem app_nil_r : ∀ (X : Type) (lst : list X),
lst ++ [] = lst.
Proof.
intros X lst. induction lst as [ | h t IHt].
- reflexivity.
- simpl. rewrite IHt. reflexivity.
Qed.
lst ++ [] = lst.
Proof.
intros X lst. induction lst as [ | h t IHt].
- reflexivity.
- simpl. rewrite IHt. reflexivity.
Qed.
At the point we rewrite, we can't substitute away t: it
is present on both sides of the equality in the inductive
hypothesis IHt : t ++ [] = t. How can we pick out which
hypothesis to rewrite in an Ltac tactic?
To solve this and other problems, Ltac contains a pattern-matching
tactic match goal. It allows us to match against the proof
state rather than against a program.
The syntax is similar to a match in Gallina (Coq's term
language), but has some new features:
The single branch above therefore specifies to match a goal whose
conclusion is the term True and whose hypotheses may be anything.
If such a match occurs, it will run apply I.
There may be multiple branches, which are tried in order.
- The word goal here is a keyword, rather than an expression
being matched. It means to match against the proof state, rather
than a program term.
- The square brackets around the pattern can often be omitted, but
they do make it easier to visually distinguish which part of the
code is the pattern.
- The turnstile ⊢ separates the hypothesis patterns (if any)
from the conclusion pattern. It represents the big horizontal
line shown by your IDE in the proof state: the hypotheses are to
the left of it, the conclusion is to the right.
- The hypotheses in the pattern need not completely describe all
the hypotheses present in the proof state. It is fine for there
to be additional hypotheses in the proof state that do not match
any of the patterns. The point is for match goal to pick out
particular hypotheses of interest, rather than fully specify the
proof state.
- The right-hand side of a branch is a tactic to run, rather than a program term.
Theorem match_ex2 : True ∧ True.
Proof.
match goal with
| [ ⊢ True ] ⇒ apply I
| [ ⊢ True ∧ True ] ⇒ split; apply I
end.
Qed.
Proof.
match goal with
| [ ⊢ True ] ⇒ apply I
| [ ⊢ True ∧ True ] ⇒ split; apply I
end.
Qed.
To see what branches are being tried, it can help to insert calls
to the identity tactic idtac. It optionally accepts an argument
to print out as debugging information.
Theorem match_ex2' : True ∧ True.
Proof.
match goal with
| [ ⊢ True ] ⇒ idtac "branch 1"; apply I
| [ ⊢ True ∧ True ] ⇒ idtac "branch 2"; split; apply I
end.
Qed.
Proof.
match goal with
| [ ⊢ True ] ⇒ idtac "branch 1"; apply I
| [ ⊢ True ∧ True ] ⇒ idtac "branch 2"; split; apply I
end.
Qed.
Only the second branch was tried. The first one did not match the
goal.
The semantics of the tactic match goal have a big
difference with the semantics of the term match. With the
latter, the first matching pattern is chosen, and later branches
are never considered. In fact, an error is produced if later
branches are known to be redundant.
But with match goal, if the tactic for the branch fails,
pattern matching continues with the next branch, until a branch
succeeds, or all branches have failed.
Theorem match_ex2'' : True ∧ True.
Proof.
match goal with
| [ ⊢ _ ] ⇒ idtac "branch 1"; apply I
| [ ⊢ True ∧ True ] ⇒ idtac "branch 2"; split; apply I
end.
Qed.
Proof.
match goal with
| [ ⊢ _ ] ⇒ idtac "branch 1"; apply I
| [ ⊢ True ∧ True ] ⇒ idtac "branch 2"; split; apply I
end.
Qed.
The first branch was tried but failed, then the second
branch was tried and succeeded. If all the branches fail, the
match goal fails.
Theorem match_ex2''' : True ∧ True.
Proof.
Fail match goal with
| [ ⊢ _ ] ⇒ idtac "branch 1"; apply I
| [ ⊢ _ ] ⇒ idtac "branch 2"; apply I
end.
Abort.
Proof.
Fail match goal with
| [ ⊢ _ ] ⇒ idtac "branch 1"; apply I
| [ ⊢ _ ] ⇒ idtac "branch 2"; apply I
end.
Abort.
Next, let's try matching against hypotheses. We can bind a
hypothesis name, as with H below, and use that name on the
right-hand side of the branch.
Theorem match_ex3 : ∀ (P : Prop), P → P.
Proof.
intros P HP.
match goal with
| [ H : _ ⊢ _ ] ⇒ apply H
end.
Qed.
Proof.
intros P HP.
match goal with
| [ H : _ ⊢ _ ] ⇒ apply H
end.
Qed.
The actual name of the hypothesis is of course HP, but the
pattern binds it as H. Using idtac, we can even observe the
actual name: stepping through the following proof causes "HP" to
be printed.
Theorem match_ex3' : ∀ (P : Prop), P → P.
Proof.
intros P HP.
match goal with
| [ H : _ ⊢ _ ] ⇒ idtac H; apply H
end.
Qed.
Proof.
intros P HP.
match goal with
| [ H : _ ⊢ _ ] ⇒ idtac H; apply H
end.
Qed.
We'll keep using idtac for awhile to observe the behavior
of match goal, but, note that it isn't necessary for the
successful proof of any of the following examples.
If there are multiple hypotheses that match, which one does Ltac
choose? Here is a big difference with regular match against
terms: Ltac will try all possible matches until one succeeds (or
all have failed).
Theorem match_ex4 : ∀ (P Q : Prop), P → Q → P.
Proof.
intros P Q HP HQ.
match goal with
| [ H : _ ⊢ _ ] ⇒ idtac H; apply H
end.
Qed.
Proof.
intros P Q HP HQ.
match goal with
| [ H : _ ⊢ _ ] ⇒ idtac H; apply H
end.
Qed.
That example prints "HQ" followed by "HP". Ltac first
matched against the most recently introduced hypothesis HQ and
tried applying it. That did not solve the goal. So Ltac
backtracks and tries the next most-recent matching hypothesis,
which is HP. Applying that does succeed.
But if there were no successful hypotheses, the entire match
would fail:
Theorem match_ex5 : ∀ (P Q R : Prop), P → Q → R.
Proof.
intros P Q R HP HQ.
Fail match goal with
| [ H : _ ⊢ _ ] ⇒ idtac H; apply H
end.
Abort.
Proof.
intros P Q R HP HQ.
Fail match goal with
| [ H : _ ⊢ _ ] ⇒ idtac H; apply H
end.
Abort.
So far we haven't been very demanding in how to match
hypotheses. The wildcard (aka joker) pattern we've used
matches everything. We could be more specific by using
metavariables:
Theorem match_ex5 : ∀ (P Q : Prop), P → Q → P.
Proof.
intros P Q HP HQ.
match goal with
| [ H : ?X ⊢ ?X ] ⇒ idtac H; apply H
end.
Qed.
Proof.
intros P Q HP HQ.
match goal with
| [ H : ?X ⊢ ?X ] ⇒ idtac H; apply H
end.
Qed.
Note that this time, the only hypothesis printed by idtac
is HP. The HQ hypothesis is ruled out, because it does not
have the form ?X ⊢ ?X.
The occurrences of ?X in that pattern are as metavariables
that stand for the same term appearing both as the type of
hypothesis H and as the conclusion of the goal.
(The syntax of match goal requires that ? to distinguish
metavariables from other identifiers that might be in
scope. However, the ? is used only in the pattern. On the
right-hand side of the branch, it's actually required to drop the
?.)
Now we have seen yet another difference between match goal
and regular match against terms: match goal allows a
metavariable to be used multiple times in a pattern, each time
standing for the same term. The regular match does not allow
that:
Fail Definition dup_first_two_elts (lst : list nat) :=
match lst with
| x :: x :: _ ⇒ true
| _ ⇒ false
end.
match lst with
| x :: x :: _ ⇒ true
| _ ⇒ false
end.
The technical term for this is linearity: regular match
requires pattern variables to be linear, meaning that they are
used only once. Tactic match goal permits non-linear
metavariables, meaning that they can be used multiple times in a
pattern and must bind the same term each time.
Now that we've learned a bit about match goal, let's return
to the proof pattern of some simple inductions:
Theorem app_nil_r' : ∀ (X : Type) (lst : list X),
lst ++ [] = lst.
Proof.
intros X lst. induction lst as [ | h t IHt].
- reflexivity.
- simpl. rewrite IHt. reflexivity.
Qed.
lst ++ [] = lst.
Proof.
intros X lst. induction lst as [ | h t IHt].
- reflexivity.
- simpl. rewrite IHt. reflexivity.
Qed.
With match goal, we can automate that proof pattern:
Ltac simple_induction t :=
induction t; simpl;
try match goal with
| [H : _ = _ ⊢ _] ⇒ rewrite H
end;
reflexivity.
Theorem app_nil_r'' : ∀ (X : Type) (lst : list X),
lst ++ [] = lst.
Proof.
intros X lst. simple_induction lst.
Qed.
induction t; simpl;
try match goal with
| [H : _ = _ ⊢ _] ⇒ rewrite H
end;
reflexivity.
Theorem app_nil_r'' : ∀ (X : Type) (lst : list X),
lst ++ [] = lst.
Proof.
intros X lst. simple_induction lst.
Qed.
That works great! Here are two other proofs that follow the same
pattern.
Theorem add_assoc'' : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p. induction n.
- reflexivity.
- simpl. rewrite IHn. reflexivity.
Qed.
Theorem add_assoc''' : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p. simple_induction n.
Qed.
Theorem plus_n_Sm : ∀ n m : nat,
S (n + m) = n + (S m).
Proof.
intros n m. induction n.
- reflexivity.
- simpl. rewrite IHn. reflexivity.
Qed.
Theorem plus_n_Sm' : ∀ n m : nat,
S (n + m) = n + (S m).
Proof.
intros n m. simple_induction n.
Qed.
n + (m + p) = (n + m) + p.
Proof.
intros n m p. induction n.
- reflexivity.
- simpl. rewrite IHn. reflexivity.
Qed.
Theorem add_assoc''' : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p. simple_induction n.
Qed.
Theorem plus_n_Sm : ∀ n m : nat,
S (n + m) = n + (S m).
Proof.
intros n m. induction n.
- reflexivity.
- simpl. rewrite IHn. reflexivity.
Qed.
Theorem plus_n_Sm' : ∀ n m : nat,
S (n + m) = n + (S m).
Proof.
intros n m. simple_induction n.
Qed.
Using match goal to Prove Tautologies
Ltac imp_intuition :=
repeat match goal with
| [ H : ?P ⊢ ?P ] ⇒ apply H
| [ ⊢ ∀ _, _ ] ⇒ intro
| [ H1 : ?P → ?Q, H2 : ?P ⊢ _ ] ⇒ apply H1 in H2
end.
repeat match goal with
| [ H : ?P ⊢ ?P ] ⇒ apply H
| [ ⊢ ∀ _, _ ] ⇒ intro
| [ H1 : ?P → ?Q, H2 : ?P ⊢ _ ] ⇒ apply H1 in H2
end.
That tactic repeatedly matches against the goal until the match
fails to make progress. At each step, the match goal does one of
three things:
Already we can prove many theorems with this tactic:
- Finds that the conclusion is already in the hypotheses, in which
case the goal is finished.
- Finds that the conclusion is a quantification, in which case it
is introduced. Since implication P → Q is itself a
quantification ∀ (_ : P), Q, this case handles introduction of
implications, too.
- Finds that two formulas of the form ?P → ?Q and ?P are in the hypotheses. This is the first time we've seen an example of matching against two hypotheses simultaneously. Note that the metavariable ?P is once more non-linear: the same formula must occur in two different hypotheses. In this case, the tactic uses forward reasoning to change hypothesis H2 into ?Q.
Example imp1 : ∀ (P : Prop), P → P.
Proof. imp_intuition. Qed.
Example imp2 : ∀ (P Q : Prop), P → (P → Q) → Q.
Proof. imp_intuition. Qed.
Example imp3 : ∀ (P Q R : Prop), (P → Q → R) → (Q → P → R).
Proof. imp_intuition. Qed.
Proof. imp_intuition. Qed.
Example imp2 : ∀ (P Q : Prop), P → (P → Q) → Q.
Proof. imp_intuition. Qed.
Example imp3 : ∀ (P Q R : Prop), (P → Q → R) → (Q → P → R).
Proof. imp_intuition. Qed.
Suppose we were to add a new logical connective: nor, the "not
or" connective.
Classically, nor P Q would be equivalent to ~(P ∨ Q). But
constructively, only one direction of that is provable.
Theorem nor_not_or : ∀ (P Q : Prop),
nor P Q → ¬ (P ∨ Q).
Proof.
intros. destruct H. unfold not. intros. destruct H. auto. auto.
Qed.
nor P Q → ¬ (P ∨ Q).
Proof.
intros. destruct H. unfold not. intros. destruct H. auto. auto.
Qed.
Some other usual theorems about nor are still provable,
though.
Theorem nor_comm : ∀ (P Q : Prop),
nor P Q ↔ nor Q P.
Proof.
intros P Q. split.
- intros H. destruct H. apply stroke; assumption.
- intros H. destruct H. apply stroke; assumption.
Qed.
Theorem nor_not : ∀ (P : Prop),
nor P P ↔ ¬P.
Proof.
intros P. split.
- intros H. destruct H. assumption.
- intros H. apply stroke; assumption.
Qed.
nor P Q ↔ nor Q P.
Proof.
intros P Q. split.
- intros H. destruct H. apply stroke; assumption.
- intros H. destruct H. apply stroke; assumption.
Qed.
Theorem nor_not : ∀ (P : Prop),
nor P P ↔ ¬P.
Proof.
intros P. split.
- intros H. destruct H. assumption.
- intros H. apply stroke; assumption.
Qed.
Exercise: 4 stars, advanced (nor_intuition)
(* Ltac nor_intuition := ... *)
Each of the three theorems below, and many others involving these
logical connectives, should be provable with just
Proof. nor_intuition. Qed.
Theorem nor_comm' : ∀ (P Q : Prop),
nor P Q ↔ nor Q P.
Proof. (* FILL IN HERE *) Admitted.
Theorem nor_not' : ∀ (P : Prop),
nor P P ↔ ¬P.
Proof. (* FILL IN HERE *) Admitted.
Theorem nor_not_and' : ∀ (P Q : Prop),
nor P Q → ¬ (P ∧ Q).
Proof. (* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_nor_intuition : option (nat×string) := None.
☐
nor P Q ↔ nor Q P.
Proof. (* FILL IN HERE *) Admitted.
Theorem nor_not' : ∀ (P : Prop),
nor P P ↔ ¬P.
Proof. (* FILL IN HERE *) Admitted.
Theorem nor_not_and' : ∀ (P Q : Prop),
nor P Q → ¬ (P ∧ Q).
Proof. (* FILL IN HERE *) Admitted.
(* Do not modify the following line: *)
Definition manual_grade_for_nor_intuition : option (nat×string) := None.
☐
Review
- try, ;, repeat
- assumption, contradiction, subst, constructor
- lia, congruence, intuition
- auto, eauto, eapply
- Ltac functions and match goal
(* 2024-08-25 14:46 *)