Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/existential.v

Created October 3, 2016 05:55
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mukeshtiwari/9fa2c9d20faab7faccecb214bdf6becc to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mukeshtiwari/9fa2c9d20faab7faccecb214bdf6becc to your computer and use it in GitHub Desktop.
Download ZIP
Raw
existential.v
T : Type
re, re0 : reg_exp T
Heqre' : Star re0 = Star re
s1, s2 : list T
H : s1 =~ re0
H0 : s2 =~ Star re0
IHexp_match1 : re0 = Star re ->
exists ss : list (list T),
s1 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)
x : list (list T)
H1 : s2 = fold app x [ ]
H2 : forall s' : list T, In s' x -> s' =~ re
============================
exists ss : list (list T),
s1 ++ s2 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)
@mukeshtiwari
Copy link
Author

mukeshtiwari commented Oct 3, 2016

T : Type
re, re0 : reg_exp T
Heqre' : Star re0 = Star re
s1, s2 : list T
H : s1 =~ re0
H0 : s2 =~ Star re0
IHexp_match1 : re0 = Star re ->
exists ss : list (list T),
s1 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)
IHexp_match2 : Star re0 = Star re ->
exists ss : list (list T),
s2 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)

exists ss : list (list T),
s1 ++ s2 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment