Changeset 1064 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 12, 2011, 5:52:07 PM (8 years ago)
Author:
mulligan
Message:

changes from today, nearly complete rtlabs translation pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1063 r1064  
    3333  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
    3434  ].
     35 
     36let rec fold_left2
     37  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A)
     38  (left: list B) (right: list C) (proof: |left| = |right|)
     39    on left: A ≝
     40  match left return λx. |x| = |right| → A with
     41  [ nil ⇒ λnil_prf.
     42    match right return λx. |[ ]| = |x| → A with
     43    [ nil ⇒ λnil_nil_prf. accu
     44    | cons hd tl ⇒ λcons_nil_absrd. ?
     45    ] nil_prf
     46  | cons hd tl ⇒ λcons_prf.
     47    match right return λx. |hd::tl| = |x| → A with
     48    [ nil ⇒ λcons_nil_absrd. ?
     49    | cons hd' tl' ⇒ λcons_cons_prf.
     50        fold_left2 …  f (f accu hd hd') tl tl' ?
     51    ] cons_prf
     52  ] proof.
     53  [ 1: normalize in cons_nil_absrd;
     54       destruct(cons_nil_absrd)
     55  | 2: normalize in cons_nil_absrd;
     56       destruct(cons_nil_absrd)
     57  | 3: normalize in cons_cons_prf;
     58       @injective_S
     59       assumption
     60  ]
     61qed.
    3562
    3663let rec remove_n_first_internal
     
    96123    foldi_from_until A 0 (|l|) f a l.
    97124
    98 definition hd
     125definition hd_safe
    99126  λA: Type[0].
    100127  λl: list A.
     
    103130  [ nil ⇒ λnil_absrd. ?
    104131  | cons hd tl ⇒ λcons_prf. hd
    105   ].
     132  ] proof.
    106133  normalize in nil_absrd;
    107134  cases(not_le_Sn_O 0)
     
    110137qed.
    111138
    112 definition tail
     139definition tail_safe
    113140  λA: Type[0].
    114141  λl: list A.
     
    117144  [ nil ⇒ λnil_absrd. ?
    118145  | cons hd tl ⇒ λcons_prf. tl
    119   ].
     146  ] proof.
    120147  normalize in nil_absrd;
    121148  cases(not_le_Sn_O 0)
     
    491518  [ nil ⇒ nil A
    492519  | cons hd tl ⇒ (rev A tl) @ [ hd ]
    493   ].
     520  ].
     521
     522lemma append_length:
     523  ∀A: Type[0].
     524  ∀l, r: list A.
     525    |(l @ r)| = |l| + |r|.
     526  #A #L #R
     527  elim L
     528  [ %
     529  | #HD #TL #IH
     530    normalize >IH %
     531  ]
     532qed.
     533
     534lemma append_nil:
     535  ∀A: Type[0].
     536  ∀l: list A.
     537    l @ [ ] = l.
     538  #A #L
     539  elim L //
     540qed.
     541
     542lemma rev_append:
     543  ∀A: Type[0].
     544  ∀l, r: list A.
     545    rev A (l @ r) = rev A r @ rev A l.
     546  #A #L #R
     547  elim L
     548  [ normalize >append_nil %
     549  | #HD #TL #IH
     550    normalize >IH
     551    @associative_append
     552  ]
     553qed.
     554
     555lemma rev_length:
     556  ∀A: Type[0].
     557  ∀l: list A.
     558    |rev A l| = |l|.
     559  #A #L
     560  elim L
     561  [ %
     562  | #HD #TL #IH
     563    normalize
     564    >(append_length A (rev A TL) [HD])
     565    normalize /2/
     566  ]
     567qed.
    494568   
    495569notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
Note: See TracChangeset for help on using the changeset viewer.