(** * ListsAI: Using LLMs to Explore Working with Structured Data *) (** This file accompanies the [Lists] 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 [Lists] make it especially interesting for LLM evaluation: reasoning about lists requires structural induction with the right induction hypothesis, and many list theorems (such as [rev_involutive]) go through only after a helper lemma (such as [rev_app_distr]) has been established. LLMs often produce plausible-looking proofs that skip precisely these helpers. _How to work through these exercises_: follow the same conventions as [BasicsAI] and [InductionAI]: - 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 [Lists.v] (and thereby on [Induction.v] and [Basics.v]). Compile in order: << rocq compile -Q . LF Basics.v rocq compile -Q . LF Induction.v rocq compile -Q . LF Lists.v rocq compile -Q . LF ListsAI.v >> *) From LF Require Export Lists. (* ================================================================= *) (** ** Provided Implementations *) (** Several exercises below involve bags (multisets). Complete implementations of [count] and [add] are provided here so that this file compiles regardless of whether you finished those exercises in [Lists]. Use these [ai_]-prefixed versions throughout this file. The list operations [app] ([++]), [length], and [rev] are given complete definitions in [Lists.v] itself, so we use them directly. *) Fixpoint ai_count (v : nat) (s : bag) : nat := match s with | nil => O | h :: t => (if h =? v then 1 else 0) + ai_count v t end. Definition ai_add (v : nat) (s : bag) : bag := v :: s. (* ################################################################# *) (** * Using LLMs as Code Generators *) (* ================================================================= *) (** ** Filtering the Nonzero Elements *) (** **** Exercise: 3 stars, standard (nonzeros_implementation) Ask an LLM to implement [my_nonzeros], a function that removes all [0]s from a list of numbers, keeping the remaining elements in order. Paste the LLM's implementation below and verify the example. Then prove [my_nonzeros_app]: that [my_nonzeros] distributes over list append. _Hint_: The proof of [my_nonzeros_app] goes by induction on the first list. In the [cons] case, you will need to reason by cases on whether the head element is [0]. If you find yourself stuck, revisit whether your definition of [my_nonzeros] matches on the head in the way the proof expects. *) Fixpoint my_nonzeros (l : natlist) : natlist (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted. Example test_my_nonzeros : my_nonzeros [0;1;0;2;3;0;0] = [1;2;3]. (* FILL IN HERE *) Admitted. Theorem my_nonzeros_app : forall l1 l2 : natlist, my_nonzeros (l1 ++ l2) = (my_nonzeros l1) ++ (my_nonzeros l2). Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM's implementation compile on the first try? Did the proof of [my_nonzeros_app] require a case analysis that the LLM did not anticipate? Describe what you changed, if anything. *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_nonzeros_implementation : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Using LLMs as Proof Generators *) (* ================================================================= *) (** ** Append Is Associative *) (** **** Exercise: 2 stars, standard (llm_app_assoc) Ask an LLM to prove associativity of list append: << forall l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3). >> 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 [l1]. Notice that [app] recurses on its first argument, so induction on [l1] lines up with how [++] computes. *) Theorem my_app_assoc : forall l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3). Proof. (* Paste the LLM's proof here, then annotate or fix it. *) (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM correctly choose to induct on [l1] rather than [l2] or [l3]? Did it explain _why_ the recursion structure of [++] makes induction on [l1] the natural choice? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_llm_app_assoc : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** Discovering the Helper Lemma for Reverse *) (** **** Exercise: 4 stars, standard (llm_rev_involutive) Ask an LLM to prove that [rev] is its own inverse: << forall l : natlist, rev (rev l) = l. >> Before looking at the LLM's answer, try proving it yourself with [induction] on [l]. 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 [my_rev_app_distr]: << forall l1 l2 : natlist, rev (l1 ++ l2) = rev l2 ++ rev l1. >> Ask the LLM: (a) Does it identify [my_rev_app_distr] as a necessary helper, or does it attempt the proof without it? (b) If it does not mention [my_rev_app_distr], does its proof actually go through in Rocq? Prove both [my_rev_app_distr] and [my_rev_involutive] below. Paste the LLM's attempts, fixing them if necessary. _Hint_: Proving [my_rev_app_distr] itself requires [app_nil_r] and [my_app_assoc] (proved above). This chain of dependencies is exactly the kind of structure LLMs tend to miss. *) (* PROOF ATTEMPT: record the goal where your manual attempt at rev (rev l) = l stalled. Replace this comment with the goal text from Rocq. *) Theorem my_rev_app_distr : forall l1 l2 : natlist, rev (l1 ++ l2) = rev l2 ++ rev l1. Proof. (* FILL IN HERE *) Admitted. Theorem my_rev_involutive : forall l : natlist, rev (rev l) = l. Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM spontaneously identify [my_rev_app_distr] as a helper, or did it attempt [rev (rev l) = l] directly? If it attempted without the helper, did the proof fail, and at which step? What does this tell you about whether LLMs track the dependency structure of inductive proofs about lists? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_llm_rev_involutive : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** The Length of a Reversed List *) (** **** Exercise: 3 stars, standard (llm_rev_length) Ask an LLM to prove that reversing a list preserves its length: << forall l : natlist, length (rev l) = length l. >> 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 the LLM did not suggest, note them in the reflection. _Hint_: Think about what [rev (h :: t)] equals, and what a lemma relating [length (l1 ++ l2)] to [length l1 + length l2] would buy you. *) (* 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_rev_length : forall l : natlist, length (rev l) = length l. 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_rev_length : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Using LLMs as Conceptual Explainers *) (* ================================================================= *) (** ** Why Pairs Need [destruct] *) (** **** Exercise: 2 stars, standard (surjective_pairing_explained) Ask an LLM: _"In Rocq, why can [(fst p, snd p) = p] not be proved by [reflexivity] for an arbitrary pair [p : natprod], and why does [destruct p] make the proof go through?"_ The following two proofs from [Lists.v] illustrate the failure and the fix. Step through them in Rocq and record your observations. *) (** This proof attempt gets stuck: *) Theorem surjective_pairing_stuck_attempt : forall (p : natprod), p = (fst p, snd p). Proof. simpl. (* What goal appears here? Why can [reflexivity] not close it? Record it in ROCQ OBSERVATION 1. *) Abort. (* ROCQ OBSERVATION 1: what goal appears after [simpl] above, and why does [reflexivity] fail on it? *) (** This proof succeeds after destructing the pair: *) Theorem surjective_pairing_works : forall (p : natprod), p = (fst p, snd p). Proof. intros p. destruct p as [n m]. (* What goal appears here now that [p] is [(n, m)]? Record it in ROCQ OBSERVATION 2. *) simpl. reflexivity. Qed. (* ROCQ OBSERVATION 2: what goal appears in the [(n, m)] case, and why does [reflexivity] now succeed? *) (** _Reflection_: Did the LLM correctly explain _why_ [reflexivity] fails on an abstract [p]? In particular, did it explain that an arbitrary [p] is not syntactically a [pair], so [fst] and [snd] cannot compute, whereas [destruct] exposes the [pair] constructor? Write 2--3 sentences evaluating the accuracy of its answer. *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_surjective_pairing_explained : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Using LLMs as Specification Designers *) (* ================================================================= *) (** ** A Property of [count] and [add] *) (** **** Exercise: 3 stars, standard (llm_count_add) Bags (multisets) are represented as [natlist]s, with [ai_count v s] counting the occurrences of [v] in [s] and [ai_add v s] inserting one copy of [v]. Ask an LLM to _state_ and _prove_ a theorem capturing the effect of [ai_add] on [ai_count] -- specifically, that adding a value [v] to a bag increases the count of [v] by exactly one: << forall (v : nat) (s : bag), ai_count v (ai_add v s) = S (ai_count v s). >> Paste the LLM's proof below and fix whatever does not compile. _Hint_: Unfold [ai_add] and let [ai_count] take one computation step; then observe what [v =? v] must reduce to. A lemma from [Induction] about [n =? n] may be useful. *) Theorem my_count_add : forall (v : nat) (s : bag), ai_count v (ai_add v s) = S (ai_count v s). Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM notice that the proof turns on [v =? v] reducing to [true]? Did it reach for the correct supporting lemma, or did it try to sidestep the obligation (e.g. with [lia] or [ring])? What does that reveal about how it reasons about a user-defined function like [ai_count]? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_llm_count_add : option (nat*string) := None. (** [] *) (* ================================================================= *) (** ** Reasoning About [natoption] *) (** **** Exercise: 2 stars, standard (llm_option_elim_hd) [Lists.v] introduces [natoption] together with [hd_error] (which returns the first element of a list as an [option]) and [option_elim] (which extracts a value from an [option], using a default for [None]). Ask an LLM to prove [option_elim_hd], relating these two functions: << forall (l : natlist) (default : nat), hd default l = option_elim default (hd_error l). >> Note that [hd_error] is an exercise in [Lists.v]; if you have not completed it, the proof will not go through. If [hd_error] is still [Admitted] in your [Lists.v], say so in the reflection and describe what the LLM's proof _would_ require. Paste the LLM's proof below and fix whatever does not compile. _Hint_: This theorem needs no induction -- a single [destruct] on [l] suffices, because [hd], [hd_error], and [option_elim] all inspect only the outermost constructor of [l]. *) Theorem my_option_elim_hd : forall (l : natlist) (default : nat), hd default l = option_elim default (hd_error l). Proof. (* FILL IN HERE *) Admitted. (** _Reflection_: Did the LLM correctly recognize that this proof needs only case analysis, not induction? If it reached for [induction], did the proof still succeed, and was the induction hypothesis ever used? *) (* WRITTEN RESPONSE: replace this comment with your answer. *) Definition manual_grade_for_llm_option_elim_hd : option (nat*string) := None. (** [] *) (* ################################################################# *) (** * Critical Evaluation of LLMs *) (* ================================================================= *) (** ** Annotating a List-Induction Proof *) (** **** Exercise: 2 stars, standard (proof_annotation) [Lists.v] proves that [nil] is a right identity for append with the following compact proof: << Theorem app_nil_r : forall l : natlist, l ++ [] = l. Proof. intros l. induction l as [| n l' IHl']. reflexivity. simpl. rewrite IHl'. 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 app_nil_r_annotated : forall l : natlist, l ++ [] = l. Proof. intros l. (* Proof state before [induction]: ROCQ SHOWS: ... LLM SAYS: ... *) induction l as [| n l' IHl']. - (* 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 IHl']: ROCQ SHOWS: ... LLM SAYS: ... *) rewrite IHl'. (* 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 [IHl'] and how it changes the goal when rewritten? Did it correctly track that the list is destructed as [n :: l'] rather than as a number? 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 the exercises in this file and in [BasicsAI] and [InductionAI] about when LLMs are and are not reliable partners for proofs about structured data. *) (* 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 reinforce a pattern first seen in [InductionAI]: LLMs are often good at _recognizing_ that structural induction is needed, but frequently miss the _helper lemmas_ that make a list proof go through. The proof of [rev_involutive] is the archetype. It depends on [rev_app_distr], which in turn depends on [app_assoc] and [app_nil_r]. None of these helpers are mentioned in the statement [rev (rev l) = l], so an LLM that reasons only from the goal text has no reason to introduce them. A human discovers the chain by attempting the proof and noticing what is missing; an LLM tends to either hallucinate a proof that skips a step or reach for an automation tactic that cannot actually close the goal. Rocq's role here is, once again, 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. Treating Rocq as the final word, and the LLM as a fast-but-fallible first draft, is the skill this course is building. *) (* 2026-09-29 *)