Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (8 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2122 r2124  
    170170qed.
    171171
    172 (*CSC: move elsewhere*)
    173 lemma pair_replace:
    174  ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
    175   P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
    176  #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
    177 qed.
    178 
    179172lemma get_arg_8_set_program_counter:
    180173  ∀M: Type[0].
     
    327320qed.
    328321
    329 (*CSC: move elsewhere*)
    330 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
    331  #P #A #a #abs destruct
    332 qed.
    333 
    334322(*
    335323lemma pi1_let_commute:
     
    360348include alias "basics/logic.ma".
    361349include alias "ASM/BitVectorTrie.ma".
    362 
    363 (*CSC: move elsewhere*)
    364 lemma jmpair_as_replace:
    365  ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c.
    366   ∀EQ:c ≃ 〈a,b〉.
    367   P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')).
    368   [2:
    369     >EQc @EQ
    370   |1:
    371     #A #B #T #P #a #b
    372     #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ
    373     letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ]
    374     change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ;
    375     @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta
    376     -EQ cases c in f; normalize //
    377   ]
    378 qed.
    379 
    380 (*CSC: move elsewhere*)
    381 lemma if_then_else_replace:
    382   ∀T: Type[0].
    383   ∀P: T → Prop.
    384   ∀t1, t2: T.
    385   ∀c, c', c'': bool.
    386     c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).
    387   #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
    388   assumption
    389 qed.
    390350
    391351lemma fetch_many_singleton:
     
    398358  #fetch_many_assm whd in fetch_many_assm;
    399359  cases (eq_bv_eq … fetch_many_assm) assumption
    400 qed.
    401 
    402 (*CSC: move elsewhere*)
    403 lemma refl_to_jmrefl:
    404   ∀a: Type[0].
    405   ∀l, r: a.
    406     l = r → l ≃ r.
    407   #a #l #r #refl destruct %
    408360qed.
    409361
Note: See TracChangeset for help on using the changeset viewer.