Обоснованная индукция для счетного предиката - PullRequest
Новая
       7

Обоснованная индукция для счетного предиката

0 голосов
/ 23 марта 2019

Вот определение для предиката Count.Он использует 2 индекса для обозначения начальных и конечных элементов: предикат «check» для подсчета / пропуска «текущего» элемента и последний аргумент «sum» для отслеживания количества элементов, которые удовлетворяют предикату check между этими индексами границы. 

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

Требуется доказать, что количество подсчитываемых элементов "сумма" неотрицательно. 

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

Очевидно, что здесь можно применить индукцию.Однако схемы типа natlike_rec3 неприменимы из-за разницы Q_Hit | Q_Miss в элементе суммы (т. Е. +1 в Q_Hit).

Вот моя попытка доказательства до шага, где должна применяться индукция. 

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 можно было бы использовать в дальнейшем с отношением по сумме и p: sum <= p.

1 Ответ

2 голосов
/ 23 марта 2019

Вы можете использовать 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.
...