Changeset 3050 for src/utilities


Ignore:
Timestamp:
Apr 1, 2013, 5:18:05 PM (8 years ago)
Author:
piccolo
Message:

1) Added general commutation theorem for monads.

2) Added some commutation lemma for push and pop that can be useful
for sigle steps of correctness proof.

3) fixed some bugs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/listb_extra.ma

    r2728 r3050  
    11include "basics/lists/listb.ma".
    22include "ASM/Util.ma".
     3include "utilities/lists.ma".
    34
    45lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
     
    1718] qed.
    1819
     20
     21lemma nth_opt_Exists : ∀A,n,l,a.
     22  nth_opt A n l = Some A a →
     23  Exists A (λa'. a' = a) l.
     24#A #n elim n
     25[ * [ #a #E normalize in E; destruct | #a #l #a' #E normalize in E; destruct % // ]
     26| #m #IH *
     27  [ #a #E normalize in E; destruct
     28  | #a #l #a' #E %2 @IH @E
     29  ]
     30] qed.
     31
     32
     33lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
     34decidable (In A l a).
     35#A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
     36[ #H % %2 assumption | * #H cases (DEC hd)
     37[ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]]
     38qed.
     39
     40lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
     41#A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
     42% #H1 @H % >H1 %
     43qed.
     44
     45lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
     46#A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *
     47[ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption]
     48qed.
     49
     50lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
     51All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
     52#A #P #l1 elim l1
     53[ #l2 change with l2 in ⊢ (???% → ?); #H % //]
     54#a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
     55* #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
     56qed.
Note: See TracChangeset for help on using the changeset viewer.