The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

I don't know what you expect: after the first rewrite, your goal becomes
true = isAddo (create_addo tt)

If we take a look at your isAddo0 axiom:

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

It says that IF isAddo a is true, then forall n .....

In your case, you want to prove that isAddo (create_addo tt) is true,
so I don't think you
gave us the correct axiom. Without more context, I don't know to help
you more, sorry.

2013/7/1  
<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.
>>>>>
>>>>
>>>
>>>
>>
>
>