Click on a command or tactic to see a detailed view of its use.
Type is_o o -> prop. Import "list" with is_o := is_o. [View list] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % adj J A K : K is J with A inserted somewhere Define adj : olist -> o -> olist -> prop by ; adj L A (A :: L) := is_o A /\ is_list L ; adj (B :: K) A (B :: L) := is_o B /\ adj K A L . Theorem adj_1_is_list : forall K A L, adj K A L -> is_list K. Theorem adj_2_is_o : forall K A L, adj K A L -> is_o A. Theorem adj_3_is_list : forall K A L, adj K A L -> is_list L. Theorem adj_exists : forall A L, is_o A -> is_list L -> exists M, adj L A M. Theorem adj_swap : forall A J K B L, adj J A K -> adj K B L -> exists U, adj J B U /\ adj U A L.induction on 2. intros. case H2. case H1. search. apply adj_1_is_list to H6. search. case H1. apply adj_3_is_list to H4. search. apply IH to H6 H4. search.Theorem adj_same : forall A L B, adj L A (B :: L) -> A = B. Theorem adj_append_1 : forall J A K L KL, adj J A K -> append K L KL -> exists JL, append J L JL /\ adj JL A KL.induction on 1. intros. case H1. case H2. apply append_2_is_list to H6. apply append_3_is_list to H6. search. case H2. apply IH to H4 H6. search.Theorem adj_1_append : forall J A K L JL, adj J A K -> append J L JL -> exists KL, append K L KL /\ adj JL A KL.induction on 1. intros. case H1. apply append_2_is_list to H2. apply append_3_is_list to H2. search. case H2. apply IH to H4 H6. search.%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % perm J K : J and K have the same elements Define perm : olist -> olist -> prop by ; perm nil nil ; perm K L := exists A KK LL, adj KK A K /\ adj LL A L /\ perm KK LL. Theorem perm_1_is_list : forall K L, perm K L -> is_list K. Theorem perm_2_is_list : forall K L, perm K L -> is_list L. Theorem perm_refl : forall L, is_list L -> perm L L. Theorem perm_sym : forall K L, perm K L -> perm L K. Theorem perm_cons_1 : forall A K L, perm (A :: K) L -> exists J, adj J A L /\ perm K J.induction on 1. intros. case H1. case H2. search. apply IH to H4. apply adj_swap to H7 H3. apply adj_1_is_list to H6. apply adj_1_is_list to H7. search.Theorem perm_cons_2 : forall A K L, perm K (A :: L) -> exists J, adj J A K /\ perm J L. Theorem adj_preserves_perm : forall A JJ J KK K, adj JJ A J -> adj KK A K -> perm JJ KK -> perm J K. Theorem perm_trans_lem : forall J K L, is_list K -> perm J K -> perm K L -> perm J L.induction on 1. intros. case H1. case H2. case H3. search. case H4. case H5. case H2. case H3. case H7. case H9. apply IH to *H5 *H8 *H11. search. apply perm_cons_1 to *H11. apply adj_swap to *H16 *H10. apply adj_preserves_perm to *H15 *H18 *H17. apply IH to *H5 *H8 *H20. backchain adj_preserves_perm. apply perm_cons_2 to *H8. apply adj_swap to *H14 *H6. apply adj_preserves_perm to *H16 *H13 *H15. apply adj_preserves_perm to *H9 *H10 *H11. apply perm_cons_1 to *H19. apply IH to *H5 *H18 *H21. backchain adj_preserves_perm.Theorem perm_trans : forall J K L, perm J K -> perm K L -> perm J L. Theorem adj_same_source : forall J A K L, adj J A K -> adj J A L -> perm K L. Theorem adj_same_result : forall J K A L, adj J A L -> adj K A L -> perm J K.induction on 1. intros. case H1. case H2. backchain perm_refl. apply adj_1_is_list to H6. apply perm_refl to H7. search. case H2. apply adj_1_is_list to H4. apply perm_refl to H7. search. apply IH to H4 H6. apply adj_1_is_list to H4. apply adj_1_is_list to H6. search.Theorem adj_same_result_diff : forall J A K B L, adj J A L -> adj K B L -> (A = B /\ perm J K) \/ exists KK, adj KK A K.induction on 1. intros. case H1. case H2. apply perm_refl to H4. search. right. witness K1. apply adj_1_is_list to H6. search. case H2. right. search. apply IH to H4 H6. case H7. apply adj_1_is_list to H4. apply adj_1_is_list to H6. search. search.Theorem adj_same_result_diff_both : forall J A K B L, adj J A L -> adj K B L -> (A = B /\ perm J K) \/ exists JJ KK, adj JJ B J /\ adj KK A K /\ perm JJ KK.induction on 1. intros. case H1. case H2. apply perm_refl to H4. search. right. witness K1, K1. apply adj_1_is_list to H6. apply perm_refl to H7. search. case H2. right. apply adj_1_is_list to H4. apply perm_refl to H7. search. apply IH to H4 H6. case H7. apply adj_1_is_list to H4. apply adj_1_is_list to H6. search. apply perm_1_is_list to H10. apply perm_2_is_list to H10. search.Theorem perm_invert : forall A J K JJ KK, perm J K -> adj JJ A J -> adj KK A K -> perm JJ KK.induction on 1. intros. case H1. case H2. apply adj_same_result_diff to H2 H4. case H7. apply adj_same_result_diff to H3 H5. case H9. apply perm_trans to *H8 *H6. apply perm_sym to *H10. backchain perm_trans. apply adj_same_result to H3 H5. apply perm_trans to *H8 *H6. apply perm_sym to *H11. backchain perm_trans. apply adj_same_result_diff to H3 H5. case H9. apply perm_sym to *H10. apply perm_trans to *H6 *H11. apply adj_same_result to H2 H4. backchain perm_trans. apply IH to H6 H8 H10. apply adj_swap to *H10 *H5. apply adj_swap to *H8 *H4. apply adj_same_result to *H2 *H15. apply adj_same_result to *H13 *H3. apply adj_preserves_perm to *H14 *H12 *H11. apply perm_trans to *H16 *H18. backchain perm_trans.Theorem adj_perm_result : forall J K A JJ, perm J K -> adj JJ A J -> exists KK, adj KK A K /\ perm JJ KK.induction on 1. intros. case H1. case H2. apply adj_same_result_diff to H2 H3. case H6. apply perm_trans to H7 H5. search. apply IH to H5 H7. apply adj_swap to H7 H3. apply adj_swap to H8 H4. witness U1. split. search. apply adj_same_result to H2 H11. apply adj_preserves_perm to H10 H12 H9. backchain perm_trans.Theorem adj_perm_source : forall J K A L, perm J K -> adj J A L -> exists LL, adj K A LL /\ perm L LL. Theorem adj_nil_1 : forall A L, adj nil A L -> L = A :: nil. Theorem perm_nil_1 : forall L, perm nil L -> L = nil. Theorem adj_det : forall A B L, adj L A (B :: nil) -> A = B /\ L = nil. Theorem perm_singleton : forall A L, perm (A :: nil) L -> L = (A :: nil). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% append and perm Theorem append_perm : forall J K L JJ KK, append J K L -> perm J JJ -> perm K KK -> exists LL, append JJ KK LL /\ perm L LL.induction on 1. intros. case H1. case H2. apply perm_2_is_list to H3. search. case H5. apply perm_cons_1 to *H2. apply IH to H5 H7 H3. apply adj_1_append to H6 H8. apply adj_3_is_list to H11. apply perm_1_is_list to H9. search.Theorem adj_perm : forall J K JJ A, perm J K -> adj JJ A J -> exists KK, adj KK A K.induction on 2. intros. case H2. apply perm_cons_1 to *H1. search. apply perm_cons_1 to *H1. apply IH to H6 H4. apply adj_swap to H7 H5. search.Theorem adj_perm_full : forall J K JJ A, perm J K -> adj JJ A J -> exists KK, adj KK A K /\ perm JJ KK.induction on 2. intros. case H2. apply perm_cons_1 to *H1. search. apply perm_cons_1 to *H1. apply IH to H6 H4. apply adj_swap to H7 H5. apply adj_1_is_list to H4. search.%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% set theoretic semantics of adj and perm Theorem adj_member : forall J A L, adj J A L -> member A L. Theorem member_adj : forall A L, is_list L -> member A L -> exists J, adj J A L. Theorem member_adj_rel : forall JJ A J B, adj JJ A J -> member B J -> A = B \/ member B JJ.induction on 1. intros. case H1. case H2. search. search. case H2. search. apply IH to *H4 H5. case H6. search. search.Theorem adj_preserves_member_lem : forall A J B L, is_list J -> member A J -> adj J B L -> member A L.induction on 2. intros. case H2. case H3. search. search. case H3. search. case H1. apply IH to H8 H4 H6. search.Theorem adj_preserves_member : forall A J B L, member A J -> adj J B L -> member A L. Theorem perm_preserves_member : forall A K L, perm K L -> member A K -> member A L.