| TPair I V T ⇒ ②{I}V.(tappend T U)
].
-interpretation "append (term)" 'Append T U = (tappend T U).
+interpretation "append (term)" 'plus T U = (tappend T U).
notation < "hvbox( ⫰[ break term 46 i ] break term 46 lv )"
non associative with precedence 46
- for @{ 'DownSpoon $M $d $lv }.
+ for @{ 'DownSpoon $M $i $lv }.
notation > "hvbox( ⫰[ break term 46 i ] break term 46 lv )"
non associative with precedence 46
- for @{ 'DownSpoon ? $d $lv }.
+ for @{ 'DownSpoon ? $i $lv }.
notation > "hvbox( ⫰{ term 46 M }[ break term 46 i ] break term 46 lv )"
non associative with precedence 46
- for @{ 'DownSpoon $M $d $lv }.
+ for @{ 'DownSpoon $M $i $lv }.
applications of λδ version 2.
In particular it contains the components below.
</body>
+ <topitem name="models">
+ <notice class="alpha" notice="Models."/>
+ Denotational semantics for λδ.
+ </topitem>
<topitem name="MLTT1">
<notice class="alpha" notice="MLTT1."/>
Martin-Löf's Type Theory with one universe
and its timeline.
</body>
<table name="apps_2_sum"/>
+ <news class="alpha" date="2018 April 30.">
+ The Models component is started for λδ version 2.
+ </news>
<news class="alpha" date="2017 March 6.">
The Examples component is moved from the Core directory.
</news>
| liftsv_nil : liftsv f (◊) (◊)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⬆*[f] T1 ≘ T2 → liftsv f T1s T2s →
- liftsv f (T1 @ T1s) (T2 @ T2s)
+ liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
.
interpretation "uniform relocation (term vector)"
/2 width=5 by liftsv_inv_nil1_aux/ qed-.
fact liftsv_inv_cons1_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
- ∀T1,T1s. X = T1 @ T1s →
+ ∀T1,T1s. X = T1 ⨮ T1s →
∃∃T2,T2s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
- Y = T2 @ T2s.
+ Y = T2 ⨮ T2s.
#f #X #Y * -X -Y
[ #U1 #U1s #H destruct
| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/
qed-.
(* Basic_2A1: includes: liftv_inv_cons1 *)
-lemma liftsv_inv_cons1: ∀f:rtmap. ∀T1,T1s,Y. ⬆*[f] T1 @ T1s ≘ Y →
+lemma liftsv_inv_cons1: ∀f:rtmap. ∀T1,T1s,Y. ⬆*[f] T1 ⨮ T1s ≘ Y →
∃∃T2,T2s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
- Y = T2 @ T2s.
+ Y = T2 ⨮ T2s.
/2 width=3 by liftsv_inv_cons1_aux/ qed-.
fact liftsv_inv_nil2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → Y = ◊ → X = ◊.
/2 width=5 by liftsv_inv_nil2_aux/ qed-.
fact liftsv_inv_cons2_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y →
- ∀T2,T2s. Y = T2 @ T2s →
+ ∀T2,T2s. Y = T2 ⨮ T2s →
∃∃T1,T1s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
- X = T1 @ T1s.
+ X = T1 ⨮ T1s.
#f #X #Y * -X -Y
[ #U2 #U2s #H destruct
| #T1s #T2s #T1 #T2 #HT12 #HT12s #U2 #U2s #H destruct /2 width=5 by ex3_2_intro/
]
qed-.
-lemma liftsv_inv_cons2: ∀f:rtmap. ∀X,T2,T2s. ⬆*[f] X ≘ T2 @ T2s →
+lemma liftsv_inv_cons2: ∀f:rtmap. ∀X,T2,T2s. ⬆*[f] X ≘ T2 ⨮ T2s →
∃∃T1,T1s. ⬆*[f] T1 ≘ T2 & ⬆*[f] T1s ≘ T2s &
- X = T1 @ T1s.
+ X = T1 ⨮ T1s.
/2 width=3 by liftsv_inv_cons2_aux/ qed-.
(* Basic_1: was: lifts1_flat (left to right) *)
#X #H #H0
elim (cpxs_fwd_sort_vector … o … H) -H #H
[ elim H0 -H0 //
- | -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s)))
+ | -H0 @(csx_cpxs_trans … (Ⓐ(V⨮Vs).⋆(next h s)))
/3 width=1 by cpxs_flat_dx, deg_next_SO/
]
]
lapply (csx_fwd_pair_sn … H) #HW1
lapply (csx_fwd_flat_dx … H) #H1
@csx_appl_simple_theq /2 width=3 by simple_flat/ -IHV12b -HW1 -H1 #X #H1 #H2
-elim (cpxs_fwd_theta_vector … o … (V2@V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
+elim (cpxs_fwd_theta_vector … o … (V2⨮V2b) … H1) -H1 /2 width=1 by liftsv_cons/ -HV12b -HV12
[ -H #H elim H2 -H2 //
| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
]
(* Basic inversion lemmas ***************************************************)
-lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T@Ts⦄ →
+lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⨮Ts⦄ →
⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Ts⦄.
normalize // qed-.
| #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
lapply (s1 … IHB … HB) #HV0
- @(s2 … IHA … (V0@V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/
+ @(s2 … IHA … (V0⨮V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/
| #p #G #L #Vs #U #T #W #HA #f #L0 #V0 #X #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
elim (lifts_inv_flat1 … H0) -H0 #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
- @(s3 … IHA … (V0@V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
+ @(s3 … IHA … (V0⨮V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
| #G #L #Vs #HVs #s #f #L0 #V0 #X #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
>(lifts_inv_sort1 … H0) -X0
lapply (s1 … IHB … HB) #HV0
- @(s4 … IHA … (V0@V0s)) /3 width=7 by gcp2_all, conj/
+ @(s4 … IHA … (V0⨮V0s)) /3 width=7 by gcp2_all, conj/
| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #f #L0 #V0 #X #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
elim (lifts_total W1 (𝐔❴↑j❵)) #W2 #HW12
lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H
lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by after_uni_succ_sn/ ] #HVW2
- @(s5 … IHA … (V0@V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/
+ @(s5 … IHA … (V0⨮V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/
| #G #L #V1s #V2s #HV12s #p #V #T #HA #HV #f #L0 #V10 #X #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V10s #X0 #HV10s #H0 #H destruct
elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
elim (lifts_total V10 (𝐔❴1❵)) #V20 #HV120
elim (liftsv_total (𝐔❴1❵) V10s) #V20s #HV120s
- @(s6 … IHA … (V10@V10s) (V20@V20s)) /3 width=7 by cp2, liftsv_cons/
+ @(s6 … IHA … (V10⨮V10s) (V20⨮V20s)) /3 width=7 by cp2, liftsv_cons/
@(HA … (⫯f)) /3 width=2 by drops_skip, ext2_pair/
[ @lifts_applv //
lapply (liftsv_trans … HV10s … HV120s ??) -V10s [3: |*: // ] #H
| #G #L #Vs #T #W #HA #HW #f #L0 #V0 #X #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #X0 #HV0s #H0 #H destruct
elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
- @(s7 … IHA … (V0@V0s)) /3 width=5 by lifts_applv/
+ @(s7 … IHA … (V0⨮V0s)) /3 width=5 by lifts_applv/
]
qed.
(* *)
(**************************************************************************)
-include "ground_2/notation/functions/append_2.ma".
include "basic_2/notation/functions/snitem_2.ma".
include "basic_2/notation/functions/snbind1_2.ma".
include "basic_2/notation/functions/snbind2_3.ma".
| LBind K I ⇒ (append L K).ⓘ{I}
].
-interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
+interpretation "append (local environment)" 'plus L1 L2 = (append L1 L2).
interpretation "local environment tail binding construction (generic)"
'SnItem I L = (append (LBind LAtom I) L).
'SnAbst L T = (append (LBind LAtom (BPair Abst T)) L).
definition d_appendable_sn: predicate (lenv→relation term) ≝ λR.
- ∀K,T1,T2. R K T1 T2 → ∀L. R (L@@K) T1 T2.
+ ∀K,T1,T2. R K T1 T2 → ∀L. R (L+K) T1 T2.
(* Basic properties *********************************************************)
-lemma append_atom: ∀L. L @@ ⋆ = L.
+lemma append_atom: ∀L. (L + ⋆) = L. (**) (* () should be redundant *)
// qed.
(* Basic_2A1: uses: append_pair *)
-lemma append_bind: ∀I,L,K. L@@(K.ⓘ{I}) = (L@@K).ⓘ{I}.
+lemma append_bind: ∀I,L,K. L+(K.ⓘ{I}) = (L+K).ⓘ{I}.
// qed.
-lemma append_atom_sn: ∀L. ⋆@@L = L.
+lemma append_atom_sn: ∀L. ⋆ + L = L.
#L elim L -L //
#L #I >append_bind //
qed.
#L1 #L2 #L3 elim L3 -L3 //
qed.
-lemma append_shift: ∀L,K,I. L@@(ⓘ{I}.K) = (L.ⓘ{I})@@K.
+lemma append_shift: ∀L,K,I. L+(ⓘ{I}.K) = (L.ⓘ{I})+K.
#L #K #I <append_assoc //
qed.
(* Basic inversion lemmas ***************************************************)
-lemma append_inv_atom3_sn: ∀L,K. ⋆ = L @@ K → ∧∧ ⋆ = L & ⋆ = K.
+lemma append_inv_atom3_sn: ∀L,K. ⋆ = L + K → ∧∧ ⋆ = L & ⋆ = K.
#L * /2 width=1 by conj/
#K #I >append_bind #H destruct
qed-.
-lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L @@ K →
+lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L + K →
∨∨ ∧∧ L0.ⓘ{I0} = L & ⋆ = K
- | ∃∃K0. K = K0.ⓘ{I0} & L0 = L @@ K0.
+ | ∃∃K0. K = K0.ⓘ{I0} & L0 = L + K0.
#I0 #L #L0 * /3 width=1 by or_introl, conj/
#K #I >append_bind #H destruct /3 width=3 by ex2_intro, or_intror/
qed-.
-lemma append_inj_sn: ∀K,L1,L2. L1@@K = L2@@K → L1 = L2.
+lemma append_inj_sn: ∀K,L1,L2. L1+K = L2+K → L1 = L2.
#K elim K -K //
#K #I #IH #L1 #L2 >append_bind #H
elim (destruct_lbind_lbind_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
(* Properties with length for local environments ****************************)
-lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
+lemma append_length: ∀L1,L2. |L1 + L2| = |L1| + |L2|.
#L1 #L2 elim L2 -L2 //
#L2 #I >append_bind >length_bind >length_bind //
qed.
(* Inversion lemmas with length for local environments **********************)
(* Basic_2A1: was: append_inj_sn *)
-lemma append_inj_length_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| →
+lemma append_inj_length_sn: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |K1| = |K2| →
L1 = L2 ∧ K1 = K2.
#K1 elim K1 -K1
[ * /2 width=1 by conj/
(* Note: lemma 750 *)
(* Basic_2A1: was: append_inj_dx *)
-lemma append_inj_length_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| →
+lemma append_inj_length_dx: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |L1| = |L2| →
L1 = L2 ∧ K1 = K2.
#K1 elim K1 -K1
[ * /2 width=1 by conj/
(* Advanced inversion lemmas ************************************************)
-lemma append_inj_dx: ∀L,K1,K2. L@@K1 = L@@K2 → K1 = K2.
+lemma append_inj_dx: ∀L,K1,K2. L+K1 = L+K2 → K1 = K2.
#L #K1 #K2 #H elim (append_inj_length_dx … H) -H //
qed-.
-lemma append_inv_refl_dx: ∀L,K. L@@K = L → K = ⋆.
+lemma append_inv_refl_dx: ∀L,K. L+K = L → K = ⋆.
#L #K #H elim (append_inj_dx … (⋆) … H) //
qed-.
-lemma append_inv_pair_dx: ∀I,L,K,V. L@@K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
+lemma append_inv_pair_dx: ∀I,L,K,V. L+K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
#I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
qed-.
lemma applv_nil: ∀T. Ⓐ◊.T = T.
// qed.
-lemma applv_cons: ∀V,Vs,T. ⒶV@Vs.T = ⓐV.ⒶVs.T.
+lemma applv_cons: ∀V,Vs,T. ⒶV⨮Vs.T = ⓐV.ⒶVs.T.
// qed.
(* Properties with simple terms *********************************************)
--- /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/functions/oplus_4.ma".
+include "ground_2/lib/list2.ma".
+
+(* LISTS OF PAIRS ***********************************************************)
+
+rec definition append2 A1 A2 (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
+[ nil2 ⇒ l2
+| cons2 a1 a2 tl ⇒ {a1, a2} ⨮ append2 A1 A2 tl l2
+].
+
+interpretation "append (list of pairs)"
+ 'OPlus A1 A2 l1 l2 = (append2 A1 A2 l1 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( l1 ⊕ break l2 )"
+ left associative with precedence 60
+ for @{ 'OPlus $A $B $l1 $l2 }.
+
+notation > "hvbox( l1 ⊕ break l2 )"
+ left associative with precedence 60
+ for @{ 'OPlus ? ? $l1 $l2 }.
+(*
+(**) fix pair notation
+notation > "hvbox( l1 ⊕{ break term 46 A, break term 46 A } break term 61 l2 )"
+ non associative with precedence 60
+ for @{ 'OPlus $A $B $l1 $l2 }.
+*)
(**************************************************************************)
include "ground_2/notation/constructors/nil_0.ma".
-include "ground_2/notation/constructors/cons_2.ma".
+include "ground_2/notation/constructors/oplusright_3.ma".
include "ground_2/lib/arith.ma".
(* LISTS ********************************************************************)
interpretation "nil (list)" 'Nil = (nil ?).
-interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
+interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl).
-rec definition length (A:Type[0]) (l:list A) on l ≝ match l with
+rec definition length A (l:list A) on l ≝ match l with
[ nil ⇒ 0
| cons _ l ⇒ ↑(length A l)
].
lemma length_nil (A:Type[0]): |nil A| = 0.
// qed.
-lemma length_cons (A:Type[0]) (l:list A) (a:A): |a@l| = ↑|l|.
+lemma length_cons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
// qed.
(* Basic inversion lemmas on length *****************************************)
/2 width=1 by length_inv_zero_dx/ qed-.
lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x →
- ∃∃tl,a. x = |tl| & l = a @ tl.
+ ∃∃tl,a. x = |tl| & l = a ⨮ tl.
#A * /2 width=4 by ex2_2_intro/
>length_nil #x #H destruct
qed-.
lemma length_inv_succ_sn (A:Type[0]) (l:list A) (x): ↑x = |l| →
- ∃∃tl,a. x = |tl| & l = a @ tl.
+ ∃∃tl,a. x = |tl| & l = a ⨮ tl.
/2 width=1 by length_inv_succ_dx/ qed.
(**************************************************************************)
include "ground_2/notation/constructors/nil_0.ma".
-include "ground_2/notation/constructors/cons_3.ma".
-include "ground_2/notation/functions/append_2.ma".
+include "ground_2/notation/constructors/oplusright_5.ma".
include "ground_2/lib/arith.ma".
(* LISTS OF PAIRS ***********************************************************)
interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?).
-interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
+interpretation "cons (list of pairs)"
+ 'OPlusRight A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl).
-rec definition append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
-[ nil2 ⇒ l2
-| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2
-].
-
-interpretation "append (list of pairs)"
- 'Append l1 l2 = (append2 ? ? l1 l2).
-
-rec definition length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
+rec definition length2 A1 A2 (l:list2 A1 A2) on l ≝ match l with
[ nil2 ⇒ 0
| cons2 _ _ l ⇒ ↑(length2 A1 A2 l)
].
(* *)
(**************************************************************************)
-include "ground_2/notation/constructors/cons_2.ma".
+include "ground_2/notation/constructors/oplusright_3.ma".
include "ground_2/lib/relations.ma".
(* STREAMS ******************************************************************)
| seq: A → stream A → stream A
.
-interpretation "cons (nstream)" 'Cons b t = (seq ? b t).
+interpretation "cons (nstream)" 'OPlusRight A a u = (seq A a u).
(* Basic properties *********************************************************)
-lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a @ u ] = t.
+lemma stream_rew (A) (t:stream A): match t with [ seq a u ⇒ a ⨮ u ] = t.
#A * //
qed.
(* STREAMS ******************************************************************)
coinductive eq_stream (A): relation (stream A) ≝
-| eq_seq: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1@t1) (b2@t2)
+| eq_seq: ∀t1,t2,b1,b2. b1 = b2 → eq_stream A t1 t2 → eq_stream A (b1⨮t1) (b2⨮t2)
.
interpretation "extensional equivalence (nstream)"
(* Basic inversion lemmas ***************************************************)
lemma eq_stream_inv_seq: ∀A,t1,t2. t1 ≗{A} t2 →
- ∀u1,u2,a1,a2. a1@u1 = t1 → a2@u2 = t2 →
+ ∀u1,u2,a1,a2. a1⨮u1 = t1 → a2⨮u2 = t2 →
u1 ≗ u2 ∧ a1 = a2.
#A #t1 #t2 * -t1 -t2
#t1 #t2 #b1 #b2 #Hb #Ht #u1 #u2 #a1 #a2 #H1 #H2 destruct /2 width=1 by conj/
(* *)
(**************************************************************************)
-include "ground_2/notation/functions/downspoon_1.ma".
+include "ground_2/notation/functions/downspoon_2.ma".
include "ground_2/lib/streams_eq.ma".
include "ground_2/lib/arith.ma".
definition tl (A:Type[0]): stream A → stream A ≝
λt. match t with [ seq _ t ⇒ t ].
-interpretation "tail (streams)" 'DownSpoon t = (tl ? t).
+interpretation "tail (streams)" 'DownSpoon A t = (tl A t).
(* basic properties *********************************************************)
-lemma hd_rew (A) (a) (t): a = hd A (a@t).
+lemma hd_rew (A) (a) (t): a = hd A (a⨮t).
// qed.
-lemma tl_rew (A) (a) (t): t = tl A (a@t).
+lemma tl_rew (A) (a) (t): t = tl A (a⨮t).
// qed.
-lemma eq_stream_split (A) (t): (hd … t) @ ⫰t ≗{A} t.
+lemma eq_stream_split (A) (t): (hd … t) ⨮ ⫰t ≗{A} t.
#A * //
qed.
(* *)
(**************************************************************************)
-include "ground_2/notation/functions/downspoonstar_2.ma".
+include "ground_2/notation/functions/downspoonstar_3.ma".
include "ground_2/lib/streams_hdtl.ma".
(* STREAMS ******************************************************************)
cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
defined.
-interpretation "recursive tail (strams)" 'DownSpoonStar n f = (tls ? n f).
+interpretation "iterated tail (strams)" 'DownSpoonStar A n f = (tls A n f).
(* basic properties *********************************************************)
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 }.
+ 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 }.
+ 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 }.
+ 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( l1 @@ break l2 )"
- right associative with precedence 47
- for @{ 'Append $l1 $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( ⫰ term 46 T )"
- non associative with precedence 46
- for @{ 'DownSpoon $T }.
--- /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 a )"
+ non associative with precedence 46
+ for @{ 'DownSpoon $S $a }.
+
+notation > "hvbox( ⫰ term 46 a )"
+ non associative with precedence 46
+ for @{ 'DownSpoon ? $a }.
+
+notation > "hvbox( ⫰{ term 46 S } break term 46 a )"
+ non associative with precedence 46
+ for @{ 'DownSpoon $S $a }.
+++ /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 n ] term 46 T )"
- non associative with precedence 46
- for @{ 'DownSpoonStar $n $T }.
--- /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( ⫰*[ break term 46 n ] break term 46 a )"
+ non associative with precedence 46
+ for @{ 'DownSpoonStar $S $n $a }.
+
+notation > "hvbox( ⫰*[ break term 46 n ] break term 46 a )"
+ non associative with precedence 46
+ for @{ 'DownSpoonStar ? $n $a }.
+
+notation > "hvbox( ⫰*{ term 46 S }[ break term 46 n ] break term 46 a )"
+ non associative with precedence 46
+ for @{ 'DownSpoonStar $S $n $a }.
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
definition rtmap: Type[0] ≝ stream nat.
-definition push: rtmap → rtmap ≝ λf. 0@f.
+definition push: rtmap → rtmap ≝ λf. 0⨮f.
interpretation "push (nstream)" 'UpSpoon f = (push f).
definition next: rtmap → rtmap.
-* #n #f @(↑n@f)
+* #n #f @(↑n⨮f)
defined.
interpretation "next (nstream)" 'UpArrow f = (next f).
(* Basic properties *********************************************************)
-lemma push_rew: ∀f. 0@f = ⫯f.
+lemma push_rew: ∀f. 0⨮f = ⫯f.
// qed.
-lemma next_rew: ∀f,n. (↑n)@f = ↑(n@f).
+lemma next_rew: ∀f,n. (↑n)⨮f = ↑(n⨮f).
// qed.
(* Basic inversion lemmas ***************************************************)
* #n1 #f1 * #n2 #f2 normalize #H destruct //
qed-.
-lemma push_inv_seq_sn: ∀f,g,n. n@g = ⫯f → 0 = n ∧ g = f.
+lemma push_inv_seq_sn: ∀f,g,n. n⨮g = ⫯f → 0 = n ∧ g = f.
#f #g #n <push_rew #H destruct /2 width=1 by conj/
qed-.
-lemma push_inv_seq_dx: ∀f,g,n. ⫯f = n@g → 0 = n ∧ g = f.
+lemma push_inv_seq_dx: ∀f,g,n. ⫯f = n⨮g → 0 = n ∧ g = f.
#f #g #n <push_rew #H destruct /2 width=1 by conj/
qed-.
-lemma next_inv_seq_sn: ∀f,g,n. n@g = ↑f → ∃∃m. m@g = f & ↑m = n.
+lemma next_inv_seq_sn: ∀f,g,n. n⨮g = ↑f → ∃∃m. m⨮g = f & ↑m = n.
* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
qed-.
-lemma next_inv_seq_dx: ∀f,g,n. ↑f = n@g → ∃∃m. m@g = f & ↑m = n.
+lemma next_inv_seq_dx: ∀f,g,n. ↑f = n⨮g → ∃∃m. m⨮g = f & ↑m = n.
* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
qed-.
(* Basic properies on compose ***********************************************)
-lemma compose_rew: ∀f2,f1,n1. f2@❴n1❵@(⫰*[↑n1]f2)∘f1 = f2∘(n1@f1).
-#f2 #f1 #n1 <(stream_rew … (f2∘(n1@f1))) normalize //
+lemma compose_rew: ∀f2,f1,n1. f2@❴n1❵⨮(⫰*[↑n1]f2)∘f1 = f2∘(n1⨮f1).
+#f2 #f1 #n1 <(stream_rew … (f2∘(n1⨮f1))) normalize //
qed.
lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
(* Basic inversion lemmas on compose ****************************************)
-lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1@f1) = n@f →
+lemma compose_inv_rew: ∀f2,f1,f,n1,n. f2∘(n1⨮f1) = n⨮f →
f2@❴n1❵ = n ∧ (⫰*[↑n1]f2)∘f1 = f.
-#f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1@f1))) normalize
+#f2 #f1 #f #n1 #n <(stream_rew … (f2∘(n1⨮f1))) normalize
#H destruct /2 width=1 by conj/
qed-.
-lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2@f2)∘(⫯f1) = n@f →
+lemma compose_inv_O2: ∀f2,f1,f,n2,n. (n2⨮f2)∘(⫯f1) = n⨮f →
n2 = n ∧ f2∘f1 = f.
#f2 #f1 #f #n2 #n <compose_rew
#H destruct /2 width=1 by conj/
qed-.
-lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2@f2)∘(↑n1@f1) = n@f →
- ↑(n2+f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S2: ∀f2,f1,f,n2,n1,n. (n2⨮f2)∘(↑n1⨮f1) = n⨮f →
+ ↑(n2+f2@❴n1❵) = n ∧ f2∘(n1⨮f1) = f2@❴n1❵⨮f.
#f2 #f1 #f #n2 #n1 #n <compose_rew
#H destruct <tls_S1 /2 width=1 by conj/
qed-.
-lemma compose_inv_S1: ∀f2,f1,f,n1,n. (↑f2)∘(n1@f1) = n@f →
- ↑(f2@❴n1❵) = n ∧ f2∘(n1@f1) = f2@❴n1❵@f.
+lemma compose_inv_S1: ∀f2,f1,f,n1,n. (↑f2)∘(n1⨮f1) = n⨮f →
+ ↑(f2@❴n1❵) = n ∧ f2∘(n1⨮f1) = f2@❴n1❵⨮f.
#f2 #f1 #f #n1 #n <compose_rew
#H destruct <tls_S1 /2 width=1 by conj/
qed-.
(* Specific properties on after *********************************************)
lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
- ∀n. n@f2 ⊚ ⫯f1 ≘ n@f.
+ ∀n. n⨮f2 ⊚ ⫯f1 ≘ n⨮f.
#f2 #f1 #f #Hf #n elim n -n /2 width=7 by after_refl, after_next/
qed.
-lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≘ n@f →
- ∀n2. n2@f2 ⊚ ↑n1@f1 ≘ ↑(n2+n)@f.
+lemma after_S2: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f →
+ ∀n2. n2⨮f2 ⊚ ↑n1⨮f1 ≘ ↑(n2+n)⨮f.
#f2 #f1 #f #n1 #n #Hf #n2 elim n2 -n2 /2 width=7 by after_next, after_push/
qed.
-lemma after_apply: ∀n1,f2,f1,f. (⫰*[↑n1] f2) ⊚ f1 ≘ f → f2 ⊚ n1@f1 ≘ f2@❴n1❵@f.
+lemma after_apply: ∀n1,f2,f1,f. (⫰*[↑n1] f2) ⊚ f1 ≘ f → f2 ⊚ n1⨮f1 ≘ f2@❴n1❵⨮f.
#n1 elim n1 -n1
[ * /2 width=1 by after_O2/
| #n1 #IH * /3 width=1 by after_S2/
(* Specific inversion lemmas on after ***************************************)
-lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≘ n@f → ∀f1. ⫯f1 = g2 →
+lemma after_inv_xpx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ⫯f1 = g2 →
f2 ⊚ f1 ≘ f ∧ n2 = n.
#f2 #g2 #f #n2 elim n2 -n2
[ #n #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [2,3: // ]
]
qed-.
-lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2@f2 ⊚ g2 ≘ n@f → ∀f1. ↑f1 = g2 →
- ∃∃m. f2 ⊚ f1 ≘ m@f & ↑(n2+m) = n.
+lemma after_inv_xnx: ∀f2,g2,f,n2,n. n2⨮f2 ⊚ g2 ≘ n⨮f → ∀f1. ↑f1 = g2 →
+ ∃∃m. f2 ⊚ f1 ≘ m⨮f & ↑(n2+m) = n.
#f2 #g2 #f #n2 elim n2 -n2
[ #n #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [2,3: // ]
#g #Hf #H elim (next_inv_seq_dx … H) -H
]
qed-.
-lemma after_inv_const: ∀f2,f1,f,n1,n. n@f2 ⊚ n1@f1 ≘ n@f → f2 ⊚ f1 ≘ f ∧ 0 = n1.
+lemma after_inv_const: ∀f2,f1,f,n1,n. n⨮f2 ⊚ n1⨮f1 ≘ n⨮f → f2 ⊚ f1 ≘ f ∧ 0 = n1.
#f2 #f1 #f #n1 #n elim n -n
[ #H elim (after_inv_pxp … H) -H [ |*: // ]
#g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
(* Specific forward lemmas on after *****************************************)
-lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1@f1 ≘ n@f → f2@❴n1❵ = n.
+lemma after_fwd_hd: ∀f2,f1,f,n1,n. f2 ⊚ n1⨮f1 ≘ n⨮f → f2@❴n1❵ = n.
#f2 #f1 #f #n1 #n #H lapply (after_fwd_at ? n1 0 … H) -H [1,2,3: // ]
/3 width=2 by at_inv_O1, sym_eq/
qed-.
-lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2@f2 ⊚ n1@f1 ≘ n@f →
+lemma after_fwd_tls: ∀f,f1,n1,f2,n2,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
(⫰*[n1]f2) ⊚ f1 ≘ f.
#f #f1 #n1 elim n1 -n1
[ #f2 #n2 #n #H elim (after_inv_xpx … H) -H //
]
qed-.
-lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2@f2 ⊚ n1@f1 ≘ n@f →
- (n2@f2)@❴n1❵ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f.
+lemma after_inv_apply: ∀f2,f1,f,n2,n1,n. n2⨮f2 ⊚ n1⨮f1 ≘ n⨮f →
+ (n2⨮f2)@❴n1❵ = n ∧ (⫰*[n1]f2) ⊚ f1 ≘ f.
/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
defined.
rec definition fun2 (n1:nat) on n1: rtmap → rtmap.
-* * [ | #n2 #f2 @(n2@f2) ]
+* * [ | #n2 #f2 @(n2⨮f2) ]
#f2 cases n1 -n1 [ @f2 ]
#n1 @(fun2 n1 f2)
defined.
rec definition fun1 (n1:nat) (f1:rtmap) on n1: rtmap → rtmap.
-* * [ | #n2 #f2 @(n1@f1) ]
+* * [ | #n2 #f2 @(n1⨮f1) ]
#f2 cases n1 -n1 [ @f1 ]
#n1 @(fun1 n1 f1 f2)
defined.
* #n2 #f2 * //
qed.
-lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1@f1.
+lemma fun1_xxn: ∀f2,f1,n1. fun1 n1 f1 (↑f2) = n1⨮f1.
* #n2 #f2 #f1 * //
qed.
(* Basic properies on cocompose *********************************************)
-lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)@(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1@f1).
-#f2 #f1 #n1 <(stream_rew … (f2~∘(n1@f1))) normalize //
+lemma cocompose_rew: ∀f2,f1,n1. (fun0 n1 f2)⨮(fun2 n1 f2)~∘(fun1 n1 f1 f2) = f2 ~∘ (n1⨮f1).
+#f2 #f1 #n1 <(stream_rew … (f2~∘(n1⨮f1))) normalize //
qed.
(* Basic inversion lemmas on compose ****************************************)
-lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x@f →
+lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f →
0 = x ∧ f2 ~∘ f1 = f.
#f2 #f1 #f #x
<cocompose_rew #H destruct
normalize /2 width=1 by conj/
qed-.
-lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ ((↑n1)@f1) = x@f →
- ∃∃n. ↑n = x & f2 ~∘ (n1@f1) = n@f.
+lemma cocompose_inv_pnx: ∀f2,f1,f,n1,x. (⫯f2) ~∘ (↑n1⨮f1) = x⨮f →
+ ∃∃n. ↑n = x & f2 ~∘ (n1⨮f1) = n⨮f.
#f2 #f1 #f #n1 #x
<cocompose_rew #H destruct
@(ex2_intro … (fun0 n1 f2)) // <cocompose_rew
/3 width=1 by eq_f2/
qed-.
-lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (↑f2) ~∘ (n1@f1) = x@f →
- 0 = x ∧ f2 ~∘ (n1@f1) = f.
+lemma cocompose_inv_nxx: ∀f2,f1,f,n1,x. (↑f2) ~∘ (n1⨮f1) = x⨮f →
+ 0 = x ∧ f2 ~∘ (n1⨮f1) = f.
#f2 #f1 #f #n1 #x
<cocompose_rew #H destruct
/2 width=1 by conj/
(* Specific properties ******************************************************)
-fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1@f1 ≡ n2@f2 → n1 = n2 ∧ f1 ≡ f2.
+fact eq_inv_seq_aux: ∀f1,f2,n1,n2. n1⨮f1 ≡ n2⨮f2 → n1 = n2 ∧ f1 ≡ f2.
#f1 #f2 #n1 #n2 @(nat_elim2 … n1 n2) -n1 -n2
[ #n2 #H elim (eq_inv_px … H) -H [2,3: // ]
#g1 #H1 #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
]
qed-.
-lemma eq_inv_seq: ∀g1,g2. g1 ≡ g2 → ∀f1,f2,n1,n2. n1@f1 = g1 → n2@f2 = g2 →
+lemma eq_inv_seq: ∀g1,g2. g1 ≡ g2 → ∀f1,f2,n1,n2. n1⨮f1 = g1 → n2⨮f2 = g2 →
n1 = n2 ∧ f1 ≡ f2.
/2 width=1 by eq_inv_seq_aux/ qed-.
#n @eq_next /3 width=5 by eq_seq/
qed.
-lemma eq_seq_id: ∀f1,f2. f1 ≡ f2 → ∀n. n@f1 ≡ n@f2.
+lemma eq_seq_id: ∀f1,f2. f1 ≡ f2 → ∀n. n⨮f1 ≡ n⨮f2.
/4 width=1 by nstream_inv_eq, nstream_eq, eq_seq/ qed.
(* Specific inversion lemmas ************************************************)
-lemma isid_inv_seq: ∀f,n. 𝐈⦃n@f⦄ → 𝐈⦃f⦄ ∧ 0 = n.
+lemma isid_inv_seq: ∀f,n. 𝐈⦃n⨮f⦄ → 𝐈⦃f⦄ ∧ 0 = n.
#f #n #H elim (isid_inv_gen … H) -H
#g #Hg #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
qed-.
(* Specific properties on at ************************************************)
-lemma at_O1: ∀i2,f. @⦃0, i2@f⦄ ≘ i2.
+lemma at_O1: ∀i2,f. @⦃0, i2⨮f⦄ ≘ i2.
#i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
qed.
-lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≘ i2 → @⦃↑i1, n@f⦄ ≘ ↑(n+i2).
+lemma at_S1: ∀n,f,i1,i2. @⦃i1, f⦄ ≘ i2 → @⦃↑i1, n⨮f⦄ ≘ ↑(n+i2).
#n elim n -n /3 width=7 by at_push, at_next/
qed.
lemma at_istot: ∀f. 𝐓⦃f⦄.
/2 width=2 by ex_intro/ qed.
-lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≘ i → @⦃i1, (m+n)@f⦄ ≘ m+i.
+lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n⨮f⦄ ≘ i → @⦃i1, (m+n)⨮f⦄ ≘ m+i.
#f #i1 #i #n #m #H elim m -m //
#m <plus_S1 /2 width=5 by at_next/ (**) (* full auto fails *)
qed.
(* Specific inversion lemmas on at ******************************************)
-lemma at_inv_O1: ∀f,n,i2. @⦃0, n@f⦄ ≘ i2 → n = i2.
+lemma at_inv_O1: ∀f,n,i2. @⦃0, n⨮f⦄ ≘ i2 → n = i2.
#f #n elim n -n /2 width=6 by at_inv_ppx/
#n #IH #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
#j2 #Hj * -i2 /3 width=1 by eq_f/
qed-.
-lemma at_inv_S1: ∀f,n,j1,i2. @⦃↑j1, n@f⦄ ≘ i2 →
+lemma at_inv_S1: ∀f,n,j1,i2. @⦃↑j1, n⨮f⦄ ≘ i2 →
∃∃j2. @⦃j1, f⦄ ≘ j2 & ↑(n+j2) = i2.
#f #n elim n -n /2 width=5 by at_inv_npx/
#n #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [2,3: // ]
(* Spercific forward lemmas on at *******************************************)
-lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n@f⦄ ≘ i2 → i1 + n ≤ i2.
+lemma at_increasing_plus: ∀f,n,i1,i2. @⦃i1, n⨮f⦄ ≘ i2 → i1 + n ≤ i2.
#f #n *
[ #i2 #H <(at_inv_O1 … H) -i2 //
| #i1 #i2 #H elim (at_inv_S1 … H) -H
]
qed-.
-lemma at_fwd_id: ∀f,n,i. @⦃i, n@f⦄ ≘ i → 0 = n.
+lemma at_fwd_id: ∀f,n,i. @⦃i, n⨮f⦄ ≘ i → 0 = n.
#f #n #i #H elim (at_fwd_id_ex … H) -H
#g #H elim (push_inv_seq_dx … H) -H //
qed-.
class "yellow"
[ { "extensions to the library" * } {
[ { "" * } {
- [ "stream ( ? @ ? )" "stream_eq ( ? ≗ ? )" "stream_hdtl ( ⫰? )" "stream_tls ( ⫰*[?]? )" * ]
- [ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ]
+ [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
+ [ "list ( ◊ ) ( ? ⨮{?} ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} ⨮{?,?} ? ) ( |?| )" * ]
[ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ]
[ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "star" "ltc" * ]
}
basic_2/rt_transition
basic_2/rt_conversion
apps_2/examples/ex_cpr_omega.ma
+apps_2/models/
projects / helm.git / commitdiff