Changeset 3540 for LTS/Final.ma


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

closed some daemons

File:
1 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
Note: See TracChangeset for help on using the changeset viewer.