Coq/Lean 交互式教程

3.1 依赖类型

依赖类型是 Coq 和 Lean 类型系统的核心特性，允许类型依赖于值。这使得我们可以编写更精确的规范。

依赖函数类型对比

(* 依赖函数类型的例子 *)
Definition identity : forall (A : Type), A -> A :=
  fun A x => x.

(* 类型依赖于参数 *)
Definition zero_or_succ : forall (b : bool), if b then nat else bool :=
  fun b => if b then 0 else false.

-- 依赖函数类型的例子
def identity : (A : Type) → A → A :=
  fun A x => x

-- 类型依赖于参数
def zeroOrSucc : (b : Bool) → if b then Nat else Bool :=
  fun b => if b then 0 else false

依赖对（Σ类型）

(* 使用 sig 定义依赖对 *)
Definition positive_nat : Type := 
  { n : nat | n > 0 }.

(* 构造依赖对 *)
Definition one_positive : positive_nat.
Proof.
  exists 1.
  auto.
Defined.

(* 另一种写法 *)
Definition two_positive : positive_nat :=
  exist _ 2 (gt_Sn_O 1).

(* 提取值和证明 *)
Definition get_value (p : positive_nat) : nat :=
  match p with
  | exist _ n _ => n
  end.

Definition get_proof (p : positive_nat) : get_value p > 0 :=
  match p with
  | exist _ _ proof => proof
  end.

向量（长度索引列表）

Inductive vec (A : Type) : nat -> Type :=
  | vnil : vec A 0
  | vcons : forall n, A -> vec A n -> vec A (S n).

Arguments vnil {A}.
Arguments vcons {A n}.

(* 向量的例子 *)
Definition vec_123 : vec nat 3 :=
  vcons 1 (vcons 2 (vcons 3 vnil)).

(* 安全的头函数 *)
Definition vhead {A : Type} {n : nat} (v : vec A (S n)) : A :=
  match v with
  | vcons _ h _ => h
  end.

(* 安全的尾函数 *)
Definition vtail {A : Type} {n : nat} (v : vec A (S n)) : vec A n :=
  match v with
  | vcons _ _ t => t
  end.

Fixpoint vmap {A B : Type} {n : nat} (f : A -> B) (v : vec A n) : vec B n :=
  match v with
  | vnil => vnil
  | vcons _ h t => vcons (f h) (vmap f t)
  end.

(* 测试 *)
Definition double (n : nat) : nat := n * 2.
Compute vmap double vec_123. (* = vcons 2 (vcons 4 (vcons 6 vnil)) *)

