From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 9 Aug 2013 10:59:49 +0000 (+0000)
Subject: - we added nat-labeled reflexive and transitive closure (for use in lambdadelta)
X-Git-Tag: make_still_working~1115
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=774c5e125eb44693a5a760226713067c41baf09f;p=helm.git

- we added nat-labeled reflexive and transitive closure (for use in lambdadelta)
- stylistic improvements in list-labeled reflexive and transitive closure
---

diff --git a/matita/matita/lib/arithmetics/lstar.ma b/matita/matita/lib/arithmetics/lstar.ma
new file mode 100644
index 000000000..ddd4113e3
--- /dev/null
+++ b/matita/matita/lib/arithmetics/lstar.ma
@@ -0,0 +1,135 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "arithmetics/nat.ma".
+
+(* nat-labeled reflexive and transitive closure *****************************)
+
+definition ltransitive: ∀B:Type[0]. predicate (ℕ→relation B) ≝ λB,R.
+                        ∀l1,b1,b. R l1 b1 b → ∀l2,b2. R l2 b b2 → R (l1+l2) b1 b2.
+
+definition inv_ltransitive: ∀B:Type[0]. predicate (ℕ→relation B) ≝
+                            λB,R. ∀l1,l2,b1,b2. R (l1+l2) b1 b2 →
+                            ∃∃b. R l1 b1 b & R l2 b b2.
+
+inductive lstar (B:Type[0]) (R: relation B): ℕ→relation B ≝
+| lstar_O: ∀b. lstar B R 0 b b
+| lstar_S: ∀b1,b. R b1 b → ∀l,b2. lstar B R l b b2 → lstar B R (l+1) b1 b2
+.
+
+fact lstar_ind_l_aux: ∀B,R,b2. ∀P:relation2 ℕ B.
+                      P 0 b2 →
+                      (∀l,b1,b. R b1 b → lstar … R l b b2 → P l b → P (l+1) b1) →
+                      ∀l,b1,b. lstar … R l b1 b → b = b2 → P l b1.
+#B #R #b2 #P #H1 #H2 #l #b1 #b #H elim H -b -b1
+[ #b #H destruct /2 width=1/
+| #b #b0 #Hb0 #l #b1 #Hb01 #IH #H destruct /3 width=4/
+]
+qed-.
+
+(* imporeved version of lstar_ind with "left_parameter" *)
+lemma lstar_ind_l: ∀B,R,b2. ∀P:relation2 ℕ B.
+                   P 0 b2 →
+                   (∀l,b1,b. R b1 b → lstar … R l b b2 → P l b → P (l+1) b1) →
+                   ∀l,b1. lstar … R l b1 b2 → P l b1.
+#B #R #b2 #P #H1 #H2 #l #b1 #Hb12
+@(lstar_ind_l_aux … H1 H2 … Hb12) //
+qed-.
+
+lemma lstar_step: ∀B,R,b1,b2. R b1 b2 → lstar B R 1 b1 b2.
+/2 width=3/
+qed.
+
+lemma lstar_inv_O: ∀B,R,l,b1,b2. lstar B R l b1 b2 → 0 = l → b1 = b2.
+#B #R #l #b1 #b2 * -l -b1 -b2 //
+#b1 #b #_ #l #b2 #_ <plus_n_Sm #H destruct
+qed-.
+
+lemma lstar_inv_S: ∀B,R,l,b1,b2. lstar B R l b1 b2 →
+                   ∀l0. l0+1 = l →
+                   ∃∃b. R b1 b & lstar B R l0 b b2.
+#B #R #l #b1 #b2 * -l -b1 -b2
+[ #b #l0 <plus_n_Sm #H destruct
+| #b1 #b #Hb1 #l #b2 #Hb2 #l0 #H
+  lapply (injective_plus_l … H) -H #H destruct /2 width=3/
+]
+qed-.
+
+lemma lstar_inv_step: ∀B,R,b1,b2. lstar B R 1 b1 b2 → R b1 b2.
+#B #R #b1 #b2 #H
+elim (lstar_inv_S … 1 … H 0) -H // #b #Hb1 #H
+<(lstar_inv_O … R … H ?) -H //
+qed-.
+
+theorem lstar_singlevalued: ∀B,R. singlevalued … R →
+                            ∀l. singlevalued … (lstar B R l).
+#B #R #HR #l #c #c1 #H @(lstar_ind_l … l c H) -l -c
+[ /2 width=5 by lstar_inv_O/
+| #l #b #b1 #Hb1 #_ #IHbc1 #c2 #H
+  elim (lstar_inv_S … R … H l) -H // #b2 #Hb2 #Hbc2
+  lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
+]
+qed-.
+
+theorem lstar_ltransitive: ∀B,R. ltransitive … (lstar B R).
+#B #R #l1 #b1 #b #H @(lstar_ind_l … l1 b1 H) -l1 -b1 // /3 width=3/
+qed-.
+
+lemma lstar_inv_ltransitive: ∀B,R. inv_ltransitive … (lstar B R).
+#B #R #l1 @(nat_ind_plus … l1) -l1 /2 width=3/
+#l1 #IHl1 #l2 #b1 #b2 <plus_plus_comm_23 #H
+elim (lstar_inv_S … b2 H (l1+l2)) -H // #b #Hb1 #Hb2
+elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/
+qed-.
+
+lemma lstar_dx: ∀B,R,l,b1,b. lstar B R l b1 b → ∀b2. R b b2 →
+                lstar B R (l+1) b1 b2.
+#B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/ /3 width=3/
+qed.
+
+inductive lstar_r (B:Type[0]) (R: relation B): ℕ → relation B ≝
+| lstar_r_O: ∀b. lstar_r B R 0 b b
+| lstar_r_S: ∀l,b1,b. lstar_r B R l b1 b → ∀b2. R b b2 →
+             lstar_r B R (l+1) b1 b2
+.
+
+lemma lstar_r_sn: ∀B,R,l,b,b2. lstar_r B R l b b2 → ∀b1. R b1 b →
+                  lstar_r B R (l+1) b1 b2.
+#B #R #l #b #b2 #H elim H -l -b2 /2 width=3/
+#l #b1 #b #_ #b2 #Hb2 #IHb1 #b0 #Hb01
+@(lstar_r_S … (l+1) … Hb2) -b2 /2 width=1/
+qed.
+
+lemma lstar_lstar_r: ∀B,R,l,b1,b2. lstar B R l b1 b2 → lstar_r B R l b1 b2.
+#B #R #l #b1 #b2 #H @(lstar_ind_l … l b1 H) -l -b1 // /2 width=3/
+qed.
+
+lemma lstar_r_inv_lstar: ∀B,R,l,b1,b2. lstar_r B R l b1 b2 → lstar B R l b1 b2.
+#B #R #l #b1 #b2 #H elim H -l -b1 -b2 // /2 width=3/
+qed-.
+
+fact lstar_ind_r_aux: ∀B,R,b1. ∀P:relation2 ℕ B.
+                      P 0 b1 →
+                      (∀l,b,b2. lstar … R l b1 b → R b b2 → P l b → P (l+1) b2) →
+                      ∀l,b,b2. lstar … R l b b2 → b = b1 → P l b2.
+#B #R #b1 #P #H1 #H2 #l #b #b2 #H elim (lstar_lstar_r … l b b2 H) -l -b -b2
+[ #b #H destruct //
+| #l #b #b0 #Hb0 #b2 #Hb02 #IHb02 #H destruct /3 width=4 by lstar_r_inv_lstar/
+]
+qed-.
+
+lemma lstar_ind_r: ∀B,R,b1. ∀P:relation2 ℕ B.
+                   P 0 b1 →
+                   (∀l,b,b2. lstar … R l b1 b → R b b2 → P l b → P (l+1) b2) →
+                   ∀l,b2. lstar … R l b1 b2 → P l b2.
+#B #R #b1 #P #H1 #H2 #l #b2 #Hb12
+@(lstar_ind_r_aux … H1 H2 … Hb12) //
+qed-.
diff --git a/matita/matita/lib/basics/lists/lstar.ma b/matita/matita/lib/basics/lists/lstar.ma
index 2b9937d1b..b7b25ab65 100644
--- a/matita/matita/lib/basics/lists/lstar.ma
+++ b/matita/matita/lib/basics/lists/lstar.ma
@@ -11,7 +11,7 @@
 
 include "basics/lists/list.ma".
 
