Не строго положительная проблема возникновения в индуктивном определении Coq - PullRequest
Новая
       5

Не строго положительная проблема возникновения в индуктивном определении Coq

1 голос
/ 26 марта 2020

Основная проблема в том, что я не могу определить такое индуктивное суждение: 

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.

1 Ответ

2 голосов
/ 26 марта 2020

Вы не можете определить это отношение как индуктивный предикат, но вы можете определить его с помощью рекурсии по формуле: 

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.

Этот прием не работает, если определение не является обоснованным в отношении структура формулы, но этого может быть достаточно для вашего варианта использования.

...