Ignore:
Timestamp:
Mar 3, 2013, 2:03:58 PM (7 years ago)
Author:
mckinna
Message:

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r2028 r2767  
    710710  ]
    711711] qed.
     712
     713include "basics/deqsets.ma".
     714
     715definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
     716 λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a.
     717
     718definition strong_decidable: Prop → Type[0] ≝
     719 λP:Prop. P + ¬ P.
     720
     721lemma strong_decidable_in_codomain:
     722 ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A.
     723  strong_decidable (in_codomain A n m a).
     724 #A #n #m elim m
     725 [ normalize #a' #a inversion (a' == a) #H
     726   [ %1 %{(VEmpty …)} >(\P H) %
     727   | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ]
     728 | -n #n #L #R #Hl #Hr #a
     729   cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl
     730   cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)}  <H % ] #Hr
     731   %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?);
     732   normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/
     733 | #n #A %2 % * #x normalize #abs destruct ]
     734qed.
     735
     736
Note: See TracChangeset for help on using the changeset viewer.