Changeset 3540
- Timestamp:
- Mar 17, 2015, 7:33:34 PM (6 years ago)
- Location:
- LTS
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Final.ma
r3535 r3540 83 83 @(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map 84 84 [2: <EQcostlabs in ⊢ (??%?); % | // ] 85 qed. 85 qed. 86 87 lemma 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 ] 93 qed. 94 95 lemma 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 100 qed. 86 101 87 102 lemma is_permutation_mem : ∀A :DeqSet. 88 103 ∀l1,l2 : list A.∀x : A.mem … x l1 → 89 104 is_permutation A l1 l2 → mem … x l2. 90 cases daemon105 #A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption 91 106 qed. 92 107 93 108 definition is_abelian ≝ λM : monoid. 94 109 ∀x,y : M.op … M x y = op … M y x. 110 111 lemma 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 ] 121 qed. 122 123 lemma 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/ 131 qed. 95 132 96 133 lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) → 97 134 ∀l1,l2 : list (abs_instr M).∀a.is_permutation … l1 l2 → 98 135 (〚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 139 change 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 ⊢ (???%); % 143 qed. 144 145 definition 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 148 lemma proof_irrelevance_temp : ∀A,B : Type[0].∀l : list A. 149 ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2. 150 applica … f x prf1 = applica … f x prf2. 151 // 152 qed. 153 154 lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A. 155 ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2. 156 f x prf1 = f x prf2. 157 #A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp 158 qed. 159 160 lemma 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) → 162 dependent_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 // 100 165 qed. 101 166 … … 105 170 (∀a : A. 106 171 ∀prf : mem … a l1.f a prf = g a ?) → 107 is_permutation B (dependent_map … l1 f) (dependent_map … l2 g).172 is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)). 108 173 [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 178 whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%); 179 whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?); 180 generalize in ⊢ (? → ???(??(??%)?)); 181 #prf1 #prf2 182 >(proof_irrelevance_all … g x prf1 prf2) 183 @is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%); 184 whd 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 ] 110 194 qed. 111 195 -
LTS/Lang_meas.ma
r3535 r3540 39 39 * #labels #code_cleaned #EQclean normalize nodelta 40 40 >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 42 66 | #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct cases lab' normalize nodelta 43 67 [ #f #c whd in ⊢ (??%% → ?); #EQ destruct %{(refl …)} cases HHcont … … 51 75 whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] ** 52 76 #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 54 102 | #i' * [|#lb] #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta 55 103 [1,3: #EQ destruct] #x whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ] … … 57 105 [2: #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ4 destruct 58 106 ] 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*) 60 131 | cases daemon 61 132 | cases daemon
Note: See TracChangeset
for help on using the changeset viewer.