Changeset 2143 for src/ASM/ASM.ma


Ignore:
Timestamp:
Jul 2, 2012, 11:37:34 AM (8 years ago)
Author:
mulligan
Message:

Changes to the subaddressing mode elim functions moved into their correct place in ASM.ma. ticks_of0 completed, with all daemons removed. Another commutation lemma added in AssemblyProofSplit?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2139 r2143  
    403403qed.
    404404
     405(* XXX: move back into ASM.ma *)
     406lemma subvector_with_to_subvector_with_tl:
     407  ∀n: nat.
     408  ∀m: nat.
     409  ∀v.
     410  ∀fixed_v.
     411  ∀proof: (subvector_with addressing_mode_tag n (S m) eq_a v fixed_v).
     412  ∀n': nat.
     413  ∀hd: addressing_mode_tag.
     414  ∀tl: Vector addressing_mode_tag n'.
     415  ∀m_refl: S n'=n.
     416  ∀v_refl: v≃hd:::tl.
     417   subvector_with addressing_mode_tag n' (S m) eq_a tl fixed_v.
     418  #n #m #v #fixed_v #proof #n' #hd #tl #m_refl #v_refl
     419  generalize in match proof; destruct
     420  whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
     421  cases (mem … eq_a ? fixed_v hd) normalize nodelta
     422  [1:
     423    whd in match (subvector_with … eq_a tl fixed_v);
     424    #assm assumption
     425  |2:
     426    normalize in ⊢ (% → ?);
     427    #absurd cases absurd
     428  ]
     429qed.
    405430
    406431let rec subaddressing_mode_elim_type
     
    437462  ] (refl … n) (refl_jmeq … v).
    438463  [20:
    439     generalize in match proof; destruct
    440     whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
    441     cases (mem … eq_a ? fixed_v hd) normalize nodelta
    442     [1:
    443       whd in match (subvector_with … eq_a tl fixed_v);
    444       #assm assumption
    445     |2:
    446       normalize in ⊢ (% → ?);
    447       #absurd cases absurd
    448     ]
     464    @(subvector_with_to_subvector_with_tl … proof … m_refl v_refl)
    449465  ]
    450466  @(is_in_subvector_is_in_supervector … proof)
     
    460476  (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) →
    461477   subaddressing_mode_elim_type n v addr Q m w H.
    462  #n #v #addr #Q #m #w elim w
    463  [ /2/
    464  | #n' #hd #tl #IH cases hd #H
    465    #INV whd #PO @IH #xaddr cases xaddr *
    466    try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
    467    @ALREADYSEEN ]
     478  #n #v #addr #Q #m #w elim w
     479  [1:
     480    /2/
     481  |2:
     482    #n' #hd #tl #IH cases hd #H
     483    #INV whd #PO @IH #xaddr cases xaddr *
     484    try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
     485    @ALREADYSEEN
     486  ]
    468487qed.
    469488
     
    474493  ∀Q: v → Prop.
    475494   subaddressing_mode_elim_type n v addr Q (S n) v ?.
    476 [ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
    477 | @subvector_with_refl @eq_a_reflexive
    478 ]
     495  [1:
     496    #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
     497  |2:
     498    @subvector_with_refl @eq_a_reflexive
     499  ]
    479500qed.
    480501 
Note: See TracChangeset for help on using the changeset viewer.