(* initial state *)
definition rtm_i: genv → term → rtm ≝
- λG,T. mk_rtm G 0 (â\8b\86) (â\97\8a) T.
+ λG,T. mk_rtm G 0 (â\8b\86) (â\92º) 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 (â\97\8a) T
+ [ mk_rtm G u E _ _ â\87\92 mk_rtm G u E (â\92º) 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 (â\97\8a) T
+ [ mk_rtm G u _ _ _ â\87\92 mk_rtm G u E (â\92º) 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 (â\97\8a) (+ⓛW. T))
- (mk_rtm G (u + 1) (E. â\91£{Abst} {u, E, W}) (â\97\8a) T)
+ rtm_step (mk_rtm G u E (â\92º) (+ⓛW. T))
+ (mk_rtm G (u + 1) (E. â\91£{Abst} {u, E, W}) (â\92º) 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)
2: binary
A: application to vector
+E: empty list
F: boolean false
T: boolean true
(* Basic_2A1: includes: liftv_nil liftv_cons *)
inductive liftsv (f:rtmap): relation (list term) ≝
-| liftsv_nil : liftsv f (â\97\8a) (â\97\8a)
+| liftsv_nil : liftsv f (â\92º) (â\92º)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⬆*[f] T1 ≘ T2 → liftsv f T1s T2s →
liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
(* Basic inversion lemmas ***************************************************)
-fact liftsv_inv_nil1_aux: â\88\80f,X,Y. â¬\86*[f] X â\89\98 Y â\86\92 X = â\97\8a â\86\92 Y = â\97\8a.
+fact liftsv_inv_nil1_aux: â\88\80f,X,Y. â¬\86*[f] X â\89\98 Y â\86\92 X = â\92º â\86\92 Y = â\92º.
#f #X #Y * -X -Y //
#T1s #T2s #T1 #T2 #_ #_ #H destruct
qed-.
(* Basic_2A1: includes: liftv_inv_nil1 *)
-lemma liftsv_inv_nil1: â\88\80f,Y. â¬\86*[f] â\97\8a â\89\98 Y â\86\92 Y = â\97\8a.
+lemma liftsv_inv_nil1: â\88\80f,Y. â¬\86*[f] â\92º â\89\98 Y â\86\92 Y = â\92º.
/2 width=5 by liftsv_inv_nil1_aux/ qed-.
fact liftsv_inv_cons1_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
Y = T2 ⨮ T2s.
/2 width=3 by liftsv_inv_cons1_aux/ qed-.
-fact liftsv_inv_nil2_aux: â\88\80f,X,Y. â¬\86*[f] X â\89\98 Y â\86\92 Y = â\97\8a â\86\92 X = â\97\8a.
+fact liftsv_inv_nil2_aux: â\88\80f,X,Y. â¬\86*[f] X â\89\98 Y â\86\92 Y = â\92º â\86\92 X = â\92º.
#f #X #Y * -X -Y //
#T1s #T2s #T1 #T2 #_ #_ #H destruct
qed-.
-lemma liftsv_inv_nil2: â\88\80f,X. â¬\86*[f] X â\89\98 â\97\8a â\86\92 X = â\97\8a.
+lemma liftsv_inv_nil2: â\88\80f,X. â¬\86*[f] X â\89\98 â\92º â\86\92 X = â\92º.
/2 width=5 by liftsv_inv_nil2_aux/ qed-.
fact liftsv_inv_cons2_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
lapply (aaa_inv_sort … HA) -HA #H destruct
>(lifts_inv_sort1 … H0) -H0
lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
- lapply (s4 â\80¦ HAtom G L2 (â\97\8a)) /2 width=1 by/
+ lapply (s4 â\80¦ HAtom G L2 (â\92º)) /2 width=1 by/
| #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1
elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
elim (lsubc_inv_bind2 … H) -H *
[ #K2 #HK20 #H destruct
lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
- lapply (s5 â\80¦ HA ? G ? ? (â\97\8a) … HV0 ?) -HA
+ lapply (s5 â\80¦ HA ? G ? ? (â\92º) … HV0 ?) -HA
/4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/
| #K2 #V2 #W2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1
lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
elim (lifts_total V2 (𝐔❴↑j❵)) #V3 #HV23
- lapply (s5 â\80¦ HA â\80¦ G â\80¦ (â\97\8a) … (ⓝW2.V2) (ⓝV.V3) ????)
+ lapply (s5 â\80¦ HA â\80¦ G â\80¦ (â\92º) … (ⓝW2.V2) (ⓝV.V3) ????)
[3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
- lapply (s7 â\80¦ HA G L2 (â\97\8a)) -HA /3 width=7 by acr_lifts/
+ lapply (s7 â\80¦ HA G L2 (â\92º)) -HA /3 width=7 by acr_lifts/
]
| #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
elim (aaa_inv_gref … HA)
lapply (acr_gcr … H1RP H2RP A) #HA
lapply (acr_gcr … H1RP H2RP B) #HB
lapply (s1 … HB) -HB #HB
- lapply (s6 â\80¦ HA G L2 (â\97\8a) (â\97\8a)) /5 width=10 by lsubc_bind, liftsv_nil, drops_skip, ext2_pair/
+ lapply (s6 â\80¦ HA G L2 (â\92º) (â\92º)) /5 width=10 by lsubc_bind, liftsv_nil, drops_skip, ext2_pair/
| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct
elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
elim (aaa_inv_cast … HA) -HA #HW #HT
elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
- lapply (s7 â\80¦ HA G L2 (â\97\8a)) /3 width=10 by/
+ lapply (s7 â\80¦ HA G L2 (â\92º)) /3 width=10 by/
]
qed.
#B #A #IHB #IHA @mk_gcr
[ #G #L #T #H
elim (cp1 … H1RP G L) #s #HK
- lapply (s2 â\80¦ IHB G L (â\97\8a) … HK) // #HB
+ lapply (s2 â\80¦ IHB G L (â\92º) … HK) // #HB
lapply (H (𝐈𝐝) L (⋆s) T ? ? ?) -H
/3 width=6 by s1, cp3, drops_refl, lifts_refl/
| #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB
lapply (acr_gcr … H1RP H2RP B) #HCB
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
lapply (acr_lifts … H1RP … HW … HL0 … HW0) -HW #HW0
-lapply (s3 â\80¦ HCA â\80¦ p G L0 (â\97\8a)) #H @H -H
-lapply (s6 â\80¦ HCA G L0 (â\97\8a) (â\97\8a) ?) // #H @H -H
+lapply (s3 â\80¦ HCA â\80¦ p G L0 (â\92º)) #H @H -H
+lapply (s6 â\80¦ HCA G L0 (â\92º) (â\92º) ?) // #H @H -H
[ @(HA … HL0) //
| lapply (s1 … HCB) -HCB #HCB
- lapply (s7 â\80¦ H2RP G L0 (â\97\8a)) /3 width=1 by/
+ lapply (s7 â\80¦ H2RP G L0 (â\92º)) /3 width=1 by/
]
qed.
(* *)
(**************************************************************************)
-include "ground_2/lib/list2.ma".
include "basic_2/notation/constructors/star_0.ma".
include "basic_2/notation/constructors/dxbind2_3.ma".
include "basic_2/notation/constructors/dxabbr_2.ma".
(* GLOBAL ENVIRONMENTS ******************************************************)
(* global environments *)
-definition genv ≝ list2 bind2 term.
+inductive genv: Type[0] ≝
+| GAtom: genv (* empty *)
+| GBind: genv → bind2 → term → genv (* binding construction *)
+.
interpretation "sort (global environment)"
- 'Star = (nil2 bind2 term).
+ 'Star = (GAtom).
interpretation "global environment binding construction (binary)"
- 'DxBind2 L I T = (cons2 bind2 term I T L).
+ 'DxBind2 G I T = (GBind G I T).
interpretation "abbreviation (global environment)"
- 'DxAbbr L T = (cons2 bind2 term Abbr T L).
+ 'DxAbbr G T = (GBind G Abbr T).
interpretation "abstraction (global environment)"
- 'DxAbst L T = (cons2 bind2 term Abst T L).
+ 'DxAbst G T = (GBind G Abst T).
(* Basic properties *********************************************************)
-axiom eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2).
+lemma eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2).
+#G1 elim G1 -G1 [| #G1 #I1 #T1 #IHG1 ] * [2,4: #G2 #I2 #T2 ]
+[3: /2 width=1 by or_introl/
+|2: elim (eq_bind2_dec I1 I2) #HI
+ [ elim (IHG1 G2) -IHG1 #HG
+ [ elim (eq_term_dec T1 T2) #HT /2 width=1 by or_introl/ ]
+ ]
+]
+@or_intror #H destruct /2 width=1 by/
+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 "basic_2/syntax/genv.ma".
+
+(* LENGTH OF A GLOBAL ENVIRONMENT *******************************************)
+
+rec definition glength G on G ≝ match G with
+[ GAtom ⇒ 0
+| GBind G _ _ ⇒ ↑(glength G)
+].
+
+interpretation "length (global environment)"
+ 'card G = (glength G).
(* Basic properties *********************************************************)
-lemma applv_nil: â\88\80T. â\92¶â\97\8a.T = T.
+lemma applv_nil: â\88\80T. â\92¶â\92º.T = T.
// qed.
lemma applv_cons: ∀V,Vs,T. ⒶV⨮Vs.T = ⓐV.ⒶVs.T.
}
]
[ { "global environments" * } {
+ [ [ "" ] "genv_length" + "( |?| )" * ]
[ [ "" ] "genv" * ]
}
]
(* *)
(**************************************************************************)
-include "ground_2/notation/constructors/nil_0.ma".
+include "ground_2/notation/constructors/circledE_1.ma".
include "ground_2/notation/constructors/oplusright_3.ma".
include "ground_2/lib/arith.ma".
| nil : list A
| cons: A → list A → list A.
-interpretation "nil (list)" 'Nil = (nil ?).
+interpretation "nil (list)" 'CircledE A = (nil A).
interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl).
(* Basic inversion lemmas on length *****************************************)
-lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 â\86\92 l = â\97\8a.
+lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 â\86\92 l = â\92º.
#A * // #a #l >length_cons #H destruct
qed-.
-lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| â\86\92 l = â\97\8a.
+lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| â\86\92 l = â\92º.
/2 width=1 by length_inv_zero_dx/ qed-.
lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x →
+++ /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/notation/constructors/nil_0.ma".
-include "ground_2/notation/constructors/oplusright_5.ma".
-include "ground_2/lib/arith.ma".
-
-(* LISTS OF PAIRS ***********************************************************)
-
-inductive list2 (A1,A2:Type[0]) : Type[0] :=
- | nil2 : list2 A1 A2
- | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2.
-
-interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?).
-
-interpretation "cons (list of pairs)"
- 'OPlusRight A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl).
-
-rec definition length2 A1 A2 (l:list2 A1 A2) on l ≝ match l with
-[ nil2 ⇒ 0
-| cons2 _ _ l ⇒ ↑(length2 A1 A2 l)
-].
-
-interpretation "length (list of pairs)"
- 'card l = (length2 ? ? 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 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation < "hvbox( Ⓔ )"
+ non associative with precedence 55
+ for @{ 'CircledE $S }.
+
+notation > "hvbox( Ⓔ )"
+ non associative with precedence 55
+ for @{ 'CircledE ? }.
+
+notation > "hvbox( Ⓔ{ term 46 C } )"
+ non associative with precedence 55
+ for @{ 'CircledE $S }.
--- /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 55
+ for @{ 'Diamond }.
+++ /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 < "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
- non associative with precedence 47
- for @{ 'OPlusRight $S1 $S2 $hd1 $hd2 $tl }.
-
-notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )"
- non associative with precedence 47
- for @{ 'OPlusRight ? ? $hd1 $hd2 $tl }.
-(*
-(**) fix pair notation
-notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮{ break term 46 S1, break term 46 S2 } break term 46 tl )"
- non associative with precedence 47
- for @{ 'OPlusRight $S1 $S2 $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 @{ 'Semicolon $hd1 $hd2 $tl }.
(* *)
(**************************************************************************)
-include "ground_2/lib/list2.ma".
+include "ground_2/notation/constructors/diamond_0.ma".
+include "ground_2/notation/constructors/semicolon_3.ma".
+include "ground_2/lib/arith.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-definition mr2: Type[0] ≝ list2 nat nat.
+inductive mr2: Type[0] :=
+ | nil2 : mr2
+ | cons2: nat → nat → mr2 → mr2.
+
+interpretation "nil (multiple relocation with pairs)"
+ 'Diamond = (nil2).
+
+interpretation "cons (multiple relocation with pairs)"
+ 'Semicolon hd1 hd2 tl = (cons2 hd1 hd2 tl).
inductive at: mr2 → relation nat ≝
| at_nil: ∀i. at (◊) i i
| at_lt : ∀cs,l,m,i1,i2. i1 < l →
- at cs i1 i2 → at ({l, m} ⨮ cs) i1 i2
+ at cs i1 i2 → at ({l, m};cs) i1 i2
| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 →
- at cs (i1 + m) i2 → at ({l, m} ⨮ cs) i1 i2
+ at cs (i1 + m) i2 → at ({l, m};cs) i1 i2
.
interpretation "application (multiple relocation with pairs)"
/2 width=3 by at_inv_nil_aux/ qed-.
fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≘ i2 →
- ∀l,m,cs0. cs = {l, m} ⨮ cs0 →
+ ∀l,m,cs0. cs = {l, m};cs0 →
i1 < l ∧ @⦃i1, cs0⦄ ≘ i2 ∨
l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≘ i2.
#cs #i1 #i2 * -cs -i1 -i2
]
qed-.
-lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 →
+lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m};cs⦄ ≘ i2 →
i1 < l ∧ @⦃i1, cs⦄ ≘ i2 ∨
l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≘ i2.
/2 width=3 by at_inv_cons_aux/ qed-.
-lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 →
+lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m};cs⦄ ≘ i2 →
i1 < l → @⦃i1, cs⦄ ≘ i2.
#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l
elim (lt_le_false … Hi1l Hli1)
qed-.
-lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 →
+lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m};cs⦄ ≘ i2 →
l ≤ i1 → @⦃i1 + m, cs⦄ ≘ i2.
#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
inductive minuss: nat → relation mr2 ≝
| minuss_nil: ∀i. minuss i (◊) (◊)
| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 →
- minuss i ({l, m} ⨮ cs1) ({l - i, m} ⨮ cs2)
+ minuss i ({l, m};cs1) ({l - i, m};cs2)
| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 →
- minuss i ({l, m} ⨮ cs1) cs2
+ minuss i ({l, m};cs1) cs2
.
interpretation "minus (multiple relocation with pairs)"
/2 width=4 by minuss_inv_nil1_aux/ qed-.
fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≘ cs2 →
- ∀l,m,cs. cs1 = {l, m} ⨮ cs →
+ ∀l,m,cs. cs1 = {l, m};cs →
l ≤ i ∧ cs ▭ m + i ≘ cs2 ∨
∃∃cs0. i < l & cs ▭ i ≘ cs0 &
- cs2 = {l - i, m} ⨮ cs0.
+ cs2 = {l - i, m};cs0.
#cs1 #cs2 #i * -cs1 -cs2 -i
[ #i #l #m #cs #H destruct
| #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/
]
qed-.
-lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 →
+lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m};cs1 ▭ i ≘ cs2 →
l ≤ i ∧ cs1 ▭ m + i ≘ cs2 ∨
∃∃cs. i < l & cs1 ▭ i ≘ cs &
- cs2 = {l - i, m} ⨮ cs.
+ cs2 = {l - i, m};cs.
/2 width=3 by minuss_inv_cons1_aux/ qed-.
-lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 →
+lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m};cs1 ▭ i ≘ cs2 →
l ≤ i → cs1 ▭ m + i ≘ cs2.
#cs1 #cs2 #l #m #i #H
elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli
elim (lt_le_false … Hil Hli)
qed-.
-lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 →
+lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m};cs1 ▭ i ≘ cs2 →
i < l →
- ∃∃cs. cs1 ▭ i ≘ cs & cs2 = {l - i, m} ⨮ cs.
+ ∃∃cs. cs1 ▭ i ≘ cs & cs2 = {l - i, m};cs.
#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
#Hli #_ #Hil elim (lt_le_false … Hil Hli)
qed-.
rec definition pluss (cs:mr2) (i:nat) on cs ≝ match cs with
[ nil2 ⇒ ◊
-| cons2 l m cs ⇒ {l + i, m} ⨮ pluss cs i
+| cons2 l m cs ⇒ {l + i, m};pluss cs i
].
interpretation "plus (multiple relocation with pairs)"
(* Basic properties *********************************************************)
-lemma pluss_SO2: ∀l,m,cs. ({l, m} ⨮ cs) + 1 = {↑l, m} ⨮ cs + 1.
+lemma pluss_SO2: ∀l,m,cs. ({l, m};cs) + 1 = {↑l, m};cs + 1.
normalize // qed.
(* Basic inversion lemmas ***************************************************)
#l #m #cs #H destruct
qed.
-lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} ⨮ cs2 →
- ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} ⨮ cs1.
+lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m};cs2 →
+ ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m};cs1.
#i #l #m #cs2 *
[ normalize #H destruct
| #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )" * ]
*)
- [ "mr2" "mr2_at ( @⦃?,?⦄ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ]
+ [ "mr2 ( ◊ ) ( {?,?};? )" "mr2_at ( @⦃?,?⦄ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ]
}
]
}
[ { "extensions to the library" * } {
[ { "" * } {
[ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
- [ "list ( â\97\8a ) ( ? ⨮{?} ? ) ( |?| )" "list2 ( â\97\8a ) ( {?,?} ⨮{?,?} ? ) ( |?| )" * ]
+ [ "list ( â\92º{?} ) ( ? ⨮{?} ? ) ( |?| )" * ]
[ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
[ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "ltc" * ]
}
#!/bin/sh
-for SRC in `find ground_2 basic_2 -name "*.ma" -or -name "*.tbl"`; do
+for SRC in `find ground_2 basic_2 apps_2 -name "*.ma" -or -name "*.tbl"`; do
sed "s!$1!$2!g" ${SRC} > ${SRC}.new
if [ ! -s ${SRC}.new ] || diff ${SRC} ${SRC}.new > /dev/null;
then rm -f ${SRC}.new;
projects / helm.git / commitdiff