Databases
StackOverflow2013
Postsdbo
POUsing forall within recursive Function definition
Body
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POUsing forall within recursive Function definition
    text
    copied!<p>I'm trying to use Function to define a recursive definition using a measure, and I'm getting the error:</p> <pre><code>Error: find_call_occs : Prod </code></pre> <p>I'm posting the whole source code at the bottom, but my function is </p> <pre><code>Function kripke_sat (M : kripke) (s : U) (p : formula) {measure size p}: Prop := match p with | Proposition p' =&gt; L M (s)(p') | Not p' =&gt; ~ kripke_sat M s p' | And p' p'' =&gt; kripke_sat M s p' /\ kripke_sat M s p'' | Or p' p'' =&gt; kripke_sat M s p' \/ kripke_sat M s p'' | Implies p' p'' =&gt; ~kripke_sat M s p' \/ kripke_sat M s p'' | Knows a p' =&gt; forall t, ~(K M a) s t \/ kripke_sat M t p' | EvKnows p' =&gt; forall i, kripke_sat M s (Knows i p' ) end. </code></pre> <p>I know the problem is due to the foralls: if I replace them with True, it works. I also know I get the same error if my right-hand-side uses implications (->). Fixpoint works with foralls, but doesn't allow me to define a measure.</p> <p>Any advice?</p> <p>As promised, my complete code is:</p> <pre><code>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 -&gt; prop. Definition beq_prop (p1 p2 :prop) : bool := match (p1,p2) with | (Atomic p1', Atomic p2') =&gt; beq_nat p1' p2' end. Inductive actor : Type := | Id : P -&gt; actor. Definition beq_actor (a1 a2: actor) : bool := match (a1,a2) with | (Id a1', Id a2') =&gt; beq_nat a1' a2' end. Inductive formula : Type := | Proposition : prop -&gt; formula | Not : formula -&gt; formula | And : formula -&gt; formula -&gt; formula | Or : formula -&gt; formula -&gt; formula | Implies : formula -&gt; formula -&gt;formula | Knows : actor -&gt; formula -&gt; formula | EvKnows : formula -&gt; formula (*me*) . Inductive con : Type := | empty : con | ext : con -&gt; prop -&gt; con. Notation " C # P " := (ext C P) (at level 30). Require Import Relations. Record kripke : Type := mkKripke { K : actor -&gt; relation U; K_equiv: forall y, equivalence _ (K y); L : U -&gt; (prop -&gt; Prop) }. Fixpoint max (a b: nat) : nat := match a, b with | 0, _ =&gt; a | _, 0 =&gt; b | S(a'), S(b') =&gt; 1 + max a' b' end. Fixpoint length (p: formula) : nat := match p with | Proposition p' =&gt; 1 | Not p' =&gt; 1 + length(p') | And p' p'' =&gt; 1 + max (length p') (length p'') | Or p' p'' =&gt; 1 + max (length p') (length p'') | Implies p' p'' =&gt; 1 + max (length p') (length p'') | Knows a p' =&gt; 1 + length(p') | EvKnows p' =&gt; 1 + length(p') end. Fixpoint numKnows (p: formula): nat := match p with | Proposition p' =&gt; 0 | Not p' =&gt; 0 + numKnows(p') | And p' p'' =&gt; 0 + max (numKnows p') (numKnows p'') | Or p' p'' =&gt; 0 + max (numKnows p') (numKnows p'') | Implies p' p'' =&gt; 0 + max (numKnows p') (numKnows p'') | Knows a p' =&gt; 0 + numKnows(p') | EvKnows p' =&gt; 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 &gt; 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 -&gt; c&lt;d -&gt; a+ c&lt; 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' =&gt; L M (s)(p') | Not p' =&gt; ~ kripke_sat M s p' | And p' p'' =&gt; kripke_sat M s p' /\ kripke_sat M s p'' | Or p' p'' =&gt; kripke_sat M s p' \/ kripke_sat M s p'' | Implies p' p'' =&gt; ~kripke_sat M s p' \/ kripke_sat M s p'' | Knows a p' =&gt; forall t, ~(K M a) s t \/ kripke_sat M t p' | EvKnows p' =&gt; forall i, kripke_sat M s (Knows i p' ) end. </code></pre>
 

Querying!

 
Guidance
An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload