-
-let rec map3
- (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D)
- (left: list A) (centre: list B) (right: list C)
- (prflc: |left| = |centre|) (prfcr: |centre| = |right|) on left ≝
- match left return λx. |x| = |centre| → list D with
- [ nil ⇒ λnil_prf.
- match centre return λx. |x| = |right| → list D with
- [ nil ⇒ λnil_nil_prf.
- match right return λx. |nil ?| = |x| → list D with
- [ nil ⇒ λnil_nil_nil_prf. nil D
- | cons hd tl ⇒ λcons_nil_nil_absrd. ?
- ] nil_nil_prf
- | cons hd tl ⇒ λnil_cons_absrd. ?
- ] prfcr
- | cons hd tl ⇒ λcons_prf.
- match centre return λx. |x| = |right| → list D with
- [ nil ⇒ λcons_nil_absrd. ?
- | cons hd' tl' ⇒ λcons_cons_prf.
- match right return λx. |right| = |x| → |cons ? hd' tl'| = |x| → list D with
- [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ?
- | cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf.
- (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?)
- ] (refl ? (|right|)) cons_cons_prf
- ] prfcr
- ] prflc.
- [ 1: normalize in cons_nil_nil_absrd;
- destruct(cons_nil_nil_absrd)
- | 2: generalize in match nil_cons_absrd;
- \ 5prfcr\ 6\ 5nil_prf #hyp="" normalize="" hyp;="" destruct(hyp)="" |="" 3:="" generalize="" in="" match="" cons_nil_absrd;=""\ 6\ 5prfcr\ 6\ 5cons_prf #hyp="" hyp;="" destruct(hyp)="" 4:="" cons_cons_nil_absrd;="" destruct(cons_cons_nil_absrd)="" 5:="" normalize="" destruct(cons_cons_cons_prf)="" assumption="" |="" 6:="" generalize="" in="" match="" cons_cons_cons_prf;=""\ 6\ 5refl_prf\ 6\ 5prfcr\ 6\ 5cons_prf #hyp="" normalize="" hyp;="" destruct(hyp)="" @sym_eq="" assumption="" ]="" lemma="" eq_rect_type0_r="" :="" ∀a:="" ∀a:a.="" ∀p:="" ∀x:a.="" eq="" type[0].="" (refl="" a="" →="" ∀x:="" a.∀p:eq="" ?="" a.="" x="" p.="" #a="" #h="" #x="" #p="" h="" generalize="" in="" match="" cases="" p="" qed.="" let="" rec="" safe_nth="" (a:="" type[0])="" (n:="" nat)="" (l:="" list="" a)="" (p:="" n=""\ 6< length A l) on n: A ≝
- match n return λo. o < length A l → A with
- [ O ⇒
- match l return λm. 0 < length A m → A with
- [ nil ⇒ λabsd1. ?
- | cons hd tl ⇒ λprf1. hd
- ]
- | S n' ⇒
- match l return λm. S n' < length A m → A with
- [ nil ⇒ λabsd2. ?
- | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
- ]
- ] ?.
- [ 1:
- @ p
- | 4:
- normalize in prf2
- normalize
- @ le_S_S_to_le
- assumption
- | 2:
- normalize in absd1;
- cases (not_le_Sn_O O)
- # H
- elim (H absd1)
- | 3:
- normalize in absd2;
- cases (not_le_Sn_O (S n'))
- # H
- elim (H absd2)
- ]
-qed.