2010-12-13 6 views
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. 

Я знаю, что проблема связана с foralls: если заменить их, правда, это работает. I также знаю, что я получаю ту же ошибку, если моя правая сторона использует значения (->). Fixpoint работает с foralls, но не позволяет мне определить меру.

Любые советы?

Как и было обещано, мой полный код:

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. 

ответ

6

"Функциональную" плагин еще очень экспериментальным. В документации вы можете найти

term0 must be build as a pure pattern-matching tree (match...with) with λ-abstractions and applications only at the end of each branch.

Но я согласен, что это сообщение об ошибке далеко не явные (сообщения, как правило, такие ошибки должны либо заканчиваться «Пожалуйста, сообщайте» или быть более удобным дружественным, я рассмотрите это как ошибку). Это означает, что фоллеты не допускаются в теле функции (я не знаю, есть ли теоретические причины для этого поведения).

Так что вам нужно сделать свое определение «вручную» без помощи Функция. Вот небольшой пример, который вы можете адаптировать для своего развития. Удачи!


Inductive form : Set := 
    | T : form 
    | K : nat -> form -> form 
    | eK : form -> form. 

Fixpoint size (f : form) : nat := match f with 
    | T => 1 
    | K _ f => S (size f) 
    | eK f => S (S (size f)) 
end. 

Require Import Wf. 
Require Import Wf_nat. 

Definition R x y := size x < size y. 
Lemma R_wf : well_founded R. 
    apply well_founded_ltof. 
Qed. 

Lemma lem1 : 
    forall x n, R x (K n x). 
unfold R; intuition. 
Qed. 

Lemma lem2 : 
    forall x n, R (K n x) (eK x). 
unfold R; intuition. 
Qed. 


Definition interpret : form -> Prop. 
(* we use the well_founded_induction instead of Function *) 
refine (well_founded_induction_type R_wf (fun _ => Prop) (fun x f => _)). 
destruct x. 
exact True.          (* ⟦T⟧ ≡ True *) 
exact (n = 2 /\ f x (lem1 x n)).    (* ⟦K n F⟧ ≡ (n = 2) ∧ ⟦F⟧ *) 
exact (forall n:nat, f (K n x) (lem2 x n)).  (* ⟦eK F⟧ ≡ ∀n:nat,⟦K n F⟧ *) 
Defined. 

PS: Я собираюсь заполнить отчет об ошибке следующей простой версией вашего кода.

Require Import Recdef. 

    Inductive I : Set := 
    | C : I. 

    Definition m (_ : I) := 0. 

    Function f (x : I) {measure m x} : Type := match x with 
    | C => nat -> nat end. 
0

Сообщение об ошибке изменилось в Coq 8.4, но проблема все еще существует. Новое сообщение об ошибке: «Ошибка: Найденный товар не может относиться к такому термину.»

Это изменение в сообщении об ошибке также может привести к ошибке Марка, будучи закрытым: http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2457