Changeset 1882 for src/common


Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 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

Location:
src/common
Files:
1 added
7 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1873 r1882  
    353353definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
    354354                         list (A × B) → res (list (A × C)) ≝
    355 λA,B,C,f. m_mmap ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
     355λA,B,C,f. m_list_map ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
    356356
    357357lemma map_partial_preserves_first:
  • src/common/Errors.ma

    r1647 r1882  
    1 (* *********************************************************************)
    2 (*                                                                     *)
    3 (*              The Compcert verified compiler                         *)
    4 (*                                                                     *)
    5 (*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
    6 (*                                                                     *)
    7 (*  Copyright Institut National de Recherche en Informatique et en     *)
    8 (*  Automatique.  All rights reserved.  This file is distributed       *)
    9 (*  under the terms of the GNU General Public License as published by  *)
    10 (*  the Free Software Foundation, either version 2 of the License, or  *)
    11 (*  (at your option) any later version.  This file is also distributed *)
    12 (*  under the terms of the INRIA Non-Commercial License Agreement.     *)
    13 (*                                                                     *)
    14 (* *********************************************************************)
    15 
    161include "basics/types.ma".
    172include "basics/logic.ma".
     
    205include "basics/russell.ma".
    216include "utilities/monad.ma".
     7include "utilities/option.ma".
     8
     9(* first, generic exception monad *)
     10
     11inductive except (E : Type[0]) (X : Type[0]) : Type[0] ≝
     12  | raise : E → except E X
     13  | success : X → except E X.
     14
     15definition Except ≝ λE.MakeMonadProps
     16  (except E)
     17  (success E)
     18  (λX,Y,m,f.match m with [raise e ⇒ raise … e | success x ⇒ f x])
     19  ????.
     20//
     21[ #X * #x %
     22| #X#Y#Z * #x#f#g %
     23| #X#Y normalize * #x #f #g #H // normalize @H
     24]
     25qed.
     26
     27unification hint 0 ≔ E,X;
     28O ≟ Except E, N ≟ max_def O
     29(*--------------------------------------*) ⊢
     30except E X ≡ monad N X.
     31
     32definition try_catch : ∀E,X.except E X → (E → X) → X ≝
     33  λE,X,m,f.match m with
     34  [ success x ⇒ x
     35  | raise e ⇒ f e
     36  ].
     37
     38interpretation "exception try catch" 'trycatch e f = (try_catch ?? e f).
     39
     40definition except_elim : ∀E,X.∀m : except E X.∀P : ? → Prop.
     41  (∀x.m = success ?? x → P (success ?? x)) →
     42  (∀e.m = raise ?? e → P (raise ?? e)) →
     43  P m.
     44#E #X * /2/
     45qed.
     46
     47definition except_success ≝ λE,X.λm : except E X.
     48  match m with [success _ ⇒ True | _ ⇒ False].
     49
     50definition except_safe ≝
     51  λE,X.λm : except E X.
     52    match m return λx.except_success ?? x → X with
     53    [ success y ⇒ λ_.y
     54    | _ ⇒ λprf.match prf in False with []
     55    ].
     56
     57definition Except_P ≝ λE.λP_e : E → Prop.mk_MonadPred (Except E)
     58  (λX,P,m. Try ! x ← m ; return P x catch e ⇒ P_e e) ???.
     59[ //
     60| #X#Y #P1 #P2 * #x normalize /2/
     61| #X #P #Q #H * #y normalize /2/
     62]
     63qed.
     64
     65definition except_P ≝ λE,P_e.m_pred … (Except_P E P_e).
     66
     67definition except_All : ∀E,X.(X → Prop) → except E X → Prop ≝
     68  λE : Type[0].except_P E (λe.True).
     69
     70definition except_Exists : ∀E,X.(X → Prop) → except E X → Prop ≝
     71  λE : Type[0].except_P E (λe.False).
     72
     73definition except_rel ≝ λE,F.λrel_e : E → F → Prop.mk_MonadRel (Except E) (Except F)
     74  (λX,Y,rel,m,n.
     75    match m with
     76    [ success x ⇒ match n with [success y ⇒ rel x y | _ ⇒ False]
     77    | raise e ⇒ match n with [raise f ⇒ rel_e e f | _ ⇒ False]
     78    ]) ???.
     79[ //
     80|*: #X#Y[#Z#W] #rel1 #rel2 [2: #H] * #x * #y normalize /2/ *
     81]
     82qed.
    2283
    2384(* * Error reporting and the error monad. *)
     
    42103  The return value is either [OK res] to indicate success,
    43104  or [Error msg] to indicate failure. *)
     105
     106(* Paolo: not using except for backward compatbility
     107  (would break Error ? msg) *)
    44108
    45109inductive res (A: Type[0]) : Type[0] ≝
     
    56120  (* bind *)
    57121  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
    58   ???.
     122  ????.
    59123//
    60124[(* bind_ret *)
     
    62126|(* bind_bind *)
    63127 #X#Y#Z*normalize //
     128| normalize #X #Y * normalize /2/
    64129]
    65130qed.
     
    67132include "hints_declaration.ma".
    68133unification hint 0 ≔ X;
    69 N ≟ max_def Res, M ≟ m_def N
     134N ≟ max_def Res
    70135(*---------------*) ⊢
    71 res X ≡ monad M X
     136res X ≡ monad N X
    72137.
    73138
     
    267332definition bind2 ≝ m_bind2 Res.
    268333definition bind3 ≝ m_bind3 Res.
    269 definition mmap ≝ m_mmap Res.
    270 definition mmap_sigma ≝ m_mmap_sigma Res.
     334definition mmap ≝ m_list_map Res.
     335definition mmap_sigma ≝ m_list_map_sigma Res.
  • src/common/Graphs.ma

    r1635 r1882  
    5959  l ≠ to_insert → lookup ? ? g l = lookup ? ? (add ? ? g to_insert s) l.
    6060
    61 axiom graph_num_nodes:
    62   ∀A: Type[0].
    63   ∀g: graph A.
    64     nat.
     61definition graph_num_nodes:
     62  ∀A: Type[0].graph A → ℕ ≝ λA,g.|g|.
     63 
     64lemma graph_num_ind : ∀A : Type[0].∀P : graph A → Prop.
     65  (∀g.(∀g'.|g'|<|g| → P g') → P g) → ∀g.P g.
     66#A#P#H#g
     67lapply (refl ? (|g|))
     68generalize in ⊢(???%→?);
     69#n lapply g -g
     70@(nat_elim1 … n)
     71#m #G #g #EQs @H >EQs #g' #DEQ @(G ? DEQ g' (refl …))
     72qed.
  • src/common/IOMonad.ma

    r1647 r1882  
    3131  (* bind *)
    3232  (bindIO O I)
    33   ???. / by /
     33  ????. / by /
    3434[(* bind_ret *)
    3535 #X#m elim m normalize // #o#f#Hi @interact_proper //
     
    3838 (* Interact *)
    3939  #o#f #Hi @interact_proper //
     40|#X #Y #m #f #g #H elim m normalize
     41  [ #o #x @interact_proper ] //
    4042]
    4143qed.
     
    4648
    4749unification hint 0 ≔ O, I, T;
    48   N ≟ IOMonad O I, M ≟ max_def N, M' ≟ m_def M
     50  N ≟ IOMonad O I, M ≟ max_def N
    4951(*******************************************) ⊢
    50   IO O I T ≡ monad M' T
     52  IO O I T ≡ monad M T
    5153.
    5254
  • src/common/Identifiers.ma

    r1635 r1882  
    33include "utilities/binary/positive.ma".
    44include "utilities/lists.ma".
     5include "utilities/extralib.ma".
    56include "common/Errors.ma".
    67
     
    370371(* Sets *)
    371372
    372 inductive identifier_set (tag:String) : Type[0] ≝
    373   an_id_set : positive_map unit → identifier_set tag.
    374 
    375 definition empty_set : ∀tag:String. identifier_set tag ≝
    376 λtag. an_id_set tag (pm_leaf unit).
    377 
    378 let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
    379   an_id_set tag (insert unit (match i with [ an_identifier i' ⇒ i' ])
    380                           it (match s with [ an_id_set s' ⇒ s' ])).
     373definition identifier_set ≝ λtag.identifier_map tag unit.
     374
     375definition empty_set : ∀tag.identifier_set tag ≝ λtag.empty_map ….
     376
     377
     378definition add_set : ∀tag.identifier_set tag → identifier tag → identifier_set tag ≝
     379  λtag,s,i.add … s i it.
    381380
    382381definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
    383382λtag,i. add_set tag (empty_set tag) i.
    384383
    385 let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
    386   match lookup_opt ? (match i with [ an_identifier i' ⇒ i' ])
    387                      (match s with [ an_id_set s' ⇒ s' ]) with
     384(* mem set is generalised to all maps *)
     385let rec mem_set (tag:String) A (s:identifier_map tag A) (i:identifier tag) on s : bool ≝
     386  match lookup … s i with
    388387  [ None ⇒ false
    389388  | Some _ ⇒ true
    390389  ].
    391 
    392 let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
    393   an_id_set tag (merge unit (match s with [ an_id_set s0 ⇒ s0 ])
    394                             (match s' with [ an_id_set s1 ⇒ s1 ])).
    395 
    396 interpretation "identifier set union" 'union a b = (union_set ? a b).
     390 
     391let rec union_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝
     392  an_id_map tag unit (merge … (λo,o'.match o with [Some _ ⇒ Some ? it | None ⇒ !_ o'; return it])
     393    (match s with [ an_id_map s0 ⇒ s0 ])
     394    (match s' with [ an_id_map s1 ⇒ s1 ])).
     395
     396
     397(* set minus is generalised to maps *)
     398let rec minus_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_map tag A ≝
     399  an_id_map tag A (merge A B A (λo,o'.match o' with [None ⇒ o | Some _ ⇒ None ?])
     400    (match s with [ an_id_map s0 ⇒ s0 ])
     401    (match s' with [ an_id_map s1 ⇒ s1 ])).
     402
     403notation "a ∖ b" left associative with precedence 50 for @{'setminus $a $b}.
     404
     405interpretation "identifier set union" 'union a b = (union_set ??? a b).
    397406notation "∅" non associative with precedence 90 for @{ 'empty }.
    398407interpretation "empty identifier set" 'empty = (empty_set ?).
    399408interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
    400 interpretation "identifier set membership" 'mem a b = (mem_set ? b a).
     409interpretation "identifier set membership" 'mem a b = (mem_set ?? b a).
     410interpretation "identifier map difference" 'setminus a b = (minus_set ??? a b).
     411
     412definition IdentifierSet : String → Setoid ≝ λtag.
     413  mk_Setoid (identifier_set tag) (λs,s'.∀i.i ∈ s = (i ∈ s')) ???.
     414  // qed.
     415
     416unification hint 0 ≔ tag;
     417S ≟ IdentifierSet tag
     418(*-----------------------------*)⊢
     419identifier_set tag ≡ std_supp S.
     420unification hint 0 ≔ tag;
     421S ≟ IdentifierSet tag
     422(*-----------------------------*)⊢
     423identifier_map tag unit ≡ std_supp S.
     424
     425lemma mem_set_add : ∀tag,A.∀i,j : identifier tag.∀s,x.
     426  i ∈ add ? A s j x = (eq_identifier ? i j ∨ i ∈ s).
     427#tag #A *#i *#j *#s #x normalize
     428@(eqb_elim i j)
     429[#EQ destruct
     430  >(lookup_opt_insert_hit A x j)
     431|#NEQ >(lookup_opt_insert_miss … s NEQ)
     432] elim (lookup_opt  A j s) normalize // qed.
     433
     434lemma mem_set_add_id : ∀tag,A,i,s,x.bool_to_Prop (i ∈ add tag A s i x).
     435#tag #A #i #s #x >mem_set_add
     436@eq_identifier_elim [#_ %| #ABS elim (absurd … (refl ? i) ABS)] qed.
     437
     438lemma in_map_domain : ∀tag,A.∀m : identifier_map tag A.∀i.
     439  if i ∈ m then (∃s.lookup … m i = Some ? s) else (lookup … m i = None ?).
     440#tag #A * #m * #i normalize
     441elim (lookup_opt A i m) normalize
     442[ % | #x %{x} % ]
     443qed.
    401444
    402445lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
    403 #tag * //
     446#tag * normalize #m >map_opt_id_eq_ext // * %
    404447qed.
    405448
    406449lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
    407 #tag * * // qed.
    408 
     450#tag * * [//] *[2: *] #l#r normalize
     451>map_opt_id_eq_ext [1,3: >map_opt_id_eq_ext [2,4: *] |*: *] //
     452qed.
     453
     454lemma minus_empty_l : ∀tag,A.∀s:identifier_map tag A. ∅ ∖ s ≅ ∅.
     455#tag #A * * [//] *[2:#x]#l#r * * normalize [1,4://]
     456#p >lookup_opt_map elim (lookup_opt ???) normalize //
     457qed.
     458
     459lemma minus_empty_r : ∀tag,A.∀s:identifier_map tag A. s ∖ ∅ = s.
     460#tag #A * * [//] *[2:#x]#l#r normalize
     461>map_opt_id >map_opt_id //
     462qed.
     463
     464lemma mem_set_union : ∀tag.∀i : identifier tag.∀s,s' : identifier_set tag.
     465  i ∈ (s ∪ s') = (i ∈ s ∨ i ∈ s').
     466#tag * #i * #s * #s' normalize
     467>lookup_opt_merge [2: @refl]
     468elim (lookup_opt ???)
     469elim (lookup_opt ???)
     470normalize // qed.
     471
     472lemma mem_set_minus : ∀tag,A,B.∀i : identifier tag.∀s : identifier_map tag A.
     473  ∀s' : identifier_map tag B.
     474  i ∈ (s ∖ s') = (i ∈ s ∧ ¬ i ∈ s').
     475#tag #A #B * #i * #s * #s' normalize
     476>lookup_opt_merge [2: @refl]
     477elim (lookup_opt ???)
     478elim (lookup_opt ???)
     479normalize // qed.
     480
     481lemma set_eq_ext_node : ∀tag.∀o,o',l,l',r,r'.
     482  an_id_map tag ? (pm_node ? o l r) ≅ an_id_map … (pm_node ? o' l' r') →
     483    o = o' ∧ an_id_map tag ? l ≅ an_id_map … l' ∧ an_id_map tag ? r ≅ an_id_map … r'.
     484#tag#o#o'#l#l'#r#r'#H
     485%[
     486%[ lapply (H (an_identifier ? one))
     487   elim o [2: *] elim o' [2,4: *] normalize // #EQ destruct
     488 | *#p lapply (H (an_identifier ? (p0 p))) normalize //
     489]| *#p lapply (H (an_identifier ? (p1 p))) normalize //
     490]
     491qed.
     492
     493lemma set_eq_ext_leaf : ∀tag,A.∀o,l,r.
     494  (∀i.i∈an_id_map tag A (pm_node ? o l r) = false) →
     495    o = None ? ∧ (∀i.i∈an_id_map tag ? l = false) ∧ (∀i.i∈an_id_map tag ? r = false).
     496#tag#A#o#l#r#H
     497%[
     498%[ lapply (H (an_identifier ? one))
     499   elim o [2: #a] normalize // #EQ destruct
     500 | *#p lapply (H (an_identifier ? (p0 p))) normalize //
     501]| *#p lapply (H (an_identifier ? (p1 p))) normalize //
     502]
     503qed.
     504
     505
     506definition id_map_size : ∀tag : String.∀A. identifier_map tag A → ℕ ≝
     507  λtag,A,s.match s with [an_id_map p ⇒ |p|].
     508
     509interpretation "identifier map domain size" 'norm s = (id_map_size ?? s).
     510
     511lemma set_eq_ext_empty_to_card : ∀tag,A.∀s : identifier_map tag A. (∀i.i∈s = false) → |s| = 0.
     512#tag#A * #s elim s [//]
     513#o#l#r normalize in ⊢((?→%)→(?→%)→?); #Hil #Hir #H
     514elim (set_eq_ext_leaf … H) * #EQ destruct #Hl #Hr normalize
     515>(Hil Hl) >(Hir Hr) // qed.
     516
     517lemma set_eq_ext_to_card : ∀tag.∀s,s' : identifier_set tag. s ≅ s' → |s| = |s'|.
     518#tag *#s elim s
     519[** [//] #o#l#r #H
     520  >(set_eq_ext_empty_to_card … (std_symm … H)) //
     521| #o#l#r normalize in ⊢((?→?→??%?)→(?→?→??%?)→?);
     522  #Hil #Hir **
     523  [#H @(set_eq_ext_empty_to_card … H)]
     524  #o'#l'#r' #H elim (set_eq_ext_node … H) * #EQ destruct(EQ) #Hl #Hr
     525  normalize >(Hil ? Hl) >(Hir ? Hr) //
     526] qed.
     527
     528lemma add_size: ∀tag,A,s,i,x.
     529  |add tag A s i x| = (if i ∈ s then 0 else 1) + |s|.
     530#tag #A *#s *#i #x
     531lapply (insert_size ? i x s)
     532lapply (refl ? (lookup_opt ? i s))
     533generalize in ⊢ (???%→?); * [2: #x']
     534normalize #EQ >EQ normalize //
     535qed.
     536
     537lemma mem_set_O_lt_card : ∀tag,A.∀i.∀s : identifier_map tag A. i ∈ s → |s| > 0.
     538#tag #A * #i * #s normalize #H
     539@(lookup_opt_O_lt_size … i)
     540% #EQ >EQ in H; normalize *
     541qed.
     542
     543(* NB: no control on values if applied to maps *)
     544definition set_subset ≝ λtag,A,B.λs : identifier_map tag A.
     545  λs' : identifier_map tag B. ∀i.i ∈ s → (bool_to_Prop (i ∈ s')).
     546
     547interpretation "identifier set subset" 'subseteq s s' = (set_subset ??? s s').
     548
     549lemma add_subset :
     550  ∀tag,A,B.∀i : identifier tag.∀x.∀s : identifier_map ? A.∀s' : identifier_map ? B.
     551    i ∈ s' → s ⊆ s' → add … s i x ⊆ s'.
     552#tag#A#B#i#x#s#s' #H #G #j
     553>mem_set_add
     554@eq_identifier_elim #H' [* >H' @H | #js @(G ? js)]
     555qed.
     556
     557definition set_forall : ∀tag,A.(identifier tag → Prop) →
     558  identifier_map tag A → Prop ≝ λtag,A,P,m.∀i. i ∈ m → P i.
     559 
     560lemma set_forall_add : ∀tag,P,m,i.set_forall tag ? P m → P i →
     561  set_forall tag ? P (add_set ? m i).
     562#tag#P#m#i#Pm#Pi#j
     563>mem_set_add
     564@eq_identifier_elim
     565[#EQ destruct(EQ) #_ @Pi
     566|#_ @Pm
     567]
     568qed.
     569
     570include "utilities/proper.ma".
     571
     572lemma minus_subset : ∀tag,A,B.minus_set tag A B ⊨ set_subset … ++> set_subset … -+> set_subset ….
     573#tag#A#B#s#s' #H #s'' #s''' #G #i
     574>mem_set_minus >mem_set_minus
     575#H' elim (andb_Prop_true … H') -H' #is #nis''
     576>(H … is)
     577elim (true_or_false_Prop (i∈s'''))
     578[ #is''' >(G … is''') in nis''; *
     579| #nis''' >nis''' %
     580]
     581qed.
     582
     583lemma subset_node : ∀tag,A,B.∀o,o',l,l',r,r'.
     584  an_id_map tag A (pm_node ? o l r) ⊆ an_id_map tag B (pm_node ? o' l' r') →
     585    opt_All ? (λ_.o' ≠ None ?) o ∧ an_id_map tag ? l ⊆ an_id_map tag  ? l' ∧
     586      an_id_map tag ? r ⊆ an_id_map tag ? r'.
     587#tag#A#B#o#o'#l#l'#r#r'#H
     588%[%
     589  [ lapply (H (an_identifier ? (one))) elim o [2: #a] elim o' [2:#b]
     590    normalize // [#_ % #ABS destruct(ABS) | #G lapply (G I) *]
     591  | *#p lapply (H (an_identifier ? (p0 p)))
     592  ]
     593 | *#p lapply (H (an_identifier ? (p1 p)))
     594] #H @H
     595qed.
     596
     597lemma subset_leaf : ∀tag,A.∀o,l,r.
     598  an_id_map tag A (pm_node ? o l r) ⊆ ∅ →
     599    o = None ? ∧ (∀i.i∈an_id_map tag ? l = false) ∧ (∀i.i∈an_id_map tag ? r = false).
     600#tag#A#o#l#r#H
     601%[
     602%[ lapply (H (an_identifier ? one))
     603   elim o [2: #a] normalize // #EQ lapply(EQ I) *
     604 | *#p lapply (H (an_identifier ? (p0 p)))
     605 ]
     606|  *#p lapply (H (an_identifier ? (p1 p)))
     607] normalize elim (lookup_opt ? p ?) normalize
     608// #a #H lapply (H I) *
     609qed.
     610
     611lemma subset_card : ∀tag,A,B.∀s : identifier_map tag A.∀s' : identifier_map tag B.
     612  s ⊆ s' → |s| ≤ |s'|.
     613#tag #A #B *#s elim s
     614[ //
     615| #o#l#r #Hil #Hir **
     616  [ #H elim (subset_leaf … H) * #EQ >EQ #Hl #Hr
     617    lapply (set_eq_ext_empty_to_card … Hl)
     618    lapply (set_eq_ext_empty_to_card … Hr)
     619    normalize //
     620  | #o' #l' #r' #H elim (subset_node … H) *
     621    elim o [2: #a] elim o' [2,4: #a']
     622    [3: #G normalize in G; elim(absurd ? (refl ??) G)
     623    |*: #_ #Hl #Hr lapply (Hil ? Hl) lapply (Hir ? Hr)
     624      normalize #H1 #H2
     625      [@le_S_S | @(transitive_le … (|l'|+|r'|)) [2: / by /]]
     626      @le_plus assumption
     627    ]
     628  ]
     629]
     630qed.
     631
     632lemma mem_set_empty : ∀tag.∀i: identifier tag. i∈∅ = false.
     633#tag * #i normalize %
     634qed.
     635
     636lemma mem_set_singl_to_eq : ∀tag.∀i,j : identifier tag.i∈{(j)} → i = j.
     637#tag
     638#i #j >mem_set_add >mem_set_empty
     639#H elim (orb_true_l … H) -H
     640[@eq_identifier_elim [//] #_] #EQ destruct
     641qed.
     642
     643lemma subset_add_set : ∀tag,i,s.s ⊆ add_set tag s i.
     644#tag#i#s#j #H >mem_set_add >H
     645>commutative_orb %
     646qed.
     647
     648lemma add_set_monotonic : ∀tag,i,s,s'.s ⊆ s' → add_set tag s i ⊆ add_set tag s' i.
     649#tag#i#s#s' #H #j >mem_set_add >mem_set_add
     650@orb_elim elim (eq_identifier ???)
     651whd lapply (H j) /2 by /
     652qed.
     653
     654lemma transitive_subset : ∀tag,A.transitive ? (set_subset tag A A).
     655#tag#A#s#s'#s''#H#G#i #is
     656@(G … (H … is))
     657qed.
     658
     659definition set_from_list : ∀tag.list (identifier tag) → identifier_map tag unit ≝
     660  λtag.foldl … (add_set ?) ∅.
     661
     662coercion id_set_from_list : ∀tag.∀l : list (identifier tag).identifier_map tag unit ≝
     663  set_from_list on _l : list (identifier ?) to identifier_map ? unit.
     664
     665lemma mem_map_domain : ∀tag,A.∀m : identifier_map tag A.∀i.
     666i∈m → lookup … m i ≠ None ?.
     667#tag#A * #m #i
     668whd in match (i∈?);
     669elim (lookup ????) normalize [2: #x]
     670* % #EQ destruct(EQ)
     671qed.
     672
     673
     674
     675lemma mem_list_as_set : ∀tag.∀l : list (identifier tag).
     676  ∀i.i ∈ l → In ? l i.
     677#tag #l @(list_elim_left … l)
     678[ #i *
     679| #t #h #Hi  #i
     680  whd in ⊢ (?(???%?)→?);
     681  >foldl_append
     682  whd in ⊢ (?(???%?)→?);
     683  >mem_set_add
     684  @eq_identifier_elim
     685  [ #EQi destruct(EQi)
     686    #_ @Exists_append_r % %
     687  | #_ #H @Exists_append_l @Hi assumption
     688  ]
     689]
     690qed.
     691
     692lemma list_as_set_mem : ∀tag.∀l : list (identifier tag).
     693  ∀i.In ? l i → i ∈ l.
     694#tag #l @(list_elim_left … l)
     695[ #i *
     696| #t #h #Hi #i #H
     697  whd in ⊢ (?(???%?));
     698  >foldl_append
     699  whd in ⊢ (?(???%?));
     700  elim (Exists_append … H) -H
     701  [ #H >mem_set_add
     702    @eq_identifier_elim [//] #_ normalize
     703    @Hi @H
     704  | * [2: *] #EQi destruct(EQi) >mem_set_add_id %
     705  ]
     706]
     707qed.
     708
     709lemma list_as_set_All : ∀tag,P.∀ l : list (identifier tag).
     710  (∀i.i ∈ l → P i) → All ? P l.
     711#tag #P #l @(list_elim_left … l)
     712[ #_ %
     713| #x #l' #Hi
     714  whd in match (l'@[x] : identifier_map tag unit);
     715  >foldl_append
     716  #H @All_append
     717  [ @Hi #i #G @H
     718    whd in ⊢ (?(???%?));
     719    >mem_set_add @orb_Prop_r @G
     720  | % [2: %]
     721    @H
     722    whd in ⊢ (?(???%?));
     723    @mem_set_add_id
     724  ]
     725]
     726qed.
     727
     728lemma All_list_as_set : ∀tag,P.∀ l : list (identifier tag).
     729  All ? P l → ∀i.i ∈ l → P i.
     730#tag #P #l @(list_elim_left … l)
     731[ * #i *
     732| #x #l' #Hi #H
     733  lapply (All_append_l … H)
     734  lapply (All_append_r … H)
     735  * #Px * #Pl' #i
     736  whd in match (l'@[x] : identifier_map ??);
     737  >foldl_append
     738  >mem_set_add
     739  @eq_identifier_elim
     740  [ #EQx >EQx #_ @Px
     741  | #_ whd in match (?∨?); @Hi @Pl'
     742  ]
     743]
     744qed. 
     745
     746
     747
  • src/common/Pointers.ma

    r1545 r1882  
    118118 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
    119119qed.
     120
     121lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
     122  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
     123#P * #r0 #b0 #H0 * #o0 * #r1 #b1 #H1 * #o1
     124#Ptrue #Pfalse
     125whd in match (eq_pointer ??);
     126@eq_region_elim #reg_eq
     127[ @eq_block_elim #block_eq
     128  [ change with (eqZb ??) in match (eq_offset ??);
     129    @eqZb_elim #offset_eq
     130    [ destruct @Ptrue %
     131    ]
     132  ]
     133]
     134@Pfalse % #EQ destruct /2 by absurd/
     135qed.
  • src/common/PositiveMap.ma

    r1601 r1882  
    191191] qed.
    192192
    193 let rec merge (A: Type[0]) (b: positive_map A) (c:positive_map A) on b: positive_map A ≝
    194 match b with
    195 [ pm_leaf ⇒ c
     193include "utilities/option.ma".
     194
     195let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
     196match b with
     197[ pm_leaf ⇒ pm_leaf ?
     198| pm_node a l r ⇒ pm_node ? (a »= f)
     199    (map_opt ?? f l)
     200    (map_opt ?? f r)
     201].
     202
     203definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
     204
     205lemma lookup_opt_map : ∀A,B,f,b,p.
     206  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
     207#A#B#f#b elim b [//]
     208#a #l #r #Hil #Hir * [//]
     209#p
     210whd in ⊢ (??(???%)(????%?));
     211whd in ⊢ (??%?); //
     212qed.
     213
     214lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
     215#A #m #f #Hf elim m [//]
     216* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
     217qed.
     218
     219lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
     220#A #m @map_opt_id_eq_ext //
     221qed.
     222
     223let rec merge A B C (choice : option A → option B → option C)
     224  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
     225match a with
     226[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
     227| pm_node o l r ⇒
     228  match b with
     229  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
     230  | pm_node o' l' r' ⇒
     231    pm_node ? (choice o o')
     232      (merge … choice l l')
     233      (merge … choice r r')
     234  ]
     235].
     236
     237lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
     238  choice (None ?) (None ?) = None ? →
     239  lookup_opt … p (merge A B C choice a b) =
     240    choice (lookup_opt … p a) (lookup_opt … p b).
     241 #A#B#C#choice#a elim a
     242[ normalize #b
     243| #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
     244]
     245#p#choice_good >lookup_opt_map
     246elim (lookup_opt ???)
     247normalize //
     248qed.
     249
     250let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
     251match b with
     252[ pm_leaf ⇒ 0
    196253| pm_node a l r ⇒
    197   match c with
    198   [ pm_leaf ⇒ pm_node A a l r
    199   | pm_node a' l' r' ⇒ pm_node A a' (merge A l l') (merge A r r')
    200   ]
    201 ].
    202 
     254  (match a with
     255   [ Some _ ⇒ 1
     256   | None ⇒ 0
     257   ]) + domain_size A l + domain_size A r
     258].
     259
     260(* just to load notation for 'norm (list.ma's notation overrides core's 'card)*)
     261include "basics/lists/list.ma".
     262interpretation "positive map size" 'norm p = (domain_size ? p).
     263
     264lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
     265#A#B#f#b elim b [//]
     266*[2:#x]#l#r#Hil#Hir normalize
     267[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
     268@le_plus assumption
     269qed.
     270
     271lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
     272#A#B#f#b elim b [//]
     273*[2:#x]#l#r#Hil#Hir normalize
     274>Hil >Hir @refl
     275qed.
     276
     277lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
     278#A#m elim m
     279[#p normalize #F elim (absurd ? (refl ??) F)
     280|* [2: #x]  #l #r #Hil #Hir * normalize
     281  [1,2,3: //
     282  |4:  #F elim (absurd ? (refl ??) F)]
     283  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
     284qed.
     285
     286lemma insert_size : ∀A,p,a,m. |insert A p a m| =
     287  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
     288#A#p elim p
     289[ #a * [2: * [2: #x] #l #r] normalize //
     290|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
     291] qed.
Note: See TracChangeset for help on using the changeset viewer.