Ignore:
Timestamp:
Apr 23, 2012, 6:10:51 PM (8 years ago)
Author:
mulligan
Message:

Changes to statements of theorems

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1897 r1899  
    4040       match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
    4141        λ${ident E}.$s ] ] (refl ? $t) }.
    42 
    43 (*
    44 lemma test:
    45   ∀b: nat.
    46   ∀c: nat × nat.
    47     Σx: nat. ∃y: nat. c = 〈y, x〉 ≝
    48   λb: nat.
    49   λc: nat × nat.
    50   match b return λb': nat. ∀r:b' = b. Σx: ?. ? with
    51   [ O ⇒ λr.
    52     let 〈left, right〉 as T return Σz:nat.∃y. c = 〈y,z〉 ≝ c in
    53     deplet 〈left', right'〉 as T' ≝ c in left'
    54   | S n ⇒ λr. deplet 〈left, right〉 as T ≝ c in left
    55   ] (refl … b).
    56 
    57 lemma test:
    58   ∀b: nat.
    59   ∀c: nat × nat.
    60     Σx: nat. ∃y: nat. c = 〈y, x〉 ≝
    61   λb: nat.
    62   λc: nat × nat.
    63   match b return λb': nat. b' = b → Σx: ?. ? with
    64   [ O ⇒ λr.
    65     deplet 〈left, right〉 as T ≝ c in
    66     deplet 〈left', right'〉 as T' ≝ c in
    67       left'
    68   | S n ⇒ λr. deplet 〈left, right〉 as T ≝ c in left
    69   ] (refl … b).
    70 
    71 lemma test:
    72   ∀b: nat.
    73   ∀c: nat × nat × nat.
    74     Σx: nat. ∃y: nat × nat. c = 〈y, x〉 ≝
    75   λb: nat.
    76   λc: nat × nat × nat.
    77   match b return λb': nat. b' = b → Σx: ?. ? with
    78   [ O ⇒ λr.
    79     deplet 〈left, centre, right〉 as T ≝ c in
    80     deplet 〈left', centre', right'〉 as T' ≝ c in
    81       left'
    82   | S n ⇒ λr. deplet 〈left, centre, right〉 as T ≝ c in left
    83   ] (refl … b).
    84 
    85 lemma pair_elim_as:
    86   ∀A,B,C: Type[0].
    87   ∀p.
    88   ∀T: ∀a: A. ∀b: B. 〈a, b〉 = p → C.
    89   ∀P: A×B → C → Prop.
    90     (∀lft, rgt. ∀H: 〈lft,rgt〉 = p. P 〈lft,rgt〉 (T lft rgt H)) →
    91       P p (let 〈lft, rgt〉 as H ≝ p in T lft rgt H).
    92  #A #B #C * /2/
    93 qed.
    94 
    95 lemma triple_elim_as:
    96   ∀A,B,C,D: Type[0].
    97   ∀p.
    98   ∀T: ∀a: A. ∀b: B. ∀c: C. 〈a, b, c〉 = p → D.
    99   ∀P: A×B×C → D → Prop.
    100     (∀lft, cntr, rgt. ∀H: 〈lft,cntr,rgt〉 = p. P 〈lft,cntr,rgt〉 (T lft cntr rgt H)) →
    101       P p (let 〈lft, cntr, rgt〉 as H ≝ p in T lft cntr rgt H).
    102  #A #B #C #D * * /2/
    103 qed. *)
    104 
    10542
    10643let rec traverse_code_internal
     
    11754          Σcost_map: identifier_map CostTag nat.
    11855            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    119             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k
     56            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k
    12057              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    12158                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
     
    224161        @(eq_identifier_elim … k lbl)
    225162        [1:
    226           #eq_assm %{program_counter} #lookup_opt_assm
    227           %{(reachable_program_counter_witness …)} try assumption
    228           >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
     163          #eq_assm %{program_counter} %
     164          [1:
     165            >eq_assm >lookup_refl %
     166          |2:
     167            %{(reachable_program_counter_witness …)} try assumption
     168            >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
     169          ]
    229170        |2:
    230171          #neq_assm
     
    234175            @(present_add_present … present_assm) assumption
    235176          |1:
    236             #program_counter' #ind_hyp' %{program_counter'}
    237             #relevant cases (ind_hyp' relevant) #reachable_witness'
    238             #ind_hyp'' %{reachable_witness'} >ind_hyp''
    239             @sym_eq @lookup_present_add_miss assumption
     177            #program_counter' #ind_hyp' %{program_counter'} %
     178            [1:
     179              cases ind_hyp' #assm #_ assumption
     180            |2:
     181              cases ind_hyp' #lookup_opt_assm * #reachable_witness'
     182              #ind_hyp'' %{reachable_witness'} >ind_hyp''
     183              @sym_eq @lookup_present_add_miss assumption
     184            ]
    240185          ]
    241186        ]
     
    402347  ∀code_memory: BitVectorTrie Byte 16.
    403348  ∀cost_labels: BitVectorTrie costlabel 16.
     349  ∀cost_labels_injective:
     350    ∀pc, pc',l.
     351      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
     352        pc = pc'.
    404353  ∀program_size: nat.
    405354  ∀program_size_limit: program_size ≤ 2^16.
     
    411360    Σcost_map: identifier_map CostTag nat.
    412361      (∀pc,k. nat_of_bitvector … pc < program_size → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    413       (∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
     362      (∀k. ∀k_pres:present … cost_map k. pc. lookup_opt … pc cost_labels = Some … k →
    414363        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
    415364          pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    416365  λcode_memory: BitVectorTrie Byte 16.
    417366  λcost_labels: BitVectorTrie costlabel 16.
     367  λcost_labels_injective.
    418368  λprogram_size: nat.
    419369  λprogram_size_limit: program_size ≤ 2^16.
     
    429379    cases (traverse_code_internal ? ? ? ? ? ? ? ? ?)
    430380    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
    431     try assumption #pc #k #pc_program_size_assm
    432     @inductive_hypothesis1
    433381    [1:
    434       @le_O_n
     382      #pc #k #pc_program_size_assm
     383      @inductive_hypothesis1
     384      [1:
     385        @le_O_n
     386      |2:
     387        normalize in match (nat_of_bitvector 16 (zero 16));
     388        <plus_n_O assumption
     389      ]
    435390    |2:
    436       normalize in match (nat_of_bitvector 16 (zero 16));
    437       <plus_n_O assumption
     391      #k #k_pres #pc #lookup_opt_assm
     392      cases (inductive_hypothesis2 ? k_pres)
     393      #program_counter' * #lookup_opt_assm' * #reachable_witness
     394      #block_cost_assm
     395      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
     396      %{reachable_witness} assumption
    438397    ]
    439398  ]
     
    443402  λprogram: list Byte.
    444403  λcost_labels: BitVectorTrie costlabel 16.
     404  λcost_labels_injective:
     405    ∀pc, pc',l.
     406      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
     407        pc = pc'.
    445408  λreachable_program_witness.
    446409  λgood_program_witness: good_program (load_code_memory program) (|program|).
     
    448411    let program_size ≝ |program| in
    449412    let code_memory ≝ load_code_memory program in
    450       traverse_code code_memory cost_labels program_size program_size_limit reachable_program_witness good_program_witness.
     413      traverse_code code_memory cost_labels cost_labels_injective program_size program_size_limit reachable_program_witness good_program_witness.
Note: See TracChangeset for help on using the changeset viewer.