matita/matita/contribs/lambdadelta/basic_2/etc/ltls/ltls.etc

   1 include "basic_2/notation/functions/droppreds_3.ma".
   2 include "basic_2/grammar/lenv_length.ma".
   3
   4 axiom pred_minus: ∀x,y. y < x → ⫰(x - y) = x - ⫯y.
   5
   6 (*
   7 axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0.
   8
   9 lemma le_succ_trans: ∀m,n. ⫯m ≤ n → m ≤ n.
  10 /2 width=1 by lt_to_le/ qed-.
  11 *)
  12
  13 lemma tls_pred: ∀f,n. 0 < n → ⫱*[n] f = ⫱ ⫱*[⫰n] f.
  14 #f #n #Hn >tls_S >S_pred //
  15 qed-.
  16
  17 definition ltls (f): lenv → lenv → rtmap ≝ λL,K. ⫱*[|L|-|K|] f.
  18
  19 interpretation "ltls (rtmap)" 'DropPreds L K f = (ltls f L K).
  20
  21 lemma ltls_refl: ∀f,L1,L2. |L1| ≤ |L2| → ⫱*[L1, L2] f = f.
  22 #f #L1 #L2 #HL12 whd in ⊢ (??%?); >(eq_minus_O … HL12) -HL12 //
  23 qed.
  24
  25 lemma ltls_pair2: ∀f,I,L1,L2,V. |L2| < |L1| → ⫱⫱*[L1, L2.ⓑ{I}V] f = ⫱*[L1, L2] f.
  26 #f #I #L1 #L2 #V #HL12 whd in ⊢ (??(?%)%); <pred_minus // <tls_pred //
  27 /2 width=1 by lt_plus_to_minus_r/
  28 qed-.
  29
  30 lemma ltls_pair1_push: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ↑f = ⫱*[L1, L2] f.
  31 #f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m //
  32 qed.
  33
  34 lemma ltls_pair1_next: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ⫯f = ⫱*[L1, L2] f.
  35 #f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m //
  36 qed.
  37
  38 lemma ltls_sle_pair: ∀f1,f2,L1,L2. ⫱*[L2, L1] f2 ⊆ ⫱*[L1, L2] f1 →
  39                      ∀I,V1. ⫱*[L2, L1.ⓑ{I}V1] f2 ⊆ ⫱*[L1.ⓑ{I}V1, L2] ⫯f1.
  40 #f1 #f2 #L1 #L2 elim (lt_or_ge (|L1|) (|L2|))
  41 [ #HL12 >ltls_refl in ⊢ (??%→?); /2 width=1 by lt_to_le/
  42   #Hf21 #I #V1 >ltls_refl in ⊢ (??%); //
  43   <(ltls_pair2 … I … V1 HL12) in Hf21; -HL12 /2 width=1 by sle_inv_tl1/
  44 | #HL21 >ltls_refl // #Hf21 #I #V1 >ltls_refl /2 width=1 by le_S/
  45   >ltls_pair1_next //
  46 ]
  47 qed.