1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "static_2/notation/relations/ideqsn_3.ma".
16 include "static_2/syntax/teq_ext.ma".
17 include "static_2/relocation/sex.ma".
19 (* SYNTACTIC EQUIVALENCE FOR SELECTED LOCAL ENVIRONMENTS ********************)
21 (* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *)
22 definition seq: relation3 pr_map lenv lenv ≝
26 "syntactic equivalence on selected entries (local environment)"
27 'IdEqSn f L1 L2 = (seq f L1 L2).
29 (* Basic properties *********************************************************)
31 lemma seq_eq_repl_back:
32 ∀L1,L2. pr_eq_repl_back … (λf. L1 ≡[f] L2).
33 /2 width=3 by sex_eq_repl_back/ qed-.
35 lemma seq_eq_repl_fwd:
36 ∀L1,L2. pr_eq_repl_fwd … (λf. L1 ≡[f] L2).
37 /2 width=3 by sex_eq_repl_fwd/ qed-.
40 ∀f2,L1,L2. L1 ≡[f2] L2 →
41 ∀f1. f1 ⊆ f2 → L1 ≡[f1] L2.
42 /2 width=3 by sle_sex_trans/ qed-.
44 (* Basic_2A1: includes: lreq_refl *)
47 /2 width=1 by sex_refl/ qed.
49 (* Basic_2A1: includes: lreq_sym *)
52 /3 width=1 by sex_sym, ceq_ext_sym/ qed-.
54 (* Basic inversion lemmas ***************************************************)
56 (* Basic_2A1: includes: lreq_inv_atom1 *)
57 lemma seq_inv_atom1 (f):
59 /2 width=4 by sex_inv_atom1/ qed-.
61 (* Basic_2A1: includes: lreq_inv_pair1 *)
62 lemma seq_inv_next1 (g):
63 ∀J,K1,Y. K1.ⓘ[J] ≡[↑g] Y →
64 ∃∃K2. K1 ≡[g] K2 & Y = K2.ⓘ[J].
66 elim (sex_inv_next1 … H) -H #Z #K2 #HK12 #H1 #H2 destruct
67 <(ceq_ext_inv_eq … H1) -Z /2 width=3 by ex2_intro/
70 (* Basic_2A1: includes: lreq_inv_zero1 lreq_inv_succ1 *)
71 lemma seq_inv_push1 (g):
72 ∀J1,K1,Y. K1.ⓘ[J1] ≡[⫯g] Y →
73 ∃∃J2,K2. K1 ≡[g] K2 & Y = K2.ⓘ[J2].
74 #g #J1 #K1 #Y #H elim (sex_inv_push1 … H) -H /2 width=4 by ex2_2_intro/
77 (* Basic_2A1: includes: lreq_inv_atom2 *)
78 lemma seq_inv_atom2 (f):
80 /2 width=4 by sex_inv_atom2/ qed-.
82 (* Basic_2A1: includes: lreq_inv_pair2 *)
83 lemma seq_inv_next2 (g):
84 ∀J,X,K2. X ≡[↑g] K2.ⓘ[J] →
85 ∃∃K1. K1 ≡[g] K2 & X = K1.ⓘ[J].
87 elim (sex_inv_next2 … H) -H #Z #K1 #HK12 #H1 #H2 destruct
88 <(ceq_ext_inv_eq … H1) -J /2 width=3 by ex2_intro/
91 (* Basic_2A1: includes: lreq_inv_zero2 lreq_inv_succ2 *)
92 lemma seq_inv_push2 (g):
93 ∀J2,X,K2. X ≡[⫯g] K2.ⓘ[J2] →
94 ∃∃J1,K1. K1 ≡[g] K2 & X = K1.ⓘ[J1].
95 #g #J2 #X #K2 #H elim (sex_inv_push2 … H) -H /2 width=4 by ex2_2_intro/
98 (* Basic_2A1: includes: lreq_inv_pair *)
99 lemma seq_inv_next (f):
100 ∀I1,I2,L1,L2. L1.ⓘ[I1] ≡[↑f] L2.ⓘ[I2] →
101 ∧∧ L1 ≡[f] L2 & I1 = I2.
102 #f #I1 #I2 #L1 #L2 #H elim (sex_inv_next … H) -H
103 /3 width=3 by ceq_ext_inv_eq, conj/
106 (* Basic_2A1: includes: lreq_inv_succ *)
107 lemma seq_inv_push (f):
108 ∀I1,I2,L1,L2. L1.ⓘ[I1] ≡[⫯f] L2.ⓘ[I2] → L1 ≡[f] L2.
109 #f #I1 #I2 #L1 #L2 #H elim (sex_inv_push … H) -H /2 width=1 by conj/
112 lemma seq_inv_tl (f):
113 ∀I,L1,L2. L1 ≡[⫰f] L2 → L1.ⓘ[I] ≡[f] L2.ⓘ[I].
114 /2 width=1 by sex_inv_tl/ qed-.
116 (* Basic_2A1: removed theorems 5:
117 lreq_pair_lt lreq_succ_lt lreq_pair_O_Y lreq_O2 lreq_inv_O_Y