-(* labeled reflexive and transitive closure *********************************)
+(* list-labeled reflexive and transitive closure ****************************)
 
 definition ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝ λA,B,R.
                         ∀l1,b1,b. R l1 b1 b → ∀l2,b2. R l2 b b2 → R (l1@l2) b1 b2. 
@@ -65,34 +65,34 @@ qed-.
 
 lemma lstar_inv_step: ∀A,B,R,a,b1,b2. lstar A B R ([a]) b1 b2 → R a b1 b2.
 #A #B #R #a #b1 #b2 #H
-elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b #Hb1 #H (**) (* simplify line *)
+elim (lstar_inv_cons ?????? H) -H [4: // |2,3: skip ] #b #Hb1 #H (**) (* simplify line *)
 <(lstar_inv_nil ?????? H ?) -H // (**) (* simplify line *)
 qed-.
 
 theorem lstar_singlevalued: ∀A,B,R. (∀a. singlevalued ?? (R a)) →
                             ∀l. singlevalued … (lstar A B R l).
-#A #B #R #HR #l #b #c1 #H @(lstar_ind_l ????????? H) -l -b
+#A #B #R #HR #l #b #c1 #H @(lstar_ind_l … l b H) -l -b
 [ /2 width=5 by lstar_inv_nil/
 | #a #l #b #b1 #Hb1 #_ #IHbc1 #c2 #H
-  elim (lstar_inv_cons ?????? H ???) -H [4: // |2,3: skip ] #b2 #Hb2 #Hbc2 (**) (* simplify line *)
+  elim (lstar_inv_cons ?????? H) -H [4: // |2,3: skip ] #b2 #Hb2 #Hbc2 (**) (* simplify line *)
   lapply (HR … Hb1 … Hb2) -b #H destruct /2 width=1/
 ]
 qed-.
 
 theorem lstar_ltransitive: ∀A,B,R. ltransitive … (lstar A B R).
-#A #B #R #l1 #b1 #b #H @(lstar_ind_l ????????? H) -l1 -b1 normalize // /3 width=3/
+#A #B #R #l1 #b1 #b #H @(lstar_ind_l … l1 b1 H) -l1 -b1 normalize // /3 width=3/
 qed-.
 
 lemma lstar_inv_ltransitive: ∀A,B,R. inv_ltransitive … (lstar A B R).
 #A #B #R #l1 elim l1 -l1 normalize /2 width=3/
 #a #l1 #IHl1 #l2 #b1 #b2 #H
-elim (lstar_inv_cons … b2 H ???) -H [4: // |2,3: skip ] #b #Hb1 #Hb2 (**) (* simplify line *)
+elim (lstar_inv_cons … b2 H) -H [4: // |2,3: skip ] #b #Hb1 #Hb2 (**) (* simplify line *)
 elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/
 qed-.
 
 lemma lstar_app: ∀A,B,R,l,b1,b. lstar A B R l b1 b → ∀a,b2. R a b b2 →
                  lstar A B R (l@[a]) b1 b2.
-#A #B #R #l #b1 #b #H @(lstar_ind_l ????????? H) -l -b1 /2 width=1/
+#A #B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/
 normalize /3 width=3/
 qed.
 
@@ -110,7 +110,7 @@ lemma lstar_r_cons: ∀A,B,R,l,b,b2. lstar_r A B R l b b2 → ∀a,b1. R a b1 b
 qed.
 
 lemma lstar_lstar_r: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → lstar_r A B R l b1 b2.
-#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -l -b1 // /2 width=3/
+#A #B #R #l #b1 #b2 #H @(lstar_ind_l … l b1 H) -l -b1 // /2 width=3/
 qed.
 
 lemma lstar_r_inv_lstar: ∀A,B,R,l,b1,b2. lstar_r A B R l b1 b2 → lstar A B R l b1 b2.
@@ -121,7 +121,7 @@ fact lstar_ind_r_aux: ∀A,B,R,b1. ∀P:relation2 (list A) B.
                       P ([]) b1 →
                       (∀a,l,b,b2. lstar … R l b1 b → R a b b2 → P l b → P (l@[a]) b2) →
                       ∀l,b,b2. lstar … R l b b2 → b = b1 → P l b2.
-#A #B #R #b1 #P #H1 #H2 #l #b #b2 #H elim (lstar_lstar_r ?????? H) -l -b -b2
+#A #B #R #b1 #P #H1 #H2 #l #b #b2 #H elim (lstar_lstar_r … l b b2 H) -l -b -b2
 [ #b #H destruct //
 | #l #b #b0 #Hb0 #a #b2 #Hb02 #IH #H destruct /3 width=4 by lstar_r_inv_lstar/
 ]