The Coq mailing list

[mtkhan AT risc.uni-linz.ac.at]

Dear Adam,

Thanks for your response. I do agree with you that the selection of
right constructs for defining functions (or any other logical prop)
helps in proving and also to find inconsistency in the theory, if there
is any.

However, I get this proof situation automatically translated from
a verification tool Why3 (http://why3.lri.fr); so in some sense
I have to live with it ;)

So any clue here?

regards,
tk




> 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.
>>
>