Ignore:
Timestamp:
May 30, 2011, 1:44:45 PM (10 years ago)
Author:
sacerdot
Message:
  1. if_then_else is now a notation for match with (to allow Russell to work better)
  2. notation for destructuring let fixed to work in pretty printing mode too
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r855 r856  
    11include "ASM/Assembly.ma".
    22include "ASM/Interpret.ma".
    3 
    4 (*
    5 axiom append_cons_commute:
    6   ∀A: Type[0].
    7   ∀l, r: list A.
    8   ∀h: A.
    9     l @ h::r = l @ [h] @ r.
    10 *)
    11 (*
    12 axiom append_associative:
    13   ∀A: Type[0].
    14   ∀l, c, r: list A.
    15     (l @ c) @ r = l
    16 *)
    173
    184let rec foldl_strong_internal
     
    4228    foldl_strong_internal A P l H [ ] l acc (refl …).
    4329
    44 (* RUSSEL **)
    45 
    4630definition bit_elim: ∀P: bool → bool. bool ≝
    4731  λP.
     
    7559qed.
    7660
     61(*
    7762lemma subvector_hd_tl:
    7863  ∀A: Type[0].
     
    185170  | @ (instruction_elim INSTR)
    186171  ].
     172*)
    187173 
    188     (* > append_cons_commute
    189     @
     174(* RUSSEL **)
    190175
    191176include "basics/jmeq.ma".
     
    218203 #A #P #p cases p #w #q @q
    219204qed.
     205
     206lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
     207 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
     208qed.
     209
     210coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
    220211
    221212(* END RUSSELL **)
     
    270261   | Some r ⇒ λ_.r] (policy_ok p).
    271262 cases abs //
     263qed.
     264
     265lemma length_append:
     266 ∀A.∀l1,l2:list A.
     267  |l1 @ l2| = |l1| + |l2|.
     268 #A #l1 elim l1
     269  [ //
     270  | #hd #tl #IH #l2 normalize <IH //]
    272271qed.
    273272
     
    308307   let 〈pc, costs〉 ≝ pc_costs in
    309308    〈labels, costs〉.
    310  [
    311  |
     309 [ whd cases construct in p3 #PC #CODE #JMEQ whd #pc #Hpc
     310   generalize in match (sig2 … t) whd in ⊢ (% → ?)
     311   >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1
     312   >length_append in Hpc <plus_n_Sm in ⊢ (% → ?) <plus_n_O in ⊢ (% → ?) #Hpc
     313   whd in ⊢ (??(????%?)?) -labels1;
     314   cases label
     315    [ whd in ⊢ (??(????%?)?)
     316      cases (le_to_or_lt_eq … Hpc)
     317      [ #H1 >(IH1 pc) [2: @(le_S_S_to_le … H1)]
     318        (* lemmas needed here *)
     319      | #H1 generalize in match (injective_S … H1) -H1 #H1
     320        (* ??? *)
     321      ]
     322    | -label #label whd in ⊢ (??(????%?)?)
     323     
     324    ]
     325 | (* dummy case *)
    312326 | whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
    313327qed.
     
    343357 #A #P
    344358qed.*)
    345 
    346 lemma length_append:
    347  ∀A.∀l1,l2:list A.
    348   |l1 @ l2| = |l1| + |l2|.
    349  #A #l1 elim l1
    350   [ //
    351   | #hd #tl #IH #l2 normalize <IH //]
    352 qed.
    353359
    354360lemma rev_preserves_length:
Note: See TracChangeset for help on using the changeset viewer.