source: src/utilities/lists.ma @ 1626

Last change on this file since 1626 was 1626, checked in by campbell, 9 years ago

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File size: 727 bytes
Line 
1include "basics/lists/list.ma".
2
3let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
4match la with
5[ nil ⇒ match lb with [ nil ⇒ True | _ ⇒ False ]
6| cons ha ta ⇒
7    match lb with [ nil ⇒ False | cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ]
8].
9
10lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → |la| = |lb|.
11#A #B #P #la elim la
12[ * [ // | #x #y * ]
13| #ha #ta #IH * [ * | #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl
14] qed.
15
16lemma All2_mp : ∀A,B,P,Q,la,lb. (∀a,b. P a b → Q a b) → All2 A B P la lb → All2 A B Q la lb.
17#A #B #P #Q #la elim la
18[ * [ // | #h #t #_ * ]
19| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
20] qed.
Note: See TracBrowser for help on using the repository browser.