重寫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*) 

消息顯示，其中勒柯克卡：

(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.