+ old and unused definition llstar replaced with new definition ltc to appear in cpms
--- /dev/null
+include "ground_2/lib/lstar.ma".
+
+(* Basic_2A1: was: d_liftable_llstar *)
+lemma d2_liftable_sn_llstar: ∀C,S,R. d_liftable2_sn C S R → ∀d. d_liftable2_sn C S (llstar … R d).
+#C #S #R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2
+[ #b #f #L #_ #U1 #HTU1 -HR -b -K /2 width=3 by ex2_intro/
+| #l #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
+ elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
+ elim (HR … HT2 … HLK … HTU) -T /3 width=5 by lstar_dx, ex2_intro/
+]
+qed-.
+
+(* Basic_2A1: was: d_deliftable_sn_llstar *)
+lemma d2_deliftable_sn_llstar: ∀C,S,R. d_deliftable2_sn C S R →
+ ∀d. d_deliftable2_sn C S (llstar … R d).
+#C #S #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
+[ /2 width=3 by lstar_O, ex2_intro/
+| #l #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1
+ elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
+ elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/lib/star.ma".
+include "basic_2/relocation/lreq_lreq.ma".
+
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+
+(* Properties with contextual transitive closure ****************************)
+
+(* Basic_2A1: was: d_liftable_LTC *)
+lemma d2_liftable_sn_CTC: ∀C,S,R. d_liftable2_sn C S R → d_liftable2_sn C S (CTC … R).
+#C #S #R #HR #K #T1 #T2 #H elim H -T2
+[ #T2 #HT12 #b #f #L #HLK #U1 #HTU1
+ elim (HR … HT12 … HLK … HTU1) /3 width=3 by inj, ex2_intro/
+| #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
+ elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
+ elim (HR … HT2 … HLK … HTU) -HR -K -T /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+(* Basic_2A1: was: d_deliftable_sn_LTC *)
+lemma d2_deliftable_sn_CTC: ∀C,S,R. d_deliftable2_sn C S R → d_deliftable2_sn C S (CTC … R).
+#C #S #R #HR #L #U1 #U2 #H elim H -U2
+[ #U2 #HU12 #b #f #K #HLK #T1 #HTU1
+ elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/
+| #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1
+ elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
+ elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+lemma co_dropable_sn_CTC: ∀R. co_dropable_sn R → co_dropable_sn (CTC … R).
+#R #HR #b #f #L1 #K1 #HLK1 #Hf #f2 #L2 #H elim H -L2
+[ #L2 #HL12 #f1 #H elim (HR … HLK1 … Hf … HL12 … H) -HR -Hf -f2 -L1
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IH #f1 #H elim (IH … H) -IH
+ #K #HK1 #HLK elim (HR … HLK … HL2 … H) -HR -f2 -L
+ /3 width=3 by step, ex2_intro/
+]
+qed-.
+
+lemma co_dropable_dx_CTC: ∀R. co_dropable_dx R → co_dropable_dx (CTC … R).
+#R #HR #f2 #L1 #L2 #H elim H -L2
+[ #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -Hf -f2 -L2
+ /3 width=3 by inj, ex2_intro/
+| #L #L2 #_ #HL2 #IHL1 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL2 … HLK2 … Hf … Hf2) -HR -L2
+ #K #HLK #HK2 elim (IHL1 … HLK … Hf … Hf2) -Hf -f2 -L
+ /3 width=5 by step, ex2_intro/
+]
+qed-.
+
+lemma co_dedropable_sn_CTC: ∀R. co_dedropable_sn R → co_dedropable_sn (CTC … R).
+#R #HR #b #f #L1 #K1 #HLK1 #f1 #K2 #H elim H -K2
+[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -f1 -K1
+ /3 width=4 by inj, ex3_intro/
+| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
+ #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -f1 -K
+ /3 width=6 by lreq_trans, step, ex3_intro/
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/lib/star.ma".
-include "ground_2/lib/lstar.ma".
-include "basic_2/relocation/lreq_lreq.ma".
-
-(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
-
-(* Properties with reflexive and transitive closure *************************)
-
-(* Basic_2A1: was: d_liftable_LTC *)
-lemma d2_liftable_sn_CTC: ∀C,S,R. d_liftable2_sn C S R → d_liftable2_sn C S (CTC … R).
-#C #S #R #HR #K #T1 #T2 #H elim H -T2
-[ #T2 #HT12 #b #f #L #HLK #U1 #HTU1
- elim (HR … HT12 … HLK … HTU1) /3 width=3 by inj, ex2_intro/
-| #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
- elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
- elim (HR … HT2 … HLK … HTU) -HR -K -T /3 width=5 by step, ex2_intro/
-]
-qed-.
-
-(* Basic_2A1: was: d_deliftable_sn_LTC *)
-lemma d2_deliftable_sn_CTC: ∀C,S,R. d_deliftable2_sn C S R → d_deliftable2_sn C S (CTC … R).
-#C #S #R #HR #L #U1 #U2 #H elim H -U2
-[ #U2 #HU12 #b #f #K #HLK #T1 #HTU1
- elim (HR … HU12 … HLK … HTU1) -HR -L -U1 /3 width=3 by inj, ex2_intro/
-| #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1
- elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
- elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by step, ex2_intro/
-]
-qed-.
-
-lemma co_dropable_sn_TC: ∀R. co_dropable_sn R → co_dropable_sn (CTC … R).
-#R #HR #b #f #L1 #K1 #HLK1 #Hf #f2 #L2 #H elim H -L2
-[ #L2 #HL12 #f1 #H elim (HR … HLK1 … Hf … HL12 … H) -HR -Hf -f2 -L1
- /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 #IH #f1 #H elim (IH … H) -IH
- #K #HK1 #HLK elim (HR … HLK … HL2 … H) -HR -f2 -L
- /3 width=3 by step, ex2_intro/
-]
-qed-.
-
-(* Basic_2A1: was: d_liftable_llstar *)
-lemma d2_liftable_sn_llstar: ∀C,S,R. d_liftable2_sn C S R → ∀d. d_liftable2_sn C S (llstar … R d).
-#C #S #R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2
-[ #b #f #L #_ #U1 #HTU1 -HR -b -K /2 width=3 by ex2_intro/
-| #l #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1
- elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1
- elim (HR … HT2 … HLK … HTU) -T /3 width=5 by lstar_dx, ex2_intro/
-]
-qed-.
-
-(* Basic_2A1: was: d_deliftable_sn_llstar *)
-lemma d2_deliftable_sn_llstar: ∀C,S,R. d_deliftable2_sn C S R →
- ∀d. d_deliftable2_sn C S (llstar … R d).
-#C #S #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2
-[ /2 width=3 by lstar_O, ex2_intro/
-| #l #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1
- elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1
- elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/
-]
-qed-.
-
-lemma co_dropable_dx_TC: ∀R. co_dropable_dx R → co_dropable_dx (CTC … R).
-#R #HR #f2 #L1 #L2 #H elim H -L2
-[ #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -Hf -f2 -L2
- /3 width=3 by inj, ex2_intro/
-| #L #L2 #_ #HL2 #IHL1 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL2 … HLK2 … Hf … Hf2) -HR -L2
- #K #HLK #HK2 elim (IHL1 … HLK … Hf … Hf2) -Hf -f2 -L
- /3 width=5 by step, ex2_intro/
-]
-qed-.
-
-lemma co_dedropable_sn_TC: ∀R. co_dedropable_sn R → co_dedropable_sn (CTC … R).
-#R #HR #b #f #L1 #K1 #HLK1 #f1 #K2 #H elim H -K2
-[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -f1 -K1
- /3 width=4 by inj, ex3_intro/
-| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1
- #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -f1 -K
- /3 width=6 by lreq_trans, step, ex3_intro/
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/relocation/drops_lstar.ma".
+include "basic_2/relocation/drops_ctc.ma".
include "basic_2/rt_transition/cpx_drops.ma".
include "basic_2/rt_computation/cpxs.ma".
class "orange"
[ { "relocation" * } {
[ { "generic slicing" * } {
- [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
+ [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
}
]
[ { "generic relocation" * } {
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/lib/relations.ma".
+
+(* FUNCTIONS ****************************************************************)
+
+definition left_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f i a.
+
+definition right_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f a i.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/logic.ma".
+include "ground_2/notation/xoa/false_0.ma".
+include "ground_2/notation/xoa/true_0.ma".
+include "ground_2/notation/xoa/or_2.ma".
+include "ground_2/notation/xoa/and_2.ma".
+include "ground_2/xoa/xoa.ma".
+
+interpretation "logical false" 'false = False.
+
+interpretation "logical true" 'true = True.
+
+(* Logical properties missing in the basic library **************************)
+
+lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
+#A #B * /2 width=1 by conj/
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "arithmetics/lstar.ma".
-
-(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************)
-
-definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝
- λA,B,R,l,a. lstar … (R a) l.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/lib/functions.ma".
+
+(* LABELLED TRANSITIVE CLOSURE **********************************************)
+
+inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝
+| ltc_rc : ∀a,b1,b2. R a b1 b2 → ltc … a b1 b2
+| ltc_trans: ∀a1,a2,b1,b,b2. ltc … a1 b1 b → ltc … a2 b b2 → ltc … (f a1 a2) b1 b2
+.
+
+(* Basic properties *********************************************************)
+
+lemma ltc_sn (A) (f) (B) (R): ∀a1,b1,b. R a1 b1 b →
+ ∀a2,b2. ltc A f B R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
+/3 width=3 by ltc_rc, ltc_trans/ qed.
+
+lemma ltc_dx (A) (f) (B) (R): ∀a1,b1,b. ltc A f B R a1 b1 b →
+ ∀a2,b2. R a2 b b2 → ltc … f … R (f a1 a2) b1 b2.
+/3 width=3 by ltc_rc, ltc_trans/ qed.
+
+(* Basic eliminators ********************************************************)
+
+lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f →
+ (∀a,b1. R a b1 b2 → Q a b1) →
+ (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
+ ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
+#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq … b2)
+#b0 #H elim H -a -b1 -b0 /2 width=2 by/
+#a1 #a2 #b1 #b #b0 #H #Hb2 #_
+generalize in match Hb2; generalize in match a2; -Hb2 -a2
+elim H -a1 -b1 -b /4 width=4 by ltc_trans/
+qed-.
+
+lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f →
+ (∀a,b2. R a b1 b2 → Q a b2) →
+ (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
+ ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
+#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq … b1)
+#b0 #H elim H -a -b0 -b2 /2 width=2 by/
+#a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_
+generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1
+elim H -a2 -b -b2 /4 width=4 by ltc_trans/
+qed-.
+
+(* Advanced elimiators with reflexivity *************************************)
+
+lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2):
+ associative … f → right_identity … f i → reflexive B (R i) →
+ Q i b2 →
+ (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) →
+ ∀a,b1. ltc … f … R a b1 b2 → Q a b1.
+#A #i #f #B #R #Q #b2 #H1f #H2f #HR #IH1 #IH2 #a #b1 #H
+@(ltc_ind_sn … R … H1f … IH2 … H) -a -b1 -H1f #a #b1 #Hb12
+>(H2f a) -H2f /3 width=4 by ltc_rc/
+qed-.
+
+lemma ltc_ind_dx_refl (A) (i) (f) (B) (R) (Q:A→predicate B) (b1):
+ associative … f → left_identity … f i → reflexive B (R i) →
+ Q i b1 →
+ (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) →
+ ∀a,b2. ltc … f … R a b1 b2 → Q a b2.
+#A #i #f #B #R #Q #b1 #H1f #H2f #HR #IH1 #IH2 #a #b2 #H
+@(ltc_ind_dx … R … H1f … IH2 … H) -a -b2 -H1f #a #b2 #Hb12
+>(H2f a) -H2f /3 width=4 by ltc_rc/
+qed-.
(**************************************************************************)
include "basics/relations.ma".
-include "ground_2/xoa/xoa_props.ma".
+include "ground_2/lib/logic.ma".
(* GENERIC RELATIONS ********************************************************)
+lemma insert_eq: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a.
+/2 width=1 by/ qed-.
+
(* Inclusion ****************************************************************)
definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
[ "stream ( ? @ ? )" "stream_eq ( ? ≗ ? )" "stream_hdtl ( ⫰? )" "stream_tls ( ⫰*[?]? )" * ]
[ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ]
[ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
- [ "relations ( ? ⊆ ? )" "star" "lstar" * ]
+ [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "star" "ltc" * ]
}
]
}
class "orange"
[ { "generated logical decomposables" * } {
[ { "" * } {
- [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ]
+ [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ]
}
]
}
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basics/logic.ma".
-include "ground_2/notation/xoa/false_0.ma".
-include "ground_2/notation/xoa/true_0.ma".
-include "ground_2/notation/xoa/or_2.ma".
-include "ground_2/notation/xoa/and_2.ma".
-include "ground_2/xoa/xoa.ma".
-
-interpretation "logical false" 'false = False.
-
-interpretation "logical true" 'true = True.
-
-(* Logical properties missing in the basic library **************************)
-
-lemma commutative_and: ∀A,B. A ∧ B → B ∧ A.
-#A #B * /2 width=1 by conj/
-qed-.
projects / helm.git / commitdiff