5
Tôi đang cố gắng để sử dụng chức năng để xác định một định nghĩa đệ quy sử dụng một biện pháp, và tôi nhận được lỗi:Sử dụng forall trong đệ quy định nghĩa Chức năng
Error: find_call_occs : Prod
tôi gửi bài mã nguồn toàn bộ tại dưới cùng, nhưng chức năng của tôi là
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.
Tôi biết vấn đề là do các yếm: nếu tôi thay thế bằng True, nó hoạt động. Tôi cũng biết tôi gặp lỗi tương tự nếu phía bên tay phải của tôi sử dụng các hàm ý (->). Fixpoint hoạt động với các quầy hàng, nhưng không cho phép tôi xác định thước đo.
Bạn có lời khuyên nào không?
Như đã hứa, mã hoàn chỉnh của tôi là:
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.