coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Computing function results, mtkhan, 07/01/2013
- Re: [Coq-Club] Computing function results, Adam Chlipala, 07/01/2013
- Re: [Coq-Club] Computing function results, mtkhan, 07/01/2013
- Re: [Coq-Club] Computing function results, Vincent Siles, 07/01/2013
- Re: [Coq-Club] Computing function results, mtkhan, 07/01/2013
- Re: [Coq-Club] Computing function results, Vincent Siles, 07/01/2013
- Re: [Coq-Club] Computing function results, mtkhan, 07/01/2013
- Re: [Coq-Club] Computing function results, Vincent Siles, 07/01/2013
- Re: [Coq-Club] Computing function results, mtkhan, 07/01/2013
- Re: [Coq-Club] Computing function results, Adam Chlipala, 07/01/2013
Archive powered by MHonArc 2.6.18.