Changeset 1976


Ignore:
Timestamp:
May 21, 2012, 7:04:21 PM (5 years ago)
Author:
tranquil
Message:
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
Location:
src
Files:
3 added
8 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1964 r1976  
    722722  @nat_of_bitvector_lt_bound
    723723qed.
     724
     725definition ASM_cost_map :
     726  ∀code_memory: BitVectorTrie Byte 16.
     727  ∀cost_labels: BitVectorTrie costlabel 16.
     728  ∀cost_map: identifier_map CostTag nat.
     729  (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k) →
     730  as_cost_map (ASM_abstract_status code_memory cost_labels) ≝
     731  λcode_memory,cost_labels,cost_map,codom_dom,l_sig.
     732  (lookup_present … cost_map (pi1 … l_sig) ?).
     733  cases l_sig #l * #pc @(codom_dom pc)
     734  qed.
     735 
     736include "utilities/permutations.ma".
     737
     738lemma tech_cost_sum_eq_as_cost :
     739  ∀code_memory: BitVectorTrie Byte 16.
     740  ∀cost_labels: BitVectorTrie costlabel 16.
     741  ∀cost_map: identifier_map CostTag nat.
     742  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     743  ∀trace.
     744  (Σ_{i < |trace|}(tech_cost_of_label cost_labels cost_map codom_dom trace i)) =
     745  (Σ_{l ∈ trace}(ASM_cost_map code_memory … codom_dom l)).
     746#cmem #clab #cmap #codom_dom #trace
     747@(list_elim_left … trace)
     748[ %
     749| #tl #hd #IH >append_length >commutative_plus
     750  >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
     751  whd in ⊢ (??%%); <IH
     752  <tech_cost_of_label_shift [2: %]
     753  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
     754  [ %
     755  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
     756  ]
     757]
     758qed.
  • src/common/IOMonad.ma

    r1949 r1976  
    165165
    166166definition IOPred ≝ λO,I,Perr.
    167   mk_MonadPred (IOMonad O I)
    168     (λA.pred_io O I A Perr)
     167  mk_InjMonadPred (IOMonad O I)
     168    (mk_MonadPred ? (λA.pred_io O I A Perr) ???)
    169169    (λA,P,a_sig.match a_sig with [ mk_Sig a prf ⇒ pred_io_inject O I A Perr P a prf ])
    170     ????.
    171 [//
    172 |#X #Y #relin #relout #m elim m
     170    ?. //
     171[ #X #P #Q #H #m elim m
     172  [#o #f #IH #H #i @IH @H
     173  | #v @H
     174  | #e //
     175  ]
     176| #X #Y #relin #relout #m elim m
    173177  [ #o #f #IH whd in ⊢ (%→?); #H
    174178    #f #G whd #i
     
    177181  | #e //
    178182  ]
    179 | #X #P #Q #H #m elim m
    180   [#o #f #IH #H #i @IH @H
    181   | #v @H
    182   | #e //
    183   ]
    184 |#X #P * #m elim m
     183| #X #P * #m elim m
    185184  [ #o #f #IH whd in ⊢ (%→?); #H
    186185    change with (Interact ?????) in ⊢ (???%);
     
    200199coercion err_to_io : ∀O,I,A.∀c:res A.IO O I A ≝ err_to_io on _c:res ? to IO ???.
    201200
     201(*
    202202lemma res_io_pred : ∀O,I,A,Perr,P.∀m : res A.pred_res … Perr P m → pred_io O I ? Perr P m.
    203203#O #I #A #Perr #P * /2/ qed.
     
    205205lemma io_res_pred : ∀O,I,A,Perr,P.∀m : res A.pred_io O I ? Perr P m → pred_res ? Perr P m.
    206206#O #I #A #Perr #P * /2/ qed.
    207 
     207*)
    208208definition err_to_io_sig : ∀O,I,T.∀P:T → Prop. res (Sig T P) → IO O I (Sig T P) ≝
    209209λO,I,T,P,v. match v with [ OK v' ⇒ Value O I (Sig T P) v' | Error m ⇒ Wrong O I (Sig T P) m ].
  • src/common/StructuredTraces.ma

    r1964 r1976  
    632632for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
    633633
    634 definition as_cost_of_trace_any_label :
    635   ∀S : abstract_status.
    636   ∀fl, start, end.
    637   as_cost_map S →
    638   trace_any_label S fl start end → ℕ ≝
    639   λS,fl,start,end,m,the_trace.
    640   Σ_{ l_sig ∈ flatten_trace_any_label … the_trace } (m l_sig).
    641 
    642 definition as_cost_of_trace_label_label :
    643   ∀S : abstract_status.
    644   ∀fl, start, end.
    645   as_cost_map S →
    646   trace_label_label S fl start end → ℕ ≝
    647   λS,fl,start,end,m,the_trace.
    648   Σ_{ l_sig ∈ flatten_trace_label_label … the_trace } (m l_sig).
    649 
    650 definition as_cost_of_trace_label_return :
    651   ∀S : abstract_status.
    652   ∀start, end.
    653   as_cost_map S →
    654   trace_label_return S start end → ℕ ≝
    655   λS,start,end,m,the_trace.
    656   Σ_{ l_sig ∈ flatten_trace_label_return … the_trace } (m l_sig).
    657 
    658634lemma lift_cost_map_same_cost :
    659635  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
     
    680656  ∀the_trace_out : trace_any_label S_out f_out start_out end_out.
    681657  tal_rel … the_trace_in the_trace_out →
    682   as_cost_of_trace_any_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    683     as_cost_of_trace_any_label … m_out the_trace_out.
     658  (Σ_{l ∈ flatten_trace_any_label … the_trace_in}
     659    (lift_cost_map_id … dec m_out l)) =
     660  (Σ_{l ∈ flatten_trace_any_label … the_trace_out} (m_out l)).
    684661#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
    685662#tal_in #tal_out #H_tal
     
    692669  ∀the_trace_out : trace_label_label S_out f_out start_out end_out.
    693670  tll_rel … the_trace_in the_trace_out →
    694   as_cost_of_trace_label_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    695     as_cost_of_trace_label_label … m_out the_trace_out.
     671  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
     672    (lift_cost_map_id … dec m_out l)) =
     673  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
    696674#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
    697675#tll_in #tll_out #H_tll
     
    704682  ∀the_trace_out : trace_label_return S_out start_out end_out.
    705683  tlr_rel … the_trace_in the_trace_out →
    706   as_cost_of_trace_label_return … (lift_cost_map_id S_in S_out dec m_out) the_trace_in =
    707     as_cost_of_trace_label_return … m_out the_trace_out.
     684  (Σ_{l ∈ flatten_trace_label_return … the_trace_in}
     685    (lift_cost_map_id … dec m_out l)) =
     686  (Σ_{l ∈ flatten_trace_label_return … the_trace_out} (m_out l)).
    708687#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
    709688#tlr_in #tlr_out #H_tlr
  • src/joint/Joint_paolo.ma

    r1949 r1976  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
     9include "basics/deqsets.ma".
     10include "basics/finset.ma". (* for DeqNat *)
    911
    1012(* Here is the structure of parameter records (downward edges are coercions,
     
    147149 { stmt_pars :> stmt_params
    148150 ; codeT: list ident → Type[0]
    149  ; code_point : Type[0]
     151 ; code_point : DeqSet
    150152 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
    151153 ; point_of_label : ∀globals.codeT globals → label → option code_point
     
    290292      (mk_stmt_params lp unit (λ_.None ?))
    291293    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    292     (* code_point ≝ *)
     294    (* code_point ≝ *)DeqNat
    293295    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
    294296    (* point_of_label ≝ *)(λglobals,c,lbl.
     
    325327  { g_u_pars :> unserialized_params }.
    326328
    327 (* move *)
    328 definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
    329   λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
    330   [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
    331     [ an_identifier i' ⇒
    332       match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
    333       [ Some y ⇒ λ_.y
    334       | None ⇒ Ⓧ
    335       ]
    336     ]
    337   ].
    338  
    339 lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
    340   (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
    341 #tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
    342 [ * ]
    343 #s * #H @H %
    344 qed.
    345 
    346329(* One common instantiation of params via Graphs of joint_statements
    347330   (all languages but LIN) *)
     
    351334      (mk_stmt_params gp label (Some ?))
    352335    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    353     (* code_point ≝ *)label
     336    (* code_point ≝ *)(Deq_identifier LabelTag)
    354337    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
    355338    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
  • src/joint/semantics_paolo.ma

    r1949 r1976  
    9090  | Proceed  : step_flow p globals labels. (* go to implicit successor *)
    9191
     92definition step_flow_cons : ∀p,globals,l,lbls.
     93  step_flow p globals lbls → step_flow p globals (l :: lbls) ≝
     94  λp,globals,l1,l2,flow.match flow with
     95  [ Redirect l ⇒ Redirect … «l, ?»
     96  | Init id f args dest ⇒ Init … id f args dest
     97  | Proceed ⇒ Proceed ???
     98  ]. cases l /2 by or_intror/ qed.
     99coercion step_flow_c : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1::l2) ≝
     100  step_flow_cons on _flow : step_flow ??? to step_flow ?? (cons ???).
     101
     102definition step_flow_append_l : ∀p,globals,l1,l2.
     103  step_flow p globals l1 → step_flow p globals (l1 @ l2) ≝
     104  λp,globals,l1,l2,flow.match flow with
     105  [ Redirect l ⇒ Redirect … «l, ?»
     106  | Init id f args dest ⇒ Init … id f args dest
     107  | Proceed ⇒ Proceed ???
     108  ]. cases l /2 by Exists_append_l/ qed.
     109coercion step_flow_l : ∀p,globals,l1,l2.∀flow : step_flow p globals l1.step_flow p globals (l1@l2) ≝
     110  step_flow_append_l on _flow : step_flow ??? to step_flow ?? (append ???).
     111
     112definition step_flow_append_r : ∀p,globals,l1,l2.
     113  step_flow p globals l2 → step_flow p globals (l1 @ l2) ≝
     114  λp,globals,l1,l2,flow.match flow with
     115  [ Redirect l ⇒ Redirect … «l, ?»
     116  | Init id f args dest ⇒ Init … id f args dest
     117  | Proceed ⇒ Proceed ???
     118  ]. cases l /2 by Exists_append_r/ qed.
     119coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝
     120  step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???).
     121
    92122inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝
    93123  | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels
    94124  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels
    95125  | FEnd  : fin_step_flow p globals labels. (* end flow *)
     126
     127definition fin_step_flow_cons : ∀p,globals,l,lbls.
     128  fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝
     129  λp,globals,l1,l2,flow.match flow with
     130  [ FRedirect l ⇒ FRedirect … «l, ?»
     131  | FTailInit id f args ⇒ FTailInit … id f args
     132  | FEnd ⇒ FEnd ???
     133  ]. cases l /2 by or_intror/ qed.
     134coercion fin_step_flow_c : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1::l2) ≝
     135  fin_step_flow_cons on _flow : fin_step_flow ??? to fin_step_flow ?? (cons ???).
     136
     137definition fin_step_flow_append_l : ∀p,globals,l1,l2.
     138  fin_step_flow p globals l1 → fin_step_flow p globals (l1@l2) ≝
     139  λp,globals,l1,l2,flow.match flow with
     140  [ FRedirect l ⇒ FRedirect … «l, ?»
     141  | FTailInit id f args ⇒ FTailInit … id f args
     142  | FEnd ⇒ FEnd ???
     143  ]. cases l /2 by Exists_append_l/ qed.
     144coercion fin_step_flow_l : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l1.fin_step_flow p globals (l1@l2) ≝
     145  fin_step_flow_append_l on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
     146
     147definition fin_step_flow_append_r : ∀p,globals,l1,l2.
     148  fin_step_flow p globals l2 → fin_step_flow p globals (l1@l2) ≝
     149  λp,globals,l1,l2,flow.match flow with
     150  [ FRedirect l ⇒ FRedirect … «l, ?»
     151  | FTailInit id f args ⇒ FTailInit … id f args
     152  | FEnd ⇒ FEnd ???
     153  ]. cases l /2 by Exists_append_r/ qed.
     154coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝
     155  fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
    96156
    97157record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
  • src/utilities/monad.ma

    r1949 r1976  
    2323 
    2424record Monad : Type[1] ≝ {
    25   monad : Type[0] → Type[0] ;
     25  monad :1> Type[0] → Type[0] ;
    2626  m_return : ∀X. X → monad X ;
    2727  m_bind : ∀X,Y. monad X → (X → monad Y) → monad Y
     
    124124record MonadProps : Type[1] ≝
    125125  { max_def :> Monad
    126   ; m_return_bind : ∀X,Y.∀x : X.∀f : X → monad max_def Y. ! y ← return x ; f y = f x
    127   ; m_bind_return : ∀X.∀m : monad max_def X.! x ← m ; return x = m
    128   ; m_bind_bind : ∀X,Y,Z. ∀m : monad max_def X.∀f : X → monad max_def Y.
    129       ∀g : Y → monad max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y
    130   ; m_bind_ext_eq : ∀X,Y.∀m : monad max_def X.∀f,g : X → monad max_def Y.
     126  ; m_return_bind : ∀X,Y.∀x : X.∀f : X → max_def Y. ! y ← return x ; f y = f x
     127  ; m_bind_return : ∀X.∀m : max_def X.! x ← m ; return x = m
     128  ; m_bind_bind : ∀X,Y,Z. ∀m : max_def X.∀f : X → max_def Y.
     129      ∀g : Y → max_def Z.! y ← (! x ← m ; f x) ; g y = ! x ← m; ! y ← f x ; g y
     130  ; m_bind_ext_eq : ∀X,Y.∀m : max_def X.∀f,g : X → max_def Y.
    131131      (∀x.f x = g x) → ! x ← m ; f x = ! x ← m ; g x
    132132  }.
     
    134134record SetoidMonadProps : Type[1] ≝
    135135  { smax_def :> Monad
    136   ; sm_eq : ∀X.relation (monad smax_def X)
     136  ; sm_eq : ∀X.relation (smax_def X)
    137137  ; sm_eq_refl : ∀X.reflexive ? (sm_eq X)
    138138  ; sm_eq_trans : ∀X.transitive ? (sm_eq X)
     
    140140  ; sm_return_proper : ∀X,x.sm_eq X (return x) (return x)
    141141  ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y (x »= f) (y »= g)
    142   ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → monad smax_def Y.
     142  ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → smax_def Y.
    143143      sm_eq Y (! y ← return x ; f y) (f x)
    144   ; sm_bind_return : ∀X.∀m : monad smax_def X.sm_eq X (! x ← m ; return x) m
    145   ; sm_bind_bind : ∀X,Y,Z. ∀m : monad smax_def X.∀f : X → monad smax_def Y.
    146       ∀g : Y → monad smax_def Z.sm_eq Z (! y ← (! x ← m ; f x) ; g y) (! x ← m; ! y ← f x ; g y)
     144  ; sm_bind_return : ∀X.∀m : smax_def X.sm_eq X (! x ← m ; return x) m
     145  ; sm_bind_bind : ∀X,Y,Z. ∀m : smax_def X.∀f : X → smax_def Y.
     146      ∀g : Y → smax_def Z.sm_eq Z (! y ← (! x ← m ; f x) ; g y) (! x ← m; ! y ← f x ; g y)
    147147  }.
    148148
    149149definition setoid_of_monad : ∀M : SetoidMonadProps.∀X : Type[0].
    150150  Setoid ≝
    151   λM,X.mk_Setoid (monad M X) (sm_eq M X) (sm_eq_refl M X) (sm_eq_trans M X) (sm_eq_sym M X).
     151  λM,X.mk_Setoid (M X) (sm_eq M X) (sm_eq_refl M X) (sm_eq_trans M X) (sm_eq_sym M X).
    152152
    153153include "hints_declaration.ma".
     
    160160include "basics/lists/list.ma".
    161161
    162 definition m_map ≝ λM,X,Y.λf : X → Y.λm : monad M X.
     162definition m_map ≝ λM : Monad.λX,Y.λf : X → Y.λm : M X.
    163163  ! x ← m ; return f x.
    164164
    165 definition m_map2 ≝ λM,X,Y,Z.λf : X → Y → Z.λm : monad M X.λn : monad M Y.
     165definition m_map2 ≝ λM : Monad.λX,Y,Z.λf : X → Y → Z.λm : M X.λn : M Y.
    166166  ! x ← m ; ! y ← n ; return f x y.
    167167 
    168 definition m_bind2 ≝ λM,X,Y,Z.λm : monad M (X × Y).λf : X → Y → monad M Z.
     168definition m_bind2 ≝ λM : Monad.λX,Y,Z.λm : M (X × Y).λf : X → Y → M Z.
    169169  ! p ← m ; f (\fst p) (\snd p).
    170170
     
    172172
    173173definition m_bind3 :
    174   ∀M,X,Y,Z,W.monad M (X×Y×Z) → (X → Y → Z → monad M W) → monad M W ≝
     174  ∀M : Monad.∀X,Y,Z,W.M (X×Y×Z) → (X → Y → Z → M W) → M W ≝
    175175  λM,X,Y,Z,W,m,f.
    176176  ! p ← m ; f (\fst (\fst p)) (\snd (\fst p)) (\snd p).
     
    178178interpretation "monad bind3" 'm_bind3 m f = (m_bind3 ? ? ? ? ? m f).
    179179
    180 definition m_join : ∀M,X.monad M (monad M X) → monad M X ≝
     180definition m_join : ∀M : Monad.∀X.M (M X) → M X ≝
    181181  λM,X,m.! x ← m ; x.
    182182
    183183definition m_sigbind2 :
    184   ∀M,A,B,C.∀P:A×B → Prop. monad M (Σx:A×B.P x) →
    185       (∀a,b. P 〈a,b〉 → monad M C) → monad M C ≝
     184  ∀M : Monad.∀A,B,C.∀P:A×B → Prop. M (Σx:A×B.P x) →
     185      (∀a,b. P 〈a,b〉 → M C) → M C ≝
    186186λM,A,B,C,P,e,f.
    187187    ! e_sig ← e ;
     
    197197
    198198definition m_list_map :
    199   ∀M,X,Y.(X → monad M Y) → list X → monad M (list Y) ≝
     199  ∀M : Monad.∀X,Y.(X → M Y) → list X → M (list Y) ≝
    200200  λM,X,Y,f,l.foldr … (λel,macc.! r ← f el; !acc ← macc; return (r :: acc)) (return [ ]) l.
    201201
    202202definition m_list_map_sigma :
    203   ∀M,X,Y,P.(X → monad M (Σy : Y.P y)) → list X → monad M (Σl : list Y.All ? P l) ≝
     203  ∀M : Monad.∀X,Y,P.(X → M (Σy : Y.P y)) → list X → M (Σl : list Y.All ? P l) ≝
    204204  λM,X,Y,P,f,l.foldr … (λel,macc.
    205205    ! «r, r_prf» ← f el ;
     
    209209
    210210definition m_bin_op :
    211   ∀M,X,Y,Z.(X → Y → Z) → monad M X → monad M Y → monad M Z ≝
     211  ∀M : Monad.∀X,Y,Z.(X → Y → Z) → M X → M Y → M Z ≝
    212212  λM,X,Y,Z,op,m,n. ! x ← m ; ! y ← n ; return op x y.
    213213
    214 unification hint 0 ≔ M, X, Y, Z, m, f ⊢
    215 m_bind M (X×Y) Z m (λp.f (\fst p) (\snd p)) ≡ m_bind2 M X Y Z m f.
    216 
    217 unification hint 0 ≔ M, X, Y, Z, W, m, f ⊢
    218 m_bind M (X×Y×Z) W m (λp.f (\fst (\fst p)) (\snd (\fst p)) (\snd p)) ≡
    219 m_bind3 M X Y Z W m f.
     214unification hint 0 ≔ M, X, Y, Z, m, f ;
     215  P ≟ Prod X Y, F ≟ λp.f (\fst p) (\snd p) ⊢
     216m_bind M P Z m F ≡ m_bind2 M X Y Z m f.
     217
     218unification hint 0 ≔ M, X, Y, Z, W, m, f ;
     219  P' ≟ Prod X Y, P ≟ Prod P' Z, F ≟ λp.f (\fst (\fst p)) (\snd (\fst p)) (\snd p) ⊢
     220m_bind M P W m F ≡ m_bind3 M X Y Z W m f.
    220221
    221222definition MakeMonadProps : ?→?→?→?→?→?→?→MonadProps ≝ λmonad,m_return,m_bind.
     
    229230 
    230231record MonadPred (M : Monad) : Type[1] ≝
    231   { m_pred :> ∀X.pred_transformer X (monad M X)
    232   ; mp_inject : ∀X,P.(Σm.m_pred X P m) → monad M (Σx.P x)
     232  { m_pred :2> ∀X.(X → Prop) → (M X → Prop)
    233233  ; mp_return : ∀X,P,x.P x → m_pred X P (return x)
    234234  ; mp_bind : ∀X,Y,Pin,Pout,m.m_pred X Pin m →
     
    236236                  m_pred ? Pout (m_bind … m f)
    237237  ; m_pred_mp : ∀X.modus_ponens ?? (m_pred X)
     238  }.
     239
     240record InjMonadPred (M : Monad) : Type[1] ≝
     241  { im_pred :> MonadPred M
     242  ; mp_inject : ∀X.∀P : X → Prop.(Σm.im_pred P m) → M (Σx.P x)
    238243  ; mp_inject_eq : ∀X,P,m.pi1 ?? m = ! x ← mp_inject X P m ; return pi1 … x
    239244  }.
    240245
    241 coercion coerc_mp_inject : ∀M.∀MP:MonadPred M.
    242   ∀X,P.∀m : Σm.m_pred ? MP X P m.monad M (Σx.P x) ≝
    243   mp_inject on _m : Sig (monad ??) (λm.m_pred ???? m) to monad ? (Sig ? (λx.? x)).
    244 
    245 lemma mp_inject_bind : ∀M : MonadProps.∀MP,X,P,Y.∀m.∀f : X → monad M Y.
     246coercion coerc_mp_inject : ∀M.∀MP:InjMonadPred M.
     247  ∀X.∀P : X → Prop.∀m : Σm.MP P m.M (Σx.P x) ≝
     248  mp_inject on _m : Sig (monad ??) (λm.im_pred ??? m) to monad ? (Sig ? (λx.? x)).
     249
     250lemma mp_inject_bind : ∀M : MonadProps.∀MP,X,P,Y.∀m.∀f : X → M Y.
    246251  ! x ← mp_inject M MP X P m ; f (pi1 … x) = ! x ← pi1 … m ; f x.
    247252#M#MP#X#P#Y#m#f >mp_inject_eq >m_bind_bind @m_bind_ext_eq #x >m_return_bind % qed.
    248253
    249254record MonadRel (M1 : Monad) (M2 : Monad) : Type[1] ≝
    250   { m_rel :> ∀X,Y.rel_transformer X Y (monad M1 X) (monad M2 Y)
     255  { m_rel :3> ∀X,Y.(X → Y → Prop) → (M1 X → M2 Y → Prop)
    251256  ; mr_return : ∀X,Y,rel,x,y.rel x y → m_rel X Y rel (return x) (return y)
    252257  ; mr_bind : ∀X,Y,Z,W,relin,relout,m,n.m_rel X Y relin m n → ∀f,g.(∀x,y.relin x y → m_rel Z W relout (f x) (g y)) →
     
    254259  ; m_rel_mp : ∀X,Y.rel_modus_ponens ???? (m_rel X Y)
    255260  }.
    256 
    257 
  • src/utilities/option.ma

    r1949 r1976  
    6262interpretation "option try and catch" 'trycatch m f = (opt_try_catch ? m f).
    6363
    64 definition OptPred ≝ λPdef : Prop.mk_MonadPred Option
    65   (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
     64definition OptPred ≝ λPdef : Prop.mk_InjMonadPred Option
     65  (mk_MonadPred ?
     66    (λX,P,x.Try ! y ← x ; return P y catch ⇒ Pdef)
     67    ???)
    6668  (λX,P,m_sig.match m_sig with [ mk_Sig m prf ⇒ match m return λx.Try ! y ← x ; return P y catch ⇒ Pdef → option (Σy.?) with [ Some x ⇒ λprf.Some ? x | None ⇒ λ_.None ? ] prf ])
    67   ????.
    68 [ @prf
     69  ?.
     70[4: @prf
    6971|*:
    70 #X[2:#Y]#P1[1,3:#P2[2:#H]]
     72#X[2:#Y]#P1[1,2:#P2[2:#H]]
    7173[1,2,4: * [5: *]] normalize /2/
    7274qed.
  • src/utilities/state.ma

    r1882 r1976  
    11include "utilities/monad.ma".
    22
    3 definition State
     3definition state_monad
    44  λS : Type[0].MakeSetoidMonadProps
    55  (* the monad *)
     
    2121qed.
    2222
    23 definition state_monad ≝ λS.monad (State S).
    24 
    2523definition state_get : ∀S.state_monad S S ≝ λS,s.〈s,s〉.
    2624definition state_set : ∀S.S → state_monad S unit ≝ λS,s.λ_.〈s,it〉.
    2725definition state_run : ∀S,X. S → (state_monad S X) → X ≝ λS,X,s,c.'pi2 (c s).
    2826
    29 include "hints_declaration.ma".
    30 unification hint 0 ≔ S,X;
    31 N ≟ State S, M ≟ smax_def N
    32 (*---------------*) ⊢
    33 state_monad S X ≡ monad M X
    34 .
    35 
    36 definition StatePred ≝ λS.λPs : S → Prop.mk_MonadPred (State S)
     27definition state_pred ≝ λS.λPs : S → Prop.mk_MonadPred (state_monad S)
    3728  (λX,P,m.∀s.Ps s → let m' ≝ m s in Ps (\fst m') ∧ P (\snd m')) ???.
    38 [ normalize /2/
     29[ normalize /2 by conj/
    3930| normalize #X#Y#P1#P2 #m #H #f #G #s #Ps lapply (H … Ps)
    4031  elim (m s) #s' #x normalize * /2/
     
    4334qed.
    4435
    45 definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (State S) (State T)
     36definition StateRel ≝ λS,T.λPs : S → T → Prop.mk_MonadRel (state_monad S) (state_monad T)
    4637  (λX,Y,P,m,n.∀s,t.Ps s t → let m' ≝ m s in let n' ≝ n t in
    4738    Ps (\fst m') (\fst n') ∧ P (\snd m') (\snd n')) ???.
Note: See TracChangeset for help on using the changeset viewer.