5
मैं एक उपाय का उपयोग कर एक पुनरावर्ती परिभाषा को परिभाषित करने के समारोह का उपयोग करने के कोशिश कर रहा हूँ, और मैं त्रुटि मिल रही है भीतर forall का उपयोग करना:पुनरावर्ती समारोह परिभाषा
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.
मुझे पता है कि समस्याएं टॉल्स के कारण हैं: यदि मैं उन्हें सही से बदलता हूं, तो यह काम करता है। मैं यह भी जानता हूं कि मुझे एक ही त्रुटि मिलती है यदि मेरा दाएं हाथ की तरफ प्रभाव (->) का उपयोग करता है। फिक्सपॉइंट फ़ॉल्स के साथ काम करता है, लेकिन मुझे माप को परिभाषित करने की अनुमति नहीं देता है।
कोई सलाह?
के रूप में वादा किया था, मेरा पूरा कोड है:
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.