Mercurial > cpdt > repo

comparison src/LogicProg.v @ 539:8dddcaaeb67a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Two English errors fixed
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Aug 2015 15:54:11 -0400
parents ed829eaa91b2
children 582bf8d4ce51
comparison
equal deleted inserted replaced
538:d53c077a630c 539:8dddcaaeb67a
396 396
397 (* begin thide *) 397 (* begin thide *)
398 Hint Resolve eq_trans : slow. 398 Hint Resolve eq_trans : slow.
399 (* end thide *) 399 (* end thide *)
400 400
401 Example three_minus_four_zero : exists x, 1 + x = 0. 401 Example from_one_to_zero : exists x, 1 + x = 0.
402 (* begin thide *) 402 (* begin thide *)
403 Time eauto. 403 Time eauto.
404 (** %\vspace{-.15in}% 404 (** %\vspace{-.15in}%
405 << 405 <<
406 Finished transaction in 0. secs (0.004u,0.s) 406 Finished transaction in 0. secs (0.004u,0.s)
775 crush. 775 crush.
776 Qed. 776 Qed.
777 777
778 Hint Resolve plus_0 times_1. 778 Hint Resolve plus_0 times_1.
779 779
780 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a ring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *) 780 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
781 781
782 Require Import Arith Ring. 782 Require Import Arith Ring.
783 783
784 Theorem combine : forall x k1 k2 n1 n2, 784 Theorem combine : forall x k1 k2 n1 n2,
785 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2). 785 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).