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.
#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
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)
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.
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.
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'
projects / helm.git / commitdiff