From: Ferruccio Guidi Date: Fri, 28 Apr 2017 14:33:54 +0000 (+0000) Subject: - more background for the exclusion binder X-Git-Tag: make_still_working~451 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=69d929da2e17a9acc74edd49c2e726c72abf42ae;p=helm.git - more background for the exclusion binder - some corrections --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_bind.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_bind.ma new file mode 100644 index 000000000..65a8e5f22 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_bind.ma @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/syntax/bind.ma". +include "basic_2/relocation/lifts.ma". + +(* GENERIC RELOCATION FOR BINDERS *******************************************) + +definition liftsb: rtmap → relation bind ≝ + λf. ext2 (lifts f). + +interpretation "uniform relocation (binder for local environments)" + 'RLiftStar i I1 I2 = (liftsb (uni i) I1 I2). + +interpretation "generic relocation (binder for local environments)" + 'RLiftStar f I1 I2 = (liftsb f I1 I2). + +(* Basic_inversion lemmas **************************************************) + +lemma liftsb_inv_unit_sn: ∀f,I,Z2. ⬆*[f] BUnit I ≡ Z2 → Z2 = BUnit I. +/2 width=2 by ext2_inv_unit_sn/ qed-. + +lemma liftsb_inv_pair_sn: ∀f:rtmap. ∀Z2,I,V1. ⬆*[f] BPair I V1 ≡ Z2 → + ∃∃V2. ⬆*[f] V1 ≡ V2 & Z2 = BPair I V2. +/2 width=1 by ext2_inv_pair_sn/ qed-. + +lemma liftsb_inv_unit_dx: ∀f,I,Z1. ⬆*[f] Z1 ≡ BUnit I → Z1 = BUnit I. +/2 width=2 by ext2_inv_unit_dx/ qed-. + +lemma liftsb_inv_pair_dx: ∀f:rtmap. ∀Z1,I,V2. ⬆*[f] Z1 ≡ BPair I V2 → + ∃∃V1. ⬆*[f] V1 ≡ V2 & Z1 = BPair I V1. +/2 width=1 by ext2_inv_pair_dx/ qed-. + +(* Basic properties *********************************************************) + +lemma liftsb_eq_repl_back: ∀I1,I2. eq_repl_back … (λf. ⬆*[f] I1 ≡ I2). +#I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/ +qed-. + +lemma liftsb_refl: ∀f. 𝐈⦃f⦄ → reflexive … (liftsb f). +/3 width=1 by lifts_refl, ext2_refl/ qed. + +lemma liftsb_total: ∀I1,f. ∃I2. ⬆*[f] I1 ≡ I2. +* [2: #I #T1 #f elim (lifts_total T1 f) ] +/3 width=2 by ext2_unit, ext2_pair, ex_intro/ +qed-. + +lemma liftsb_split_trans: ∀f,I1,I2. ⬆*[f] I1 ≡ I2 → + ∀f1,f2. f2 ⊚ f1 ≡ f → + ∃∃I. ⬆*[f1] I1 ≡ I & ⬆*[f2] I ≡ I2. +#f #I1 #I2 * -I1 -I2 /2 width=3 by ext2_unit, ex2_intro/ +#I #V1 #V2 #HV12 #f1 #f2 #Hf elim (lifts_split_trans … HV12 … Hf) -f +/3 width=3 by ext2_pair, ex2_intro/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma liftsb_fwd_isid: ∀f,I1,I2. ⬆*[f] I1 ≡ I2 → 𝐈⦃f⦄ → I1 = I2. +#f #I1 #I2 * -I1 -I2 /3 width=3 by lifts_fwd_isid, eq_f2/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma index d3fa65354..3822e2dd0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma @@ -106,13 +106,13 @@ qed-. (* Advanced proprerties *****************************************************) (* Basic_2A1: includes: lift_inj *) -lemma lifts_inj: ∀f,T1,U. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2. +lemma lifts_inj: ∀f. is_inj2 … (lifts f). #f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝 … f) /3 width=6 by lifts_div3, lifts_fwd_isid/ qed-. (* Basic_2A1: includes: lift_mono *) -lemma lifts_mono: ∀f,T,U1. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2. +lemma lifts_mono: ∀f,T. is_mono … (lifts f T). #f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝 … f) /3 width=6 by lifts_conf, lifts_fwd_isid/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_bind.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_bind.ma new file mode 100644 index 000000000..10ad3cc52 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_bind.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lifts_lifts.ma". +include "basic_2/relocation/lifts_bind.ma". + +(* GENERIC RELOCATION FOR BINDERS *******************************************) + +(* Main properties **********************************************************) + +theorem liftsb_div3: ∀f2,I,I2. ⬆*[f2] I2 ≡ I → ∀f,I1. ⬆*[f] I1 ≡ I → + ∀f1. f2 ⊚ f1 ≡ f → ⬆*[f1] I1 ≡ I2. +#f2 #I #I2 * -I -I2 #I [2: #V #V2 #HV2 ] #f #I1 #H +[ elim (liftsb_inv_pair_dx … H) | lapply (liftsb_inv_unit_dx … H) ] -H +/3 width=6 by lifts_div3, ext2_pair, ext2_unit/ +qed-. + +theorem liftsb_trans: ∀f1,I1,I. ⬆*[f1] I1 ≡ I → ∀f2,I2. ⬆*[f2] I ≡ I2 → + ∀f. f2 ⊚ f1 ≡ f → ⬆*[f] I1 ≡ I2. +#f1 #I1 #I * -I1 -I #I1 [2: #V1 #V #HV1 ] #f2 #I2 #H +[ elim (liftsb_inv_pair_sn … H) | lapply (liftsb_inv_unit_sn … H) ] -H +/3 width=6 by lifts_trans, ext2_pair, ext2_unit/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma index 8acd0a571..62af6ac90 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma @@ -25,10 +25,10 @@ inductive liftsv (f:rtmap): relation (list term) ≝ liftsv f (T1 @ T1s) (T2 @ T2s) . -interpretation "uniform relocation (vector)" +interpretation "uniform relocation (term vector)" 'RLiftStar i T1s T2s = (liftsv (uni i) T1s T2s). -interpretation "generic relocation (vector)" +interpretation "generic relocation (term vector)" 'RLiftStar f T1s T2s = (liftsv f T1s T2s). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight_bind.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight_bind.ma new file mode 100644 index 000000000..152ecbba1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight_bind.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/syntax/bind_weight.ma". +include "basic_2/relocation/lifts_weight.ma". +include "basic_2/relocation/lifts_bind.ma". + +(* GENERIC RELOCATION FOR BINDERS *******************************************) + +(* Forward lemmas with weight for binders ***********************************) + +lemma liftsb_fwd_bw: ∀f,I1,I2. ⬆*[f] I1 ≡ I2 → ♯{I1} = ♯{I2}. +#f #I1 #I2 * -I1 -I2 /2 width=2 by lifts_fwd_tw/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma index ca474406d..8787d709b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma @@ -21,16 +21,69 @@ inductive bind: Type[0] ≝ | BPair: bind2 → term → bind . +inductive ext2 (R:relation term): relation bind ≝ +| ext2_unit: ∀I. ext2 R (BUnit I) (BUnit I) +| ext2_pair: ∀I,V1,V2. R V1 V2 → ext2 R (BPair I V1) (BPair I V2) +. + +(* Basic_inversion lemmas **************************************************) + +fact ext2_inv_unit_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 → + ∀I. Z1 = BUnit I → Z2 = BUnit I. +#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ] +#J #H destruct // +qed-. + +lemma ext2_inv_unit_sn: ∀R,I,Z2. ext2 R (BUnit I) Z2 → Z2 = BUnit I. +/2 width=4 by ext2_inv_unit_sn_aux/ qed-. + +fact ext2_inv_pair_sn_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 → + ∀I,V1. Z1 = BPair I V1 → + ∃∃V2. R V1 V2 & Z2 = BPair I V2. +#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ] +#J #W1 #H destruct /2 width=3 by ex2_intro/ +qed-. + +lemma ext2_inv_pair_sn: ∀R,Z2,I,V1. ext2 R (BPair I V1) Z2 → + ∃∃V2. R V1 V2 & Z2 = BPair I V2. +/2 width=3 by ext2_inv_pair_sn_aux/ qed-. + +fact ext2_inv_unit_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 → + ∀I. Z2 = BUnit I → Z1 = BUnit I. +#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #_ ] +#J #H destruct // +qed-. + +lemma ext2_inv_unit_dx: ∀R,I,Z1. ext2 R Z1 (BUnit I) → Z1 = BUnit I. +/2 width=4 by ext2_inv_unit_dx_aux/ qed-. + +fact ext2_inv_pair_dx_aux: ∀R,Z1,Z2. ext2 R Z1 Z2 → + ∀I,V2. Z2 = BPair I V2 → + ∃∃V1. R V1 V2 & Z1 = BPair I V1. +#R #Z1 #Z2 * -Z1 -Z2 #I [2: #V1 #V2 #HV12 ] +#J #W2 #H destruct /2 width=3 by ex2_intro/ +qed-. + +lemma ext2_inv_pair_dx: ∀R,Z1,I,V2. ext2 R Z1 (BPair I V2) → + ∃∃V1. R V1 V2 & Z1 = BPair I V1. +/2 width=3 by ext2_inv_pair_dx_aux/ qed-. + (* Basic properties ********************************************************) lemma eq_bind_dec: ∀I1,I2:bind. Decidable (I1 = I2). * #I1 [2: #V1 ] * #I2 [2,4: #V2 ] -[ elim (eq_bind2_dec I1 I2) #HI - [ elim (eq_term_dec V1 V2) #HV /2 width=1 by or_introl/ ] - @or_intror #H destruct /2 width=1 by/ -| @or_intror #H destruct -| @or_intror #H destruct -| elim (eq_bind1_dec I1 I2) #HI /2 width=1 by or_introl/ - @or_intror #H destruct /2 width=1 by/ +[1: elim (eq_bind2_dec I1 I2) #HI + [ elim (eq_term_dec V1 V2) #HV ] +|4: elim (eq_bind1_dec I1 I2) #HI ] +/2 width=1 by or_introl/ +@or_intror #H destruct /2 width=1 by/ +qed-. + +lemma ext2_refl: ∀R. reflexive … R → reflexive … (ext2 R). +#R #HR * /2 width=1 by ext2_pair/ +qed. + +lemma ext2_sym: ∀R. symmetric … R → symmetric … (ext2 R). +#R #HR #T1 #T2 * /3 width=1 by ext2_unit, ext2_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind_weight.ma index 2dda071d3..85277a353 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind_weight.ma @@ -12,10 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/syntax/term.ma". - -(* BINDERS FOR LOCAL ENVIRONMENTS ******************************************) - include "basic_2/syntax/term_weight.ma". include "basic_2/syntax/bind.ma".