修复条款的减少。 （Coq）

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.