From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 13 Oct 2014 22:02:52 +0000 (+0000)
Subject: - lambdadelta: minor corrections
X-Git-Tag: make_still_working~818
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=47bffe161a4be4a4d06f259215c4ccd7c2e56ad6;p=helm.git

- lambdadelta: minor corrections
- predefined_virtuals: some additions
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
index e8ecc622c..730714b5c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma
@@ -42,45 +42,45 @@ qed-.
 
 (* Basic_1: was: pc3_refl *)
 lemma cpcs_refl: ∀G,L. reflexive … (cpcs G L).
-/2 width=1/ qed.
+/2 width=1 by inj/ qed.
 
 (* Basic_1: was: pc3_s *)
 lemma cpcs_sym: ∀G,L. symmetric … (cpcs G L).
-#G #L @TC_symmetric // qed.
+#G #L @TC_symmetric // qed-.
 
-lemma cpc_cpcs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T2.
-/2 width=1/ qed.
+lemma cpc_cpcs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
+/2 width=1 by inj/ qed.
 
 lemma cpcs_strap1: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L @step qed.
+#G #L @step qed-.
 
 lemma cpcs_strap2: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L @TC_strap qed.
+#G #L @TC_strap qed-.
 
 (* Basic_1: was: pc3_pr2_r *)
 lemma cpr_cpcs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=1/ qed.
+/3 width=1 by cpc_cpcs, or_introl/ qed.
 
 (* Basic_1: was: pc3_pr2_x *)
 lemma cpr_cpcs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡ T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=1/ qed.
+/3 width=1 by cpc_cpcs, or_intror/ qed.
 
 lemma cpcs_cpr_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3/ qed.
+/3 width=3 by cpcs_strap1, or_introl/ qed-.
 
 (* Basic_1: was: pc3_pr2_u *)
 lemma cpcs_cpr_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3/ qed.
+/3 width=3 by cpcs_strap2, or_introl/ qed-.
 
 lemma cpcs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3/ qed.
+/3 width=3 by cpcs_strap1, or_intror/ qed-.
 
 lemma cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3/ qed-.
+/3 width=3 by cpr_cpcs_dx, cpcs_strap1, or_intror/ qed-.
 
 (* Basic_1: was: pc3_pr2_u2 *)
 lemma cpcs_cpr_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-/3 width=3/ qed.
+/3 width=3 by cpcs_strap2, or_intror/ qed-.
 
 (* Basic_1: removed theorems 9:
             clear_pc3_trans pc3_ind_left
diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma
index 69641dbf7..1f437491f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma
@@ -21,35 +21,35 @@ include "basic_2/equivalence/cpcs.ma".
 
 (* Basic_1: was: pc3_pr3_r *)
 lemma cpcs_cprs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /3 width=3/
+#G #L #T1 #T2 #H @(cprs_ind … H) -T2 /3 width=3 by cpcs_cpr_strap1, cpcs_strap1, cpc_cpcs/
 qed.
 
 (* Basic_1: was: pc3_pr3_x *)
 lemma cpcs_cprs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡* T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /3 width=3/
+#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /3 width=3 by cpcs_cpr_div, cpcs_strap1, cpcs_cprs_dx/
 qed.
 
 lemma cpcs_cprs_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /2 width=3/
-qed.
+#G #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /2 width=3 by cpcs_cpr_strap1/
+qed-.
 
 lemma cpcs_cprs_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /width=1/ /2 width=3/
-qed.
+#G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /2 width=3 by cpcs_cpr_strap2/
+qed-.
 
 lemma cpcs_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /2 width=3/
-qed.
+#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_div/
+qed-.
 
 (* Basic_1: was: pc3_pr3_conf *)
 lemma cpcs_cprs_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /width=1/ /2 width=3/
-qed.
+#G #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /2 width=3 by cpcs_cpr_conf/
+qed-.
 
 (* Basic_1: was: pc3_pr3_t *)
 (* Basic_1: note: pc3_pr3_t should be renamed *)
 lemma cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
-#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=1/ /2 width=3/
+#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_div, cpcs_cprs_dx/
 qed.
 
 lemma cprs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma
index 27a0e473f..4ad9ae29e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma
@@ -38,7 +38,7 @@ lemma fqu_lpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T
 /3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
 [ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
   #K2 #W2 #HLK2 #HVW2 #H destruct
-  /3 width=5 by fqu_fquq, cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
+  /3 width=5 by cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
 | #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #K2 #HK12
   elim (drop_lpx_trans … HLK1 … HK12) -HK12
   /3 width=7 by fqu_drop, ex3_2_intro/
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 91b69fc6c..3b04c75b3 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1524,8 +1524,8 @@ let predefined_classes = [
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "（"; ];
  [")"; "❩"; "❫"; "❳"; "）"; ];
- ["["; "〚"; ] ;
- ["]"; "〛"; ] ;
+ ["["; "⦋"; "〚"; ] ;
+ ["]"; "⦌"; "〛"; ] ;
  ["{"; "❴"; "⦃" ] ;
  ["}"; "❵"; "⦄" ] ;
  ["□"; "◽"; "▪"; "◾"; ];