Changeset 1061 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 8, 2011, 5:49:22 PM (9 years ago)
Author:
mulligan
Message:

more work, bug found, ridiculous map3 function with dep. types added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1060 r1061  
    148148      destruct(cons_prf)
    149149      assumption
     150  ]
     151qed.
     152
     153let rec map3
     154  (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D)
     155  (left: list A) (centre: list B) (right: list C)
     156  (prflc: |left| = |centre|) (prfcr: |centre| = |right|) on left ≝
     157  match left return λx. |x| = |centre| → list D with
     158  [ nil ⇒ λnil_prf.
     159    match centre return λx. |x| = |right| → list D with
     160    [ nil ⇒ λnil_nil_prf.
     161      match right return λx. |nil ?| = |x| → list D with
     162      [ nil        ⇒ λnil_nil_nil_prf. nil D
     163      | cons hd tl ⇒ λcons_nil_nil_absrd. ?
     164      ] nil_nil_prf
     165    | cons hd tl ⇒ λnil_cons_absrd. ?
     166    ] prfcr
     167  | cons hd tl ⇒ λcons_prf.
     168    match centre return λx. |x| = |right| → list D with
     169    [ nil ⇒ λcons_nil_absrd. ?
     170    | cons hd' tl' ⇒ λcons_cons_prf.
     171      match right return λx. |right| = |x| → |cons ? hd' tl'| = |x| → list D with
     172      [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ?
     173      | cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf.
     174        (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?)
     175      ] (refl ? (|right|)) cons_cons_prf
     176    ] prfcr
     177  ] prflc.
     178  [ 1: normalize in cons_nil_nil_absrd;
     179       destruct(cons_nil_nil_absrd)
     180  | 2: generalize in match nil_cons_absrd;
     181       <prfcr <nil_prf #HYP
     182       normalize in HYP;
     183       destruct(HYP)
     184  | 3: generalize in match cons_nil_absrd;
     185       <prfcr <cons_prf #HYP
     186       normalize in HYP;
     187       destruct(HYP)
     188  | 4: normalize in cons_cons_nil_absrd;
     189       destruct(cons_cons_nil_absrd)
     190  | 5: normalize in cons_cons_cons_prf;
     191       destruct(cons_cons_cons_prf)
     192       assumption
     193  | 6: generalize in match cons_cons_cons_prf;
     194       <refl_prf <prfcr <cons_prf #HYP
     195       normalize in HYP;
     196       destruct(HYP)
     197       @sym_eq assumption
    150198  ]
    151199qed.
Note: See TracChangeset for help on using the changeset viewer.