(** * InductionAI: Using LLMs to Explore Proof by Induction *) (** This file accompanies the [Induction] chapter of _Logical Foundations_. Each exercise asks you to interact with a large language model (LLM) and then engage critically with its output using Rocq as the ground truth. The themes of [Induction] make it especially interesting for LLM evaluation: inductive proofs require precisely the right case splits and induction hypotheses, and LLMs often make subtle errors here that are hard to spot without a proof assistant. _How to work through these exercises_: follow the same conventions as [BasicsAI]: - Follow each LLM interaction prompt. - Paste or adapt the LLM's output in the space provided. - Written reflections go in comments marked [WRITTEN RESPONSE]. - Every [Admitted] should be replaced by a real proof, unless the exercise explicitly says to leave it. _Compilation_: this file depends on [Induction.v] (and thereby on [Basics.v]). Compile in order: << rocq compile -Q . LF Basics.v rocq compile -Q . LF Induction.v rocq compile -Q . LF InductionAI.v >> *) From LF Require Export Induction. (* ================================================================= *) (** ** Provided Implementations *) (** The exercises below involve binary numbers. Complete implementations of [incr] and [bin_to_nat] are provided here so that this file compiles regardless of whether you finished those exercises in [Basics] and [Induction]. Use these [ai_]-prefixed versions throughout this file. *) Fixpoint ai_incr (m : bin) : bin := match m with | Z => B1 Z | B0 m' => B1 m' | B1 m' => B0 (ai_incr m') end. Fixpoint ai_bin_to_nat (m : bin) : nat := match m with | Z => 0 | B0 m' => 2 * ai_bin_to_nat m' | B1 m' => 1 + 2 * ai_bin_to_nat m' end. (** The following commuting-diagram lemma is _stated_ here for use in Exercise 1. It is _proved_ in Exercise 2. Complete Exercise 2 before relying on this in a closed proof of Exercise 1. *) Lemma ai_bin_to_nat_pres_incr : forall b : bin, ai_bin_to_nat (ai_incr b) = 1 + ai_bin_to_nat b. Proof. (* Proved in Exercise 2 (llm_bin_to_nat_pres_incr) below. *) (* FILL IN HERE *) Admitted. (* ################################################################# *) (** * Using LLMs as Code Generators *) (* ================================================================= *) (** ** Converting Natural Numbers to Binary *) (** **** Exercise: 3 stars, standard (nat_to_bin_implementation) Ask an LLM to implement [my_nat_to_bin], a function that converts a unary natural number to a binary number represented by [bin]. Paste the LLM's implementation below. Then prove [my_nat_bin_nat]: that converting a natural number to binary and back yields the original number. _Hint_: The proof of [my_nat_bin_nat] goes through smoothly using [ai_bin_to_nat_pres_incr] (proved in Exercise 2 below) as a lemma. If you find yourself in a complicated induction, revisit whether your definition of [my_nat_to_bin] is as simple as possible -- the recursive structure of the proof will mirror the recursive structure of the function. *) Fixpoint my_nat_to_bin (n : nat) : bin (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. Theorem my_nat_bin_nat : forall n : nat, ai_bin_to_nat (my_nat_to_bin n) = n. Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM's implementation compile on the first try? Did [my_nat_bin_nat] require any helper lemmas that the LLM did not mention? Describe what you changed, if anything. *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_nat_to_bin_implementation : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Using LLMs as Proof Generators *) (* ================================================================= *) (** ** The Commuting Diagram for Binary Increment *) (** **** Exercise: 3 stars, standard (llm_bin_to_nat_pres_incr) The following theorem says that binary increment and conversion to unary commute -- i.e., it does not matter whether you increment first and then convert, or convert first and then increment: << ai_incr bin -----------------------> bin | | ai_bin_to_nat | | ai_bin_to_nat | | v v nat -----------------------> nat S >> Ask an LLM to prove [ai_bin_to_nat_pres_incr]. Paste the LLM's proof attempt below. - If Rocq _accepts_ it: annotate each tactic line with a brief comment explaining the proof state at that point. - If Rocq _rejects_ it: identify the exact failing step, explain why it fails, and complete the proof yourself. _Hint_: The key structure is induction on [b]. Pay attention to what arithmetic simplification Rocq needs in the [B1] case. *) Theorem my_bin_to_nat_pres_incr : forall b : bin, ai_bin_to_nat (ai_incr b) = 1 + ai_bin_to_nat b. Proof. (* Paste the LLM's proof here, then annotate or fix it. *) (* FILL IN HERE *) Admitted. (** Once you have a proof, copy it into [ai_bin_to_nat_pres_incr] above so that Exercise 1 can use it. *) (** _Reflection_: Did the LLM's proof work without modification? If not, at which step did it fail, and what was the error? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_llm_bin_to_nat_pres_incr : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** Discovering Helper Lemmas for Addition *) (** **** Exercise: 3 stars, standard (llm_add_comm) Ask an LLM to prove commutativity of addition: << forall n m : nat, n + m = m + n. >> Before looking at the LLM's answer, try proving it yourself with [induction]. You will likely get stuck in the inductive step. Record in the comment marked [PROOF ATTEMPT] what goal you reach and why the proof stalls. A key ingredient is the lemma [plus_n_Sm]: << forall n m : nat, S (n + m) = n + (S m). >> Ask the LLM: (a) Does it identify [my_plus_n_Sm] as a necessary helper, or does it attempt the proof without it? (b) If it does not mention [my_plus_n_Sm], does its proof actually go through in Rocq? Prove both [my_plus_n_Sm] and [my_add_comm] below. Paste the LLM's attempts, fixing them if necessary. *) (* PROOF ATTEMPT: record the goal where your manual attempt stalled. Replace this comment with the goal text from Rocq. *) Theorem my_plus_n_Sm : forall n m : nat, S (n + m) = n + (S m). Proof. (* FILL IN HERE *) Admitted. Theorem my_add_comm : forall n m : nat, n + m = m + n. Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM spontaneously identify [my_plus_n_Sm] as a helper, or did it attempt the proof without it? If it attempted without the helper, did the proof fail? What does this tell you about whether LLMs "understand" the dependency structure of inductive proofs? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_llm_add_comm : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** Discovering Helper Lemmas for Multiplication *) (** **** Exercise: 4 stars, standard (llm_mul_comm) Ask an LLM to prove commutativity of multiplication: [[ forall m n : nat, m * n = n * m. ]] Before pasting its answer, write 2--3 sentences in the comment marked [STRATEGY] predicting what helper lemma(s) you think the proof will need and why. Paste the LLM's proof below (including any helper lemmas it proposes). Fix whatever does not compile. If you add helper lemmas not suggested by the LLM, note them in the reflection. _Hint_: Think about what [n * (1 + k)] equals, and what [mul_plus_distr_r] (distributivity of multiplication over addition) would buy you if you had it. *) (* STRATEGY: write your prediction here before looking at the LLM's answer. Replace this comment with your prediction. *) (** Provide any helper lemmas the LLM suggests (or that you discover are needed) here, with their proofs: *) (* FILL IN HERE -- add helper Theorem/Lemma statements and proofs *) Theorem my_mul_comm : forall m n : nat, m * n = n * m. Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM's proof compile without modification? Compare the helpers the LLM proposed to your prediction. Which lemmas were missing or unnecessary? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_llm_mul_comm : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Using LLMs as Conceptual Explainers *) (* ================================================================= *) (** ** Why Induction Succeeds Where Destruct Fails *) (** **** Exercise: 2 stars, standard (induction_vs_destruct) Ask an LLM: _"In Rocq, why can [n + 0 = n] not be proved using [destruct], and why does [induction] succeed where [destruct] fails?"_ The following two proofs from [Induction.v] illustrate the failure and the fix. Step through them in Rocq and record your observations. *) (** This proof attempt gets stuck: *) Theorem add_0_r_destruct_attempt : forall n : nat, n + 0 = n. Proof. intros n. destruct n as [| n'] eqn:E. - reflexivity. - simpl. (* What goal appears here? Record it in ROCQ OBSERVATION 1. *) Abort. (* ROCQ OBSERVATION 1: what goal appears in the [S n'] case above? Replace this comment with the goal. *) (** This proof succeeds using induction: *) Theorem add_0_r_induction : forall n : nat, n + 0 = n. Proof. intros n. induction n as [| n' IHn']. - reflexivity. - simpl. (* What goal appears here, and what is IHn'? Record both in ROCQ OBSERVATION 2. *) rewrite -> IHn'. reflexivity. Qed. (* ROCQ OBSERVATION 2: what is the goal in the inductive step, and what does IHn' say? Replace this comment with both. *) (** _Reflection_: Did the LLM's explanation correctly identify _why_ [destruct] fails? In particular, did it explain what the [S n'] case of [destruct] leaves you with versus what [induction] gives you (the induction hypothesis)? Write 2--3 sentences evaluating the accuracy of its answer. *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_induction_vs_destruct : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** Translating Between Formal and Informal Proofs *) (** **** Exercise: 2 stars, standard (formal_informal_proof) [Induction.v] shows both a compact Rocq proof and an English-prose proof of [add_assoc]. Ask an LLM to write an informal (English) proof of [my_add_comm] in the same style as the English proof of [add_assoc] in [Induction.v]. Then do the reverse: compose a brief informal proof of [eqb_refl] (the theorem [(n =? n) = true] for all [n]) yourself -- do not just paraphrase Rocq tactics into English -- and then ask the LLM to translate your informal proof into a Rocq proof. Paste the LLM's formal proof into [my_eqb_refl] below. _Note_: You do not need to write out your informal proof in this file; describe it in the reflection. *) Theorem my_eqb_refl : forall n : nat, (n =? n) = true. Proof. (* Paste the LLM's formalization of your informal proof here. *) (* FILL IN HERE *) Admitted. (** _Reflection_: (a) Did the LLM's informal proof of [my_add_comm] correctly identify both the base case and the inductive step? Did it make the induction hypothesis explicit? (b) Did the LLM's formalization of your informal [eqb_refl] proof compile in Rocq? If not, what was wrong? (c) What does this exercise reveal about the relationship between informal mathematical reasoning and formal Rocq proofs? *) (* WRITTEN RESPONSE: replace this comment with your answers to (a), (b), and (c). *) Definition manual_grade_for_formal_informal_proof : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** Why [bin_nat_bin] Fails *) (** **** Exercise: 2 stars, standard (bin_nat_bin_failure) Converting a [nat] to [bin] and back always gives the same [nat] (that is what [my_nat_bin_nat] proves). But the reverse direction -- converting [bin] to [nat] and back to [bin] -- does not always return the original [bin]. Ask an LLM: _"In the [Induction] chapter of Software Foundations, why does [bin_nat_bin] fail? That is, why is it not the case that [nat_to_bin (bin_to_nat b) = b] for all [b]?"_ Then explore the failure in Rocq by evaluating the examples below. Record the results in the comments. *) Compute (ai_bin_to_nat (B0 (B0 (B1 Z)))). (* ===> what does this evaluate to? Record in ROCQ OBSERVATION 1. *) Compute (my_nat_to_bin (ai_bin_to_nat (B0 (B0 (B1 Z))))). (* ===> what does this evaluate to? Is it equal to B0 (B0 (B1 Z))? Record in ROCQ OBSERVATION 2. NOTE: [my_nat_to_bin] will be [Admitted] until you complete Exercise 1. Replace this [Compute] with a specific example using your implementation once it is done. *) (* ROCQ OBSERVATION 1: result of computing ai_bin_to_nat (B0 (B0 (B1 Z))). *) (* ROCQ OBSERVATION 2: result of converting back. Is it the same binary representation? Why or why not? *) (** _Reflection_: Did the LLM correctly identify the root cause of the failure? (The key is that the same _natural number_ can have multiple _binary representations_ -- e.g., [4] can be represented as [B0 (B0 (B1 Z))] or [B0 (B0 (B0 (B1 Z)))] depending on whether leading zeros are allowed.) Write 2--3 sentences assessing the LLM's explanation. *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_bin_nat_bin_failure : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Using LLMs as Strategy Advisors *) (* ================================================================= *) (** ** Classifying Proof Strategies *) (** **** Exercise: 2 stars, standard (classifying_strategies) [Induction.v] suggests this exercise (informally): for each theorem below, predict whether its proof requires only (a) simplification and rewriting, (b) case analysis via [destruct], or (c) induction. Write your predictions _before_ looking at the LLM's answer. Ask an LLM to classify each theorem. Then check each classification in Rocq by attempting the predicted proof technique. Record the results in the table below. *) (** Theorem | Your prediction | LLM prediction | Rocq verdict -------------------------|-----------------|----------------|------------- [leb_refl] | | | [zero_neqb_S] | | | [andb_false_r] | | | [S_neqb_0] | | | [mult_1_l] | | | [all3_spec] | | | [mult_plus_distr_r] | | | [mult_assoc] | | | *) (** Prove each theorem using the technique you discovered: *) Theorem my_leb_refl : forall n : nat, (n <=? n) = true. Proof. (* FILL IN HERE *) Admitted. Theorem my_zero_neqb_S : forall n : nat, 0 =? (S n) = false. Proof. (* FILL IN HERE *) Admitted. Theorem my_andb_false_r : forall b : bool, andb b false = false. Proof. (* FILL IN HERE *) Admitted. Theorem my_S_neqb_0 : forall n : nat, (S n) =? 0 = false. Proof. (* FILL IN HERE *) Admitted. Theorem my_mult_1_l : forall n : nat, 1 * n = n. Proof. (* FILL IN HERE *) Admitted. Theorem my_all3_spec : forall b c : bool, orb (andb b c) (orb (negb b) (negb c)) = true. Proof. (* FILL IN HERE *) Admitted. Theorem my_mult_plus_distr_r : forall n m p : nat, (n + m) * p = (n * p) + (m * p). Proof. (* FILL IN HERE *) Admitted. Theorem my_mult_assoc : forall n m p : nat, n * (m * p) = (n * m) * p. Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: How many of the LLM's classifications agreed with Rocq? Were there any cases where the LLM's suggested technique failed and a different one was needed? What pattern, if any, explains which theorems require induction? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_classifying_strategies : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** The [replace] Tactic *) (** **** Exercise: 2 stars, standard (replace_vs_rewrite) Ask an LLM: _"In Rocq, when is the [replace] tactic needed instead of [rewrite]? Give an example where [rewrite add_comm] fails but [replace] succeeds."_ The following proof from [Induction.v] illustrates the issue. Step through both proof attempts below and record in the comments what happens when [rewrite add_comm] is applied in the wrong direction. *) (** This proof attempt goes wrong: *) Theorem plus_rearrange_attempt : forall n m p q : nat, (n + m) + (p + q) = (m + n) + (p + q). Proof. intros n m p q. rewrite add_comm. (* What has Rocq rewritten? Is it what we wanted? Record the resulting goal in ROCQ OBSERVATION. *) Abort. (* ROCQ OBSERVATION: what goal did Rocq produce after [rewrite add_comm] above? Why is that not what we wanted? *) (** Now prove the same theorem using [replace]: *) Theorem my_plus_rearrange : forall n m p q : nat, (n + m) + (p + q) = (m + n) + (p + q). Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM correctly explain when [replace] is needed? Did it predict which use of [+] in the goal [rewrite] would mistakenly target? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_replace_vs_rewrite : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Using LLMs as Specification Designers *) (* ================================================================= *) (** ** Defining Normalization *) (** **** Exercise: 3 stars, standard (llm_normalize) The advanced section of [Induction] introduces [normalize], a function that converts any [bin] to its canonical (no leading zeros) form. The key property it must satisfy is: << nat_to_bin (bin_to_nat b) = normalize b. >> Ask an LLM to define [my_normalize]. Rules the LLM must respect: - Do _not_ use [bin_to_nat] or [nat_to_bin] in the definition. - Do use [ai_incr] or a doubling function for [bin]. - [normalize Z = Z]. - [normalize (B0 Z) = Z] (leading zero dropped). - [normalize (B0 (B1 Z)) = B0 (B1 Z)] (non-leading zero kept). Paste the LLM's definition below and verify the examples. If any example fails, correct the definition. _Hint_: Structuring the recursion so that it _always_ reaches the end of the [bin] and processes each bit exactly once -- rather than "looking ahead" -- tends to produce the simplest definition. *) Fixpoint my_normalize (b : bin) : bin (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. Example normalize_ex1 : my_normalize Z = Z. (* FILL IN HERE *) Admitted. Example normalize_ex2 : my_normalize (B0 Z) = Z. (* FILL IN HERE *) Admitted. Example normalize_ex3 : my_normalize (B0 (B0 Z)) = Z. (* FILL IN HERE *) Admitted. Example normalize_ex4 : my_normalize (B0 (B1 Z)) = B0 (B1 Z). (* FILL IN HERE *) Admitted. Example normalize_ex5 : my_normalize (B1 (B0 (B0 Z))) = B1 Z. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM's definition pass all the examples on the first try? If not, describe the failing case and what you changed. What does a failing example tell you about an LLM's grasp of the subtle invariant (no leading zeros) this function must maintain? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_llm_normalize : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Critical Evaluation of LLMs *) (* ================================================================= *) (** ** Annotating a Proof *) (** **** Exercise: 2 stars, standard (proof_annotation) [Induction.v] presents the following compact proof of associativity of addition: << Theorem add_assoc' : forall n m p : nat, n + (m + p) = (n + m) + p. Proof. intros n m p. induction n as [| n' IHn']. reflexivity. simpl. rewrite IHn'. reflexivity. Qed. >> Ask an LLM to annotate this proof: for each tactic, it should explain what the proof state looks like _before_ and _after_ that tactic executes. Then step through the proof yourself in Rocq and compare the LLM's annotations to what Rocq actually shows. Record discrepancies below. *) (** Step through this proof in your IDE and compare to the LLM's annotations: *) Theorem add_assoc_annotated : forall n m p : nat, n + (m + p) = (n + m) + p. Proof. intros n m p. (* Proof state before [induction]: ROCQ SHOWS: ... LLM SAYS: ... *) induction n as [| n' IHn']. - (* Base case. Proof state before [reflexivity]: ROCQ SHOWS: ... LLM SAYS: ... *) reflexivity. - (* Inductive case. Proof state before [simpl]: ROCQ SHOWS: ... LLM SAYS: ... *) simpl. (* Proof state before [rewrite IHn']: ROCQ SHOWS: ... LLM SAYS: ... *) rewrite IHn'. (* Proof state before [reflexivity]: ROCQ SHOWS: ... LLM SAYS: ... *) reflexivity. Qed. (** _Reflection_: How accurate were the LLM's annotations? Did it correctly describe the induction hypothesis [IHn'] and how it changes the goal when rewritten? Were there any states where the LLM's description was subtly wrong? Write 3--4 sentences. *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_proof_annotation : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** Final Reflection *) (** **** Exercise: 2 stars, standard (final_reflection) Choose two exercises from this file that you found most revealing about LLM capabilities or limitations. For each: (a) Summarize what you asked the LLM and what it produced. (b) Describe the specific point where Rocq agreed or disagreed with the LLM. (c) Explain what the disagreement (or agreement) tells you. Then write a short paragraph (4--6 sentences) synthesizing what you have learned across all the exercises in this file and in [BasicsAI] about when LLMs are and are not reliable partners for inductive proof development. *) (* WRITTEN RESPONSE: name the two exercises, give answers to (a), (b), and (c) for each, then write your synthesis paragraph. Replace this comment with your answer. *) Definition manual_grade_for_final_reflection : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Summary *) (** The exercises in this file highlight a recurring pattern: LLMs are often good at _recognizing_ that induction is needed, but frequently miss the _helper lemmas_ that make an inductive proof go through. This is not surprising. A helper lemma like [plus_n_Sm] is needed precisely because the statement of [add_comm] does not mention it. A human mathematician discovers the helper by attempting the proof and noticing what is missing; an LLM tends to either hallucinate a proof that skips the missing step or reach for a tactic ([omega], [ring], [lia]) that sidesteps the issue entirely. Rocq's role here is clear: it is the only participant in the conversation that cannot be wrong. When Rocq rejects a proof step, the proof step is wrong -- no matter how plausible the LLM's reasoning sounds. Cultivating the habit of treating Rocq as the final word, and the LLM as a fast-but-fallible first draft, is the skill this course is building. *) (* 2026-08-10 *)