求Coq Contexts、evars、e* tactics教程及定理空洞填充等技术解答

Great questions! Let's break this down into parts to cover all your needs:

1. Quality Resources for Coq Contexts, Evars, and e* Tactics #

Here are some trusted resources to dive deep into these topics:

• Coq Reference Manual: The official manual has dedicated sections on Contexts and Environments (covering how Coq manages variable contexts) and Evar Manipulation Tactics (detailing eapply, eauto, evar, instantiate, and more). It’s the most authoritative source for exact syntax and behavior.
• Certified Programming with Dependent Types (CPDT): This book includes in-depth chapters on evars, existential variables, and advanced tactic usage. It walks through practical examples of using e-tactics to handle partial proofs and manage dynamic contexts.
• Coq in a Hurry: A concise community tutorial that has a section on advanced tactics, including e-tactics and context management—perfect for quick reference when you’re stuck on a specific tactic.
• Hands-on Exercises:
  • Practice defining contexts with Context (x : nat) (f : nat -> bool). and writing theorems that depend on these variables to get comfortable with context management.
  • Experiment with eapply on lemmas with existential variables, then use instantiate to fill in the gaps manually. Try using eauto with custom hint databases to automate evar resolution.

2. Building Abstract Contexts for Extraction to OCaml/Haskell #

Absolutely, this is not only feasible but a common pattern in Coq development! Here are two reliable approaches:

• Parameters/Axioms: Declare abstract variables using Parameter or Axiom to define your context. For example:

  Parameter my_abstract_func : nat -> list nat -> bool.
  Axiom func_constraint : forall n l, my_abstract_func n l = true -> n > 0.
  

  When extracted to OCaml/Haskell, these become abstract values (e.g., val my_abstract_func : int -> int list -> bool in OCaml). You can then implement these functions in your target language, just make sure to respect the Coq-side constraints to avoid runtime inconsistencies.
• Module Signatures: Use module types to define an abstract context interface, then write your proofs within a functor that takes this interface as a parameter. Example:

  Module Type ABSTRACT_CONTEXT.
    Parameter process_data : string -> nat.
    Axiom process_valid : forall s, process_data s >= 0.
  End ABSTRACT_CONTEXT.
  
  Module MyCertifiedCode (Ctx : ABSTRACT_CONTEXT).
    Theorem data_safe : forall s, Ctx.process_data s >= 0.
    Proof. apply Ctx.process_valid. Qed.
  End MyCertifiedCode.
  

  Extraction will generate a module type in OCaml/Haskell; you can then create a concrete module implementing process_data and pass it to MyCertifiedCode to get the fully functional extracted code.

3. Resources for Theorem Holes and Filling Them #

Theorem holes (placeholders like Admit, admit, or evar ? markers) are a key part of iterative proof development. Here’s how to learn about filling them:

• Key Concepts & Tactics:
  • For Admitted theorems: Reopen the proof later with Proof. followed by your proof script, then replace Admit with Qed. once complete.
  • For evar holes (?): Use instantiate n with (term) to manually fill the nth evar, or let e-tactics like eauto or eapply resolve them automatically. You can also use show to inspect the current evars and their types.
• Resources:
  • CPDT: The Proof Management chapter covers handling partial proofs, evar resolution, and filling holes systematically.
  • Software Foundations (Logical Foundations): Volume 1 includes exercises on proof strategies, where you’ll practice filling in incomplete proofs and using tactics to resolve gaps.
  • Coq Reference Manual: The Proof Handling section details the syntax and behavior of admit, evar, and related tactics for managing proof holes.
• Practice Tips: Start with simple theorems, intentionally leave holes (e.g., use admit in the middle of a proof), then work backwards to fill them. Experiment with eauto with different hint levels to see how it resolves evars automatically.

内容的提问来源于stack exchange，提问作者rausted