Ignore:
Timestamp:
Dec 5, 2010, 11:54:59 PM (9 years ago)
Author:
sacerdot
Message:

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

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

Legend:

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

    r370 r374  
    9595nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : Bool ≝
    9696 match l return λm.λ_:Vector addressing_mode_tag m.Bool with
    97   [ Empty ⇒ false
    98   | Cons m he (tl: Vector addressing_mode_tag m) ⇒
     97  [ VEmpty ⇒ false
     98  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
    9999     is_a he A ∨ is_in ? tl A ].
    100100
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r359 r374  
    8282  λn: Nat.
    8383  λb: Bool.
    84     ? (pad (S n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
    85   nrewrite > plus_minus_inverse_right
    86    [ napply (λx.x) | /2/]
     84   (pad (S n - (S Z)) (S Z) [[b]])⌈(S n - (S Z)) + S Z ↦ S n⌉.
     85 /2/.
    8786nqed.
    8887
     
    105104  λb, c: BitVector n.
    106105    full_add n b c false.
    107 
  • Deliverables/D4.1/Matita/BitVector.ma

    r362 r374  
    205205  let difference ≝ n - size in
    206206   less_than_or_equal_b_elim …
    207     (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector n ↦ BitVector (difference+size)⌉))
     207    (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉))
    208208    (λH:¬(size ≤ n). max n).
    209209 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.
     
    212212nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
    213213  match b with
    214     [ Empty ⇒ Z
    215     | Cons o hd tl ⇒
     214    [ VEmpty ⇒ Z
     215    | VCons o hd tl ⇒
    216216      let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z ] in
    217217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
  • Deliverables/D4.1/Matita/BitVectorTrie.ma

    r357 r374  
    1212       : A ≝
    1313  (match b return λx.λ_. x = n → A with
    14     [ Empty ⇒
     14    [ VEmpty ⇒
    1515      (match t return λx.λ_. Z = x → A with
    1616        [ Leaf l ⇒ λ_.l
     
    1818        | Stub s ⇒ λ_.a
    1919        ])
    20     | Cons o hd tl ⇒
     20    | VCons o hd tl ⇒
    2121      match t return λx.λ_. (S o) = x → A with
    2222        [ Leaf l ⇒ λK.⊥
    2323        | Node h l r ⇒
    2424           match hd with
    25              [ true ⇒ λK. lookup A h (tl⌈h ↦ o⌉) r a
    26              | false ⇒ λK. lookup A h (tl⌈h ↦ o⌉) l a
     25             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
     26             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
    2727             ]
    2828        | Stub s ⇒ λ_. a
     
    3636       : BitVectorTrie A n ≝
    3737   match b with
    38     [ Empty ⇒ Leaf A a
    39     | Cons o hd tl ⇒
     38    [ VEmpty ⇒ Leaf A a
     39    | VCons o hd tl ⇒
    4040      match hd with
    4141        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
     
    4848                 BitVectorTrie A n → BitVectorTrie A n ≝
    4949  (match b with
    50     [ Empty ⇒ λ_. Leaf A a
    51     | Cons o hd tl ⇒ λt.
     50    [ VEmpty ⇒ λ_. Leaf A a
     51    | VCons o hd tl ⇒ λt.
    5252          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
    5353            [ Leaf l ⇒ λprf.⊥
    5454            | Node p l r ⇒ λprf.
    5555               match hd with
    56                 [ true ⇒  Node A o (l⌈o ↦ p⌉) (insert A o tl a (r⌈o ↦ p⌉))
    57                 | false ⇒ Node A o (insert A o tl a (l⌈o ↦ p⌉)) (r⌈o ↦ p⌉)
     56                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
     57                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
    5858                ]
    59             | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (Cons ? o hd tl) a)
     59            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
    6060            ] (refl ? (S o))
    6161    ]).
  • Deliverables/D4.1/Matita/DoTest.ma

    r372 r374  
    55ndefinition testmem ≝ assembly test.
    66ndefinition teststatus ≝ load testmem initialise_status.
    7 ndefinition testfinal ≝ execute (four * two_hundred_and_fifty_six) teststatus.
     7ndefinition testfinal ≝ execute four (*(four * two_hundred_and_fifty_six)*) teststatus.
    88
    99notation "'STATUS'" with precedence 90 for @{ 'status }.
    1010interpretation "status" 'status = (mk_Status ??????????).
    1111
    12 (*
    13 nlemma xoo: testfinal = testfinal.
    14  nnormalize in ⊢ (??%?); @;
    15 nqed.
    16 *)
     12nlet rec execute_trace (n: Nat) (s: Status) on n: List ? ≝
     13  match n with
     14    [ Z ⇒ []
     15    | S o ⇒
     16       first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s)
     17    ].
    1718
    18 (*
    19 nlemma test:
    20  (let status ≝
    21  load
    22   (assembly [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]])])
    23    initialise_status
    24   in
    25    fetch (code_memory status) (program_counter status)
    26   ) = ?.
    27 ##[ nnormalize in ⊢ (??%?);
    28 *)
     19interpretation "left" 'left x = (Left ?? x).
     20interpretation "right" 'right x = (Right ?? x).
    2921
    30 (*
    31 nlemma xoo:
    32  (let testfinal ≝ testfinal in
    33  first … (first … (fetch (code_memory testfinal) (program_counter testfinal)))) =
    34  first … (first … (fetch (code_memory testfinal) (program_counter testfinal))).
    35  nnormalize in ⊢ (??%?);
    36 nqed.
     22notation < "'L' x" with precedence 70 for @{ 'left $x }.
     23notation < "'R' x" with precedence 70 for @{ 'right $x }.
    3724
    38 ndefinition is_JZ ≝
    39  λi: instruction.match i with
    40      [ Jump arg ⇒
    41         match arg with
    42          [ JZ arg ⇒
    43             match arg with
    44              [ RELATIVE arg ⇒ arg
    45              | _ ⇒ zero eight ]
    46          | _ ⇒ zero eight ]
    47      | _ ⇒ zero eight ].
     25notation < "𝟘" with precedence 90 for @{ 'zero }.
     26notation < "𝟙" with precedence 90 for @{ 'one }.
     27notation < "𝟚" with precedence 90 for @{ 'two }.
     28notation < "𝟛" with precedence 90 for @{ 'three }.
     29notation < "𝟜" with precedence 90 for @{ 'four }.
     30notation < "𝟝" with precedence 90 for @{ 'five }.
     31notation < "𝟞" with precedence 90 for @{ 'six }.
     32notation < "𝟟" with precedence 90 for @{ 'seven }.
     33notation < "𝟠" with precedence 90 for @{ 'eight }.
     34notation < "𝟡" with precedence 90 for @{ 'nine }.
     35notation < "𝔸" with precedence 90 for @{ 'a }.
     36notation < "𝔹" with precedence 90 for @{ 'b }.
     37notation < "∁" with precedence 90 for @{ 'c }.
     38notation < "𝔻" with precedence 90 for @{ 'd }.
     39notation < "𝔼" with precedence 90 for @{ 'e }.
     40notation < "𝔽" with precedence 90 for @{ 'f }.
     41
     42
     43interpretation "zero" 'zero = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))).
     44interpretation "one" 'one = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))).
     45interpretation "two" 'two = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))).
     46interpretation "three" 'three = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))).
     47interpretation "four" 'four = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))).
     48interpretation "five" 'five = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))).
     49interpretation "six" 'six = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))).
     50interpretation "seven" 'seven = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))).
     51interpretation "eight" 'eight = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? false (VEmpty ?))))).
     52interpretation "nine" 'nine = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ?? true (VEmpty ?))))).
     53interpretation "A" 'a = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? false (VEmpty ?))))).
     54interpretation "B" 'b = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ?? true (VEmpty ?))))).
     55interpretation "C" 'c = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? false (VEmpty ?))))).
     56interpretation "D" 'd = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ?? true (VEmpty ?))))).
     57interpretation "E" 'e = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? false (VEmpty ?))))).
     58interpretation "F" 'f = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ?? true (VEmpty ?))))).
     59
     60notation < "𝟘l" with precedence 90 for @{ 'zero4 $l }.
     61notation < "𝟙l" with precedence 90 for @{ 'one4 $l }.
     62notation < "𝟚l" with precedence 90 for @{ 'two4 $l }.
     63notation < "𝟛l" with precedence 90 for @{ 'three4 $l }.
     64notation < "𝟜l" with precedence 90 for @{ 'four4 $l }.
     65notation < "𝟝l" with precedence 90 for @{ 'five4 $l }.
     66notation < "𝟞l" with precedence 90 for @{ 'six4 $l }.
     67notation < "𝟟l" with precedence 90 for @{ 'seven4 $l }.
     68notation < "𝟠l" with precedence 90 for @{ 'eight4 $l }.
     69notation < "𝟡l" with precedence 90 for @{ 'nine4 $l }.
     70notation < "𝔸l" with precedence 90 for @{ 'a4 $l }.
     71notation < "𝔹l" with precedence 90 for @{ 'b4 $l }.
     72notation < "∁l" with precedence 90 for @{ 'c4 $l }.
     73notation < "𝔻l" with precedence 90 for @{ 'd4 $l }.
     74notation < "𝔼l" with precedence 90 for @{ 'e4 $l }.
     75notation < "𝔽l" with precedence 90 for @{ 'f4 $l }.
     76
     77interpretation "zero4" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
     78interpretation "one4" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
     79interpretation "two4" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
     80interpretation "three4" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
     81interpretation "four4" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
     82interpretation "five4" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
     83interpretation "six4" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
     84interpretation "seven4" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
     85interpretation "eight4" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
     86interpretation "nine4" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
     87interpretation "A4" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
     88interpretation "B4" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
     89interpretation "C4" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) false l)))).
     90interpretation "D4" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S Z)))) true l)))).
     91interpretation "E4" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) false l)))).
     92interpretation "F4" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S Z)))) true l)))).
     93
     94interpretation "zero8" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     95interpretation "one8" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     96interpretation "two8" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     97interpretation "three8" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     98interpretation "four8" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     99interpretation "five8" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     100interpretation "six8" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     101interpretation "seven8" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     102interpretation "eight8" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     103interpretation "nine8" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     104interpretation "A8" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     105interpretation "B8" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     106interpretation "C8" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     107interpretation "D8" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     108interpretation "E8" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) false l)))).
     109interpretation "F8" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S Z)))))))) true l)))).
     110
     111interpretation "zero16" 'zero4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
     112interpretation "one16" 'one4 l = (VCons ?? false (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     113interpretation "two16" 'two4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
     114interpretation "three16" 'three4 l = (VCons ?? false (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     115interpretation "four16" 'four4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
     116interpretation "five16" 'five4 l = (VCons ?? false (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     117interpretation "six16" 'six4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
     118interpretation "seven16" 'seven4 l = (VCons ?? false (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     119interpretation "eight16" 'eight4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
     120interpretation "nine16" 'nine4 l = (VCons ?? true (VCons ?? false (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     121interpretation "A16" 'a4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
     122interpretation "B16" 'b4 l = (VCons ?? true (VCons ?? false (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     123interpretation "C16" 'c4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
     124interpretation "D16" 'd4 l = (VCons ?? true (VCons ?? true (VCons ?? false (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     125interpretation "E16" 'e4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) false l)))).
     126interpretation "F16" 'f4 l = (VCons ?? true (VCons ?? true (VCons ?? true (VCons ? (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))) true l)))).
     127
     128notation < "…" with precedence 90 for @{ 'hide }.
     129interpretation "[[relative]]" 'hide = (VCons ?? relative (VEmpty ?)).
    48130
    49131nlemma xoo:
    50  (let testfinal ≝ testfinal in
    51    is_JZ
    52     (first … (first … (fetch (code_memory testfinal) (program_counter testfinal))))
    53     )
    54   = zero eight.
     132 execute_trace one_hundred_and_twenty_eight teststatus =
     133 execute_trace four teststatus.
    55134 nnormalize in ⊢ (??%?);
    56 
    57 *)
    58 
     135(* nnormalize in ⊢ (???%);
     136 @.
     137nqed.
    59138
    60139nlemma xoo: program_counter testfinal = program_counter testfinal.
     
    63142 @.
    64143nqed.
     144*)
  • Deliverables/D4.1/Matita/Interpret.ma

    r372 r374  
    255255            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    256256            let new_cy_flag ≝ get_index' ? Z ? old_acc in
    257             let new_acc ≝ shift_left ? eight one old_acc old_cy_flag in
     257            let new_acc ≝ shift_left one old_acc old_cy_flag in
    258258            let s ≝ set_arg_1 s CARRY new_cy_flag in
    259259              set_8051_sfr s SFR_ACC_A new_acc
     
    262262            let old_acc ≝ get_8051_sfr s SFR_ACC_A in
    263263            let new_cy_flag ≝ get_index' ? seven ? old_acc in
    264             let new_acc ≝ shift_right ? eight one old_acc old_cy_flag in
     264            let new_acc ≝ shift_right one old_acc old_cy_flag in
    265265            let s ≝ set_arg_1 s CARRY new_cy_flag in
    266266              set_8051_sfr s SFR_ACC_A new_acc
  • Deliverables/D4.1/Matita/Plogic/equality.ma

    r328 r374  
    1818    refl: eq A x x.
    1919
    20 notation "hvbox(t⌈h ↦ o⌉)"
     20notation "hvbox(t⌈o ↦ h⌉)"
    2121  with precedence 45
    2222  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
  • Deliverables/D4.1/Matita/Vector.ma

    r373 r374  
    1212
    1313ninductive Vector (A: Type[0]): Nat → Type[0] ≝
    14   Empty: Vector A Z
    15 | Cons: ∀n: Nat. A → Vector A n → Vector A (S n).
     14  VEmpty: Vector A Z
     15| VCons: ∀n: Nat. A → Vector A n → Vector A (S n).
    1616
    1717(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    2727  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.
    2828
    29 interpretation "Vector vnil" 'vnil = (Empty ?).
    30 interpretation "Vector vcons" 'vcons hd tl = (Cons ? ? hd tl).
     29interpretation "Vector vnil" 'vnil = (VEmpty ?).
     30interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl).
    3131
    3232notation "hvbox(l break !!! break n)"
     
    4343    [ Z ⇒
    4444      match v return λx.λ_. Z < x → A with
    45         [ Empty ⇒ λabsd1: Z < Z. ?
    46         | Cons p hd tl ⇒ λprf1: Z < S p. hd
     45        [ VEmpty ⇒ λabsd1: Z < Z. ?
     46        | VCons p hd tl ⇒ λprf1: Z < S p. hd
    4747        ]
    4848    | S o ⇒
    4949      (match v return λx.λ_. S o < x → A with
    50         [ Empty ⇒ λprf: S o < Z. ?
    51         | Cons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
     50        [ VEmpty ⇒ λprf: S o < Z. ?
     51        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
    5252        ])
    5353    ]) lt.
     
    7373    [ Z ⇒
    7474      match v with
    75         [ Empty ⇒ Nothing A
    76         | Cons p hd tl ⇒ Just A hd
     75        [ VEmpty ⇒ Nothing A
     76        | VCons p hd tl ⇒ Just A hd
    7777        ]
    7878    | S o ⇒
    7979      match v with
    80         [ Empty ⇒ Nothing A
    81         | Cons p hd tl ⇒ get_index_weak_v A p tl o
     80        [ VEmpty ⇒ Nothing A
     81        | VCons p hd tl ⇒ get_index_weak_v A p tl o
    8282        ]
    8383    ].
     
    8989    [ Z ⇒
    9090      match v return λx.λ_. Z < x → Vector A x with
    91         [ Empty ⇒ λabsd1: Z < Z. Empty A
    92         | Cons p hd tl ⇒ λprf1: Z < S p. (a ::: tl)
     91        [ VEmpty ⇒ λabsd1: Z < Z. [[ ]]
     92        | VCons p hd tl ⇒ λprf1: Z < S p. (a ::: tl)
    9393        ]
    9494    | S o ⇒
    9595      (match v return λx.λ_. S o < x → Vector A x with
    96         [ Empty ⇒ λprf: S o < Z. Empty A
    97         | Cons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
     96        [ VEmpty ⇒ λprf: S o < Z. [[ ]]
     97        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
    9898        ])
    9999    ]) lt.
     
    107107    [ Z ⇒
    108108      match v with
    109         [ Empty ⇒ Nothing (Vector A n)
    110         | Cons o hd tl ⇒ Just (Vector A n) (? (Cons A o a tl))
     109        [ VEmpty ⇒ Nothing (Vector A n)
     110        | VCons o hd tl ⇒ Just (Vector A n) (? (VCons A o a tl))
    111111        ]
    112112    | S o ⇒
    113113      match v with
    114         [ Empty ⇒ Nothing (Vector A n)
    115         | Cons p hd tl ⇒
     114        [ VEmpty ⇒ Nothing (Vector A n)
     115        | VCons p hd tl ⇒
    116116            let settail ≝ set_index_weak A p tl o a in
    117117              match settail with
    118118                [ Nothing ⇒ Nothing (Vector A n)
    119                 | Just j ⇒ Just (Vector A n) (? (Cons A p hd j))
     119                | Just j ⇒ Just (Vector A n) (? (VCons A p hd j))
    120120                ]
    121121        ]
     
    130130    | S o ⇒
    131131      match v with
    132         [ Empty ⇒ Nothing (Vector A n)
    133         | Cons p hd tl ⇒ ? (drop A p tl o)
     132        [ VEmpty ⇒ Nothing (Vector A n)
     133        | VCons p hd tl ⇒ ? (drop A p tl o)
    134134        ]
    135135    ].
     
    144144  | S m' ⇒ λv.
    145145     match v return λl.λ_:Vector A l.l = S (m' + n) → (Vector A (S m')) × (Vector A n) with
    146       [ Empty ⇒ λK.⊥
    147       | Cons o he tl ⇒ λK.
    148          match split A m' n (tl⌈Vector A (m'+n)↦Vector A o⌉) with
     146      [ VEmpty ⇒ λK.⊥
     147      | VCons o he tl ⇒ λK.
     148         match split A m' n (tl⌈Vector A o↦Vector A (m'+n)⌉) with
    149149          [ mk_Cartesian v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].
    150150// [ ndestruct | nlapply (S_inj … K); //]
     
    154154≝ λA,n,v.
    155155 match v return λl.λ_:Vector A l.l = S n → A × (Vector A n) with
    156   [ Empty ⇒ λK.⊥
    157   | Cons o he tl ⇒ λK. 〈he,(tl⌈Vector A n ↦ Vector A o⌉)〉
     156  [ VEmpty ⇒ λK.⊥
     157  | VCons o he tl ⇒ λK. 〈he,(tl⌈Vector A o ↦ Vector A n⌉)〉
    158158  ] (? : S ? = S ?).
    159159// [ ndestruct | nlapply (S_inj … K); //]
     
    170170                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
    171171  match v with
    172     [ Empty ⇒ x
    173     | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
     172    [ VEmpty ⇒ x
     173    | VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
    174174    ].
    175175
     
    178178                      (v: Vector A n) (q: Vector B n) on v : C n ≝
    179179  (match v return λx.λ_. x = n → C n with
    180     [ Empty ⇒
     180    [ VEmpty ⇒
    181181      match q return λx.λ_. Z = x → C x with
    182         [ Empty ⇒ λprf: Z = Z. c
    183         | Cons o hd tl ⇒ λabsd. ⊥
    184         ]
    185     | Cons o hd tl ⇒
     182        [ VEmpty ⇒ λprf: Z = Z. c
     183        | VCons o hd tl ⇒ λabsd. ⊥
     184        ]
     185    | VCons o hd tl ⇒
    186186      match q return λx.λ_. S o = x → C x with
    187         [ Empty ⇒ λabsd: S o = Z. ⊥
    188         | Cons p hd' tl' ⇒ λprf: S o = S p.
    189            (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B o ↦ Vector B p⌉)))⌈C (S p) ↦ C (S o)⌉
     187        [ VEmpty ⇒ λabsd: S o = Z. ⊥
     188        | VCons p hd' tl' ⇒ λprf: S o = S p.
     189           (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B p ↦ Vector B o⌉)))⌈C (S o) ↦ C (S p)⌉
    190190        ]
    191191    ]) (refl ? n).
     
    196196                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
    197197  match v with
    198     [ Empty ⇒ x
    199     | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
     198    [ VEmpty ⇒ x
     199    | VCons n hd tl ⇒ f (fold_left A B n f x tl) hd
    200200    ].
    201201   
     
    207207             (f: A → B) (v: Vector A n) on v ≝
    208208  match v with
    209     [ Empty ⇒ Empty B
    210     | Cons n hd tl ⇒ (f hd) ::: (map A B n f tl)
     209    [ VEmpty ⇒ [[ ]]
     210    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
    211211    ].
    212212
     
    214214             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
    215215  (match v return (λx.λr. x = n → Vector C x) with
    216     [ Empty ⇒ λ_. Empty C
    217     | Cons n hd tl ⇒
     216    [ VEmpty ⇒ λ_. [[ ]]
     217    | VCons n hd tl ⇒
    218218      match q return (λy.λr. S n = y → Vector C (S n)) with
    219         [ Empty ⇒ ?
    220         | Cons m hd' tl' ⇒
     219        [ VEmpty ⇒ ?
     220        | VCons m hd' tl' ⇒
    221221            λe: S n = S m.
    222222              (f hd hd') ::: (zip_with A B C n f tl ?)
     
    247247nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝
    248248  match n return λn. Vector A n with
    249     [ Z ⇒ Empty A
     249    [ Z ⇒ [[ ]]
    250250    | S m ⇒ h ::: (replicate A m h)
    251251    ].
     
    254254                (v: Vector A n) (q: Vector A m) on v ≝
    255255  match v return (λn.λv. Vector A (n + m)) with
    256     [ Empty ⇒ q
    257     | Cons o hd tl ⇒ hd ::: (append A o m tl q)
     256    [ VEmpty ⇒ q
     257    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
    258258    ].
    259259   
     
    268268  a :::
    269269    (match v with
    270        [ Empty ⇒ Empty A
    271        | Cons o hd tl ⇒ scan_left A B o f (f a hd) tl
     270       [ VEmpty ⇒ VEmpty A
     271       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
    272272       ]).
    273273
     
    275275                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
    276276  match v with
    277     [ Empty ⇒ ?
    278     | Cons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
     277    [ VEmpty ⇒ ?
     278    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
    279279    ].
    280280    //.
     
    284284(* Other manipulations.                                                       *)
    285285(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    286    
    287 nlet rec length (A: Type[0]) (n: Nat) (v: Vector A n) on v ≝
    288   match v with
    289     [ Empty ⇒ Z
    290     | Cons n hd tl ⇒ S $ length A n tl
    291     ].
    292286
    293287nlet rec reverse (A: Type[0]) (n: Nat)
    294288                 (v: Vector A n) on v ≝
    295289  match v return (λm.λv. Vector A m) with
    296     [ Empty ⇒ Empty A
    297     | Cons o hd tl ⇒ ? (append A o ? (reverse A o tl) (Cons A Z hd (Empty A)))
     290    [ VEmpty ⇒ [[ ]]
     291    | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]])
    298292    ].
    299293    nrewrite < (succ_plus ? ?).
     
    309303                        (v: Vector A n) on v ≝
    310304  match v return λn.λv. List A with
    311     [ Empty ⇒ ? (cic:/matita/ng/List/List.con(0,1,1) A)
    312     | Cons o hd tl ⇒ hd :: (list_of_vector A o tl)
    313     ].
    314     //.
    315 nqed.
     305    [ VEmpty ⇒ []
     306    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
     307    ].
    316308
    317309nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝
    318310  match l return λl. Vector A (length A l) with
    319     [ Empty ⇒ ? (cic:/matita/ng/Vector/Vector.con(0,1,1) A)
    320     | Cons hd tl ⇒ ? (hd ::: (vector_of_list A tl))
    321     ].
    322     nnormalize.
    323     //.
    324     //.
    325 nqed.
     311    [ Empty ⇒ [[ ]]
     312    | Cons hd tl ⇒ hd ::: (vector_of_list A tl)
     313    ].
    326314
    327315(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
     
    335323    | S o ⇒
    336324        match v with
    337           [ Empty ⇒ Empty A
    338           | Cons p hd tl ⇒
    339              rotate_left A (S p) o (? (append A p ? tl (Cons A ? hd (Empty A))))
     325          [ VEmpty ⇒ [[ ]]
     326          | VCons p hd tl ⇒
     327             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S Z) ↦ Vector A (S p)⌉)
    340328          ]
    341329    ].
    342     nrewrite < (succ_plus ? ?).
    343     nrewrite > (plus_zero ?).
    344     //.
     330 //.
    345331nqed.
    346332
     
    350336  λv: Vector A n.
    351337    reverse A n (rotate_left A n m (reverse A n v)).
    352    
     338
    353339ndefinition shift_left_1 ≝
    354340  λA: Type[0].
    355341  λn: Nat.
    356   λv: Vector A n.
     342  λv: Vector A (S n).
    357343  λa: A.
    358     match v with
    359       [ Empty ⇒ ?
    360       | Cons o hd tl ⇒ reverse A n (? (Cons A o a (reverse A o tl)))
    361       ].
    362       //.
     344   match v return λy.λ_. y = S n → Vector A y with
     345     [ VEmpty ⇒ λH.⊥
     346     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
     347     ] (refl ? (S n)).
     348 ndestruct.
    363349nqed.
    364350
     
    366352  λA: Type[0].
    367353  λn: Nat.
    368   λv: Vector A n.
     354  λv: Vector A (S n).
    369355  λa: A.
    370     reverse A n (shift_left_1 A n (reverse A n v) a).
     356    reverse … (shift_left_1 … (reverse … v) a).
    371357   
    372358ndefinition shift_left ≝
    373359  λA: Type[0].
    374360  λn, m: Nat.
    375   λv: Vector A n.
     361  λv: Vector A (S n).
    376362  λa: A.
    377     iterate (Vector A n) (λx. shift_left_1 A n x a) v m.
     363    iterate … (λx. shift_left_1 … x a) v m.
    378364   
    379365ndefinition shift_right ≝
    380366  λA: Type[0].
    381367  λn, m: Nat.
    382   λv: Vector A n.
     368  λv: Vector A (S n).
    383369  λa: A.
    384     iterate (Vector A n) (λx. shift_right_1 A n x a) v m.
     370    iterate … (λx. shift_right_1 … x a) v m.
    385371
    386372(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    388374(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    389375
    390 nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b
     376nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b : Bool
    391377  (match b return λx.λ_. n = x → Bool with
    392     [ Empty ⇒
     378    [ VEmpty ⇒
    393379      match c return λx.λ_. x = Z → Bool with
    394         [ Empty ⇒ λ_. true
    395         | Cons p hd tl ⇒ λabsd.?
    396         ]
    397     | Cons o hd tl ⇒
     380        [ VEmpty ⇒ λ_. true
     381        | VCons p hd tl ⇒ λabsd.⊥
     382        ]
     383    | VCons o hd tl ⇒
    398384        match c return λx.λ_. x = S o → Bool with
    399           [ Empty ⇒ λabsd. ?
    400           | Cons p hd' tl' ⇒
     385          [ VEmpty ⇒ λabsd.⊥
     386          | VCons p hd' tl' ⇒
    401387            λprf.
    402388              if (f hd hd') then
    403                 (eq_v A o f tl ?)
     389                (eq_v A o f tl (tl'⌈Vector A p ↦ Vector A o⌉))
    404390              else
    405391                false
     
    407393    ]) (refl ? n).
    408394    ##[##1,2: ndestruct
    409       | nlapply (S_inj … prf); #X; nrewrite < X;
    410         napply tl' ]
     395      | nlapply (S_inj … prf); #X; nrewrite < X; @]
    411396nqed.
    412397
     
    452437  @.
    453438nqed.
    454 
    455 nlemma length_correct:
    456   ∀A: Type[0].
    457   ∀n: Nat.
    458   ∀v: Vector A n.
    459     length A n v = n.
    460   #A n v.
    461   nelim v.
    462   nnormalize.
    463   @.
    464   #N H V H2.
    465   nnormalize.
    466   nrewrite > H2.
    467   @.
    468 nqed.
    469 
    470 nlemma map_length:
    471   ∀A, B: Type[0].
    472   ∀n: Nat.
    473   ∀v: Vector A n.
    474   ∀f: A → B.
    475     length A n v = length B n (map A B n f v).
    476   #A B n v f.
    477   nelim v.
    478   nnormalize.
    479   @.
    480   #N H V H2.
    481   nnormalize.
    482   nrewrite > H2.
    483   @.
    484 nqed.
Note: See TracChangeset for help on using the changeset viewer.