Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 534:ed829eaa91b2
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 *) |