- some pending conjectures closed in basic_2 and ground_2

- bug fix in decidability of lift

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma
index df330a7df56c63dce10e67980081351afb4acee4..99260ba797a31f4337c78d4782a4aeb490a76621 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/lib/bool.ma".
 include "ground_2/lib/arith.ma".
 
 (* ITEMS ********************************************************************)
@@ -43,16 +44,35 @@ inductive item2: Type[0] ≝
 
 (* Basic properties *********************************************************)
 
-axiom eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
+lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2).
+* #i1 * #i2 [2,3,4,6,7,8: @or_intror #H destruct ]
+elim (eq_nat_dec i1 i2) /2 width=1 by or_introl/
+#Hni12 @or_intror #H destruct /2 width=1 by/ 
+qed-.
 
 (* Basic_1: was: bind_dec *)
-axiom eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2).
+lemma eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2).
+* * /2 width=1 by or_introl/
+@or_intror #H destruct
+qed-.
 
 (* Basic_1: was: flat_dec *)
-axiom eq_flat2_dec: ∀I1,I2:flat2. Decidable (I1 = I2).
+lemma eq_flat2_dec: ∀I1,I2:flat2. Decidable (I1 = I2).
+* * /2 width=1 by or_introl/
+@or_intror #H destruct
+qed-.
 
 (* Basic_1: was: kind_dec *)
