- two discrimination lemmas

- some decidability axioms (proof postponed)

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 f8c868a7159010208053712a389843528915d74d..4aa9ec978e9cc534283be64f0407fd5c81fbf4d7 100644 (file)
--- 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 7b35d0ca5d3e4b875b888a66b8e88534822005ad..8851da3cb465d24afddb3acad79626ccc0034353 100644 (file)
--- 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 621dda22579e36651ed5b6b44262b2bc56232c20..ce8357d21bb0d283609706d73aeb79e751011630 100644 (file)
--- 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 a18844e9ba805359bd53b7d772c597e099167e02..187e0f49bcfc21dfe6201094ae9030c3785b84c4 100644 (file)
--- 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 <plus_n_Sm #H destruct
 qed.

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
index e68ab1785666d895c110d1f0eddfdcf188d67d3c..e438b44f0c6bea578f1b243f7985aa68a8f51ec6 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
@@ -17,6 +17,9 @@ include "Ground_2/xoa_props.ma".
 
 (* PROPERTIES of RELATIONS **************************************************)
 
+definition Decidable: Prop → Prop ≝
+   λR. R ∨ (R → False). 
+
 definition confluent: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
                       ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
                       ∃∃a. R2 a1 a & R1 a2 a.