source: src/utilities/lists.ma @ 1628

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

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

File size: 1.1 KB
Line 
1include "basics/lists/list.ma".
2
3(* An alternative form of All that can be easier to use sometimes. *)
4lemma 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 ⊢ (???% → ?);
8generalize 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
16let rec All2 (A,B:Type[0]) (P:A → B → Prop) (la:list A) (lb:list B) on la : Prop ≝
17match 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
23lemma 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
29lemma 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.