From 71690ba2c49a618d36e5eafcc16726e1ba80f038 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 2 Feb 2010 07:46:03 +0000
Subject: [PATCH] boolean arithmetics

---
 .../matita/nlibrary/arithmetics/nat.ma        | 157 +++++++++++++++++-
 1 file changed, 154 insertions(+), 3 deletions(-)

diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index 0418444e3..d1e401ae5 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -428,9 +428,9 @@ ntheorem le_n_Sm_elim : ∀n,m:nat.n ≤ S m →
 (* le and eq *)
 
 ntheorem le_to_le_to_eq: ∀n,m. n ≤ m → m ≤ n → n = m.
-napply nat_elim2; /3/; nqed.
+napply nat_elim2; /4/; nqed.
 
-ntheorem lt_O_S : \forall n:nat. O < S n.
+ntheorem lt_O_S : ∀n:nat. O < S n.
 /2/; nqed.
 
 (*
@@ -836,7 +836,7 @@ ntheorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
 napply nat_elim2; 
   ##[//
   ##|#n; #abs; napply False_ind;/2/;
-  ##|/3/;
+  ##|#n; #m; #Hind; #c; napplyS Hind; /2/;
   ##]
 nqed.
 
@@ -981,3 +981,154 @@ ntheorem monotonic_le_minus_r:
 napply le_plus_to_minus;
 napply (transitive_le ??? (le_plus_minus_m_m ? q));/2/;
 nqed.
+
+(*********************** boolean arithmetics ********************) 
+include "basics/bool.ma".
+
+nlet rec eqb n m ≝ 
+match n with 
+  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 
+  | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqb p q]
+  ].
+	   
+(*
+ntheorem eqb_to_Prop: ∀n,m:nat. 
+match (eqb n m) with
+[ true  \Rightarrow n = m 
+| false \Rightarrow n \neq m].
+intros.
+apply (nat_elim2
+(\lambda n,m:nat.match (eqb n m) with
+[ true  \Rightarrow n = m 
+| false \Rightarrow n \neq m])).
+intro.elim n1.
+simplify.reflexivity.
+simplify.apply not_eq_O_S.
+intro.
+simplify.unfold Not.
+intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
+intros.simplify.
+generalize in match H.
+elim ((eqb n1 m1)).
+simplify.apply eq_f.apply H1.
+simplify.unfold Not.intro.apply H1.apply inj_S.assumption.
+qed.
+
+theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
+(n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)). 
+intros.
+cut 
+(match (eqb n m) with
+[ true  \Rightarrow n = m
+| false \Rightarrow n \neq m] \to (P (eqb n m))).
+apply Hcut.apply eqb_to_Prop.
+elim (eqb n m).
+apply ((H H2)).
+apply ((H1 H2)).
+qed. 
+
+*)
+
+ntheorem eqb_n_n: ∀n. eqb n n = true.
+#n; nelim n; nnormalize; //.
+nqed. 
+
+ntheorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
+napply nat_elim2; 
+  ##[#n; ncases n; nnormalize; //; 
+     #m; #abs; napply False_ind;/2/;
+  ##|nnormalize; #m; #abs; napply False_ind;/2/;
+  ##|nnormalize; 
+     #n; #m; #Hind; #eqnm; napply eq_f; napply Hind; //;
+  ##]
+nqed.
+
+ntheorem eqb_false_to_not_eq: ∀n,m:nat.
+  eqb n m = false → n ≠ m.
+napply nat_elim2; 
+  ##[#n; ncases n; nnormalize; /2/; 
+  ##|/2/;
+  ##|nnormalize;/2/; 
+  ##]
+nqed.
+
+ntheorem eq_to_eqb_true: ∀n,m:nat.
+  n = m → eqb n m = true.
+//; nqed.
+
+ntheorem not_eq_to_eqb_false: ∀n,m:nat.
+  n ≠  m → eqb n m = false.
+#n; #m; #noteq; 
+nelim (true_or_false (eqb n m)); //;
+#Heq; napply False_ind; napply noteq;/2/;
+nqed.
+
+nlet rec leb n m ≝ 
+match n with 
+    [ O ⇒ true
+    | (S p) ⇒
+	match m with 
+        [ O ⇒ false
+	      | (S q) ⇒ leb p q]].
+
+ntheorem leb_elim: ∀n,m:nat. ∀P:bool → Prop. 
+(n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
+napply nat_elim2; nnormalize;
+  ##[/2/
+  ##|/3/;
+  ##|#n; #m; #Hind; #P; #Pt; #Pf; napply Hind;
+    ##[#lenm; napply Pt; napply le_S_S;//;
+    ##|#nlenm; napply Pf; #leSS; /3/;
+    ##]
+  ##]
+nqed.
+
+ntheorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
+#n; #m; napply leb_elim;
+  ##[//;
+  ##|#_; #abs; napply False_ind; /2/;
+  ##]
+nqed.
+
+ntheorem leb_false_to_not_le:∀n,m.
+  leb n m = false → n ≰ m.
+#n; #m; napply leb_elim;
+  ##[#_; #abs; napply False_ind; /2/;
+  ##|//;
+  ##]
+nqed.
+
+ntheorem le_to_leb_true: ∀n,m. n ≤ m → leb n m = true.
+#n; #m; napply leb_elim; //;
+#H; #H1; napply False_ind; /2/;
+nqed.
+
+ntheorem lt_to_leb_false: ∀n,m. m < n → leb n m = false.
+#n; #m; napply leb_elim; //;
+#H; #H1; napply False_ind; /2/;
+nqed.
+
+(* serve anche ltb? 
+ndefinition ltb ≝λn,m. leb (S n) m.
+
+ntheorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop. 
+(n < m → P true) → (n ≮ m → P false) → P (ltb n m).
+#n; #m; #P; #Hlt; #Hnlt;
+napply leb_elim; /3/; nqed.
+
+ntheorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m.
+#n; #m; #Hltb; napply leb_true_to_le; nassumption;
+nqed.
+
+ntheorem ltb_false_to_not_lt:∀n,m.
+  ltb n m = false → n ≮ m.
+#n; #m; #Hltb; napply leb_false_to_not_le; nassumption;
+nqed.
+
+ntheorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true.
+#n; #m; #Hltb; napply le_to_leb_true; nassumption;
+nqed.
+
+ntheorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
+#n; #m; #Hltb; napply lt_to_leb_false; /2/;
+nqed. *)
-- 
2.39.2