From aec661d51ffa04b4248cdfece772b58780737e3f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 4 Nov 2011 11:59:52 +0000 Subject: [PATCH] - two discrimination lemmas - some decidability axioms (proof postponed) --- .../contribs/lambda_delta/Basic_2/Basic_1.txt | 5 ----- .../lambda_delta/Basic_2/grammar/item.ma | 14 +++++++++++- .../lambda_delta/Basic_2/grammar/term.ma | 22 +++++++++++++++++++ .../contribs/lambda_delta/Ground_2/arith.ma | 6 ++++- .../contribs/lambda_delta/Ground_2/star.ma | 3 +++ 5 files changed, 43 insertions(+), 7 deletions(-) diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt index f8c868a71..4aa9ec978 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt +++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt @@ -384,11 +384,7 @@ subst/fwd subst_lref_gt subst/fwd subst_head subst/props subst_lift_SO subst/props subst_subst0 -T/dec terms_props__bind_dec T/dec bind_dec_not -T/dec terms_props__flat_dec -T/dec terms_props__kind_dec -T/dec term_dec T/dec binder_dec T/dec abst_dec tlist/props tslt_wf__q_ind @@ -400,7 +396,6 @@ T/props not_abbr_abst T/props not_void_abst T/props not_abbr_void T/props not_abst_void -T/props thead_x_y_y T/props tweight_lt ty3/arity ty3_arity ty3/arity_props ty3_predicative diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma index 7b35d0ca5..8851da3cb 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma @@ -21,7 +21,6 @@ *) include "Ground_2/list.ma". -include "Ground_2/star.ma". include "Basic_2/notation.ma". (* ITEMS ********************************************************************) @@ -55,6 +54,19 @@ coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2. coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2. +(* Basic properties *********************************************************) + +axiom item0_eq_dec: ∀I1,I2:item0. Decidable (I1 = I2). + +(* Basic_1: was: bind_dec *) +axiom bind2_eq_dec: ∀I1,I2:bind2. Decidable (I1 = I2). + +(* Basic_1: was: flat_dec *) +axiom flat2_eq_dec: ∀I1,I2:flat2. Decidable (I1 = I2). + +(* Basic_1: was: kind_dec *) +axiom item2_eq_dec: ∀I1,I2:item2. Decidable (I1 = I2). + (* Basic_1: removed theorems 19: s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc s_arith0 s_arith1 diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma index 621dda225..ce8357d21 100644 --- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma @@ -35,3 +35,25 @@ interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2). interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2). interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2). + +(* Basic inversion lemmas ***************************************************) + +lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False. +#I #T #V elim V -V +[ #J #H destruct +| #J #W #U #IHW #_ #H destruct -I /2/ (**) (* improve context after destruct *) +] +qed. + +(* Basic_1: was: thead_x_y_y *) +lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False. +#I #V #T elim T -T +[ #J #H destruct +| #J #W #U #_ #IHU #H destruct -I V /2/ (**) (* improve context after destruct *) +] +qed. + +(* Basic properties *********************************************************) + +(* Basic_1: was: term_dec *) +axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2). diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma index a18844e9b..187e0f49b 100644 --- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma @@ -13,10 +13,14 @@ (**************************************************************************) include "arithmetics/nat.ma". -include "Ground_2/xoa_props.ma". +include "Ground_2/star.ma". (* ARITHMETICAL PROPERTIES **************************************************) +axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). + +axiom lt_dec: ∀n1,n2. Decidable (n1 < n2). + lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False. #n #m