X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fext.ma;h=d07234a71190f9ce6a14eea84c380039d90657b0;hb=dd882e640319d8117644986cc0e824d1d3156c5e;hp=b933ed7b6df0d760a3dca8f45c83e64b92cd4612;hpb=f5f0e9cd26adc526ee69a693d5e10ccb47cc399e;p=helm.git

diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma
index b933ed7b6..d07234a71 100644
--- a/matita/matita/lib/lambda/ext.ma
+++ b/matita/matita/lib/lambda/ext.ma
@@ -12,118 +12,105 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/types.ma".
+include "basics/list.ma".
 
 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
 
-(* from sn.ma *****************************************************************)
+(* arithmetics ****************************************************************)
 
-(* all(P,l) holds when P holds for all members of l *)
-let rec all (P:T→Prop) l on l ≝ match l with 
-   [ nil ⇒ True
-   | cons A D ⇒ P A ∧ all P D
-   ].
+lemma arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
+#x #y #HS @nmk (elim HS) -HS /3/
+qed.
 
-(* all(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
-let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with
-   [ nil          ⇒ l2 = nil ?
-   | cons hd1 tl1 ⇒ match l2 with
-      [ nil          ⇒ False
-      | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A P tl1 tl2
-      ]
-   ].
+lemma arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
+#i #p #k #H @plus_to_minus
+>commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/
+qed.
 
-(* Appl F l generalizes App applying F to a list of arguments
- * The head of l is applied first
- *)
-let rec Appl F l on l ≝ match l with 
-   [ nil ⇒ F
-   | cons A D ⇒ Appl (App F A) D  
-   ].
+lemma arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
+#x #y #z #H @nmk (elim H) -H /3/
+qed.
 
-(* FG: do we need this? 
-definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
+lemma arith4: ∀x,y. S x ≰ y → x≠y → y < x.
+#x #y #H1 #H2 lapply (not_le_to_lt … H1) -H1 #H1 @not_eq_to_le_to_lt /2/
+qed.
 
-theorem lift_appl: ∀p,k,l,F. lift (Appl F l) p k = 
-                             Appl (lift F p k) (map … (lift0 p k) l). 
-#p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
+lemma arith5: ∀x,y. x < y → S (y - 1) ≰ x.
+#x #y #H @lt_to_not_le <minus_Sn_m /2/
 qed.
-*)
 
-(* from rc.ma *****************************************************************)
+(* lists **********************************************************************)
 
-theorem arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
-#x #y #HS @nmk (elim HS) -HS /3/
+lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
+#A #l2 #l1 elim l1 -l1; normalize //
 qed.
 
-theorem arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
-#i #p #k #H @plus_to_minus
->commutative_plus >(commutative_plus k) >associative_plus @eq_f /2/
+(* all(?,P,l) holds when P holds for all members of l *)
+let rec all (A:Type[0]) (P:A→Prop) l on l ≝ match l with 
+   [ nil        ⇒ True
+   | cons hd tl ⇒ P hd ∧ all A P tl
+   ].
+
+lemma all_hd: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀l. all … P l → P (hd … l a).
+#A #P #a #Ha #l elim l -l [ #_ @Ha | #b #l #_ #Hl elim Hl -Hl; normalize // ]
 qed.
 
-theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
-#x #y #z #H @nmk (elim H) -H /3/
+lemma all_tl: ∀A:Type[0]. ∀P:A→Prop. ∀l. all … P l →  all … P (tail … l).
+#A #P #l elim l -l // #b #l #IH #Hl elim Hl -Hl; normalize //
+qed.
+
+lemma all_nth: ∀A:Type[0]. ∀P:A→Prop. ∀a. P a → ∀i,l. all … P l → P (nth i … l a).
+#A #P #a #Ha #i elim i -i [ @all_hd // | #i #IH #l #Hl @IH /2/ ]
 qed.
 
-theorem length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
-#A #l2 #l1 (elim l1) -l1 (normalize) //
+lemma all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
+#A #P #l2 #l1 elim l1 -l1; normalize // #hd #tl #IH1 #H elim H -H /3/
 qed.
 
-theorem lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
-#i #p #k #Hik normalize >(le_to_leb_true … Hik) //
+(* all2(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
+let rec all2 (A,B:Type[0]) (P:A→B→Prop) l1 l2 on l1 ≝ match l1 with
+   [ nil          ⇒ l2 = nil ?
+   | cons hd1 tl1 ⇒ match l2 with
+      [ nil          ⇒ False
+      | cons hd2 tl2 ⇒ P hd1 hd2 ∧ all2 A B P tl1 tl2
+      ]
+   ].
+
+lemma all2_length: ∀A,B:Type[0]. ∀P:A→B→Prop. 
+                   ∀l1,l2. all2 … P l1 l2 → |l1|=|l2|.
+#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
+#x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
+#x2 #l2 #_ #H elim H -H; normalize /3/
+qed. 
+
+lemma all2_hd: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
+               ∀l1,l2. all2 … P l1 l2 → P (hd … l1 a) (hd … l2 b).
+#A #B #P #a #b #Hab #l1 elim l1 -l1 [ #l2 #H2 >H2 @Hab ]
+#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
+#x2 #l2 #_ #H elim H -H; normalize //
 qed.
 
-theorem lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
-#i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
+lemma all2_tl: ∀A,B:Type[0]. ∀P:A→B→Prop.
+               ∀l1,l2. all2 … P l1 l2 →  all2 … P (tail … l1) (tail … l2).
+#A #B #P #l1 elim l1 -l1 [ #l2 #H >H // ]
+#x1 #l1 #_ #l2 elim l2 -l2 [ #false elim false ]
+#x2 #l2 #_ #H elim H -H; normalize // 
 qed.
 
-theorem lift_app: ∀M,N,k,p.
-                  lift (App M N) k p = App (lift M k p) (lift N k p).
-// qed.
-
-theorem lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p = 
-                     Lambda (lift N k p) (lift M (k + 1) p).
-// qed.
-
-theorem lift_prod: ∀N,M,k,p.
-                   lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
-// qed.
-
-(* telescopic non-delifting substitution of l in M.
- * [this is the telescoping delifting substitution lifted by |l|]
- * Rel 0 is replaced with the head of l
- *)
-let rec substc M l on l ≝ match l with
-   [ nil ⇒ M
-   | cons A D ⇒ (lift (substc M[0≝A] D) 0 1)
-   ]. 
-
-notation "M [ l ]" non associative with precedence 90 for @{'Substc $M $l}.
-
-interpretation "Substc" 'Substc M l = (substc M l).
-
-(* this is just to test that substitution works as expected
-theorem test1: ∀A,B,C. (App (App (Rel 0) (Rel 1)) (Rel 2))[A::B::C::nil ?] = 
-                       App (App (lift A 0 1) (lift B 0 2)) (lift C 0 3).
-#A #B #C normalize 
->lift_0 >lift_0 >lift_0
->lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1>lift_lift1
-normalize
+lemma all2_nth: ∀A,B:Type[0]. ∀P:A→B→Prop. ∀a,b. P a b →
+                ∀i,l1,l2. all2 … P l1 l2 → P (nth i … l1 a) (nth i … l2 b).
+#A #B #P #a #b #Hab #i elim i -i [ @all2_hd // | #i #IH #l1 #l2 #H @IH /2/ ]
 qed.
-*)
 
-theorem substc_refl: ∀l,t. (lift t 0 (|l|))[l] = (lift t 0 (|l|)).
-#l (elim l) -l (normalize) // #A #D #IHl #t cut (S (|D|) = |D| + 1) // (**) (* eliminate cut *)
+lemma all2_append: ∀A,B,P,l2,m2. all2 A B P l2 m2 →
+                   ∀l1,m1. all2 A B P l1 m1 → all2 A B P (l1 @ l2) (m1 @ m2).
+#A #B #P #l2 #m2 #H2 #l1 (elim l1) -l1 [ #m1 #H >H @H2 ] 
+#x1 #l1 #IH1 #m2 elim m2 -m2 [ #false elim false ]
+#x2 #m2 #_ #H elim H -H /3/
 qed.
 
-theorem substc_sort: ∀n,l. (Sort n)[l] = Sort n.
-//
+lemma all2_symmetric: ∀A. ∀P:A→A→Prop. symmetric … P → symmetric … (all2 … P).
+#A #P #HP #l1 elim l1 -l1 [ #l2 #H >H // ]
+#x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
+#x2 #l2 #_ #H elim H -H /3/
 qed.
-(* FG: not needed for now 
-(* nautral terms *)
-inductive neutral: T → Prop ≝
-   | neutral_sort: ∀n.neutral (Sort n)
-   | neutral_rel: ∀i.neutral (Rel i)
-   | neutral_app: ∀M,N.neutral (App M N)
-.
-*)