有根据的计数谓词归纳

Question

这是Count谓词的定义。它使用2个索引来表示起始和结束元素，“检查”谓词来计算/跳过“当前”元素，使用最后一个参数“sum”来跟踪满足这些边界索引之间的检查谓词的元素数量。

Require Import ZArith.

Open Scope Z_scope.

Inductive Count : Z -> Z -> (Z -> Prop) -> Z -> Prop :=
    | Q_Nil:
        forall (m n : Z),
        forall (check : Z -> Prop),
          (n <= m) ->
            (Count m n check 0)
    | Q_Hit:
        forall (m n sum : Z),
        forall (check : Z -> Prop),
          let x := (n - 1) in
            (m < n) ->
            (check x) ->
            (Count m x check sum) ->
              (Count m n check (1 + sum))
    | Q_Miss:
        forall (m n sum : Z),
        forall (check : Z -> Prop),
          let x := (n - 1) in
            (m < n) ->
            ~(check x) ->
            (Count m x check sum) ->
              (Count m n check sum).

需要证明计数元素“sum”的数量是非负的。

Goal
  forall (m n sum : Z),
  forall (check : Z -> Prop),
    (Count m n check sum) -> (0 <= sum).
Proof.

显然，感应可以在这里应用。然而，像natlike_rec3这样的方案由于sum元素中的Q_Hit | Q_Miss差异（即Q_Hit中的+1）而不适用。

这是我的证明尝试，直到应该应用归纳的步骤。

Proof.
Require Import Psatz.
intros m n sum check.
assert (X: n <= m \/ n > m) by lia.
destruct X as [le|gt].
+ intro.
  inversion H; subst; intuition.
+ pose (p := (n - m)).
  assert (PZ: p > 0). { subst p. auto with zarith. }
  replace n with (m + p) in * by (subst p; auto with zarith).

1 subgoal
m, n, sum : Z
check : Z -> Prop
p := n - m : Z
gt : m + p > m
PZ : p > 0
______________________________________(1/1)
Count m (m + p) check sum -> 0 <= sum

我认为也许well_founded_induction_type_2可以进一步用于sum和p：sum <= p上的关系。

Answer 1

你可以在induction假设上使用Count（在某种程度上，这是Inductive类型的主要观点）。

Proof.
  intros.
  induction H.
  all: omega.
  (* or, as a single sequence: intros; induction H; omega. *)
  (* lia also works instead of omega, and should probably be preferred nowadays (Require Import Lia.) *)
Qed.