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  

1  include "basics/lists/list.ma". 

2  

3  let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝ 

4  match 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  

10  lemma 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  

16  lemma 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.