Mercurial > cpdt > repo

comparison src/LogicProg.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents 582bf8d4ce51
children
comparison
equal deleted inserted replaced
573:c3d77f2bb92c 574:1dc1d41620b6
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 11
12 Require Import List Omega. 12 Require Import List Lia.
13 13
14 Require Import Cpdt.CpdtTactics. 14 Require Import Cpdt.CpdtTactics.
15 15
16 Set Implicit Arguments. 16 Set Implicit Arguments.
17 Set Asymmetric Patterns. 17 Set Asymmetric Patterns.
150 auto 6. 150 auto 6.
151 151
152 (** Sometimes it is useful to see a description of the proof tree that [auto] finds, with the %\index{tactics!info}%[info] tactical. (This tactical is not available in Coq 8.4 as of this writing, but I hope it reappears soon. The special case %\index{tactics!info\_auto}%[info_auto] tactic is provided as a chatty replacement for [auto].) *) 152 (** Sometimes it is useful to see a description of the proof tree that [auto] finds, with the %\index{tactics!info}%[info] tactical. (This tactical is not available in Coq 8.4 as of this writing, but I hope it reappears soon. The special case %\index{tactics!info\_auto}%[info_auto] tactic is provided as a chatty replacement for [auto].) *)
153 153
154 Restart. 154 Restart.
155 info auto 6. 155 info_auto 6.
156 (** %\vspace{-.15in}%[[ 156 (** %\vspace{-.15in}%[[
157 == apply PlusS; apply PlusS; apply PlusS; apply PlusS; 157 == apply PlusS; apply PlusS; apply PlusS; apply PlusS;
158 apply PlusS; apply PlusO. 158 apply PlusS; apply PlusO.
159 ]] 159 ]]
160 *) 160 *)
218 apply PlusO. 218 apply PlusO.
219 219
220 (** The [auto] tactic will not perform these sorts of steps that introduce unification variables, but the %\index{tactics!eauto}%[eauto] tactic will. It is helpful to work with two separate tactics, because proof search in the [eauto] style can uncover many more potential proof trees and hence take much longer to run. *) 220 (** The [auto] tactic will not perform these sorts of steps that introduce unification variables, but the %\index{tactics!eauto}%[eauto] tactic will. It is helpful to work with two separate tactics, because proof search in the [eauto] style can uncover many more potential proof trees and hence take much longer to run. *)
221 221
222 Restart. 222 Restart.
223 info eauto 6. 223 info_eauto 6.
224 (** %\vspace{-.15in}%[[ 224 (** %\vspace{-.15in}%[[
225 == eapply ex_intro; apply PlusS; apply PlusS; 225 == eapply ex_intro; apply PlusS; apply PlusS;
226 apply PlusS; apply PlusS; apply PlusO. 226 apply PlusS; apply PlusS; apply PlusO.
227 ]] 227 ]]
228 *) 228 *)
429 429
430 Example needs_trans : forall x y, 1 + x = y 430 Example needs_trans : forall x y, 1 + x = y
431 -> y = 2 431 -> y = 2
432 -> exists z, z + x = 3. 432 -> exists z, z + x = 3.
433 (* begin thide *) 433 (* begin thide *)
434 info eauto with slow. 434 info_eauto with slow.
435 (** %\vspace{-.2in}%[[ 435 (** %\vspace{-.2in}%[[
436 == intro x; intro y; intro H; intro H0; simple eapply ex_intro; 436 == intro x; intro y; intro H; intro H0; simple eapply ex_intro;
437 apply plusS; simple eapply eq_trans. 437 apply plusS; simple eapply eq_trans.
438 exact H. 438 exact H.
439 439
670 crush. 670 crush.
671 Qed. 671 Qed.
672 672
673 Hint Resolve EvalPlus'. 673 Hint Resolve EvalPlus'.
674 674
675 (** Further, we instruct [eauto] to apply %\index{tactics!omega}%[omega], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic. Via [Hint Extern], we ask for use of [omega] on any equality goal. The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *) 675 (** Further, we instruct [eauto] to apply %\index{tactics!lia}%[lia], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic. Via [Hint Extern], we ask for use of [lia] on any equality goal. The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *)
676 676
677 Hint Extern 1 (_ = _) => abstract omega. 677 Hint Extern 1 (_ = _) => abstract lia.
678 (* end thide *) 678 (* end thide *)
679 679
680 (** Now we can return to [eval1'] and prove it automatically. *) 680 (** Now we can return to [eval1'] and prove it automatically. *)
681 681
682 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8). 682 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
694 : forall var : nat, 694 : forall var : nat,
695 eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8) 695 eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8)
696 ]] 696 ]]
697 *) 697 *)
698 698
699 (** The lemma [eval1'_subproof] was generated by [abstract omega]. 699 (** The lemma [eval1'_subproof] was generated by [abstract lia].
700 700
701 Now we are ready to take advantage of logic programming's flexibility by searching for a program (arithmetic expression) that always evaluates to a particular symbolic value. *) 701 Now we are ready to take advantage of logic programming's flexibility by searching for a program (arithmetic expression) that always evaluates to a particular symbolic value. *)
702 702
703 Example synthesize1 : exists e, forall var, eval var e (var + 7). 703 Example synthesize1 : exists e, forall var, eval var e (var + 7).
704 (* begin thide *) 704 (* begin thide *)