- 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 a0d3a5ea61b2049c916c1d0ec7193957e397b255..bfe0fe3e9a53f19a18f04f82e7e6f50a0f82cbf7 100644 (file)
--- 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
 (* 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
    | 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_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.
 
 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 *)
 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 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) //
        >(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 … 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/
        [ >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| → 
 (* 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
 #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 ? ? ([?]) ?)
          >(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
      ]
    | #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
    | #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.
 
    | #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 *)
 #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 596424938e459fb0e62d51f5e8fd0bc5d13b475b..e8ca08046d97164ea86bd987624231f01bb1940b 100644 (file)
--- 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 _ [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}.