let missing path =
failwith (P.sprintf "probe: missing path: %s" path)
-let unrooted path =
- failwith (P.sprintf "probe: missing root: %s" path)
+let unrooted path roots =
+ failwith (P.sprintf "probe: missing root: %s (found roots: %u)" path (L.length roots))
let out_int i = P.printf "%u\n" i
| [root] ->
let buri = L.assoc "baseuri" (B.load_root_file root) in
F.concat bdir file, F.concat buri file
- | _ ->
- if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir else
+ | roots ->
+ if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir roots else
aux (F.dirname bdir) (F.concat (F.basename bdir) file)
in
aux dir file
(guarded_by_constructors status ~subst ~metasenv types bo r_uri r_len len)
then
raise (TypeCheckerFailure
- (lazy "CoFix: not guarded by constructors"))
+ (lazy ("CoFix: not guarded by constructors: " ^ status#ppobj (uri,height,metasenv,subst,kind))))
) fl dfl
;;
-include "basic_2/grammar/lenv_length.ma".
-
lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → |L| < m →
s = Ⓣ ∧ K = ⋆.
#L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize in ⊢ (?%?→?); #H1m
]
qed-.
-lemma drop_fwd_length: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → |L1| = |L2| + m.
-#L1 #L2 #l #m #H elim H -L1 -L2 -l -m //
-#l #m #H >H -m //
-qed-.
-
-lemma drop_fwd_length_le2: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → m ≤ |L1|.
-#L1 #L2 #l #m #H lapply (drop_fwd_length … H) -H //
-qed-.
-
-lemma drop_fwd_length_le4: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → |L2| ≤ |L1|.
-#L1 #L2 #l #m #H lapply (drop_fwd_length … H) -H //
-qed-.
-
-lemma drop_fwd_length_lt2: ∀L1,I2,K2,V2,l,m.
- ⬇[Ⓕ, l, m] L1 ≡ K2. ⓑ{I2} V2 → m < |L1|.
-#L1 #I2 #K2 #V2 #l #m #H
-lapply (drop_fwd_Y2 … H) #Hm
-lapply (drop_fwd_length … H) -l #H <(yplus_O2 m) >H -L1
-/2 width=1 by monotonic_ylt_plus_sn/
-qed-.
-
-lemma drop_fwd_length_lt4: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → 0 < m → |L2| < |L1|.
-#L1 #L2 #l #m #H
-lapply (drop_fwd_Y2 … H) #Hm
-lapply (drop_fwd_length … H) -l
-/2 width=1 by monotonic_ylt_plus_sn/
-qed-.
-
-lemma drop_fwd_length_eq1: ∀L1,L2,K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
- |L1| = |L2| → |K1| = |K2|.
-#L1 #L2 #K1 #K2 #l #m #HLK1 #HLK2 #HL12
-lapply (drop_fwd_Y2 … HLK1) #Hm
-lapply (drop_fwd_length … HLK1) -HLK1
-lapply (drop_fwd_length … HLK2) -HLK2
-#H #H0 >H in HL12; -H >H0 -H0 #H
-@(yplus_inv_monotonic_dx … H) -H // (**) (* auto fails *)
-qed-.
-
-lemma drop_fwd_length_eq2: ∀L1,L2,K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
- |K1| = |K2| → |L1| = |L2|.
-#L1 #L2 #K1 #K2 #l #m #HLK1 #HLK2 #HL12
-lapply (drop_fwd_length … HLK1) -HLK1
-lapply (drop_fwd_length … HLK2) -HLK2 //
-qed-.
-
-lemma drop_inv_length_eq: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 →
- |L1| = |L2| → m = 0.
-#L1 #L2 #l #m #H #HL12 lapply (drop_fwd_length … H) -H
->HL12 -L1 #H elim (discr_yplus_x_xy … H) -H //
-#H elim (ylt_yle_false (|L2|) (∞)) //
-qed-.
-
lemma drop_fwd_be: ∀L,K,s,l,m,i. ⬇[s, l, m] L ≡ K → |K| ≤ i → i < l → |L| ≤ i.
#L #K #s #l #m #i #HLK #HK #Hl elim (ylt_split i (|L|)) //
#HL elim (drop_O1_lt (Ⓕ) … HL) #I #K0 #V #HLK0 -HL
#H elim (ylt_yle_false … H) -H //
qed-.
-lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 →
-|t1| + ∥t2∥ = ∥t1∥ + |t2|.
-#L1 #L2 #t1 #H elim H -L1 -L2 -t1
-[ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H
- #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 //
-| #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize
-
lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2.
#K2 #i @(ynat_ind … i) -i
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/grammar/lenv_length.ma".
+include "basic_2/grammar/cl_restricted_weight.ma".
+include "basic_2/relocation/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Forward lemmas on length for local environments **************************)
+
+lemma frees_fwd_length: ∀L,T,t. L ⊢ 𝐅*⦃T⦄ ≡ t → |L| = |t|.
+#L #T #t #H elim H -L -T -t //
+[ #p ] #I #L #V #T #t1 #t2 #t [ #b ] #_ #_ #Ht elim (sor_inv_length … Ht) -Ht //
+qed-.
lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆.
/2 width=1 by length_inv_zero_dx/ qed-.
-lemma length_inv_pos_dx: ∀n,L. |L| = ⫯n →
- ∃∃I,K,V. |K| = n & L = K. ⓑ{I}V.
+(* Basic_2A1: was: length_inv_pos_dx *)
+lemma length_inv_succ_dx: ∀n,L. |L| = ⫯n →
+ ∃∃I,K,V. |K| = n & L = K. ⓑ{I}V.
#n * /3 width=5 by injective_S, ex2_3_intro/
>length_atom #H destruct
qed-.
-lemma length_inv_pos_sn: ∀n,L. ⫯n = |L| →
- ∃∃I,K,V. n = |K| & L = K. ⓑ{I}V.
+(* Basic_2A1: was: length_inv_pos_sn *)
+lemma length_inv_succ_sn: ∀n,L. ⫯n = |L| →
+ ∃∃I,K,V. n = |K| & L = K. ⓑ{I}V.
#l #L #H lapply (sym_eq ??? H) -H
-#H elim (length_inv_pos_dx … H) -H /2 width=5 by ex2_3_intro/
+#H elim (length_inv_succ_dx … H) -H /2 width=5 by ex2_3_intro/
qed-.
(* Basic_2A1: removed theorems 1: length_inj *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "ground_2/relocation/rtmap_isfin.ma".
+include "basic_2/grammar/lenv_length.ma".
+include "basic_2/relocation/drops.ma".
+
+(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Forward lemmas with length for local environments ************************)
+
+(* Basic_2A1: includes: drop_fwd_length_le4 *)
+lemma drops_fwd_length_le4: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → |L2| ≤ |L1|.
+#L1 #L2 #c #f #H elim H -L1 -L2 -f /2 width=1 by le_S, le_S_S/
+qed-.
+
+(* Basic_2A1: includes: drop_fwd_length_eq1 *)
+theorem drops_fwd_length_eq1: ∀L1,K1,c1,c2,f. ⬇*[c1, f] L1 ≡ K1 →
+ ∀L2,K2. ⬇*[c2, f] L2 ≡ K2 →
+ |L1| = |L2| → |K1| = |K2|.
+#L1 #K1 #c1 #c2 #f #HLK1 elim HLK1 -L1 -K1 -f
+[ #f #_ #L2 #K2 #HLK2 #H lapply (length_inv_zero_sn … H) -H
+ #H destruct elim (drops_inv_atom1 … HLK2) -HLK2 //
+| #I1 #L1 #K1 #V1 #f #_ #IH #X2 #K2 #HX #H elim (length_inv_succ_sn … H) -H
+ #I2 #L2 #V2 #H12 #H destruct lapply (drops_inv_drop1 … HX) -HX
+ #HLK2 @(IH … HLK2 H12) (**) (* auto fails *)
+| #I1 #L1 #K1 #V1 #V2 #f #_ #_ #IH #X2 #Y2 #HX #H elim (length_inv_succ_sn … H) -H
+ #I2 #L2 #V2 #H12 #H destruct elim (drops_inv_skip1 … HX) -HX
+ #K2 #W2 #HLK2 #_ #H destruct
+ lapply (IH … HLK2 H12) -f /2 width=1 by/ (**) (* full auto fails *)
+]
+qed-.
+
+(* forward lemmas with finite colength assignment ***************************)
+
+lemma drops_fwd_fcla: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 →
+ ∃∃n. 𝐂⦃f⦄ ≡ n & |L1| = |L2| + n.
+#L1 #L2 #f #H elim H -L1 -L2 -f
+[ /4 width=3 by fcla_isid, ex2_intro/
+| #I #L1 #L2 #V #f #_ * /3 width=3 by fcla_next, ex2_intro, eq_f/
+| #I #L1 #L2 #V1 #V2 #f #_ #_ * /3 width=3 by fcla_push, ex2_intro/
+]
+qed-.
+
+(* Basic_2A1: includes: drop_fwd_length *)
+lemma drops_fcla_fwd: ∀L1,L2,f,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃f⦄ ≡ n →
+ |L1| = |L2| + n.
+#l1 #l2 #f #n #Hf #Hn elim (drops_fwd_fcla … Hf) -Hf
+#m #Hm #H <(fcla_mono … Hm … Hn) -f //
+qed-.
+
+lemma drops_fwd_fcla_le2: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 →
+ ∃∃n. 𝐂⦃f⦄ ≡ n & n ≤ |L1|.
+#L1 #L2 #f #H elim (drops_fwd_fcla … H) -H /2 width=3 by ex2_intro/
+qed-.
+
+(* Basic_2A1: includes: drop_fwd_length_le2 *)
+lemma drops_fcla_fwd_le2: ∀L1,L2,f,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃f⦄ ≡ n →
+ n ≤ |L1|.
+#L1 #L2 #f #n #H #Hn elim (drops_fwd_fcla_le2 … H) -H
+#m #Hm #H <(fcla_mono … Hm … Hn) -f //
+qed-.
+
+lemma drops_fwd_fcla_lt2: ∀L1,I2,K2,V2,f. ⬇*[Ⓣ, f] L1 ≡ K2.ⓑ{I2}V2 →
+ ∃∃n. 𝐂⦃f⦄ ≡ n & n < |L1|.
+#L1 #I2 #K2 #V2 #f #H elim (drops_fwd_fcla … H) -H
+#n #Hf #H >H -L1 /3 width=3 by le_S_S, ex2_intro/
+qed-.
+
+(* Basic_2A1: includes: drop_fwd_length_lt2 *)
+lemma drops_fcla_fwd_lt2: ∀L1,I2,K2,V2,f,n.
+ ⬇*[Ⓣ, f] L1 ≡ K2.ⓑ{I2}V2 → 𝐂⦃f⦄ ≡ n →
+ n < |L1|.
+#L1 #I2 #K2 #V2 #f #n #H #Hn elim (drops_fwd_fcla_lt2 … H) -H
+#m #Hm #H <(fcla_mono … Hm … Hn) -f //
+qed-.
+
+(* Basic_2A1: includes: drop_fwd_length_lt4 *)
+lemma drops_fcla_fwd_lt4: ∀L1,L2,f,n. ⬇*[Ⓣ, f] L1 ≡ L2 → 𝐂⦃f⦄ ≡ n → 0 < n →
+ |L2| < |L1|.
+#L1 #L2 #f #n #H #Hf #Hn lapply (drops_fcla_fwd … H Hf) -f
+/2 width=1 by lt_minus_to_plus_r/ qed-.
+
+(* Basic_2A1: includes: drop_inv_length_eq *)
+lemma drops_inv_length_eq: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → |L1| = |L2| → 𝐈⦃f⦄.
+#L1 #L2 #f #H #HL12 elim (drops_fwd_fcla … H) -H
+#n #Hn <HL12 -L2 #H lapply (discr_plus_x_xy … H) -H
+/2 width=3 by fcla_inv_xp/
+qed-.
+
+(* Basic_2A1: includes: drop_fwd_length_eq2 *)
+theorem drops_fwd_length_eq2: ∀L1,L2,K1,K2,f. ⬇*[Ⓣ, f] L1 ≡ K1 → ⬇*[Ⓣ, f] L2 ≡ K2 →
+ |K1| = |K2| → |L1| = |L2|.
+#L1 #L2 #K1 #K2 #f #HLK1 #HLK2 #HL12
+elim (drops_fwd_fcla … HLK1) -HLK1 #n1 #Hn1 #H1 >H1 -L1
+elim (drops_fwd_fcla … HLK2) -HLK2 #n2 #Hn2 #H2 >H2 -L2
+<(fcla_mono … Hn2 … Hn1) -f //
+qed-.
+
+theorem drops_conf_div: ∀L1,L2,f1,f2. ⬇*[Ⓣ, f1] L1 ≡ L2 → ⬇*[Ⓣ, f2] L1 ≡ L2 →
+ ∃∃n. 𝐂⦃f1⦄ ≡ n & 𝐂⦃f2⦄ ≡ n.
+#L1 #L2 #f1 #f2 #H1 #H2
+elim (drops_fwd_fcla … H1) -H1 #n1 #Hf1 #H1
+elim (drops_fwd_fcla … H2) -H2 #n2 #Hf2 >H1 -L1 #H
+lapply (injective_plus_r … H) -L2 #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+theorem drops_conf_div_fcla: ∀L1,L2,f1,f2,n1,n2.
+ ⬇*[Ⓣ, f1] L1 ≡ L2 → ⬇*[Ⓣ, f2] L1 ≡ L2 → 𝐂⦃f1⦄ ≡ n1 → 𝐂⦃f2⦄ ≡ n2 →
+ n1 = n2.
+#L1 #L2 #f1 #f2 #n1 #n2 #Hf1 #Hf2 #Hn1 #Hn2
+lapply (drops_fcla_fwd … Hf1 Hn1) -f1 #H1
+lapply (drops_fcla_fwd … Hf2 Hn2) -f2 >H1 -L1
+/2 width=1 by injective_plus_r/
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/notation/relations/lazyeq_7.ma".
-include "basic_2/grammar/genv.ma".
-include "basic_2/multiple/lleq.ma".
-
-(* LAZY EQUIVALENCE FOR CLOSURES ********************************************)
-
-inductive fleq (l) (G) (L1) (T): relation3 genv lenv term ≝
-| fleq_intro: ∀L2. L1 ≡[T, l] L2 → fleq l G L1 T G L2 T
-.
-
-interpretation
- "lazy equivalence (closure)"
- 'LazyEq l G1 L1 T1 G2 L2 T2 = (fleq l G1 L1 T1 G2 L2 T2).
-
-(* Basic properties *********************************************************)
-
-lemma fleq_refl: ∀l. tri_reflexive … (fleq l).
-/2 width=1 by fleq_intro/ qed.
-
-lemma fleq_sym: ∀l. tri_symmetric … (fleq l).
-#l #G1 #L1 #T1 #G2 #L2 #T2 * /3 width=1 by fleq_intro, lleq_sym/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma fleq_inv_gen: ∀G1,G2,L1,L2,T1,T2,l. ⦃G1, L1, T1⦄ ≡[l] ⦃G2, L2, T2⦄ →
- ∧∧ G1 = G2 & L1 ≡[T1, l] L2 & T1 = T2.
-#G1 #G2 #L1 #L2 #T1 #T2 #l * -G2 -L2 -T2 /2 width=1 by and3_intro/
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/multiple/lleq_lleq.ma".
-include "basic_2/multiple/fleq.ma".
-
-(* LAZY EQUIVALENCE FOR CLOSURES *******************************************)
-
-(* Main properties **********************************************************)
-
-theorem fleq_trans: ∀l. tri_transitive … (fleq l).
-#l #G1 #G #L1 #L #T1 #T * -G -L -T
-#L #HT1 #G2 #L2 #T2 * -G2 -L2 -T2
-/3 width=3 by lleq_trans, fleq_intro/
-qed-.
-
-theorem fleq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2,l.
- ⦃G, L, T⦄ ≡[l] ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡[l] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡[l] ⦃G2, L2, T2⦄.
-/3 width=5 by fleq_trans, fleq_sym/ qed-.
-
-theorem fleq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T,l.
- ⦃G1, L1, T1⦄ ≡[l] ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡[l] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡[l] ⦃G2, L2, T2⦄.
-/3 width=5 by fleq_trans, fleq_sym/ qed-.
(* Basic inversion lemmas ***************************************************)
+fact frees_inv_atom_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀J. L = ⋆ → X = ⓪{J} → 𝐈⦃f⦄.
+#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
+[5,6: #I #L #V #T [ #p ] #f1 #f2 #f #_ #_ #_ #_ #_ #J #_ #H destruct
+|*: #I #L #V [1,3,4: #x ] #f #_ #_ #J #H destruct
+]
+qed-.
+
+lemma frees_inv_atom: ∀I,f. ⋆ ⊢ 𝐅*⦃⓪{I}⦄ ≡ f → 𝐈⦃f⦄.
+/2 width=6 by frees_inv_atom_aux/ qed-.
+
fact frees_inv_sort_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x → 𝐈⦃f⦄.
#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
[ #_ #L #V #f #_ #_ #x #H destruct
| #_ #L #_ #i #f #_ #_ #x #H destruct
-| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
+| #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
| #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
]
qed-.
#L #X #f #H elim H -L -X -f /3 width=3 by isid_push/
[ #_ #L #V #f #_ #_ #x #H destruct
| #_ #L #_ #i #f #_ #_ #x #H destruct
-| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
+| #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
| #I #L #V #T #f1 #f2 #f #_ #_ #_ #_ #_ #x #H destruct
]
qed-.
-lemma frees_inv_gref: ∀L,p,f. L ⊢ 𝐅*⦃§p⦄ ≡ f → 𝐈⦃f⦄.
+lemma frees_inv_gref: ∀L,l,f. L ⊢ 𝐅*⦃§l⦄ ≡ f → 𝐈⦃f⦄.
/2 width=5 by frees_inv_gref_aux/ qed-.
fact frees_inv_zero_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → X = #0 →
| #I #L #V #s #f #_ #H destruct
| /3 width=7 by ex3_4_intro, or_intror/
| #I #L #V #i #f #_ #H destruct
-| #I #L #V #p #f #_ #H destruct
-| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #H destruct
+| #I #L #V #l #f #_ #H destruct
+| #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #H destruct
| #I #L #V #T #f1 #f2 #f #_ #_ #_ #H destruct
]
qed-.
| #I #L #V #s #f #_ #j #H destruct
| #I #L #V #f #_ #j #H destruct
| #I #L #V #i #f #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/
-| #I #L #V #p #f #_ #j #H destruct
-| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #j #H destruct
+| #I #L #V #l #f #_ #j #H destruct
+| #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #j #H destruct
| #I #L #V #T #f1 #f2 #f #_ #_ #_ #j #H destruct
]
qed-.
| #I #L #V #s #f #_ #J #W #U #b #H destruct
| #I #L #V #f #_ #J #W #U #b #H destruct
| #I #L #V #i #f #_ #J #W #U #b #H destruct
-| #I #L #V #p #f #_ #J #W #U #b #H destruct
-| #I #L #V #T #a #f1 #f2 #f #HV #HT #Hf #J #W #U #b #H destruct /2 width=5 by ex3_2_intro/
+| #I #L #V #l #f #_ #J #W #U #b #H destruct
+| #I #L #V #T #p #f1 #f2 #f #HV #HT #Hf #J #W #U #b #H destruct /2 width=5 by ex3_2_intro/
| #I #L #V #T #f1 #f2 #f #_ #_ #_ #J #W #U #b #H destruct
]
qed-.
| #I #L #V #s #f #_ #J #W #U #H destruct
| #I #L #V #f #_ #J #W #U #H destruct
| #I #L #V #i #f #_ #J #W #U #H destruct
-| #I #L #V #p #f #_ #J #W #U #H destruct
-| #I #L #V #T #a #f1 #f2 #f #_ #_ #_ #J #W #U #H destruct
+| #I #L #V #l #f #_ #J #W #U #H destruct
+| #I #L #V #T #p #f1 #f2 #f #_ #_ #_ #J #W #U #H destruct
| #I #L #V #T #f1 #f2 #f #HV #HT #Hf #J #W #U #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f.
/2 width=4 by frees_inv_flat_aux/ qed-.
+(* Basic forward lemmas ****************************************************)
+
+lemma frees_fwd_isfin: ∀L,T,f. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄.
+#L #T #f #H elim H -L -T -f
+/3 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_push, isfin_next/
+qed-.
+
(* Basic properties ********************************************************)
lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f).
elim (eq_inv_nx … Hf12) -Hf12 /3 width=3 by frees_zero/
| #I #L #V #i #f1 #_ #IH #f2 #Hf12
elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_lref/
-| #I #L #V #p #f1 #_ #IH #f2 #Hf12
+| #I #L #V #l #f1 #_ #IH #f2 #Hf12
elim (eq_inv_px … Hf12) -Hf12 /3 width=3 by frees_gref/
| /3 width=7 by frees_bind, sor_eq_repl_back3/
| /3 width=7 by frees_flat, sor_eq_repl_back3/
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/lreq.ma".
+include "basic_2/relocation/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Properties on ranged equivalence for local environments ******************)
+
+lemma frees_lreq_conf: ∀L1,T,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≡[f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
+#L1 #T #f #H elim H -L1 -T -f
+[ #I #f #Hf #X #H lapply (lreq_inv_atom1 … H) -H
+ #H destruct /2 width=1 by frees_atom/
+| #I #L1 #V1 #s #f #_ #IH #X #H elim (lreq_inv_push1 … H) -H
+ /3 width=1 by frees_sort/
+| #I #L1 #V1 #f #_ #IH #X #H elim (lreq_inv_next1 … H) -H
+ /3 width=1 by frees_zero/
+| #I #L1 #V1 #i #f #_ #IH #X #H elim (lreq_inv_push1 … H) -H
+ /3 width=1 by frees_lref/
+| #I #L1 #V1 #l #f #_ #IH #X #H elim (lreq_inv_push1 … H) -H
+ /3 width=1 by frees_gref/
+| /6 width=5 by frees_bind, lreq_inv_tl, sle_lreq_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+| /5 width=5 by frees_flat, sle_lreq_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+]
+qed-.
+
+lemma lreq_frees_trans: ∀L1,T,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L2 ≡[f] L1 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
+/3 width=3 by frees_lreq_conf, lreq_sym/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "ground_2/relocation/rtmap_id.ma".
+include "basic_2/grammar/cl_restricted_weight.ma".
+include "basic_2/relocation/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Advanced properties ******************************************************)
+
+lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅*⦃T⦄ ≡ f.
+@(f2_ind … rfw) #n #IH #L *
+[ cases L -L /3 width=2 by frees_atom, ex_intro/
+ #L #I #V *
+ [ #s #Hn destruct elim (IH L (⋆s)) -IH /3 width=2 by frees_sort, ex_intro/
+ | * [2: #i ] #Hn destruct
+ [ elim (IH L (#i)) -IH /3 width=2 by frees_lref, ex_intro/
+ | elim (IH L V) -IH /3 width=2 by frees_zero, ex_intro/
+ ]
+ | #l #Hn destruct elim (IH L (§l)) -IH /3 width=2 by frees_gref, ex_intro/
+ ]
+| * [ #p ] #I #V #T #Hn destruct elim (IH L V) // #f1 #HV
+ [ elim (IH (L.ⓑ{I}V) T) -IH // #f2 #HT
+ elim (sor_isfin_ex f1 (⫱f2))
+ /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
+ | elim (IH L T) -IH // #f2 #HT
+ elim (sor_isfin_ex f1 f2)
+ /3 width=6 by frees_fwd_isfin, frees_flat, ex_intro/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/notation/relations/lazyeq_6.ma".
+include "basic_2/grammar/genv.ma".
+include "basic_2/relocation/frees_weight.ma".
+include "basic_2/relocation/frees_lreq.ma".
+
+(* LAZY EQUIVALENCE FOR CLOSURES ********************************************)
+
+inductive freq (G) (L1) (T): relation3 genv lenv term ≝
+| fleq_intro: ∀L2,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → freq G L1 T G L2 T
+.
+
+interpretation
+ "ranged equivalence (closure)"
+ 'LazyEq G1 L1 T1 G2 L2 T2 = (freq G1 L1 T1 G2 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma freq_refl: tri_reflexive … freq.
+#G #L #T elim (frees_total L T) /2 width=3 by fleq_intro/
+qed.
+
+lemma freq_sym: tri_symmetric … freq.
+#G1 #L1 #T1 #G2 #L2 #T2 * /4 width=3 by fleq_intro, frees_lreq_conf, lreq_sym/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma freq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄ →
+ ∃∃f. G1 = G2 & L1 ⊢ 𝐅*⦃T1⦄ ≡ f & L1 ≡[f] L2 & T1 = T2.
+#G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=3 by ex4_intro/
+qed-.
+
+(* Basic_2A1: removed theorems 6:
+ fleq_refl fleq_sym fleq_inv_gen
+ fleq_trans fleq_canc_sn fleq_canc_dx
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/lreq_lreq.ma".
+include "basic_2/relocation/frees_frees.ma".
+include "basic_2/relocation/freq.ma".
+
+(* LAZY EQUIVALENCE FOR CLOSURES *******************************************)
+
+(* Main properties **********************************************************)
+
+theorem freq_trans: tri_transitive … freq.
+#G1 #G #L1 #L #T1 #T * -G -L -T
+#L #f1 #H1T11 #Hf1 #G2 #L2 #T2 * -G2 -L2 -T2 #L2 #f2 #HT12 #Hf2
+lapply (frees_lreq_conf … H1T11 … Hf1) #HT11
+lapply (frees_mono … HT12 … HT11) -HT11 -HT12
+/4 width=7 by fleq_intro, lreq_eq_repl_back, lreq_trans/
+qed-.
+
+theorem freq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2.
+ ⦃G, L, T⦄ ≡ ⦃G1, L1, T1⦄→ ⦃G, L, T⦄ ≡ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄.
+/3 width=5 by freq_trans, freq_sym/ qed-.
+
+theorem freq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T.
+ ⦃G1, L1, T1⦄ ≡ ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≡ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≡ ⦃G2, L2, T2⦄.
+/3 width=5 by freq_trans, freq_sym/ qed-.
#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/
qed-.
+lemma lexs_inv_tl: ∀RN,RP,I,L1,L2,V1,V2,f. L1 ⦻*[RN, RP, ⫱f] L2 →
+ RN L1 V1 V2 → RP L1 V1 V2 →
+ L1.ⓑ{I}V1 ⦻*[RN, RP, f] L2.ⓑ{I}V2.
+#RN #RP #I #L2 #L2 #V1 #V2 #f elim (pn_split f) *
+/2 width=1 by lexs_next, lexs_push/
+qed-.
+
(* Basic properties *********************************************************)
lemma lexs_eq_repl_back: ∀RN,RP,L1,L2. eq_repl_back … (λf. L1 ⦻*[RN, RP, f] L2).
#I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push … H) -H /2 width=1 by conj/
qed-.
+lemma lreq_inv_tl: ∀I,L1,L2,V,f. L1 ≡[⫱f] L2 → L1.ⓑ{I}V ≡[f] L2.ⓑ{I}V.
+/2 width=1 by lexs_inv_tl/ qed-.
+
(* Basic_2A1: removed theorems 5:
lreq_pair_lt lreq_succ_lt lreq_pair_O_Y lreq_O2 lreq_inv_O_Y
*)
lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
// qed-.
+lemma discr_plus_x_xy: ∀x,y. x = x + y → y = 0.
+/2 width=2 by le_plus_minus_comm/ qed-.
+
lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
/2 width=1 by monotonic_pred/ qed-.
#g #m #_ #_ #H destruct
qed-.
+lemma fcla_inv_isid: ∀f,n. 𝐂⦃f⦄ ≡ n → 𝐈⦃f⦄ → 0 = n.
+#f #n #H elim H -f -n /3 width=3 by isid_inv_push/
+#f #n #_ #_ #H elim (isid_inv_next … H) -H //
+qed-.
+
+(* Main forward lemmas ******************************************************)
+
+theorem fcla_mono: ∀f,n1. 𝐂⦃f⦄ ≡ n1 → ∀n2. 𝐂⦃f⦄ ≡ n2 → n1 = n2.
+#f #n #H elim H -f -n
+[ /2 width=3 by fcla_inv_isid/
+| /3 width=3 by fcla_inv_px/
+| #f #n1 #_ #IH #n2 #H elim (fcla_inv_nx … H) -H [2,3 : // ]
+ #g #Hf #H destruct /3 width=1 by eq_f/
+]
+qed-.
+
(* Basic properties *********************************************************)
lemma fcla_eq_repl_back: ∀n. eq_repl_back … (λf. 𝐂⦃f⦄ ≡ n).
interpretation "test for finite colength (rtmap)"
'IsFinite f = (isfin f).
-(* Basic properties *********************************************************)
-
-lemma isfin_isid: ∀f. 𝐈⦃f⦄ → 𝐅⦃f⦄.
-/3 width=2 by fcla_isid, ex_intro/ qed.
-
-lemma isfin_push: ∀f. 𝐅⦃f⦄ → 𝐅⦃↑f⦄.
-#f * /3 width=2 by fcla_push, ex_intro/
-qed.
-
-lemma isfin_next: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫯f⦄.
-#f * /3 width=2 by fcla_next, ex_intro/
-qed.
-
-lemma isfin_eq_repl_back: eq_repl_back … isfin.
-#f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
-qed-.
-
-lemma isfin_eq_repl_fwd: eq_repl_fwd … isfin.
-/3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
-
(* Basic eliminators ********************************************************)
lemma isfin_ind (R:predicate rtmap): (∀f. 𝐈⦃f⦄ → R f) →
lemma isfin_fwd_push: ∀g. 𝐅⦃g⦄ → ∀f. ↑f = g → 𝐅⦃f⦄.
#g * /3 width=4 by fcla_inv_px, ex_intro/
qed-.
+
+(* Basic properties *********************************************************)
+
+lemma isfin_eq_repl_back: eq_repl_back … isfin.
+#f1 * /3 width=4 by fcla_eq_repl_back, ex_intro/
+qed-.
+
+lemma isfin_eq_repl_fwd: eq_repl_fwd … isfin.
+/3 width=3 by isfin_eq_repl_back, eq_repl_sym/ qed-.
+
+lemma isfin_isid: ∀f. 𝐈⦃f⦄ → 𝐅⦃f⦄.
+/3 width=2 by fcla_isid, ex_intro/ qed.
+
+lemma isfin_push: ∀f. 𝐅⦃f⦄ → 𝐅⦃↑f⦄.
+#f * /3 width=2 by fcla_push, ex_intro/
+qed.
+
+lemma isfin_next: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫯f⦄.
+#f * /3 width=2 by fcla_next, ex_intro/
+qed.
+
+lemma isfin_tl: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫱f⦄.
+#f elim (pn_split f) * #g #H #Hf destruct
+/3 width=3 by isfin_fwd_push, isfin_inv_next/
+qed.
#f1 #f2 #Hf1 #Hf2 #f #Hf elim (sor_isfin_ex … Hf1 … Hf2) -Hf1 -Hf2
/3 width=6 by sor_mono, isfin_eq_repl_back/
qed-.
+
+(* Inversion lemmas on inclusion ********************************************)
+
+corec lemma sor_inv_sle_sn: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f1 ⊆ f.
+#f1 #f2 #f * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0
+/3 width=5 by sle_push, sle_next, sle_weak/
+qed-.
+
+corec lemma sor_inv_sle_dx: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⊆ f.
+#f1 #f2 #f * -f1 -f2 -f
+#f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H0
+/3 width=5 by sle_push, sle_next, sle_weak/
+qed-.
projects / helm.git / commitdiff