-- File: sort -- This file contains the example of sorting of records, as in Section 8.4. Path "../lol" Path "../lolplus" Load "lambdaLsubplus" Load "sort" -- so we have Perm ----------------------- -- PREDICATE Ordered -- ----------------------- Def OrderedId := \B<:{|id:Nat|}. \l:List B. @P:List B -> *p. P (nil B) -> (@a:B.@m:List B. P m -> (@b:B. Elem b m -> a`id<=b`id) -> P (a;m)) -> P l : @B<:{|id:Nat|}. List B -> *p Implicit 1 OrderedId Prove OrderedId_nil : @B<:{|id:Nat|}. OrderedId (nil B) Unfold OrderedId Intros Assumption Exit Prove OrderedId_cons : @B<:{|id:Nat|}.@a:B.@m:List B. OrderedId m -> (@b:B. Elem b m -> a`id<=b`id) -> OrderedId (a;m) Intros Unfold OrderedId Intros Apply H3 Apply H Then Assumption Assumption Exit Prove OrderedId_singleton : @B<:{|id:Nat|}. @m:B. OrderedId (singleton m) Intros Apply OrderedId_cons Apply OrderedId_nil Intros FalseE Apply Elem_nil_ On H Exit Prove OrderedId_exh : @B<:{|id:Nat|}. @l:List B. OrderedId l -> l = nil B \/ Ex a:B. Ex m:List B. l = a;m /\ (@b:B. Elem b m -> a`id<=b`id) /\ OrderedId m Intros Apply H OrIL Refl Intros OrIR ExistsI a ExistsI m AndI Refl AndI Assumption OrE H1 Rewrite H3 Apply OrderedId_nil ExistsE H3 ExistsE H4 AndE H5 Rewrite H6 AndE H7 Apply OrderedId_cons Assumption Assumption Exit Prove OrderedId_cons_ : @B<:{|id:Nat|}. @a:B.@m:List B. OrderedId (a;m) -> (@b:B. Elem b m -> a`id<=b`id) /\ OrderedId m Intros 4 OrE OrderedId_exh On H FalseE Apply cons_is_nil_ On H2 ExistsE H2 ExistsE H3 AndE H4 AndE cons_is_cons_ On H5 Rewrite H8 Repeat Rewrite H9 Assumption Exit ----------------------- -- FUNCTION insertId -- ----------------------- Def insertId := \B<:{|id:Nat|}. \n:B. primreclist (singleton n) ( \head:B. \tail:List B. \insert_tail:List B. if (leq n`id head`id) (n;head;tail) (head;insert_tail)) : @B<:{|id:Nat|}. B -> List B -> List B implicit 1 insertId Prove insertId_nil : @B<:{|id:Nat|}. @m:B. insertId m (nil B) = singleton m Intros Unfold insertId Apply primreclist_nil Exit Prove Le__insertId : @B<:{|id:Nat|}. @m,n:B.@l:List B. m`id<=n`id -> insertId m (n;l) = m;n;l Intros Unfold insertId Rewrite primreclist_cons Rewrite Le__leq_true On H Rewrite if_true Refl Exit Prove Gt__insertId : @B<:{|id:Nat|}. @m,n:B.@l:List B. n`id<m`id -> insertId m (n;l) = n;(insertId m l) Intros Unfold 1 insertId Rewrite primreclist_cons Rewrite Gt__leq_false On H Rewrite if_false Refl Exit Prove Elem_insertId_ : @B<:{|id:Nat|}. @m,n:B.@ns:List B. Elem m (insertId n ns) -> m=n \/ Elem m ns Intros 3 Apply indlist Rewrite insertId_nil Unfold singleton Intro OrIL OrE Elem_cons_ On H Then Try Assumption FalseE Apply Elem_nil_ On H2 Intros 2 OrE Le_Or_Gt n`id a`id Rewrite Le__insertId Assumption Intros Apply Elem_cons_ Assumption Rewrite Gt__insertId Then Try Assumption Intros OrE Elem_cons_ On H2 OrIR Rewrite H4 Apply Elem_a_a_cons OrE H1 On H4 OrIL Assumption OrIR Apply Elem_a_b_cons Assumption Exit Prove OrderedId_insertId : @B<:{|id:Nat|}. @m:B. @l:List B. OrderedId l -> OrderedId (insertId m l) Intros 2 Apply indlist Intro Rewrite insertId_nil Apply OrderedId_singleton Intros AndE OrderedId_cons_ On H1 OrE Le_Or_Gt On m`id, a`id Rewrite Le__insertId Then Try Assumption Apply OrderedId_cons Assumption Intros Apply Le_trans On H6 OrE Elem_cons_ On H7 Rewrite H9 Apply Le_refl Apply H3 Then Assumption Rewrite Gt__insertId Then Try Assumption Apply OrderedId_cons Apply H Then Assumption Intros OrE Elem_insertId_ On H7 Rewrite H9 Apply m_Lt_n__m_Le_n Assumption Apply H3 Assumption Exit Prove Perm_insertId : @B<:{|id:Nat|}. @m:B. @l:List B. Perm (insertId m l) (m;l) Intros 2 Apply indlist Rewrite insertId_nil Apply Perm_refl Intros OrE Le_Or_Gt On m`id, a`id Rewrite Le__insertId Assumption Apply Perm_refl Rewrite Gt__insertId Assumption Apply Perm_trans On a;m;as Apply Perm_cons Assumption First Perm (nil B ++ (a;m;as)) (nil B ++ (m;a;as)) Apply Perm_swap Repeat Rewrite nil_concat Intro Then Assumption Exit ------------ -- sortId -- ------------ Def sortId := \B<:{|id:Nat|}. primreclist (nil B) (\head:B. \tail:List B. \sort_tail:List B. insertId head sort_tail) : @B<:{|id:Nat|}. List B -> List B Implicit 1 sortId Prove sortId_nil : @B<:{|id:Nat|}. sortId (nil B) = nil B Intro Unfold sortId Apply primreclist_nil Exit Prove sortId_cons : @B<:{|id:Nat|}. @m:B.@l:List B. sortId (m;l) = insertId m (sortId l) Intros Unfold 1 sortId Apply primreclist_cons Exit Prove OrderedId_sortId : @B<:{|id:Nat|}. @l:List B. OrderedId (sortId l) Intro Apply indlist Rewrite sortId_nil Apply OrderedId_nil Intros Rewrite sortId_cons Apply OrderedId_insertId Assumption Exit Prove Perm_sortId : @B<:{|id:Nat|}. @l:List B. Perm (sortId l) l Intro Apply indlist Rewrite sortId_nil Apply Perm_refl Intros Rewrite sortId_cons Forward Perm_cons On a, H Apply Perm_trans On H1 Apply Perm_insertId Exit