Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 36:9e46ade5af21

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Manual Proofs About Constructors
author Adam Chlipala <adamc@hcoop.net>
date Fri, 12 Sep 2008 14:59:08 -0400
parents 6d05ee182b65
children c9ade53b27aa
comparison
equal deleted inserted replaced
35:6d05ee182b65 36:9e46ade5af21
1002 1002
1003 After a few moments of squinting at this goal, it becomes apparent that we need to do a case analysis on the structure of [ls]. The rest is routine. *) 1003 After a few moments of squinting at this goal, it becomes apparent that we need to do a case analysis on the structure of [ls]. The rest is routine. *)
1004 1004
1005 destruct ls; crush. 1005 destruct ls; crush.
1006 1006
1007 (** We can go further in automating the proof by exploiting the hint mechanism further. *) 1007 (** We can go further in automating the proof by exploiting the hint mechanism. *)
1008 1008
1009 Restart. 1009 Restart.
1010 Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) => 1010 Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) =>
1011 destruct LS; crush. 1011 destruct LS; crush.
1012 induction tr1 using nat_tree_ind'; crush. 1012 induction tr1 using nat_tree_ind'; crush.
1013 Qed. 1013 Qed.
1014 1014
1015 (** We will go into great detail on hints in a later chapter, but the only important thing to note here is that we register a pattern that describes a conclusion we expect to encounter during the proof. The pattern may contain unification variables, whose names are prefixed with question marks, and we may refer to those bound variables in a tactic that we ask to have run whenever the pattern matches. 1015 (** We will go into great detail on hints in a later chapter, but the only important thing to note here is that we register a pattern that describes a conclusion we expect to encounter during the proof. The pattern may contain unification variables, whose names are prefixed with question marks, and we may refer to those bound variables in a tactic that we ask to have run whenever the pattern matches.
1016 1016
1017 The advantage of using the hint is not very clear here, because the original proof was so short. However, the hint has fundamentally improved the readability of our proof. Before, the proof refered to the local variable [ls], which has an automatically-generated name. To a human reading the proof script without stepping through it interactively, it was not clear where [ls] came from. The hint explains to the reader the process for choosing which variables to case analyze on, and the hint can continue working even if the rest of the proof structure changes significantly. *) 1017 The advantage of using the hint is not very clear here, because the original proof was so short. However, the hint has fundamentally improved the readability of our proof. Before, the proof refered to the local variable [ls], which has an automatically-generated name. To a human reading the proof script without stepping through it interactively, it was not clear where [ls] came from. The hint explains to the reader the process for choosing which variables to case analyze on, and the hint can continue working even if the rest of the proof structure changes significantly. *)
1018
1019
1020 (** * Manual Proofs About Constructors *)
1021
1022 (** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *)
1023
1024 Theorem true_neq_false : true <> false.
1025 (** We begin with the tactic [red], which is short for "one step of reduction," to unfold the definition of logical negation. *)
1026
1027 red.
1028 (** [[
1029
1030 ============================
1031 true = false -> False
1032 ]]
1033
1034 The negation is replaced with an implication of falsehood. We use the tactic [intro H] to change the assumption of the implication into a hypothesis named [H]. *)
1035
1036 intro H.
1037 (** [[
1038
1039 H : true = false
1040 ============================
1041 False
1042 ]]
1043
1044 This is the point in the proof where we apply some creativity. We define a function whose utility will become clear soon. *)
1045
1046 Definition f (b : bool) := if b then True else False.
1047
1048 (** It is worth recalling the difference between the lowercase and uppercase versions of truth and falsehood: [True] and [False] are logical propositions, while [true] and [false] are boolean values that we can case-analyze. We have defined [f] such that our conclusion of [False] is computationally equivalent to [f false]. Thus, the [change] tactic will let us change the conclusion to [f false]. *)
1049
1050 change (f false).
1051 (** [[
1052
1053 H : true = false
1054 ============================
1055 f false
1056 ]]
1057
1058 Now the righthand side of [H]'s equality appears in the conclusion, so we can rewrite. *)
1059
1060 rewrite <- H.
1061 (** [[
1062
1063 H : true = false
1064 ============================
1065 f true
1066 ]]
1067
1068 We are almost done. Just how close we are to done is revealed by computational simplification. *)
1069
1070 simpl.
1071 (** [[
1072
1073 H : true = false
1074 ============================
1075 True
1076 ]] *)
1077
1078 trivial.
1079 Qed.
1080
1081 (** I have no trivial automated version of this proof to suggest, beyond using [discriminate] or [congruence] in the first place.
1082
1083 %\medskip%
1084
1085 We can perform a similar manual proof of injectivity of the constructor [S]. I leave a walk-through of the details to curious readers who want to run the proof script interactively. *)
1086
1087 Theorem S_inj' : forall n m : nat, S n = S m -> n = m.
1088 intros n m H.
1089 change (pred (S n) = pred (S m)).
1090 rewrite H.
1091 reflexivity.
1092 Qed.
1093