 Timestamp:
 Oct 19, 2011, 7:17:04 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1393 r1424 19 19 ]) (refl ? n). 20 20 @K 21 qed. 22 23 lemma Sm_leq_n_m_leq_n: 24 ∀m, n: nat. 25 S m ≤ n → m ≤ n. 26 #m #n /2/ 27 qed. 28 29 let rec bvtfold_aux 30 (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat) 31 on n: n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → b ≝ 32 match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16  n) → b with 33 [ O ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16. 34 match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with 35 [ Leaf l ⇒ λproof. f path l seed 36  Stub s ⇒ λproof. seed 37  Node n' l r ⇒ λabsrd. ⊥ 38 ] (refl … 0) 39  S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16  S n'). 40 match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with 41 [ Leaf l ⇒ λabsrd. ⊥ 42  Stub s ⇒ λproof. seed 43  Node n'' l r ⇒ λproof. 44 bvtfold_aux a b f (bvtfold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16  S n') ↦ 16  n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16  S n') ↦ 16  n'⌉) 45 ] (refl … (S n')) 46 ]. 47 [ 1, 2: destruct(absrd) 48  3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le // 49  4,7: destruct(proof) % 50  5,6: @Sm_leq_n_m_leq_n // ] 21 51 qed. 22 52 … … 57 87 ] 58 88  #h #f #P #Hf #_ normalize // 89 90 59 91 ] 60 92 qed. … … 596 628 ] 597 629 ] qed. 598
Note: See TracChangeset
for help on using the changeset viewer.