The Coq mailing list

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

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