Ignore:
Timestamp:
Jun 27, 2012, 5:05:33 PM (8 years ago)
Author:
sacerdot
Message:

Final shuffling around

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2124 r2128  
    33include "ASM/StatusProofs.ma".
    44include alias "arithmetics/nat.ma".
    5 
    6 lemma is_in_monotonic_wrt_append:
    7   ∀m, n: nat.
    8   ∀p: Vector addressing_mode_tag m.
    9   ∀q: Vector addressing_mode_tag n.
    10   ∀to_search: addressing_mode.
    11     bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
    12   #m #n #p #q #to_search #assm
    13   elim q try assumption
    14   #n' #hd #tl #inductive_hypothesis
    15   normalize
    16   cases (is_a ??) try @I
    17   >inductive_hypothesis @I
    18 qed.
    19 
    20 corollary is_in_hd_tl:
    21   ∀to_search: addressing_mode.
    22   ∀hd: addressing_mode_tag.
    23   ∀n: nat.
    24   ∀v: Vector addressing_mode_tag n.
    25     bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
    26   #to_search #hd #n #v
    27   elim v
    28   [1:
    29     #absurd
    30     normalize in absurd; cases absurd
    31   |2:
    32     #n' #hd' #tl #inductive_hypothesis #assm
    33     >vector_cons_append >(vector_cons_append … hd' tl)
    34     @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
    35     assumption
    36   ]
    37 qed.
    385
    396let rec encoding_check
Note: See TracChangeset for help on using the changeset viewer.