- some commutations between the rt-steps and the s-steps proved

- some bugs fixed

diff --git a/matita/components/binaries/Makefile b/matita/components/binaries/Makefile
index 15ff284f3485cf56863ea6323f409596dee0fe2c..2f2faf326cda902d4dff123da209d510bce4eab3 100644 (file)
--- a/matita/components/binaries/Makefile
+++ b/matita/components/binaries/Makefile
@@ -4,7 +4,7 @@ H=@
 #CSC: by Andrea
 #BINARIES=extractor  table_creator  utilities saturate transcript
 #FG: my binaries
-BINARIES=mac matex matitadep probe xoa
+BINARIES=matex matitadep probe xoa
 
 all: $(BINARIES:%=rec@all@%) 
 opt: $(BINARIES:%=rec@opt@%)

diff --git a/matita/components/binaries/Makefile.common b/matita/components/binaries/Makefile.common
index 8f8033dbb9f6ad327f65a43c77f2986b3251c537..78733ed391afb90b53d75acc62cc0d30ea3ba228 100644 (file)
--- a/matita/components/binaries/Makefile.common
+++ b/matita/components/binaries/Makefile.common
@@ -9,7 +9,7 @@ OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\"
 OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) 
 OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS)
 
-all:
+opt:
        @echo "  OCAMLBUILD $(EXEC).native" 
        $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" $(EXEC).native 
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
index 73f3be9e7f48bb30597a0689c733e6f73e395eac..afb3e127a6a9b65c02dcd0afe41e0835cb80f1f0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -41,6 +41,13 @@ interpretation "uniform relocation (term)"
 interpretation "generic relocation (term)"
    'RLiftStar f T1 T2 = (lifts f T1 T2).
 
+definition liftable2: predicate (relation term) ≝
+                      λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → 
+                      ∃∃U2. ⬆*[f] T2 ≡ U2 & R U1 U2.
+
+definition deliftable2_sn: predicate (relation term) ≝
+                           λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 →
+                           ∃∃T2. ⬆*[f] T2 ≡ U2 & R T1 T2.
 
 (* Basic inversion lemmas ***************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma
new file mode 100644 (file)
index 0000000..205514c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/syntax/tdeq.ma".
+include "basic_2/relocation/lifts.ma".
+
+(* GENERIC RELOCATION FOR TERMS *********************************************)
+
+(* Properties with degree-based equivalence for terms ***********************)
+
+lemma tdeq_lifts: ∀h,o. liftable2 (tdeq h o).
+#h #o #T1 #T2 #H elim H -T1 -T2 [||| * ]
+[ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort1 … H) -H
+  /3 width=5 by lifts_sort, tdeq_sort, ex2_intro/
+| #i #f #X #H elim (lifts_inv_lref1 … H) -H
+  /3 width=3 by lifts_lref, tdeq_lref, ex2_intro/
+| #l #f #X #H >(lifts_inv_gref1 … H) -H
+  /2 width=3 by lifts_gref, tdeq_gref, ex2_intro/
+| #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H elim (lifts_inv_bind1 … H) -H
+  #W1 #U1 #HVW1 #HTU1 #H destruct
+  elim (IHV … HVW1) -V1 elim (IHT … HTU1) -T1
+  /3 width=5 by lifts_bind, tdeq_pair, ex2_intro/
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H elim (lifts_inv_flat1 … H) -H
+  #W1 #U1 #HVW1 #HTU1 #H destruct
+  elim (IHV … HVW1) -V1 elim (IHT … HTU1) -T1
+  /3 width=5 by lifts_flat, tdeq_pair, ex2_intro/
+]
+qed-.
+
+(* Inversion lemmas with degree-based equivalence for terms *****************)
+
+lemma tdeq_inv_lifts: ∀h,o. deliftable2_sn (tdeq h o).
+#h #o #U1 #U2 #H elim H -U1 -U2 [||| * ]
+[ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort2 … H) -H
+  /3 width=5 by lifts_sort, tdeq_sort, ex2_intro/
+| #i #f #X #H elim (lifts_inv_lref2 … H) -H
+  /3 width=3 by lifts_lref, tdeq_lref, ex2_intro/
+| #l #f #X #H >(lifts_inv_gref2 … H) -H
+  /2 width=3 by lifts_gref, tdeq_gref, ex2_intro/
+| #p #I #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_bind2 … H) -H
+  #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1
+  /3 width=5 by lifts_bind, tdeq_pair, ex2_intro/
+| #I #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_flat2 … H) -H
+  #V1 #T1 #HVW1 #HTU1 #H destruct
+  elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1
+  /3 width=5 by lifts_flat, tdeq_pair, ex2_intro/
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma
index c8aaacf06c83e47e5fd77219d175b55d36acb3bb..8bc29f3016399ac11b58a932cd20647ae81a28f5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma
@@ -14,6 +14,7 @@
 
 (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
 
+include "basic_2/relocation/lifts_tdeq.ma".
 include "basic_2/s_computation/fqus_fqup.ma".
 include "basic_2/rt_transition/cpx_drops.ma".
 
@@ -62,65 +63,67 @@ lemma fqus_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T
 | * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
 ]
 qed-.
