From 3048b59f346316abfb7499c90a58e86267baad97 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 16 Mar 2021 18:23:24 -0400 Subject: [PATCH] Revising before tomorrow's lecture --- LogicProgramming.v | 46 ++++++++++++++++++------------------- LogicProgramming_template.v | 2 +- 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/LogicProgramming.v b/LogicProgramming.v index 563939e..cdea144 100644 --- a/LogicProgramming.v +++ b/LogicProgramming.v @@ -44,7 +44,7 @@ Qed. * automate searching through sequences of that kind, when we prime it with good * suggestions of single proof steps to try, as with this command: *) -Hint Constructors plusR : core. +Local Hint Constructors plusR : core. (* That is, every constructor of [plusR] should be considered as an atomic proof * step, from which we enumerate step sequences. *) @@ -195,17 +195,17 @@ Qed. * programs in the same way as we did above for a logic program. Let us prove * that the constructors of [plusR] have natural interpretations as lemmas about * [plus]. We can find the first such lemma already proved in the standard - * library, using the [SearchRewrite] command to find a library function proving + * library, using the [Search] command to find a library function proving * an equality whose lefthand or righthand side matches a pattern with * wildcards. *) -SearchRewrite (O + _). +Search (O + _). (* The command [Hint Immediate] asks [auto] and [eauto] to consider this lemma * as a candidate step for any leaf of a proof tree, meaning that all premises * of the rule need to match hypotheses. *) -Hint Immediate plus_O_n : core. +Local Hint Immediate plus_O_n : core. (* The counterpart to [PlusS] we will prove ourselves. *) @@ -219,7 +219,7 @@ Qed. (* The command [Hint Resolve] adds a new candidate proof step, to be attempted * at any level of a proof tree, not just at leaves. *) -Hint Resolve plusS : core. +Local Hint Resolve plusS : core. (* Now that we have registered the proper hints, we can replicate our previous * examples with the normal, functional addition [plus]. *) @@ -251,7 +251,7 @@ Proof. linear_arithmetic. Qed. -Hint Resolve plusO : core. +Local Hint Resolve plusO : core. (* Note that, if we consider the inputs to [plus] as the inputs of a * corresponding logic program, the new rule [plusO] introduces an ambiguity. @@ -304,7 +304,7 @@ End slow. * _hint databases_ to segregate hints into different groups that may be called * on as needed. Here we put [eq_trans] into the database [slow]. *) -Hint Resolve eq_trans : slow. +Local Hint Resolve eq_trans : slow. Example from_one_to_zero : exists x, 1 + x = 0. Proof. @@ -367,7 +367,7 @@ Proof. simplify; equality. Qed. -Hint Resolve length_O length_S : core. +Local Hint Resolve length_O length_S : core. (* Let us apply these hints to prove that a [list nat] of length 2 exists. * (Here we register [length_O] with [Hint Resolve] instead of [Hint Immediate] @@ -424,7 +424,7 @@ Proof. linear_arithmetic. Qed. -Hint Resolve plusO' : core. +Local Hint Resolve plusO' : core. (* Finally, we meet [Hint Extern], the command to register a custom hint. That * is, we provide a pattern to match against goals during proof search. @@ -434,7 +434,7 @@ Hint Resolve plusO' : core. * effect on proof-search time, i.e. when we manage to give lower priorities to * the cheaper rules. *) -Hint Extern 1 (sum _ = _) => simplify : core. +Local Hint Extern 1 (sum _ = _) => simplify : core. (* Now we can find a length-2 list whose sum is 0. *) @@ -497,7 +497,7 @@ Inductive eval (var : nat) : exp -> nat -> Prop := -> eval var e2 n2 -> eval var (Plus e1 e2) (n1 + n2). -Hint Constructors eval : core. +Local Hint Constructors eval : core. (* We can use [auto] to execute the semantics for specific expressions. *) @@ -531,7 +531,7 @@ Proof. simplify; subst; auto. Qed. -Hint Resolve EvalPlus' : core. +Local Hint Resolve EvalPlus' : core. (* Further, we instruct [eauto] to apply [ring], via [Hint Extern]. We should * try this step for any equality goal. *) @@ -597,7 +597,7 @@ Proof. simplify; subst; auto. Qed. -Hint Resolve EvalConst' EvalVar' : core. +Local Hint Resolve EvalConst' EvalVar' : core. (* Next, we prove a few hints that feel a bit like cheating, as they telegraph * the procedure for choosing values of [k] and [n]. Nonetheless, with these @@ -673,14 +673,14 @@ Ltac robust_ring_simplify := (* This tactic is pretty expensive, but let's try it eventually whenever the * goal is an equality. *) -Hint Extern 5 (_ = _) => robust_ring_simplify : core. +Local Hint Extern 5 (_ = _) => robust_ring_simplify : core. (* The only other missing ingredient is priming Coq with some good ideas for * instantiating existential quantifiers. These will all be tried in some * order, in a particular proof search. *) -Hint Extern 1 (exists n : nat, _) => exists 0 : core. -Hint Extern 1 (exists n : nat, _) => exists 1 : core. -Hint Extern 1 (exists n : nat, _) => eexists (_ + _) : core. +Local Hint Extern 1 (exists n : nat, _) => exists 0 : core. +Local Hint Extern 1 (exists n : nat, _) => exists 1 : core. +Local Hint Extern 1 (exists n : nat, _) => eexists (_ + _) : core. (* Note how this last hint uses [eexists] to provide an instantiation with * wildcards inside it. Each underscore is replaced with a fresh unification * variable. *) @@ -695,9 +695,9 @@ Qed. (* Here's a quick tease using a feature that we'll explore fully in a later * class. Let's use a mysterious construct [sigT] instead of [exists]. *) -Hint Extern 1 (sigT (fun n : nat => _)) => exists 0 : core. -Hint Extern 1 (sigT (fun n : nat => _)) => exists 1 : core. -Hint Extern 1 (sigT (fun n : nat => _)) => eexists (_ + _) : core. +Local Hint Extern 1 (sigT (fun n : nat => _)) => exists 0 : core. +Local Hint Extern 1 (sigT (fun n : nat => _)) => exists 1 : core. +Local Hint Extern 1 (sigT (fun n : nat => _)) => eexists (_ + _) : core. Theorem linear_computable : forall e, sigT (fun k => sigT (fun n => forall var, eval var e (k * var + n))). @@ -814,7 +814,7 @@ Abort. * restatement of the theorem we mean to prove. Luckily, a simpler form * suffices, by appealing to the [equality] tactic. *) -Hint Extern 1 (_ <> _) => equality : core. +Local Hint Extern 1 (_ <> _) => equality : core. Theorem bool_neq : true <> false. Proof. @@ -856,7 +856,7 @@ End forall_and. (* After our success on this example, we might get more ambitious and seek to * generalize the hint to all possible predicates [P]. *) -Fail Hint Extern 1 (?P ?X) => +Fail Local Hint Extern 1 (?P ?X) => match goal with | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X)) end : core. @@ -871,7 +871,7 @@ Fail Hint Extern 1 (?P ?X) => * leave out the pattern to the left of the [=>], incorporating the * corresponding logic into the Ltac script. *) -Hint Extern 1 => +Local Hint Extern 1 => match goal with | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X)) end : core. diff --git a/LogicProgramming_template.v b/LogicProgramming_template.v index a867c3f..cf8f500 100644 --- a/LogicProgramming_template.v +++ b/LogicProgramming_template.v @@ -173,7 +173,7 @@ Inductive eval (var : nat) : exp -> nat -> Prop := -> eval var e2 n2 -> eval var (Plus e1 e2) (n1 + n2). -Hint Constructors eval : core. +Local Hint Constructors eval : core. Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)). Proof.