From ffe34220d80cba65eccf2396fba7f692cc6448c8 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 25 Aug 2011 13:20:47 +0000
Subject: [PATCH] - weakening leq, we proved cpr_bind_dx - we imple,ented some
 statistics in the Makefile

---
 .../lambda-delta/Basic-2/reduction/cpr.ma     | 21 ++++++-----
 .../lambda-delta/Basic-2/substitution/drop.ma |  2 +-
 .../lambda-delta/Basic-2/substitution/leq.ma  | 25 ++-----------
 matita/matita/contribs/lambda-delta/Makefile  | 37 ++++++++++++++++++-
 4 files changed, 51 insertions(+), 34 deletions(-)

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
index 090c6cf6f..245cadff9 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
@@ -33,18 +33,19 @@ lemma cpr_tps: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 ⇒ T2.
 
 lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
 /2/ qed.
-(*
-(* NOTE: new property *)
-lemma cpr_bind: ∀I,L,V1,V2,T1,T2.
-                V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 → L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+
+lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 →
+                   L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 * /3 width=5/
+qed.
+
+lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 →
+                   L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
 elim (tps_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-@ex2_1_intro
-[3: @tps_bind [3: // |4: @HT02 |1,2: skip ]
-|1: skip
-|2: @tpr_delta [2: @HV12 |3: @HT1 |1: skip |6: ]
-]   
-*)
+lapply (tps_leq_repl … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0 /3 width=5/
+qed.
+
 (* NOTE: new property *)
 lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
                 L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2.
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma
index f9219f27f..a6752fac6 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/drop.ma
@@ -141,7 +141,7 @@ lemma drop_leq_drop1: ∀L1,L2,d,e. L1 [d, e] ≈ L2 →
 #L1 #L2 #d #e #H elim H -H L1 L2 d e
 [ #d #e #I #K1 #V #i #H
   lapply (drop_inv_sort1 … H) -H #H destruct
-| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #I #K1 #V #i #_ #_ #H
+| #L1 #L2 #I #K1 #V #i #_ #_ #H
   elim (lt_zero_false … H)
 | #L1 #L2 #I #V #e #HL12 #IHL12 #J #K1 #W #i #H #_ #Hie
   elim (drop_inv_O1 … H) -H * #Hi #HLK1
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma
index 7f5c12e01..7612bcb85 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/leq.ma
@@ -18,8 +18,7 @@ include "Basic-2/grammar/lenv_length.ma".
 
 inductive leq: lenv → nat → nat → lenv → Prop ≝
 | leq_sort: ∀d,e. leq (⋆) d e (⋆)
-| leq_comp: ∀L1,L2,I1,I2,V1,V2.
-            leq L1 0 0 L2 → leq (L1. 𝕓{I1} V1) 0 0 (L2. 𝕓{I2} V2)
+| leq_OO:   ∀L1,L2. leq L1 0 0 L2
 | leq_eq:   ∀L1,L2,I,V,e. leq L1 0 e L2 → leq (L1. 𝕓{I} V) 0 (e + 1) (L2.𝕓{I} V)
 | leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
             leq L1 d e L2 → leq (L1. 𝕓{I1} V1) (d + 1) e (L2. 𝕓{I2} V2)
@@ -31,7 +30,7 @@ interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2).
 
 lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
 #d elim d -d
-[ #e elim e -e [ #L elim L -L /2/ | #e #IHe #L elim L -L /2/ ]
+[ #e elim e -e // #e #IHe #L elim L -L /2/
 | #d #IHd #e #L elim L -L /2/
 ]
 qed.
@@ -43,25 +42,7 @@ qed.
 lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d →
                    ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2.
 
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ 
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
 qed.
 
-lemma leq_fwd_length: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → |L1| = |L2|.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize //
-qed.  
-
 (* Basic inversion lemmas ***************************************************)
-
-lemma leq_inv_sort1_aux: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e
-[ //
-| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #H destruct
-| #L1 #L2 #I #V #e #_ #_ #H destruct
-| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #_ #H destruct
-qed.
-
-lemma leq_inv_sort1: ∀L2,d,e. ⋆ [d, e] ≈ L2 → L2 = ⋆.
-/2 width=5/ qed.
-
-lemma leq_inv_sort2: ∀L1,d,e. L1 [d, e] ≈ ⋆ → L1 = ⋆.
-/3/ qed.
diff --git a/matita/matita/contribs/lambda-delta/Makefile b/matita/matita/contribs/lambda-delta/Makefile
index b435949e3..978291c7d 100644
--- a/matita/matita/contribs/lambda-delta/Makefile
+++ b/matita/matita/contribs/lambda-delta/Makefile
@@ -5,8 +5,43 @@ XOA     = xoa.native
 CONF    = Ground-2/xoa.conf.xml
 TARGETS = Ground-2/xoa_natation.ma Ground-2/xoa.ma
 
-all: $(TARGETS)
+all:
+
+xoa: $(TARGETS)
 
 $(TARGETS): $(CONF)
 	@echo "  EXEC $(XOA) $(CONF)"
 	$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(CONF)
+
+stats: MAS = $(shell find -name "*.ma")
+
+stats: CHARS = $(shell cat $(MAS) | wc -c)
+
+stats:
+	@printf '\e[1;40;35m'
+	@printf '%-8s %6i' Chars $(CHARS)
+	@printf '   %-8s %5i' Lines `cat $(MAS) | wc -l`
+	@printf '   %-6s %3i' Pages `echo $$(($(CHARS) / 5120))`
+	@printf '\e[0m\n'
+	@printf '\e[1;40;36m'
+	@printf '%-8s %6i' Sources `ls $(MAS) | wc -l`
+	@printf '   %-27s' ''
+#	@printf '   %-8s %5i' Objs `ls *.vo | wc -l`
+#	@printf '   %-6s %3i' Files `ls *.v | wc -l`
+	@printf '\e[0m\n'	
+	@printf '\e[1;40;32m'
+	@printf '%-8s %6i' Theorems `grep theorem $(MAS) | wc -l`
+	@printf '   %-8s %5i' Lemmas `grep lemma $(MAS) | wc -l`
+	@printf '   %-6s %3i' Proofs `grep qed $(MAS) | wc -l`	
+#	@printf '   %-9s %3i' Generated `grep Derive *.v | wc -l`
+	@printf '\e[0m\n'	
+	@printf '\e[1;40;33m'
+	@printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l` 
+	@printf '   %-27s' ''
+#	@printf '   %-8s %5i' Local `grep "Local" *.v | wc -l`
+	@printf '\e[0m\n'
+	@printf '\e[1;40;31m'
+	@printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l`
+	@printf '   %-8s %5i' Comments `grep "(\*[^*]*$$" $(MAS) | wc -l`
+	@printf '   %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
+	@printf '\e[0m\n'
-- 
2.39.2