-(*
-lemma fqu_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
-                         ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h, o] U2 → (T2 = U2 → ⊥) →
-                         ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
+
+lemma fqu_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
+                           ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
+                           ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
 #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
+[ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❴1❵)
   #U2 #HVU2 @(ex3_intro … U2)
-  [1,3: /3 width=7 by fqu_drop, cpx_delta, drop_pair, drop_drop/
-  | #H destruct
-    lapply (lift_inv_lref2_be … HVU2 ? ?) -HVU2 //
+  [1,3: /3 width=7 by cpx_delta, fqu_drop/
+  | #H lapply (tdeq_inv_lref1 … H) -H
+    #H destruct /2 width=5 by lifts_inv_lref2_uni_lt/
   ]
-| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))
+| #I #G #L #V1 #T #V2 #HV12 #H0 @(ex3_intro … (②{I}V2.T))
   [1,3: /2 width=4 by fqu_pair_sn, cpx_pair_sn/
-  | #H0 destruct /2 width=1 by/
+  | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/
   ]
-| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2))
+| #p #I #G #L #V #T1 #T2 #HT12 #H0 @(ex3_intro … (ⓑ{p,I}V.T2))
   [1,3: /2 width=4 by fqu_bind_dx, cpx_bind/
-  | #H0 destruct /2 width=1 by/
+  | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/
   ]
-| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2))
+| #I #G #L #V #T1 #T2 #HT12 #H0 @(ex3_intro … (ⓕ{I}V.T2))
   [1,3: /2 width=4 by fqu_flat_dx, cpx_flat/
-  | #H0 destruct /2 width=1 by/
+  | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/
+  ]
+| #I #G #L #V #T1 #U1 #HTU1 #T2 #HT12 #H0
+  elim (cpx_lifts … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12 /3 width=1 by drops_refl, drops_drop/
+  #U2 #HTU2 #HU12 @(ex3_intro … U2)
+  [1,3: /3 width=1 by fqu_drop/
+  | #H elim (tdeq_inv_lifts … H … HTU1) -U1
+    #X2 #H <(lifts_inj … HTU2 … H) -U2 /2 width=1 by/
   ]
-| #G #L #K #T1 #U1 #k #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (k+1))
-  #U2 #HTU2 @(ex3_intro … U2)
-  [1,3: /2 width=10 by cpx_lift, fqu_drop/
-  | #H0 destruct /3 width=5 by lift_inj/
 ]
 qed-.
 
-lemma fquq_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
-                          ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h, o] U2 → (T2 = U2 → ⊥) →
-                          ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12
-[ #H12 elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2
+lemma fquq_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
+                            ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
+                            ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 
+[ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2
   /3 width=4 by fqu_fquq, ex3_intro/
 | * #HG #HL #HT destruct /3 width=4 by ex3_intro/
 ]
 qed-.
 
-lemma fqup_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
-                          ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h, o] U2 → (T2 = U2 → ⊥) →
-                          ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
+lemma fqup_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ →
+                            ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
+                            ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄.
 #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
