Changeset 3552 for LTS/Final.ma


Ignore:
Timestamp:
Apr 9, 2015, 11:04:21 PM (5 years ago)
Author:
piccolo
Message:

closed all daemons

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Final.ma

    r3549 r3552  
    8686qed.
    8787
    88 lemma is_multiset_mem_neq_zero : ∀A : DeqSet.
    89 ∀l : list A.∀x.mem … x l → mult … (list_to_multiset … l) x ≠ O.
    90 #A #l elim l [ #x *] #x #xs #IH #y *
    91 [ #EQ destruct % normalize >(\b (refl …)) normalize nodelta normalize #EQ destruct
    92 | #H normalize cases(?==?) normalize [ % #EQ destruct] @IH //
    93 ]
    94 qed.
    95 
    96 lemma mem_neq_zero_is_multiset : ∀A : DeqSet.
    97 ∀l: list A.∀x.mult … (list_to_multiset … l) x ≠ O → mem … x l.
    98 #A #l elim l [ #x * #H cases H % ]
    99 #x #xs #IH #y normalize inversion(y==x) normalize nodelta
    100 #H normalize [#_ % >(\P H) % ] #H1 %2 @IH assumption
    101 qed.
    102 
    103 lemma is_permutation_mem : ∀A :DeqSet.
    104 ∀l1,l2 : list A.∀x : A.mem … x l1 →
    105 is_permutation A l1 l2 → mem … x l2.
    106 #A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption
    107 qed.
    108 
    109 lemma mem_list : ∀A : Type[0].
    110 ∀l : list A.∀x : A.mem … x l →
    111 ∃l1,l2.l=l1 @ [x] @ l2.
    112 #A #l elim l
    113 [ #x *]
    114 #x #xs #IH #y *
    115 [ #EQ destruct %{[]} %{xs} %
    116 | #H cases(IH … H) #l1 * #l2 #EQ destruct
    117   %{(x :: l1)} %{l2} %
    118 ]
    119 qed.
    120 
    121 lemma is_permutation_case : ∀A : DeqSet.
    122 ∀x : A.∀xs : list A.∀l : list A.is_permutation … (x::xs) l →
    123 ∃l1,l2 : list A.is_permutation A xs (l1@l2) ∧ l = l1 @ [x] @ l2.
    124 #A #x #xs #l #H cases(mem_list … x (is_permutation_mem … H)) [2: %%]
    125 #l1 * #l2 #EQ destruct %{l1} %{l2} % //
    126 @(permute_equal_right … [x]) @permute_append_all
    127 @(is_permutation_transitive … H)
    128 /4 by is_permutation_append_left_cancellable, permute_append_l1, permute_append_all/
    129 qed.
    13088
    13189lemma action_on_permutation : ∀M : abstract_transition_sys.is_abelian (abs_instr M) →
     
    13997>big_op_associative in ⊢ (???%); >big_op_associative in ⊢ (???%); >(Hab … l1)
    14098>is_associative >act_op in ⊢ (???%); <big_op_associative in ⊢ (???%); %
    141 qed.
    142 
    143 definition applica : ∀A,B : Type[0].∀ l : list A.(∀a : A.mem … a l → B) → ∀a : A.mem … a l → B ≝
    144 λA,B,l,f,x,prf.f x prf.
    145 
    146 lemma proof_irrelevance_temp :  ∀A,B : Type[0].∀l : list A.
    147 ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
    148 applica … f x prf1 = applica … f x prf2.
    149 //
    150 qed.
    151 
    152 lemma proof_irrelevance_all : ∀A,B : Type[0].∀l : list A.
    153 ∀f : (∀a : A.mem … a l → B).∀x.∀prf1,prf2.
    154 f x prf1 = f x prf2.
    155 #A #B #l #f #x #prf1 #prf2 @proof_irrelevance_temp
    156 qed.
    157 
    158 lemma dependent_map_extensional : ∀A,B : Type[0].∀l : list A.
    159 ∀f,g : (∀a.mem … a l → B).(∀a,prf1,prf2.f a prf1 = g a prf2) →
    160 dependent_map … l f = dependent_map … l g.
    161 #A #B #l elim l // #x #xs #IH #f #g #H whd in ⊢ (??%%);
    162 @eq_f2 // @IH //
    163 qed.
    164 
    165 lemma is_permutation_dependent_map : ∀A,B : DeqSet.∀l1,l2 : list A.
    166 ∀f : (∀a : A.mem … a l1 → B).∀g : (∀a : A.mem … a l2 → B).
    167 ∀perm : is_permutation A l1 l2.
    168 (∀a : A.
    169  ∀prf : mem … a l1.f a prf = g a ?) →
    170 is_permutation B (dependent_map … l1 (λa,prf.f a prf)) (dependent_map … l2 (λa,prf.g a prf)).
    171 [2: @(is_permutation_mem … perm) //]
    172 #A #B #l1 elim l1 -l1
    173 [ * // #x #xs #f #g #H @⊥ lapply(H … x) normalize >(\b (refl …)) normalize #EQ destruct ]
    174 #x #xs #IH #l2 #f #g #H #H1 cases(is_permutation_case … H) #l3 * #l4 * #H2 #EQ destruct
    175 >dependent_map_append >dependent_map_append @permute_append_l1 >associative_append
    176 whd in match (dependent_map ????); whd in match (dependent_map ????) in ⊢ (???%);
    177 whd in match(append ???); >H1 generalize in ⊢ (??(??(??%)?)?);
    178 generalize in ⊢ (? → ???(??(??%)?));
    179 #prf1 #prf2
    180 >(proof_irrelevance_all … g x prf1 prf2)
    181 @is_permutation_cons whd in match (dependent_map ?? [ ] ?) in ⊢ (???%);
    182 whd in match (append ? [ ] ?) in ⊢ (???%); @permute_append_l1
    183 @(is_permutation_transitive …(IH … (l3@l4) …) )
    184 [2: assumption
    185 |3: #a #prf @(g a) cases(mem_append ???? prf) [ /3 by mem_append_l1/ | #H6 @mem_append_l2 @mem_append_l2 //]
    186 | @hide_prf #a #prf generalize in ⊢ (??(??%)?); #prf' >H1 //
    187 ]
    188 >dependent_map_append @is_permutation_append
    189 [ >dependent_map_extensional [ @is_permutation_eq | // |]
    190 | >dependent_map_extensional [ @is_permutation_eq | // |]
    191 ]
    19299qed.
    193100
Note: See TracChangeset for help on using the changeset viewer.