The Coq mailing list

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

Hi Vincent and Pierre,

Yea these worked for the isDDO case. What about the other function
isAddo? Any clue here?

Thanks.
taimoor


> Dear tk,
> you can try to assert a specialized version of your axiom and then use
> it to rewrite your goal, something like:
>
> assert (HH := isDDO_def nil a1 b0 b).
> simpl in HH.
> rewrite HH.
>
>
> I'm pretty sure there is a nicer way to do this, but I don't know it :)
>
> Cheers,
> V.
>
> 2013/7/1  
> <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.
>>>>
>>>
>>
>>
>