在 Coq 中重写匹配

Question

在 Coq 中，假设我有一个定点函数 f，它的匹配定义在 (g x) 上，并且我想使用 (g x = ...) 形式的假设证明。以下是一个最小的工作示例（实际上 f、g 会更复杂）：

Definition g (x:nat) := x.

Fixpoint f (x:nat) := 
  match g x with
    | O => O
    | S y => match x with 
      | O => S O
      | S z => f z
      end 
  end.

Lemma test : forall (x : nat), g x = O -> f x = O.
Proof.
  intros.
  unfold f.
  rewrite H. (*fails*)

该消息显示了 Coq 卡住的位置：

(fix f (x0 : nat) : nat :=
   match g x0 with
   | 0 => 0
   | S _ => match x0 with
            | 0 => 1
            | S z0 => f z0
            end
   end) x = 0

Error: Found no subterm matching "g x" in the current goal.

但是，命令 unfold f. rewrite H. 不起作用。

如何将 Coq 转换为 unfold f 然后使用 H？

Answer 1

Parameter g: nat -> nat.

(* You could restructure f in one of two ways: *)

(* 1. Use a helper then prove an unrolling lemma: *)

Definition fhelp fhat (x:nat) := 
  match g x with
    | O => O
    | S y => match x with 
      | O => S O
      | S z => fhat z
      end 
  end.

Fixpoint f (x:nat) := fhelp f x.

Lemma funroll : forall x, f x = fhelp f x.
destruct x; simpl; reflexivity.
Qed.

Lemma test : forall (x : nat), g x = O -> f x = O.
Proof.
  intros.
  rewrite funroll.
  unfold fhelp.
  rewrite H.
  reflexivity.
Qed.

(* 2. Use Coq's "Function": *)

Function f2 (x:nat) := 
  match g x with
    | O => O
    | S y => match x with 
      | O => S O
      | S z => f2 z
      end 
  end.

Check f2_equation.

Lemma test2 : forall (x : nat), g x = O -> f2 x = O.
Proof.
  intros.
  rewrite f2_equation.
  rewrite H.
  reflexivity.
Qed.

Answer 2

我不确定这是否能解决一般问题，但在您的特定情况下（因为 g 是如此简单），这个有效：

Lemma test : forall (x : nat), g x = O -> f x = O.
Proof.
  unfold g.
  intros ? H. rewrite H. reflexivity.
Qed.

Answer 3

这是另一个解决方案，但当然是针对这个微不足道的例子。也许会给你一些想法。引理 test2 : forall (x : nat), g x = O -> f x = O.
证明。
=>简介;
模式 x;
在 H 中展开 g;
重写 H;
琐碎。
Qed.

在 Coq 中重写匹配

Rewriting a match in Coq

coq