(**************************************************************************)
include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/class_c_1.ma".
+include "delayed_updating/notation/functions/class_c_2.ma".
include "ground/arith/nat_plus.ma".
include "ground/arith/nat_pred_succ.ma".
include "ground/lib/subset.ma".
+include "ground/lib/bool_and.ma".
include "ground/generated/insert_eq_1.ma".
(* CLOSED CONDITION FOR PATH ************************************************)
-inductive pcc: relation2 nat path โ
+inductive pcc (o): relation2 nat path โ
| pcc_empty:
- pcc (๐) (๐)
+ pcc o (๐) (๐)
| pcc_d_dx (p) (n) (k):
- pcc (n+ninj k) p โ pcc n (pโ๐ฑk)
+ (โ = o โ n = โโn) โ
+ pcc o (n+ninj k) p โ pcc o n (pโ๐ฑk)
| pcc_m_dx (p) (n):
- pcc n p โ pcc n (pโ๐บ)
+ pcc o n p โ pcc o n (pโ๐บ)
| pcc_L_dx (p) (n):
- pcc n p โ pcc (โn) (pโ๐)
+ pcc o n p โ pcc o (โn) (pโ๐)
| pcc_A_dx (p) (n):
- pcc n p โ pcc n (pโ๐)
+ pcc o n p โ pcc o n (pโ๐)
| pcc_S_dx (p) (n):
- pcc n p โ pcc n (pโ๐ฆ)
+ pcc o n p โ pcc o n (pโ๐ฆ)
.
interpretation
"closed condition (path)"
- 'ClassC n = (pcc n).
+ 'ClassC o n = (pcc o n).
+
+(* Advanced constructions ***************************************************)
+
+lemma pcc_false_d_dx (p) (n) (k:pnat):
+ p ฯต ๐โจโป,n+kโฉ โ pโ๐ฑk ฯต ๐โจโป,nโฉ.
+#p #n #k #H0
+@pcc_d_dx [| // ]
+#H0 destruct
+qed.
+
+lemma pcc_true_d_dx (p) (n:pnat) (k:pnat):
+ p ฯต ๐โจโ,n+kโฉ โ pโ๐ฑk ฯต ๐โจโ,nโฉ.
+/2 width=1 by pcc_d_dx/
+qed.
(* Basic inversions ********************************************************)
-lemma pcc_inv_empty (n):
- (๐) ฯต ๐โจnโฉ โ ๐ = n.
-#n @(insert_eq_1 โฆ (๐))
+lemma pcc_inv_empty (o) (n):
+ (๐) ฯต ๐โจo,nโฉ โ ๐ = n.
+#o #n @(insert_eq_1 โฆ (๐))
#x * -n //
-#p #n [ #k ] #_ #H0 destruct
+#p #n [ #k #_ ] #_ #H0 destruct
qed-.
-lemma pcc_inv_d_dx (p) (n) (k):
- pโ๐ฑk ฯต ๐โจnโฉ โ p ฯต ๐โจn+kโฉ.
-#p #n #h @(insert_eq_1 โฆ (pโ๐ฑh))
+(**) (* alias *)
+alias symbol "DownArrow" (instance 4) = "predecessor (non-negative integers)".
+alias symbol "UpArrow" (instance 3) = "successor (non-negative integers)".
+alias symbol "and" (instance 1) = "logical and".
+
+lemma pcc_inv_d_dx (o) (p) (n) (k):
+ pโ๐ฑk ฯต ๐โจo, nโฉ โ
+ โงโง (โ = o โ n = โโn)
+ & p ฯต ๐โจo, n+kโฉ.
+#o #p #n #h @(insert_eq_1 โฆ (pโ๐ฑh))
#x * -x -n
-[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+[|*: #x #n [ #k #Ho ] #Hx ] #H0 destruct
+/3 width=1 by conj/
qed-.
-lemma pcc_inv_m_dx (p) (n):
- pโ๐บ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
-#p #n @(insert_eq_1 โฆ (pโ๐บ))
+lemma pcc_inv_m_dx (o) (p) (n):
+ pโ๐บ ฯต ๐โจo,nโฉ โ p ฯต ๐โจo,nโฉ.
+#o #p #n @(insert_eq_1 โฆ (pโ๐บ))
#x * -x -n
-[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
qed-.
-lemma pcc_inv_L_dx (p) (n):
- pโ๐ ฯต ๐โจnโฉ โ
- โงโง p ฯต ๐โจโnโฉ & n = โโn.
-#p #n @(insert_eq_1 โฆ (pโ๐))
+lemma pcc_inv_L_dx (o) (p) (n):
+ pโ๐ ฯต ๐โจo,nโฉ โ
+ โงโง p ฯต ๐โจo,โnโฉ & n = โโn.
+#o #p #n @(insert_eq_1 โฆ (pโ๐))
#x * -x -n
-[|*: #x #n [ #k ] #Hx ] #H0 destruct
+[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct
<npred_succ /2 width=1 by conj/
qed-.
-lemma pcc_inv_A_dx (p) (n):
- pโ๐ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
-#p #n @(insert_eq_1 โฆ (pโ๐))
+lemma pcc_inv_A_dx (o) (p) (n):
+ pโ๐ ฯต ๐โจo,nโฉ โ p ฯต ๐โจo,nโฉ.
+#o #p #n @(insert_eq_1 โฆ (pโ๐))
#x * -x -n
-[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
qed-.
-lemma pcc_inv_S_dx (p) (n):
- pโ๐ฆ ฯต ๐โจnโฉ โ p ฯต ๐โจnโฉ.
-#p #n @(insert_eq_1 โฆ (pโ๐ฆ))
+lemma pcc_inv_S_dx (o) (p) (n):
+ pโ๐ฆ ฯต ๐โจo,nโฉ โ p ฯต ๐โจo,nโฉ.
+#o #p #n @(insert_eq_1 โฆ (pโ๐ฆ))
#x * -x -n
-[|*: #x #n [ #k ] #Hx ] #H0 destruct //
+[|*: #x #n [ #k #_ ] #Hx ] #H0 destruct //
+qed-.
+
+(* Advanced destructions ****************************************************)
+
+lemma pcc_des_d_dx (o) (p) (n) (k):
+ pโ๐ฑk ฯต ๐โจo,nโฉ โ p ฯต ๐โจo,n+kโฉ.
+#o #p #n #k #H0
+elim (pcc_inv_d_dx โฆ H0) -H0 #H1 #H2 //
+qed-.
+
+lemma pcc_des_gen (o) (p) (n):
+ p ฯต ๐โจo,nโฉ โ p ฯต ๐โจโป,nโฉ.
+#o #p #n #H0 elim H0 -p -n //
+#p #n [ #k #Ho ] #_ #IH
+/2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx, pcc_false_d_dx/
qed-.
(* Advanced inversions ******************************************************)
-lemma pcc_inv_empty_succ (n):
- (๐) ฯต ๐โจโnโฉ โ โฅ.
-#n #H0
+lemma pcc_inv_empty_succ (o) (n):
+ (๐) ฯต ๐โจo,โnโฉ โ โฅ.
+#o #n #H0
lapply (pcc_inv_empty โฆ H0) -H0 #H0
/2 width=7 by eq_inv_zero_nsucc/
qed-.
-lemma pcc_inv_L_dx_zero (p):
- pโ๐ ฯต ๐โจ๐โฉ โ โฅ.
-#p #H0
+lemma pcc_true_inv_d_dx_zero (p) (k):
+ pโ๐ฑk ฯต ๐โจโ,๐โฉ โ โฅ.
+#p #k #H0
+elim (pcc_inv_d_dx โฆ H0) -H0 #H0 #_
+elim (eq_inv_zero_nsucc โฆ (H0 ?)) -H0 //
+qed-.
+
+lemma pcc_inv_L_dx_zero (o) (p):
+ pโ๐ ฯต ๐โจo,๐โฉ โ โฅ.
+#o #p #H0
elim (pcc_inv_L_dx โฆ H0) -H0 #_ #H0
/2 width=7 by eq_inv_zero_nsucc/
qed-.
-lemma pcc_inv_L_dx_succ (p) (n):
- pโ๐ ฯต ๐โจโnโฉ โ p ฯต ๐โจnโฉ.
-#p #n #H0
+lemma pcc_inv_L_dx_succ (o) (p) (n):
+ pโ๐ ฯต ๐โจo,โnโฉ โ p ฯต ๐โจo,nโฉ.
+#o #p #n #H0
elim (pcc_inv_L_dx โฆ H0) -H0 //
qed-.
+(* Constructions with land **************************************************)
+
+lemma pcc_land_dx (o1) (o2) (p) (n):
+ p ฯต ๐โจo1,nโฉ โ p ฯต ๐โจo1โงo2,nโฉ.
+#o1 * /2 width=2 by pcc_des_gen/
+qed.
+
+lemma pcc_land_sn (o1) (o2) (p) (n):
+ p ฯต ๐โจo2,nโฉ โ p ฯต ๐โจo1โงo2,nโฉ.
+* /2 width=2 by pcc_des_gen/
+qed.
+
(* Main constructions with path_append **************************************)
-theorem pcc_append_bi (p) (q) (m) (n):
- p ฯต ๐โจmโฉ โ q ฯต ๐โจnโฉ โ pโq ฯต ๐โจm+nโฉ.
-#p #q #m #n #Hm #Hm elim Hm -Hm // -Hm
-#p #n [ #k ] #_ #IH [3: <nplus_succ_dx ]
-/2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
+theorem pcc_append_bi (o1) (o2) (p) (q) (m) (n):
+ p ฯต ๐โจo1,mโฉ โ q ฯต ๐โจo2,nโฉ โ pโq ฯต ๐โจo1โงo2,m+nโฉ.
+#o1 #o2 #p #q #m #n #Hm #Hn elim Hn -q -n
+/2 width=1 by pcc_m_dx, pcc_A_dx, pcc_S_dx, pcc_land_dx/
+#q #n [ #k #Ho2 ] #_ #IH
+[ @pcc_d_dx // #H0
+ elim (andb_inv_true_sn โฆ H0) -H0 #_ #H0 >Ho2 //
+ <nplus_succ_dx <npred_succ //
+| <nplus_succ_dx /2 width=1 by pcc_L_dx/
+]
qed.
(* Constructions with path_lcons ********************************************)
-lemma pcc_m_sn (q) (n):
- q ฯต ๐โจnโฉ โ (๐บโq) ฯต ๐โจnโฉ.
-#q #n #Hq
-lapply (pcc_append_bi (๐โ๐บ) โฆ Hq) -Hq
+lemma pcc_m_sn (o) (q) (n):
+ q ฯต ๐โจo,nโฉ โ (๐บโq) ฯต ๐โจo,nโฉ.
+#o #q #n #Hq
+lapply (pcc_append_bi (โ) โฆ (๐โ๐บ) โฆ Hq) -Hq
/2 width=3 by pcc_m_dx/
qed.
-lemma pcc_L_sn (q) (n):
- q ฯต ๐โจnโฉ โ (๐โq) ฯต ๐โจโnโฉ.
-#q #n #Hq
-lapply (pcc_append_bi (๐โ๐) โฆ Hq) -Hq
+lemma pcc_L_sn (o) (q) (n):
+ q ฯต ๐โจo,nโฉ โ (๐โq) ฯต ๐โจo,โnโฉ.
+#o #q #n #Hq
+lapply (pcc_append_bi (โ) โฆ (๐โ๐) โฆ Hq) -Hq
/2 width=3 by pcc_L_dx/
qed.
-lemma pcc_A_sn (q) (n):
- q ฯต ๐โจnโฉ โ (๐โq) ฯต ๐โจnโฉ.
-#q #n #Hq
-lapply (pcc_append_bi (๐โ๐) โฆ Hq) -Hq
+lemma pcc_A_sn (o) (q) (n):
+ q ฯต ๐โจo,nโฉ โ (๐โq) ฯต ๐โจo,nโฉ.
+#o #q #n #Hq
+lapply (pcc_append_bi (โ) โฆ (๐โ๐) โฆ Hq) -Hq
/2 width=3 by pcc_A_dx/
qed.
-lemma pcc_S_sn (q) (n):
- q ฯต ๐โจnโฉ โ (๐ฆโq) ฯต ๐โจnโฉ.
-#q #n #Hq
-lapply (pcc_append_bi (๐โ๐ฆ) โฆ Hq) -Hq
+lemma pcc_S_sn (o) (q) (n):
+ q ฯต ๐โจo,nโฉ โ (๐ฆโq) ฯต ๐โจo,nโฉ.
+#o #q #n #Hq
+lapply (pcc_append_bi (โ) โฆ (๐โ๐ฆ) โฆ Hq) -Hq
/2 width=3 by pcc_S_dx/
qed.
(* Main inversions **********************************************************)
-theorem pcc_mono (q) (n1):
- q ฯต ๐โจn1โฉ โ โn2. q ฯต ๐โจn2โฉ โ n1 = n2.
-#q1 #n1 #Hn1 elim Hn1 -q1 -n1
-[|*: #q1 #n1 [ #k1 ] #_ #IH ] #n2 #Hn2
+theorem pcc_mono (o1) (o2) (q) (n1):
+ q ฯต ๐โจo1,n1โฉ โ โn2. q ฯต ๐โจo2,n2โฉ โ n1 = n2.
+#o1 #o2 #q1 #n1 #Hn1 elim Hn1 -q1 -n1
+[|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] #n2 #Hn2
[ <(pcc_inv_empty โฆ Hn2) -n2 //
-| lapply (pcc_inv_d_dx โฆ Hn2) -Hn2 #Hn2
+| lapply (pcc_des_d_dx โฆ Hn2) -Hn2 #Hn2
lapply (IH โฆ Hn2) -q1 #H0
/2 width=2 by eq_inv_nplus_bi_dx/
| lapply (pcc_inv_m_dx โฆ Hn2) -Hn2 #Hn2
]
qed-.
-theorem pcc_inj_L_sn (p1) (p2) (q1) (n):
- q1 ฯต ๐โจnโฉ โ โq2. q2 ฯต ๐โจnโฉ โ
+theorem pcc_inj_L_sn (o1) (o2) (p1) (p2) (q1) (n):
+ q1 ฯต ๐โจo1,nโฉ โ โq2. q2 ฯต ๐โจo2,nโฉ โ
p1โ๐โq1 = p2โ๐โq2 โ q1 = q2.
-#p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n
-[|*: #q1 #n1 [ #k1 ] #_ #IH ] * //
+#o1 #o2 #p1 #p2 #q1 #n #Hq1 elim Hq1 -q1 -n
+[|*: #q1 #n1 [ #k1 #_ ] #_ #IH ] * //
[1,3,5,7,9,11: #l2 #q2 ] #Hq2
<list_append_lcons_sn <list_append_lcons_sn #H0
elim (eq_inv_list_lcons_bi ????? H0) -H0 #H0 #H1 destruct
[ elim (pcc_inv_L_dx_zero โฆ Hq2)
-| lapply (pcc_inv_d_dx โฆ Hq2) -Hq2 #Hq2
+| lapply (pcc_des_d_dx โฆ Hq2) -Hq2 #Hq2
<(IH โฆ Hq2) //
| lapply (pcc_inv_m_dx โฆ Hq2) -Hq2 #Hq2
<(IH โฆ Hq2) //
]
qed-.
-theorem pcc_inv_L_sn (q) (n) (m):
- (๐โq) ฯต ๐โจnโฉ โ q ฯต ๐โจmโฉ โ
+theorem pcc_inv_L_sn (o) (q) (n) (m):
+ (๐โq) ฯต ๐โจo,nโฉ โ q ฯต ๐โจo,mโฉ โ
โงโง โn = m & n = โโn.
-#q #n #m #H1q #H2q
+#o #q #n #m #H1q #H2q
lapply (pcc_L_sn โฆ H2q) -H2q #H2q
<(pcc_mono โฆ H2q โฆ H1q) -q -n
/2 width=1 by conj/