-[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2
+[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2
   /3 width=4 by fqu_fqup, ex3_intro/
 | #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2
-  #U1 #HTU1 #H #H12 elim (fqu_cpx_trans_neq … H1 … HTU1 H) -T1
+  #U1 #HTU1 #H #H12 elim (fqu_cpx_trans_ntdeq … H1 … HTU1 H) -T1
   /3 width=8 by fqup_strap2, ex3_intro/
 ]
 qed-.
 
-lemma fqus_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
-                          ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h, o] U2 → (T2 = U2 → ⊥) →
-                          ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12
-[ #H12 elim (fqup_cpx_trans_neq … H12 … HTU2 H) -T2
+lemma fqus_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ →
+                            ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) →
+                            ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12
+[ #H12 elim (fqup_cpx_trans_ntdeq … H12 … HTU2 H) -T2
   /3 width=4 by fqup_fqus, ex3_intro/
 | * #HG #HL #HT destruct /3 width=4 by ex3_intro/
 ]
 qed-.
-*)
\ No newline at end of file

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml
index 01f59045d18adb38f6dd3652f8002996ac2f282d..d796a4a66c8293d076d36a75083540aeb3e810fc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml
@@ -1,4 +1,6 @@
-let cols = int_of_string (Sys.getenv "COLUMNS")
+let cols =
+   try int_of_string (Sys.getenv "COLUMNS")
+   with Not_found -> failwith "environment variable COLUMNS not visible"
 
 let hl = ref []
 
@@ -52,3 +54,4 @@ let main =
    Array.fast_sort compare files;
    let c = Array.fold_left (write l) 0 files in
    if 0 < c && c < cols then print_newline ();
+

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt
index 716b8611f3d54e8a6fb795dcfa82fdbf136415c4..f2ca8d42aecf8b42249cdd4e3ff8ca84b6e91ed9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt
@@ -1,5 +1,5 @@
 cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma
-cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma
+cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma
 lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma
 cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma
 cpr.ma cpr_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
index b1658534c05551142f02545961b9d2211ecac349..21d140e51abf96759559b202c163d89dd76685f7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
@@ -103,6 +103,12 @@ lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → ∀d. deg h o s1 d
 #s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/  
 qed-.
 
+lemma tdeq_inv_pair: ∀h,o,I,V1,V2,T1,T2. ②{I}V1.T1 ≡[h, o] ②{I}V2.T2 →
+                     V1 ≡[h, o] V2 ∧ T1 ≡[h, o] T2.
+#h #o #I #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H
+#V0 #T0 #HV #HT #H destruct /2 width=1 by conj/
+qed-. 
+
 (* Basic forward lemmas *****************************************************)
 
 lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≡[h, o] Y → ∃J. Y = ⓪{J}.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index a0f7ae830b2ec60fa701a26ad93fcc406ec92c37..d98e42c5cd95ec75e1b07a5179f91373b7ec9125 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -139,7 +139,7 @@ table {
         ]
         [ { "context-sensitive rt-reduction" * } {
              [ "lpx_lleq" * ]
-             [ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ]
+             [ "cpx_lreq" + "cpx_llpx_sn" + "cpx_lleq" * ]
           }
         ]
 *)
@@ -151,7 +151,7 @@ table {
         ]
         [ { "uncounted context-sensitive rt-transition" * } {
              [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ]
-             [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
+             [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" * ]
           }
         ]
         [ { "counted context-sensitive rt-transition" * } {
@@ -223,7 +223,7 @@ table {
         ]
         [ { "generic relocation for terms" * } {
              [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
-             [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_lifts" * ]
+             [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
           }
         ]
         [ { "ranged equivalence for local environments" * } {