Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents 549d604c3d16
children 4b1242b277b2
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
418 418
419 Theorem nsize_nsplice : forall tr1 tr2 : nat_btree, nsize (nsplice tr1 tr2) 419 Theorem nsize_nsplice : forall tr1 tr2 : nat_btree, nsize (nsplice tr1 tr2)
420 = plus (nsize tr2) (nsize tr1). 420 = plus (nsize tr2) (nsize tr1).
421 (* begin thide *) 421 (* begin thide *)
422 (* begin hide *) 422 (* begin hide *)
423 Hint Rewrite n_plus_O plus_assoc : cpdt. 423 Hint Rewrite n_plus_O plus_assoc.
424 (* end hide *) 424 (* end hide *)
425 (** [Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [n_plus_O plus_assoc : cpdt.] *) 425 (** [Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [n_plus_O plus_assoc.] *)
426 426
427 induction tr1; crush. 427 induction tr1; crush.
428 Qed. 428 Qed.
429 (* end thide *) 429 (* end thide *)
430 430
1123 1123
1124 Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2) 1124 Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2)
1125 = plus (ntsize tr2) (ntsize tr1). 1125 = plus (ntsize tr2) (ntsize tr1).
1126 (* begin thide *) 1126 (* begin thide *)
1127 (* begin hide *) 1127 (* begin hide *)
1128 Hint Rewrite plus_S : cpdt. 1128 Hint Rewrite plus_S.
1129 (* end hide *) 1129 (* end hide *)
1130 (** [Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [plus_S : cpdt.] *) 1130 (** [Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [plus_S.] *)
1131 1131
1132 (** We know that the standard induction principle is insufficient for the task, so we need to provide a %\index{tactics!using}%[using] clause for the [induction] tactic to specify our alternate principle. *) 1132 (** We know that the standard induction principle is insufficient for the task, so we need to provide a %\index{tactics!using}%[using] clause for the [induction] tactic to specify our alternate principle. *)
1133 1133
1134 induction tr1 using nat_tree_ind'; crush. 1134 induction tr1 using nat_tree_ind'; crush.
1135 1135