Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Computing function results

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Computing function results


Chronological Thread 
  • From: mtkhan AT risc.uni-linz.ac.at
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Computing function results
  • Date: Mon, 1 Jul 2013 11:10:08 +0200 (CEST)
  • Importance: Normal

Hi,

I have the following proof situation

1 subgoal
m : list (symbol * list Z * list Z * symbol)
a : addo
b : list symbol
a1 : Z
b0 : Z
H : a = to_abstract_addo (a1, b0, b) m
______________________________________(1/1)
isDDO m a1 b0 b = isAddo (to_abstract_addo (a1, b0, b) m)

as m is a list, I can run induction over m. By executing following commands


induction m.
simpl.

the situation simplifies to the following:

2 subgoals
a : addo
b : list symbol
a1 : Z
b0 : Z
H : a = to_abstract_addo (a1, b0, b) Nil
______________________________________(1/2)
isDDO Nil a1 b0 b = isAddo (create_addo tt)


______________________________________(2/2)
isDDO (Cons a0 m) a1 b0 b = isAddo (to_abstract_addo (a1, b0, b) (Cons a0 m))

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. For example, in isDDO_def, the pattern
Nil returns true; but I don't have any clue here.

Can any one help me here in computing function results on either
side of the goal?

Thanks.

regards,
tk






Archive powered by MHonArc 2.6.18.

Top of Page