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 "basic_2/notation/relations/lazyeqalt_4.ma".
16 include "basic_2/substitution/lleq_ldrop.ma".
17 include "basic_2/substitution/lleq_lleq.ma".
19 inductive lleqa: relation4 ynat term lenv lenv ≝
20 | lleqa_sort: ∀L1,L2,d,k. |L1| = |L2| → lleqa d (⋆k) L1 L2
21 | lleqa_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → lleqa d (#i) L1 L2
22 | lleqa_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
23 ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
24 lleqa (yinj 0) V K1 K2 → lleqa d (#i) L1 L2
25 | lleqa_free: ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → lleqa d (#i) L1 L2
26 | lleqa_gref: ∀L1,L2,d,p. |L1| = |L2| → lleqa d (§p) L1 L2
27 | lleqa_bind: ∀a,I,L1,L2,V,T,d.
28 lleqa d V L1 L2 → lleqa (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
29 lleqa d (ⓑ{a,I}V.T) L1 L2
30 | lleqa_flat: ∀I,L1,L2,V,T,d.
31 lleqa d V L1 L2 → lleqa d T L1 L2 → lleqa d (ⓕ{I}V.T) L1 L2
35 "lazy equivalence (local environment) alternative"
36 'LazyEqAlt T d L1 L2 = (lleqa d T L1 L2).
38 (* Main inversion lemmas ****************************************************)
40 theorem lleqa_inv_lleq: ∀L1,L2,T,d. L1 ⋕⋕[T, d] L2 → L1 ⋕[T, d] L2.
41 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d
42 /2 width=8 by lleq_flat, lleq_bind, lleq_gref, lleq_free, lleq_lref, lleq_skip, lleq_sort/
45 (* Main properties **********************************************************)
47 theorem lleq_lleqa: ∀L1,T,L2,d. L1 ⋕[T, d] L2 → L1 ⋕⋕[T, d] L2.
48 #L1 #T @(f2_ind … rfw … L1 T) -L1 -T
49 #n #IH #L1 * * /3 width=3 by lleqa_gref, lleqa_sort, lleq_fwd_length/
50 [ #i #Hn #L2 #d #H elim (lleq_fwd_lref … H) [ * || * ]
51 /4 width=9 by lleqa_free, lleqa_lref, lleqa_skip, lleq_fwd_length, ldrop_fwd_rfw/
52 | #a #I #V #T #Hn #L2 #d #H elim (lleq_inv_bind … H) -H /3 width=1 by lleqa_bind/
53 | #I #V #T #Hn #L2 #d #H elim (lleq_inv_flat … H) -H /3 width=1 by lleqa_flat/