Changeset 315


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

Decidable equality on vectors and its specialisation to bitvectors.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r314 r315  
    185185nqed.
    186186
     187ndefinition eq_bv ≝
     188  λn: Nat.
     189  λb, c: BitVector n.
     190    eq_v Bool n (λd, e.
     191      if inclusive_disjunction (conjunction d e) (conjunction (negation d)
     192                                                              (negation e)) then
     193        true
     194      else
     195        false) b c.
     196
    187197naxiom plus_minus_inverse_left:
    188198  ∀m, n: Nat.
  • 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.