-axiom eq_item2_dec: ∀I1,I2:item2. Decidable (I1 = I2).
+lemma eq_item2_dec: ∀I1,I2:item2. Decidable (I1 = I2).
+* [ #a1 ] #I1 * [1,3: #a2 ] #I2
+[2,3: @or_intror #H destruct
+| elim (eq_bool_dec a1 a2) #Ha
+  [ elim (eq_bind2_dec I1 I2) /2 width=1 by or_introl/ #HI ]
+  @or_intror #H destruct /2 width=1 by/
+| elim (eq_flat2_dec I1 I2) /2 width=1 by or_introl/ #HI
+  @or_intror #H destruct /2 width=1 by/
+]
+qed-.
 
 (* Basic_1: removed theorems 21:
             s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
index c34238632d50c18f97f9044bb0295291fa3a3b04..49d6cf5b83e309207cd7ea4201dc3e1a2d4b8b42 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
@@ -40,7 +40,17 @@ interpretation "abstraction (local environment)"
 
 (* Basic properties *********************************************************)
 
-axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+lemma eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] * [2,4: #L2 #I2 #V2 ]
+[1,4: @or_intror #H destruct
+| elim (eq_bind2_dec I1 I2) #HI
+  [ elim (eq_term_dec V1 V2) #HV
+    [ elim (IHL1 L2) -IHL1 /2 width=1 by or_introl/ #HL ]
+  ]
+  @or_intror #H destruct /2 width=1 by/
+| /2 width=1 by or_introl/
+]
+qed-.
 
 (* Basic inversion lemmas ***************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
index 77725446a9ebf79e1aedd380433dd4f315bc702d..fc039863e108caa96c9def45f1052b16f87f1da1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
@@ -93,7 +93,18 @@ interpretation "native type annotation (term)"
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: term_dec *)
-axiom eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
+lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
+#T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ]
+[1,4: @or_intror #H destruct
+| elim (eq_item2_dec I1 I2) #HI
+  [ elim (IHV1 V2) -IHV1 #HV
+    [ elim (IHT1 T2) -IHT1 /2 width=1 by or_introl/ #HT ]
+  ]
+  @or_intror #H destruct /2 width=1 by/
+| elim (eq_item0_dec I1 I2) /2 width=1 by or_introl/ #HI
+  @or_intror #H destruct /2 width=1 by/
+]
+qed-.
 
 (* Basic inversion lemmas ***************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
index f90b349b3de0b7fe55dc57e698833d5f666ce3dc..f8848629202d42750d885d59d179636b93995ace 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift.ma
@@ -39,7 +39,7 @@ interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2).
 (* Basic inversion lemmas ***************************************************)
 
 fact lift_inv_O2_aux: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
-#d #e #T1 #T2 #H elim H -d -e -T1 -T2 // /3 width=1/
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 /3 width=1 by eq_f2/
 qed-.
 
 lemma lift_inv_O2: ∀d,T1,T2. ⇧[d, 0] T1 ≡ T2 → T1 = T2.
@@ -60,8 +60,8 @@ fact lift_inv_lref1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀i. T1 = #i →
                          (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
 #d #e #T1 #T2 * -d -e -T1 -T2
 [ #k #d #e #i #H destruct
-| #j #d #e #Hj #i #Hi destruct /3 width=1/
-| #j #d #e #Hj #i #Hi destruct /3 width=1/
+| #j #d #e #Hj #i #Hi destruct /3 width=1 by or_introl, conj/
+| #j #d #e #Hj #i #Hi destruct /3 width=1 by or_intror, conj/
 | #p #d #e #i #H destruct
 | #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
@@ -104,7 +104,7 @@ fact lift_inv_bind1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
 | #i #d #e #_ #a #I #V1 #U1 #H destruct
 | #i #d #e #_ #a #I #V1 #U1 #H destruct
 | #p #d #e #a #I #V1 #U1 #H destruct
-| #b #J #W1 #W2 #T1 #T2 #d #e #HW #HT #a #I #V1 #U1 #H destruct /2 width=5/
+| #b #J #W1 #W2 #T1 #T2 #d #e #HW #HT #a #I #V1 #U1 #H destruct /2 width=5 by ex3_2_intro/
 | #J #W1 #W2 #T1 #T2 #d #e #_ #HT #a #I #V1 #U1 #H destruct
 ]
 qed-.
@@ -124,7 +124,7 @@ fact lift_inv_flat1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
 | #i #d #e #_ #I #V1 #U1 #H destruct
 | #p #d #e #I #V1 #U1 #H destruct
 | #a #J #W1 #W2 #T1 #T2 #d #e #_ #_ #I #V1 #U1 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V1 #U1 #H destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
@@ -149,8 +149,8 @@ fact lift_inv_lref2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀i. T2 = #i →
                          (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
 #d #e #T1 #T2 * -d -e -T1 -T2
 [ #k #d #e #i #H destruct
-| #j #d #e #Hj #i #Hi destruct /3 width=1/
-| #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4 width=1/
+| #j #d #e #Hj #i #Hi destruct /3 width=1 by or_introl, conj/
+| #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4 width=1 by monotonic_le_plus_l, or_intror, conj/
 | #p #d #e #i #H destruct
 | #a #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
 | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #i #H destruct
@@ -207,7 +207,7 @@ fact lift_inv_bind2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
 | #i #d #e #_ #a #I #V2 #U2 #H destruct
 | #i #d #e #_ #a #I #V2 #U2 #H destruct
 | #p #d #e #a #I #V2 #U2 #H destruct
-| #b #J #W1 #W2 #T1 #T2 #d #e #HW #HT #a #I #V2 #U2 #H destruct /2 width=5/
+| #b #J #W1 #W2 #T1 #T2 #d #e #HW #HT #a #I #V2 #U2 #H destruct /2 width=5 by ex3_2_intro/
 | #J #W1 #W2 #T1 #T2 #d #e #_ #_ #a #I #V2 #U2 #H destruct
 ]
 qed-.
@@ -228,7 +228,7 @@ fact lift_inv_flat2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
 | #i #d #e #_ #I #V2 #U2 #H destruct
 | #p #d #e #I #V2 #U2 #H destruct
 | #a #J #W1 #W2 #T1 #T2 #d #e #_ #_ #I #V2 #U2 #H destruct
-| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width=5/
+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
@@ -246,8 +246,8 @@ lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → ⊥.
   | lapply (lift_inv_gref2 … H) -H #H destruct
   ]
 | * [ #a ] #I #W2 #U2 #IHW2 #_ #T #H
-  [ elim (lift_inv_bind2 … H) -H #W1 #U1 #HW12 #_ #H destruct /2 width=2/
-  | elim (lift_inv_flat2 … H) -H #W1 #U1 #HW12 #_ #H destruct /2 width=2/
+  [ elim (lift_inv_bind2 … H) -H #W1 #U1 #HW12 #_ #H destruct /2 width=2 by/
+  | elim (lift_inv_flat2 … H) -H #W1 #U1 #HW12 #_ #H destruct /2 width=2 by/
   ]
 ]
 qed-.
@@ -261,8 +261,8 @@ lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → ⊥.
   | lapply (lift_inv_gref2 … H) -H #H destruct
   ]
 | * [ #a ] #I #W2 #U2 #_ #IHU2 #V #d #e #H
-  [ elim (lift_inv_bind2 … H) -H #W1 #U1 #_ #HU12 #H destruct /2 width=4/
-  | elim (lift_inv_flat2 … H) -H #W1 #U1 #_ #HU12 #H destruct /2 width=4/
+  [ elim (lift_inv_bind2 … H) -H #W1 #U1 #_ #HU12 #H destruct /2 width=4 by/
+  | elim (lift_inv_flat2 … H) -H #W1 #U1 #_ #HU12 #H destruct /2 width=4 by/
   ]
 ]
 qed-.
@@ -272,16 +272,16 @@ qed-.
 lemma lift_fwd_pair1: ∀I,T2,V1,U1,d,e. ⇧[d,e] ②{I}V1.U1 ≡ T2 →
                       ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & T2 = ②{I}V2.U2.
 * [ #a ] #I #T2 #V1 #U1 #d #e #H
-[ elim (lift_inv_bind1 … H) -H /2 width=4/
-|  elim (lift_inv_flat1 … H) -H /2 width=4/
+[ elim (lift_inv_bind1 … H) -H /2 width=4 by ex2_2_intro/
+|  elim (lift_inv_flat1 … H) -H /2 width=4 by ex2_2_intro/
 ]
 qed-.
 
 lemma lift_fwd_pair2: ∀I,T1,V2,U2,d,e. ⇧[d,e] T1 ≡ ②{I}V2.U2 →
                       ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & T1 = ②{I}V1.U1.
 * [ #a ] #I #T1 #V2 #U2 #d #e #H
-[ elim (lift_inv_bind2 … H) -H /2 width=4/
-|  elim (lift_inv_flat2 … H) -H /2 width=4/
+[ elim (lift_inv_bind2 … H) -H /2 width=4 by ex2_2_intro/
+|  elim (lift_inv_flat2 … H) -H /2 width=4 by ex2_2_intro/
 ]
 qed-.
 
@@ -305,7 +305,7 @@ qed-.
 
 (* Basic_1: was: lift_lref_gt *)
 lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ⇧[d, e] #(i - e) ≡ #i.
-#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=2/
+#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %); /3 width=2 by lift_lref_ge, le_plus_to_minus_r, le_plus_b/
 qed.
 
 lemma lift_lref_ge_minus_eq: ∀d,e,i,j. d + e ≤ i → j = i - e → ⇧[d, e] #j ≡ #i.
@@ -314,18 +314,18 @@ lemma lift_lref_ge_minus_eq: ∀d,e,i,j. d + e ≤ i → j = i - e → ⇧[d, e]
 (* Basic_1: was: lift_r *)
 lemma lift_refl: ∀T,d. ⇧[d, 0] T ≡ T.
 #T elim T -T
-[ * #i // #d elim (lt_or_ge i d) /2 width=1/
-| * /2 width=1/
+[ * #i // #d elim (lt_or_ge i d) /2 width=1 by lift_lref_lt, lift_lref_ge/
+| * /2 width=1 by lift_bind, lift_flat/
 ]
 qed.
 
 lemma lift_total: ∀T1,d,e. ∃T2. ⇧[d,e] T1 ≡ T2.
 #T1 elim T1 -T1
-[ * #i /2 width=2/ #d #e elim (lt_or_ge i d) /3 width=2/
+[ * #i /2 width=2/ #d #e elim (lt_or_ge i d) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/
 | * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #d #e
   elim (IHV1 d e) -IHV1 #V2 #HV12
-  [ elim (IHT1 (d+1) e) -IHT1 /3 width=2/
-  | elim (IHT1 d e) -IHT1 /3 width=2/
+  [ elim (IHT1 (d+1) e) -IHT1 /3 width=2 by lift_bind, ex_intro/
+  | elim (IHT1 d e) -IHT1 /3 width=2 by lift_flat, ex_intro/
   ]
 ]
 qed.
@@ -337,51 +337,49 @@ lemma lift_split: ∀d1,e2,T1,T2. ⇧[d1, e2] T1 ≡ T2 →
 #d1 #e2 #T1 #T2 #H elim H -d1 -e2 -T1 -T2
 [ /3 width=3/
 | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
-  lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/
+  lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3 by lift_lref_lt, ex2_intro/
 | #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
-  lapply (transitive_le … (i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21
-  >(plus_minus_m_m e2 e1 ?) // /3 width=3/
+  lapply (transitive_le … (i+e1) Hd21 ?) /2 width=1 by monotonic_le_plus_l/ -Hd21 #Hd21
+  >(plus_minus_m_m e2 e1 ?) /3 width=3 by lift_lref_ge, ex2_intro/
 | /3 width=3/
 | #a #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
   elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
-  elim (IHT (d2+1) … ? ? He12) /2 width=1/ /3 width=5/
+  elim (IHT (d2+1) … ? ? He12) /3 width=5 by lift_bind, le_S_S, ex2_intro/
 | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
   elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
-  elim (IHT d2 … ? ? He12) // /3 width=5/
+  elim (IHT d2 … ? ? He12) /3 width=5 by lift_flat, ex2_intro/
 ]
 qed.
 
 (* Basic_1: was only: dnf_dec2 dnf_dec *)
 lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ⇧[d,e] T1 ≡ T2).
 #T1 elim T1 -T1
-[ * [1,3: /3 width=2/ ] #i #d #e
-  elim (lt_dec i d) #Hid
-  [ /4 width=2/
-  | lapply (false_lt_to_le … Hid) -Hid #Hid
-    elim (lt_dec i (d + e)) #Hide
-    [ @or_intror * #T1 #H
-      elim (lift_inv_lref2_be … H Hid Hide)
-    | lapply (false_lt_to_le … Hide) -Hide /4 width=2/
+[ * [1,3: /3 width=2 by lift_sort, lift_gref, ex_intro, or_introl/ ] #i #d #e
+  elim (lt_or_ge i d) #Hdi
+  [ /4 width=3 by lift_lref_lt, ex_intro, or_introl/
+  | elim (lt_or_ge i (d + e)) #Hide
+    [ @or_intror * #T1 #H elim (lift_inv_lref2_be … H Hdi Hide)
+    | -Hdi /4 width=2 by lift_lref_ge_minus, ex_intro, or_introl/
     ]
   ]
 | * [ #a ] #I #V2 #T2 #IHV2 #IHT2 #d #e
   [ elim (IHV2 d e) -IHV2
     [ * #V1 #HV12 elim (IHT2 (d+1) e) -IHT2
-      [ * #T1 #HT12 @or_introl /3 width=2/
+      [ * #T1 #HT12 @or_introl /3 width=2 by lift_bind, ex_intro/
       | -V1 #HT2 @or_intror * #X #H
-        elim (lift_inv_bind2 … H) -H /3 width=2/
+        elim (lift_inv_bind2 … H) -H /3 width=2 by ex_intro/
       ]
     | -IHT2 #HV2 @or_intror * #X #H
-      elim (lift_inv_bind2 … H) -H /3 width=2/
+      elim (lift_inv_bind2 … H) -H /3 width=2 by ex_intro/
     ]
   | elim (IHV2 d e) -IHV2
     [ * #V1 #HV12 elim (IHT2 d e) -IHT2
       [ * #T1 #HT12 /4 width=2/
       | -V1 #HT2 @or_intror * #X #H
-        elim (lift_inv_flat2 … H) -H /3 width=2/
+        elim (lift_inv_flat2 … H) -H /3 width=2 by ex_intro/
       ]
     | -IHT2 #HV2 @or_intror * #X #H
-      elim (lift_inv_flat2 … H) -H /3 width=2/
+      elim (lift_inv_flat2 … H) -H /3 width=2 by ex_intro/
     ]
   ]
 ]

diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
index 656a4425577d9810533248ed264f2630981cc9a6..1af2859d70e14f7e17e5469cbf3a217d3287bab9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
+++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/arith.etc
@@ -16,3 +16,17 @@ qed-.
 lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w.
 #x #y #z #w #H <le_plus_minus_comm // /3 width=1 by lt_to_le, le_plus_a/
 qed-.
+
+lemma lt_dec: ∀n2,n1. Decidable (n1 < n2).
+#n2 elim n2 -n2
+[ /4 width=3 by or_intror, absurd, nmk/
+| #n2 #IHn2 * /2 width=1 by or_introl/
+  #n1 elim (IHn2 n1) -IHn2
+  /4 width=1 by le_S_S, monotonic_pred, or_intror, or_introl/
+]
+qed-.
+
+lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
+#x #y #H elim (decidable_lt x y) /2 width=1 by not_lt_to_le/
+#Hxy elim (H Hxy)
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 1afc42ebcbccd6d0365a2869eb9035071a03916f..557957bea4ba1254ac01f3f96cf4c3d719c88b77 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -60,9 +60,13 @@ lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
 
 (* Properties ***************************************************************)
 
-axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
-
-axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
+lemma eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
+#n1 elim n1 -n1 [| #n1 #IHn1 ] * [2,4: #n2 ]
+[1,4: @or_intror #H destruct
+| elim (IHn1 n2) -IHn1 /3 width=1 by or_intror, or_introl/
+| /2 width=1 by or_introl/
+]
+qed-.
 
 lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
 #m #n elim (lt_or_ge m n) /2 width=1 by or3_intro0/
@@ -115,11 +119,6 @@ lemma lt_zero_false: ∀n. n < 0 → ⊥.
 #n #H elim (lt_to_not_le … H) -H /2 width=1 by/
 qed-.
 
-lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x.
-#x #y #H elim (decidable_lt x y) /2 width=1 by not_lt_to_le/
-#Hxy elim (H Hxy)
-qed-.
-
 lemma pred_inv_refl: ∀m. pred m = m → m = 0.
 * // normalize #m #H elim (lt_refl_false m) //
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
index fed25ceda5ee8ce17d1c23c3e6e76e36401b5a8a..d2acdb2bc79c4ad3e2862072d9567056407650d7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/bool.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basics/bool.ma".
+include "ground_2/lib/star.ma".
 include "ground_2/notation/constructors/no_0.ma".
 include "ground_2/notation/constructors/yes_0.ma".
 
@@ -22,9 +23,16 @@ interpretation "boolean false" 'no = false.
 
 interpretation "boolean true" 'yes = true.
 
+(* Basic properties *********************************************************)
+
 lemma orb_false_r: ∀b1,b2:bool. (b1 ∨ b2) = false → b1 = false ∧ b2 = false.
 * normalize /2 width=1 by conj/ #b2 #H destruct
 qed-.
 
 lemma commutative_orb: commutative … orb.
 * * // qed.
+
+lemma eq_bool_dec: ∀b1,b2:bool. Decidable (b1 = b2).
+* * /2 width=1 by or_introl/
+@or_intror #H destruct
+qed-.