Ignore:
Timestamp:
Nov 26, 2010, 5:32:34 PM (9 years ago)
Author:
mulligan
Message:

Decidable equality on vectors and its specialisation to bitvectors.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Vector.ma

    r311 r315  
    362362  λa: A.
    363363    iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
     364
     365(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     366(* Decidable equality.                                                        *)
     367(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     368
     369nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b ≝
     370  (match b return λx.λ_. n = x → Bool with
     371    [ Empty ⇒
     372      match c return λx.λ_. x = Z → Bool with
     373        [ Empty ⇒ λ_. true
     374        | Cons p hd tl ⇒ λabsd.?
     375        ]
     376    | Cons o hd tl ⇒
     377        match c return λx.λ_. x = S o → Bool with
     378          [ Empty ⇒ λabsd. ?
     379          | Cons p hd' tl' ⇒
     380            λprf.
     381              if (f hd hd') then
     382                (eq_v A o f tl ?)
     383              else
     384                false
     385          ]
     386    ]) (refl ? n).
     387    ##[##1, 3:
     388        ndestruct (absd);
     389        ndestruct (prf);
     390        napply tl';
     391    ##|##2:
     392        ndestruct (absd);
     393    ##]
     394nqed.
    364395   
    365396(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.