From 70ac3a792389497103fb80b5a1a144706addb7cb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 1 Feb 2012 16:19:30 +0000 Subject: [PATCH] - notation fix for reducible and normal forms - some refactoring - improved Makefile produces a table with numerical summary --- .../Basic_2/computation/acp_cr.ma | 2 +- .../Basic_2/grammar/term_simple.ma | 4 +- .../lambda_delta/Basic_2/grammar/thom.ma | 10 ++-- .../contribs/lambda_delta/Basic_2/notation.ma | 38 ++++++++----- .../lambda_delta/Basic_2/reducibility/tif.ma | 54 +++++++++++++++++++ .../lambda_delta/Basic_2/reducibility/tnf.ma | 8 +-- .../reducibility/{tnf_trf.ma => tnf_tif.ma} | 14 ++--- .../lambda_delta/Basic_2/reducibility/tpr.ma | 2 +- .../lambda_delta/Basic_2/reducibility/trf.ma | 53 +++--------------- .../Basic_2/reducibility/twhnf.ma | 4 +- .../lambda_delta/Basic_2/substitution/lift.ma | 4 +- .../lambda_delta/Basic_2/unfold/lifts.ma | 4 +- matita/matita/contribs/lambda_delta/Makefile | 30 +++++++++-- 13 files changed, 140 insertions(+), 87 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/reducibility/tif.ma rename matita/matita/contribs/lambda_delta/Basic_2/reducibility/{tnf_trf.ma => tnf_tif.ma} (86%) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma index 46f864522..fef5e4c92 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma @@ -27,7 +27,7 @@ definition S1 ≝ λRP,C:lenv→predicate term. (* Note: this is Tait's iii, or Girard's CR4 *) definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term. ∀L,Vs. all … (RP L) Vs → - ∀T. 𝕊[T] → NF … (RR L) RS T → C L (ⒶVs.T). + ∀T. 𝐒[T] → NF … (RR L) RS T → C L (ⒶVs.T). (* Note: this is Tait's ii *) definition S3 ≝ λRP,C:lenv→predicate term. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma index 8f7c70374..557299afd 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma @@ -25,12 +25,12 @@ interpretation "simple (term)" 'Simple T = (simple T). (* Basic inversion lemmas ***************************************************) -fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = ⓑ{J} W. U → False. +fact simple_inv_bind_aux: ∀T. 𝐒[T] → ∀J,W,U. T = ⓑ{J} W. U → False. #T * -T [ #I #J #W #U #H destruct | #I #V #T #J #W #U #H destruct ] qed. -lemma simple_inv_bind: ∀I,V,T. 𝕊[ⓑ{I} V. T] → False. +lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → False. /2 width=6/ qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma index 149b27a17..153492028 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma @@ -19,7 +19,7 @@ include "Basic_2/grammar/term_simple.ma". inductive thom: relation term ≝ | thom_atom: ∀I. thom (⓪{I}) (⓪{I}) | thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2) - | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] → + | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝐒[T1] → 𝐒[T2] → thom (ⓐV1. T1) (ⓐV2. T2) . @@ -38,13 +38,13 @@ qed. lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1. /3 width=2/ qed. -lemma simple_thom_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝕊[T1] → 𝕊[T2]. +lemma simple_thom_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝐒[T1] → 𝐒[T2]. #T1 #T2 #H elim H -T1 -T2 // #V1 #V2 #T1 #T2 #H elim (simple_inv_bind … H) qed. (**) (* remove from index *) -lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1]. +lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝐒[T2] → 𝐒[T1]. /3 width=3/ qed-. (* Basic inversion lemmas ***************************************************) @@ -63,7 +63,7 @@ lemma thom_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 → /2 width=5/ qed-. fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 → - ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] & + ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] & I = Appl & T2 = ⓐW2. U2. #T1 #T2 * -T1 -T2 [ #J #I #W1 #U1 #H destruct @@ -73,7 +73,7 @@ fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 qed. lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 → - ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] & + ∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] & I = Appl & T2 = ⓐW2. U2. /2 width=4/ qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma index f10f7b4f6..c25341f63 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma @@ -104,7 +104,7 @@ notation "hvbox( # [ x , break y ] )" non associative with precedence 90 for @{ 'Weight $x $y }. -notation "hvbox( 𝕊 [ T ] )" +notation "hvbox( 𝐒 [ T ] )" non associative with precedence 45 for @{ 'Simple $T }. @@ -114,6 +114,18 @@ notation "hvbox( T1 break [ d , break e ] ≼ break T2 )" (* Substitution *************************************************************) +notation "hvbox( L ⊢ break [ d , break e ] break 𝐑 [ T ] )" + non associative with precedence 45 + for @{ 'Reducible $L $d $e $T }. + +notation "hvbox( L ⊢ break [ d , break e ] break 𝐈 [ T ] )" + non associative with precedence 45 + for @{ 'NotReducible $L $d $e $T }. + +notation "hvbox( L ⊢ break [ d , break e ] break 𝐍 [ T ] )" + non associative with precedence 45 + for @{ 'Normal $L $d $e $T }. + notation "hvbox( ⇧ [ d , break e ] break T1 ≡ break T2 )" non associative with precedence 45 for @{ 'RLift $d $e $T1 $T2 }. @@ -180,51 +192,51 @@ notation "hvbox( T1 ÷ ⊑ break T2 )" (* Reducibility *************************************************************) -notation "hvbox( ℝ [ T ] )" +notation "hvbox( 𝐑 [ T ] )" non associative with precedence 45 for @{ 'Reducible $T }. -notation "hvbox( L ⊢ ℝ [ T ] )" +notation "hvbox( L ⊢ break 𝐑 [ T ] )" non associative with precedence 45 for @{ 'Reducible $L $T }. -notation "hvbox( 𝕀 [ T ] )" +notation "hvbox( 𝐈 [ T ] )" non associative with precedence 45 for @{ 'NotReducible $T }. -notation "hvbox( L ⊢ 𝕀 [ T ] )" +notation "hvbox( L ⊢ break 𝐈 [ T ] )" non associative with precedence 45 for @{ 'NotReducible $L $T }. -notation "hvbox( ℕ [ T ] )" +notation "hvbox( 𝐍 [ T ] )" non associative with precedence 45 for @{ 'Normal $T }. -notation "hvbox( L ⊢ ℕ [ T ] )" +notation "hvbox( L ⊢ break 𝐍 [ T ] )" non associative with precedence 45 for @{ 'Normal $L $T }. -notation "hvbox( 𝕎ℍℝ [ T ] )" +notation "hvbox( 𝐖𝐇𝐑 [ T ] )" non associative with precedence 45 for @{ 'WHdReducible $T }. -notation "hvbox( L ⊢ 𝕎ℍℝ [ T ] )" +notation "hvbox( L ⊢ break 𝐖𝐇𝐑 [ T ] )" non associative with precedence 45 for @{ 'WHdReducible $L $T }. -notation "hvbox( 𝕎ℍ𝕀 [ T ] )" +notation "hvbox( 𝐖𝐇𝐈 [ T ] )" non associative with precedence 45 for @{ 'NotWHdReducible $T }. -notation "hvbox( L ⊢ 𝕎ℍ𝕀 [ T ] )" +notation "hvbox( L ⊢ break 𝐖𝐇𝐈 [ T ] )" non associative with precedence 45 for @{ 'NotWHdReducible $L $T }. -notation "hvbox( 𝕎ℍℕ [ T ] )" +notation "hvbox( 𝐖𝐇𝐍 [ T ] )" non associative with precedence 45 for @{ 'WHdNormal $T }. -notation "hvbox( L ⊢ 𝕎ℍℕ [ T ] )" +notation "hvbox( L ⊢ break 𝐖𝐇𝐍 [ T ] )" non associative with precedence 45 for @{ 'WHdNormal $L $T }. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tif.ma new file mode 100644 index 000000000..5b89755a7 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tif.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/trf.ma". + +(* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************) + +definition tif: predicate term ≝ λT. 𝐑[T] → False. + +interpretation "context-free irreducibility (term)" + 'NotReducible T = (tif T). + +(* Basic inversion lemmas ***************************************************) + +lemma tif_inv_abbr: ∀V,T. 𝐈[ⓓV.T] → False. +/2 width=1/ qed-. + +lemma tif_inv_abst: ∀V,T. 𝐈[ⓛV.T] → 𝐈[V] ∧ 𝐈[T]. +/4 width=1/ qed-. + +lemma tif_inv_appl: ∀V,T. 𝐈[ⓐV.T] → ∧∧ 𝐈[V] & 𝐈[T] & 𝐒[T]. +#V #T #HVT @and3_intro /3 width=1/ +generalize in match HVT; -HVT elim T -T // +* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/ +qed-. + +lemma tif_inv_cast: ∀V,T. 𝐈[ⓣV.T] → False. +/2 width=1/ qed-. + +(* Basic properties *********************************************************) + +lemma tif_atom: ∀I. 𝐈[⓪{I}]. +/2 width=4/ qed. + +lemma tif_abst: ∀V,T. 𝐈[V] → 𝐈[T] → 𝐈[ⓛV.T]. +#V #T #HV #HT #H +elim (trf_inv_abst … H) -H /2 width=1/ +qed. + +lemma tif_appl: ∀V,T. 𝐈[V] → 𝐈[T] → 𝐒[T] → 𝐈[ⓐV.T]. +#V #T #HV #HT #S #H +elim (trf_inv_appl … H) -H /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma index 8c84f092c..5a7205cc0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma @@ -24,14 +24,14 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma tnf_inv_abst: ∀V,T. ℕ[ⓛV.T] → ℕ[V] ∧ ℕ[T]. +lemma tnf_inv_abst: ∀V,T. 𝐍[ⓛV.T] → 𝐍[V] ∧ 𝐍[T]. #V1 #T1 #HVT1 @conj [ #V2 #HV2 lapply (HVT1 (ⓛV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (ⓛV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // ] qed-. -lemma tnf_inv_appl: ∀V,T. ℕ[ⓐV.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T]. +lemma tnf_inv_appl: ∀V,T. 𝐍[ⓐV.T] → ∧∧ 𝐍[V] & 𝐍[T] & 𝐒[T]. #V1 #T1 #HVT1 @and3_intro [ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // @@ -42,7 +42,7 @@ lemma tnf_inv_appl: ∀V,T. ℕ[ⓐV.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T]. ] qed-. -lemma tnf_inv_abbr: ∀V,T. ℕ[ⓓV.T] → False. +lemma tnf_inv_abbr: ∀V,T. 𝐍[ⓓV.T] → False. #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU lapply (H U ?) -H /2 width=3/ #H destruct @@ -53,7 +53,7 @@ lemma tnf_inv_abbr: ∀V,T. ℕ[ⓓV.T] → False. ] qed. -lemma tnf_inv_cast: ∀V,T. ℕ[ⓣV.T] → False. +lemma tnf_inv_cast: ∀V,T. 𝐍[ⓣV.T] → False. #V #T #H lapply (H T ?) -H /2 width=1/ #H @(discr_tpair_xy_y … H) qed-. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_trf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_tif.ma similarity index 86% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_trf.ma rename to matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_tif.ma index 3ffafb2c8..2888ff9d6 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_trf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_tif.ma @@ -13,14 +13,14 @@ (**************************************************************************) include "Basic_2/substitution/tps_lift.ma". -include "Basic_2/reducibility/trf.ma". +include "Basic_2/reducibility/tif.ma". include "Basic_2/reducibility/tnf.ma". (* CONTEXT-FREE NORMAL TERMS ************************************************) (* Main properties properties ***********************************************) -lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝕀[T1] → T1 = T2. +lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝐈[T1] → T1 = T2. #T1 #T2 #H elim H -T1 -T2 [ // | * #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H @@ -47,11 +47,11 @@ lemma tpr_tif_eq: ∀T1,T2. T1 ➡ T2 → 𝕀[T1] → T1 = T2. ] qed. -theorem tif_tnf: ∀T1. 𝕀[T1] → ℕ[T1]. +theorem tif_tnf: ∀T1. 𝐈[T1] → 𝐍[T1]. /2 width=1/ qed. (* Note: this property is unusual *) -lemma tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False. +lemma tnf_trf_false: ∀T1. 𝐑[T1] → 𝐍[T1] → False. #T1 #H elim H -T1 [ #V #T #_ #IHV #H elim (tnf_inv_abst … H) -H /2 width=1/ | #V #T #_ #IHT #H elim (tnf_inv_abst … H) -H /2 width=1/ @@ -64,11 +64,11 @@ lemma tnf_trf_false: ∀T1. ℝ[T1] → ℕ[T1] → False. ] qed. -theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1]. +theorem tnf_tif: ∀T1. 𝐍[T1] → 𝐈[T1]. /2 width=3/ qed. -lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[ⓛV.T]. +lemma tnf_abst: ∀V,T. 𝐍[V] → 𝐍[T] → 𝐍[ⓛV.T]. /4 width=1/ qed. -lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[ⓐV.T]. +lemma tnf_appl: ∀V,T. 𝐍[V] → 𝐍[T] → 𝐒[T] → 𝐍[ⓐV.T]. /4 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma index c2508c851..0edd15211 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma @@ -156,7 +156,7 @@ elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct qed-. (* Note: the main property of simple terms *) -lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝕊[T1] → +lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒[T1] → ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U = ⓐV2. T2. #V1 #T1 #U #H #HT1 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma index 67fcf4b67..3ae5bfd17 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma @@ -14,7 +14,7 @@ include "Basic_2/grammar/term_simple.ma". -(* CONTEXT-FREE REDUCIBLE AND IRREDUCIBLE TERMS *****************************) +(* CONTEXT-FREE REDUCIBLE TERMS *********************************************) (* reducible terms *) inductive trf: predicate term ≝ @@ -31,16 +31,9 @@ interpretation "context-free reducibility (term)" 'Reducible T = (trf T). -(* irreducible terms *) -definition tif: predicate term ≝ λT. ℝ[T] → False. - -interpretation - "context-free irreducibility (term)" - 'NotReducible T = (tif T). - (* Basic inversion lemmas ***************************************************) -fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T = ⓪{I} → False. +fact trf_inv_atom_aux: ∀I,T. 𝐑[T] → T = ⓪{I} → False. #I #T * -T [ #V #T #_ #H destruct | #V #T #_ #H destruct @@ -52,10 +45,10 @@ fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T = ⓪{I} → False. ] qed. -lemma trf_inv_atom: ∀I. ℝ[⓪{I}] → False. +lemma trf_inv_atom: ∀I. 𝐑[⓪{I}] → False. /2 width=4/ qed-. -fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = ⓛW. U → ℝ[W] ∨ ℝ[U]. +fact trf_inv_abst_aux: ∀W,U,T. 𝐑[T] → T = ⓛW. U → 𝐑[W] ∨ 𝐑[U]. #W #U #T * -T [ #V #T #HV #H destruct /2 width=1/ | #V #T #HT #H destruct /2 width=1/ @@ -67,11 +60,11 @@ fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = ⓛW. U → ℝ[W] ∨ ℝ[U]. ] qed. -lemma trf_inv_abst: ∀V,T. ℝ[ⓛV.T] → ℝ[V] ∨ ℝ[T]. +lemma trf_inv_abst: ∀V,T. 𝐑[ⓛV.T] → 𝐑[V] ∨ 𝐑[T]. /2 width=3/ qed-. -fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = ⓐW. U → - ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False). +fact trf_inv_appl_aux: ∀W,U,T. 𝐑[T] → T = ⓐW. U → + ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False). #W #U #T * -T [ #V #T #_ #H destruct | #V #T #_ #H destruct @@ -84,35 +77,5 @@ fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = ⓐW. U → ] qed. -lemma trf_inv_appl: ∀W,U. ℝ[ⓐW.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False). +lemma trf_inv_appl: ∀W,U. 𝐑[ⓐW.U] → ∨∨ 𝐑[W] | 𝐑[U] | (𝐒[U] → False). /2 width=3/ qed-. - -lemma tif_inv_abbr: ∀V,T. 𝕀[ⓓV.T] → False. -/2 width=1/ qed-. - -lemma tif_inv_abst: ∀V,T. 𝕀[ⓛV.T] → 𝕀[V] ∧ 𝕀[T]. -/4 width=1/ qed-. - -lemma tif_inv_appl: ∀V,T. 𝕀[ⓐV.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T]. -#V #T #HVT @and3_intro /3 width=1/ -generalize in match HVT; -HVT elim T -T // -* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/ -qed-. - -lemma tif_inv_cast: ∀V,T. 𝕀[ⓣV.T] → False. -/2 width=1/ qed-. - -(* Basic properties *********************************************************) - -lemma tif_atom: ∀I. 𝕀[⓪{I}]. -/2 width=4/ qed. - -lemma tif_abst: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕀[ⓛV.T]. -#V #T #HV #HT #H -elim (trf_inv_abst … H) -H /2 width=1/ -qed. - -lemma tif_appl: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕊[T] → 𝕀[ⓐV.T]. -#V #T #HV #HT #S #H -elim (trf_inv_appl … H) -H /2 width=1/ -qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma index 1ee06ad02..2497ea273 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma @@ -25,7 +25,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma twhnf_inv_thom: ∀T. 𝕎ℍℕ[T] → T ≈ T. +lemma twhnf_inv_thom: ∀T. 𝐖𝐇𝐍[T] → T ≈ T. normalize /2 width=1/ qed-. @@ -52,5 +52,5 @@ lemma tpr_thom: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2. ] qed. -lemma twhnf_thom: ∀T. T ≈ T → 𝕎ℍℕ[T]. +lemma twhnf_thom: ∀T. T ≈ T → 𝐖𝐇𝐍[T]. /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma index f9d1ddb93..cb8aac3a0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma @@ -271,13 +271,13 @@ lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → #[T1] = #[T2]. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize // qed-. -lemma lift_simple_dx: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2]. +lemma lift_simple_dx: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2]. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 // #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H elim (simple_inv_bind … H) qed-. -lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1]. +lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1]. #d #e #T1 #T2 #H elim H -d -e -T1 -T2 // #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H elim (simple_inv_bind … H) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma index 57405868f..6a3c647a0 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma @@ -112,11 +112,11 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2]. +lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2]. #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/ qed-. -lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1]. +lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1]. #T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/ qed-. diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 10271b7ce..e5a20a1f3 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -25,6 +25,13 @@ stats: $(PACKAGES:%=%.stats) %.stats: CHARS = $(shell cat $(MAS) | wc -c) +%.stats: C1 = $(shell grep "inductive\|record" $(MAS) | wc -l) +%.stats: C2 = $(shell grep "definition\|let rec" $(MAS) | wc -l) +%.stats: P1 = $(shell grep "theorem " $(MAS) | wc -l) +%.stats: P2 = $(shell grep "lemma " $(MAS) | wc -l) + +%.stats: TBL = ld_$*_sum + %.stats: @printf '\x1B[1;40;37m' @printf '%-15s %-42s' 'Statistics for:' $* @@ -42,9 +49,9 @@ stats: $(PACKAGES:%=%.stats) # @printf ' %-6s %3i' Files `ls *.v | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;32m' - @printf '%-8s %6i' Theorems `grep theorem $(MAS) | wc -l` - @printf ' %-8s %5i' Lemmas `grep lemma $(MAS) | wc -l` - @printf ' %-6s %3i' Facts `grep fact $(MAS) | wc -l` + @printf '%-8s %6i' Theorems `grep "theorem " $(MAS) | wc -l` + @printf ' %-8s %5i' Lemmas `grep "lemma " $(MAS) | wc -l` + @printf ' %-6s %3i' Facts `grep "fact " $(MAS) | wc -l` @printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l` @printf '\x1B[0m\n' @printf '\x1B[1;40;33m' @@ -58,3 +65,20 @@ stats: $(PACKAGES:%=%.stats) @printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` @printf ' %-10s' '' @printf '\x1B[0m\n' + @printf 'name "$(TBL)"\n\n' > $*/$(TBL).tbl + @printf 'table {\n' >> $*/$(TBL).tbl + @printf ' class "grey" [ "category"\n' >> $*/$(TBL).tbl + @printf ' [ "objects" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf ' class "green" [ "propositions"\n' >> $*/$(TBL).tbl + @printf ' [ "theorems" "$(P1)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "lemmas" "$(P2)" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf ' class "yellow" [ "concepts"\n' >> $*/$(TBL).tbl + @printf ' [ "declared" "$(C1)" * ]\n' >> $*/$(TBL).tbl + @printf ' [ "defined" "$(C2)" * ]\n' >> $*/$(TBL).tbl + @printf ' ]\n' >> $*/$(TBL).tbl + @printf '}\n\n' >> $*/$(TBL).tbl + @printf 'class "component" { 0 }\n\n' >> $*/$(TBL).tbl + @printf 'class "plane" { 1 } { 3 } \n\n' >> $*/$(TBL).tbl + @printf 'class "number" { 2 } { 4 } \n\n' >> $*/$(TBL).tbl -- 2.39.2