Hi,
I see that the coinduction scheme obtained from coinductively definition
predicate, in some cases, may require lazy list must not be LNIL. For
instance,
using the LUNFOLD, I've defined the stream function mainly to rule out the
LNIL case as:
|- StreamD xs = LUNFOLD (\n. SOME (THE (LTL n),THE (LHD n))) xs: thm
However, when I use it to for proving some useful properties over streams,
which is defined coinductively as:
|- !A a s. a IN A /\ streams A s ==> streams A (a:::s): thm
and the resulting coinductive scheme produced is:
|- !A streams'.
(!a0. streams' a0 ==> ?a s. (a0 = a:::s) /\ a IN A /\ streams' s)
==>
!a0. streams' a0 ==> streams A a0: thm
Suppose, I've a property of form:
`P (StreamD s) ==> streams A (StreamD s)`
By abbreviating the 'xs = StreamD s', I applied the coinduction scheme and
ends up:
?a xs'. (xs = a:::xs') /\ a IN A /\ Abbrev (xs' = xs) /\ P xs'
------------------------------------
0. Abbrev (xs = StreamD s)
1. P xs
The first conjunction can be easily made true by using `LHD xs` and `LTL
xs`. This also require that the lazy list 'xs' should not be LNIL, which
can also be easily inferred (from premise 0). However, this makes Abbrev
(LTL xs = xs) false..
Is there any way that I can use the coinduction scheme directly such that I
can have
∃a xs'. (StreamD xs = a:::xs') ∧ a ∈ A ∧ P xs'
------------------------------------
0. P xs
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
