通过修复减少条款。 （考克）

Question

函数“f”出现在我的证明中。我需要证明当它的两个论点是相同的数字时它等于零。实际上，函数 f 等价于“大于或等于”函数“geq”。

我正在使用https://github.com/HoTT/HoTT 库，但很明显问题不是特定于库的，所以我在下面做了一个独立的示例。它至少应该可以使用 Coq v8.5 运行。库中的部分代码：

Local Set Typeclasses Strict Resolution.
Local Unset Elimination Schemes.
Global Set Keyed Unification.
Global Unset Refine Instance Mode.
Global Unset Strict Universe Declaration.
Global Unset Universe Minimization ToSet.
Inductive paths {A : Type} (a : A) : A -> Type :=
  idpath : paths a a.
Arguments idpath {A a} , [A] a.
Scheme paths_ind := Induction for paths Sort Type.
Arguments paths_ind [A] a P f y p.
Scheme paths_rec := Minimality for paths Sort Type.
Arguments paths_rec [A] a P f y p.
Definition paths_rect := paths_ind.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope. 

Inductive Bool := true | false.

Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end.

主要部分：

Definition code_n := (fix code_n (m n : nat) {struct m} : Bool :=
       match m with
       | 0 =>
           match n with
           | 0 => true
           | S n' =>false 
           end
       | S m' =>
           match n with
           | 0 => false
           | S n' => code_n m' n'
           end
       end).

Definition f (m:nat) := (fix acc (m0 : nat) : nat :=
   match m0 with
   | 0 => 0
   | S m1 => add (if code_n m1 m then 1 else 0) (acc m1)
   end).

Eval compute in f 1 1. (*=0*)
Eval compute in f 1 2. (*=1*)
Eval compute in f 2 2. (*=0*)
Fixpoint impprf (m:nat): f m m = 0. (*How to prove it??*)

作为第一步，当两个参数相等时，很容易证明 code_n 为真：

Fixpoint code_n_eq (v : nat): (code_n v v) = true 
:= match v as n return (code_n n n = true) with
   | 0 => @idpath Bool true
   | S v0 => code_n_eq v0
   end.

第二步：问题可以重新表述为证明

code_n_eq (S m) (S m) = code_n_eq m m. 

或者，也许，那个

(0 = code_n_eq m m)-> (0 =  code_n_eq (S m) (S m) ).

Answer 1

为了使证明更容易，我不得不用标准的类似物替换您的自定义定义，并且我冒昧地重新排列了代码。您可以还原更改并看到一切仍然有效，前提是您使用bool 而不是Bool 和+ 而不是add。

Fixpoint code_n (m n : nat) {struct m} : bool :=
  match m, n with
  | 0, 0 => true
  | 0, S _ | S _, 0 => false
  | S m', S n' => code_n m' n'
  end.

Fixpoint f (m n :nat) : nat :=
  match n with
  | 0 => 0
  | S n' => (if code_n n' m then 1 else 0) + (f m n')
  end.

在接下来的内容中，我将使用一些证明自动化来展示主要思想，而不是陷入细节。通常，当我们试图通过归纳来证明一个引理时，首先证明一个更强的陈述会更容易（甚至可能是唯一的方法）。

Require Import Omega.  (* to use `omega` magical tactic *)

Lemma code_n_eq m n :
  (code_n m n) = true <-> m = n.
Proof.
  revert n; induction m; destruct n; try easy; firstorder.
Qed.

(* generalize what we want to prove *)
Lemma gte m n :
  m >= n -> f m n = 0.
Proof.
  revert m; induction n; destruct m; try easy; firstorder.
  simpl. destruct (code_n n (S m)) eqn:E.
  - apply code_n_eq in E; omega.
  - assert (m >= n); firstorder.
Qed.

Lemma impprf (m:nat): f m m = 0.
Proof. apply gte. auto. Qed.