Skip to content

Instantly share code, notes, and snippets.

@mukeshtiwari

mukeshtiwari/omega_not_solve.v

Created September 15, 2016 00:37
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save mukeshtiwari/fa4e52fe993207e6cd238499f2c23047 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
omega_not_solve.v
A : Type
O : Op A
l : list A
Hmon : mon O
Hfin : forall a : A, In a l
H : card l (iter O 0 full_ss) >= card l (iter O 1 full_ss) + 1
============================
card l (iter O 1 full_ss) + 1 <= card l (iter O 0 full_ss)
@mukeshtiwari
Copy link
Author

mukeshtiwari commented Sep 15, 2016

After doing some minor changes omega can solve

assert (card l (iter O 0 full_ss) >= card l (iter O 1 full_ss) + 1 ->
card l (iter O 1 full_ss) + 1 <= card l (iter O 0 full_ss)) by omega.
specialize (H0 H). omega.

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