Changeset 2211


Ignore:
Timestamp:
Jul 18, 2012, 3:57:09 PM (5 years ago)
Author:
boender
Message:
  • finished proof of sigma specification
  • added some stuff to Util, as usual
Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2153 r2211  
    1717        (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd x) 〈0,short_jump〉)))
    1818        (sigma_compact_unsafe program (create_label_map program) x))
    19         (\fst x < 2^16)
     19        (\fst x 2^16)
    2020    ]) ≝
    2121 let labels ≝ create_label_map program in
     
    260260    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    261261    sigma_compact_unsafe program (create_label_map program) p ∧
    262     \fst p < 2^16.
     262    \fst p 2^16.
    263263  ∀l.|l| ≤ |program| → ∀acc:ℕ.
    264264  match \snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy)) with
     
    332332    \fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉) ∧
    333333    sigma_compact_unsafe program (create_label_map program) p ∧
    334     \fst p < 2^16.
     334    \fst p 2^16.
    335335  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    336336  [ None ⇒ True
     
    418418    match p with
    419419      [ None ⇒ True
    420       | Some pol ⇒ And (*And (out_of_program_none program pol)*)
    421       (sigma_compact program (create_label_map program) pol)
    422       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
     420      | Some pol ⇒ And (And (And
     421          (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0)
     422          (\fst pol = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd pol) 〈0,short_jump〉)))
     423          (sigma_compact program (create_label_map program) pol))
     424          (\fst pol ≤ 2^16)
    423425      ].
    424426#program @(\snd (jump_expansion_internal program (S (2*|program|))))
     
    441443      [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS)
    442444      | -Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq
    443         @conj
    444         [ @(equal_compact_unsafe_compact ?? Fp)
     445        @conj [ @conj [ @conj
     446        [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     447        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
     448        ]
     449        | @(equal_compact_unsafe_compact ?? Fp)
    445450          [ lapply (jump_pc_equal program (2*|program|))
    446451            >Feq >Geq normalize nodelta #H @H @Heq
    447           | cases daemon
     452          | cases daemon (* true, but have to add this to properties *)
    448453          | @(proj2 ?? (proj1 ?? HGp))
    449454          ]
    450         (*| @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*80s*)
    451           >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq
    452           [ destruct (Geq) / by /
    453           | cases (jump_expansion_step program (create_label_map (pi1 ?? program)) «Fp,?») in Geq;
    454             #x cases x -x #Sch #So normalize nodelta cases So
    455             [ normalize nodelta #_ #ABS destruct (ABS)
    456             | -So normalize nodelta #Sp #HSp #Seq <(proj1 ?? (pair_destruct ?????? (pi1_eq ???? Seq)))
    457               cases Sch in HSp Seq; #HSp #Seq
    458               [ @refl
    459               | normalize nodelta in Seq; @(proj2 ?? (proj1 ?? HSp))
    460                 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Seq))))
    461                 @Heq
    462               ]
    463             ]
    464           ]
    465         ]*)
    466         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     455        ]
     456        | @(proj2 ?? HGp)
    467457        ]
    468458      ]
     
    552542      #z cases z -z #Gch #Go cases Go normalize nodelta
    553543      [ #HGp #Geq @I
    554       | -Go #Gp normalize nodelta #HGp #Geq @conj
    555         [ @(equal_compact_unsafe_compact ?? Fp)
     544      | -Go #Gp normalize nodelta #HGp #Geq @conj [ @conj [ @conj
     545        [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     546        | @(proj2 ?? (proj1 ?? (proj1 ?? HGp)))
     547        ]
     548        | @(equal_compact_unsafe_compact ?? Fp)
    556549          [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
    557550            #H @H #i #Hi
     
    580573                >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
    581574              ]
    582             | cases daemon
     575            | cases daemon (* true, but have to add to properties in some way *)
    583576            | @(proj2 ?? (proj1 ?? HGp))
    584577            ]
    585           | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))
     578          ]
     579          | @(proj2 ?? HGp)
    586580          ]
    587581        ]
     
    608602include alias "basics/logic.ma".
    609603
     604lemma pc_increases: ∀i,j:ℕ.∀program.∀pol:Σp:ppc_pc_map.
     605  And (And (And
     606    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)
     607    (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
     608    (sigma_compact program (create_label_map program) p))
     609    (\fst p ≤ 2^16).i ≤ j → j ≤ |program| →
     610  \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 i) (\snd pol) 〈0,short_jump〉) ≤
     611  \fst (bvt_lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 j) (\snd pol) 〈0,short_jump〉).
     612 #i #j #program #pol #H elim (le_to_eq_plus … H) #n #Hn >Hn -Hn -j elim n
     613 [ <plus_n_O #_ @le_n
     614 | -n #n <plus_n_Sm #Hind #H @(transitive_le ??? (Hind (le_S_to_le … H)))
     615   lapply (proj2 ?? (proj1 ?? (pi2 ?? pol)) (i+n) H)
     616   lapply (refl ? (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)))
     617   cases (lookup_opt … (bitvector_of_nat ? (i+n)) (\snd pol)) in ⊢ (???% → %);
     618   [ normalize nodelta #_ #abs cases abs
     619   | #x cases x -x #pc #jl #EQ normalize nodelta
     620     lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)))
     621     cases (lookup_opt … (bitvector_of_nat ? (S (i+n))) (\snd pol)) in ⊢ (???% → %);
     622     [ normalize nodelta #_ #abs cases abs
     623     | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hcomp
     624       >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     625       >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hcomp @le_plus_n_r
     626     ]
     627   ]
     628 ]
     629qed.
     630 
    610631(* The glue between Policy and Assembly. *)
    611632(*CSC: modified to really use the specification in Assembly.ma.*)
     
    630651#fpc #fpol #Hfpol
    631652@conj
    632 [ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
     653[ lapply (proj1 ?? (proj1 ?? (proj1 ?? Hfpol))) cases (bvt_lookup ??? fpol 〈0,short_jump〉)
    633654  #x #y #Hx normalize nodelta >Hx / by refl/
    634 | cases daemon (* leaving this until stabilisation of sigma predicate *)
    635   (*#ppc #ppc_ok normalize nodelta @conj
    636   [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok)
     655| #ppc #ppc_ok normalize nodelta @conj
     656  [ lapply ((proj2 ?? (proj1 ?? Hfpol)) (nat_of_bitvector ? ppc) ppc_ok)
    637657    >bitvector_of_nat_inverse_nat_of_bitvector
    638658    lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
    639     [ normalize nodelta #_ #abs cases abs
    640     | #x cases x -x #x1 #y1 normalize nodelta #Hl_ppc
    641       >(plus_n_O (nat_of_bitvector 16 ppc)) >plus_n_Sm <add_bitvector_of_nat_plus
    642       >bitvector_of_nat_inverse_nat_of_bitvector
    643       lapply (refl ? (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol))
    644       cases (lookup_opt … (add 16 ppc (bitvector_of_nat 16 1)) fpol) in ⊢ (???% → %);
    645       [ normalize nodelta #_ #abs cases abs
    646       | #x cases x -x #x2 #y2 normalize nodelta #Hl_Sppc
    647         #Hcompact >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉)
    648         >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
    649         >add_bitvector_of_nat_plus whd in match (fetch_pseudo_instruction ???);
    650         >(nth_safe_nth … 〈None ?, Comment []〉)
    651         >Hcompact <plus_n_O
    652         cases (nth (nat_of_bitvector ? ppc) ? (\snd program) ?) #a #b normalize nodelta
    653         whd in match instruction_size; normalize nodelta
    654         whd in match assembly_1_pseudoinstruction; normalize nodelta
    655         whd in match expand_pseudo_instruction; normalize nodelta
    656         cases b
    657         [2,3,6: #p [3: #q] normalize nodelta @refl
    658         |4,5: #p normalize nodelta
    659           >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta
    660           >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
    661           whd in match (create_label_map ?);
    662           cases (lookup ?? (bitvector_of_nat ?
    663           (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉)
    664           #z1 #z2 normalize nodelta @refl
     659    [ #Hl normalize nodelta #abs cases abs
     660    | #x cases x -x #pc #jl #Hl normalize nodelta <add_bitvector_of_nat_Sm
     661      >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative
     662      lapply (refl ? (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol))
     663      cases (lookup_opt … (add ? ppc (bitvector_of_nat ? 1)) fpol) in ⊢ (???% → %);
     664      [ #Hl normalize nodelta #abs cases abs
     665      | #x cases x -x #Spc #Sjl #SHl normalize nodelta #Hcompact
     666        >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
     667        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
     668        >add_bitvector_of_nat_plus >Hcompact whd in match instruction_size;
     669        normalize nodelta whd in match assembly_1_pseudoinstruction;
     670        normalize nodelta whd in match expand_pseudo_instruction;
     671        normalize nodelta whd in match fetch_pseudo_instruction;
     672        normalize nodelta
     673        lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok))
     674        cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %);
     675        #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉)
     676        >Hli normalize nodelta cases instr
     677        [2,3,6: #x [3: #y] normalize nodelta %
     678        |4,5: #x normalize nodelta
     679          >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
     680          whd in match create_label_map; normalize nodelta
     681          >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
     682          cases (bvt_lookup … (bitvector_of_nat ?
     683           (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     684          #lpc #ljl normalize nodelta @refl
    665685        |1: #pi cases pi
    666686          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    667             [1,2,3,6,7,24,25: #p #q
    668             |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #p]
    669             normalize nodelta @refl
    670           |9,10,11,12,13,14,15,16,17: [1,2,6,7: #p |3,4,5,8,9: #q #p] normalize nodelta
     687            [1,2,3,6,7,24,25: #x #y
     688            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     689            normalize nodelta %
     690          |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
    671691            whd in match expand_relative_jump; normalize nodelta
    672692            whd in match expand_relative_jump_internal; normalize nodelta
    673             >(lookup_opt_lookup_hit … Hl_Sppc 〈0,short_jump〉) normalize nodelta
    674             >(lookup_opt_lookup_hit … Hl_ppc 〈0,short_jump〉) normalize nodelta
    675             whd in match (create_label_map ?);
    676             cases (lookup ?? (bitvector_of_nat ?
    677             (lookup_def ?? (\fst (create_label_cost_map (\snd program))) p 0)) fpol 〈0,short_jump〉)
    678             #z1 #z2 normalize nodelta @refl
     693            >(lookup_opt_lookup_hit … SHl 〈0,short_jump〉) normalize nodelta
     694            whd in match create_label_map; normalize nodelta
     695            >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) normalize nodelta
     696            cases (bvt_lookup … (bitvector_of_nat ?
     697             (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     698            #lpc #ljl normalize nodelta %
    679699          ]
    680700        ]
    681701      ]
    682     ]
    683   | cases daemon (* XXX remains to be done *)
    684   ] *)
    685 ]
    686 qed.           
     702    ]
     703  | (* Basic proof scheme:
     704       - ppc < |snd program|, hence our instruction is in the program
     705       - either we are the last non-zero-size instruction, in which case we are
     706         either smaller than 2^16 (because the entire program is), or we are exactly
     707         2^16 and something weird happens
     708       - or we are not, in which case we are definitely smaller than 2^16 (by transitivity
     709         through the next non-zero instruction)
     710    *)
     711    elim (le_to_or_lt_eq … (proj2 ?? Hfpol)) #Hfpc
     712    [ %1 @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol)))
     713      lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
     714      >bitvector_of_nat_inverse_nat_of_bitvector
     715      lapply (refl ? (lookup_opt … ppc fpol)) cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
     716      [ normalize nodelta #_ #abs cases abs
     717      | #x cases x -x #pc #jl #EQ normalize nodelta
     718        lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
     719        cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
     720        [ normalize nodelta #_ #abs cases abs
     721        | #x cases x -x #Spc #Sjl #SEQ normalize nodelta whd in match instruction_size;
     722          normalize nodelta whd in match assembly_1_pseudoinstruction;
     723          normalize nodelta whd in match expand_pseudo_instruction;
     724          normalize nodelta whd in match fetch_pseudo_instruction;
     725          normalize nodelta
     726          lapply (refl ? (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok))
     727          cases (nth_safe … (nat_of_bitvector ? ppc) (\snd program) ppc_ok) in ⊢ (???% → %);
     728          #label #instr normalize nodelta #Hli <(nth_safe_nth ? (\snd program) (nat_of_bitvector 16 ppc) ppc_ok 〈None ?, Comment []〉)
     729          >Hli normalize nodelta cases instr
     730          [2,3,6: #x [3: #y] normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     731            normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
     732            [1,3,5: <H
     733              lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     734              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X
     735            |2,4,6: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     736              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     737              #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
     738            ]
     739          |4,5: #x normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     740            normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
     741            [1,3: <add_bitvector_of_nat_Sm in SEQ;
     742              >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ
     743              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta
     744              cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     745              #lpc #ljl normalize nodelta #H <H
     746              lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     747              <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector
     748              >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2
     749            |2,4: lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     750              >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     751              #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
     752            ]
     753          |1: #pi cases pi
     754            [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     755              [1,2,3,6,7,24,25: #x #y
     756              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     757              normalize nodelta #H >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     758              normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
     759              [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
     760                <H lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     761                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #X @X
     762              |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
     763                lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     764                >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     765                #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
     766              ]
     767            |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x]
     768              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     769              normalize nodelta >nat_of_bitvector_bitvector_of_nat_inverse
     770              [1,3,5,7,9,11,13,15,17: <add_bitvector_of_nat_Sm in SEQ;
     771                >bitvector_of_nat_inverse_nat_of_bitvector >add_commutative #SEQ
     772                whd in match expand_relative_jump; normalize nodelta
     773                whd in match expand_relative_jump_internal; normalize nodelta
     774                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) normalize nodelta
     775                cases (bvt_lookup ?? (bitvector_of_nat ? (lookup_def ?? (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     776                #lpc #ljl normalize nodelta #H <H
     777                lapply (pc_increases (S (nat_of_bitvector 16 ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?))
     778                <add_bitvector_of_nat_Sm >bitvector_of_nat_inverse_nat_of_bitvector
     779                >add_commutative >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #H2 @H2
     780              |2,4,6,8,10,12,14,16,18:
     781                lapply (pc_increases (nat_of_bitvector 16 ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?))
     782                >bitvector_of_nat_inverse_nat_of_bitvector >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     783                #H @(le_to_lt_to_lt … Hfpc) >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @H
     784              ]
     785            ]
     786          ]
     787        ]
     788      ]
     789    | (* the program is of length 2^16 and ppc is followed by only zero-size instructions
     790       * until the end of the program *)
     791      elim (le_to_or_lt_eq … (pc_increases (nat_of_bitvector ? ppc) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok) (le_n ?)))
     792      [ lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc) ppc_ok)
     793        >bitvector_of_nat_inverse_nat_of_bitvector
     794        lapply (refl ? (lookup_opt … ppc fpol))
     795        cases (lookup_opt … ppc fpol) in ⊢ (???% → %);
     796        [ #_ normalize nodelta #abs cases abs
     797        | #x cases x -x #pc #jl #EQ normalize nodelta
     798          lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol))
     799          cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc))) fpol) in ⊢ (???% → %);
     800          [ #_ normalize nodelta #abs cases abs
     801          | #x cases x -x #Spc #Sjl #SEQ normalize nodelta #Hc
     802            >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hpc normalize nodelta
     803            >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     804            >nat_of_bitvector_bitvector_of_nat_inverse
     805            [2: <Hfpc >(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) @Hpc ]
     806            elim (le_to_or_lt_eq … (pc_increases (S (nat_of_bitvector ? ppc)) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok (le_n ?)))
     807            [ <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
     808              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #HSpc %1
     809              >Hc in HSpc;
     810              whd in match create_label_map;
     811              whd in match fetch_pseudo_instruction; normalize nodelta
     812              >(nth_safe_nth … 〈None ?, Comment []〉)
     813              cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
     814              #lbl #ins normalize nodelta
     815              whd in match instruction_size;
     816              whd in match assembly_1_pseudoinstruction;
     817              whd in match expand_pseudo_instruction; normalize nodelta
     818              <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
     819              >add_commutative #SEQ cases ins
     820              [2,3,6: #x [3: #y] normalize nodelta #H @H
     821              |4,5: #x normalize nodelta
     822                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     823                >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     824                cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     825                #lpc #ljl normalize nodelta #H @H
     826              |1: #pi cases pi
     827                [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     828                  [1,2,3,6,7,24,25: #x #y
     829                  |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     830                  normalize nodelta #H @H
     831                |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
     832                  whd in match expand_relative_jump;
     833                  whd in match expand_relative_jump_internal; normalize nodelta
     834                  >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     835                  >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     836                  cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     837                  #lpc #ljl normalize nodelta #H @H
     838                ]
     839              ]
     840            | <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
     841              >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) #Hspc %2 @conj
     842              [ #ppc' #ppc_ok' #Hppc'
     843                (* S ppc < ppc' < |\snd program| *)
     844                (* lookup S ppc = 2^16 *)
     845                (* lookup |\snd program| = 2^16 *)
     846                (* lookup ppc' = 2^16 → instruction size = 0 *)
     847                lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector ? ppc') ppc_ok')
     848                >bitvector_of_nat_inverse_nat_of_bitvector
     849                lapply (refl ? (lookup_opt … ppc' fpol))
     850                cases (lookup_opt … ppc' fpol) in ⊢ (???% → %);
     851                [ normalize nodelta #_ #abs cases abs
     852                | normalize nodelta #x cases x -x #xpc #xjl #XEQ normalize nodelta
     853                  lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol))
     854                  cases (lookup_opt … (bitvector_of_nat ? (S (nat_of_bitvector ? ppc'))) fpol) in ⊢ (???% → %);
     855                  [ normalize nodelta #_ #abs cases abs
     856                  | normalize nodelta #x cases x -x #Sxpc #Sxjl #SXEQ normalize nodelta
     857                    #Hpcompact
     858                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (nat_of_bitvector ? ppc') (\snd program) «〈fpc,fpol〉,Hfpol» Hppc' (le_S_to_le … ppc_ok'))
     859                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1
     860                    lapply (pc_increases (nat_of_bitvector ? ppc') (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … ppc_ok') (le_n ?))
     861                    <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2
     862                    lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle2 -Hle1
     863                    >bitvector_of_nat_inverse_nat_of_bitvector
     864                    >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉) #Hxpc
     865                    lapply (pc_increases (S (nat_of_bitvector ? ppc)) (S (nat_of_bitvector ? ppc')) (\snd program) «〈fpc,fpol〉,Hfpol» (le_S_to_le … (le_S_S … Hppc')) ppc_ok')
     866                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉) >Hspc #Hle1
     867                    lapply (pc_increases (S (nat_of_bitvector ? ppc')) (|\snd program|) (\snd program) «〈fpc,fpol〉,Hfpol» ppc_ok' (le_n ?))
     868                    <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc #Hle2
     869                    lapply (le_to_le_to_eq ?? Hle2 Hle1) -Hle1 -Hle2
     870                    >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉) #HSxpc
     871                    >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H
     872                    @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction;
     873                    normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)
     874                    cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;
     875                    #lbl #ins normalize nodelta
     876                    whd in match instruction_size;
     877                    whd in match assembly_1_pseudoinstruction;
     878                    whd in match expand_pseudo_instruction; normalize nodelta
     879                    <add_bitvector_of_nat_Sm in SXEQ; >bitvector_of_nat_inverse_nat_of_bitvector
     880                    >add_commutative #SXEQ cases ins
     881                    [2,3,6: #x [3: #y] normalize nodelta #H @(sym_eq ??? H)
     882                    |4,5: #x normalize nodelta
     883                      >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉)
     884                      >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉)
     885                      cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     886                      #lpc #ljl normalize nodelta #H @(sym_eq ??? H)
     887                    |1: #pi cases pi
     888                      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     889                        [1,2,3,6,7,24,25: #x #y
     890                        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta
     891                          #H @(sym_eq ??? H)
     892                      |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
     893                        whd in match expand_relative_jump;
     894                        whd in match expand_relative_jump_internal; normalize nodelta
     895                        >(lookup_opt_lookup_hit … XEQ 〈0,short_jump〉)
     896                        >(lookup_opt_lookup_hit … SXEQ 〈0,short_jump〉)
     897                        cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     898                        #lpc #ljl normalize nodelta #H @(sym_eq ??? H)
     899                      ]
     900                    ]
     901                  ]
     902                ]
     903              | >Hc in Hspc;
     904                whd in match create_label_map;
     905                whd in match fetch_pseudo_instruction; normalize nodelta
     906                >(nth_safe_nth … 〈None ?, Comment []〉)
     907                cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)
     908                 #lbl #ins normalize nodelta
     909                whd in match instruction_size;
     910                whd in match assembly_1_pseudoinstruction;
     911                whd in match expand_pseudo_instruction; normalize nodelta
     912                <add_bitvector_of_nat_Sm in SEQ; >bitvector_of_nat_inverse_nat_of_bitvector
     913                >add_commutative #SEQ cases ins
     914                [2,3,6: #x [3: #y] normalize nodelta #H @H
     915                |4,5: #x normalize nodelta
     916                  >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     917                  >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     918                  cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     919                  #lpc #ljl normalize nodelta #H @H
     920                |1: #pi cases pi
     921                  [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     922                    [1,2,3,6,7,24,25: #x #y
     923                    |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta
     924                    #H @H
     925                  |9,10,11,12,13,14,15,16,17: [3,4,5,8,9: #y #x |1,2,6,7: #x] normalize nodelta
     926                    whd in match expand_relative_jump;
     927                    whd in match expand_relative_jump_internal; normalize nodelta
     928                    >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     929                    >(lookup_opt_lookup_hit … SEQ 〈0,short_jump〉)
     930                    cases (lookup … (bitvector_of_nat ? (lookup_def … (\fst (create_label_cost_map (\snd program))) x 0)) fpol 〈0,short_jump〉)
     931                    #lpc #ljl normalize nodelta #H @H
     932                  ]
     933                ]
     934              ]
     935            ]
     936          ]
     937        ]
     938      | >bitvector_of_nat_inverse_nat_of_bitvector
     939        <(proj2 ?? (proj1 ?? (proj1 ?? Hfpol))) >Hfpc
     940        cases (lookup … ppc fpol 〈0,short_jump〉) #pc #jl normalize nodelta #Hpc %1 >Hpc
     941        >bitvector_of_nat_exp_zero whd in match (nat_of_bitvector ? (zero ?));
     942        <plus_O_n whd in match instruction_size; normalize nodelta
     943        lapply (refl ? (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?))
     944        [5: cases (assembly_1_pseudoinstruction ??? ppc (λx0.zero 16) ?) in ⊢ (???% → %);
     945          #len #ins #Hass lapply (fst_snd_assembly_1_pseudoinstruction … Hass)
     946          #Hli >Hli
     947          lapply (assembly1_pseudoinstruction_lt_2_to_16 ??? ppc (λx0.zero 16) ?)
     948          [5: >Hass / by /
     949          ]
     950        ]
     951      ]
     952    ]
     953  ]
     954]
     955qed.
  • src/ASM/PolicyFront.ma

    r2152 r2211  
    122122   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in
    123123   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in
    124      (*opc ≤ pc ∧*) jmpleq oj j.
     124     jmpleq oj j.
    125125     
    126126(* this is the instruction size as determined by the jump length given *)
     
    407407       (∀i.i ≤ |program| → ∃pc.
    408408         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
    409        (\fst p < 2^16)         
     409       (\fst p 2^16)         
    410410    ] ≝
    411411  λprogram.λlabels.
     
    425425   〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉
    426426  ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in
    427   if geb (\fst (pi1 ?? final_policy)) 2^16 then
     427  if gtb (\fst (pi1 ?? final_policy)) 2^16 then
    428428    None ?
    429429  else
     
    431431[ / by I/
    432432| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    433   @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    434 | @conj [ @conj [ @conj [ @conj (*[@conj
    435   [ (* out_of_program_none *)
    436     #i #Hi2 >append_length <commutative_plus @conj
    437     [ (* → *) #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
    438       cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
    439       [ >lookup_opt_insert_miss
    440         [ (* USE[pass]: out_of_program_none → *)
    441           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2))
    442           @le_S_to_le @le_S_to_le @Hi
    443         | @bitvector_of_nat_abs
    444           [ @Hi2
    445           | @(transitive_lt … Hi2) @le_S_to_le @Hi
    446           | @sym_neq @lt_to_not_eq @le_S_to_le @Hi
    447           ]
    448         ]
    449       | >lookup_opt_insert_miss
    450         [ <Hi
    451           (* USE[pass]: out_of_program_none → *)
    452           @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?))
    453           [ >Hi @Hi2
    454           | @le_S @le_n
    455           ]
    456         | @bitvector_of_nat_abs
    457           [ @Hi2
    458           | @(transitive_lt … Hi2) <Hi @le_n
    459           | @sym_neq @lt_to_not_eq <Hi @le_n
    460           ]
    461         ]
    462       ]
    463     | (* ← *) cases p -p #p cases p -p #pc #p #Hp cases x in prf; -x #l #pi #prf
    464       normalize nodelta cases (decidable_eq_nat i (S (|prefix|)))
    465       [ #Hi >Hi >lookup_opt_insert_hit #H destruct (H)
    466       | #Hi >lookup_opt_insert_miss
    467         [ #Hl
    468           (* USE[pass]: out_of_program_none ← *)
    469           elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl))
    470           [ #Hi3 @Hi3
    471           | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi
    472           ]
    473         | @bitvector_of_nat_abs
    474           [ @Hi2
    475           | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length
    476             <plus_n_Sm @le_S_S @le_plus_n_r
    477           | @Hi
    478           ]
    479         ]
    480       ]
    481     ]
    482   | *)
     433  @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ]
     434| @conj [ @conj [ @conj [ @conj
    483435  [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
    484436    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
     
    594546    ]
    595547  ]
    596 | @conj [ @conj [ @conj [ @conj (*[ @conj
    597   [ #i cases i
    598     [ #Hi2 @conj
    599       [ (* → *) #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
    600       | (* ← *) >lookup_opt_insert_hit #Hl destruct (Hl)
    601       ]
    602     | -i #i #Hi2 @conj
    603       [ #Hi >lookup_opt_insert_miss
    604         [ / by refl/
    605         | @bitvector_of_nat_abs
    606           [ @Hi2
    607           | / by /
    608           | @sym_neq @lt_to_not_eq / by /
    609           ]
    610         ]
    611       | #_ @le_S_S @le_O_n
    612       ]
    613     ] *)
     548| @conj [ @conj [ @conj [ @conj
    614549  [ #i cases i
    615550    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
  • src/ASM/PolicyStep.ma

    r2152 r2211  
    1717    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
    1818    (sigma_compact_unsafe program labels policy))
    19     (\fst policy < 2^16)).
     19    (\fst policy 2^16)).
    2020  (Σx:bool × (option ppc_pc_map).
    2121    let 〈no_ch,y〉 ≝ x in
     
    3030       (sigma_jump_equal program old_policy p → no_ch = true))
    3131       (no_ch = true → sigma_pc_equal program old_policy p))
    32        (\fst p < 2^16)
     32       (\fst p 2^16)
    3333    ])
    3434    ≝
     
    9393        (Stub ??)〉〉
    9494    ) in
    95     if geb (\fst final_policy) 2^16 then
     95    if gtb (\fst final_policy) 2^16 then
    9696      〈eqb final_added 0, None ?〉
    9797    else
     
    127127    ]
    128128  | #abs >abs in Hsig; #Hsig
    129     @(absurd ? Hsig) @le_to_not_lt @leb_true_to_le <geb_to_leb @Hge
     129    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
    130130  ]
    131131| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
     
    141141     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
    142142  ]
    143   | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
     143  | @not_lt_to_le @ltb_false_to_not_lt @p1
    144144  ]
    145145|4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
     
    153153  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
    154154   * commented out for full proofs, but this needs a lot of memory and time *)
    155   [ (* not_jump_default *) cases daemon (*
    156     #i >append_length <commutative_plus #Hi normalize in Hi;
     155  [ (* not_jump_default *) cases daemon
     156    (* #i >append_length <commutative_plus #Hi normalize in Hi;
    157157    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    158158    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     
    160160        [ >(nth_append_first ? i prefix ?? Hi)
    161161          (* USE[pass]: not_jump_default *)
    162           @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)
     162          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi)
    163163        | @bitvector_of_nat_abs
    164164          [ @(transitive_lt ??? Hi) ]
     
    199199      ]
    200200    ] *)
    201   | (* 0 ↦ 0 *) cases daemon (*
    202     <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
     201  | (* 0 ↦ 0 *) cases daemon
     202    (* <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    203203    [ cases (decidable_eq_nat 0 (|prefix|))
    204204      [ #Heq <Heq >lookup_insert_hit
    205205        (* USE: inc_pc = fst policy *)
    206         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     206        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     207        <Heq
    207208        (* USE[pass]: 0 ↦ 0 *)
    208         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    209         <Heq #ONE #TWO >TWO >ONE @refl
     209        @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    210210      | #Hneq >lookup_insert_miss
    211         [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     211        [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    212212        | @bitvector_of_nat_abs
    213213          [3: @Hneq]
     
    216216    | @bitvector_of_nat_abs
    217217      [3: @lt_to_not_eq / by / ]
    218     ]     
     218    ]
    219219    [1,3: / by /
    220220    |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
     
    226226    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
    227227  ]
    228   | (* jump_increase *) cases daemon (*
    229     #i >append_length >commutative_plus #Hi normalize in Hi;
     228  | (* jump_increase *) cases daemon
     229    (* #i >append_length >commutative_plus #Hi normalize in Hi;
    230230    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    231231    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    232232      [ (* USE[pass]: jump_increase *)
    233         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi))
     233        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
    234234        <(proj2 ?? (pair_destruct ?????? Heq2))
    235235        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
     
    322322    ] *)
    323323  ]
    324   | (* sigma_compact_unsafe *) cases daemon (*
    325     #i >append_length <commutative_plus #Hi normalize in Hi;
     324  | (* sigma_compact_unsafe *) cases daemon
     325    (* #i >append_length <commutative_plus #Hi normalize in Hi;
    326326    <(proj2 ?? (pair_destruct ?????? Heq2))
    327327    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     
    332332            [ >lookup_opt_insert_miss
    333333              [ (* USE[pass]: sigma_compact_unsafe *)
    334                 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
     334                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
    335335                [ @le_S_to_le @Hi ]
    336336                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
     
    351351            | >Hi >lookup_opt_insert_hit normalize nodelta
    352352              (* USE[pass]: sigma_compact_unsafe *)
    353               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
     353              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
    354354              [ <Hi @le_n
    355355              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
     
    357357                | #x cases x -x #x1 #x2
    358358                  (* USE: inc_pc = fst inc_sigma *)
    359                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     359                  lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    360360                  <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
    361361                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
     
    393393      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
    394394      (* USE: out_of_program_none ← *)
    395       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i ?))
     395      lapply (proj2 ?? (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i ?))
    396396      [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r
    397397      | >Hi
    398398        (* USE: inc_pc = fst policy *)
    399         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     399        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    400400        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
    401401        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
    402402        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
    403           [ @H @refl
     403          [ @H %
    404404          | @le_to_not_lt @le_n
    405405          ]
     
    427427    ] *)
    428428  ]
    429   | (* policy_jump_equal → added = 0 *) cases daemon (*
    430     <(proj2 ?? (pair_destruct ?????? Heq2))
     429  | (* policy_jump_equal → added = 0 *) cases daemon
     430    (* <(proj2 ?? (pair_destruct ?????? Heq2))
    431431    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
    432432    (* USE[pass]: policy_jump_equal → added = 0 *)
    433     >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) ?)
     433    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) ?)
    434434    [ cases instr in Heq1 Heq;
    435435      [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
     
    437437        #Heq lapply Holdeq -Holdeq
    438438        (* USE: inc_pc = fst inc_sigma *)
    439         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     439        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    440440        lapply (Heq (|prefix|) ?)
    441441        [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     
    458458          <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq -Holdeq
    459459          (* USE: inc_pc = fst inc_sigma *)
    460           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     460          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    461461          lapply (Heq (|prefix|) ?)
    462462          [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     
    496496    ] *)
    497497  ]
    498   | (* added = 0 → policy_pc_equal *) cases daemon (*
    499     (* USE: added = 0 → policy_pc_equal *)
    500     lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     498  | (* added = 0 → policy_pc_equal *) cases daemon
     499    (* USE[pass]: added = 0 → policy_pc_equal *)
     500    (* lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    501501    <(proj2 ?? (pair_destruct ?????? Heq2))
    502502    <(proj1 ?? (pair_destruct ?????? Heq2))
     
    527527          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
    528528            @sym_eq (* USE: fst p = lookup |prefix| *)
    529              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     529            @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    530530          |2,4,6: @bitvector_of_nat_abs
    531531            [3,6,9: @lt_to_not_eq @le_n
     
    538538      |2,4,6: >Hi >lookup_insert_hit
    539539        (* USE fst p = lookup |prefix| *)
    540         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     540        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    541541        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    542542        (* USE: sigma_compact (from old_sigma) *)
     
    587587             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
    588588             (* USE: fst p = lookup |prefix| *)
    589              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     589             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    590590           |2,4: @bitvector_of_nat_abs
    591591             [3,6: @lt_to_not_eq @le_n
     
    601601           @jump_length_le_max / by I/
    602602         |2,4: #H (* USE: fst p = lookup |prefix| *)
    603            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     603           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    604604           <(Hold ? (|prefix|) (le_n (|prefix|)))
    605605           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
     
    671671              >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq
    672672              (* USE: fst p = lookup |prefix| *)
    673               @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     673              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    674674            |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    675675              @bitvector_of_nat_abs
     
    686686          >Hi >lookup_insert_hit
    687687          (* USE fst p = lookup |prefix| *)
    688           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     688          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    689689          <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    690690          (* USE: sigma_compact (from old_sigma) *)
     
    746746              [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
    747747              (* USE: fst p = lookup |prefix| *)
    748               @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
     748              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    749749            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    750750              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
     
    797797    ] *)
    798798  ]
    799   | (* out_of_program_none *) cases daemon 
     799  | (* out_of_program_none *) cases daemon
    800800    (* #i #Hi2 >append_length <commutative_plus @conj
    801801    [ (* → *) #Hi normalize in Hi;
     
    969969    ] *)
    970970  ]
    971   | (* sigma_safe *) cases daemon
    972     (* #i >append_length >commutative_plus #Hi normalize in Hi;
     971  | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
    973972    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    974973    [ >nth_append_first [2: @Hi]
     
    978977          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
    979978            [ >lookup_insert_miss
    980               [ lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
    981                 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi))
    982                lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma))
    983                 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) in ⊢ (???% → %);
    984                 [ normalize nodelta #_ #abs cases abs
    985                 | #x cases x -x #ipc #ij #EQi normalize nodelta
    986                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
    987                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
    988                   [ normalize nodelta #_ #abs cases abs
    989                   | #x cases x -x #Sipc #Sij #EQSi normalize nodelta #Hcompact
    990                     >(lookup_opt_lookup_hit … EQi 〈0,short_jump〉)
    991                     >(lookup_opt_lookup_hit … EQSi 〈0,short_jump〉) >Hcompact
    992                     normalize nodelta (*cases ij*) normalize nodelta
    993                     lapply (refl ? (nth i ? prefix 〈None ?, Comment []〉))
    994                     cases (nth i ? prefix 〈None ?, Comment []〉) in ⊢ (???% → %);
    995                     #lbl #ins normalize nodelta #Hins #Hind #dest #Hi
    996                     lapply (Hind dest Hi) -Hind #Hind
    997                     elim (decidable_le (lookup_def … labels dest 0) (S (|prefix|)))
    998                     [ #Hle elim (le_to_or_lt_eq … Hle) -Hle #Hle
    999                       [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) -Hle #Hle
    1000                         [ >(le_to_leb_true ?? (le_S_to_le ?? Hle)) in Hind;
    1001                           >(le_to_leb_true ?? (le_S ?? (le_S_to_le ?? Hle)))
    1002                           normalize nodelta >lookup_insert_miss
    1003                           [ >lookup_insert_miss
    1004                             [ #H @H
    1005                             | @bitvector_of_nat_abs
    1006                               [3: @lt_to_not_eq @Hle
    1007                               |1: @(transitive_lt ??? Hle)
    1008                               ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    1009                                >append_length @le_S_S @le_plus_n_r
    1010                             ]
    1011                           | @bitvector_of_nat_abs
    1012                             [3: @lt_to_not_eq @le_S_to_le @le_S_S @Hle
    1013                             |1: @(transitive_lt ??? Hle) @le_S_to_le
    1014                             ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    1015                             >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    1016                           ]
    1017                         | >Hle >Hle in Hind; >(le_to_leb_true ?? (le_n (|prefix|)))
    1018                           >(le_to_leb_true ?? (le_S ?? (le_n (|prefix|))))
    1019                           normalize nodelta >lookup_insert_miss
    1020                           [ >lookup_insert_hit
    1021                             >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1022                             #H @H
    1023                           | @bitvector_of_nat_abs
    1024                             [3: @lt_to_not_eq @le_n
    1025                             |1: @le_S_to_le
    1026                             ] @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
    1027                             >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    1028                           ]
    1029                         ]
    1030                       | >Hle >Hle in Hind;
    1031                         >(not_le_to_leb_false (S (|prefix|)) (|prefix|))
    1032                         [2: @le_to_not_lt @le_n]
    1033                         >(le_to_leb_true ?? (le_n (S (|prefix|))))
    1034                         normalize nodelta >lookup_insert_hit
    1035                         lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    1036                         [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    1037                         | lapply (proj2 ?? (proj1 ?? Hpolicy))
    1038                           lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    1039                           cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    1040                           [ normalize nodelta #_ #_ #abs cases abs
    1041                           | #x cases x -x #opc #oj #EQo
    1042                             lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    1043                             cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    1044                             [ normalize nodelta #_ #_ #abs cases abs
    1045                             | #x cases x -x #Sopc #Soj #EQSo normalize nodelta
    1046                               #Hadded #Hcommon
    1047                               >(lookup_opt_lookup_hit … EQSo 〈0,short_jump〉)
    1048                               >Hcommon >(lookup_opt_lookup_hit … EQo 〈0,short_jump〉) in Holdeq;
    1049                               #Holdeq >(proj1 ?? (pair_destruct ?????? Holdeq))
    1050                               >(commutative_plus old_pc ?) >associative_plus
    1051                               <Hadded
    1052                               <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1053                               >prf >nth_append_second
    1054                               [ <minus_n_n whd in match (nth ????); >p1 cases instr in Heq1;
    1055                                 [2,3,6: #x [3: #y] normalize nodelta #Heq1
    1056                                   <(proj2 ?? (pair_destruct ?????? Heq1))
    1057                                   <(commutative_plus inc_pc)
    1058                                   >(instruction_size_irrelevant ?? oj short_jump)
    1059                                   [1,3,5: #H @H
    1060                                   |2,4,6: @nmk #H @H
    1061                                   ]
    1062                                 |4,5: #x normalize nodelta #Heq1
    1063                                   <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
    1064                                   cases daemon (* axiomatise this *)
    1065                                 |1: #pi cases pi
    1066                                   [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    1067                                     [1,2,3,6,7,24,25: #x #y
    1068                                     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    1069                                     normalize nodelta #Heq1
    1070                                     <(proj2 ?? (pair_destruct ?????? Heq1))
    1071                                     <(commutative_plus inc_pc)
    1072                                     >(instruction_size_irrelevant ?? oj short_jump)
    1073                                     [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    1074                                       #H @H
    1075                                     |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    1076                                       @nmk #H @H
    1077                                     ]
    1078                                   |9,10,11,12,13,14,15,16,17:
    1079                                     #x [3,4,5,8,9: #y] normalize nodelta #Heq1
    1080                                     <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
    1081                                     cases daemon (* axiomatise this *)
    1082                                   ]
    1083                                 ]
    1084                               | @le_n
    1085                               ]
    1086                             ]
    1087                           ]
    1088                         ]
    1089                       ]
    1090                     | #X >(not_le_to_leb_false … X)
    1091                       >(not_le_to_leb_false … (lt_to_not_le … (le_S_to_le … (not_le_to_lt … X)))) in Hind;
    1092                       normalize nodelta <(proj1 ?? (pair_destruct ?????? Heq2))
    1093                       cases instr in Heq1;
    1094                       [2,3,6: #x [3: #y] normalize nodelta #_ #H @H
    1095                       |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) #Hind
    1096                         cases daemon (* axiomatise this *)
    1097                       |1: #pi cases pi
    1098                         [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    1099                           [1,2,3,6,7,24,25: #x #y
    1100                           |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    1101                           normalize nodelta #_ #H @H
    1102                         |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    1103                           normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    1104                           #Hind cases daemon (* axiomatise this *)
    1105                         ]
    1106                       ]
    1107                     ]
    1108                   ]
    1109                 ]
    1110               | @bitvector_of_nat_abs
    1111                 [3: @lt_to_not_eq @Hi
    1112                 |1: @(transitive_lt ??? Hi)
    1113                 ]
    1114                 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    1115                 @le_S_S @le_plus_n_r
    1116               ]
    1117             | >Hi >lookup_insert_hit lapply ((proj2 ?? Hpolicy) i)
    1118             ] XXX to be continued *)
     979              [ >lookup_insert_miss
     980                [ (* USE[pass]: sigma_safe *)
     981                  lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
     982                  cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
     983                  #pc #j normalize nodelta
     984                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
     985                  #Spc #Sj normalize nodelta
     986                  cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
     987                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
     988                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
     989                    [1,4,7: *)
     990                 
    1119991  ]         
    1120992| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
  • src/ASM/Util.ma

    r2149 r2211  
    17551755  cases (lt_to_not_zero … relevant)
    17561756qed.
     1757
     1758lemma ltb_false_to_not_lt: ∀p,q:ℕ.ltb p q = false → p ≮ q.
     1759  #p #q #H @leb_false_to_not_le @H
     1760qed.
     1761
     1762lemma ltb_true_to_lt: ∀p,q:ℕ.ltb p q = true → p < q.
     1763 #p #q #H @leb_true_to_le @H
     1764qed.
     1765 
     1766lemma plus_equals_zero: ∀x,y:ℕ.x + y = x → y = 0.
     1767 #x #y cases y
     1768 [ #_ @refl
     1769 | -y #y elim x
     1770   [ <plus_O_n / by /
     1771   | -x #x #Hind #H2 @Hind normalize in H2; @injective_S @H2
     1772   ]
     1773 ]
     1774qed.
Note: See TracChangeset for help on using the changeset viewer.