]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc_new/ltls.etc
some improvements towards the confluence of lfpr ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_new / 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.