Основная проблема в том, что я не могу определить такое индуктивное суждение:
Inductive forces : nat -> Prop :=
| KM_cond (n : nat) : ~ forces 0 ->
forces n.
На самом деле я пытаюсь определить семантику Крипке для Intuitionisti c Logi c
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).
Я не могу понять, что могло бы быть go неправильным, если бы я определил эту индуктивную вещь, и я не могу придумать какой-либо другой способ достижения этого определения.
ОБНОВЛЕНИЕ:
Это необходимые определения:
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.