From 60779bad5c038c5573514800a7b50eafb45013fa Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 9 Mar 2011 21:06:55 +0000
Subject: [PATCH] more notation and all-purpose lemmas

---
 matita/matita/lib/lambda/ext.ma             | 67 +++++++++++++--------
 matita/matita/lib/lambda/lambda_notation.ma | 20 ++++--
 2 files changed, 58 insertions(+), 29 deletions(-)

diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma
index ebbd051f7..d37fb9f52 100644
--- a/matita/matita/lib/lambda/ext.ma
+++ b/matita/matita/lib/lambda/ext.ma
@@ -12,47 +12,60 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/types.ma".
+include "lambda/subst.ma".
+include "basics/list.ma".
 include "lambda/lambda_notation.ma".
 
 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
 
 (* arithmetics ****************************************************************)
 
-theorem arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
+lemma arith1: ∀x,y. (S x) ≰ (S y) → x ≰ y.
 #x #y #HS @nmk (elim HS) -HS /3/
 qed.
 
-theorem arith2: ∀i,p,k. k ≤ i → i + p - (k + p) = i - k.
+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.
 
-theorem arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
+lemma arith3: ∀x,y,z. x ≰ y → x + z ≰ y + z.
 #x #y #z #H @nmk (elim H) -H /3/
 qed.
 
-theorem arith4: ∀x,y. S x ≰ y → x≠y → y < x.
+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 arith5: ∀x,y. x < y → S (y - 1) ≰ x.
+lemma arith5: ∀x,y. x < y → S (y - 1) ≰ x.
 #x #y #H @lt_to_not_le <minus_Sn_m /2/
 qed.
 
 (* lists **********************************************************************)
 
-(* all(P,l) holds when P holds for all members of l *)
+(* 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
    ].
 
-theorem all_append: ∀A,P,l2,l1. all A P l1 → all A P l2 → all A P (l1 @ l2).
+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 // ]
+qed.
+
+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 //
+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.
+
+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) /3/
 qed.
 
-(* all(?,P,l1,l2) holds when P holds for all paired members of l1 and l2 *)
+(* all2(?,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
@@ -61,7 +74,7 @@ let rec all2 (A:Type[0]) (P:A→A→Prop) l1 l2 on l1 ≝ match l1 with
       ]
    ].
 
-theorem length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
+lemma length_append: ∀A. ∀(l2,l1:list A). |l1@l2| = |l1| + |l2|.
 #A #l2 #l1 (elim l1) -l1 (normalize) //
 qed.
 
@@ -75,7 +88,7 @@ let rec Appl F l on l ≝ match l with
    | cons A D ⇒ Appl (App F A) D  
    ].
 
-theorem appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
+lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
 #N #l (elim l) -l // #hd #tl #IHl #M >IHl //
 qed.
 
@@ -93,41 +106,45 @@ inductive neutral: T → Prop ≝
 (* FG: do we need this? 
 definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
 
-theorem lift_appl: ∀p,k,l,F. lift (Appl F l) p k = 
+lemma 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 //
 qed.
 *)
 
-theorem lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
+lemma 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) //
 qed.
 
-theorem lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
+lemma 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/
 qed.
 
-theorem lift_app: ∀M,N,k,p.
-                  lift (App M N) k p = App (lift M k p) (lift N k p).
+lemma 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).
+lemma 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).
+lemma lift_prod: ∀N,M,k,p.
+                 lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
 // qed.
 
-theorem subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
+lemma subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
 // qed.
 
-theorem subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
+lemma subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
 // qed.
 
-theorem subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
+lemma subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
 // qed.
 
+
+axiom lift_subst_lt: ∀A,B,i,j,k. lift (B[j≝A]) (j+k) i =
+                     (lift B (j+k+1) i)[j≝lift A k i].
+
 (* telescopic delifting substitution of l in M.
  * Rel 0 is replaced with the head of l
  *)
@@ -138,10 +155,10 @@ let rec tsubst M l on l ≝ match l with
 
 interpretation "telescopic substitution" 'Subst1 M l = (tsubst M l).
 
-theorem tsubst_refl: ∀l,t. (lift t 0 (|l|))[l] = t.
+lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[l] = t.
 #l (elim l) -l (normalize) // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
 qed.
 
-theorem tsubst_sort: ∀n,l. (Sort n)[l] = Sort n.
+lemma tsubst_sort: ∀n,l. (Sort n)[l] = Sort n.
 //
 qed.
diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index f7f8d9d8f..0ad437ab0 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -30,16 +30,28 @@ notation "hvbox(M break [ l ])"
    non associative with precedence 90
    for @{'Subst1 $M $l}.
 
-(* evaluation, interpretation *)
+(* interpretation *)
 
 notation "hvbox(〚term 90 T〛)"
    non associative with precedence 50
-   for @{'Eval $T}.
+   for @{'IInt $T}.
 
 notation "hvbox(〚term 90 T〛 break _ [term 90 E])"
    non associative with precedence 50
-   for @{'Eval1 $T $E}.
+   for @{'IInt1 $T $E}.
 
 notation "hvbox(〚term 90 T〛 break _ [term 90 E1 break , term 90 E2])"
    non associative with precedence 50
-   for @{'Eval2 $T $E1 $E2}.
+   for @{'IInt2 $T $E1 $E2}.
+
+notation "hvbox(《term 90 T》)"
+   non associative with precedence 50
+   for @{'EInt $T}.
+
+notation "hvbox(《term 90 T》 break _ [term 90 E])"
+   non associative with precedence 50
+   for @{'EInt1 $T $E}.
+
+notation "hvbox(《term 90 T》 break _ [term 90 E1 break , term 90 E2])"
+   non associative with precedence 50
+   for @{'EInt2 $T $E1 $E2}.
-- 
2.39.2