Email Gateway (Aug 13 2025 at 14:55): Email Gateway (Aug 13 2025 at 14:55):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Dear List,
does anyone know if the subsequence preorder on lazy lists has been
formalized in Isabelle:
lsubseq :: 'a llist => 'a llist => bool
xs lsubseq ys, iff xs can be obtained by erasing an arbitrary number
of elements from ys
It should be reflexive and transitive, but is not antisymmetric:
1212... lsubseq 2121... lsubseq 1212...
I'm trying with the following definition:
definition "lsubseq a b ≡ ∃i. a = lmap snd (lfilter fst (lzip i b))"
reflexivity is straightforward, but proving transitivity seems
non-straightforward (with my limited knowledge of coinductive).
Any ideas, pointers to formalizations, etc?
--
Peter
Email Gateway (Aug 13 2025 at 15:02):From: Manuel Eberl <manuel@pruvisto.org>
Yes. It's called "subseq" and it is available in HOL-Library.Sublist.
It's a special case of the notion of the "homoeomorphic embedding"
list_emb, which lifts a relation R on list elements to a relation R on
lists, which basically works like the "list_all2" relator except that
you're also allowed to ignore elements in the second list entirely.
Cheers,
Manuel
On 13/08/2025 16:55, Peter (via cl-isabelle-users Mailing List) wrote:
Dear List,
does anyone know if the subsequence preorder on lazy lists has been
formalized in Isabelle:lsubseq :: 'a llist => 'a llist => bool
xs
lsubseqys, iff xs can be obtained by erasing an arbitrary number
of elements from ysIt should be reflexive and transitive, but is not antisymmetric:
1212...
lsubseq2121...lsubseq1212...I'm trying with the following definition:
definition "lsubseq a b ≡ ∃i. a = lmap snd (lfilter fst (lzip i b))"
reflexivity is straightforward, but proving transitivity seems
non-straightforward (with my limited knowledge of coinductive).Any ideas, pointers to formalizations, etc?
--
Peter
Email Gateway (Aug 13 2025 at 15:09):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
@Manuel: That one is on ordinary lists, whereas Peter asked for lazy lists.
@Peter: There is the emb function on lazy lists here:
This one has the extra feature that finite lazy lists are only embedded in other finite lazy lists. To omit that one could simply drop the lfinite assumption in the first introduction rule.
I don’t think we proved transitivity or reflexivity, but both should hold.
Dmitriy
On 13 Aug 2025, at 17.01, Manuel Eberl <manuel@pruvisto.org> wrote:
Yes. It's called "subseq" and it is available in HOL-Library.Sublist.
It's a special case of the notion of the "homoeomorphic embedding" list_emb, which lifts a relation R on list elements to a relation R on lists, which basically works like the "list_all2" relator except that you're also allowed to ignore elements in the second list entirely.
Cheers,
Manuel
On 13/08/2025 16:55, Peter (via cl-isabelle-users Mailing List) wrote:
Dear List,
does anyone know if the subsequence preorder on lazy lists has been formalized in Isabelle:
lsubseq :: 'a llist => 'a llist => bool
xs lsubseq ys, iff xs can be obtained by erasing an arbitrary number of elements from ys
It should be reflexive and transitive, but is not antisymmetric:
1212... lsubseq 2121... lsubseq 1212...
I'm trying with the following definition:
definition "lsubseq a b ≡ ∃i. a = lmap snd (lfilter fst (lzip i b))"
reflexivity is straightforward, but proving transitivity seems non-straightforward (with my limited knowledge of coinductive).
Any ideas, pointers to formalizations, etc?
--
Peter
Email Gateway (Aug 13 2025 at 15:59):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Indeed:
lemma emb_refl: "emb lxs lxs"
proof (coinduction arbitrary: lxs)
case (emb lxs)
then show ?case
by (cases lxs) (auto intro!: exI[of _ "[]"])
qed
lemma emb_prepedD: "emb (prepend xs lxs) lys ⟹ emb lxs lys"
by (induct xs arbitrary: lys)
(auto elim!: emb_LConsE simp add: emb_prepend prepend_LCons)
lemma emb_trans: "emb lxs lys ⟹ emb lys lzs ⟹ emb lxs lzs"
proof (coinduction arbitrary: lxs lys lzs)
case (emb lxs lys lzs)
then show ?case
proof (cases lxs rule: llist.exhaust)
case LNil
then show ?thesis
using emb emb_lfinite by auto
next
case (LCons x lxs')
with emb show ?thesis
unfolding LCons
by (auto dest!: emb_prepedD elim!: emb_LConsE)
qed
qed
Dmitriy
On 13 Aug 2025, at 17.09, Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk> wrote:
@Manuel: That one is on ordinary lists, whereas Peter asked for lazy lists.
@Peter: There is the emb function on lazy lists here:
This one has the extra feature that finite lazy lists are only embedded in other finite lazy lists. To omit that one could simply drop the lfinite assumption in the first introduction rule.
I don’t think we proved transitivity or reflexivity, but both should hold.
Dmitriy
On 13 Aug 2025, at 17.01, Manuel Eberl <manuel@pruvisto.org> wrote:
Yes. It's called "subseq" and it is available in HOL-Library.Sublist.
It's a special case of the notion of the "homoeomorphic embedding" list_emb, which lifts a relation R on list elements to a relation R on lists, which basically works like the "list_all2" relator except that you're also allowed to ignore elements in the second list entirely.
Cheers,
Manuel
On 13/08/2025 16:55, Peter (via cl-isabelle-users Mailing List) wrote:
Dear List,
does anyone know if the subsequence preorder on lazy lists has been formalized in Isabelle:
lsubseq :: 'a llist => 'a llist => bool
xs lsubseq ys, iff xs can be obtained by erasing an arbitrary number of elements from ys
It should be reflexive and transitive, but is not antisymmetric:
1212... lsubseq 2121... lsubseq 1212...
I'm trying with the following definition:
definition "lsubseq a b ≡ ∃i. a = lmap snd (lfilter fst (lzip i b))"
reflexivity is straightforward, but proving transitivity seems non-straightforward (with my limited knowledge of coinductive).
Any ideas, pointers to formalizations, etc?
--
Peter
Email Gateway (Aug 13 2025 at 16:19):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Nice, thank you!
your proof works without adaptation on the version without lfinite.
--
Peter
p.s.
I was almost there, but didn't see that I needed to generalize over
lzs ... lack of experience with coinductive, as said ;)
On 13/08/2025 17:59, Dmitriy Traytel (via cl-isabelle-users Mailing
List) wrote:
Indeed:
lemma emb_refl: "emb lxs lxs"
proof (coinduction arbitrary: lxs)
case (emb lxs)
then show ?case
by (cases lxs) (auto intro!: exI[of _ "[]"])
qedlemma emb_prepedD: "emb (prepend xs lxs) lys ⟹ emb lxs lys"
by (induct xs arbitrary: lys)
(auto elim!: emb_LConsE simp add: emb_prepend prepend_LCons)lemma emb_trans: "emb lxs lys ⟹ emb lys lzs ⟹ emb lxs lzs"
proof (coinduction arbitrary: lxs lys lzs)
case (emb lxs lys lzs)
then show ?case
proof (cases lxs rule: llist.exhaust)
case LNil
then show ?thesis
using emb emb_lfinite by auto
next
case (LCons x lxs')
with emb show ?thesis
unfolding LCons
by (auto dest!: emb_prepedD elim!: emb_LConsE)
qed
qedDmitriy
On 13 Aug 2025, at 17.09, Dmitriy Traytel
<cl-isabelle-users@lists.cam.ac.uk> wrote:@Manuel: That one is on ordinary lists, whereas Peter asked for lazy
lists.@Peter: There is the emb function on lazy lists here:
https://www.isa-afp.org/sessions/ordered_resolution_prover/#Lazy_List_Chain.html%23Lazy_List_Chain.emb|const
<https://www.isa-afp.org/sessions/ordered_resolution_prover/#Lazy_List_Chain.html%2523Lazy_List_Chain.emb%7Cconst>This one has the extra feature that finite lazy lists are only
embedded in other finite lazy lists. To omit that one could simply
drop the lfinite assumption in the first introduction rule.I don’t think we proved transitivity or reflexivity, but both should
hold.Dmitriy
On 13 Aug 2025, at 17.01, Manuel Eberl <manuel@pruvisto.org> wrote:
Yes. It's called "subseq" and it is available in HOL-Library.Sublist.
It's a special case of the notion of the "homoeomorphic embedding"
list_emb, which lifts a relation R on list elements to a relation R
on lists, which basically works like the "list_all2" relator except
that you're also allowed to ignore elements in the second list entirely.Cheers,
Manuel
On 13/08/2025 16:55, Peter (via cl-isabelle-users Mailing List) wrote:
Dear List,
does anyone know if the subsequence preorder on lazy lists has been
formalized in Isabelle:lsubseq :: 'a llist => 'a llist => bool
xs
lsubseqys, iff xs can be obtained by erasing an arbitrary
number of elements from ysIt should be reflexive and transitive, but is not antisymmetric:
1212...
lsubseq2121...lsubseq1212...I'm trying with the following definition:
definition "lsubseq a b ≡ ∃i. a = lmap snd (lfilter fst (lzip i b))"
reflexivity is straightforward, but proving transitivity seems
non-straightforward (with my limited knowledge of coinductive).Any ideas, pointers to formalizations, etc?
--
Peter
Last updated: Aug 20 2025 at 20:23 UTC