Last change
on this file since 1628 was
1628,
checked in by campbell, 8 years ago

Show that the universe generated by Clight/fresh.ma is good.

File size:
1.1 KB

Line  

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

2  

3  (* An alternative form of All that can be easier to use sometimes. *) 

4  lemma All_alt : ∀A,P,l. 

5  (∀a,pre,post. l = pre@a::post → P a) → 

6  All A P l. 

7  #A #P #l #H lapply (refl ? l) change with ([ ] @ l) in ⊢ (???% → ?); 

8  generalize in ⊢ (???(??%?) → ?); elim l in ⊢ (? → ???(???%) → %); 

9  [ #pre #E % 

10   #a #tl #IH #pre #E % 

11  [ @(H a pre tl E) 

12   @(IH (pre@[a])) >associative_append @E 

13  ] 

14  ] qed. 

15  

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

17  match la with 

18  [ nil ⇒ match lb with [ nil ⇒ True  _ ⇒ False ] 

19   cons ha ta ⇒ 

20  match lb with [ nil ⇒ False  cons hb tb ⇒ P ha hb ∧ All2 A B P ta tb ] 

21  ]. 

22  

23  lemma All2_length : ∀A,B,P,la,lb. All2 A B P la lb → la = lb. 

24  #A #B #P #la elim la 

25  [ * [ //  #x #y * ] 

26   #ha #ta #IH * [ *  #hb #tb * #H1 #H2 whd in ⊢ (??%%); >(IH … H2) @refl 

27  ] qed. 

28  

29  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. 

30  #A #B #P #Q #la elim la 

31  [ * [ //  #h #t #_ * ] 

32   #ha #ta #IH * [ //  #hb #tb #H * #H1 #H2 % [ @H @H1  @(IH … H2) @H ] ] 

33  ] qed. 

Note: See
TracBrowser
for help on using the repository browser.