Changeset 2128


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

Final shuffling around

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2124 r2128  
    244244 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
    245245 cases (is_a hd am) in ISIN; /2/
     246qed.
     247
     248lemma is_in_monotonic_wrt_append:
     249  ∀m, n: nat.
     250  ∀p: Vector addressing_mode_tag m.
     251  ∀q: Vector addressing_mode_tag n.
     252  ∀to_search: addressing_mode.
     253    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
     254  #m #n #p #q #to_search #assm
     255  elim q try assumption
     256  #n' #hd #tl #inductive_hypothesis
     257  normalize
     258  cases (is_a ??) try @I
     259  >inductive_hypothesis @I
     260qed.
     261
     262corollary is_in_hd_tl:
     263  ∀to_search: addressing_mode.
     264  ∀hd: addressing_mode_tag.
     265  ∀n: nat.
     266  ∀v: Vector addressing_mode_tag n.
     267    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
     268  #to_search #hd #n #v
     269  elim v
     270  [1:
     271    #absurd
     272    normalize in absurd; cases absurd
     273  |2:
     274    #n' #hd' #tl #inductive_hypothesis #assm
     275    >vector_cons_append >(vector_cons_append … hd' tl)
     276    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
     277    assumption
     278  ]
    246279qed.
    247280
  • 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.