(* initial state *)
definition rtm_i: genv → term → rtm ≝
- λG,T. mk_rtm G 0 (â\8b\86) (â\9f ) T.
+ λG,T. mk_rtm G 0 (â\8b\86) (â\97\8a) T.
(* update code *)
definition rtm_t: rtm → term → rtm ≝
λM,T. match M with
- [ mk_rtm G u E _ _ â\87\92 mk_rtm G u E (â\9f ) T
+ [ mk_rtm G u E _ _ â\87\92 mk_rtm G u E (â\97\8a) T
].
(* update closure *)
definition rtm_u: rtm → xenv → term → rtm ≝
λM,E,T. match M with
- [ mk_rtm G u _ _ _ â\87\92 mk_rtm G u E (â\9f ) T
+ [ mk_rtm G u _ _ _ â\87\92 mk_rtm G u E (â\97\8a) T
].
(* get global environment *)
rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T))
(mk_rtm G u (E. ④{Abbr} {u, D, V}) S T)
| rtm_push : ∀G,u,E,W,T.
- rtm_step (mk_rtm G u E (â\9f ) (+ⓛW. T))
- (mk_rtm G (u + 1) (E. â\91£{Abst} {u, E, W}) (â\9f ) T)
+ rtm_step (mk_rtm G u E (â\97\8a) (+ⓛW. T))
+ (mk_rtm G (u + 1) (E. â\91£{Abst} {u, E, W}) (â\97\8a) T)
| rtm_theta : ∀G,u,E,S,V,T.
rtm_step (mk_rtm G u E S (+ⓓV. T))
(mk_rtm G u (E. ④{Abbr} {u, E, V}) S T)
[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
- @(s4 … HAtom … (◊)) //
+ lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/
| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
lapply (acr_gcr … H1RP H2RP B) #HB
elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
[ #K2 #HK20 #H destruct
elim (lift_total V0 0 (i0 +1)) #V #HV0
elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2
- @(s5 … HB … (◊) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
+ lapply (s5 … HB ? G ? ? (◊) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
| -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
#K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct
lapply (drop_fwd_drop2 … HLK2) #HLK2b
lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B
elim (lift_total V0 0 (i0 +1)) #V3 #HV03
elim (lift_total V2 0 (i0 +1)) #V #HV2
- @(s5 … HB … (◊) … (ⓝV3.V) … HLK2) [2: /2 width=1 by lift_flat/ ]
- @(s7 … HB … (◊)) [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ]
+ lapply (s5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) [1,3: /2 width=1 by lift_flat/ ]
+ lapply (s7 … HB G L2 (◊)) #H @H -H [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ]
]
| #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
lapply (acr_gcr … H1RP H2RP B) #HB
lapply (s1 … HB) -HB #HB
- @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, drops_skip, liftv_nil/
+ lapply (s6 … HA G L2 (◊) (◊)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/
| #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
@(acr_abst … H1RP H2RP) [ /2 width=5 by/ ]
#L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B
elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
- @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
+ @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
/3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
- @(s7 … HA … (◊)) /2 width=5 by/
+ lapply (s7 … HA G L2 (◊)) /3 width=5 by/
]
qed.
*)
lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
∀A. gcr RR RS RP (acr RP A).
-#RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
-#B #A #IHB #IHA @mk_gcr normalize
+#RR #RS #RP #H1RP #H2RP #A elim A -A //
+#B #A #IHB #IHA @mk_gcr
[ /3 width=7 by drops_cons, lifts_cons/
| #G #L #T #H
elim (cp1 … H1RP G L) #k #HK
- lapply (H ? (⋆k) ? (⟠) ? ? ?) -H
- [3,5: // |2,4: skip
- | @(s2 … IHB … (◊)) //
+ lapply (H L (⋆k) T (◊) ? ? ?) -H //
+ [ lapply (s2 … IHB G L (◊) … HK) //
| #H @(cp2 … H1RP … k) @(s1 … IHA) //
]
| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB
lapply (acr_gcr … H1RP H2RP B) #HCB
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
lapply (gcr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0
-@(s3 … HCA … (◊))
-@(s6 … HCA … (◊) (◊)) //
+lapply (s3 … HCA … a G L0 (◊)) #H @H -H
+lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H
[ @(HA … HL0) //
| lapply (s1 … HCB) -HCB #HCB
- @(s7 … H2RP … (◊)) /2 width=1 by/
+ lapply (s7 … H2RP G L0 (◊)) /3 width=1 by/
]
qed.
(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
inductive drops (s:bool): list2 nat nat → relation lenv ≝
-| drops_nil : â\88\80L. drops s (â\9f ) L L
+| drops_nil : â\88\80L. drops s (â\97\8a) L L
| drops_cons: ∀L1,L,L2,des,d,e.
drops s des L1 L → ⇩[s, d, e] L ≡ L2 → drops s ({d, e} @ des) L1 L2
.
(* Basic inversion lemmas ***************************************************)
-fact drops_inv_nil_aux: â\88\80L1,L2,s,des. â\87©*[s, des] L1 â\89¡ L2 â\86\92 des = â\9f → L1 = L2.
+fact drops_inv_nil_aux: â\88\80L1,L2,s,des. â\87©*[s, des] L1 â\89¡ L2 â\86\92 des = â\97\8a → L1 = L2.
#L1 #L2 #s #des * -L1 -L2 -des //
#L1 #L #L2 #d #e #des #_ #_ #H destruct
qed-.
(* Basic_1: was: drop1_gen_pnil *)
-lemma drops_inv_nil: â\88\80L1,L2,s. â\87©*[s, â\9f ] L1 ≡ L2 → L1 = L2.
+lemma drops_inv_nil: â\88\80L1,L2,s. â\87©*[s, â\97\8a] L1 ≡ L2 → L1 = L2.
/2 width=4 by drops_inv_nil_aux/ qed-.
fact drops_inv_cons_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 →
(* GENERIC TERM RELOCATION **************************************************)
inductive lifts: list2 nat nat → relation term ≝
-| lifts_nil : â\88\80T. lifts (â\9f ) T T
+| lifts_nil : â\88\80T. lifts (â\97\8a) T T
| lifts_cons: ∀T1,T,T2,des,d,e.
⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2
.
(* Basic inversion lemmas ***************************************************)
-fact lifts_inv_nil_aux: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 des = â\9f → T1 = T2.
+fact lifts_inv_nil_aux: â\88\80T1,T2,des. â\87§*[des] T1 â\89¡ T2 â\86\92 des = â\97\8a → T1 = T2.
#T1 #T2 #des * -T1 -T2 -des //
#T1 #T #T2 #d #e #des #_ #_ #H destruct
qed-.
-lemma lifts_inv_nil: â\88\80T1,T2. â\87§*[â\9f ] T1 ≡ T2 → T1 = T2.
+lemma lifts_inv_nil: â\88\80T1,T2. â\87§*[â\97\8a] T1 ≡ T2 → T1 = T2.
/2 width=3 by lifts_inv_nil_aux/ qed-.
fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 →
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
inductive at: list2 nat nat → relation nat ≝
-| at_nil: â\88\80i. at (â\9f ) i i
+| at_nil: â\88\80i. at (â\97\8a) i i
| at_lt : ∀des,d,e,i1,i2. i1 < d →
at des i1 i2 → at ({d, e} @ des) i1 i2
| at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
(* Basic inversion lemmas ***************************************************)
-fact at_inv_nil_aux: â\88\80des,i1,i2. @â¦\83i1, desâ¦\84 â\89¡ i2 â\86\92 des = â\9f → i1 = i2.
+fact at_inv_nil_aux: â\88\80des,i1,i2. @â¦\83i1, desâ¦\84 â\89¡ i2 â\86\92 des = â\97\8a → i1 = i2.
#des #i1 #i2 * -des -i1 -i2
[ //
| #des #d #e #i1 #i2 #_ #_ #H destruct
]
qed-.
-lemma at_inv_nil: â\88\80i1,i2. @â¦\83i1, â\9f ⦄ ≡ i2 → i1 = i2.
+lemma at_inv_nil: â\88\80i1,i2. @â¦\83i1, â\97\8a⦄ ≡ i2 → i1 = i2.
/2 width=3 by at_inv_nil_aux/ qed-.
fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
inductive minuss: nat → relation (list2 nat nat) ≝
-| minuss_nil: â\88\80i. minuss i (â\9f ) (â\9f )
+| minuss_nil: â\88\80i. minuss i (â\97\8a) (â\97\8a)
| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
minuss i ({d, e} @ des1) ({d - i, e} @ des2)
| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
(* Basic inversion lemmas ***************************************************)
-fact minuss_inv_nil1_aux: â\88\80des1,des2,i. des1 â\96 i â\89¡ des2 â\86\92 des1 = â\9f â\86\92 des2 = â\9f .
+fact minuss_inv_nil1_aux: â\88\80des1,des2,i. des1 â\96 i â\89¡ des2 â\86\92 des1 = â\97\8a â\86\92 des2 = â\97\8a.
#des1 #des2 #i * -des1 -des2 -i
[ //
| #des1 #des2 #d #e #i #_ #_ #H destruct
]
qed-.
-lemma minuss_inv_nil1: â\88\80des2,i. â\9f â\96 i â\89¡ des2 â\86\92 des2 = â\9f .
+lemma minuss_inv_nil1: â\88\80des2,i. â\97\8a â\96 i â\89¡ des2 â\86\92 des2 = â\97\8a.
/2 width=4 by minuss_inv_nil1_aux/ qed-.
fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
-[ nil2 â\87\92 â\9f
+[ nil2 â\87\92 â\97\8a
| cons2 d e des ⇒ {d + i, e} @ pluss des i
].
(* Basic inversion lemmas ***************************************************)
-lemma pluss_inv_nil2: â\88\80i,des. des + i = â\9f â\86\92 des = â\9f .
+lemma pluss_inv_nil2: â\88\80i,des. des + i = â\97\8a â\86\92 des = â\97\8a.
#i * // normalize
#d #e #des #H destruct
qed.
class "wine"
[ { "examples" * } {
[ { "terms with special features" * } {
- [ "ex_sta_ldec" "ex_cpr_omega" * ]
+ [ "ex_sta_ldec" + "ex_cpr_omega" * ]
}
]
}
(* *)
(**************************************************************************)
-include "ground_2/notation/constructors/nil_1.ma".
-include "ground_2/notation/constructors/nil_2.ma".
+include "ground_2/notation/constructors/nil_0.ma".
+include "ground_2/notation/constructors/cons_2.ma".
include "ground_2/notation/constructors/cons_3.ma".
-include "ground_2/notation/constructors/cons_5.ma".
include "ground_2/notation/functions/append_2.ma".
include "ground_2/lib/arith.ma".
| nil : list A
| cons: A → list A → list A.
-interpretation "nil (list)" 'Nil A = (nil A).
+interpretation "nil (list)" 'Nil = (nil ?).
-interpretation "cons (list)" 'Cons A hd tl = (cons A hd tl).
+interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
let rec all A (R:predicate A) (l:list A) on l ≝
match l with
| nil2 : list2 A1 A2
| cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
-interpretation "nil (list of pairs)" 'Nil A1 A2 = (nil2 A1 A2).
+interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?).
-interpretation "cons (list of pairs)" 'Cons A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl).
+interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
[ nil2 ⇒ l2
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( hd @ break tl )"
+ right associative with precedence 47
+ for @{ 'Cons $hd $tl }.
(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-notation "hvbox( hd @ break tl )"
- right associative with precedence 47
- for @{ 'Cons ? $hd $tl }.
+notation "hvbox( { term 46 hd1 , break term 46 hd2 } @ break term 46 tl )"
+ non associative with precedence 47
+ for @{ 'Cons $hd1 $hd2 $tl }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "hvbox( { term 46 hd1 , break term 46 hd2 } @ break term 46 tl )"
- non associative with precedence 47
- for @{ 'Cons ? ? $hd1 $hd2 $tl }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "◊"
+ non associative with precedence 46
+ for @{ 'Nil }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "◊"
- non associative with precedence 46
- for @{ 'Nil ? }.
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
-
-notation "⟠"
- non associative with precedence 46
- for @{ 'Nil ? ? }.
projects / helm.git / commitdiff