Changeset 1516 for src/ASM/Vector.ma


Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (9 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r1330 r1516  
    6060    ]) lt.
    6161    [ cases (not_le_Sn_O O)
    62       normalize in absd1
     62      normalize in absd1;
    6363      # H
    6464      cases (H absd1)
    6565    | cases (not_le_Sn_O (S o))
    66       normalize in prf
     66      normalize in prf;
    6767      # H
    6868      cases (H prf)
    6969    | normalize
    70       normalize in prf
     70      normalize in prf;
    7171      @ le_S_S_to_le
    7272      assumption
     
    474474  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
    475475  ] P v.
    476 #A #n #P #v generalize in match P cases v normalize //
     476#A #n #P #v lapply P cases v normalize //
    477477qed.
    478478
     
    487487  normalize /2/
    488488| #m #h #t #IH #y @(vector_inv_n … y)
    489   #h' #t' #Ht #Hf whd in ⊢ (?%)
     489  #h' #t' #Ht #Hf whd in ⊢ (?%);
    490490  @(f_elim ? h h') #Eh
    491491  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
     
    497497#A #f #f_true #n #v elim v
    498498[ //
    499 | #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl
     499| #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl
    500500] qed.
    501501
     
    508508[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
    509509| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
    510   #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/
     510  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
    511511] qed.
    512512
Note: See TracChangeset for help on using the changeset viewer.