Changeset 2801 for src/common


Ignore:
Timestamp:
Mar 7, 2013, 1:29:31 PM (7 years ago)
Author:
piccolo
Message:

Partial commit not yet finished

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/ExtraIdentifiers.ma

    r2783 r2801  
    235235
    236236
    237 
    238 
     237lemma empty_set_minus : ∀tag,A,B.∀m : identifier_map tag B. empty_map tag A =
     238empty_map tag A ∖ m.
     239#tag #A #B * #m normalize @eq_f elim m [%] #opt_b #l #r #IHl #IHr normalize
     240cases opt_b normalize [2: #b] <IHl <IHr %
     241qed.
     242
     243
  • src/common/ExtraMonads.ma

    r2783 r2801  
    6969; mfr_bind1 : ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n →
    7070       ∀f,g.(∀x.m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g)
     71; mfr_bind_inversion1 :  ∀X,Y,Z,W,F,G,m,n. m_frel1 X Y F m n →
     72       ∀f,g.(∀x.m = return F x → n = return x → m_frel1 Z W G (f (F x)) (g x)) → m_frel1 ?? G (m_bind … m f) (m_bind … n g)
    7173; m_frel_ext1 : ∀X,Y,F,G.(∀x.F  x = G x) → ∀ u,v.m_frel1 X Y F u v → m_frel1 X Y G u v
    7274}.
     
    9092mk_MonadFunctRel1 ??
    9193(λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
    92 ???.
     94????.
    9395[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
    9496| #X #Y #Z #W #F #G * [#x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     
    9698  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
    9799  >n_spec <w_spec % //
     100| #X #Y #Z #W #F #G * [ #x | #e ] #n #H #f #g #H1 #z
     101  whd in ⊢ (??%% → ?); [2: #EQ destruct(EQ)] #H2 cases(H x (refl …))
     102  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption ] #w
     103  * #w_spec #EQz %{w} >n_spec <w_spec % //
    98104| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
    99105  % //
     
    118124  mk_MonadFunctRel1 ??
    119125  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
    120 ???.
     126????.
    121127[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
    122128| #X #Y #Z #W #F #G * [| #x] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     
    124130  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
    125131  >n_spec <w_spec % //
     132| #X #Y #Z #W #F #G * [ | #x ] #n #H #f #g #H1 #z
     133  whd in ⊢ (??%% → ?); [ #EQ destruct(EQ)] #H2 cases(H x (refl …))
     134  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w
     135  * #w_spec #EQz %{w} >n_spec <w_spec % //
    126136| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
    127137  % //
     
    146156  λO,I.mk_MonadFunctRel1 ??
    147157  (λX,Y,F,m,n.∀y.m = return y → ∃ x. n = return x ∧ y = F x)
    148 ???.
     158????.
    149159[ #X #Y #F #y #x normalize #EQ destruct(EQ) %{y} % //
    150160| #X #Y #Z #W #F #G * [#o #r | #x | #e] #n #H #f #g #H1 #z whd in ⊢ (??%% → ?); #EQ destruct
     
    152162  cases(H1 y z ?) [2: <x_spec whd in ⊢ (???%); assumption] #w * #w_spec #z_spec %{w}
    153163  >n_spec <w_spec % //
     164| #X #Y #Z #W #F #G * [ #o #r | #x | #e ] #n #H #f #g #H1 #z
     165  whd in ⊢ (??%% → ?); #EQ destruct(EQ) cases(H x (refl …))
     166  #y * #n_spec #x_spec cases(H1 y ? n_spec z ?) [2,3: <x_spec // assumption] #w
     167  * #w_spec #EQz %{w} >n_spec <w_spec % //
    154168| #X #Y #F #G #ext #u #v #K #x #u_spec cases(K x u_spec) #y * #v_spec #y_spec %{y}
    155169  % //
Note: See TracChangeset for help on using the changeset viewer.