Fixpoint vappend {A : Type} {n m : nat} 
  (v1 : vec A n) (v2 : vec A m) : vec A (n + m) :=
  match v1 with
  | vnil => v2           (* n = 0, 所以 vec A (0 + m) = vec A m *)
  | vcons _ h t =>       (* n = S n', t : vec A n' *)
    vcons h (vappend t v2)  
    (* vappend t v2 : vec A (n' + m) *)
    (* vcons h _ : vec A (S (n' + m)) = vec A (S n' + m) = vec A (n + m) *)
  end.

(* 测试 *)
Example test_vappend : 
  vappend (vcons 1 (vcons 2 vnil)) (vcons 3 vnil) = 
  vcons 1 (vcons 2 (vcons 3 vnil)).
Proof. reflexivity. Qed.

依赖模式匹配

(* convoy 模式 *)
Definition vhead' {A : Type} {n : nat} (v : vec A n) : 
  match n with
  | 0 => unit
  | S _ => A
  end :=
  match v in vec _ m return 
    match m with
    | 0 => unit
    | S _ => A
    end
  with
  | vnil => tt
  | vcons _ h _ => h
  end.

(* 使用依赖类型确保安全性 *)
Definition safe_div : forall (n m : nat), m <> 0 -> nat.
  intros n m H.
  exact (n / m).
Defined.

Definition bounded_nat (n : nat) : Type :=
  { m : nat | m < n }.

(* 构造函数 *)
Definition mk_bounded {n : nat} (m : nat) (H : m < n) : bounded_nat n :=
  exist _ m H.

(* 零（对于 n > 0）*)
Definition bzero {n : nat} (H : 0 < n) : bounded_nat n :=
  exist _ 0 H.

(* 后继（安全的）*)
Definition bsucc {n : nat} (b : bounded_nat n) : option (bounded_nat n).
  destruct b as [m Hm].
  destruct (S m <? n) eqn:E.
  - apply Some. exists (S m).
    apply Nat.ltb_lt. assumption.
  - exact None.
Defined.

3.2 高阶函数与证明

高阶函数是函数式编程的核心，在 Coq 和 Lean 中它们也是证明的重要工具。

Map、Filter 和 Fold 对比

Require Import List.
Import ListNotations.

(* map 的定义和性质 *)
Fixpoint map {A B : Type} (f : A -> B) (l : list A) : list B :=
  match l with
  | [] => []
  | h :: t => (f h) :: (map f t)
  end.

-- map 的定义和性质
def map {α β : Type} (f : α → β) : List α → List β
  | [] => []
  | h :: t => f h :: map f t

函数组合

(* 函数组合 *)
Definition compose {A B C : Type} (g : B -> C) (f : A -> B) : A -> C :=
  fun x => g (f x).

Notation "g ∘ f" := (compose g f) (at level 40, left associativity).

(* 组合的性质 *)
Theorem compose_assoc : forall A B C D (h : C -> D) (g : B -> C) (f : A -> B),
  (h ∘ g) ∘ f = h ∘ (g ∘ f).
Proof.
  intros. reflexivity.
Qed.

(* map 与组合的关系 *)
Theorem map_compose : forall A B C (g : B -> C) (f : A -> B) (l : list A),
  map g (map f l) = map (g ∘ f) l.
Proof.
  intros A B C g f l.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.

高阶谓词

(* 所有元素满足谓词 *)
Fixpoint all {A : Type} (P : A -> bool) (l : list A) : bool :=
  match l with
  | [] => true
  | h :: t => P h && all P t
  end.

(* 存在元素满足谓词 *)
Fixpoint any {A : Type} (P : A -> bool) (l : list A) : bool :=
  match l with
  | [] => false
  | h :: t => P h || any P t
  end.

(* 高阶谓词的性质 *)
Theorem all_forall : forall A (P : A -> bool) (l : list A),
  all P l = true <-> forall x, In x l -> P x = true.
Proof.
  intros A P l.
  split.
  - (* -> *)
    intros H x Hin.
    induction l.
    + inversion Hin.
    + simpl in H. apply andb_prop in H.
      destruct H as [Ha Ht].
      destruct Hin.
      * subst. assumption.
      * apply IHl; assumption.
  - (* <- *)
    intros H.
    induction l.
    + reflexivity.
    + simpl. apply andb_true_intro.
      split.
      * apply H. left. reflexivity.
      * apply IHl. intros x Hin.
        apply H. right. assumption.
Qed.

Theorem filter_app : forall A (P : A -> bool) (l1 l2 : list A),
  filter P (l1 ++ l2) = filter P l1 ++ filter P l2.
Proof.
  intros A P l1 l2.
  induction l1 as [| a l1' IHl1'].
  - (* l1 = [] *)
    simpl.  (* filter P ([] ++ l2) = filter P l2 *)
            (* filter P [] ++ filter P l2 = [] ++ filter P l2 = filter P l2 *)
    reflexivity.
    
  - (* l1 = a :: l1' *)
    simpl.  (* 左边: filter P ((a :: l1') ++ l2) = filter P (a :: (l1' ++ l2)) *)
            (* 右边: filter P (a :: l1') ++ filter P l2 *)
    
    destruct (P a) eqn:HPa.  (* 对 P a 的值进行分情况讨论 *)
    
    + (* P a = true *)
      simpl.  (* 左边: a :: filter P (l1' ++ l2) *)
              (* 右边: a :: (filter P l1' ++ filter P l2) *)
      rewrite IHl1'.  (* 应用归纳假设 *)
      reflexivity.
      
    + (* P a = false *)
      (* 左边: filter P (l1' ++ l2) *)
      (* 右边: filter P l1' ++ filter P l2 *)
      assumption.  (* 这正是归纳假设 IHl1' *)
Qed.

Fixpoint partition {A : Type} (P : A -> bool) (l : list A) 
  : list A * list A :=
  match l with
  | [] => ([], [])
  | h :: t =>
    let (yes, no) := partition P t in
    if P h then (h :: yes, no)
    else (yes, h :: no)
  end.

(* 性质：partition 保持元素 *)
Theorem partition_elements : forall A (P : A -> bool) (l : list A),
  let (yes, no) := partition P l in
  l = yes ++ no \/ l = no ++ yes.
Proof.
  (* 证明略，需要仔细的归纳 *)
Admitted.

函数外延性

(* 函数外延性公理 *)
Axiom functional_extensionality : forall A B (f g : A -> B),
  (forall x, f x = g x) -> f = g.

(* 使用函数外延性的例子 *)
Theorem compose_id_left : forall A B (f : A -> B),
  (fun x => x) ∘ f = f.
Proof.
  intros A B f.
  apply functional_extensionality.
  intros x. reflexivity.
Qed.

3.3 类型类（Type Classes）

类型类提供了一种组织和使用多态函数的方式，类似于 Haskell 的类型类。

定义类型类

(* 定义 Eq 类型类 *)
Class Eq (A : Type) := {
  eqb : A -> A -> bool;
  eqb_refl : forall x, eqb x x = true;
  eqb_sym : forall x y, eqb x y = eqb y x;
  eqb_trans : forall x y z, 
    eqb x y = true -> eqb y z = true -> eqb x z = true
}.

(* 定义 Show 类型类 *)
Class Show (A : Type) := {
  show : A -> string
}.

(* 定义 Monoid 类型类 *)
Class Monoid (A : Type) := {
  mempty : A;
  mappend : A -> A -> A;
  mappend_assoc : forall x y z, 
    mappend x (mappend y z) = mappend (mappend x y) z;
  mappend_id_l : forall x, mappend mempty x = x;
  mappend_id_r : forall x, mappend x mempty = x
}.

实例声明

(* nat 的 Eq 实例 *)
Instance nat_eq : Eq nat := {
  eqb := Nat.eqb
}.
Proof.
  - apply Nat.eqb_refl.
  - apply Nat.eqb_sym.
  - intros x y z H1 H2.
    apply Nat.eqb_eq in H1.
    apply Nat.eqb_eq in H2.
    subst. apply Nat.eqb_refl.
Defined.

(* list 的 Monoid 实例 *)
Instance list_monoid {A : Type} : Monoid (list A) := {
  mempty := [];
  mappend := @app A
}.
Proof.
  - apply app_assoc.
  - reflexivity.
  - apply app_nil_r.
Defined.

(* nat 的 Show 实例 *)
Require Import String.
Open Scope string_scope.

Instance nat_show : Show nat := {
  show := fun n => 
    match n with
    | 0 => "0"
    | 1 => "1"
    | 2 => "2"
    | _ => "..."
    end
}.

使用类型类

(* 泛型函数使用类型类 *)
Definition elem {A : Type} `{Eq A} (x : A) (l : list A) : bool :=
  fold_right (fun y acc => eqb x y || acc) false l.

(* 上下文约束 *)
Definition show_pair {A B : Type} `{Show A} `{Show B} 
  (p : A * B) : string :=
  "(" ++ show (fst p) ++ ", " ++ show (snd p) ++ ")".

(* 多个约束 *)
Definition show_if_equal {A : Type} `{Eq A} `{Show A} 
  (x y : A) : string :=
  if eqb x y then show x else "not equal".

(* 使用 Monoid *)
Definition concat_all {A : Type} `{Monoid A} (l : list A) : A :=
  fold_right mappend mempty l.

Class Ord (A : Type) `{Eq A} := {
  le : A -> A -> bool;
  le_refl : forall x, le x x = true;
  le_trans : forall x y z, 
    le x y = true -> le y z = true -> le x z = true;
  le_antisym : forall x y,
    le x y = true -> le y x = true -> eqb x y = true
}.

Instance nat_ord : Ord nat := {
  le := Nat.leb
}.
Proof.
  - intros x. apply Nat.leb_refl.
  - intros x y z.
    repeat rewrite Nat.leb_le.
    apply Nat.le_trans.
  - intros x y.
    repeat rewrite Nat.leb_le.
    intros H1 H2.
    apply Nat.eqb_eq.
    apply Nat.le_antisymm; assumption.
Defined.

(* 插入排序实现 *)
Fixpoint insert {A : Type} `{Ord A} (x : A) (l : list A) : list A :=
  match l with
  | [] => [x]              (* 空列表：直接返回单元素列表 *)
  | h :: t =>              (* 非空列表：比较 x 和头部元素 h *)
    if le x h then         (* 如果 x <= h *)
      x :: h :: t          (* x 插入到最前面 *)
    else                   (* 否则 *)
      h :: insert x t      (* 保留 h，递归地将 x 插入尾部 *)
  end.

Fixpoint sort {A : Type} `{Ord A} (l : list A) : list A :=
  match l with
  | [] => []               (* 空列表已排序 *)
  | h :: t =>              (* 非空列表 *)
    insert h (sort t)      (* 先排序尾部，然后插入头部 *)
  end.

(* 测试 - 使用 nat 的 Ord 实例 *)
Compute sort [3; 1; 4; 1; 5; 9; 2; 6].
(* = [1; 1; 2; 3; 4; 5; 6; 9] *)

(* 可选：证明排序的正确性 *)
Lemma insert_sorted : forall {A : Type} `{Ord A} (x : A) (l : list A),
  sorted l -> sorted (insert x l).
(* 证明略 *)

3.4 自动化证明

Coq 提供了多种自动化策略来简化证明过程。

auto 和 eauto

(* auto 使用基本的证明搜索 *)
Theorem auto_example : forall P Q R : Prop,
  (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  auto.  (* 自动完成证明 *)
Qed.

(* auto 的深度控制 *)
Theorem auto_depth : forall P Q R S : Prop,
  (P -> Q) -> (Q -> R) -> (R -> S) -> P -> S.
Proof.
  auto 4.  (* 搜索深度为 4 *)
Qed.

(* eauto 使用存在量词 *)
Theorem eauto_example : forall (A : Type) (P : A -> Prop),
  (exists x, P x) -> exists y, P y.
Proof.
  eauto.
Qed.

omega 和 lia

Require Import Omega.
Require Import Lia.

(* omega 解决线性算术 *)
Theorem omega_example : forall n m : nat,
  n + m = m + n.
Proof.
  intros. omega.
Qed.

(* lia 是 omega 的现代版本 *)
Theorem lia_example : forall x y z : nat,
  x < y -> y < z -> x + 2 < z + 1.
Proof.
  intros. lia.
Qed.

(* 复杂的线性不等式 *)
Theorem complex_ineq : forall a b c : nat,
  a + b < c -> 2 * a + 2 * b < 2 * c.
Proof.
  intros. lia.
Qed.

ring 和 field

Require Import Ring.
Require Import Field.

(* ring 解决环上的等式 *)
Theorem ring_example : forall x y : nat,
  (x + y) * (x + y) = x * x + 2 * x * y + y * y.
Proof.
  intros. ring.
Qed.

(* 对于有理数域 *)
Require Import QArith.
Open Scope Q_scope.

Theorem field_example : forall x y : Q,
  y <> 0 -> (x + y) / y = x / y + 1.
Proof.
  intros. field. assumption.
Qed.

Hint 数据库

(* 创建自定义 Hint 数据库 *)
Create HintDb mybase.

Theorem my_lemma1 : forall n : nat, n + 0 = n.
Proof. auto. Qed.

Theorem my_lemma2 : forall n : nat, 0 + n = n.
Proof. auto. Qed.

(* 添加到数据库 *)
Hint Resolve my_lemma1 : mybase.
Hint Resolve my_lemma2 : mybase.

(* 使用数据库 *)
Theorem use_hints : forall n m : nat,
  (n + 0) + (0 + m) = n + m.
Proof.
  intros. auto with mybase.
Qed.

(* Hint 的不同模式 *)
Hint Immediate my_lemma1 : mybase.  (* 立即应用 *)
Hint Unfold plus : mybase.          (* 展开定义 *)
Hint Constructors nat : mybase.     (* 使用构造器 *)

Ltac 编程基础

(* 定义自定义策略 *)
Ltac my_auto := 
  intros; 
  repeat (simpl; auto).

(* 条件策略 *)
Ltac break_match :=
  match goal with
  | [ |- context[match ?X with _ => _ end] ] => destruct X
  end.

(* 重复应用 *)
Ltac crush :=
  intros;
  repeat (break_match; simpl; auto).

(* 使用自定义策略 *)
Theorem custom_tactic_example : forall b1 b2 : bool,
  (if b1 then true else false) = b1.
Proof.
  crush.
Qed.

(* 更复杂的 Ltac *)
Ltac inv H := inversion H; clear H; subst.

Ltac find_rewrite :=
  match goal with
  | [ H : ?X = ?Y |- context[?X] ] => rewrite H
  end.

Ltac solve_by_inversion :=
  intros; 
  match goal with
  | [ H : _ |- _ ] => inv H; auto
  end.

Ltac solve_bool :=
  intros;
  repeat match goal with
  | [ |- context[if ?X then _ else _] ] => destruct X
  | [ |- context[_ && _] ] => apply andb_true_intro; split
  | [ |- context[_ || _] ] => apply orb_true_intro
  | [ H : ?X = true |- context[?X] ] => rewrite H
  | [ H : ?X = false |- context[?X] ] => rewrite H
  | _ => simpl; auto
  end.

(* 测试 *)
Theorem test_solve_bool : forall b1 b2 : bool,
  b1 = true -> b2 = true -> b1 && b2 = true.
Proof.
  solve_bool.
Qed.

Create HintDb listbase.

(* 添加基本引理 *)
Hint Resolve app_nil_l app_nil_r : listbase.
Hint Resolve app_assoc : listbase.
Hint Resolve in_eq in_cons : listbase.

(* 自定义引理 *)
Lemma in_app_iff : forall A (l1 l2 : list A) (x : A),
  In x (l1 ++ l2) <-> In x l1 \/ In x l2.
Proof.
  intros. split.
  - apply in_app_or.
  - apply in_or_app.
Qed.

Hint Resolve -> in_app_iff : listbase.
Hint Resolve <- in_app_iff : listbase.

(* 使用数据库 *)
Theorem test_listbase : forall A (x : A) (l : list A),
  In x (l ++ [x]).
Proof.
  intros. auto with listbase.
Qed.

3.5 归纳-递归类型

本节探讨更复杂的归纳类型定义，包括嵌套归纳、相互归纳和归纳-递归定义。

嵌套归纳类型

(* 嵌套列表 *)
Inductive nested_list (A : Type) : Type :=
  | NNil : nested_list A
  | NCons : A -> nested_list A -> nested_list A
  | NNest : nested_list (nested_list A) -> nested_list A.

(* 展平嵌套列表 *)
Fixpoint flatten {A : Type} (nl : nested_list A) : list A :=
  match nl with
  | NNil _ => []
  | NCons _ x xs => x :: flatten xs
  | NNest _ nls => 
      flat_map flatten (flatten_nested nls)
  end
with flatten_nested {A : Type} (nl : nested_list (nested_list A)) 
  : list (nested_list A) :=
  match nl with
  | NNil _ => []
  | NCons _ x xs => x :: flatten_nested xs
  | NNest _ _ => [] (* 防止无限嵌套 *)
  end.

相互归纳类型

(* 偶数和奇数的相互定义 *)
Inductive even : nat -> Prop :=
  | even_O : even 0
  | even_S : forall n, odd n -> even (S n)
with odd : nat -> Prop :=
  | odd_S : forall n, even n -> odd (S n).

(* 相互递归函数 *)
Fixpoint evenb (n : nat) : bool :=
  match n with
  | 0 => true
  | S n' => oddb n'
  end
with oddb (n : nat) : bool :=
  match n with
  | 0 => false
  | S n' => evenb n'
  end.

(* 证明它们的关系 *)
Theorem even_evenb : forall n,
  even n <-> evenb n = true.
Proof.
  intros n.
  split.
  - intros H. induction H.
    + reflexivity.
    + simpl. assumption.
  - intros H. 
    (* 需要相互归纳，这里省略 *)
Admitted.

归纳族（Inductive Families）

(* 有限集合的表示 *)
Inductive fin : nat -> Type :=
  | F1 : forall n, fin (S n)
  | FS : forall n, fin n -> fin (S n).

(* fin n 有恰好 n 个元素 *)
Definition fin_to_nat {n : nat} (f : fin n) : nat :=
  match f with
  | F1 _ => 0
  | FS _ f' => S (fin_to_nat f')
  end.

(* 类型安全的列表索引 *)
Fixpoint nth_fin {A : Type} {n : nat} 
  (l : vec A n) (i : fin n) : A :=
  match i in fin m return vec A m -> A with
  | F1 n' => fun l => 
      match l with
      | vcons _ h _ => h
      end
  | FS n' i' => fun l =>
      match l with
      | vcons _ _ t => nth_fin t i'
      end
  end l.

归纳-递归定义

(* 良基树：每个节点的子树列表是有限的 *)
Inductive tree (A : Type) : Type :=
  | Leaf : A -> tree A
  | Node : list (tree A) -> tree A.

(* 树的大小 *)
Fixpoint tree_size {A : Type} (t : tree A) : nat :=
  match t with
  | Leaf _ => 1
  | Node ts => S (trees_size ts)
  end
with trees_size {A : Type} (ts : list (tree A)) : nat :=
  match ts with
  | [] => 0
  | t :: ts' => tree_size t + trees_size ts'
  end.

(* 更复杂的例子：带约束的归纳类型 *)
Inductive sorted_list : nat -> Type :=
  | sorted_nil : sorted_list 0
  | sorted_cons : forall (n : nat) (l : sorted_list n),
      n <= (hd n l) -> sorted_list n
with hd (default : nat) {n : nat} (l : sorted_list n) : nat :=
  match l with
  | sorted_nil => default
  | sorted_cons x _ _ => x
  end.

终止性证明

(* 使用 Program 处理复杂的终止性 *)
Require Import Program.

Program Fixpoint merge (l1 l2 : list nat) 
  {measure (length l1 + length l2)} : list nat :=
  match l1, l2 with
  | [], _ => l2
  | _, [] => l1
  | h1 :: t1, h2 :: t2 =>
      if h1 <=? h2 
      then h1 :: merge t1 l2
      else h2 :: merge l1 t2
  end.
Next Obligation.
  simpl. lia.
Defined.
Next Obligation.
  simpl. lia.
Defined.

(* 使用 Function 定义 *)
Require Import Recdef.

Function ack (n m : nat) {wf lt n} : nat :=
  match n with
  | 0 => S m
  | S n' =>
      match m with
      | 0 => ack n' 1
      | S m' => ack n' (ack n m')
      end
  end.
Proof.
  - intros. simpl. auto.
  - intros. simpl. auto.
  - apply lt_wf.
Defined.

Require Import String.

(* JSON 值的归纳定义 *)
Inductive json : Type :=
  | JNull : json                                (* null *)
  | JBool : bool -> json                        (* true/false *)
  | JNumber : nat -> json                       (* 简化：只用自然数 *)
  | JString : string -> json                    (* "..." *)
  | JArray : list json -> json                  (* [...] *)
  | JObject : list (string * json) -> json.     (* {...} *)

(* 计算 JSON 值的大小 - 展示相互递归 *)
Fixpoint json_size (j : json) : nat :=
  match j with
  | JNull => 1
  | JBool _ => 1  
  | JNumber _ => 1
  | JString _ => 1
  | JArray l => S (json_list_size l)      (* 1 + 数组内容大小 *)
  | JObject l => S (json_pairs_size l)    (* 1 + 对象内容大小 *)
  end
with json_list_size (l : list json) : nat :=
  match l with
  | [] => 0
  | j :: js => json_size j + json_list_size js
  end
with json_pairs_size (l : list (string * json)) : nat :=
  match l with
  | [] => 0
  | (_, j) :: ps => json_size j + json_pairs_size ps
  end.

Inductive btree (A : Type) : Type :=
  | BLeaf : btree A
  | BNode : A -> btree A -> btree A -> btree A.

Fixpoint height {A : Type} (t : btree A) : nat :=
  match t with
  | BLeaf _ => 0
  | BNode _ l r => S (max (height l) (height r))
  end.

Inductive balanced {A : Type} : btree A -> Prop :=
  | balanced_leaf : balanced (BLeaf A)
  | balanced_node : forall x l r,
      balanced l ->
      balanced r ->
      (height l = height r \/ 
       height l = S (height r) \/ 
       S (height l) = height r) ->
      balanced (BNode A x l r).

(* 平衡树的高度是对数级的 *)
Theorem balanced_height_log : forall A (t : btree A),
  balanced t -> 
  (* 省略具体的对数关系 *)
  True.
Proof.
  (* 证明略 *)
  trivial.
Qed.

Program Fixpoint quicksort (l : list nat) 
  {measure (length l)} : list nat :=
  match l with
  | [] => []
  | x :: xs =>
      let lesser := filter (fun y => y <? x) xs in
      let greater := filter (fun y => negb (y <? x)) xs in
      quicksort lesser ++ [x] ++ quicksort greater
  end.
Next Obligation.
  (* lesser 的长度小于原列表 *)
  apply filter_length.
Defined.
Next Obligation.
  (* greater 的长度小于原列表 *)
  apply filter_length.
Defined.

4.1 数据结构验证

本节展示如何在 Coq 中实现和验证常见的数据结构。

平衡二叉搜索树

(* 二叉搜索树的定义 *)
Inductive BST (A : Type) : Type :=
  | Empty : BST A
  | Node : A -> BST A -> BST A -> BST A.

(* 插入操作 *)
Fixpoint insert {A : Type} `{Ord A} (x : A) (t : BST A) : BST A :=
  match t with
  | Empty _ => Node _ x (Empty _) (Empty _)
  | Node _ y l r =>
      if le x y then Node _ y (insert x l) r
      else Node _ y l (insert x r)
  end.

(* BST 性质的归纳定义 *)
Inductive is_bst {A : Type} `{Ord A} : BST A -> Prop :=
  | bst_empty : is_bst (Empty A)
  | bst_node : forall x l r,
      is_bst l ->
      is_bst r ->
      (forall y, In_bst y l -> le y x = true) ->
      (forall y, In_bst y r -> le x y = true) ->
      is_bst (Node A x l r)
with In_bst {A : Type} : A -> BST A -> Prop :=
  | in_here : forall x l r, In_bst x (Node A x l r)
  | in_left : forall x y l r, In_bst x l -> In_bst x (Node A y l r)
  | in_right : forall x y l r, In_bst x r -> In_bst x (Node A y l r).

(* 插入保持 BST 性质 *)
Theorem insert_preserves_bst : forall A `{Ord A} (x : A) (t : BST A),
  is_bst t -> is_bst (insert x t).
Proof.
  intros A H x t Hbst.
  induction Hbst.
  - simpl. constructor; try constructor; intros y Hin; inversion Hin.
  - simpl. destruct (le x x0) eqn:Hle.
    + constructor.
      * apply IHHbst1.
      * assumption.
      * intros y Hin. (* 证明略 *)
Admitted.

红黑树

(* 颜色定义 *)
Inductive color : Type := Red | Black.

(* 红黑树定义 *)
Inductive RBTree (A : Type) : Type :=
  | Leaf : RBTree A
  | Node : color -> A -> RBTree A -> RBTree A -> RBTree A.

(* 红黑树不变量 *)
Inductive is_red_black {A : Type} : nat -> RBTree A -> Prop :=
  | rb_leaf : is_red_black 1 (Leaf A)
  | rb_red : forall n x l r,
      is_red_black n l ->
      is_red_black n r ->
      is_red_black n (Node A Red x l r)
  | rb_black : forall n x l r,
      is_red_black n l ->
      is_red_black n r ->
      is_red_black (S n) (Node A Black x l r).

(* 没有连续的红节点 *)
Inductive no_red_red {A : Type} : RBTree A -> Prop :=
  | nrr_leaf : no_red_red (Leaf A)
  | nrr_black : forall x l r,
      no_red_red l ->
      no_red_red r ->
      no_red_red (Node A Black x l r)
  | nrr_red : forall x l r,
      no_red_red l ->
      no_red_red r ->
      is_black l ->
      is_black r ->
      no_red_red (Node A Red x l r)
with is_black {A : Type} : RBTree A -> Prop :=
  | black_leaf : is_black (Leaf A)
  | black_node : forall x l r,
      is_black (Node A Black x l r).

函数式队列

(* 使用两个列表实现队列 *)
Record queue (A : Type) : Type := mk_queue {
  front : list A;
  rear : list A
}.

(* 队列操作 *)
Definition empty_queue {A : Type} : queue A :=
  mk_queue A [] [].

Definition enqueue {A : Type} (x : A) (q : queue A) : queue A :=
  mk_queue A (front A q) (x :: rear A q).

Definition dequeue {A : Type} (q : queue A) : option (A * queue A) :=
  match front A q with
  | [] => 
      match rev (rear A q) with
      | [] => None
      | h :: t => Some (h, mk_queue A t [])
      end
  | h :: t => Some (h, mk_queue A t (rear A q))
  end.

(* 队列的抽象表示 *)
Definition queue_to_list {A : Type} (q : queue A) : list A :=
  front A q ++ rev (rear A q).

(* 正确性定理 *)
Theorem enqueue_correct : forall A (x : A) (q : queue A),
  queue_to_list (enqueue x q) = queue_to_list q ++ [x].
Proof.
  intros. unfold queue_to_list, enqueue. simpl.
  rewrite rev_cons. rewrite app_assoc. reflexivity.
Qed.

(* 完全二叉树表示的堆 *)
Inductive heap : Type :=
  | HEmpty : heap
  | HNode : nat -> nat -> heap -> heap -> heap.
  (* 第一个 nat 是值，第二个是大小 *)

(* 堆性质 *)
Inductive is_heap : heap -> Prop :=
  | heap_empty : is_heap HEmpty
  | heap_node : forall v s l r,
      is_heap l ->
      is_heap r ->
      (forall x, heap_min l = Some x -> v <= x) ->
      (forall x, heap_min r = Some x -> v <= x) ->
      is_heap (HNode v s l r)
with heap_min : heap -> option nat :=
  | min_empty : heap_min HEmpty = None
  | min_node : forall v s l r,
      heap_min (HNode v s l r) = Some v.

(* 插入操作 *)
Fixpoint heap_insert (x : nat) (h : heap) : heap :=
  match h with
  | HEmpty => HNode x 1 HEmpty HEmpty
  | HNode v s l r =>
      if x <=? v then
        (* x 成为新根 *)
        if size l <=? size r then
          HNode x (S s) (heap_insert v l) r
        else
          HNode x (S s) l (heap_insert v r)
      else
        (* v 保持为根 *)
        if size l <=? size r then
          HNode v (S s) (heap_insert x l) r
        else
          HNode v (S s) l (heap_insert x r)
  end
where size (h : heap) : nat :=
  match h with
  | HEmpty => 0
  | HNode _ s _ _ => s
  end.

4.2 算法正确性

本节展示如何验证经典算法的正确性。

排序算法验证

(* 排序的规范 *)
Definition sorted (l : list nat) : Prop :=
  forall i j, i < j < length l -> 
    nth i l 0 <= nth j l 0.

(* 排列关系 *)
Definition permutation (l1 l2 : list nat) : Prop :=
  forall x, count_occ Nat.eq_dec l1 x = count_occ Nat.eq_dec l2 x.

(* 插入排序的实现 *)
Fixpoint insert_sorted (x : nat) (l : list nat) : list nat :=
  match l with
  | [] => [x]
  | h :: t => 
      if x <=? h then x :: h :: t
      else h :: insert_sorted x t
  end.

Fixpoint insertion_sort (l : list nat) : list nat :=
  match l with
  | [] => []
  | h :: t => insert_sorted h (insertion_sort t)
  end.

(* 正确性证明 *)
Theorem insertion_sort_correct : forall l : list nat,
  sorted (insertion_sort l) /\ 
  permutation l (insertion_sort l).
Proof.
  intros l.
  split.
  - (* 排序性 *)
    induction l.
    + unfold sorted. intros. simpl in H. lia.
    + simpl. (* 证明需要关于 insert_sorted 的引理 *)
Admitted.

(* 归并排序 *)
Fixpoint split {A : Type} (l : list A) : list A * list A :=
  match l with
  | [] => ([], [])
  | [x] => ([x], [])
  | x :: y :: t =>
      let (l1, l2) := split t in
      (x :: l1, y :: l2)
  end.

Fixpoint merge (l1 l2 : list nat) : list nat :=
  match l1, l2 with
  | [], _ => l2
  | _, [] => l1
  | h1 :: t1, h2 :: t2 =>
      if h1 <=? h2 
      then h1 :: merge t1 l2
      else h2 :: merge l1 t2
  end.

Function merge_sort (l : list nat) {measure length l} : list nat :=
  match l with
  | [] => []
  | [x] => [x]
  | _ => 
      let (l1, l2) := split l in
      merge (merge_sort l1) (merge_sort l2)
  end.
Proof.
  (* 终止性证明 *)
  - intros. (* split 产生更小的列表 *)
Admitted.

搜索算法验证

(* 二分搜索 *)
Fixpoint binary_search_aux (l : list nat) (x : nat) 
  (lo hi : nat) (fuel : nat) : option nat :=
  match fuel with
  | O => None
  | S fuel' =>
      if hi <=? lo then None
      else
        let mid := (lo + hi) / 2 in
        match nth_error l mid with
        | None => None
        | Some y =>
            if x =? y then Some mid
            else if x <? y 
                 then binary_search_aux l x lo mid fuel'
                 else binary_search_aux l x (S mid) hi fuel'
        end
  end.

Definition binary_search (l : list nat) (x : nat) : option nat :=
  binary_search_aux l x 0 (length l) (length l).

(* 正确性规范 *)
Theorem binary_search_correct : forall l x,
  sorted l ->
  match binary_search l x with
  | Some i => nth_error l i = Some x
  | None => ~ In x l
  end.
Proof.
  (* 需要对 binary_search_aux 进行归纳 *)
Admitted.

图算法

(* 图的表示 *)
Definition graph := nat -> list nat.

(* 深度优先搜索 *)
Fixpoint dfs_visit (g : graph) (visited : list nat) 
  (v : nat) (fuel : nat) : list nat :=
  match fuel with
  | O => visited
  | S fuel' =>
      if existsb (Nat.eqb v) visited 
      then visited
      else
        let visited' := v :: visited in
        fold_left (fun acc u => dfs_visit g acc u fuel') 
                  (g v) visited'
  end.

(* 路径存在性 *)
Inductive path (g : graph) : nat -> nat -> list nat -> Prop :=
  | path_nil : forall v, path g v v []
  | path_cons : forall u v w p,
      In w (g u) ->
      path g w v p ->
      path g u v (u :: p).

(* DFS 的正确性 *)
Theorem dfs_finds_path : forall g u v fuel,
  fuel >= length (nodes g) ->
  (exists p, path g u v p) <-> 
  In v (dfs_visit g [] u fuel).
Proof.
  (* 证明略 *)
Admitted.

(* 带权图 *)
Definition weighted_graph := nat -> list (nat * nat).
(* (节点, 权重) 对的列表 *)

(* 距离映射 *)
Definition dist_map := nat -> option nat.

(* 更新距离 *)
Definition update_dist (d : dist_map) (v : nat) (new_d : nat) : dist_map :=
  fun u => if u =? v then Some new_d else d u.

(* Dijkstra 算法的一步 *)
Definition dijkstra_step (g : weighted_graph) 
  (dist : dist_map) (v : nat) : dist_map :=
  match dist v with
  | None => dist
  | Some d =>
      fold_left (fun acc '(u, w) =>
        match acc u with
        | None => update_dist acc u (d + w)
        | Some d' => 
            if d + w <? d' 
            then update_dist acc u (d + w)
            else acc
        end) (g v) dist
  end.

(* 最短路径的规范 *)
Definition is_shortest_path (g : weighted_graph) 
  (s t : nat) (d : nat) : Prop :=
  exists p : list nat,
    path_weight g s t p = Some d /\
    forall p', path_weight g s t p' = Some d' -> d <= d'.

4.3 编译器验证基础

本节介绍如何构建和验证一个简单的编程语言。

简单表达式语言

(* 算术表达式 *)
Inductive aexp : Type :=
  | ANum : nat -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

(* 布尔表达式 *)
Inductive bexp : Type :=
  | BTrue : bexp
  | BFalse : bexp
  | BEq : aexp -> aexp -> bexp
  | BLe : aexp -> aexp -> bexp
  | BNot : bexp -> bexp
  | BAnd : bexp -> bexp -> bexp.

(* 求值函数 *)
Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n => n
  | APlus a1 a2 => aeval a1 + aeval a2
  | AMinus a1 a2 => aeval a1 - aeval a2
  | AMult a1 a2 => aeval a1 * aeval a2
  end.

Fixpoint beval (b : bexp) : bool :=
  match b with
  | BTrue => true
  | BFalse => false
  | BEq a1 a2 => aeval a1 =? aeval a2
  | BLe a1 a2 => aeval a1 <=? aeval a2
  | BNot b1 => negb (beval b1)
  | BAnd b1 b2 => beval b1 && beval b2
  end.

(* 优化：常量折叠 *)
Fixpoint fold_constants_aexp (a : aexp) : aexp :=
  match a with
  | ANum n => ANum n
  | APlus a1 a2 =>
      match fold_constants_aexp a1, fold_constants_aexp a2 with
      | ANum n1, ANum n2 => ANum (n1 + n2)
      | a1', a2' => APlus a1' a2'
      end
  | AMinus a1 a2 =>
      match fold_constants_aexp a1, fold_constants_aexp a2 with
      | ANum n1, ANum n2 => ANum (n1 - n2)
      | a1', a2' => AMinus a1' a2'
      end
  | AMult a1 a2 =>
      match fold_constants_aexp a1, fold_constants_aexp a2 with
      | ANum n1, ANum n2 => ANum (n1 * n2)
      | a1', a2' => AMult a1' a2'
      end
  end.

(* 优化的正确性 *)
Theorem fold_constants_aexp_sound : forall a,
  aeval (fold_constants_aexp a) = aeval a.
Proof.
  intros a.
  induction a; simpl; try reflexivity.
  - (* APlus *)
    destruct (fold_constants_aexp a1) eqn:Ha1;
    destruct (fold_constants_aexp a2) eqn:Ha2;
    rewrite <- IHa1, <- IHa2; simpl; reflexivity.
  - (* AMinus 和 AMult 类似 *)
Admitted.

命令式语言

(* 命令语言 *)
Inductive com : Type :=
  | CSkip : com
  | CAss : string -> aexp -> com
  | CSeq : com -> com -> com
  | CIf : bexp -> com -> com -> com
  | CWhile : bexp -> com -> com.

(* 程序状态 *)
Definition state := string -> nat.

(* 更新状态 *)
Definition update (st : state) (x : string) (n : nat) : state :=
  fun y => if string_dec x y then n else st y.

(* 大步操作语义 *)
Inductive ceval : com -> state -> state -> Prop :=
  | E_Skip : forall st,
      ceval CSkip st st
  | E_Ass : forall st a1 n x,
      aeval st a1 = n ->
      ceval (CAss x a1) st (update st x n)
  | E_Seq : forall c1 c2 st st' st'',
      ceval c1 st st' ->
      ceval c2 st' st'' ->
      ceval (CSeq c1 c2) st st''
  | E_IfTrue : forall st st' b c1 c2,
      beval st b = true ->
      ceval c1 st st' ->
      ceval (CIf b c1 c2) st st'
  | E_IfFalse : forall st st' b c1 c2,
      beval st b = false ->
      ceval c2 st st' ->
      ceval (CIf b c1 c2) st st'
  | E_WhileFalse : forall b st c,
      beval st b = false ->
      ceval (CWhile b c) st st
  | E_WhileTrue : forall st st' st'' b c,
      beval st b = true ->
      ceval c st st' ->
      ceval (CWhile b c) st' st'' ->
      ceval (CWhile b c) st st''.

类型系统

(* 简单类型 *)
Inductive ty : Type :=
  | TNat : ty
  | TBool : ty.

(* 类型环境 *)
Definition context := string -> option ty.

(* 表达式的类型判断 *)
Inductive has_type_aexp : context -> aexp -> ty -> Prop :=
  | T_ANum : forall Γ n,
      has_type_aexp Γ (ANum n) TNat
  | T_APlus : forall Γ a1 a2,
      has_type_aexp Γ a1 TNat ->
      has_type_aexp Γ a2 TNat ->
      has_type_aexp Γ (APlus a1 a2) TNat
  (* 其他规则类似 *).

(* 类型安全 *)
Theorem type_safety_aexp : forall Γ a T,
  has_type_aexp Γ a T ->
  (T = TNat /\ exists n, aeval a = n).
Proof.
  intros Γ a T H.
  induction H.
  - split. reflexivity. exists n. reflexivity.
  - destruct IHhas_type_aexp1, IHhas_type_aexp2.
    split. reflexivity.
    destruct H2, H3.
    exists (x + x0). simpl. rewrite H2, H3. reflexivity.
Qed.

(* 命令的类型判断 *)
Inductive well_typed : context -> com -> Prop :=
  | WT_Skip : forall Γ,
      well_typed Γ CSkip
  | WT_Ass : forall Γ x a,
      Γ x = Some TNat ->
      has_type_aexp Γ a TNat ->
      well_typed Γ (CAss x a)
  | WT_Seq : forall Γ c1 c2,
      well_typed Γ c1 ->
      well_typed Γ c2 ->
      well_typed Γ (CSeq c1 c2)
  | WT_If : forall Γ b c1 c2,
      has_type_bexp Γ b TBool ->
      well_typed Γ c1 ->
      well_typed Γ c2 ->
      well_typed Γ (CIf b c1 c2)
  | WT_While : forall Γ b c,
      has_type_bexp Γ b TBool ->
      well_typed Γ c ->
      well_typed Γ (CWhile b c).

(* 类型保持定理 *)
Theorem preservation : forall Γ c st st',
  well_typed Γ c ->
  ceval c st st' ->
  (* 状态类型保持 *)
  forall x T, Γ x = Some T -> 
    exists n, st' x = n.
Proof.
  (* 对 ceval 进行归纳 *)
Admitted.

4.4 数学定理证明

本节展示如何在 Coq 中形式化和证明数学定理。

皮亚诺算术

(* 自然数的皮亚诺公理 *)
Module Peano.

Parameter N : Type.
Parameter O : N.
Parameter S : N -> N.

(* 公理 1：O 不是任何数的后继 *)
Axiom peano1 : forall n : N, S n <> O.

(* 公理 2：S 是单射 *)
Axiom peano2 : forall n m : N, S n = S m -> n = m.

(* 公理 3：归纳原理 *)
Axiom peano_ind : forall P : N -> Prop,
  P O ->
  (forall n, P n -> P (S n)) ->
  forall n, P n.

(* 定义加法 *)
Fixpoint plus (n m : N) : N :=
  match n with
  | O => m
  | S n' => S (plus n' m)
  end.

(* 证明加法的性质 *)
Theorem plus_O_r : forall n : N, plus n O = n.
Proof.
  intros n.
  pattern n.
  apply peano_ind.
  - reflexivity.
  - intros n' IH.
    simpl. rewrite IH. reflexivity.
Qed.

End Peano.

群论基础

(* 群的定义 *)
Class Group (G : Type) := {
  op : G -> G -> G;
  e : G;
  inv : G -> G;
  
  assoc : forall a b c, op a (op b c) = op (op a b) c;
  id_l : forall a, op e a = a;
  id_r : forall a, op a e = a;
  inv_l : forall a, op (inv a) a = e;
  inv_r : forall a, op a (inv a) = e
}.

Notation "a * b" := (op a b) (at level 40, left associativity).

(* 群的基本定理 *)
Section GroupTheorems.
  Context {G : Type} `{Group G}.
  
  (* 单位元唯一 *)
  Theorem unique_identity : forall e',
    (forall a, e' * a = a) -> e' = e.
  Proof.
    intros e' H0.
    rewrite <- (id_r e').
    rewrite <- (H0 e).
    reflexivity.
  Qed.
  
  (* 逆元唯一 *)
  Theorem unique_inverse : forall a b c,
    b * a = e -> a * c = e -> b = c.
  Proof.
    intros a b c Hba Hac.
    rewrite <- (id_r b).
    rewrite <- Hac.
    rewrite <- assoc.
    rewrite Hba.
    rewrite id_l.
    reflexivity.
  Qed.
  
  (* 消去律 *)
  Theorem left_cancel : forall a b c,
    a * b = a * c -> b = c.
  Proof.
    intros a b c H0.
    rewrite <- (id_l b).
    rewrite <- (inv_l a).
    rewrite assoc.
    rewrite H0.
    rewrite <- assoc.
    rewrite inv_l.
    rewrite id_l.
    reflexivity.
  Qed.
End GroupTheorems.

(* 整数模 n 群 *)
Instance Zn_group (n : nat) (Hn : n > 0) : Group (fin n) := {
  op := fun a b => fin_add a b;
  e := fin_zero;
  inv := fun a => fin_neg a
}.
Proof.
  (* 证明群公理 *)
Admitted.

实数构造

(* 柯西序列 *)
Definition cauchy_sequence := nat -> Q.

Definition is_cauchy (s : cauchy_sequence) : Prop :=
  forall ε : Q, ε > 0 -> exists N : nat,
    forall m n : nat, m >= N -> n >= N ->
      Qabs (s m - s n) < ε.

(* 等价关系 *)
Definition cauchy_equiv (s1 s2 : cauchy_sequence) : Prop :=
  forall ε : Q, ε > 0 -> exists N : nat,
    forall n : nat, n >= N ->
      Qabs (s1 n - s2 n) < ε.

(* 实数定义为柯西序列的等价类 *)
Record R : Type := mk_real {
  seq : cauchy_sequence;
  seq_cauchy : is_cauchy seq
}.

(* 实数运算 *)
Definition Rplus (x y : R) : R.
  destruct x as [sx Hx], y as [sy Hy].
  exists (fun n => sx n + sy n).
  (* 证明和仍是柯西序列 *)
Admitted.

(* 完备性 *)
Theorem R_complete : forall s : nat -> R,
  (forall ε : Q, ε > 0 -> exists N : nat,
    forall m n : nat, m >= N -> n >= N ->
      R_dist (s m) (s n) < ε) ->
  exists L : R, forall ε : Q, ε > 0 ->
    exists N : nat, forall n : nat, n >= N ->
      R_dist (s n) L < ε.
Proof.
  (* 完备性的证明 *)
Admitted.

拓扑学基础

(* 拓扑空间 *)
Record TopologicalSpace : Type := {
  carrier : Type;
  open : (carrier -> Prop) -> Prop;
  
  open_univ : open (fun _ => True);
  open_empty : open (fun _ => False);
  open_inter : forall U V, open U -> open V -> 
    open (fun x => U x /\ V x);
  open_union : forall F : (carrier -> Prop) -> Prop,
    (forall U, F U -> open U) ->
    open (fun x => exists U, F U /\ U x)
}.

(* 连续函数 *)
Definition continuous {X Y : TopologicalSpace} 
  (f : carrier X -> carrier Y) : Prop :=
  forall V, open Y V -> open X (fun x => V (f x)).

(* 同胚 *)
Definition homeomorphism {X Y : TopologicalSpace}
  (f : carrier X -> carrier Y) (g : carrier Y -> carrier X) : Prop :=
  continuous f /\ continuous g /\
  (forall x, g (f x) = x) /\ (forall y, f (g y) = y).

(* 紧致性 *)
Definition compact (X : TopologicalSpace) : Prop :=
  forall F : (carrier X -> Prop) -> Prop,
  (forall U, F U -> open X U) ->
  (forall x, exists U, F U /\ U x) ->
  exists G : (carrier X -> Prop) -> Prop,
    (forall U, G U -> F U) /\
    (exists l : list (carrier X -> Prop),
      (forall U, In U l <-> G U) /\
      (forall x, exists U, In U l /\ U x)).

(* 幂集的定义 *)
Definition powerset (A : Type) := A -> Prop.

(* 康托尔定理 *)
Theorem Cantor : forall (A : Type) (f : A -> powerset A),
  ~ (forall P : powerset A, exists a : A, f a = P).
Proof.
  intros A f H.
  (* 构造对角集合 *)
  pose (D := fun x : A => ~ (f x x)).
  (* D 不在 f 的值域中 *)
  destruct (H D) as [a Ha].
  (* 得出矛盾 *)
  assert (D a <-> f a a) by (rewrite <- Ha; reflexivity).
  unfold D in H0.
  destruct H0.
  specialize (H0 (H1 (fun H2 => H2 H2))).
  exact (H0 H0).
Qed.

(* 推论：实数不可数 *)
Corollary reals_uncountable :
  ~ exists f : nat -> R, forall r : R, exists n : nat, f n = r.
Proof.
  intros [f Hf].
  (* 使用对角化论证 *)
  (* 构造一个不在序列中的实数 *)
Admitted.

4.5 程序提取

Coq 可以从证明中提取可执行程序。

提取到 OCaml

(* 定义一个验证过的排序函数 *)
Definition sort_with_proof (l : list nat) :
  { l' : list nat | sorted l' /\ permutation l l' }.
Proof.
  exists (insertion_sort l).
  apply insertion_sort_correct.
Defined.

(* 提取排序函数 *)
Definition verified_sort (l : list nat) : list nat :=
  proj1_sig (sort_with_proof l).

(* 提取指令 *)
Require Extraction.
Extraction Language OCaml.

(* 基本类型映射 *)
Extract Inductive nat => "int"
  [ "0" "(fun x -> x + 1)" ]
  "(fun zero succ n -> if n = 0 then zero () else succ (n-1))".

Extract Inductive list => "list" [ "[]" "(::)" ].

(* 提取到文件 *)
Extraction "verified_sort.ml" verified_sort.

(* 生成的 OCaml 代码示例：
let rec insert_sorted x = function
  | [] -> [x]
  | h :: t -> 
      if x <= h then x :: h :: t
      else h :: insert_sorted x t

let rec verified_sort = function
  | [] -> []
  | h :: t -> insert_sorted h (verified_sort t)
*)

提取到 Haskell

(* 切换到 Haskell *)
Extraction Language Haskell.

(* Haskell 特定的映射 *)
Extract Inductive nat => "Prelude.Integer"
  [ "0" "\\x -> x Prelude.+ 1" ]
  "\\zero succ n -> if n Prelude.== 0 then zero () else succ (n Prelude.- 1)".

Extract Inductive list => "[]" [ "[]" "(:)" ].
Extract Inductive prod => "(,)" [ "(,)" ].
Extract Inductive option => "Prelude.Maybe" [ "Prelude.Nothing" "Prelude.Just" ].

(* 提取纯函数式的二叉搜索树 *)
Extraction "BST.hs" BST insert lookup.

(* 生成的 Haskell 代码示例：
data BST a = Empty | Node a (BST a) (BST a)

insert :: Ord a => a -> BST a -> BST a
insert x Empty = Node x Empty Empty
insert x (Node y l r) =
  if x <= y
  then Node y (insert x l) r
  else Node y l (insert x r)
*)

提取优化

(* 优化提取：去除证明项 *)
Definition gcd_with_proof (a b : nat) :
  { d : nat | d > 0 /\ 
              (exists q1, a = q1 * d) /\ 
              (exists q2, b = q2 * d) /\
              (forall d', d' > 0 -> 
                (exists q1, a = q1 * d') -> 
                (exists q2, b = q2 * d') -> 
                d' <= d) }.
Proof.
  (* 欧几里得算法的验证实现 *)
Admitted.

(* 提取时只保留计算部分 *)
Definition gcd (a b : nat) : nat :=
  proj1_sig (gcd_with_proof a b).

(* 内联优化 *)
Extraction Inline gcd_with_proof.
Extraction NoInline gcd.

(* 避免提取某些定义 *)
Extract Constant mult => "( * )".
Extract Constant plus => "( + )".

(* 提取整个模块 *)
Recursive Extraction Library List.
Recursive Extraction Library Arith.

与原生代码集成

(* 外部函数接口 *)
Parameter read_file : string -> option string.
Parameter write_file : string -> string -> bool.

(* 提取到实际的文件操作 *)
Extract Constant read_file => 
  "(fun filename ->
     try 
       let ic = open_in filename in
       let n = in_channel_length ic in
       let s = Bytes.create n in
       really_input ic s 0 n;
       close_in ic;
       Some (Bytes.to_string s)
     with _ -> None)".

Extract Constant write_file =>
  "(fun filename content ->
     try
       let oc = open_out filename in
       output_string oc content;
       close_out oc;
       true
     with _ -> false)".

(* 验证的文件处理程序 *)
Definition process_file (f : string -> string) 
  (input output : string) : bool :=
  match read_file input with
  | None => false
  | Some content => write_file output (f content)
  end.

(* 使用验证过的转换函数 *)
Definition verified_transform (s : string) : string :=
  (* 某个经过验证的字符串转换 *)
  s.

Definition main : bool :=
  process_file verified_transform "input.txt" "output.txt".

Extraction "file_processor.ml" main.

(* JSON 解析器 *)
Inductive parse_result (A : Type) :=
  | Success : A -> string -> parse_result A
  | Failure : string -> parse_result A.

Definition parser (A : Type) := string -> parse_result A.

(* 解析器组合子 *)
Definition parse_char (c : ascii) : parser unit :=
  fun s => match s with
  | EmptyString => Failure _ "EOF"
  | String c' s' => 
      if ascii_dec c c' 
      then Success _ tt s'
      else Failure _ "char mismatch"
  end.

(* JSON 值解析器 *)
Fixpoint parse_json (s : string) : parse_result json :=
  (* 实现省略 *).

(* 验证解析器的正确性 *)
Theorem parse_json_correct : forall s j s',
  parse_json s = Success _ j s' ->
  valid_json j.
Proof.
  (* 证明解析出的 JSON 是有效的 *)
Admitted.

(* 提取配置 *)
Extract Inductive ascii => "char"
  [ (* 128 个 ASCII 字符的映射 *) ].

Extract Inductive string => "string"
  [ "String.empty" "(fun c s -> String.make 1 c ^ s)" ].

(* 提取到 OCaml *)
Extraction "json_parser.ml" parse_json.

5.1 数学形式化

Lean 在数学形式化方面有着强大的生态系统，特别是 Mathlib 库。

使用 Mathlib

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

-- 证明三角恒等式
theorem sin_squared_plus_cos_squared (x : ℝ) : 
  Real.sin x ^ 2 + Real.cos x ^ 2 = 1 := by
  simp [Real.sin_sq_add_cos_sq]

群论示例

import Mathlib.Algebra.Group.Defs

-- 定义群的性质
class MyGroup (G : Type*) extends Mul G, One G, Inv G where
  mul_assoc : ∀ a b c : G, (a * b) * c = a * (b * c)
  one_mul : ∀ a : G, 1 * a = a
  mul_one : ∀ a : G, a * 1 = a
  inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1

-- 证明逆元的唯一性
theorem inv_unique {G : Type*} [MyGroup G] (a b : G) 
  (h : a * b = 1) : b = a⁻¹ := by
  have h1 : a⁻¹ * (a * b) = a⁻¹ * 1 := by rw [h]
  rw [MyGroup.mul_one] at h1
  rw [← MyGroup.mul_assoc, MyGroup.inv_mul_cancel, MyGroup.one_mul] at h1
  exact h1

theorem left_cancel {G : Type*} [MyGroup G] (a b c : G) 
  (h : a * b = a * c) : b = c := by
  have h1 : a⁻¹ * (a * b) = a⁻¹ * (a * c) := by rw [h]
  rw [← MyGroup.mul_assoc, ← MyGroup.mul_assoc] at h1
  rw [MyGroup.inv_mul_cancel, MyGroup.inv_mul_cancel] at h1
  rw [MyGroup.one_mul, MyGroup.one_mul] at h1
  exact h1

5.2 程序验证与优化

Lean 4 作为一个功能完整的编程语言，可以编写高效的验证程序。

验证排序算法

-- 定义有序列表
def Sorted : List Nat → Prop
  | [] => True
  | [_] => True
  | x :: y :: xs => x ≤ y ∧ Sorted (y :: xs)

-- 插入排序
def insertSorted (x : Nat) : List Nat → List Nat
  | [] => [x]
  | y :: ys => if x ≤ y then x :: y :: ys 
               else y :: insertSorted x ys

def insertionSort : List Nat → List Nat
  | [] => []
  | x :: xs => insertSorted x (insertionSort xs)

-- 证明插入保持有序性
theorem insertSorted_preserves_sorted (x : Nat) (l : List Nat) :
  Sorted l → Sorted (insertSorted x l) := by
  intro h
  induction l with
  | nil => simp [insertSorted, Sorted]
  | cons y ys ih =>
    simp [insertSorted]
    split_ifs with h1
    · cases ys with
      | nil => simp [Sorted, h1]
      | cons z zs => 
        simp [Sorted] at h ⊢
        exact ⟨h1, h⟩
    · cases ys with
      | nil => simp [Sorted, le_of_not_le h1]
      | cons z zs =>
        simp [Sorted] at h ⊢
        exact ⟨h.1, ih h.2⟩

使用依赖类型优化

-- 带长度信息的向量
inductive Vec (α : Type) : Nat → Type where
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

-- 安全的头部函数
def head {α : Type} {n : Nat} : Vec α (n + 1) → α
  | Vec.cons x _ => x

-- 向量拼接
def append {α : Type} {m n : Nat} : 
  Vec α m → Vec α n → Vec α (m + n)
  | Vec.nil, ys => ys
  | Vec.cons x xs, ys => Vec.cons x (append xs ys)

def vecMap {α β : Type} {n : Nat} (f : α → β) : 
  Vec α n → Vec β n
  | Vec.nil => Vec.nil
  | Vec.cons x xs => Vec.cons (f x) (vecMap f xs)

-- 证明 map 保持长度
example {α β : Type} {n : Nat} (f : α → β) (v : Vec α n) :
  ∃ (w : Vec β n), w = vecMap f v := by
  use vecMap f v
  rfl

5.3 元编程与自动化

Lean 4 提供了强大的元编程能力，可以编写自定义策略和代码生成器。

自定义策略

import Lean

open Lean Meta Elab Tactic

-- 定义一个简单的策略
def myTrivial : TacticM Unit := do
  let goal ← getMainGoal
  let goalType ← goal.getType
  
  -- 尝试 rfl
  try
    let expr ← mkAppM ``Eq.refl #[← mkFreshExprMVar goalType]
    goal.assign expr
    return
  catch _ => pure ()
  
  -- 尝试 trivial
  evalTactic (← `(tactic| trivial))

-- 注册策略
elab "my_trivial" : tactic => myTrivial

-- 使用示例
example : 2 + 2 = 4 := by my_trivial

宏和语法扩展

-- 定义新的语法
syntax "prove_by_cases" term "with" cases:term,* : tactic

macro_rules
  | `(tactic| prove_by_cases $e with $[$cases],*) => 
    `(tactic| cases $e <;> [$[$cases],*])

-- 使用新语法
example (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  prove_by_cases h with
    (right; assumption),
    (left; assumption)

import Lean.Elab.Tactic

open Lean Meta Elab Tactic

def simpArith : TacticM Unit := do
  evalTactic (← `(tactic| simp [add_comm, add_assoc, mul_comm, mul_assoc]))
  try (evalTactic (← `(tactic| ring)))
  
elab "simp_arith" : tactic => simpArith

-- 测试
example (a b c : Nat) : a + b + c = c + b + a := by
  simp_arith

5.4 交互式定理证明

Lean 的交互式证明环境提供了丰富的工具支持。

结构化证明

-- 使用 have 和 show 的结构化证明
theorem sqrt_two_irrational : ¬ ∃ (p q : ℕ), q ≠ 0 ∧ p * p = 2 * q * q := by
  intro ⟨p, q, hq, h_eq⟩
  
  -- 假设 p 和 q 互质
  have h_coprime : Nat.gcd p q = 1 := by sorry  -- 简化处理
  
  -- p² 是偶数，所以 p 是偶数
  have p_even : Even p := by
    have : Even (p * p) := by
      use q * q
      rw [h_eq]
      ring
    exact even_of_even_sq this
  
  -- 设 p = 2k
  obtain ⟨k, hk⟩ := p_even
  
  -- 代入原式得到 q² 也是偶数
  have q_even : Even q := by
    have : 2 * k * (2 * k) = 2 * q * q := by
      rw [← hk] at h_eq
      exact h_eq
    have : 2 * (2 * k * k) = 2 * q * q := by ring_nf at this ⊢; exact this
    have : 2 * k * k = q * q := by linarith
    have : Even (q * q) := by use k * k; exact this.symm
    exact even_of_even_sq this
  
  -- 但这与互质矛盾
  sorry  -- 完整证明需要更多细节

计算证明（calc）

-- 使用 calc 进行链式推理
example (a b c d : ℝ) (h1 : a = b) (h2 : b < c) (h3 : c ≤ d) : 
  a < d := by
  calc a = b := h1
       _ < c := h2
       _ ≤ d := h3

theorem even_sq_of_even (n : ℕ) : Even n → Even (n * n) := by
  intro h
  -- 因为 n 是偶数，存在 k 使得 n = 2k
  obtain ⟨k, hk⟩ := h
  
  -- 证明 n² 是偶数
  show Even (n * n)
  
  -- n² = (2k)² = 4k² = 2(2k²)
  have : n * n = 2 * (2 * k * k) := by
    rw [hk]
    ring
  
  -- 因此 n² 是偶数
  use 2 * k * k
  exact this

5.5 Lean 项目实践

本节介绍如何组织和管理 Lean 项目。

项目结构

# 创建新项目
lake new my_project
cd my_project

# 项目结构
my_project/
├── MyProject.lean       # 主文件
├── MyProject/
│   ├── Basic.lean      # 基础定义
│   ├── Theorems.lean   # 定理证明
│   └── Examples.lean   # 示例
├── lakefile.lean       # 构建配置
└── lean-toolchain      # Lean 版本

使用 Lake 构建系统

-- lakefile.lean
import Lake
open Lake DSL

package «my_project» where
  -- 添加依赖
  dependencies := #[
    {
      name := `mathlib
      src := Source.git 
        "https://github.com/leanprover-community/mathlib4.git" 
        "main"
    }
  ]

@[default_target]
lean_lib «MyProject» where
  -- 库配置
  roots := #[`MyProject]

文档和测试

/-!
# My Project

这是项目文档的主页。

## 主要内容

- 基础定义
- 核心定理
- 应用示例
-/

-- 文档字符串
/-- 计算列表的长度 -/
def myLength {α : Type} : List α → Nat
  | [] => 0
  | _ :: xs => 1 + myLength xs

-- 单元测试
#eval myLength [1, 2, 3]  -- 期望输出: 3

-- 属性测试
theorem myLength_correct {α : Type} (l : List α) :
  myLength l = l.length := by
  induction l with
  | nil => rfl
  | cons x xs ih => simp [myLength, List.length, ih]

-- Stack.lean
namespace Stack

/-- 栈数据结构 -/
structure Stack (α : Type) where
  items : List α

/-- 创建空栈 -/
def empty {α : Type} : Stack α := ⟨[]⟩

/-- 压栈 -/
def push {α : Type} (s : Stack α) (x : α) : Stack α :=
  ⟨x :: s.items⟩

/-- 弹栈 -/
def pop {α : Type} : Stack α → Option (α × Stack α)
  | ⟨[]⟩ => none
  | ⟨x :: xs⟩ => some (x, ⟨xs⟩)

/-- 栈是否为空 -/
def isEmpty {α : Type} (s : Stack α) : Bool :=
  s.items.isEmpty

-- 验证性质
theorem push_pop {α : Type} (s : Stack α) (x : α) :
  pop (push s x) = some (x, s) := by
  simp [push, pop]

theorem empty_isEmpty {α : Type} :
  isEmpty (empty : Stack α) = true := by
  simp [isEmpty, empty]

end Stack

A. Coq 标准库参考

常用模块

• Arith - 自然数算术
• List - 列表操作
• Bool - 布尔运算
• Logic - 逻辑连接词
• Relations - 关系理论
• Sorting - 排序算法
• Wellfounded - 良基关系

重要策略速查

(* 基本策略 *)
reflexivity    (* 证明反身性 *)
symmetry       (* 交换等式两边 *)
transitivity   (* 传递性 *)
assumption     (* 使用假设 *)
exact H        (* 精确应用 *)

(* 引入和应用 *)
intros         (* 引入全称量词 *)
apply H        (* 应用假设或定理 *)
eapply H       (* 延迟实例化 *)

(* 分解 *)
destruct       (* 分情况讨论 *)
induction      (* 归纳法 *)
inversion      (* 反演 *)

(* 重写 *)
rewrite H      (* 使用等式重写 *)
rewrite <- H   (* 反向重写 *)
subst          (* 替换变量 *)

(* 简化 *)
simpl          (* 简化表达式 *)
unfold f       (* 展开定义 *)
fold f         (* 折叠定义 *)

(* 自动化 *)
auto           (* 自动证明 *)
eauto          (* 扩展自动证明 *)
lia            (* 线性算术 *)
ring           (* 环运算 *)
field          (* 域运算 *)

B. Coq 常见错误与调试

类型错误

错误：The term "x" has type "nat" while it is expected to have type "bool"

解决：检查类型是否匹配，可能需要类型转换函数。

未完成的证明

错误：Error: Attempt to save an incomplete proof

解决：使用 Admitted 暂时承认，或完成所有子目标。

策略失败

错误：Error: No applicable tactic

解决：检查当前目标，可能需要先做一些准备工作。

C. Lean 标准库参考

常用模块

• Init - 基础定义和符号
• Std - 标准库扩展
• Mathlib - 数学库
• Mathlib.Data.Nat - 自然数
• Mathlib.Data.List - 列表操作
• Mathlib.Logic.Basic - 基础逻辑
• Mathlib.Tactic - 策略库
• Mathlib.Algebra - 代数结构
• Mathlib.Analysis - 分析学
• Mathlib.Topology - 拓扑学

重要策略速查

-- 基本策略
rfl           -- 证明反身性
symm          -- 交换等式两边
trans         -- 传递性
assumption    -- 使用假设
exact h       -- 精确应用

-- 引入和应用
intro         -- 引入假设
intros        -- 引入多个假设
apply h       -- 应用假设或定理
refine        -- 精细化目标

-- 分解
cases         -- 分情况讨论
induction     -- 归纳法
match         -- 模式匹配
obtain        -- 解构存在量词

-- 重写
rw [h]        -- 使用等式重写
simp          -- 简化器
simp only     -- 受限简化
conv          -- 转换模式

-- 简化
dsimp         -- 定义简化
unfold f      -- 展开定义
change        -- 改变目标形式

-- 自动化
simp          -- 简化器
ring          -- 环策略
linarith      -- 线性算术
norm_num      -- 数值计算
omega         -- Presburger 算术
aesop         -- 自动证明搜索

-- 数学专用
field_simp    -- 域简化
ring_nf       -- 环标准形式
group         -- 群论策略
abel          -- 阿贝尔群策略

类型类实例

-- 常用类型类
instance : Add Nat := ⟨Nat.add⟩
instance : Mul Nat := ⟨Nat.mul⟩
instance : OfNat Nat n := ⟨n⟩

-- 代数结构
instance : Monoid α where
  mul := (· * ·)
  one := 1
  mul_assoc := mul_assoc
  one_mul := one_mul
  mul_one := mul_one

-- 自定义实例
instance : ToString MyType where
  toString x := s!"MyType: {x.field}"

元编程基础

-- 自定义策略
syntax "my_tactic" : tactic
macro_rules
  | `(tactic| my_tactic) => `(tactic| simp; rfl)

-- 宏定义
macro "prove_by" t:tactic : tactic =>
  `(tactic| first | $t | simp | rfl)

-- 元变量操作
open Lean Meta in
def myTactic : TacticM Unit := do
  let goal ← getMainGoal
  let type ← goal.getType
  trace[myTactic] "Goal type: {type}"

D. Lean 常见错误与调试

类型错误

错误：type mismatch

-- 错误示例
def f (n : Nat) : Bool := n  -- 错误：期望 Bool，得到 Nat

-- 修正
def f (n : Nat) : Bool := n > 0

类型推断失败

错误：failed to synthesize instance

-- 错误示例
#check (2 : ℝ) + (3 : ℕ)  -- 错误：无法推断加法实例

-- 修正
#check (2 : ℝ) + (3 : ℝ)  -- 显式类型标注
#check (2 : ℝ) + ↑3       -- 使用强制转换

策略失败

错误：tactic failed

-- 调试技巧
theorem my_theorem : P := by
  trace_state  -- 显示当前目标
  sorry        -- 暂时跳过

-- 使用 try 和 first
theorem my_theorem : P := by
  try simp     -- 尝试简化
  first        -- 尝试多个策略
  | rfl
  | assumption
  | sorry

终止性检查

错误：failed to prove termination

-- 错误示例
def badFib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n => badFib (n - 1) + badFib (n - 2)  -- 错误：n-2 可能不减小

-- 修正1：使用 termination_by
def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

-- 修正2：显式终止证明
def fib' (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => fib' n + fib' (n + 1)
termination_by n

Universe 级别错误

错误：universe level mismatch

-- 错误示例
def bad : Type → Type := fun α => List α  -- 错误：universe 不匹配

-- 修正
def good : Type u → Type u := fun α => List α
-- 或
def good' (α : Type u) : Type u := List α

调试工具

-- 跟踪选项
set_option trace.Meta.synthInstance true  -- 跟踪实例合成
set_option trace.simp true               -- 跟踪简化器
set_option pp.all true                   -- 显示所有隐式参数

-- 检查表达式
#check @List.map        -- 查看完整类型
#print List.map         -- 查看定义
#reduce 2 + 3          -- 计算表达式

-- 目标检查
example : P := by
  trace_target           -- 显示目标
  trace_state           -- 显示完整状态
  sorry

-- 性能分析
set_option profiler true
#eval expensive_computation

包管理问题

Lake 构建错误处理：

# 清理缓存
lake clean

# 更新依赖
lake update

# 详细输出
lake build -v

# 检查 lean-toolchain
cat lean-toolchain

E. Ltac：Coq 的策略语言

Ltac (Language of Tactics) 是 Coq 的策略编程语言，允许用户编写自定义策略、组合现有策略，并实现证明自动化。

为什么需要 Ltac？

Ltac 存在的核心原因是证明的重复性模式需要自动化：

• 手动证明的痛点：很多证明包含大量重复的步骤模式
• 领域特定性：不同领域的证明有不同的模式，需要定制化
• 可组合性：基本策略需要灵活组合来解决复杂问题

本质上，Ltac 就是一个模式匹配的状态机，它的设计目标是：

• 对证明状态（goals 和 hypotheses）进行模式匹配
• 根据匹配结果选择和组合策略
• 提供回溯机制处理失败情况

什么是 Ltac？

Ltac 是一种领域特定语言，专门用于：

• 组合和编排基本策略
• 编写可重用的证明模式
• 实现证明自动化
• 处理证明中的重复性工作

基础语法

(* 定义一个简单的策略 *)
Ltac my_simpl := simpl; reflexivity.

(* 使用自定义策略 *)
Theorem test : 2 + 2 = 4.
Proof.
  my_simpl.  (* 相当于执行 simpl; reflexivity *)
Qed.

(* 带参数的策略 *)
Ltac apply_n_times tac n :=
  match n with
  | O => idtac  (* 什么都不做 *)
  | S ?n' => tac; apply_n_times tac n'
  end.

策略组合器

(* tac1; tac2 - 先执行 tac1，然后对所有子目标执行 tac2 *)
Ltac intro_and_simpl := intros; simpl.

(* 选择性组合 *)
Ltac solve_simple :=
  simpl;
  first [ reflexivity | assumption | trivial ].

(* tac1 || tac2 - 尝试 tac1，如果失败则尝试 tac2 *)
Ltac auto_solve :=
  reflexivity || assumption || auto.

(* try - 尝试执行，失败也不报错 *)
Ltac safe_rewrite H :=
  try rewrite H.

模式匹配

Ltac break_and :=
  match goal with
  | [ |- ?A /\ ?B ] => split
  end.

(* 更复杂的模式匹配 *)
Ltac find_eq_and_rewrite :=
  match goal with
  | [ H : ?x = ?y |- context[?x] ] => rewrite H
  | [ H : ?x = ?y |- context[?y] ] => rewrite <- H
  end.

Ltac contradict :=
  match goal with
  | [ H : False |- _ ] => contradiction
  | [ H : ?P, H' : ~ ?P |- _ ] => contradiction
  end.

(* 查找并使用等式 *)
Ltac use_eq :=
  match goal with
  | [ H : _ = _ |- _ ] => rewrite H || rewrite <- H
  end.

实用 Ltac 策略示例

(* 解决简单的算术等式 *)
Ltac crush_arith :=
  intros;
  repeat (simpl in *; 
          try ring;
          try lia;
          auto).

(* 自动分解合取和存在量词 *)
Ltac decompose_ex :=
  repeat match goal with
  | [ H : exists x, _ |- _ ] => destruct H
  | [ H : _ /\ _ |- _ ] => destruct H
  end.

(* 打印当前目标状态 *)
Ltac print_goal :=
  match goal with
  | [ |- ?G ] => idtac "Current goal:" G
  end.

(* 标记证明步骤 *)
Ltac step msg :=
  idtac "Step:" msg;
  print_goal.

高级特性

(* 递归地应用简化 *)
Ltac simpl_all :=
  simpl;
  repeat match goal with
  | [ H : _ |- _ ] => simpl in H
  end.

(* 深度优先搜索证明 *)
Ltac depth_first_proof n :=
  match n with
  | O => fail
  | S ?n' =>
    first [ reflexivity
          | assumption
          | (progress simpl; depth_first_proof n')
          | (progress auto; depth_first_proof n') ]
  end.

(* 清理无用假设 *)
Ltac cleanup :=
  repeat match goal with
  | [ H : ?X = ?X |- _ ] => clear H
  | [ H : True |- _ ] => clear H
  end.

(* 生成新假设 *)
Ltac remember_all :=
  repeat match goal with
  | [ |- context[?f ?x] ] =>
    let y := fresh "y" in
    remember (f x) as y
  end.

Ltac2：下一代策略语言

Coq 正在开发 Ltac2，这是 Ltac 的继任者，提供：

• 静态类型系统
• 更好的性能
• 更清晰的语义
• 与 OCaml 更好的互操作性

From Ltac2 Require Import Ltac2.

(* Ltac2 策略定义 *)
Ltac2 my_auto () :=
  first [ reflexivity ()
        | assumption ()
        | auto () ].

(* 使用 Ltac2 策略 *)
Goal forall x : nat, x = x.
Proof.
  ltac2:(my_auto ()).
Qed.

最佳实践

1. 命名规范：使用描述性名称，如 solve_by_induction 而非 tac1
2. 错误处理：使用 try 和 first 来处理可能失败的策略
3. 模块化：将复杂策略分解为小的、可重用的组件
4. 文档：为复杂的 Ltac 策略添加注释说明其用途
5. 调试：使用 idtac 和 fail 来调试策略

Ltac solve_bool_eq :=
  intros;
  repeat match goal with
  | [ b : bool |- _ ] => destruct b
  | [ |- context[if ?b then _ else _] ] => destruct b
  | [ H : _ && _ = true |- _ ] => apply andb_true_iff in H; destruct H
  | [ H : _ || _ = false |- _ ] => apply orb_false_iff in H; destruct H
  end;
  simpl in *;
  try reflexivity;
  try discriminate;
  try contradiction.

(* 测试策略 *)
Example test_bool_eq1 : forall b : bool,
  b && true = b.
Proof.
  solve_bool_eq.
Qed.

Example test_bool_eq2 : forall b1 b2 : bool,
  b1 && b2 = true -> b1 = true /\ b2 = true.
Proof.
  solve_bool_eq.
Qed.

高级自动化技术

(* 自动应用相关假设 *)
Ltac smart_apply :=
  match goal with
  | [ H : forall x, ?P x -> ?Q x, H' : ?P ?a |- ?Q ?a ] => 
    apply (H a H')
  | [ H : ?P -> ?Q, H' : ?P |- ?Q ] => 
    apply (H H')
  | [ H : forall x, ?P x |- ?P ?a ] => 
    apply H
  end.

(* 传递性链式推理 *)
Ltac chain_trans :=
  match goal with
  | [ H1 : ?a = ?b, H2 : ?b = ?c |- ?a = ?c ] =>
    transitivity b; [exact H1 | exact H2]
  | [ H1 : ?a <= ?b, H2 : ?b <= ?c |- ?a <= ?c ] =>
    transitivity b; [exact H1 | exact H2]
  end.

(* 自动前向推理 *)
Ltac forward_reasoning :=
  repeat match goal with
  | [ H : ?P -> ?Q, H' : ?P |- _ ] =>
    let H_new := fresh "H" in
    assert (H_new : Q) by (apply H; exact H')
  end.

(* 自动归纳策略 *)
Ltac auto_induction x :=
  induction x;
  intros;
  simpl in *;
  try reflexivity;
  try (rewrite IHx; reflexivity);
  try (rewrite <- IHx; reflexivity);
  auto.

(* 列表相关的自动化 *)
Ltac list_solver :=
  intros;
  repeat match goal with
  | [ |- context[?l ++ nil] ] => rewrite app_nil_r
  | [ |- context[nil ++ ?l] ] => rewrite app_nil_l
  | [ |- context[(?l1 ++ ?l2) ++ ?l3] ] => rewrite app_assoc
  | [ H : ?l = nil |- _ ] => destruct l; [clear H | discriminate H]
  | [ H : nil = ?l |- _ ] => destruct l; [clear H | discriminate H]
  | [ H : ?h :: ?t = nil |- _ ] => discriminate H
  | [ H : nil = ?h :: ?t |- _ ] => discriminate H
  end;
  auto.

(* 自然数归纳的高级策略 *)
Ltac nat_ind_strong P :=
  intro n;
  pattern n;
  apply (nat_ind P);
  [clear n | intro n'; intro IHn'].

(* 自动反证法 *)
Ltac by_contradiction :=
  match goal with
  | [ |- ?P ] =>
    destruct (classic P) as [H | H];
    [exact H | exfalso]
  end.

(* 寻找矛盾 *)
Ltac find_contradiction :=
  match goal with
  | [ H : ?P, H' : ~ ?P |- _ ] => contradiction
  | [ H : ?x <> ?x |- _ ] => contradiction
  | [ H : ?x = ?y, H' : ?x <> ?y |- _ ] => contradiction
  | [ H : ?x < ?x |- _ ] => apply lt_irrefl in H; contradiction
  | [ H : S ?n <= ?n |- _ ] => apply le_S_n in H; apply le_Sn_n in H; contradiction
  end.

(* 带深度限制的证明搜索 *)
Ltac bounded_search depth :=
  match depth with
  | O => fail "Search depth exceeded"
  | S ?d =>
    first [ assumption
          | reflexivity
          | (progress simpl; bounded_search d)
          | (progress auto; bounded_search d)
          | (left; bounded_search d)
          | (right; bounded_search d)
          | (split; bounded_search d)
          | (intro; bounded_search d) ]
  end.

(* 启发式证明搜索 *)
Ltac heuristic_prove :=
  (* 先尝试简单策略 *)
  try reflexivity;
  try assumption;
  try discriminate;
  (* 然后尝试分解 *)
  repeat match goal with
  | [ |- _ /\ _ ] => split
  | [ H : _ /\ _ |- _ ] => destruct H
  | [ H : _ \/ _ |- _ ] => destruct H
  | [ |- exists _, _ ] => eexists
  end;
  (* 最后尝试自动化 *)
  auto.

(* 集合论证明自动化 *)
Ltac set_solver :=
  intros;
  unfold subset, element_of, empty_set in *;
  firstorder.

(* 排列组合证明自动化 *)
Ltac perm_solver :=
  intros;
  repeat match goal with
  | [ |- Permutation ?l ?l ] => reflexivity
  | [ H : Permutation ?l1 ?l2 |- Permutation ?l2 ?l1 ] => 
    apply Permutation_sym; exact H
  | [ H1 : Permutation ?l1 ?l2, H2 : Permutation ?l2 ?l3 |- Permutation ?l1 ?l3 ] =>
    eapply Permutation_trans; [exact H1 | exact H2]
  end.

(* 等价关系证明自动化 *)
Ltac equiv_solver :=
  intros;
  repeat match goal with
  | [ |- ?R ?x ?x ] => apply refl_equiv
  | [ H : ?R ?x ?y |- ?R ?y ?x ] => apply sym_equiv; exact H
  | [ H1 : ?R ?x ?y, H2 : ?R ?y ?z |- ?R ?x ?z ] =>
    eapply trans_equiv; [exact H1 | exact H2]
  end.

性能优化技巧

(* 避免重复计算 *)
Ltac cache_computation term :=
  let v := fresh "cached" in
  remember term as v.

(* 惰性匹配 - 只在需要时匹配 *)
Ltac lazy_match :=
  lazymatch goal with
  | [ |- ?P /\ ?Q ] => split
  | [ |- ?P ] => fail "Not a conjunction"
  end.

(* 多线程策略（概念性） *)
Ltac parallel_try tac1 tac2 :=
  first [progress tac1 | progress tac2].

(* 记忆化策略结果 *)
Ltac memoized_auto := 
  let cache := fresh "cache" in
  assert (cache : True) by constructor;
  auto;

调试和错误处理

(* 详细的错误信息 *)
Ltac fail_with_context msg :=
  match goal with
  | [ |- ?G ] => fail "Error:" msg "in goal:" G
  end.

(* 断言和前置条件检查 *)
Ltac assert_precondition P :=
  assert P by (auto || fail "Precondition failed").

(* 策略执行跟踪 *)
Ltac trace_exec tac name :=
  idtac "Entering" name;
  let result := tac in
  idtac "Exiting" name;
  result.

(* 超时处理 *)
Ltac with_timeout n tac :=
  timeout n tac.

与其他 Coq 特性的集成

(* 与类型类集成 *)
Ltac typeclass_solver :=
  typeclasses eauto.

(* 与 Program 集成 *)
Ltac program_simpl :=
  program_simpl;
  try solve [program_solve_wf].

(* 与 setoid 重写集成 *)
Ltac setoid_rewrite_all :=
  repeat match goal with
  | [ H : ?R ?x ?y |- context[?x] ] => setoid_rewrite H
  end.

(* 与 ssreflect 集成 *)
Ltac ssr_auto :=
  by []; done.

Ltac length_solver :=
  intros;
  repeat match goal with
  | [ l : list _ |- _ ] => destruct l; simpl in *
  | [ |- context[length (?l1 ++ ?l2)] ] => rewrite app_length
  | [ H : length ?l = 0 |- _ ] => apply length_zero_iff_nil in H; subst
  | [ |- length ?l = 0 ] => apply length_zero_iff_nil
  | [ H : length ?l = S ?n |- _ ] => 
    destruct l; [discriminate H | simpl in H; injection H; clear H; intro H]
  end;
  try ring;
  auto.

Example length_example1 : forall (A : Type) (l : list A),
  length l = 0 -> l = nil.
Proof.
  length_solver.
Qed.

Example length_example2 : forall (A : Type) (l1 l2 : list A),
  length (l1 ++ l2) = length l1 + length l2.
Proof.
  length_solver.
Qed.

实战中的 Ltac 最佳实践

(* 创建模块化的策略库 *)
Module MyTactics.
  
  (* 基础策略 *)
  Ltac basic_cleanup :=
    intros;
    simpl in *;
    unfold not in *;
    repeat match goal with
    | [ H : ?X = ?X |- _ ] => clear H
    | [ H : True |- _ ] => clear H
    | [ H : ?X -> ?X |- _ ] => clear H
    end.
  
  (* 中级策略 *)
  Ltac solve_by_inverting :=
    basic_cleanup;
    repeat match goal with
    | [ H : ?f _ = ?f _ |- _ ] => injection H; clear H; intros; subst
    | [ H : Some _ = Some _ |- _ ] => injection H; clear H; intros; subst
    | [ H : Some _ = None |- _ ] => discriminate H
    | [ H : None = Some _ |- _ ] => discriminate H
    end;
    auto.
  
  (* 高级策略 *)
  Ltac full_auto :=
    basic_cleanup;
    solve_by_inverting;
    repeat (progress (auto; firstorder)).
    
End MyTactics.

Import MyTactics.

(* 为编译器验证设计的策略 *)
Ltac eval_step :=
  match goal with
  | [ |- context[eval_expr (EConst ?n)] ] => 
    unfold eval_expr; simpl
  | [ |- context[eval_expr (EPlus ?e1 ?e2)] ] =>
    unfold eval_expr; simpl;
    rewrite <- eval_expr_sound
  | [ |- context[eval_expr (EVar ?x)] ] =>
    unfold eval_expr; simpl;
    rewrite lookup_correct
  end.

(* 类型系统的自动化 *)
Ltac type_check :=
  repeat match goal with
  | [ |- has_type _ (TConst _) TInt ] => 
    constructor
  | [ |- has_type ?env (TVar ?x) ?t ] => 
    apply T_Var; apply lookup_env
  | [ |- has_type ?env (TApp ?f ?x) ?t ] =>
    eapply T_App; [type_check | type_check]
  end.

(* 使用子目标标记 *)
Ltac prove_with_labels :=
  match goal with
  | [ |- ?P /\ ?Q ] => 
    split; 
    [ idtac "Proving" P; prove_with_labels
    | idtac "Proving" Q; prove_with_labels ]
  | [ |- forall x, ?P x ] =>
    let x' := fresh x in
    intro x';
    idtac "Proving for" x';
    prove_with_labels
  | _ => auto
  end.

(* 结构化证明 *)
Ltac structured_proof :=
  (* 阶段1: 初始化 *)
  intros; simpl in *;
  (* 阶段2: 分解复杂结构 *)
  repeat match goal with
  | [ H : exists x, _ |- _ ] => destruct H
  | [ H : _ /\ _ |- _ ] => destruct H
  | [ |- _ /\ _ ] => split
  end;
  (* 阶段3: 应用域特定知识 *)
  repeat match goal with
  | [ H : ?P -> ?Q, H' : ?P |- _ ] => 
    apply H in H'
  end;
  (* 阶段4: 终结 *)
  auto.

性能调优和经验教训

1. 避免回溯：使用 lazymatch 代替 match 来避免不必要的回溯
2. 早期失败：在不可能成功的情况下尽早使用 fail
3. 缓存结果：使用 remember 来避免重复计算
4. 限制搜索空间：使用 only 和 using 来限制自动化策略的搜索范围
5. 渐进式开发：先编写简单版本，然后逐步优化

(* 使用 Info 命令 *)
Goal forall n m : nat, n + m = m + n.
Proof.
  intros.
  Info 2 auto.  (* 查看 auto 执行的详细步骤 *)
  
  (* 使用 Show Ltac Profile *)
  Set Ltac Profiling.
  (* 执行一些策略 *)
  Show Ltac Profile.
  
  (* 使用 debug 模式 *)
  Set Ltac Debug.
  auto.
  Unset Ltac Debug.
Abort.

Ltac 的可编程性和替代方案

Ltac 的 AST 和外部访问

Ltac 确实有内部 AST 表示，但：

• 有限的外部访问：Ltac 的 AST 不像 MetaCoq 那样完全暴露给外部
• Ltac2 的改进：新的 Ltac2 提供了更好的程序化接口
• ML 插件：可以通过 OCaml 插件访问更底层的证明状态

(* OCaml 插件直接操作证明状态 *)
let my_tactic : unit Proofview.tactic =
  Proofview.Goal.enter (fun gl ->
    let env = Proofview.Goal.env gl in
    let sigma = Proofview.Goal.sigma gl in
    let concl = Proofview.Goal.concl gl in
    (* 直接操作证明状态 *)
    ...
  )

不使用 Ltac 的替代方案

# Python 示例使用 SerAPI
from serapi import SerAPI

coq = SerAPI()
coq.add("Theorem test : 2 + 2 = 4.")
state = coq.query_goals()
# 程序化地分析状态并发送策略
coq.execute("simpl.")
coq.execute("reflexivity.")

From MetaCoq.Template Require Import All.

(* 直接构造证明项 *)
Definition my_proof : 2 + 2 = 4 :=
  eq_refl 4.

(* 或者程序化生成证明 *)
MetaCoq Quote Definition q_proof := my_proof.

% Elpi 策略示例
solve (goal _ _ {{ lp:A = lp:B }} as G) GL :-
  % 直接操作证明状态
  coq.unify-eq A B ok,
  refine {{ eq_refl lp:A }} G GL.

(* 完全跳过策略，直接写证明项 *)
Definition my_theorem : forall n : nat, n + 0 = n :=
  fix f n := match n with
  | 0 => eq_refl 0
  | S n' => f_equal S (f n')
  end.

为什么 Ltac 仍然流行？

1. 集成性：Ltac 深度集成在 Coq 中，无需额外工具
2. 表达力：对证明状态的模式匹配很自然
3. 生态系统：大量现有代码使用 Ltac
4. 学习曲线：比 OCaml 插件或 MetaCoq 更容易上手

未来展望

Ltac 虽然强大，但也有一些局限性。Coq 社区正在开发新的解决方案：

• Ltac2：提供静态类型和更好的性能
• Elpi：基于 λProlog 的策略语言
• MetaCoq：元编程框架
• ML 策略：使用 OCaml 编写高性能策略

掌握 Ltac 是成为 Coq 高手的必经之路。通过编写自定义策略，您可以大大提高证明效率，并为特定领域构建强大的自动化工具。

Ltac2：下一代策略语言

设计动机

Ltac1 的主要问题：

• 动态类型：运行时才发现类型错误
• 性能问题：解释执行，回溯开销大
• 语义模糊：求值顺序不明确
• 调试困难：错误信息不友好

Ltac2 的核心特性

From Ltac2 Require Import Ltac2.

(* 类型明确的策略定义 *)
Ltac2 my_tactic (n : int) (tac : unit -> unit) : unit :=
  match Int.equal n 0 with
  | true => ()
  | false => tac (); my_tactic (Int.sub n 1) tac
  end.

(* 多态策略 *)
Ltac2 map_hyps (f : ident -> constr -> unit) : unit :=
  List.iter (fun h => 
    let typ := Constr.type (Control.hyp h) in
    f h typ
  ) (Control.hyps ()).

Ltac2 Type exn ::= [ MyError (string) ].

Ltac2 safe_assumption () :=
  match Control.case (fun () => assumption) with
  | Val _ => Message.print (Message.of_string "Assumption succeeded")
  | Err e => Control.throw (MyError "No matching assumption")
  end.

Ltac2 mutable debug : bool := false.

Module MyTactics.
  Ltac2 trace (msg : string) :=
    if debug then Message.print (Message.of_string msg)
    else ().
    
  Ltac2 smart_intro () :=
    trace "Introducing...";
    intro.
End MyTactics.

(* 明确的求值控制 *)
Ltac2 lazy_or tac1 tac2 :=
  Control.plus (fun () => tac1 ()) (fun _ => tac2 ()).

(* 高效的循环 *)
Ltac2 repeat_n (n : int) (tac : unit -> unit) :=
  let rec aux i :=
    if Int.equal i 0 then ()
    else (tac (); aux (Int.sub i 1))
  in aux n.

Ltac2 实战示例

Ltac2 crush_arith () :=
  (* 类型安全的模式匹配 *)
  repeat (
    first [
      reflexivity
    | progress (Std.intros)
    | progress (Std.simpl)
    | match! goal with
      | [ h : ?x = ?y |- _ ] => Std.rewrite h
      | [ |- context [?n + 0] ] => 
        Pattern.rewrite (fun () => open_constr:(_ + 0)) 
                        (fun () => open_constr:(_))
                        (fun () => plus_n_O)
      end
    ]
  ).

(* 使用 *)
Goal forall n m : nat, n + 0 + m = n + m.
Proof.
  ltac2:(crush_arith ()).
Qed.

Ltac2 vs Ltac1 对比

F. MetaCoq：元编程框架

MetaCoq 是 Coq 的元编程框架，允许在 Coq 内部操作和生成 Coq 项。它提供了对 Coq 的内部表示的完全访问。

核心概念

MetaCoq 提供了：

• 具体化（Reification）：将 Coq 项转换为 AST
• 反具体化（Reflection）：将 AST 转换回 Coq 项
• 类型检查器：在 Coq 内验证项的类型
• 求值器：在 Coq 内求值项

基本使用

From MetaCoq.Template Require Import All.

Definition foo := 42.

(* 获取 foo 的 AST *)
MetaCoq Quote Definition foo_ast := foo.
(* foo_ast = tConst "Top.foo" [] *)

(* 获取更复杂的项 *)
MetaCoq Quote Definition plus_ast := (fun x y : nat => x + y).
Print plus_ast.
(* 显示完整的 AST 结构 *)

(* 程序化构造 AST *)
Definition my_const_ast := 
  tConstruct {| inductive_mind := "Coq.Init.Datatypes.nat"; 
                inductive_ind := 0 |} 1 [].  (* S 构造子 *)

(* 转换回 Coq 项 *)
MetaCoq Unquote Definition my_num := 
  (tApp my_const_ast [tConstruct ... 0 []]).  (* S O *)
(* my_num = 1 *)

From MetaCoq.Template Require Import All.
Import MCMonadNotation.

(* 自动生成等式证明 *)
Definition make_eq_proof (n : nat) : TemplateMonad unit :=
  let rhs := tApp (tConst "Nat.add" []) 
                  [tConst "n" []; tConstruct ... 0 []] in
  let eq_type := tApp (tConst "eq" []) [tInd ...; tConst "n" []; rhs] in
  proof <- tmLemma ("n_plus_0_eq_" ++ string_of_nat n) eq_type ;;
  tmDefinition ("proof_" ++ string_of_nat n) proof.

(* 运行元程序 *)
MetaCoq Run (make_eq_proof 5).

高级应用

(* 自动生成 Decidable 实例 *)
MetaCoq Derive Decidable for nat.
MetaCoq Derive Decidable for list.

(* 自动生成归纳原理 *)
MetaCoq Derive Induction for tree.

(* 定义优化变换 *)
Definition optimize_plus (t : term) : term :=
  match t with
  | tApp (tConst "Nat.add" _) [x; tConstruct _ 0 []] => x  (* x + 0 => x *)
  | tApp (tConst "Nat.add" _) [tConstruct _ 0 []; y] => y  (* 0 + y => y *)
  | _ => t
  end.

(* 应用到具体函数 *)
MetaCoq Quote Definition original := (fun n => n + 0 + 0).
Definition optimized := optimize_plus original.
MetaCoq Unquote Definition better_fun := optimized.

(* 简单的编译器示例 *)
Inductive expr :=
  | EConst (n : nat)
  | EPlus (e1 e2 : expr).

Fixpoint compile (e : expr) : term :=
  match e with
  | EConst n => tConstruct ... (* 编码自然数 *)
  | EPlus e1 e2 => 
    tApp (tConst "Nat.add" []) [compile e1; compile e2]
  end.

(* 证明编译器正确性 *)
Lemma compile_correct : forall e,
  eval (unquote (compile e)) = eval_expr e.

MetaCoq 的主要组件

(* MetaCoq 的核心 AST 类型 *)
Inductive term :=
  | tRel (n : nat)                          (* de Bruijn 索引 *)
  | tVar (id : ident)                       (* 变量 *)
  | tEvar (ev : nat) (args : list term)    (* 存在变量 *)
  | tSort (s : sort)                        (* 类型宇宙 *)
  | tProd (na : name) (ty : term) (body : term)  (* 依赖乘积 *)
  | tLambda (na : name) (ty : term) (body : term) (* 函数 *)
  | tLetIn (na : name) (def : term) (def_ty : term) (body : term)
  | tApp (f : term) (args : list term)     (* 应用 *)
  | tConst (c : kername) (u : list Level.t) (* 常量 *)
  | tInd (ind : inductive) (u : list Level.t) (* 归纳类型 *)
  | tConstruct (ind : inductive) (idx : nat) (u : list Level.t)
  | tCase (ind_nbparams_relevance : inductive * nat * relevance)
          (type_info : term)
          (discr : term)
          (branches : list (nat * term))
  | tProj (proj : projection) (t : term)
  | tFix (mfix : mfixpoint term) (idx : nat)
  | tCoFix (mfix : mfixpoint term) (idx : nat)
  | tInt (i : PrimInt63.int)
  | tFloat (f : PrimFloat.float).

(* MetaCoq 的 Template Monad 操作 *)
Inductive TemplateMonad : Type -> Type :=
  | tmReturn {A} : A -> TemplateMonad A
  | tmBind {A B} : TemplateMonad A -> (A -> TemplateMonad B) -> 
                   TemplateMonad B
  | tmPrint : term -> TemplateMonad unit
  | tmMsg : string -> TemplateMonad unit
  | tmFail {A} : string -> TemplateMonad A
  | tmEval : reductionStrategy -> term -> TemplateMonad term
  | tmDefinition : ident -> option term -> term -> TemplateMonad unit
  | tmAxiom : ident -> term -> TemplateMonad unit
  | tmLemma : ident -> term -> TemplateMonad term
  | tmFreshName : ident -> TemplateMonad ident
  | tmQuote : forall {A}, A -> TemplateMonad term
  | tmUnquote : term -> TemplateMonad typed_term
  | tmUnquoteTyped : forall A, term -> TemplateMonad A
  | tmExistingInstance : ident -> TemplateMonad unit
  | tmInferInstance : option reductionStrategy -> term -> 
                      TemplateMonad (option term).

MetaCoq vs Ltac2 对比

实际选择建议

1. 使用 Ltac2：
   • 需要编写复杂的证明自动化
   • 关注性能和类型安全
   • 想要更好的错误信息
2. 使用 MetaCoq：
   • 需要生成 Coq 代码
   • 实现领域特定语言
   • 开发验证工具
   • 需要深度内省 Coq 项
3. 结合使用：

   (* MetaCoq 生成定理和证明框架 *)
   MetaCoq Run (generate_lemmas ...).
   
   (* Ltac2 完成具体证明 *)
   Ltac2 prove_generated_lemmas () := ...

实战示例：自动生成数据结构操作

From MetaCoq.Template Require Import All.

(* 为任意数据类型生成 fold 函数 *)
Definition generate_fold (ind_name : string) : TemplateMonad unit :=
  (* 获取归纳类型信息 *)
  ind_info <- tmQuoteInductive ind_name ;;
  match ind_info with
  | Build_mutual_inductive_body _ _ bodies _ =>
    match bodies with
    | [body] =>
      (* 构造 fold 函数的类型 *)
      let fold_type := ... in
      (* 构造 fold 函数的定义 *)
      let fold_body := ... in
      (* 定义 fold 函数 *)
      tmDefinition (ind_name ++ "_fold") (Some fold_type) fold_body
    | _ => tmFail "Multiple mutually inductive types not supported"
    end
  end.

(* 使用示例 *)
Inductive tree (A : Type) :=
  | Leaf : A -> tree A
  | Node : tree A -> tree A -> tree A.

MetaCoq Run (generate_fold "tree").
(* 自动生成 tree_fold 函数 *)

总结

MetaCoq 为 Coq 提供了强大的元编程能力，使得：

• 可以在 Coq 内部分析和生成 Coq 代码
• 能够实现复杂的代码变换和优化
• 支持开发经过验证的工具和编译器
• 为领域特定语言提供实现基础

虽然学习曲线较陡，但 MetaCoq 在需要深度元编程的场景中是不可替代的工具。