Great!. This worked perfectly and solved some persistent issues...:)
On Tue, Aug 28, 2018 at 12:54 AM <michael.norr...@data61.csiro.au> wrote:
> 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
>
--
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
