Changeset 3540


Ignore:
Timestamp:
Mar 17, 2015, 7:33:34 PM (6 years ago)
Author:
piccolo
Message:

closed some daemons

Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • LTS/Final.ma

    r3535 r3540  
    8383@(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map
    8484[2: <EQcostlabs in ⊢ (??%?); % | // ]
    85 qed. 
     85qed.
     86
     87lemma is_multiset_mem_neq_zero : ∀A : DeqSet.
     88∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O.
     89#A #l elim l [ #x *] #x #xs #IH #y *
     90[ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct
     91| #H normalize cases(?==?) normalize [ % #EQ destruct] @IH //
     92]
     93qed.
     94
     95lemma mem_neq_zero_is_multiset : ∀A : DeqSet.
     96∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l.
     97#A #l elim l [ #x * #H cases H % ]
     98#x #xs #IH #y normalize inversion(y==x) normalize nodelta
     99#H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption
     100qed.
    86101
    87102lemma is_permutation_mem : ∀A :DeqSet.
    88103∀l1,l2 : list A.∀x : A.mem … x l1 →
    89104is_permutation A l1 l2 → mem … x l2.
    90 cases daemon
     105#A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption
    91106qed.
    92107
    93108definition is_abelian ≝ λM : monoid.
    94109∀x,y : M.op … M x y = op … M y x.
     110
     111lemma mem_list : ∀A : Type[0].
     112∀l : list A.∀x : A.mem … x l →
     113∃l1,l2.l=l1 @ [x] @ l2.
     114#A #l elim l
     115[ #x *]
     116#x #xs #IH #y *
     117[ #EQ destruct %{[]} %{xs} %
     118| #H cases(IH … H) #l1 * #l2 #EQ destruct
     119  %{(x :: l1)} %{l2} %
     120]
     121qed.
     122
     123lemma is_permutation_case : ∀A : DeqSet.
     124∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l →
     125∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2.
     126#A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%]
     127#l1 * #l2 #EQ destruct %{l1} %{l2} % //
     128@(permute_equal_right … [x]) @permute_append_all
     129@(is_permutation_transitive … H)
     130/4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/
     131qed.
    95132
    96133lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) →
    97134∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 →
    98135(〚l1〛 a) = (〚l2〛 a).
    99 cases daemon
     136#M #Hab #l1 elim l1 -l1
     137[ * // #x #xs #a #H lapply(H x) normalize >(\b (refl …)) normalize #EQ destruct]
     138#x #xs #IH #l #a #H cases(is_permutation_case … H) #l1 * #l2 * #H1 #H2 destruct
     139change with ([?]@?) in match (?::?); >big_op_associative >act_op >(IH … H1)
     140<associative_append
     141>big_op_associative in ⊢ (???%); >big_op_associative in ⊢ (???%); >(Hab … l1)
     142>is_associative >act_op in ⊢ (???%); <big_op_associative in ⊢ (???%); %
     143qed.
     144
     145definition applica : ∀A,B : Type[0].∀ l : list A.(∀a : A.mem … a l → B) → ∀a : A.mem … a l → B ≝
     146λA,B,l,f,x,prf.f x prf.
     147
     148lemma proof_irrelevance_temp :  ∀A,B : Type[0].∀l : list A.
     149∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
     150applica … f x prf1 = applica … f x prf2.
     151//
     152qed.
     153
     154lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A.
     155∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
     156f x prf1 = f x prf2.
     157#A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp
     158qed.
     159
     160lemma dependent_map_extensional : ∀A,B : Type[0].∀l : list A.
     161∀f,g : (∀a.mem … a l → B).(∀a,prf1,prf2.f a prf1 = g a prf2) →
     162dependent_map … l f = dependent_map … l g.
     163#A #B #l elim l // #x #xs #IH #f #g #H whd in ⊢ (??%%);
     164@eq_f2 // @IH //
    100165qed.
    101166
    … …  
    105170(∀a : A.
    106171 ∀prf : mem … a l1.f a prf = g a ?) →
    107 is_permutation B (dependent_map … l1 f) (dependent_map … l2 g).
     172is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)).
    108173[2: @(is_permutation_mem … perm) //]
    109 cases daemon
     174#A #B #l1 elim l1 -l1
     175[ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ]
     176#x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct
     177>dependent_map_append >dependent_map_append @permute_append_l1 >associative_append
     178whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%);
     179whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?);
     180generalize in ⊢ (? → ???(??(??%)?));
     181#prf1 #prf2
     182>(proof_irrelevance_all … g x prf1 prf2)
     183@is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%);
     184whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1
     185@(is_permutation_transitive …(IH … (l3@l4) …) )
     186[2: assumption
     187|3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //]
     188| @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 //
     189]
     190>dependent_map_append @is_permutation_append
     191[ >dependent_map_extensional [ @is_permutation_eq | // |]
     192| >dependent_map_extensional [ @is_permutation_eq | // |]
     193]
    110194qed.
    111195

  • LTS/Lang_meas.ma

    r3535 r3540  
    3939    * #labels #code_cleaned #EQclean normalize nodelta
    4040    >EQcode in EQcall_post; inversion(code ? s1')
    41         [2,3,4,5,6,7: cases daemon (*ASSURDI*)
     41        [2,3,4,5,6,7:
     42          [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     43            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
     44          #_ whd in ⊢ (??%% → ?);
     45          [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     46          | cases(call_post_clean ?????); normalize nodelta
     47            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     48               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     49                 [| #z cases(?∧?) normalize nodelta
     50                 ]
     51               ]
     52            ]
     53          | cases(call_post_clean ?????) normalize nodelta
     54            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     55               [| #y cases(?∧?) normalize nodelta
     56               ]
     57            ]
     58          | cases(call_post_clean ?????) normalize nodelta
     59             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     60                [ cases (?==?) normalize nodelta ]
     61             ]]
     62          | cases(call_post_clean ?????) normalize nodelta
     63             [| #x cases(? ∧ ?) normalize nodelta ]
     64          ]
     65          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    4266        | #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct cases lab' normalize nodelta
    4367          [ #f #c whd in ⊢ (??%% → ?); #EQ destruct %{(refl …)} cases HHcont
    … …  
    5175  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
    5276  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode_s1 inversion(code ? s1')
    53   [1,2,4,5,6,7: cases daemon (* ASSURDI*)
     77  [1,2,4,5,6,7:
     78    [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     79            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
     80          #_ whd in ⊢ (??%% → ?);
     81          [ |
     82          | cases(call_post_clean ?????); normalize nodelta
     83            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     84               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     85                 [| #z cases(?∧?) normalize nodelta
     86                 ]
     87               ]
     88            ]
     89          | cases(call_post_clean ?????) normalize nodelta
     90            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     91               [| #y cases(?∧?) normalize nodelta
     92               ]
     93            ]
     94          | cases(call_post_clean ?????) normalize nodelta
     95             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     96                [ cases (?==?) normalize nodelta ]
     97             ]]
     98          | cases(call_post_clean ?????) normalize nodelta
     99             [| #x cases(? ∧ ?) normalize nodelta ]
     100          ]
     101          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    54102  | #i' * [|#lb] #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
    55103    [1,3: #EQ destruct] #x whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
    … …  
    57105    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ4 destruct
    58106 ]
    59 | cases daemon
     107| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #instrs #new_m #EQcode_s1 #EQeval #EQcont_s2 #EQ destruct #EQ destruct
     108  #Hio1 #Hio2 #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta
     109  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
     110  [1,2,3,5,6,7:
     111    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
     112       | #lin #io #lout #instr #_ ]
     113          #_ whd in ⊢ (??%% → ?);
     114          [ |
     115          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     116          | cases(call_post_clean ?????) normalize nodelta
     117            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     118               [| #y cases(?∧?) normalize nodelta
     119               ]
     120            ]
     121          | cases(call_post_clean ?????) normalize nodelta
     122             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     123                [ cases (?==?) normalize nodelta ]
     124             ]]
     125          | cases(call_post_clean ?????) normalize nodelta
     126             [| #x cases(? ∧ ?) normalize nodelta ]
     127          ]
     128          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     129  ]
     130  cases daemon (*TODO*)
    60131| cases daemon
    61132| cases daemon
Note: See TracChangeset for help on using the changeset viewer.