Ignore:
Timestamp:
Oct 30, 2012, 12:32:31 PM (8 years ago)
Author:
campbell
Message:

Tidy away generic results about folds on positive/identifier maps.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2418 r2420  
    326326  ].
    327327
     328(* Fold over the entries in a map.  There are some lemmas to help reason about
     329   this near the bottom of the file (they require sets). *)
     330
    328331definition foldi:
    329332  ∀A, B: Type[0].
     
    11201123
    11211124
    1122 
     1125(* Returns the domain of a map as the canonical set (one made only from the
     1126   empty set and addition. *)
     1127definition domain_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝
     1128λtag,A,m. an_id_map tag unit (domain_of_pm A (match m with [ an_id_map m ⇒ m ])).
     1129lemma domain_of_map_present : ∀tag,A,m,id.
     1130  present tag A m id ↔ present tag unit (domain_of_map … m) id.
     1131#tag #A * #m * #p @domain_of_pm_present
     1132qed.
     1133
     1134(* Some lemmas for reasoning about folds. *)
     1135
     1136lemma foldi_ind : ∀A,B,tag,f,m,b. ∀P:B → identifier_set tag → Prop.
     1137  P b (empty_set …) →
     1138  (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →
     1139  P (foldi A B tag f m b) (domain_of_map … m).
     1140#A #B #tag #f * #m #b #P #P0 #STEP
     1141whd in match (foldi ??????); change with (an_id_map ?? (domain_of_pm A m)) in match (domain_of_map ???);
     1142@pm_fold_ind
     1143[ @P0
     1144| #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps))
     1145  [ normalize >FR /3/
     1146  | @L
     1147  | @pre
     1148  ]
     1149] qed.
     1150
     1151lemma foldi_ind' : ∀A,B,tag,f,m,b,b'. ∀P:B → identifier_set tag → Prop.
     1152  P b (empty_set …) →
     1153  (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →
     1154  foldi A B tag f m b = b' →
     1155  P b' (domain_of_map … m).
     1156#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11  destruct @foldi_ind /2/
     1157qed.
     1158
Note: See TracChangeset for help on using the changeset viewer.