Changeset 1057 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 5, 2011, 5:53:11 PM (8 years ago)
Author:
mulligan
Message:

changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r998 r1057  
    88example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
    99example not_implemented: False. cases daemon qed.
     10 
     11let rec map2_opt
     12  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
     13  (left: list A) (right: list B) on left ≝
     14  match left with
     15  [ nil ⇒
     16    match right with
     17    [ nil ⇒ Some ? (nil C)
     18    | _ ⇒ None ?
     19    ]
     20  | cons hd tl ⇒
     21    match right with
     22    [ nil ⇒ None ?
     23    | cons hd' tl' ⇒
     24      match map2_opt A B C f tl tl' with
     25      [ None ⇒ None ?
     26      | Some tail ⇒ Some ? (f hd hd' :: tail)
     27      ]
     28    ]
     29  ].
     30
     31let rec map2
     32  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
     33  (left: list A) (right: list B) (proof: | left | = | right |) on left ≝
     34  match left return λx. | x | = | right | → list C with
     35  [ nil ⇒
     36    match right return λy. | [] | = | y | → list C with
     37    [ nil ⇒ λnil_prf. nil C
     38    | _ ⇒ λcons_absrd. ?
     39    ]
     40  | cons hd tl ⇒
     41    match right return λy. | hd::tl | = | y | → list C with
     42    [ nil ⇒ λnil_absrd. ?
     43    | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ?
     44    ]
     45  ] proof.
     46  [1: normalize in cons_absrd;
     47      destruct(cons_absrd)
     48  |2: normalize in nil_absrd;
     49      destruct(nil_absrd)
     50  |3: normalize in cons_prf;
     51      destruct(cons_prf)
     52      assumption
     53  ]
     54qed.
    1055 
    1156lemma eq_rect_Type0_r :
Note: See TracChangeset for help on using the changeset viewer.