Я пытаюсь использовать функцию для определения рекурсивного определения, используя меру, и получаю ошибку:
Error: find_call_occs : Prod
Я публикую весь исходный код внизу, но мойфункция
Function kripke_sat (M : kripke) (s : U) (p : formula) {measure size p}: Prop :=
match p with
| Proposition p' => L M (s)(p')
| Not p' => ~ kripke_sat M s p'
| And p' p'' => kripke_sat M s p' /\ kripke_sat M s p''
| Or p' p'' => kripke_sat M s p' \/ kripke_sat M s p''
| Implies p' p'' => ~kripke_sat M s p' \/ kripke_sat M s p''
| Knows a p' => forall t, ~(K M a) s t \/ kripke_sat M t p'
| EvKnows p' => forall i, kripke_sat M s (Knows i p' )
end.
Я знаю, что проблема связана с ошибками: если я заменю их на True, это сработает.Я также знаю, что получаю ту же ошибку, если моя правая сторона использует значения (->).Fixpoint работает с данными, но не позволяет мне определять меру.
Любой совет?
Как и обещал, мой полный код:
Module Belief.
Require Import Arith.EqNat.
Require Import Arith.Gt.
Require Import Arith.Plus.
Require Import Arith.Le.
Require Import Arith.Lt.
Require Import Logic.
Require Import Logic.Classical_Prop.
Require Import Init.Datatypes.
Require Import funind.Recdef.
(* Formalization of a variant of a logic of knowledge, as given in Halpern 1995 *)
Section Kripke.
Variable n : nat.
(* Universe of "worlds" *)
Definition U := nat.
(* Universe of Principals *)
Definition P := nat.
(* Universe of Atomic propositions *)
Definition A := nat.
Inductive prop : Type :=
| Atomic : A -> prop.
Definition beq_prop (p1 p2 :prop) : bool :=
match (p1,p2) with
| (Atomic p1', Atomic p2') => beq_nat p1' p2'
end.
Inductive actor : Type :=
| Id : P -> actor.
Definition beq_actor (a1 a2: actor) : bool :=
match (a1,a2) with
| (Id a1', Id a2') => beq_nat a1' a2'
end.
Inductive formula : Type :=
| Proposition : prop -> formula
| Not : formula -> formula
| And : formula -> formula -> formula
| Or : formula -> formula -> formula
| Implies : formula -> formula ->formula
| Knows : actor -> formula -> formula
| EvKnows : formula -> formula (*me*)
.
Inductive con : Type :=
| empty : con
| ext : con -> prop -> con.
Notation " C # P " := (ext C P) (at level 30).
Require Import Relations.
Record kripke : Type := mkKripke {
K : actor -> relation U;
K_equiv: forall y, equivalence _ (K y);
L : U -> (prop -> Prop)
}.
Fixpoint max (a b: nat) : nat :=
match a, b with
| 0, _ => a
| _, 0 => b
| S(a'), S(b') => 1 + max a' b'
end.
Fixpoint length (p: formula) : nat :=
match p with
| Proposition p' => 1
| Not p' => 1 + length(p')
| And p' p'' => 1 + max (length p') (length p'')
| Or p' p'' => 1 + max (length p') (length p'')
| Implies p' p'' => 1 + max (length p') (length p'')
| Knows a p' => 1 + length(p')
| EvKnows p' => 1 + length(p')
end.
Fixpoint numKnows (p: formula): nat :=
match p with
| Proposition p' => 0
| Not p' => 0 + numKnows(p')
| And p' p'' => 0 + max (numKnows p') (numKnows p'')
| Or p' p'' => 0 + max (numKnows p') (numKnows p'')
| Implies p' p'' => 0 + max (numKnows p') (numKnows p'')
| Knows a p' => 0 + numKnows(p')
| EvKnows p' => 1 + numKnows(p')
end.
Definition size (p: formula): nat :=
(numKnows p) + (length p).
Definition twice (n: nat) : nat :=
n + n.
Theorem duh: forall a: nat, 1 + a > a.
Proof. induction a. apply gt_Sn_O.
apply gt_n_S in IHa. unfold plus in *. apply IHa. Qed.
Theorem eq_lt_lt: forall (a b c d: nat), a = b -> c<d -> a+ c< b+d.
Proof. intros. apply plus_le_lt_compat.
apply eq_nat_elim with (n:=a) (m := b). apply le_refl.
apply eq_nat_is_eq. apply H. apply H0. Qed.
Function kripke_sat (M : kripke) (s : U) (p : formula) {measure size p}: Prop :=
match p with
| Proposition p' => L M (s)(p')
| Not p' => ~ kripke_sat M s p'
| And p' p'' => kripke_sat M s p' /\ kripke_sat M s p''
| Or p' p'' => kripke_sat M s p' \/ kripke_sat M s p''
| Implies p' p'' => ~kripke_sat M s p' \/ kripke_sat M s p''
| Knows a p' => forall t, ~(K M a) s t \/ kripke_sat M t p'
| EvKnows p' => forall i, kripke_sat M s (Knows i p' )
end.