Don’t use abbreviations before starting your proof: it’s muddling your
quantifications.
Instead, use
!s. (?s0. s = StreamD s0) /\ P s ==> streams A s
as your goal and follow with
ho_match_mp_tac streams_coind >> dsimp[]
You will then end up with
∀s0.
P (StreamD s0) ⇒
∃a s0'. (StreamD s0 = a:::StreamD s0') ∧ a ∈ A ∧ P (StreamD s0')
as your goal.
Michael
From: Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Tuesday, 28 August 2018 at 13:53
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Lazy list: Stream in coinduction
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
