From 65b817d7ae4404b5ed1f1c9fed8fa744bc830a23 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 6 Feb 2022 13:03:43 -0500 Subject: [PATCH] Revising for Wednesday's lecture --- RuleInduction.v | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/RuleInduction.v b/RuleInduction.v index 5be223b..5341633 100644 --- a/RuleInduction.v +++ b/RuleInduction.v @@ -19,6 +19,8 @@ Theorem favorites_below_50 : forall n, my_favorite_numbers n -> n < 50. Proof. simplify. invert H. + (* [invert]: case analysis on which rules may have been used to prove an + * instance of an inductive predicate *) linear_arithmetic. linear_arithmetic. linear_arithmetic. @@ -82,6 +84,8 @@ Theorem lt_lt' : forall n m, n < m -> lt' n m. Proof. simplify. replace m with (S (m - n - 1) + n) by linear_arithmetic. + (* [replace]: change a subterm into another one, adding an obligation to prove + * equality of the two. *) apply lt_lt''. Qed. @@ -260,6 +264,8 @@ Module SimplePropositional. apply ValidTruth. propositional. + (* [propositional]: simplify goal according to the rules of propositional + * logic, a decidable theory. *) propositional. apply ValidAnd.