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/lazyeq_6.ma".
16 include "basic_2/grammar/genv.ma".
17 include "basic_2/relocation/frees_weight.ma".
18 include "basic_2/relocation/frees_lreq.ma".
20 (* LAZY EQUIVALENCE FOR CLOSURES ********************************************)
22 inductive freq (G) (L1) (T): relation3 genv lenv term ≝
23 | fleq_intro: ∀L2,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → freq G L1 T G L2 T
27 "ranged equivalence (closure)"
28 'LazyEq G1 L1 T1 G2 L2 T2 = (freq G1 L1 T1 G2 L2 T2).
30 (* Basic properties *********************************************************)
32 lemma freq_refl: tri_reflexive … freq.
33 #G #L #T elim (frees_total L T) /2 width=3 by fleq_intro/
36 lemma freq_sym: tri_symmetric … freq.
37 #G1 #L1 #T1 #G2 #L2 #T2 * /4 width=3 by fleq_intro, frees_lreq_conf, lreq_sym/
40 (* Basic inversion lemmas ***************************************************)
42 lemma freq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄ →
43 ∃∃f. G1 = G2 & L1 ⊢ 𝐅*⦃T1⦄ ≡ f & L1 ≡[f] L2 & T1 = T2.
44 #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=3 by ex4_intro/
47 (* Basic_2A1: removed theorems 6:
48 fleq_refl fleq_sym fleq_inv_gen
49 fleq_trans fleq_canc_sn fleq_canc_dx