Ignore:
Timestamp:
Oct 19, 2011, 7:17:04 PM (8 years ago)
Author:
sacerdot
Message:
  1. fold function over BitVectorTries? moved from ERTLToLTL to ASM/BitVectorTrie
  2. ERTLToLTL now compiles again after removal of spill.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1393 r1424  
    1919  ]) (refl ? n).
    2020 @K
     21qed.
     22
     23lemma Sm_leq_n_m_leq_n:
     24  ∀m, n: nat.
     25    S m ≤ n → m ≤ n.
     26  #m #n /2/
     27qed.
     28
     29let 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 // ]
    2151qed.
    2252
     
    5787   ]
    5888 | #h #f #P #Hf #_ normalize //
     89
     90
    5991 ]
    6092qed.
     
    596628  ]
    597629] qed.
    598 
Note: See TracChangeset for help on using the changeset viewer.