From ebc170efe71cf4ee842acfbe58bb6864e76ba98c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 23 Mar 2016 19:10:29 +0000 Subject: [PATCH] - ng_kernel: we print the offending term when guarded_by_constructors fails - probe: we print the roots when more than one root is found - lambdadelta: first working commit for the "relocation" component --- matita/components/binaries/probe/engine.ml | 8 +- .../components/ng_kernel/nCicTypeChecker.ml | 2 +- .../basic_2/etc_new/drops/drops_length.etc | 61 --------- .../basic_2/etc_new/frees/frees_length.etc | 26 ++++ .../basic_2/grammar/lenv_length.ma | 12 +- .../basic_2/relocation/drops_length.ma | 126 ++++++++++++++++++ .../lambdadelta/basic_2/relocation/frees.ma | 41 ++++-- .../basic_2/relocation/frees_lreq.ma | 40 ++++++ .../basic_2/relocation/frees_weight.ma | 43 ++++++ .../basic_2/relocation/{fleq.ma => freq.ma} | 33 +++-- .../relocation/{fleq_fleq.ma => freq_freq.ma} | 27 ++-- .../lambdadelta/basic_2/relocation/lexs.ma | 7 + .../lambdadelta/basic_2/relocation/lreq.ma | 3 + .../lambdadelta/ground_2/lib/arith.ma | 3 + .../ground_2/relocation/rtmap_fcla.ma | 16 +++ .../ground_2/relocation/rtmap_isfin.ma | 45 ++++--- .../ground_2/relocation/rtmap_sor.ma | 14 ++ 17 files changed, 379 insertions(+), 128 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_length.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma rename matita/matita/contribs/lambdadelta/basic_2/relocation/{fleq.ma => freq.ma} (57%) rename matita/matita/contribs/lambdadelta/basic_2/relocation/{fleq_fleq.ma => freq_freq.ma} (56%) diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index 5117f57fc..c959e648c 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -24,8 +24,8 @@ let unsupported protocol = 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 @@ -50,8 +50,8 @@ let get_uri str = | [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 diff --git a/matita/components/ng_kernel/nCicTypeChecker.ml b/matita/components/ng_kernel/nCicTypeChecker.ml index 6871dc6ee..b60734508 100644 --- a/matita/components/ng_kernel/nCicTypeChecker.ml +++ b/matita/components/ng_kernel/nCicTypeChecker.ml @@ -1329,7 +1329,7 @@ let typecheck_obj status (uri,height,metasenv,subst,kind) = (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 ;; diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc index a0926cad1..667f9689d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc @@ -1,5 +1,3 @@ -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 @@ -90,58 +88,6 @@ lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L ] 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 @@ -151,13 +97,6 @@ elim (drop_conf_lt … HLK … HLK0 … H0) -HLK -HLK0 -H0 #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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_length.etc new file mode 100644 index 000000000..292525b1b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees_length.etc @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma index f608f8c3c..a7a99ba01 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma @@ -41,16 +41,18 @@ 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 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma new file mode 100644 index 000000000..b553a9c69 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma @@ -0,0 +1,126 @@ +(**************************************************************************) +(* ___ *) +(* ||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 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma index dee6950e3..e5e5b098c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma @@ -40,11 +40,21 @@ interpretation (* 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-. @@ -56,12 +66,12 @@ fact frees_inv_gref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x #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 → @@ -72,8 +82,8 @@ 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-. @@ -91,8 +101,8 @@ fact frees_inv_lref_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀j. X = #(⫯j | #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-. @@ -109,8 +119,8 @@ fact frees_inv_bind_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T,a. X = | #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-. @@ -126,8 +136,8 @@ fact frees_inv_flat_aux: ∀L,X,f. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = | #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-. @@ -136,6 +146,13 @@ lemma frees_inv_flat: ∀I,L,V,T,f. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f → ∃∃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). @@ -147,7 +164,7 @@ lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ 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/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma new file mode 100644 index 000000000..d0231ec6a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_lreq.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma new file mode 100644 index 000000000..c8b3b7f46 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees_weight.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma similarity index 57% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma index 1ca5528a6..c9a335348 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma @@ -12,32 +12,39 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeq_7.ma". +include "basic_2/notation/relations/lazyeq_6.ma". include "basic_2/grammar/genv.ma". -include "basic_2/multiple/lleq.ma". +include "basic_2/relocation/frees_weight.ma". +include "basic_2/relocation/frees_lreq.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 +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 - "lazy equivalence (closure)" - 'LazyEq l G1 L1 T1 G2 L2 T2 = (fleq l G1 L1 T1 G2 L2 T2). + "ranged equivalence (closure)" + 'LazyEq G1 L1 T1 G2 L2 T2 = (freq G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma fleq_refl: ∀l. tri_reflexive … (fleq l). -/2 width=1 by fleq_intro/ qed. +lemma freq_refl: tri_reflexive … freq. +#G #L #T elim (frees_total L T) /2 width=3 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/ +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 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/ +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 +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fleq_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq_freq.ma similarity index 56% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fleq_fleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/freq_freq.ma index 915be044e..dafa01768 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fleq_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq_freq.ma @@ -12,23 +12,26 @@ (* *) (**************************************************************************) -include "basic_2/multiple/lleq_lleq.ma". -include "basic_2/multiple/fleq.ma". +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 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/ +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 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 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 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-. +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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index 8140a5d31..a79a3e4d9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -145,6 +145,13 @@ lemma lexs_inv_push: ∀RN,RP,I1,I2,L1,L2,V1,V2,f. #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). diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma index 58914d3a6..20541fef7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma @@ -91,6 +91,9 @@ lemma lreq_inv_push: ∀I1,I2,L1,L2,V1,V2,f. #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 *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index d70ea1bfa..3cb9e9f30 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -155,6 +155,9 @@ qed. 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-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma index 14542cf48..26af72dfa 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma @@ -58,6 +58,22 @@ lemma fcla_inv_xp: ∀g,m. 𝐂⦃g⦄ ≡ m → 0 = m → 𝐈⦃g⦄. #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). diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma index 45c8ea854..0c9a65bf2 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma @@ -23,26 +23,6 @@ definition isfin: predicate rtmap ≝ 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) → @@ -65,3 +45,28 @@ qed-. 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. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma index b93214bea..e76c1ca3c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma @@ -176,3 +176,17 @@ lemma sor_isfin: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∀f. f1 ⋓ f2 ≡ #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-. -- 2.39.2