From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 25 May 2011 12:22:16 +0000 (+0000)
Subject: - degree: some improvements and the Deg_append lemma
X-Git-Tag: make_still_working~2489
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=41c4bfe9415b1b40278878dd767b734c61a47a69;p=helm.git

- degree: some improvements and the Deg_append lemma
- lambda_notation: the K interpretation (CC to Fomega mapping)
---

diff --git a/matita/matita/lib/lambda/degree.ma b/matita/matita/lib/lambda/degree.ma
index a0d3a5ea6..bfe0fe3e9 100644
--- a/matita/matita/lib/lambda/degree.ma
+++ b/matita/matita/lib/lambda/degree.ma
@@ -21,7 +21,7 @@ include "lambda/ext_lambda.ma".
 (* degree assigned to the term t in the environment L *)
 let rec deg L t on t ≝ match t with
    [ Sort i     ⇒ i + 3
-   | Rel i      ⇒ (nth i … L 0) - 1
+   | Rel i      ⇒ (nth i … L 0)
    | App m _    ⇒ deg L m 
    | Lambda n m ⇒ let l ≝ deg L n in deg (l::L) m
    | Prod n m   ⇒ let l ≝ deg L n in deg (l::L) m
@@ -39,16 +39,16 @@ lemma deg_lambda: ∀n,m,L. ║Lambda n m║_[L] = ║m║_[║n║_[L]::L].
 lemma deg_prod: ∀n,m,L. ║Prod n m║_[L] = ║m║_[║n║_[L]::L].
 // qed.
 
-lemma deg_rel_lt: ∀LK,L,i. (S i) ≤ |L| → ║Rel i║_[L @ LK] = ║Rel i║_[L].
-#LK #L elim L -L [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
-#l #L #IHL #i elim i -i // #i #_ #Hie @IHL @le_S_S_to_le @Hie
+lemma deg_rel_lt: ∀L,K,i. (S i) ≤ |K| → ║Rel i║_[K @ L] = ║Rel i║_[K].
+#L #K elim K -K [1: #i #Hie elim (not_le_Sn_O i) #Hi elim (Hi Hie) ]
+#k #K #IHK #i elim i -i // #i #_ #Hie @IHK @le_S_S_to_le @Hie
 qed.
 
-lemma deg_rel_not_le: ∀K,L,i. (S i) ≰ |L| →
-                      ║Rel i║_[L @ K] = ║Rel (i-|L|)║_[K].
-#K #L elim L -L [ normalize // ]
-#l #L #IHL #i elim i -i [1: -IHL #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
-normalize #i #_ #Hie @IHL /2/
+lemma deg_rel_not_le: ∀L,K,i. (S i) ≰ |K| →
+                      ║Rel i║_[K @ L] = ║Rel (i-|K|)║_[L].
+#L #K elim K -K [ normalize // ]
+#k #K #IHK #i elim i -i [1: -IHK #Hie elim Hie -Hie #Hie; elim (Hie ?) /2/ ]
+normalize #i #_ #Hie @IHK /2/
 qed.
 
 (* weakeing and thinning lemma for the degree assignment *)
@@ -57,11 +57,11 @@ lemma deg_lift: ∀p,L,Lp. p = |Lp| → ∀t,k,Lk. k = |Lk| →
                 ║lift t k p║_[Lk @ Lp @ L] = ║t║_[Lk @ L].
 #p #L #Lp #HLp #t elim t -t //
    [ #i #k #Lk #HLk @(leb_elim (S i) k) #Hik
-     [ >(lift_rel_lt … Hik) >HLk in Hik #Hik
+     [ >(lift_rel_lt … Hik) >HLk in Hik -HLk #Hik
        >(deg_rel_lt … Hik) >(deg_rel_lt … Hik) //
-     | >(lift_rel_not_le … Hik) >HLk in Hik #Hik
+     | >(lift_rel_not_le … Hik) >HLk in Hik -HLk #Hik
        >(deg_rel_not_le … Hik) <associative_append
-       >(deg_rel_not_le …) >length_append >HLp;
+       >(deg_rel_not_le …) >length_append >HLp -HLp
        [ >arith2 // @not_lt_to_le /2/ | @(arith3 … Hik) ]
      ]
    | #m #n #IHm #_ #k #Lk #HLk >lift_app >deg_app /3/
@@ -80,13 +80,13 @@ qed.
 (* substitution lemma for the degree assignment *)
 (* NOTE: >commutative_plus comes from |a::b| ↦ S |b| rather than |b| + 1 *)
 lemma deg_subst: ∀v,L,t,k,Lk. k = |Lk| → 
-                 ║t[k≝v]║_[Lk @ L] = ║t║_[Lk @ ║v║_[L]+1::L].
+                 ║t[k≝v]║_[Lk @ L] = ║t║_[Lk @ ║v║_[L]::L].
 #v #L #t elim t -t //
    [ #i #k #Lk #HLk @(leb_elim (S i) k) #H1ik
      [ >(subst_rel1 … H1ik) >HLk in H1ik #H1ik
        >(deg_rel_lt … H1ik) >(deg_rel_lt … H1ik) //
      | @(eqb_elim i k) #H2ik
-       [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HLk in H1ik #H1ik
+       [ >H2ik in H1ik -H2ik i #H1ik >subst_rel2 >HLk in H1ik -HLk #H1ik
          >(deg_rel_not_le … H1ik) <minus_n_n >(deg_lift ? ? ? ? ? ? ([])) normalize //
        | lapply (arith4 … H1ik H2ik) -H1ik H2ik #Hik >(subst_rel3 … Hik)
          >deg_rel_not_le; [2: /2/ ] <(associative_append ? ? ([?]) ?)
@@ -96,23 +96,29 @@ lemma deg_subst: ∀v,L,t,k,Lk. k = |Lk| →
      ]
    | #m #n #IHm #_ #k #Lk #HLk >subst_app >deg_app /3/
    | #n #m #IHn #IHm #k #Lk #HLk >subst_lambda > deg_lambda
-     >IHn // >commutative_plus in ⊢ (??(? ? %)?) >(IHm … (? :: ?)) /2/
+     >IHn // >commutative_plus >(IHm … (? :: ?)) /2/
    | #n #m #IHn #IHm #k #Lk #HLk >subst_prod > deg_prod
-     >IHn // >commutative_plus in ⊢ (??(? ? %)?) >(IHm … (? :: ?)) /2/
+     >IHn // >commutative_plus >(IHm … (? :: ?)) /2/
    | #m #IHm #k #Lk #HLk >IHm //
    ]
 qed.
 
-lemma deg_subst_0: ∀t,v,L. ║t[0≝v]║_[L] = ║t║_[║v║_[L]+1::L].
+lemma deg_subst_0: ∀t,v,L. ║t[0≝v]║_[L] = ║t║_[║v║_[L]::L].
 #t #v #L >(deg_subst ???? ([])) //
 qed.
 
 (* The degree context  ********************************************************)
 
 (* degree context assigned to the type context G *)
-let rec Deg G ≝ match G with
-   [ nil      ⇒ nil …
-   | cons t F ⇒ let H ≝ Deg F in ║t║_[H] :: H
+let rec Deg L G on G ≝ match G with
+   [ nil      ⇒ L
+   | cons t F ⇒ let H ≝ Deg L F in ║t║_[H] - 1 :: H
    ].
 
-interpretation "degree assignment (type context)" 'IInt G = (Deg G).
+interpretation "degree assignment (type context)" 'IInt1 G L = (Deg L G).
+
+interpretation "degree assignment (type context)" 'IInt G = (Deg (nil ?) G).
+
+lemma Deg_append: ∀L,G,H. ║H @ G║_[L] = ║H║_[║G║_[L]].
+#L #G #H elim H normalize //
+qed.
diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index 596424938..e8ca08046 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -92,3 +92,7 @@ notation "hvbox(《T》 break _ [E])"
 notation "hvbox(《T》 break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'XInt2 $T $E1 $E2}.
+
+notation "hvbox(𝕂{T} break _ [E])"
+   non associative with precedence 50
+   for @{'IK1 $T $E}.