New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Missing lemmas #1

Closed

pi8027 opened this issue Mar 26, 2021 · 0 comments · Fixed by #2

Owner

pi8027 commented Mar 26, 2021

stablesort/theories/stablesort.v

Lines 351 to 352 in 2c5694b

    
           (* TODO: *) 
        
           (* Lemma mem2_sort s x y : leT x y -> mem2 s x y -> mem2 (sort _ leT s) x y. *)

stablesort/theories/stablesort.v

Lines 377 to 380 in 2c5694b

    
           (* TODO: *) 
        
           (* Lemma mem2_sort_in s : *) 
        
           (*   {in s &, total leT} -> {in s & &, transitive leT} -> *) 
        
           (*   forall x y, leT x y -> mem2 s x y -> mem2 (sort _ leT s) x y. *)

sort leT (s1 ++ s2) = merge leT (sort leT s1) (sort leT s2)
sort _ (sort _ _) = sort _ _

The text was updated successfully, but these errors were encountered:

pi8027 mentioned this issue

Add sort_sort(_in) lemmas #2

Merged

pi8027 closed this as completed in #2

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