The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Has someone suggested before giving proper definitions of your 
identifiers with [Inductive] and [Fixpoint] rather than [Parameter] and 
[Axiom]?  Coq users tend to be skeptical of any development using axioms 
in the way that you are.  You certainly get much more convenient term 
simplification doing things more idiomatically.  If you _can't_ define 
your notions constructively, then how are you convincing yourself that 
they are logically consistent?

On 07/01/2013 05:10 AM, 
mtkhan AT risc.uni-linz.ac.at
 wrote:
> I have the following function definitions of isDDO and isAddo:
>
> Parameter isAddo: addo ->  bool.
>
> Parameter isDDO: (list (symbol* (list Z)* (list Z)* symbol)%type) ->  Z ->  Z
>    ->  (list symbol) ->  bool.
>
> Axiom isDDO_def : forall (a:(list (symbol* (list Z)* (list Z)* symbol)%type))
>    (anzdelta:Z) (anzsigma:Z) (g:(list symbol)),
>    match a with
>    | Nil =>  ((isDDO a anzdelta anzsigma g) = true)
>    | (Cons e l) =>  (((isDDOTerm e anzdelta anzsigma g) = true) ->  ((isDDO a
>        anzdelta anzsigma g) = (isDDO l anzdelta anzsigma g))) /\
>        ((~ ((isDDOTerm e anzdelta anzsigma g) = true)) ->  ((isDDO a anzdelta
>        anzsigma g) = false))
>    end.
>
> Axiom isAddo0 : forall (a:addo), ((isAddo a) = true) ->  forall (n:Z),
>    ((0%Z<= n)%Z /\ (n<  (length_addo a))%Z) ->
>    ((isAddo_term (get_addo_data a) (get_addo_term a n)) = true).
>
>
> In the first goal, I simply need to compute the function results
> and it should simply work.
>