Coq归纳定义中的非严格正出现问题

Question

主要问题是我无法定义这样的归纳命题：

Inductive forces : nat -> Prop :=
  | KM_cond (n : nat) : ~ forces 0 ->
        forces n.

---

实际上，我正在尝试为直觉逻辑定义Kripke语义学

Inductive forces (M : Kripke_model) (x : world) : prop -> Prop :=
  | KM_cond (A B : prop) : set_In x (worlds M) ->
      (forall y, (rel M) x y -> (~ forces M y A \/ forces M y B)) ->
        forces M x (A then B).

但出现以下错误

Non strictly positive occurrence of "forces"

如果我只是删除否定，问题就会消失

Inductive forces (M : Kripke_model) (x : world) : prop -> Prop :=
  | KM_cond (A B : prop) : set_In x (worlds M) ->
      (forall y, (rel M) x y -> (forces M y A \/ forces M y B)) ->
        forces M x (A then B).

但同样存在->问题

Inductive forces (M : Kripke_model) (x : world) : prop -> Prop :=
  | KM_cond (A B : prop) : set_In x (worlds M) ->
      (forall y, (rel M) x y -> (forces M y A -> forces M y B)) ->
        forces M x (A then B).

我无法理解如果定义此归纳法可能会出什么问题，并且我无法想到实现此定义的任何其他方法。

UPDATE：

这些是必需的定义：

From Coq Require Import Lists.List.
From Coq Require Import Lists.ListSet.
From Coq Require Import Relations.
Import ListNotations.

Definition var := nat.

Inductive prop : Type :=
  | bot
  | atom (p : var)
  | conj (A B : prop)
  | disj (A B : prop)
  | cond (A B : prop).

Notation "A 'and' B" := (conj A B) (at level 50, left associativity).
Notation "A 'or' B" := (disj A B) (at level 50, left associativity).
Notation "A 'then' B" := (cond A B) (at level 60, no associativity).

Definition world := nat.

Definition preorder {X : Type} (R : relation X) : Prop :=
  (forall x : X, R x x) /\ (forall x y z : X, R x y -> R y z -> R x z).

Inductive Kripke_model : Type :=
  | Kripke (W : set world) (R : relation world) (v : var -> world -> bool)
    (HW : W <> empty_set world)
    (HR : preorder R)
    (Hv : forall x y p, In x W -> In y W ->
      R x y -> (v p x) = true -> (v p y) = true).

Definition worlds (M : Kripke_model) :=
  match M with
  | Kripke W _ _ _ _ _ => W
  end.

Definition rel (M : Kripke_model) :=
  match M with
  | Kripke _ R _ _ _ _ => R
  end.

Definition val (M : Kripke_model) :=
  match M with
  | Kripke _ _ v _ _ _ => v
  end.

Answer 1

您不能将此关系定义为归纳谓词，但可以通过对公式进行递归来定义它：

Fixpoint forces (M : Kripke_model) (x : world) (p : prop) : Prop :=
  match p with
  | bot => False
  | atom p => val M p x = true
  | conj p q => forces M x p /\ forces M x q
  | disj p q => forces M x p \/ forces M x q
  | cond p q => forall y, rel M x y -> forces M y p -> forces M y q
  end.

如果有关公式结构的定义不充分，则此技巧不起作用，但对于您的用例来说可能就足够了。