Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents 4a663981b699
children d65e9c1c9041
comparison
equal deleted inserted replaced
533:8921cfa2f503 534:ed829eaa91b2
1 (* Copyright (c) 2008-2012, Adam Chlipala 1 (* Copyright (c) 2008-2012, 2015, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import List. 11 Require Import List.
12 12
13 Require Import CpdtTactics. 13 Require Import Cpdt.CpdtTactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 Set Asymmetric Patterns.
16 (* end hide *) 17 (* end hide *)
17 18
18 19
19 (** %\part{Basic Programming and Proving} 20 (** %\part{Basic Programming and Proving}
20 21
392 (* begin thide *) 393 (* begin thide *)
393 induction n1; crush. 394 induction n1; crush.
394 Qed. 395 Qed.
395 (* end thide *) 396 (* end thide *)
396 397
398 Hint Rewrite n_plus_O plus_assoc.
399
397 Theorem nsize_nsplice : forall tr1 tr2 : nat_btree, nsize (nsplice tr1 tr2) 400 Theorem nsize_nsplice : forall tr1 tr2 : nat_btree, nsize (nsplice tr1 tr2)
398 = plus (nsize tr2) (nsize tr1). 401 = plus (nsize tr2) (nsize tr1).
399 (* begin thide *) 402 (* begin thide *)
400 Hint Rewrite n_plus_O plus_assoc.
401
402 induction tr1; crush. 403 induction tr1; crush.
403 Qed. 404 Qed.
404 (* end thide *) 405 (* end thide *)
405 406
406 (** It is convenient that these proofs go through so easily, but it is still useful to look into the details of what happened, by checking the statement of the tree induction principle. *) 407 (** It is convenient that these proofs go through so easily, but it is still useful to look into the details of what happened, by checking the statement of the tree induction principle. *)
1080 Qed. 1081 Qed.
1081 (* end thide *) 1082 (* end thide *)
1082 1083
1083 (** Now we begin the proof of the theorem, adding the lemma [plus_S] as a hint. *) 1084 (** Now we begin the proof of the theorem, adding the lemma [plus_S] as a hint. *)
1084 1085
1086 Hint Rewrite plus_S.
1087
1085 Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2) 1088 Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2)
1086 = plus (ntsize tr2) (ntsize tr1). 1089 = plus (ntsize tr2) (ntsize tr1).
1087 (* begin thide *) 1090 (* begin thide *)
1088 Hint Rewrite plus_S.
1089
1090 (** 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. *) 1091 (** 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. *)
1091 1092
1092 induction tr1 using nat_tree_ind'; crush. 1093 induction tr1 using nat_tree_ind'; crush.
1093 1094
1094 (** One subgoal remains: [[ 1095 (** One subgoal remains: [[
1113 destruct ls; crush. 1114 destruct ls; crush.
1114 1115
1115 (** We can go further in automating the proof by exploiting the hint mechanism.%\index{Vernacular commands!Hint Extern}% *) 1116 (** We can go further in automating the proof by exploiting the hint mechanism.%\index{Vernacular commands!Hint Extern}% *)
1116 1117
1117 Restart. 1118 Restart.
1118 1119
1119 Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) => 1120 Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) =>
1120 destruct LS; crush. 1121 destruct LS; crush.
1121 induction tr1 using nat_tree_ind'; crush. 1122 induction tr1 using nat_tree_ind'; crush.
1122 Qed. 1123 Qed.
1123 (* end thide *) 1124 (* end thide *)