Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (9 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1647 r1882  
    11include "basics/lists/list.ma".
     2include "ASM/Util.ma". (* coercion from bool to Prop *)
     3
     4lemma All_map : ∀A,B,P,Q,f,l.
     5All A P l →
     6(∀a.P a → Q (f a)) →
     7All B Q (map A B f l).
     8#A #B #P #Q #f #l elim l //
     9#h #t #IH * #Ph #Pt #F % [@(F ? Ph) | @(IH Pt F)] qed.
     10
     11lemma Exists_map : ∀A,B,P,Q,f,l.
     12Exists A P l →
     13(∀a.P a → Q (f a)) →
     14Exists B Q (map A B f l).
     15#A #B #P #Q #f #l elim l //
     16#h #t #IH * #H #F
     17[ %1 @(F ? H) | %2 @(IH H F) ]
     18qed.
    219
    320lemma All_append : ∀A,P,l,r. All A P l → All A P r → All A P (l@r).
     
    3249] qed.
    3350
     51lemma All_split : ∀A,P,l. All A P l → ∀pre,x,post.l = pre @ x :: post → P x.
     52#A #P #l elim l
     53[ * * normalize [2: #y #pre'] #x #post #ABS destruct(ABS)
     54| #hd #tl #IH * #Phd #Ptl * normalize [2: #y #pre'] #x #post #EQ destruct(EQ)
     55  [ @(IH Ptl … (refl …))
     56  | @Phd
     57  ]
     58]
     59qed.
     60
    3461let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
    3562match la with
     
    5784] H.
    5885
     86lemma All_rev : ∀A,P,l.All A P l → All A P (rev ? l).
     87#A#P#l elim l //
     88#h #t #Hi * #Ph #Pt normalize
     89>rev_append_def
     90@All_append
     91[ @(Hi Pt)
     92| %{Ph I}
     93]
     94qed.
     95
     96lemma Exists_rev : ∀A,P,l.Exists A P l → Exists A P (rev ? l).
     97#A#P#l elim l //
     98#h #t #Hi normalize >rev_append_def
     99* [ #Ph @Exists_append_r %{Ph} | #Pt @Exists_append_l @(Hi Pt)]
     100qed.
     101
     102include "utilities/option.ma".
     103
     104lemma find_All : ∀A,B.∀P : A → Prop.∀Q : B → Prop.∀f.(∀x.P x → opt_All ? Q (f x)) →
     105  ∀l. All ? P l → opt_All ? Q (find … f l).
     106#A#B#P#Q#f#H#l elim l [#_%]
     107#x #l' #Hi
     108* #Px #AllPl'
     109whd in ⊢ (???%);
     110lapply (H x Px)
     111lapply (refl ? (f x))
     112generalize in ⊢ (???%→?); #o elim o [2: #b] #fx_eq >fx_eq [//]
     113#_ whd in ⊢ (???%); @(Hi AllPl')
     114qed.
     115
    59116include "utilities/monad.ma".
    60117
     
    65122  list
    66123  (λX,x.[x])
    67   (λX,Y,l,f.\fold [append ?, [ ]]_{x ∈ l} (f x))
    68   ???. normalize
     124  (λX,Y,l,f.foldr … (λx.append ? (f x)) [ ] l)
     125  ????. normalize
    69126[ / by /
    70127| #X#m elim m normalize //
    71128| #X#Y#Z #m #f#g
    72129  elim m normalize [//]
    73   #x#l' #Hi
    74   <(fold_sum ?? (f x) ? [ ] (Append ?))
    75   >Hi //
     130  #x#l' #Hi elim (f x)
     131  [@Hi] normalize #hd #tl #IH >associative_append >IH %
     132|#X#Y#m #f #g #H elim m normalize [//]
     133  #hd #tl #IH >H >IH %
    76134] qed.
    77135
    78136unification hint 0 ≔ X ;
    79 N ≟ max_def List, M ≟ m_def N
     137N ≟ max_def List
    80138(*---------------------------*)⊢
    81 list X ≡ monad M X.
     139list X ≡ monad N X.
     140
     141definition In ≝ λA.λl : list A.λx : A.Exists A (eq ? x) l.
     142
     143lemma All_In : ∀A,P,l,x. All A P l → In A l x → P x.
     144#A#P#l#x #Pl #xl elim (Exists_All … xl Pl)
     145#x' * #EQx' >EQx' //
     146qed.
     147
     148lemma In_All : ∀A,P,l.(∀x.In A l x → P x) → All A P l.
     149#A#P#l elim l
     150[#_ %
     151|#x #l' #IH #H %
     152  [ @H % %
     153  | @IH #y #G @H %2 @G
     154  ]
     155]
     156qed.
     157
     158
     159lemma nth_opt_append_l : ∀A,l1,l2,n.|l1| > n → nth_opt A n (l1 @ l2) = nth_opt A n l1.
     160#A#l1 elim l1 normalize
     161[ #l2 #n #ABS elim (absurd ? ABS ?) //
     162| #x #l' #IH #l2 #n cases n normalize
     163  [//
     164  | #n #H @IH @le_S_S_to_le assumption
     165  ]
     166]
     167qed.
     168
     169lemma nth_opt_append_r : ∀A,l1,l2,n.|l1| ≤ n → nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
     170#A#l1 elim l1
     171[#l2 #n #_ <minus_n_O %
     172|#x #l' #IH #l2 #n normalize in match (|?|); whd in match (nth_opt ???);
     173  cases n -n
     174  [  #ABS elim (absurd ? ABS ?) //
     175  | #n #H whd in ⊢ (??%?); >minus_S_S @IH @le_S_S_to_le assumption
     176  ]
     177]
     178qed.
     179
     180lemma nth_opt_append_hit_l : ∀A,l1,l2,n,x. nth_opt A n l1 = Some ? x →
     181  nth_opt A n (l1 @ l2) = Some ? x.
     182#A #l1 elim l1 normalize
     183[ #l2 #n #x #ABS destruct
     184| #hd #tl #IH #l2 * [2: #n] #x normalize /2 by /
     185]
     186qed.
     187
     188lemma nth_opt_append_miss_l : ∀A,l1,l2,n. nth_opt A n l1 = None ? →
     189  nth_opt A n (l1 @ l2) = nth_opt A (n - |l1|) l2.
     190#A #l1 elim l1 normalize
     191[ #l2 #n #_ <minus_n_O %
     192| #hd #tl #IH #l2 * [2: #n] normalize
     193  [ @IH
     194  | #ABS destruct(ABS)
     195  ]
     196]
     197qed.
     198
     199 
     200(* count occurrences satisfying a test *)
     201let rec count A (f : A → bool) (l : list A) on l : ℕ ≝
     202  match l with
     203  [ nil ⇒ 0
     204  | cons x l' ⇒ (if f x then 1 else 0) + count A f l'
     205  ].
     206 
     207theorem count_append : ∀A,f,l1,l2.count A f (l1@l2) = count A f l1 + count A f l2.
     208#A #f #l1 elim l1
     209[ #l2 %
     210| #hd #tl #IH #l2 normalize elim (f hd) normalize >IH %
     211]
     212qed.
     213
     214
     215include "utilities/option.ma".
     216
     217lemma position_of_from_aux : ∀A,test,l,n.
     218  position_of_aux A test l n = !n' ← position_of A test l; return n + n'.
     219#A #test #l elim l
     220[ normalize #_ %
     221| #hd #tl #IH #n
     222  normalize in ⊢ (??%?); >IH
     223  normalize elim (test hd) normalize
     224  [ <plus_n_O %
     225  | >(IH 1) whd in match (position_of ???);
     226    elim (position_of_aux ??? 0) normalize
     227    [ % | #x <plus_n_Sm % ]
     228  ]
     229]
     230qed.
     231
     232definition position_of_safe ≝ λA,test,l.λprf : count A test l ≥ 1.
     233  opt_safe ? (position_of A test l) ?.
     234  lapply prf -prf elim l normalize
     235  [ #ABS elim (absurd ? ABS (not_le_Sn_O 0))
     236  |#hd #tl #IH elim (test hd) normalize
     237    [2: >position_of_from_aux #H
     238      change with (position_of_aux ????) in match (position_of ???);
     239      >(opt_to_opt_safe … (IH H)) @opt_safe_elim normalize #x]
     240    #_ % #ABS destruct(ABS)
     241qed.
     242
     243definition index_of ≝
     244  λA,test,l.λprf : eqb (count A test l) 1.position_of_safe A test l ?.
     245  lapply prf -prf @eqb_elim #EQ * >EQ %
     246qed.
     247
     248lemma position_of_append_hit : ∀A,test,l1,l2,x.
     249  position_of A test (l1@l2) = Some ? x →
     250    position_of A test l1 = Some ? x ∨
     251      (position_of A test l1 = None ? ∧
     252        ! p ← position_of A test l2 ; return (|l1| + p) = Some ? x).
     253#A#test#l1 elim l1
     254[ #l2 #x change with l2 in match (? @ l2); #EQ >EQ %2
     255  % %
     256| #hd #tl #IH #l2 #x
     257  normalize elim (test hd) normalize
     258  [#H %{H}
     259  | >position_of_from_aux
     260    lapply (refl … (position_of A test (tl@l2)))
     261    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
     262    normalize #EQ destruct(EQ)
     263    elim (IH … Heq) -IH
     264    [ #G %
     265    | * #G #H
     266     lapply (refl … (position_of A test l2))
     267     generalize in ⊢ (???%→?); * [2: #x'] #H' >H' in H; normalize
     268     #EQ destruct (EQ) %2 %]
     269    >position_of_from_aux
     270    [1,2: >G % | >H' %]
     271  ]
     272]
     273qed.
     274
     275lemma position_of_hit : ∀A,test,l,x.position_of A test l = Some ? x →
     276  count A test l ≥ 1.
     277#A#test#l elim l normalize
     278[#x #ABS destruct(ABS)
     279|#hd #tl #IH #x elim (test hd) normalize [#EQ destruct(EQ) //]
     280  >position_of_from_aux
     281  lapply (refl … (position_of ? test tl))
     282  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
     283  #EQ destruct(EQ) @(IH … Heq)
     284]
     285qed.
     286
     287lemma position_of_miss : ∀A,test,l.position_of A test l = None ? →
     288  count A test l = 0.
     289#A#test#l elim l normalize
     290[ #_ %
     291|#hd #tl #IH elim (test hd) normalize [#EQ destruct(EQ)]
     292  >position_of_from_aux
     293  lapply (refl … (position_of ? test tl))
     294  generalize in ⊢ (???%→?); * [2: #x'] #Heq >Heq normalize
     295  #EQ destruct(EQ) @(IH … Heq)
     296]
     297qed.
     298
     299
     300lemma position_of_append_miss : ∀A,test,l1,l2.
     301  position_of A test (l1@l2) = None ? →
     302    position_of A test l1 = None ? ∧ position_of A test l2 = None ?.
     303#A#test#l1 elim l1
     304[ #l2 change with l2 in match (? @ l2); #EQ >EQ % %
     305| #hd #tl #IH #l2
     306  normalize elim (test hd) normalize
     307  [#H destruct(H)
     308  | >position_of_from_aux
     309    lapply (refl … (position_of A test (tl@l2)))
     310    generalize in ⊢ (???%→?); * [2: #n'] #Heq >Heq
     311    normalize #EQ destruct(EQ)
     312    elim (IH … Heq) #H1 #H2
     313    >position_of_from_aux
     314    >position_of_from_aux
     315    >H1 >H2 normalize % %
     316  ]
     317]
     318qed.
     319
     320
Note: See TracChangeset for help on using the changeset viewer.