From 2c8220e5e0c09486355aa79d5cd8a7716c444aca Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 7 Mar 2016 17:04:28 +0000 Subject: [PATCH] more results on after ... --- .../ground_2/relocation/rtmap_after.ma | 45 +++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma index 45a72459e..cdded4f97 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma @@ -159,6 +159,47 @@ lemma after_inv_pxx: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1. ↑f1 = g1 → ] qed-. +(* Basic properties *********************************************************) + +let corec after_eq_repl_back_2: ∀f1,f. eq_repl_back (λf2. f2 ⊚ f1 ≡ f) ≝ ?. +#f1 #f #f2 * -f2 -f1 -f +#f21 #f1 #f #g21 [1,2: #g1 ] #g #Hf #H21 [1,2: #H1 ] #H #g22 #H0 +[ cases (eq_inv_px … H0 … H21) -g21 /3 width=7 by after_refl/ +| cases (eq_inv_px … H0 … H21) -g21 /3 width=7 by after_push/ +| cases (eq_inv_nx … H0 … H21) -g21 /3 width=5 by after_next/ +] +qed-. + +lemma after_eq_repl_fwd_2: ∀f1,f. eq_repl_fwd (λf2. f2 ⊚ f1 ≡ f). +#f1 #f @eq_repl_sym /2 width=3 by after_eq_repl_back_2/ +qed-. + +let corec after_eq_repl_back_1: ∀f2,f. eq_repl_back (λf1. f2 ⊚ f1 ≡ f) ≝ ?. +#f2 #f #f1 * -f2 -f1 -f +#f2 #f11 #f #g2 [1,2: #g11 ] #g #Hf #H2 [1,2: #H11 ] #H #g2 #H0 +[ cases (eq_inv_px … H0 … H11) -g11 /3 width=7 by after_refl/ +| cases (eq_inv_nx … H0 … H11) -g11 /3 width=7 by after_push/ +| @(after_next … H2 H) /2 width=5 by/ +] +qed-. + +lemma after_eq_repl_fwd_1: ∀f2,f. eq_repl_fwd (λf1. f2 ⊚ f1 ≡ f). +#f2 #f @eq_repl_sym /2 width=3 by after_eq_repl_back_1/ +qed-. + +let corec after_eq_repl_back_0: ∀f1,f2. eq_repl_back (λf. f2 ⊚ f1 ≡ f) ≝ ?. +#f2 #f1 #f * -f2 -f1 -f +#f2 #f1 #f01 #g2 [1,2: #g1 ] #g01 #Hf01 #H2 [1,2: #H1 ] #H01 #g02 #H0 +[ cases (eq_inv_px … H0 … H01) -g01 /3 width=7 by after_refl/ +| cases (eq_inv_nx … H0 … H01) -g01 /3 width=7 by after_push/ +| cases (eq_inv_nx … H0 … H01) -g01 /3 width=5 by after_next/ +] +qed-. + +lemma after_eq_repl_fwd_0: ∀f2,f1. eq_repl_fwd (λf. f2 ⊚ f1 ≡ f). +#f2 #f1 @eq_repl_sym /2 width=3 by after_eq_repl_back_0/ +qed-. + (* Main properties **********************************************************) let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 → @@ -220,6 +261,10 @@ let corec after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ] qed-. +lemma after_mono_eq: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1,g2,g. g1 ⊚ g2 ≡ g → + f1 ≗ g1 → f2 ≗ g2 → f ≗ g. +/4 width=4 by after_mono, after_eq_repl_back_1, after_eq_repl_back_2/ qed-. + (* Properties on tls ********************************************************) lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → -- 2.39.2