The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

Dear all,

I am trying to define a realizability relation for a first order
theory. Basically, I need to define a relation by recursion on
formulas of the theory. Below is a (hopefully not oversimplified)
example of what I am trying to achive. My questions:

1. Are there better approaches? (For example maybe it is better to use
Coq only as metatheory with which to formalize first order logic?)
2. How do I define the realizability relation so that Coq accepts it?

The example (pastebin: http://pastebin.com/tQC4KGJj):


Parameter A : Type.

(* imagine that A has pairing and think of these as projections, if you want 
to
   make sense of the realizability definition below *)
Parameter p0 p1 : A -> A.

Inductive is_A_atom : Prop -> Prop :=
| eq_false          : is_A_atom False
| eq_atom (a b : A) : is_A_atom (a = b).

Inductive is_A_formula : Prop -> Type :=
| atom_formula P   : is_A_atom P -> is_A_formula P
| and_formula  P Q : is_A_formula P -> is_A_formula Q -> is_A_formula (P /\ 
Q).

Definition A_formulas := {P : Prop & is_A_formula P}.

(* gives recursive call has principal argument ... not equal to subterm of P 
*)
Fixpoint realizes (P : A_formulas) : A -> Prop := fun a =>
let (P, pf) := P in match pf with
| atom_formula _ _          => P
| and_formula P Q pf_P pf_Q => realizes (existT _ P pf_P) (p0 a) /\
                               realizes (existT _ Q pf_Q) (p1 a)
end.

(* this is the form I would prefer, this gives "cannot guess decreasing
   argument of fix". I guess this is caused by the above error *)
Fixpoint realizes' (a : A) (P : A_formulas) : Prop :=
let (P, pf) := P in match pf with
| atom_formula _ _          => P
| and_formula P Q pf_P pf_Q => realizes' (p0 a) (existT _ P pf_P) /\
                               realizes' (p1 a) (existT _ Q pf_Q)
end.


Best regards,

Anders Lundstedt