coq - Coq归纳定义中的非严格正发生问题

Question

主要问题是我无法定义这样一个归纳命题:

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

---

事实上，我正在尝试为直觉逻辑定义克里普克语义

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

我不明白如果我定义这个 Inductive 东西可能会出什么问题，我也想不出任何其他方法来实现这个定义。

更新:

这些是需要的定义:

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.

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