Changeset 1071 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 15, 2011, 2:40:40 PM (8 years ago)
Author:
mulligan
Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1064 r1071  
    215215
    216216let rec reduce
    217   (A: Type[0]) (left: list A) (right: list A) on left ≝
     217  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝
    218218  match left with
    219219  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
     
    222222    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
    223223    | cons hd' tl' ⇒
    224       let 〈cleft, cright〉 ≝ reduce A tl tl' in
     224      let 〈cleft, cright〉 ≝ reduce A B tl tl' in
    225225      let 〈commonl, restl〉 ≝ cleft in
    226226      let 〈commonr, restr〉 ≝ cright in
     
    238238
    239239let rec reduce_strong
    240   (A: Type[0]) (left: list A) (right: list A)
    241     on left : Σret: ((list A) × (list A)) × ((list A) × (list A)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
     240  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
     241    on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
    242242  match left with
    243243  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
     
    246246    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
    247247    | cons hd' tl' ⇒
    248       let 〈cleft, cright〉 ≝ reduce_strong A tl tl' in
     248      let 〈cleft, cright〉 ≝ reduce_strong A B tl tl' in
    249249      let 〈commonl, restl〉 ≝ cleft in
    250250      let 〈commonr, restr〉 ≝ cright in
     
    255255  | 2: normalize %
    256256  | 3: normalize
    257        generalize in match (sig2 … (reduce_strong A tl tl1));
     257       generalize in match (sig2 … (reduce_strong A B tl tl1));
    258258       >p2 >p3 >p4 normalize in ⊢ (% → ?)
    259259       #HYP //
     
    464464    mapi_internal A B 0 f l.
    465465
     466let rec zip_pottier
     467  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
     468    on left ≝
     469  match left with
     470  [ nil ⇒ [ ]
     471  | cons hd tl ⇒
     472    match right with
     473    [ nil ⇒ [ ]
     474    | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl'
     475    ]
     476  ].
     477
     478let rec zip_safe
     479  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
     480    on left ≝
     481  match left return λx. |x| = |right| → list (A × B) with
     482  [ nil ⇒ λnil_prf.
     483    match right return λx. |[ ]| = |x| → list (A × B) with
     484    [ nil ⇒ λnil_nil_prf. [ ]
     485    | cons hd tl ⇒ λnil_cons_absrd. ?
     486    ] nil_prf
     487  | cons hd tl ⇒ λcons_prf.
     488    match right return λx. |hd::tl| = |x| → list (A × B) with
     489    [ nil ⇒ λcons_nil_absrd. ?
     490    | cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ?
     491    ] cons_prf
     492  ] prf.
     493  [ 1: normalize in nil_cons_absrd;
     494       destruct(nil_cons_absrd)
     495  | 2: normalize in cons_nil_absrd;
     496       destruct(cons_nil_absrd)
     497  | 3: normalize in cons_cons_prf;
     498       @injective_S
     499       assumption
     500  ]
     501qed.
     502
    466503let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
    467504  match l with
Note: See TracChangeset for help on using the changeset viewer.