Changeset 2767 for src/ASM/BitVectorTrie.ma
 Timestamp:
 Mar 3, 2013, 2:03:58 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r2028 r2767 710 710 ] 711 711 ] qed. 712 713 include "basics/deqsets.ma". 714 715 definition 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 718 definition strong_decidable: Prop → Type[0] ≝ 719 λP:Prop. P + ¬ P. 720 721 lemma 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 ] 734 qed. 735 736
Note: See TracChangeset
for help on using the changeset viewer.