module ET = MrcTypes
+module RL = RecommLib
let read_substs substs ich =
- let map subst =
- let words = String.split_on_char ' ' subst in
- List.filter ((<>) "") words
- in
while true do
let line = input_line ich in
- let subst = String.split_on_char ',' line in
- substs := List.map map subst :: !substs
+ let subst = RL.split_on_char ',' line in
+ substs := List.map (RL.split_on_char ' ') subst :: !substs
done
let read_file file =
let force = ref false
+let subst = ref None
+
let chdir path =
Sys.chdir path
+let start_substs () =
+ subst := Some (open_out "subst.txt")
+
+let write_substs lint = function
+ | None -> ()
+ | Some och -> EO.write_substs och lint
+
+let stop_substs = function
+ | None -> ()
+ | Some och -> close_out och
+
let rec process path name =
let file = Filename.concat path name in
if Sys.is_directory file then begin
Printf.eprintf "processing: %S\n" file;
let orig = EI.read_srcs file in
let lint = EC.recomm_srcs orig in
+ write_substs lint !subst;
if !force || (!write && lint <> orig) then EO.write_srcs file lint
end else begin
Printf.eprintf "skipping: %S\n" file
let msg_r = " Replace the input files (default: no)"
let msg_s = " Log section comments (default: no)"
let msg_t = " Log title comments (default: no)"
+let msg_u = " Write substitution file (default: no)"
let msg_w = " Write the changed output files (default: no)"
let main =
"-r", Arg.Set EO.replace, msg_r;
"-s", Arg.Set EC.log_s, msg_s;
"-t", Arg.Set EC.log_t, msg_t;
+ "-u", Arg.Unit start_substs, msg_u;
"-w", Arg.Set write, msg_w;
- ] (process "") ""
+ ] (process "") "";
+ stop_substs !subst
let rec recomm srcs st =
match srcs with
- | [] ->
+ | [] ->
st
- | ET.Line _ as hd :: tl ->
+ | ET.Line _ as hd :: tl ->
recomm tl @@ add hd @@ st
- | ET.Text _ as hd :: tl ->
+ | ET.Text _ as hd :: tl ->
recomm tl @@ add hd @@ st
- | ET.Mark s as hd :: tl ->
+ | ET.Mark s as hd :: tl ->
if !log_m then log red s;
recomm tl @@ add hd @@ st
- | ET.Key (s1, s2) as hd :: tl ->
+ | ET.Key (s1, s2) as hd :: tl ->
if middle st then Printf.eprintf "middle: %S\n" s1;
if !log_k then log prune (s1^s2);
recomm tl @@ add hd @@ st
- | ET.Title ss :: tl ->
+ | ET.Title ss :: tl ->
if middle st then Printf.eprintf "middle: TITLE\n";
let r, ss1, ss2 = !c_line k_final ET.OO [] ss in
let ss2 =
let s = String.concat " " ss in
if !log_t then log blue s;
recomm tl @@ add (ET.Title ss) @@ st
- | ET.Slice ss :: tl ->
+ | ET.Slice ss :: tl ->
if middle st then Printf.eprintf "middle: Section\n";
let r, ss1, ss2 = !s_line k_final ET.OO [] ss in
let ss2 =
let s = String.capitalize_ascii (String.concat " " ss) in
if !log_s then log sky s;
recomm tl @@ add (ET.Slice ss) @@ st
- | ET.Other (_, s, _) as hd :: tl ->
+ | ET.Other (_, _, s, _) as hd :: tl ->
if !log_o && not (Array.mem s mute_o) then log black s;
recomm tl @@ add hd @@ st
--- /dev/null
+let split_on_char c s =
+ List.filter ((<>) "") (String.split_on_char c s)
--- /dev/null
+val split_on_char: char -> string -> string list
+module EL = RecommLib
module ET = RecommTypes
let width = ref 78
end
let out_src och = function
- | ET.Line s ->
+ | ET.Line s ->
Printf.fprintf och "%s" s
- | ET.Text s ->
+ | ET.Text s ->
Printf.fprintf och "%s" s
- | ET.Mark s ->
+ | ET.Mark s ->
Printf.fprintf och "(* *%s*)" s
- | ET.Key (s1, s2) ->
+ | ET.Key (s1, s2) ->
let s3 =
if s1 = "NOTE" then complete (s1^s2) 0 else ""
in
Printf.fprintf och "(* %s%s%s*)" s1 s2 s3
- | ET.Title ss ->
+ | ET.Title ss ->
let s = String.concat " " ss in
Printf.fprintf och "(* %s %s*)" s (complete s 1)
- | ET.Slice ss ->
+ | ET.Slice ss ->
let s = String.capitalize_ascii (String.concat " " ss) in
Printf.fprintf och "(* %s %s*)" s (complete s 1)
- | ET.Other (s1, s2, s3) ->
+ | ET.Other (_, s1, s2, s3) ->
Printf.fprintf och "%s%s%s" s1 s2 s3
let write_srcs file srcs =
let och = open_out target in
List.iter (out_src och) srcs;
close_out och
+
+let write_subst och n s =
+ Printf.fprintf och "%s %s\n" s n
+
+let rec write_fst och = function
+ | [] -> ()
+ | ET.Other (2, _, s, _) :: ET.Line _ :: ET.Text t :: tl ->
+ write_snd och tl s (EL.split_on_char ' ' t)
+ | ET.Other (2, _, s, _) :: tl ->
+ Printf.eprintf "skipping fst: %S\n" s;
+ write_fst och tl
+ | _ :: tl -> write_fst och tl
+
+and write_snd och tl s = function
+ | "definition" :: n :: _
+ | "fact" :: n :: _
+ | "lemma" :: n :: _
+ | "inductive" :: n :: _
+ | "theorem" :: n :: _ ->
+ let ss = EL.split_on_char ' ' s in
+ List.iter (write_subst och n) (List.tl ss);
+ write_fst och tl
+ | t :: _ ->
+ Printf.eprintf "skipping snd: %S %S\n" s t;
+ write_fst och tl
+ | [] ->
+ Printf.eprintf "skipping snd: %S\n" s;
+ write_fst och tl
+
+let write_substs = write_fst
val replace: bool ref
val write_srcs: string -> RecommTypes.srcs -> unit
+
+val write_substs: out_channel -> RecommTypes.srcs -> unit
| SP sw sws { $2 :: $3 }
src_l:
- | NL { ET.Line $1 }
- | OP sp PP inns CP { ET.Mark $4 }
- | OP sp KW inns CP { ET.Key ($3, $4) }
- | OP sp CW cws CP { ET.Title ($3 :: $4) }
- | OP sp HW sws CP { ET.Slice (lc $3 :: $4) }
- | OP sp CP { ET.Other ($1, $2, $3) }
- | OP sp inns_r CP { ET.Other ($1, $2 ^ $3, $4) }
- | OP SR inns CP { ET.Other ($1, $2 ^ $3, $4) }
- | OP SR SR inns CP { ET.Other ($1, $2 ^ $3 ^ $4, $5) }
- | OP SP SR inns CP { ET.Mark $4 }
+ | NL { ET.Line $1 }
+ | OP sp PP inns CP { ET.Mark $4 }
+ | OP sp KW inns CP { ET.Key ($3, $4) }
+ | OP sp CW cws CP { ET.Title ($3 :: $4) }
+ | OP sp HW sws CP { ET.Slice (lc $3 :: $4) }
+ | OP sp CP { ET.Other (0, $1, $2, $3) }
+ | OP sp inns_r CP { ET.Other (0, $1, $2 ^ $3, $4) }
+ | OP SR inns CP { ET.Other (1, $1, $2 ^ $3, $4) }
+ | OP SR SR inns CP { ET.Other (2, $1, $2 ^ $3 ^ $4, $5) }
+ | OP SP SR inns CP { ET.Mark $4 }
src:
| outs { ET.Text $1 }
(* section *)
| Slice of words
(* other comment *)
- | Other of text * text * text
+ | Other of int * text * text * text
type srcs = src list
(* Decidability of predicates ***********************************************)
-lemma dec_lt (R:predicate nat):
- (∀n. Decidable … (R n)) →
- ∀n. Decidable … (∃∃m. m < n & R m).
-#R #HR #n elim n -n [| #n * ]
-[ @or_intror * /2 width=2 by lt_zero_false/
-| * /4 width=3 by lt_S, or_introl, ex2_intro/
-| #H0 elim (HR n) -HR
- [ /3 width=3 by or_introl, ex2_intro/
- | #Hn @or_intror * #m #Hmn #Hm
- elim (le_to_or_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
- /4 width=3 by lt_S_S_to_lt, ex2_intro/
- ]
-]
-qed-.
-
lemma dec_min (R:predicate nat):
(∀n. Decidable … (R n)) → ∀n. R n →
∃∃m. m ≤ n & R m & (∀p. p < m → R p → ⊥).
(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
(*** le *)
-(*** le_ind *)
inductive nle (m:nat): predicate nat ≝
| nle_refl : nle m m
| nle_succ_dx: ∀n. nle m n → nle m (↑n)
lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥.
#m @(nat_ind_succ … m) -m [| #m #IH ] #H
-[ /3 width=2 by nle_inv_zero_dx, eq_inv_zero_nsucc/
+[ /2 width=2 by nle_inv_succ_zero/
| /3 width=1 by nle_inv_succ_bi/
]
qed-.
(∀m,n. m ≤ n → Q m n → Q (↑m) (↑n)) →
∀m,n. m ≤ n → Q m n.
#Q #IH1 #IH2 #m #n @(nat_ind_2_succ … m n) -m -n //
-[ #m #H elim (nle_inv_succ_zero … H)
+[ #m #_ #H elim (nle_inv_succ_zero … H)
| /4 width=1 by nle_inv_succ_bi/
]
qed-.
/2 width=1 by nle_plus_bi_sn/ qed.
(*** le_plus_a *)
-lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
+lemma nle_plus_dx_sn (o) (m) (n): n ≤ m → n ≤ o + m.
+/2 width=3 by nle_trans/ qed.
+
+(*** le_plus_b *)
+lemma nle_plus_dx_dx (o) (m) (n): n ≤ m → n ≤ m + o.
/2 width=3 by nle_trans/ qed.
(* Main constructions with nplus ********************************************)
| /4 width=1 by nlt_inv_succ_bi/
]
qed-.
+
+(* Advanced constructions (decidability) ************************************)
+
+(*** dec_lt *)
+lemma dec_nlt (R:predicate nat):
+ (∀n. Decidable … (R n)) →
+ ∀n. Decidable … (∃∃m. m < n & R m).
+#R #HR #n @(nat_ind_succ … n) -n [| #n * ]
+[ @or_intror * /2 width=2 by nlt_inv_zero_dx/
+| * /4 width=3 by nlt_succ_dx_trans, ex2_intro, or_introl/
+| #H0 elim (HR n) -HR
+ [ /3 width=3 by or_introl, ex2_intro/
+ | #Hn @or_intror * #m #Hmn #Hm
+ elim (nle_split_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
+ [ /4 width=3 by nlt_inv_succ_bi, ex2_intro/
+ | lapply (eq_inv_nsucc_bi … H) -H /2 width=1 by/
+ ]
+]
+qed-.
@nlt_i >nplus_succ_dx /2 width=1 by nle_plus_bi_sn/
qed.
+lemma nlt_plus_dx_dx (o) (m) (n): m < n → m < n + o.
+/2 width=1 by nle_plus_dx_dx/ qed.
+
+lemma nlt_plus_dx_sn (o) (m) (n) : m < n → m < o + n.
+/2 width=1 by nle_plus_dx_sn/ qed.
+
lemma nlt_succ_plus_dx_refl_sn (m) (n): m < ↑(m + n).
/2 width=1/ qed.
#n #IH <nplus_succ_dx <nminus_succ_bi //
qed.
-(*** minus_plus_m_m *)
+(*** minus_plus_m_m_commutative *)
lemma nminus_plus_sn_refl_dx (m) (n): m = n + m - n.
#m #n <nplus_comm //
qed.
| ∧∧ 𝟎 = n & 𝟎 = o.
#m #n @(nat_ind_2_succ … m n) -m -n
[ /3 width=1 by or_introl, conj/
-| #m #o #Ho
+| #m #_ #o #Ho
lapply (eq_inv_nplus_bi_sn … (𝟎) Ho) -Ho
/3 width=1 by or_intror, conj/
| #m #n #IH #o
--- /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/arith/nat_rplus_succ.ma".
+include "ground/arith/nat_plus.ma".
+
+(* ADDITION FOR NON-NEGATIVE INTEGERS ***************************************)
+
+(* Constructions with rplus *************************************************)
+
+lemma nrplus_inj_sn (p) (n):
+ ninj (p + n) = ninj p + n.
+#p #n @(nat_ind_succ … n) -n //
+#n #IH <nplus_succ_dx <IH //
+qed.
+
+(* Constructions with rplus and npsucc **************************************)
+
+lemma nrplus_npsucc_sn (m) (n):
+ npsucc (m + n) = npsucc m + n.
+#m @(nat_ind_succ … m) -m //
+#m #IH #n <npsucc_succ <nrplus_succ_sn //
+qed.
(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
+definition pnpred (p): nat ≝
+ psplit … (𝟎) ninj p.
+
+interpretation
+ "positive predecessor (non-negative integers)"
+ 'DownArrow p = (pnpred p).
+
(*** pred *)
definition npred (m): nat ≝ match m with
[ nzero ⇒ 𝟎
-| ninj p ⇒ psplit … (𝟎) ninj p
+| ninj p ⇒ ↓p
].
interpretation
lemma npred_zero: 𝟎 = ↓𝟎.
// qed.
+lemma npred_inj (p): ↓p = ↓(ninj p).
+// qed.
+
lemma npred_one: 𝟎 = ↓𝟏.
// qed.
(* PREDECESSOR FOR NON-NEGATIVE INTEGERS ************************************)
+(* Constructions with npsucc ************************************************)
+
+lemma pnpred_succ (n): n = pnpred (npsucc n).
+* //
+qed.
+
+lemma npsucc_pred (p): p = npsucc (pnpred p).
+* //
+qed.
+
+(* Constructions with nsucc and psucc ***************************************)
+
+lemma pnpred_psucc (p): pnpred (psucc p) = nsucc (pnpred p).
+* // qed.
+
(* Constructions with nsucc *************************************************)
(*** pred_Sn pred_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 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_iter.ma".
+
+(* RIGHT ADDITION FOR NON-NEGATIVE INTEGERS *********************************)
+
+definition nrplus: pnat → nat → pnat ≝
+ λp,n. psucc^n p.
+
+interpretation
+ "right plus (non-negative integers)"
+ 'plus p n = (nrplus p n).
+
+(* Basic constructions ******************************************************)
+
+lemma nrplus_zero_dx (p): p = p + 𝟎.
+// qed.
+
+lemma nrplus_unit_dx (p): ↑p = p + 𝟏.
+// qed.
+
+lemma nrplus_succ_sn (p) (n): ↑(p+n) = ↑p + n.
+#p #n @(niter_appl … psucc)
+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/arith/nat_succ_iter.ma".
+include "ground/arith/nat_rplus.ma".
+
+(* RIGHT ADDITION FOR NON-NEGATIVE INTEGERS *********************************)
+
+(* Constructions with nsucc *************************************************)
+
+lemma nrplus_succ_dx (p) (n): ↑(p+n) = p + ↑n.
+#p #n @(niter_succ … psucc)
+qed.
+
+lemma nrplus_succ_shift (p) (n): ↑p + n = p + ↑n.
+// qed.
+
+lemma nrplus_unit_sn (n): ↑n = 𝟏 + n.
+#n @(nat_ind_succ … n) -n //
+qed.
+
+(* Advanced constructions ***************************************************)
+
+lemma nrplus_comm_23 (p) (n1) (n2):
+ p + n1 + n2 = p + n2 + n1.
+#p #n1 @(nat_ind_succ … n1) -n1 //
+qed.
(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
-definition nsucc_pos (m): pnat ≝
+definition npsucc (m): pnat ≝
match m with
[ nzero ⇒ 𝟏
| ninj p ⇒ ↑p
interpretation
"positive successor (non-negative integers)"
- 'UpArrow m = (nsucc_pos m).
+ 'UpArrow m = (npsucc m).
definition nsucc (m): nat ≝
ninj (↑m).
(* Basic constructions ******************************************************)
+lemma npsucc_zero: (𝟏) = ↑𝟎.
+// qed.
+
+lemma npsucc_inj (p): (↑p) = ↑(ninj p).
+// qed.
+
lemma nsucc_zero: ninj (𝟏) = ↑𝟎.
// qed.
lemma nsucc_inj (p): ninj (↑p) = ↑(ninj p).
// qed.
+lemma npsucc_succ (n): psucc (npsucc n) = npsucc (nsucc n).
+// qed.
+
(* Basic eliminations *******************************************************)
(*** nat_ind *)
(*** nat_elim2 *)
lemma nat_ind_2_succ (Q:relation2 …):
(∀n. Q (𝟎) n) →
- (∀m. Q (↑m) (𝟎)) →
+ (∀m. Q m (𝟎) → Q (↑m) (𝟎)) →
(∀m,n. Q m n → Q (↑m) (↑n)) →
∀m,n. Q m n.
#Q #IH1 #IH2 #IH3 #m @(nat_ind_succ … m) -m [ // ]
(* Basic inversions *********************************************************)
-(*** injective_S *)
-lemma eq_inv_nsucc_bi: injective … nsucc.
+lemma eq_inv_npsucc_bi: injective … npsucc.
* [| #p1 ] * [2,4: #p2 ]
-[1,4: <nsucc_zero <nsucc_inj #H destruct
-| <nsucc_inj <nsucc_inj #H destruct //
+[ 1,4: <npsucc_zero <npsucc_inj #H destruct
+| <npsucc_inj <npsucc_inj #H destruct //
| //
]
qed-.
+(*** injective_S *)
+lemma eq_inv_nsucc_bi: injective … nsucc.
+#n1 #n2 #H
+@eq_inv_npsucc_bi @eq_inv_ninj_bi @H
+qed-.
+
lemma eq_inv_nsucc_zero (m): ↑m = 𝟎 → ⊥.
* [ <nsucc_zero | #p <nsucc_inj ] #H destruct
qed-.
| /2 width=1 by or_introl/
]
qed-.
+
+(* Basic eliminations *******************************************************)
+
+lemma pnat_ind_2 (Q:relation2 …):
+ (∀q. Q (𝟏) q) →
+ (∀p. Q p (𝟏) → Q (↑p) (𝟏)) →
+ (∀p,q. Q p q → Q (↑p) (↑q)) →
+ ∀p,q. Q p q.
+#Q #IH1 #IH2 #IH3 #p elim p -p [ // ]
+#p #IH #q elim q -q /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 "ground/generated/insert_eq_1.ma".
+include "ground/arith/pnat.ma".
+
+(* ORDER FOR POSITIVE INTEGERS **********************************************)
+
+inductive ple (p:pnat): predicate pnat ≝
+| ple_refl : ple p p
+| ple_succ_dx: ∀q. ple p q → ple p (↑q)
+.
+
+interpretation
+ "less equal (positive integers)"
+ 'leq p q = (ple p q).
+
+(* Basic constructions ******************************************************)
+
+lemma ple_succ_dx_refl (p): p ≤ ↑p.
+/2 width=1 by ple_refl, ple_succ_dx/ qed.
+
+lemma ple_unit_sx (p): 𝟏 ≤ p.
+#p elim p -p /2 width=1 by ple_succ_dx/
+qed.
+
+lemma ple_succ_bi (p) (q): p ≤ q → ↑p ≤ ↑q.
+#p #q #H elim H -q /2 width=1 by ple_refl, ple_succ_dx/
+qed.
+
+lemma pnat_split_le_ge (p) (q): ∨∨ p ≤ q | q ≤ p.
+#p #q @(pnat_ind_2 … p q) -p -q
+[ /2 width=1 by or_introl/
+| /2 width=1 by or_intror/
+| #p #q * /3 width=2 by ple_succ_bi, or_introl, or_intror/
+]
+qed-.
+
+(* Basic destructions *******************************************************)
+
+lemma ple_des_succ_sn (p) (q): ↑p ≤ q → p ≤ q.
+#p #q #H elim H -q /2 width=1 by ple_succ_dx/
+qed-.
+
+(* Basic inversions *********************************************************)
+
+lemma ple_inv_succ_bi (p) (q): ↑p ≤ ↑q → p ≤ q.
+#p #q @(insert_eq_1 … (↑q))
+#x * -x
+[ #H destruct //
+| #o #Ho #H destruct
+ /2 width=1 by ple_des_succ_sn/
+]
+qed-.
+
+lemma ple_inv_unit_dx (p): p ≤ 𝟏 → 𝟏 = p.
+#p @(insert_eq_1 … (𝟏))
+#y * -y
+[ #H destruct //
+| #y #_ #H destruct
+]
+qed-.
+
+(* Advanced inversions ******************************************************)
+
+lemma ple_inv_succ_unit (p): ↑p ≤ 𝟏 → ⊥.
+#p #H
+lapply (ple_inv_unit_dx … H) -H #H destruct
+qed-.
+
+lemma ple_inv_succ_sn_refl (p): ↑p ≤ p → ⊥.
+#p elim p -p [| #p #IH ] #H
+[ /2 width=2 by ple_inv_succ_unit/
+| /3 width=1 by ple_inv_succ_bi/
+]
+qed-.
+
+theorem ple_antisym (p) (q): p ≤ q → q ≤ p → p = q.
+#p #q #H elim H -q //
+#q #_ #IH #Hq
+lapply (ple_des_succ_sn … Hq) #H
+lapply (IH H) -IH -H #H destruct
+elim (ple_inv_succ_sn_refl … Hq)
+qed-.
+
+(* Advanced eliminations ****************************************************)
+
+lemma ple_ind_alt (Q: relation2 pnat pnat):
+ (∀q. Q (𝟏) (q)) →
+ (∀p,q. p ≤ q → Q p q → Q (↑p) (↑q)) →
+ ∀p,q. p ≤ q → Q p q.
+#Q #IH1 #IH2 #p #q @(pnat_ind_2 … p q) -p -q //
+[ #p #_ #H elim (ple_inv_succ_unit … H)
+| /4 width=1 by ple_inv_succ_bi/
+]
+qed-.
+
+(* Advanced constructions ***************************************************)
+
+theorem ple_trans: Transitive … ple.
+#p #q #H elim H -q /3 width=1 by ple_des_succ_sn/
+qed-.
+
+lemma ple_dec (p) (q): Decidable … (p ≤ q).
+#p #q elim (pnat_split_le_ge p q) [ /2 width=1 by or_introl/ ]
+#Hqp elim (eq_pnat_dec p q) [ #H destruct /2 width=1 by ple_refl, or_introl/ ]
+/4 width=1 by ple_antisym, or_intror/
+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/arith/pnat_plus.ma".
+include "ground/arith/pnat_le.ma".
+
+(* ORDER FOR POSITIVE INTEGERS **********************************************)
+
+(* Constructions with pplus *************************************************)
+
+lemma ple_plus_bi_dx (p) (q1) (q2): q1 ≤ q2 → q1 + p ≤ q2 + p.
+#p #q1 #q2 #H elim H -q2 /2 width=3 by ple_trans/
+qed.
+
+lemma ple_plus_bi_sn (p) (q1) (q2): q1 ≤ q2 → p + q1 ≤ p + q2.
+#p #q1 #q2 #H <pplus_comm <pplus_comm in ⊢ (??%);
+/2 width=1 by ple_plus_bi_dx/
+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/arith/pnat_pred.ma".
+include "ground/arith/pnat_le.ma".
+
+(* ORDER FOR POSITIVE INTEGERS **********************************************)
+
+(* Destructions with ppred **************************************************)
+
+lemma ple_inv_pred_sn (p) (q): ↓p ≤ q → p ≤ ↑q.
+#p #q elim p -p
+/2 width=1 by ple_succ_bi/
+qed-.
+
+(* Constructions with ppred *************************************************)
+
+lemma ple_succ_pred_dx_refl (p): p ≤ ↑↓p.
+#p @ple_inv_pred_sn // qed.
+
+lemma ple_pred_sn_refl (p): ↓p ≤ p.
+#p elim p -p //
+qed.
+
+lemma ple_pred_bi (p) (q): p ≤ q → ↓p ≤ ↓q.
+#p #q #H elim H -q //
+/2 width=3 by ple_trans/
+qed.
+
+lemma ple_pred_sn (p) (q): p ≤ ↑q → ↓p ≤ q.
+#p #q elim p -p //
+/2 width=1 by ple_pred_bi/
+qed-.
+
+(* Inversions with ppred ****************************************************)
+
+lemma ple_inv_succ_sn (p) (q):
+ ↑p ≤ q → ∧∧ p ≤ ↓q & q = ↑↓q.
+#p #q * -q
+[ /2 width=3 by ple_refl, conj/
+| #q #Hq /3 width=1 by ple_des_succ_sn, 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 "ground/xoa/or_3.ma".
+include "ground/arith/pnat_le.ma".
+
+(* STRICT ORDER FOR POSITIVE INTEGERS ***************************************)
+
+definition plt: relation2 pnat pnat ≝
+ λp,q. ↑p ≤ q.
+
+interpretation
+ "less (positive integers)"
+ 'lt p q = (plt p q).
+
+(* Basic constructions ******************************************************)
+
+lemma plt_i (p) (q): ↑p ≤ q → p < q.
+// qed.
+
+lemma plt_refl_succ (q): q < ↑q.
+// qed.
+
+lemma plt_succ_dx (p) (q): p ≤ q → p < ↑q.
+/2 width=1 by ple_succ_bi/ qed.
+
+lemma plt_succ_dx_trans (p) (q): p < q → p < ↑q.
+/2 width=1 by ple_succ_dx/ qed.
+
+lemma plt_unit_succ (p): 𝟏 < ↑p.
+/2 width=1 by ple_succ_bi/ qed.
+
+lemma plt_succ_bi (p) (q): p < q → ↑p < ↑q.
+/2 width=1 by ple_succ_bi/ qed.
+
+lemma ple_split_lt_eq (p) (q): p ≤ q → ∨∨ p < q | p = q.
+#p #q * -q /3 width=1 by ple_succ_bi, or_introl/
+qed-.
+
+lemma pnat_split_unit_gt (q): ∨∨ 𝟏 = q | 𝟏 < q.
+#q elim (ple_split_lt_eq (𝟏) q ?)
+/2 width=1 by or_introl, or_intror/
+qed-.
+
+lemma pnat_split_lt_ge (p) (q): ∨∨ p < q | q ≤ p.
+#p #q elim (pnat_split_le_ge p q) /2 width=1 by or_intror/
+#H elim (ple_split_lt_eq … H) -H /2 width=1 by ple_refl, or_introl, or_intror/
+qed-.
+
+lemma pnat_split_lt_eq_gt (p) (q): ∨∨ p < q | q = p | q < p.
+#p #q elim (pnat_split_lt_ge p q) /2 width=1 by or3_intro0/
+#H elim (ple_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
+qed-.
+
+lemma le_false_plt (p) (q): (q ≤ p → ⊥) → p < q.
+#p #q elim (pnat_split_lt_ge p q) [ // ]
+#H #Hq elim Hq -Hq //
+qed.
+
+lemma plt_ple_trans (r) (p) (q): p < r → r ≤ q → p < q.
+/2 width=3 by ple_trans/ qed-.
+
+lemma ple_plt_trans (r) (p) (q): p ≤ r → r < q → p < q.
+/3 width=3 by ple_succ_bi, ple_trans/ qed-.
+
+(* Basic inversions *********************************************************)
+
+lemma plt_inv_succ_dx (p) (q): p < ↑q → p ≤ q.
+/2 width=1 by ple_inv_succ_bi/ qed-.
+
+lemma plt_inv_succ_bi (p) (q): ↑p < ↑q → p < q.
+/2 width=1 by ple_inv_succ_bi/ qed-.
+
+lemma plt_ge_false (p) (q): p < q → q ≤ p → ⊥.
+/3 width=4 by ple_inv_succ_sn_refl, plt_ple_trans/ qed-.
+
+lemma plt_inv_refl (p): p < p → ⊥.
+/2 width=4 by plt_ge_false/ qed-.
+
+lemma plt_inv_unit_dx (p): p < 𝟏 → ⊥.
+/2 width=4 by plt_ge_false/ qed-.
+
+(* Basic destructions *******************************************************)
+
+lemma plt_des_le (p) (q): p < q → p ≤ q.
+/2 width=3 by ple_trans/ qed-.
+
+lemma plt_des_lt_unit_sn (p) (q): p < q → 𝟏 < q.
+/3 width=3 by ple_plt_trans/ qed-.
+
+(* Main constructions *******************************************************)
+
+theorem plt_trans: Transitive … plt.
+/3 width=3 by plt_des_le, plt_ple_trans/ qed-.
+
+(* Advanced eliminations ****************************************************)
+
+lemma pnat_ind_lt_le (Q:predicate …):
+ (∀q. (∀p. p < q → Q p) → Q q) → ∀q,p. p ≤ q → Q p.
+#Q #H1 #q elim q -q
+[ #p #H <(ple_inv_unit_dx … H) -p
+ @H1 -H1 #r #H elim (plt_inv_unit_dx … H)
+| /5 width=3 by plt_ple_trans, ple_inv_succ_bi/
+]
+qed-.
+
+lemma pnat_ind_lt (Q:predicate …):
+ (∀q. (∀p. p < q → Q p) → Q q) → ∀q. Q q.
+/4 width=2 by pnat_ind_lt_le/ qed-.
+
+lemma plt_ind_alt (Q: relation2 pnat pnat):
+ (∀q. Q (𝟏) (↑q)) →
+ (∀p,q. p < q → Q p q → Q (↑p) (↑q)) →
+ ∀p,q. p < q → Q p q.
+#Q #IH1 #IH2 #p #q @(pnat_ind_2 … q p) -p -q //
+[ #p #H
+ elim (plt_inv_unit_dx … H)
+| /4 width=1 by plt_inv_succ_bi/
+]
+qed-.
+
+(* Advanced constructions (decidability) ************************************)
+
+lemma dec_plt (R:predicate pnat):
+ (∀q. Decidable … (R q)) →
+ ∀q. Decidable … (∃∃p. p < q & R p).
+#R #HR #q elim q -q [| #q * ]
+[ @or_intror * /2 width=2 by plt_inv_unit_dx/
+| * /4 width=3 by plt_succ_dx_trans, ex2_intro, or_introl/
+| #H0 elim (HR q) -HR
+ [ /3 width=3 by or_introl, ex2_intro/
+ | #Hq @or_intror * #p #Hpq #Hp
+ elim (ple_split_lt_eq … Hpq) -Hpq #H destruct [ -Hq | -H0 ]
+ /4 width=3 by plt_inv_succ_bi, 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/arith/pnat_le_pred.ma".
+include "ground/arith/pnat_lt.ma".
+
+(* STRICT ORDER FOR POSITIVE INTEGERS ***************************************)
+
+(* Destructions with ppred **************************************************)
+
+lemma plt_des_gen (p) (q): p < q → q = ↑↓q.
+#p #q elim q -q //
+#H elim (plt_inv_unit_dx … H)
+qed-.
+
+(* Inversions with ppred ****************************************************)
+
+lemma plt_inv_gen (p) (q): p < q → ∧∧ p ≤ ↓q & q = ↑↓q.
+/2 width=1 by ple_inv_succ_sn/ qed-.
+
+lemma plt_inv_succ_sn (p) (q): ↑p < q → ∧∧ p < ↓q & q = ↑↓q.
+/2 width=1 by ple_inv_succ_sn/ qed-.
+
+lemma plt_inv_pred_dx (p) (q): p < ↓q → ↑p < q.
+#p #q #H >(plt_des_gen (𝟏) q)
+[ /2 width=1 by plt_succ_bi/
+| /3 width=3 by ple_plt_trans, plt_ple_trans/
+]
+qed-.
+
+lemma plt_inv_pred_bi (p) (q):
+ ↓p < ↓q → p < q.
+/3 width=3 by plt_inv_pred_dx, ple_plt_trans/
+qed-.
+
+(* Constructions with ppred *************************************************)
+
+lemma plt_unit_sn (q): q = ↑↓q → 𝟏 < q.
+// qed.
+
+lemma plt_pred_bi (p) (q): 𝟏 < p → p < q → ↓p < ↓q.
+#p #q #Hp #Hpq
+@ple_inv_succ_bi
+<(plt_des_gen … Hp) -Hp
+<(plt_des_gen … Hpq) //
+qed.
#p #q #r elim r -r //
#r #IH <pplus_succ_dx <pplus_succ_dx <IH -IH //
qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_unit_pplus (p) (q): 𝟏 = p + q → ⊥.
+#p #q elim q -q
+[ <pplus_one_dx #H destruct
+| #q #_ <pplus_succ_dx #H destruct
+]
+qed-.
+
+lemma eq_inv_pplus_unit (p) (q):
+ p + q = 𝟏 → ⊥.
+/2 width=3 by eq_inv_unit_pplus/ qed-.
+
+lemma eq_inv_pplus_bi_dx (r) (p) (q): p + r = q + r → p = q.
+#r elim r -r /3 width=1 by eq_inv_psucc_bi/
+qed-.
+
+lemma eq_inv_pplus_bi_sn (r) (p) (q): r + p = r + q → p = q.
+#r #p #q <pplus_comm <pplus_comm in ⊢ (???%→?);
+/2 width=2 by eq_inv_pplus_bi_dx/
+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/notation/functions/downarrow_1.ma".
+include "ground/arith/pnat_split.ma".
+
+(* PREDECESSOR FOR POSITIVE INTEGERS ****************************************)
+
+definition ppred (p): pnat ≝ psplit … (𝟏) (λp.p) p.
+
+interpretation
+ "predecessor (positive integers)"
+ 'DownArrow p = (ppred p).
+
+(* Basic constructions ******************************************************)
+
+lemma ppred_unit: 𝟏 = ↓𝟏.
+// qed.
+
+lemma ppred_succ (p): p = ↓↑p.
+// qed.
+
+(* Basic inversions *********************************************************)
+
+lemma ppred_inv_refl (p): p = ↓p → 𝟏 = p.
+#p elim p -p //
+#p #IH #H /2 width=1 by/
+qed-.
+
+lemma pnat_split_unit_pos (p): ∨∨ 𝟏 = p | p = ↑↓p.
+#p elim p -p
+/2 width=1 by or_introl, or_intror/
+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 *)
+(* *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( @↑❪ term 46 T1 , break term 46 f ❫ ≘ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RAtSucc $T1 $f $T2 }.
include "ground/notation/functions/diamond_0.ma".
include "ground/notation/functions/semicolon_3.ma".
-include "ground/lib/arith.ma".
+include "ground/arith/nat.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
(**************************************************************************)
include "ground/notation/relations/rat_3.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_lt.ma".
include "ground/relocation/mr2.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
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)
+elim (nlt_ge_false … Hi1l Hli1)
qed-.
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
-elim (lt_le_false … Hi1l Hli1)
+elim (nlt_ge_false … Hi1l Hli1)
qed-.
(* Main properties **********************************************************)
(* *)
(**************************************************************************)
+include "ground/xoa/ex_3_1.ma".
include "ground/notation/relations/rminus_3.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_minus.ma".
+include "ground/arith/nat_lt.ma".
include "ground/relocation/mr2.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
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)
+elim (nlt_ge_false … Hil Hli)
qed-.
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.
#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)
+#Hli #_ #Hil elim (nlt_ge_false … Hil Hli)
qed-.
(* *)
(**************************************************************************)
+include "ground/arith/nat_minus_plus.ma".
include "ground/relocation/mr2.ma".
(* 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) + 𝟏) = ❨↑l,m❩;cs + 𝟏.
normalize // qed.
(* Basic inversion lemmas ***************************************************)
#i #l #m #cs2 *
[ normalize #H destruct
| #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct
- <minus_plus_m_m /2 width=3 by ex2_intro/
+ <nminus_plus_sn_refl_sn /2 width=3 by 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/notation/functions/upspoon_1.ma".
-include "ground/lib/stream_tls.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-definition rtmap: Type[0] ≝ stream nat.
-
-definition push: rtmap → rtmap ≝ λf. 0⨮f.
-
-interpretation "push (nstream)" 'UpSpoon f = (push f).
-
-definition next: rtmap → rtmap.
-* #n #f @(↑n⨮f)
-defined.
-
-interpretation "next (nstream)" 'UpArrow f = (next f).
-
-(* Basic properties *********************************************************)
-
-lemma push_rew: ∀f. 0⨮f = ⫯f.
-// qed.
-
-lemma next_rew: ∀f,n. (↑n)⨮f = ↑(n⨮f).
-// qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma injective_push: injective ? ? push.
-#f1 #f2 normalize #H destruct //
-qed-.
-
-lemma discr_push_next: ∀f1,f2. ⫯f1 = ↑f2 → ⊥.
-#f1 * #n2 #f2 normalize #H destruct
-qed-.
-
-lemma discr_next_push: ∀f1,f2. ↑f1 = ⫯f2 → ⊥.
-* #n1 #f1 #f2 normalize #H destruct
-qed-.
-
-lemma injective_next: injective ? ? next.
-* #n1 #f1 * #n2 #f2 normalize #H destruct //
-qed-.
-
-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.
-#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.
-* #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.
-* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma case_prop: ∀R:predicate rtmap.
- (∀f. R (⫯f)) → (∀f. R (↑f)) → ∀f. R f.
-#R #H1 #H2 * * //
-qed-.
-
-lemma case_type0: ∀R:rtmap→Type[0].
- (∀f. R (⫯f)) → (∀f. R (↑f)) → ∀f. R f.
-#R #H1 #H2 * * //
-qed-.
-
-lemma iota_push: ∀R,a,b,f. a f = case_type0 R a b (⫯f).
-// qed.
-
-lemma iota_next: ∀R,a,b,f. b f = case_type0 R a b (↑f).
-#R #a #b * //
-qed.
-
-(* Poperties with stream_tl *************************************************)
-
-lemma tl_push: ∀f. f = ⫰⫯f.
-// qed.
-
-lemma tl_next: ∀f. ⫰f = ⫰↑f.
-* // 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/relocation/nstream_istot.ma".
-include "ground/relocation/rtmap_after.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-corec definition compose: rtmap → rtmap → rtmap.
-#f2 * #n1 #f1 @(seq … (f2@❨n1❩)) @(compose ? f1) -compose -f1
-@(⫰*[↑n1] f2)
-defined.
-
-interpretation "functional composition (nstream)"
- 'compose f2 f1 = (compose f2 f1).
-
-(* 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 //
-qed.
-
-lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
-#f2 * #n1 #f1 #f <compose_rew <compose_rew
-* -f <tls_S1 /2 width=1 by eq_f2/
-qed.
-
-(* Basic inversion lemmas on compose ****************************************)
-
-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
-#H destruct /2 width=1 by conj/
-qed-.
-
-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.
-#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.
-#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.
-#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.
-#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.
-#n1 elim n1 -n1
-[ * /2 width=1 by after_O2/
-| #n1 #IH * /3 width=1 by after_S2/
-]
-qed-.
-
-corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
-* #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
-[ cases n1 -n1
- [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
- | #n1 #H cases (compose_inv_S2 … H) -H * -n /3 width=7 by after_push/
- ]
-| #n2 >next_rew #H cases (compose_inv_S1 … H) -H * -n /3 width=5 by after_next/
-]
-qed-.
-
-theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
-/2 width=1 by after_total_aux/ qed.
-
-(* Specific inversion lemmas on after ***************************************)
-
-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: // ]
- #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
-| #n2 #IH #n #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
- #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
- #x #Hx #H destruct elim (IH … Hg) [2,3: // ] -IH -Hg
- #H destruct /2 width=1 by conj/
-]
-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.
-#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
- #x #Hx #Hg destruct /2 width=3 by ex2_intro/
-| #n2 #IH #n #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [2,3: // ]
- #g #Hg #H elim (next_inv_seq_dx … H) -H
- #x #Hx #H destruct elim (IH … Hg) -IH -Hg [2,3: // ]
- #m #Hf #Hm destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-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/
-| #n #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/
-]
-qed-.
-
-lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
-/2 width=4 by after_mono/ qed-.
-
-(* Specific forward lemmas on after *****************************************)
-
-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 →
- (⫰*[n1]f2) ⊚ f1 ≘ f.
-#f #f1 #n1 elim n1 -n1
-[ #f2 #n2 #n #H elim (after_inv_xpx … H) -H //
-| #n1 #IH * #m1 #f2 #n2 #n #H elim (after_inv_xnx … H) -H [2,3: // ]
- #m #Hm #H destruct /2 width=3 by/
-]
-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.
-/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
-
-(* Properties on apply ******************************************************)
-
-lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
-/4 width=6 by after_fwd_at, at_inv_total, sym_eq/ 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/relocation/rtmap_basic.ma".
-include "ground/relocation/nstream_after.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-(* Specific properties on basic relocation **********************************)
-
-lemma apply_basic_lt: ∀m,n,i. i < m → 𝐁❨m,n❩@❨i❩ = i.
-/3 width=1 by at_inv_total, at_basic_lt/ qed-.
-
-lemma apply_basic_ge: ∀m,n,i. m ≤ i → 𝐁❨m,n❩@❨i❩ = n+i.
-/3 width=1 by at_inv_total, at_basic_ge/ qed-.
-
-(* Specific main properties on basic relocation *****************************)
-
-theorem basic_swap: ∀d1,d2. d2 ≤ d1 →
- ∀h1,h2. 𝐁❨d2,h2❩∘𝐁❨d1,h1❩ ≡ 𝐁❨h2+d1,h1❩∘𝐁❨d2,h2❩.
-#d1 #d2 #Hd21 #h1 #h2
-@nstream_inv_eq
-@nstream_eq_inv_ext #i
-<compose_apply <compose_apply
-elim (lt_or_ge i d2) #Hd2
-[ lapply (lt_to_le_to_lt … Hd2 Hd21) -Hd21 #Hd1
- >(apply_basic_lt … Hd1) >(apply_basic_lt … Hd2) >apply_basic_lt
- /2 width=1 by le_plus_a/
-| elim (lt_or_ge i d1) -Hd21 #Hd1
- [ >(apply_basic_lt … Hd1) >(apply_basic_ge … Hd2) >apply_basic_lt
- /2 width=1 by monotonic_lt_plus_r/
- | >(apply_basic_ge … Hd1) >(apply_basic_ge … Hd2)
- >apply_basic_ge [2: /2 width=1 by le_plus_a/ ]
- >apply_basic_ge /2 width=1 by monotonic_le_plus_r/
- ]
-]
-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/notation/functions/cocompose_2.ma".
-include "ground/relocation/rtmap_coafter.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-rec definition fun0 (n1:nat) on n1: rtmap → nat.
-* * [ | #n2 #f2 @0 ]
-#f2 cases n1 -n1 [ @0 ]
-#n1 @(↑(fun0 n1 f2))
-defined.
-
-rec definition fun2 (n1:nat) on n1: rtmap → rtmap.
-* * [ | #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) ]
-#f2 cases n1 -n1 [ @f1 ]
-#n1 @(fun1 n1 f1 f2)
-defined.
-
-corec definition cocompose: rtmap → rtmap → rtmap.
-#f2 * #n1 #f1 @(seq … (fun0 n1 f2)) @(cocompose (fun2 n1 f2) (fun1 n1 f1 f2))
-defined.
-
-interpretation "functional co-composition (nstream)"
- 'CoCompose f1 f2 = (cocompose f1 f2).
-
-(* Basic properties on funs *************************************************)
-
-(* Note: we need theese since matita blocks recursive δ when ι is blocked *)
-lemma fun0_xn: ∀f2,n1. 0 = fun0 n1 (↑f2).
-* #n2 #f2 * //
-qed.
-
-lemma fun2_xn: ∀f2,n1. f2 = fun2 n1 (↑f2).
-* #n2 #f2 * //
-qed.
-
-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 //
-qed.
-
-(* Basic inversion lemmas on compose ****************************************)
-
-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.
-#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.
-#f2 #f1 #f #n1 #x
-<cocompose_rew #H destruct
-/2 width=1 by conj/
-qed-.
-
-(* Specific properties on coafter *******************************************)
-
-corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≘ f.
-* #n2 #f2 * #n1 #f1 * #n #f cases n2 -n2
-[ cases n1 -n1
- [ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
- | #n1 #H cases (cocompose_inv_pnx … H) -H /3 width=7 by coafter_push/
- ]
-| #n2 >next_rew #H cases (cocompose_inv_nxx … H) -H /3 width=5 by coafter_next/
-]
-qed-.
-
-theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≘ f2 ~∘ f1.
-/2 width=1 by coafter_total_aux/ qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.tcs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/relocation/rtmap_eq.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-(* Specific properties ******************************************************)
-
-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/
-| #n1 #H elim (eq_inv_np … H) -H //
-| #n1 #n2 #IH #H lapply (eq_inv_nn … H ????) -H [1,2,3,4: // ]
- #H elim (IH H) -IH -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 →
- n1 = n2 ∧ f1 ≡ f2.
-/2 width=1 by eq_inv_seq_aux/ qed-.
-
-corec lemma nstream_eq: ∀f1,f2. f1 ≡ f2 → f1 ≗ f2.
-* #n1 #f1 * #n2 #f2 #Hf cases (eq_inv_gen … Hf) -Hf *
-#g1 #g2 #Hg #H1 #H2
-[ cases (push_inv_seq_dx … H1) -H1 * -n1 #H1
- cases (push_inv_seq_dx … H2) -H2 * -n2 #H2
- @eq_seq /2 width=1 by/
-| cases (next_inv_seq_dx … H1) -H1 #m1 #H1 * -n1
- cases (next_inv_seq_dx … H2) -H2 #m2 #H2 * -n2
- cases (eq_inv_seq … Hg … H1 H2) -g1 -g2 #Hm #Hf
- @eq_seq /2 width=1 by/
-]
-qed-.
-
-corec lemma nstream_inv_eq: ∀f1,f2. f1 ≗ f2 → f1 ≡ f2.
-* #n1 #f1 * #n2 #f2 #H cases (eq_stream_inv_seq ??? H) -H [2,3,4,5,6,7: // ]
-#Hf * -n2 cases n1 -n1 /3 width=5 by eq_push/
-#n @eq_next /3 width=5 by eq_seq/
-qed.
-
-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.
+++ /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/notation/functions/identity_0.ma".
-include "ground/relocation/rtmap_eq.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-corec definition id: rtmap ≝ ⫯id.
-
-interpretation "identity (nstream)"
- 'Identity = (id).
-
-(* Basic properties *********************************************************)
-
-lemma id_rew: ⫯𝐈𝐝 = 𝐈𝐝.
-<(stream_rew … (𝐈𝐝)) in ⊢ (???%); normalize //
-qed.
-
-lemma id_eq_rew: ⫯𝐈𝐝 ≡ 𝐈𝐝.
-cases id_rew in ⊢ (??%); //
-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/notation/functions/identity_0.ma".
-include "ground/relocation/rtmap_isid.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-(* Specific inversion lemmas ************************************************)
-
-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-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.tcs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground/notation/functions/apply_2.ma".
-include "ground/relocation/nstream_eq.ma".
-include "ground/relocation/rtmap_istot.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-rec definition apply (i: nat) on i: rtmap → nat ≝ ?.
-* #n #f cases i -i
-[ @n
-| #i lapply (apply i f) -apply -i -f
- #i @(↑(n+i))
-]
-defined.
-
-interpretation "functional application (nstream)"
- 'Apply f i = (apply i f).
-
-(* Specific properties on at ************************************************)
-
-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).
-#n elim n -n /3 width=7 by at_push, at_next/
-qed.
-
-lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩.
-#i1 elim i1 -i1
-[ * // | #i #IH * /3 width=1 by at_S1/ ]
-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.
-#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.
-#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 →
- ∃∃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: // ]
-#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
-#i2 #Hi * -j2 /2 width=3 by ex2_intro/
-qed-.
-
-lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2.
-/2 width=6 by at_mono/ qed-.
-
-(* Spercific forward lemmas on at *******************************************)
-
-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
- #j1 #Ht * -i2 /4 width=2 by at_increasing, monotonic_le_plus_r, le_S_S/
-]
-qed-.
-
-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-.
-
-(* Basic properties *********************************************************)
-
-lemma apply_O1: ∀n,f. (n⨮f)@❨0❩ = n.
-// qed.
-
-lemma apply_S1: ∀n,f,i. (n⨮f)@❨↑i❩ = ↑(n+f@❨i❩).
-// qed.
-
-lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
-#i elim i -i [2: #i #IH ] * #n1 #f1 * #n2 #f2 #H
-elim (eq_inv_seq_aux … H) -H normalize //
-#Hn #Hf /4 width=1 by eq_f2, eq_f/
-qed.
-
-lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
-* #n #f * //
-qed.
-
-(* Main inversion lemmas ****************************************************)
-
-theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
-/2 width=4 by at_inj/ qed-.
-
-corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
-* #n1 #f1 * #n2 #f2 #Hf @eq_seq
-[ @(Hf 0)
-| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
- lapply (Hf 0) >apply_O1 >apply_O1 #H destruct
- lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
- /3 width=2 by injective_plus_r, injective_S/
-]
-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/relocation/rtmap_sor.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-axiom union: rtmap → rtmap → rtmap.
-
-interpretation "union (nstream)"
- 'union f1 f2 = (union f1 f2).
-
-(* Specific properties on sor ***********************************************)
-
-axiom sor_total: ∀f1,f2. f1 ⋓ f2 ≘ f1 ∪ f2.
--- /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/notation/functions/upspoon_1.ma".
+include "ground/lib/stream.ma".
+include "ground/arith/pnat.ma".
+
+(* RELOCATION P-STREAM ******************************************************)
+
+definition rtmap: Type[0] ≝ stream pnat.
+
+definition push: rtmap → rtmap ≝ λf. 𝟏⨮f.
+
+interpretation "push (pstream)" 'UpSpoon f = (push f).
+
+definition next: rtmap → rtmap.
+* #p #f @(↑p⨮f)
+defined.
+
+interpretation "next (pstream)" 'UpArrow f = (next f).
+
+(* Basic properties *********************************************************)
+
+lemma push_rew: ∀f. 𝟏⨮f = ⫯f.
+// qed.
+
+lemma next_rew: ∀f,p. (↑p)⨮f = ↑(p⨮f).
+// qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma injective_push: injective ? ? push.
+#f1 #f2 <push_rew <push_rew #H destruct //
+qed-.
+
+lemma discr_push_next: ∀f1,f2. ⫯f1 = ↑f2 → ⊥.
+#f1 * #p2 #f2 <push_rew <next_rew #H destruct
+qed-.
+
+lemma discr_next_push: ∀f1,f2. ↑f1 = ⫯f2 → ⊥.
+* #p1 #f1 #f2 <next_rew <push_rew #H destruct
+qed-.
+
+lemma injective_next: injective ? ? next.
+* #p1 #f1 * #p2 #f2 <next_rew <next_rew #H destruct //
+qed-.
+
+lemma push_inv_seq_sn: ∀f,g,p. p⨮g = ⫯f → ∧∧ 𝟏 = p & g = f.
+#f #g #p <push_rew #H destruct /2 width=1 by conj/
+qed-.
+
+lemma push_inv_seq_dx: ∀f,g,p. ⫯f = p⨮g → ∧∧ 𝟏 = p & g = f.
+#f #g #p <push_rew #H destruct /2 width=1 by conj/
+qed-.
+
+lemma next_inv_seq_sn: ∀f,g,p. p⨮g = ↑f → ∃∃q. q⨮g = f & ↑q = p.
+* #q #f #g #p <next_rew #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma next_inv_seq_dx: ∀f,g,p. ↑f = p⨮g → ∃∃q. q⨮g = f & ↑q = p.
+* #q #f #g #p <next_rew #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma case_prop (Q:predicate rtmap):
+ (∀f. Q (⫯f)) → (∀f. Q (↑f)) → ∀f. Q f.
+#Q #H1 #H2 * * //
+qed-.
+
+lemma case_type0 (Q:rtmap→Type[0]):
+ (∀f. Q (⫯f)) → (∀f. Q (↑f)) → ∀f. Q f.
+#Q #H1 #H2 * * //
+qed-.
+
+lemma iota_push: ∀Q,a,b,f. a f = case_type0 Q a b (⫯f).
+// qed.
+
+lemma iota_next: ∀Q,a,b,f. b f = case_type0 Q a b (↑f).
+#Q #a #b * //
+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/relocation/pstream_tls.ma".
+include "ground/relocation/pstream_istot.ma".
+include "ground/relocation/rtmap_after.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+corec definition compose: rtmap → rtmap → rtmap.
+#f2 * #p1 #f1 @(stream_cons … (f2@❨p1❩)) @(compose ? f1) -compose -f1
+@(⫰*[p1]f2)
+defined.
+
+interpretation "functional composition (nstream)"
+ 'compose f2 f1 = (compose f2 f1).
+
+(* Basic properies on compose ***********************************************)
+
+lemma compose_rew: ∀f2,f1,p1. f2@❨p1❩⨮(⫰*[p1]f2)∘f1 = f2∘(p1⨮f1).
+#f2 #f1 #p1 <(stream_rew … (f2∘(p1⨮f1))) normalize //
+qed.
+
+lemma compose_next: ∀f2,f1,f. f2∘f1 = f → (↑f2)∘f1 = ↑f.
+#f2 * #p1 #f1 #f <compose_rew <compose_rew
+* -f /2 width=1 by eq_f2/
+qed.
+
+(* Basic inversion lemmas on compose ****************************************)
+
+lemma compose_inv_rew: ∀f2,f1,f,p1,p. f2∘(p1⨮f1) = p⨮f →
+ f2@❨p1❩ = p ∧ (⫰*[p1]f2)∘f1 = f.
+#f2 #f1 #f #p1 #p <compose_rew
+#H destruct /2 width=1 by conj/
+qed-.
+
+lemma compose_inv_O2: ∀f2,f1,f,p2,p. (p2⨮f2)∘(⫯f1) = p⨮f →
+ p2 = p ∧ f2∘f1 = f.
+#f2 #f1 #f #p2 #p <compose_rew
+#H destruct /2 width=1 by conj/
+qed-.
+
+lemma compose_inv_S2: ∀f2,f1,f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
+ f2@❨p1❩+p2 = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+#f2 #f1 #f #p2 #p1 #p <compose_rew
+#H destruct >nsucc_inj <stream_tls_swap
+/2 width=1 by conj/
+qed-.
+
+lemma compose_inv_S1: ∀f2,f1,f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
+ ↑(f2@❨p1❩) = p ∧ f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+#f2 #f1 #f #p1 #p <compose_rew
+#H destruct /2 width=1 by conj/
+qed-.
+
+(* Specific properties on after *********************************************)
+
+lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
+ ∀p. p⨮f2 ⊚ ⫯f1 ≘ p⨮f.
+#f2 #f1 #f #Hf #p elim p -p
+/2 width=7 by after_refl, after_next/
+qed.
+
+lemma after_S2: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f →
+ ∀p2. p2⨮f2 ⊚ ↑p1⨮f1 ≘ (p+p2)⨮f.
+#f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
+/2 width=7 by after_next, after_push/
+qed.
+
+lemma after_apply: ∀p1,f2,f1,f.
+ (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
+#p1 elim p1 -p1
+[ * /2 width=1 by after_O2/
+| #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
+ /3 width=1 by after_S2/
+]
+qed-.
+
+corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
+* #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
+[ cases p1 -p1
+ [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
+ | #p1 #H cases (compose_inv_S2 … H) -H * -p /3 width=7 by after_push/
+ ]
+| #p2 >next_rew #H cases (compose_inv_S1 … H) -H * -p >next_rew
+ /3 width=5 by after_next/
+]
+qed-.
+
+theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
+/2 width=1 by after_total_aux/ qed.
+
+(* Specific inversion lemmas on after ***************************************)
+
+lemma after_inv_xpx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ⫯f1 = g2 →
+ f2 ⊚ f1 ≘ f ∧ p2 = p.
+#f2 #g2 #f #p2 elim p2 -p2
+[ #p #Hf #f1 #H2 elim (after_inv_ppx … Hf … H2) -g2 [|*: // ]
+ #g #Hf #H elim (push_inv_seq_dx … H) -H destruct /2 width=1 by conj/
+| #p2 #IH #p #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [|*: // ]
+ #g1 #Hg #H1 elim (next_inv_seq_dx … H1) -H1
+ #x #Hx #H destruct elim (IH … Hg) [|*: // ] -IH -Hg
+ #H destruct /2 width=1 by conj/
+]
+qed-.
+
+lemma after_inv_xnx: ∀f2,g2,f,p2,p. p2⨮f2 ⊚ g2 ≘ p⨮f → ∀f1. ↑f1 = g2 →
+ ∃∃q. f2 ⊚ f1 ≘ q⨮f & q+p2 = p.
+#f2 #g2 #f #p2 elim p2 -p2
+[ #p #Hf #f1 #H2 elim (after_inv_pnx … Hf … H2) -g2 [|*: // ]
+ #g #Hf #H elim (next_inv_seq_dx … H) -H
+ #x #Hx #Hg destruct /2 width=3 by ex2_intro/
+| #p2 #IH #p #Hf #f1 #H2 elim (after_inv_nxx … Hf) -Hf [|*: // ]
+ #g #Hg #H elim (next_inv_seq_dx … H) -H
+ #x #Hx #H destruct elim (IH … Hg) -IH -Hg [|*: // ]
+ #m #Hf #Hm destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma after_inv_const: ∀f2,f1,f,p1,p.
+ p⨮f2 ⊚ p1⨮f1 ≘ p⨮f → f2 ⊚ f1 ≘ f ∧ 𝟏 = p1.
+#f2 #f1 #f #p1 #p elim p -p
+[ #H elim (after_inv_pxp … H) -H [|*: // ]
+ #g2 #Hf #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
+| #p #IH #H lapply (after_inv_nxn … H ????) -H /2 width=5 by/
+]
+qed-.
+
+lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
+/2 width=4 by after_mono/ qed-.
+
+(* Specific forward lemmas on after *****************************************)
+
+lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
+#f2 #f1 #f #p1 #p #H lapply (after_fwd_at ? p1 (𝟏) … H) -H [4:|*: // ]
+/3 width=2 by at_inv_O1, sym_eq/
+qed-.
+
+lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
+ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
+#f #f1 #p1 elim p1 -p1
+[ #f2 #p2 #p #H elim (after_inv_xpx … H) -H //
+| #p1 #IH * #q2 #f2 #p2 #p #H elim (after_inv_xnx … H) -H [|*: // ]
+ #x #Hx #H destruct /2 width=3 by/
+]
+qed-.
+
+lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
+ (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
+/3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
+
+(* Properties on apply ******************************************************)
+
+lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
+/4 width=6 by after_fwd_at, at_inv_total, sym_eq/ 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/arith/nat_lt_plus.ma".
+include "ground/relocation/rtmap_basic_at.ma".
+include "ground/relocation/pstream_after.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+(* Specific properties on basic relocation **********************************)
+
+lemma apply_basic_lt: ∀m,n,i. ninj i ≤ m → 𝐁❨m,n❩@❨i❩ = i.
+/3 width=1 by at_inv_total, at_basic_lt/ qed-.
+
+lemma apply_basic_ge: ∀m,n,i. m < ninj i → 𝐁❨m,n❩@❨i❩ = i+n.
+/3 width=1 by at_inv_total, at_basic_ge/ qed-.
+
+(* Specific main properties on basic relocation *****************************)
+
+theorem basic_swap: ∀d1,d2. d2 ≤ d1 →
+ ∀h1,h2. 𝐁❨d2,h2❩∘𝐁❨d1,h1❩ ≡ 𝐁❨d1+h2,h1❩∘𝐁❨d2,h2❩.
+#d1 #d2 #Hd21 #h1 #h2
+@nstream_inv_eq
+@nstream_eq_inv_ext #i
+<compose_apply <compose_apply
+elim (nat_split_lt_ge d2 i) #Hd2
+[ elim (nat_split_lt_ge d1 i) -Hd21 #Hd1
+ [ >(apply_basic_ge … Hd1) >(apply_basic_ge … Hd2) >apply_basic_ge
+ [ >apply_basic_ge // >nrplus_inj_sn /2 width=1 by nlt_plus_bi_sn/
+ | >nrplus_inj_sn /2 width=2 by nlt_plus_dx_dx/
+ ]
+ | >(apply_basic_lt … Hd1) >(apply_basic_ge … Hd2)
+ >apply_basic_lt // >nrplus_inj_sn /2 width=1 by nle_plus_bi_dx/
+ ]
+| lapply (nle_trans … Hd2 … Hd21) -Hd21 #Hd1
+ >(apply_basic_lt … Hd1) >(apply_basic_lt … Hd2)
+ >apply_basic_lt /2 width=1 by nle_plus_dx_dx/
+]
+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/notation/functions/cocompose_2.ma".
+include "ground/relocation/rtmap_coafter.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+rec definition fun0 (p1:pnat) on p1: rtmap → pnat.
+* * [ | #p2 #f2 @(𝟏) ]
+#f2 cases p1 -p1 [ @(𝟏) ]
+#p1 @(↑(fun0 p1 f2))
+defined.
+
+rec definition fun2 (p1:pnat) on p1: rtmap → rtmap.
+* * [ | #p2 #f2 @(p2⨮f2) ]
+#f2 cases p1 -p1 [ @f2 ]
+#p1 @(fun2 p1 f2)
+defined.
+
+rec definition fun1 (p1:pnat) (f1:rtmap) on p1: rtmap → rtmap.
+* * [ | #p2 #f2 @(p1⨮f1) ]
+#f2 cases p1 -p1 [ @f1 ]
+#p1 @(fun1 p1 f1 f2)
+defined.
+
+corec definition cocompose: rtmap → rtmap → rtmap.
+#f2 * #p1 #f1
+@(stream_cons … (fun0 p1 f2)) @(cocompose (fun2 p1 f2) (fun1 p1 f1 f2))
+defined.
+
+interpretation "functional co-composition (nstream)"
+ 'CoCompose f1 f2 = (cocompose f1 f2).
+
+(* Basic properties on funs *************************************************)
+
+(* Note: we need theese since matita blocks recursive δ when ι is blocked *)
+lemma fun0_xn: ∀f2,p1. 𝟏 = fun0 p1 (↑f2).
+* #p2 #f2 * //
+qed.
+
+lemma fun2_xn: ∀f2,p1. f2 = fun2 p1 (↑f2).
+* #p2 #f2 * //
+qed.
+
+lemma fun1_xxn: ∀f2,f1,p1. fun1 p1 f1 (↑f2) = p1⨮f1.
+* #p2 #f2 #f1 * //
+qed.
+
+(* Basic properies on cocompose *********************************************)
+
+lemma cocompose_rew: ∀f2,f1,p1. (fun0 p1 f2)⨮(fun2 p1 f2)~∘(fun1 p1 f1 f2) = f2 ~∘ (p1⨮f1).
+#f2 #f1 #p1 <(stream_rew … (f2~∘(p1⨮f1))) normalize //
+qed.
+
+(* Basic inversion lemmas on compose ****************************************)
+
+lemma cocompose_inv_ppx: ∀f2,f1,f,x. (⫯f2) ~∘ (⫯f1) = x⨮f →
+ ∧∧ 𝟏 = 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,p1,x. (⫯f2) ~∘ (↑p1⨮f1) = x⨮f →
+ ∃∃p. ↑p = x & f2 ~∘ (p1⨮f1) = p⨮f.
+#f2 #f1 #f #p1 #x
+<cocompose_rew #H destruct
+@(ex2_intro … (fun0 p1 f2)) // <cocompose_rew
+/3 width=1 by eq_f2/
+qed-.
+
+lemma cocompose_inv_nxx: ∀f2,f1,f,p1,x. (↑f2) ~∘ (p1⨮f1) = x⨮f →
+ ∧∧ 𝟏 = x & f2 ~∘ (p1⨮f1) = f.
+#f2 #f1 #f #p1 #x
+<cocompose_rew #H destruct
+/2 width=1 by conj/
+qed-.
+
+(* Specific properties on coafter *******************************************)
+
+corec lemma coafter_total_aux: ∀f2,f1,f. f2 ~∘ f1 = f → f2 ~⊚ f1 ≘ f.
+* #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
+[ cases p1 -p1
+ [ #H cases (cocompose_inv_ppx … H) -H /3 width=7 by coafter_refl, eq_f2/
+ | #p1 #H cases (cocompose_inv_pnx … H) -H /3 width=7 by coafter_push/
+ ]
+| #p2 >next_rew #H cases (cocompose_inv_nxx … H) -H /3 width=5 by coafter_next/
+]
+qed-.
+
+theorem coafter_total: ∀f2,f1. f2 ~⊚ f1 ≘ f2 ~∘ f1.
+/2 width=1 by coafter_total_aux/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/lib/stream_eq.ma".
+include "ground/relocation/rtmap_eq.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+(* Specific properties ******************************************************)
+
+fact eq_inv_seq_aux: ∀f1,f2,p1,p2. p1⨮f1 ≡ p2⨮f2 → p1 = p2 ∧ f1 ≡ f2.
+#f1 #f2 #p1 #p2 @(pnat_ind_2 … p1 p2) -p1 -p2
+[ #p2 #H elim (eq_inv_px … H) -H [2,3: // ]
+ #g1 #H1 #H elim (push_inv_seq_dx … H) -H /2 width=1 by conj/
+| #p1 #_ #H elim (eq_inv_np … H) -H //
+| #p1 #p2 #IH #H lapply (eq_inv_nn … H ????) -H [5:|*: // ]
+ #H elim (IH H) -IH -H /2 width=1 by conj/
+]
+qed-.
+
+lemma eq_inv_seq: ∀g1,g2. g1 ≡ g2 → ∀f1,f2,p1,p2. p1⨮f1 = g1 → p2⨮f2 = g2 →
+ p1 = p2 ∧ f1 ≡ f2.
+/2 width=1 by eq_inv_seq_aux/ qed-.
+
+corec lemma nstream_eq: ∀f1,f2. f1 ≡ f2 → f1 ≗ f2.
+* #p1 #f1 * #p2 #f2 #Hf cases (eq_inv_gen … Hf) -Hf *
+#g1 #g2 #Hg #H1 #H2
+[ cases (push_inv_seq_dx … H1) -H1 * -p1 #H1
+ cases (push_inv_seq_dx … H2) -H2 * -p2 #H2
+ @stream_eq_cons /2 width=1 by/
+| cases (next_inv_seq_dx … H1) -H1 #m1 #H1 * -p1
+ cases (next_inv_seq_dx … H2) -H2 #m2 #H2 * -p2
+ cases (eq_inv_seq … Hg … H1 H2) -g1 -g2 #Hm #Hf
+ @stream_eq_cons /2 width=1 by/
+]
+qed-.
+
+corec lemma nstream_inv_eq: ∀f1,f2. f1 ≗ f2 → f1 ≡ f2.
+* #p1 #f1 * #p2 #f2 #H cases (stream_eq_inv_cons ??? H) -H [|*: // ]
+#Hf * -p2 cases p1 -p1 /3 width=5 by eq_push/
+#n @eq_next /3 width=5 by stream_eq_cons/
+qed.
+
+lemma eq_seq_id: ∀f1,f2. f1 ≡ f2 → ∀n. n⨮f1 ≡ n⨮f2.
+/4 width=1 by nstream_inv_eq, nstream_eq, stream_eq_cons/ 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/notation/functions/identity_0.ma".
+include "ground/relocation/rtmap_eq.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+corec definition id: rtmap ≝ ⫯id.
+
+interpretation "identity (nstream)"
+ 'Identity = (id).
+
+(* Basic properties *********************************************************)
+
+lemma id_rew: ⫯𝐈𝐝 = 𝐈𝐝.
+<(stream_rew … (𝐈𝐝)) in ⊢ (???%); normalize //
+qed.
+
+lemma id_eq_rew: ⫯𝐈𝐝 ≡ 𝐈𝐝.
+cases id_rew in ⊢ (??%); //
+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/relocation/rtmap_isid.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+(* Specific inversion lemmas ************************************************)
+
+lemma isid_inv_seq: ∀f,p. 𝐈❪p⨮f❫ → 𝐈❪f❫ ∧ 𝟏 = p.
+#f #p #H elim (isid_inv_gen … H) -H
+#g #Hg #H elim (push_inv_seq_dx … H) -H /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.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/notation/functions/apply_2.ma".
+include "ground/arith/pnat_le_plus.ma".
+include "ground/relocation/pstream_eq.ma".
+include "ground/relocation/rtmap_istot.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+rec definition apply (i: pnat) on i: rtmap → pnat.
+* #p #f cases i -i
+[ @p
+| #i lapply (apply i f) -apply -i -f
+ #i @(i+p)
+]
+defined.
+
+interpretation "functional application (nstream)"
+ 'Apply f i = (apply i f).
+
+(* Specific properties on at ************************************************)
+
+lemma at_O1: ∀i2,f. @❪𝟏, i2⨮f❫ ≘ i2.
+#i2 elim i2 -i2 /2 width=5 by at_refl, at_next/
+qed.
+
+lemma at_S1: ∀p,f,i1,i2. @❪i1, f❫ ≘ i2 → @❪↑i1, p⨮f❫ ≘ i2+p.
+#p elim p -p /3 width=7 by at_push, at_next/
+qed.
+
+lemma at_total: ∀i1,f. @❪i1, f❫ ≘ f@❨i1❩.
+#i1 elim i1 -i1
+[ * // | #i #IH * /3 width=1 by at_S1/ ]
+qed.
+
+lemma at_istot: ∀f. 𝐓❪f❫.
+/2 width=2 by ex_intro/ qed.
+
+lemma at_plus2: ∀f,i1,i,p,q. @❪i1, p⨮f❫ ≘ i → @❪i1, (p+q)⨮f❫ ≘ i+q.
+#f #i1 #i #p #q #H elim q -q
+/2 width=5 by at_next/
+qed.
+
+(* Specific inversion lemmas on at ******************************************)
+
+lemma at_inv_O1: ∀f,p,i2. @❪𝟏, p⨮f❫ ≘ i2 → p = i2.
+#f #p elim p -p /2 width=6 by at_inv_ppx/
+#p #IH #i2 #H elim (at_inv_xnx … H) -H [|*: // ]
+#j2 #Hj * -i2 /3 width=1 by eq_f/
+qed-.
+
+lemma at_inv_S1: ∀f,p,j1,i2. @❪↑j1, p⨮f❫ ≘ i2 →
+ ∃∃j2. @❪j1, f❫ ≘ j2 & j2+p = i2.
+#f #p elim p -p /2 width=5 by at_inv_npx/
+#p #IH #j1 #i2 #H elim (at_inv_xnx … H) -H [|*: // ]
+#j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
+#i2 #Hi * -j2 /2 width=3 by ex2_intro/
+qed-.
+
+lemma at_inv_total: ∀f,i1,i2. @❪i1, f❫ ≘ i2 → f@❨i1❩ = i2.
+/2 width=6 by at_mono/ qed-.
+
+(* Spercific forward lemmas on at *******************************************)
+
+lemma at_increasing_plus: ∀f,p,i1,i2. @❪i1, p⨮f❫ ≘ i2 → i1 + p ≤ ↑i2.
+#f #p *
+[ #i2 #H <(at_inv_O1 … H) -i2 //
+| #i1 #i2 #H elim (at_inv_S1 … H) -H
+ #j1 #Ht * -i2 <pplus_succ_sn
+ /4 width=2 by at_increasing, ple_plus_bi_dx, ple_succ_bi/
+]
+qed-.
+
+lemma at_fwd_id: ∀f,p,i. @❪i, p⨮f❫ ≘ i → 𝟏 = p.
+#f #p #i #H elim (at_fwd_id_ex … H) -H
+#g #H elim (push_inv_seq_dx … H) -H //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma apply_O1: ∀p,f. (p⨮f)@❨𝟏❩ = p.
+// qed.
+
+lemma apply_S1: ∀p,f,i. (p⨮f)@❨↑i❩ = f@❨i❩+p.
+// qed.
+
+lemma apply_eq_repl (i): eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
+#i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
+elim (eq_inv_seq_aux … H) -H #Hp #Hf //
+>apply_S1 >apply_S1 /3 width=1 by eq_f2/
+qed.
+
+lemma apply_S2: ∀f,i. (↑f)@❨i❩ = ↑(f@❨i❩).
+* #p #f * //
+qed.
+
+(* Main inversion lemmas ****************************************************)
+
+theorem apply_inj: ∀f,i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
+/2 width=4 by at_inj/ qed-.
+
+corec theorem nstream_eq_inv_ext: ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
+* #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
+[ @(Hf (𝟏))
+| @nstream_eq_inv_ext -nstream_eq_inv_ext #i
+ lapply (Hf (𝟏)) >apply_O1 >apply_O1 #H destruct
+ lapply (Hf (↑i)) >apply_S1 >apply_S1 #H
+ /3 width=2 by eq_inv_pplus_bi_dx, eq_inv_psucc_bi/
+]
+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/relocation/rtmap_sor.ma".
+
+(* RELOCATION N-STREAM ******************************************************)
+
+axiom union: rtmap → rtmap → rtmap.
+
+interpretation "union (nstream)"
+ 'union f1 f2 = (union f1 f2).
+
+(* Specific properties on sor ***********************************************)
+
+axiom sor_total: ∀f1,f2. f1 ⋓ f2 ≘ f1 ∪ f2.
--- /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/lib/stream_hdtl.ma".
+include "ground/relocation/pstream.ma".
+
+(* RELOCATION P-STREAM ******************************************************)
+
+(* Poperties with stream_tl *************************************************)
+
+lemma tl_push: ∀f. f = ⫰⫯f.
+// qed.
+
+lemma tl_next: ∀f. ⫰f = ⫰↑f.
+* // 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/lib/stream_tls.ma".
+include "ground/arith/nat_pred_succ.ma".
+include "ground/relocation/pstream_tl.ma".
+
+(* RELOCATION P-STREAM ******************************************************)
+
+(* Poperties with stream_tls ************************************************)
+
+lemma tls_next: ∀f. ∀p:pnat. ⫰*[p]f = ⫰*[p]↑f.
+#f #p >(npsucc_pred p) <stream_tls_swap <stream_tls_swap //
+qed.
(* *)
(**************************************************************************)
-include "ground/relocation/nstream.ma".
+include "ground/relocation/pstream.ma".
(* RELOCATION MAP ***********************************************************)
(**************************************************************************)
include "ground/notation/relations/rafter_3.ma".
+include "ground/arith/nat_pred_succ.ma".
include "ground/relocation/rtmap_istot.ma".
(* RELOCATION MAP ***********************************************************)
(* Properties on tls ********************************************************)
-lemma after_tls: ∀n,f1,f2,f. @❪0, f1❫ ≘ n →
+(* Note: this requires ↑ on first n *)
+lemma after_tls: ∀n,f1,f2,f. @❪𝟏, f1❫ ≘ ↑n →
f1 ⊚ f2 ≘ f → ⫱*[n]f1 ⊚ f2 ≘ ⫱*[n]f.
-#n elim n -n //
+#n @(nat_ind_succ … n) -n //
#n #IH #f1 #f2 #f #Hf1 #Hf
cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
cases (after_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≘ f → 𝐈❪f❫ → 𝐈❪f1❫ ∧ 𝐈❪f2❫.
/3 width=4 by after_fwd_isid2, after_fwd_isid1, conj/ qed-.
-(* Properties on isuni ******************************************************)
-
-lemma after_isid_isuni: ∀f1,f2. 𝐈❪f2❫ → 𝐔❪f1❫ → f1 ⊚ ↑f2 ≘ ↑f1.
-#f1 #f2 #Hf2 #H elim H -H
-/5 width=7 by after_isid_dx, after_eq_repl_back2, after_next, after_push, eq_push_inv_isid/
-qed.
-
-lemma after_uni_next2: ∀f2. 𝐔❪f2❫ → ∀f1,f. ↑f2 ⊚ f1 ≘ f → f2 ⊚ ↑f1 ≘ f.
-#f2 #H elim H -f2
-[ #f2 #Hf2 #f1 #f #Hf
- elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H0 destruct
- /4 width=7 by after_isid_inv_sn, after_isid_sn, after_eq_repl_back0, eq_next/
-| #f2 #_ #g2 #H2 #IH #f1 #f #Hf
- elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H0 destruct
- /3 width=5 by after_next/
-]
-qed.
-
-(* Properties on uni ********************************************************)
-
-lemma after_uni: ∀n1,n2. 𝐔❨n1❩ ⊚ 𝐔❨n2❩ ≘ 𝐔❨n1+n2❩.
-@nat_elim2 [3: #n #m <plus_n_Sm ] (**) (* full auto fails *)
-/4 width=5 by after_uni_next2, after_isid_dx, after_isid_sn, after_next/
-qed.
-
(* Forward lemmas on at *****************************************************)
lemma after_at_fwd: ∀i,i1,f. @❪i1, f❫ ≘ i → ∀f2,f1. f2 ⊚ f1 ≘ f →
]
qed-.
-(* Properties with at *******************************************************)
-
-lemma after_uni_dx: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. f2 ⊚ 𝐔❨i1❩ ≘ f → 𝐔❨i2❩ ⊚ ⫱*[i2] f2 ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- lapply (after_isid_inv_dx … Hf ?) -Hf
- /3 width=3 by after_isid_sn, after_eq_repl_back0/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct
- elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- <tls_xn /3 width=5 by after_next/
- | #g2 #Hg2 #H2 destruct
- elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- <tls_xn /3 width=5 by after_next/
- ]
-]
-qed.
-
-lemma after_uni_sn: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. 𝐔❨i2❩ ⊚ ⫱*[i2] f2 ≘ f → f2 ⊚ 𝐔❨i1❩ ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- lapply (after_isid_inv_sn … Hf ?) -Hf
- /3 width=3 by after_isid_dx, after_eq_repl_back0/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct /3 width=7 by after_push/
- | #g2 #Hg2 #H2 destruct /3 width=5 by after_next/
- ]
-]
-qed-.
-
-lemma after_uni_succ_dx: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. f2 ⊚ 𝐔❨↑i1❩ ≘ f → 𝐔❨↑i2❩ ⊚ ⫱*[↑i2] f2 ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H
- lapply (after_isid_inv_dx … Hg ?) -Hg
- /4 width=5 by after_isid_sn, after_eq_repl_back0, after_next/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct
- elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- <tls_xn /3 width=5 by after_next/
- | #g2 #Hg2 #H2 destruct
- elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- <tls_xn /3 width=5 by after_next/
- ]
-]
-qed.
-
-lemma after_uni_succ_sn: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. 𝐔❨↑i2❩ ⊚ ⫱*[↑i2] f2 ≘ f → f2 ⊚ 𝐔❨↑i1❩ ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- elim (after_inv_nxx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- lapply (after_isid_inv_sn … Hg ?) -Hg
- /4 width=7 by after_isid_dx, after_eq_repl_back0, after_push/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct <tls_xn in Hg; /3 width=7 by after_push/
- | #g2 #Hg2 #H2 destruct <tls_xn in Hg; /3 width=5 by after_next/
- ]
-]
-qed-.
-
-lemma after_uni_one_dx: ∀f2,f. ⫯f2 ⊚ 𝐔❨↑O❩ ≘ f → 𝐔❨↑O❩ ⊚ f2 ≘ f.
-#f2 #f #H @(after_uni_succ_dx … (⫯f2)) /2 width=3 by at_refl/
-qed.
-
-lemma after_uni_one_sn: ∀f1,f. 𝐔❨↑O❩ ⊚ f1 ≘ f → ⫯f1 ⊚ 𝐔❨↑O❩ ≘ f.
-/3 width=3 by after_uni_succ_sn, at_refl/ qed-.
-
(* Forward lemmas on istot **************************************************)
lemma after_istot_fwd: ∀f2,f1,f. f2 ⊚ f1 ≘ f → 𝐓❪f2❫ → 𝐓❪f1❫ → 𝐓❪f❫.
/3 width=8 by at_inj, at_eq_repl_back/
qed-.
-corec fact after_inj_O_aux: ∀f1. @❪0, f1❫ ≘ 0 → H_after_inj f1.
+corec fact after_inj_O_aux: ∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_after_inj f1.
#f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
cases (at_inv_pxp … H1f1) -H1f1 [ |*: // ] #g1 #H1
lapply (istot_inv_push … H2f1 … H1) -H2f1 #H2g1
-cases (H2g1 0) #n #Hn
+cases (H2g1 (𝟏)) #p #Hp
cases (after_inv_pxx … H1f … H1) -H1f * #g21 #g #H1g #H21 #H
[ cases (after_inv_pxp … H2f … H1 H) -f1 -f #g22 #H2g #H22
@(eq_push … H21 H22) -f21 -f22
| cases (after_inv_pxn … H2f … H1 H) -f1 -f #g22 #H2g #H22
@(eq_next … H21 H22) -f21 -f22
]
-@(after_inj_O_aux (⫱*[n]g1) … (⫱*[n]g)) -after_inj_O_aux
+@(after_inj_O_aux (⫱*[↓p]g1) … (⫱*[↓p]g)) -after_inj_O_aux
/2 width=1 by after_tls, istot_tls, at_pxx_tls/
qed-.
-fact after_inj_aux: (∀f1. @❪0, f1❫ ≘ 0 → H_after_inj f1) →
- ∀i2,f1. @❪0, f1❫ ≘ i2 → H_after_inj f1.
+fact after_inj_aux: (∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_after_inj f1) →
+ ∀i2,f1. @❪𝟏, f1❫ ≘ i2 → H_after_inj f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #H1g1 #H1
qed-.
theorem after_inj: ∀f1. H_after_inj f1.
-#f1 #H cases (H 0) /3 width=7 by after_inj_aux, after_inj_O_aux/
+#f1 #H cases (H (𝟏)) /3 width=7 by after_inj_aux, after_inj_O_aux/
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/relocation/rtmap_uni.ma".
+include "ground/relocation/rtmap_nat.ma".
+include "ground/relocation/rtmap_after.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+lemma after_uni_dx: ∀l2,l1,f2. @↑❪l1, f2❫ ≘ l2 →
+ ∀f. f2 ⊚ 𝐔❨l1❩ ≘ f → 𝐔❨l2❩ ⊚ ⫱*[l2] f2 ≘ f.
+#l2 @(nat_ind_succ … l2) -l2
+[ #l1 #f2 #Hf2 #f #Hf
+ elim (rm_nat_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+ lapply (after_isid_inv_dx … Hf ?) -Hf
+ /3 width=3 by after_isid_sn, after_eq_repl_back0/
+| #l2 #IH #l1 #f2 #Hf2 #f #Hf
+ elim (rm_nat_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
+ [ #g2 #k1 #Hg2 #H1 #H2 destruct
+ elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+ <tls_xn /3 width=5 by after_next/
+ | #g2 #Hg2 #H2 destruct
+ elim (after_inv_nxx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+ <tls_xn /3 width=5 by after_next/
+ ]
+]
+qed.
+
+lemma after_uni_sn: ∀l2,l1,f2. @↑❪l1, f2❫ ≘ l2 →
+ ∀f. 𝐔❨l2❩ ⊚ ⫱*[l2] f2 ≘ f → f2 ⊚ 𝐔❨l1❩ ≘ f.
+#l2 @(nat_ind_succ … l2) -l2
+[ #l1 #f2 #Hf2 #f #Hf
+ elim (rm_nat_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+ lapply (after_isid_inv_sn … Hf ?) -Hf
+ /3 width=3 by after_isid_dx, after_eq_repl_back0/
+| #l2 #IH #l1 #f2 #Hf2 #f #Hf
+ elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
+ elim (rm_nat_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
+ [ #g2 #k1 #Hg2 #H1 #H2 destruct /3 width=7 by after_push/
+ | #g2 #Hg2 #H2 destruct /3 width=5 by after_next/
+ ]
+]
+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/arith/nat_plus.ma".
+include "ground/relocation/rtmap_uni.ma".
+include "ground/relocation/rtmap_after.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+(* Properties on isuni ******************************************************)
+
+lemma after_isid_isuni: ∀f1,f2. 𝐈❪f2❫ → 𝐔❪f1❫ → f1 ⊚ ↑f2 ≘ ↑f1.
+#f1 #f2 #Hf2 #H elim H -H
+/5 width=7 by after_isid_dx, after_eq_repl_back2, after_next, after_push, eq_push_inv_isid/
+qed.
+
+lemma after_uni_next2: ∀f2. 𝐔❪f2❫ → ∀f1,f. ↑f2 ⊚ f1 ≘ f → f2 ⊚ ↑f1 ≘ f.
+#f2 #H elim H -f2
+[ #f2 #Hf2 #f1 #f #Hf
+ elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H0 destruct
+ /4 width=7 by after_isid_inv_sn, after_isid_sn, after_eq_repl_back0, eq_next/
+| #f2 #_ #g2 #H2 #IH #f1 #f #Hf
+ elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H0 destruct
+ /3 width=5 by after_next/
+]
+qed.
+
+(* Properties on uni ********************************************************)
+
+lemma after_uni: ∀n1,n2. 𝐔❨n1❩ ⊚ 𝐔❨n2❩ ≘ 𝐔❨n2+n1❩.
+#n1 @(nat_ind_succ … n1) -n1
+/3 width=5 by after_isid_sn, after_next, eq_f/
+qed.
+
+lemma after_uni_sn_pushs (m) (f): 𝐔❨m❩ ⊚ f ≘ ↑*[m]f.
+#m @(nat_ind_succ … m) -m
+/2 width=5 by after_isid_sn, after_next/
+qed.
+
+(* Properties with at *******************************************************)
+
+lemma after_uni_succ_dx: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
+ ∀f. f2 ⊚ 𝐔❨i1❩ ≘ f → 𝐔❨i2❩ ⊚ ⫱*[i2] f2 ≘ f.
+#i2 elim i2 -i2
+[ #i1 #f2 #Hf2 #f #Hf
+ elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+ elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H
+ lapply (after_isid_inv_dx … Hg ?) -Hg
+ /4 width=5 by after_isid_sn, after_eq_repl_back0, after_next/
+| #i2 #IH #i1 #f2 #Hf2 #f #Hf >nsucc_inj
+ elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
+ [ #g2 #j1 #Hg2 #H1 #H2 destruct >nsucc_inj in Hf; #Hf
+ elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+ <tls_xn /3 width=5 by after_next/
+ | #g2 #Hg2 #H2 destruct
+ elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
+ <tls_xn /3 width=5 by after_next/
+ ]
+]
+qed.
+
+lemma after_uni_succ_sn: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
+ ∀f. 𝐔❨i2❩ ⊚ ⫱*[i2] f2 ≘ f → f2 ⊚ 𝐔❨i1❩ ≘ f.
+#i2 elim i2 -i2
+[ #i1 #f2 #Hf2 #f #Hf
+ elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
+ elim (after_inv_nxx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
+ lapply (after_isid_inv_sn … Hg ?) -Hg
+ /4 width=7 by after_isid_dx, after_eq_repl_back0, after_push/
+| #i2 #IH #i1 #f2 #Hf2 #f >nsucc_inj #Hf
+ elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
+ elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
+ [ #g2 #j1 #Hg2 #H1 #H2 destruct <tls_xn in Hg; /3 width=7 by after_push/
+ | #g2 #Hg2 #H2 destruct <tls_xn in Hg; /3 width=5 by after_next/
+ ]
+]
+qed-.
+
+lemma after_uni_one_dx: ∀f2,f. ⫯f2 ⊚ 𝐔❨𝟏❩ ≘ f → 𝐔❨𝟏❩ ⊚ f2 ≘ f.
+#f2 #f #H @(after_uni_succ_dx … (⫯f2)) /2 width=3 by at_refl/
+qed.
+
+lemma after_uni_one_sn: ∀f1,f. 𝐔❨𝟏❩ ⊚ f1 ≘ f → ⫯f1 ⊚ 𝐔❨𝟏❩ ≘ f.
+/3 width=3 by after_uni_succ_sn, at_refl/ qed-.
(**************************************************************************)
include "ground/notation/relations/rat_3.ma".
-include "ground/relocation/rtmap_uni.ma".
+include "ground/arith/pnat_plus.ma".
+include "ground/arith/pnat_lt_pred.ma".
+include "ground/relocation/rtmap_id.ma".
(* RELOCATION MAP ***********************************************************)
-coinductive at: rtmap → relation nat ≝
-| at_refl: ∀f,g,j1,j2. ⫯f = g → 0 = j1 → 0 = j2 → at g j1 j2
+coinductive at: relation3 rtmap pnat pnat ≝
+| at_refl: ∀f,g,j1,j2. ⫯f = g → 𝟏 = j1 → 𝟏 = j2 → at g j1 j2
| at_push: ∀f,i1,i2. at f i1 i2 → ∀g,j1,j2. ⫯f = g → ↑i1 = j1 → ↑i2 = j2 → at g j1 j2
| at_next: ∀f,i1,i2. at f i1 i2 → ∀g,j2. ↑f = g → ↑i2 = j2 → at g i1 j2
.
(* Basic inversion lemmas ***************************************************)
-lemma at_inv_ppx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. 0 = i1 → ⫯g = f → 0 = i2.
+lemma at_inv_ppx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
#f #i1 #i2 * -f -i1 -i2 //
[ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
| #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (discr_push_next … H)
(* Advanced inversion lemmas ************************************************)
+alias symbol "UpArrow" (instance 3) = "successor (positive integers)".
lemma at_inv_ppn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
- ∀g,j2. 0 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
+ ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
#f #i1 #i2 #Hf #g #j2 #H1 #H <(at_inv_ppx … Hf … H1 H) -f -g -i1 -i2
#H destruct
qed-.
+alias symbol "UpArrow" (instance 7) = "successor (positive integers)".
lemma at_inv_npp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
- ∀g,j1. ↑j1 = i1 → ⫯g = f → 0 = i2 → ⊥.
+ ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
#x2 #Hg * -i2 #H destruct
qed-.
qed-.
lemma at_inv_xnp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
- ∀g. ↑g = f → 0 = i2 → ⊥.
+ ∀g. ↑g = f → 𝟏 = i2 → ⊥.
#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
#x2 #Hg * -i2 #H destruct
qed-.
#x2 #Hg * -i2 #H destruct //
qed-.
-lemma at_inv_pxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 0 = i1 → 0 = i2 → ∃g. ⫯g = f.
+lemma at_inv_pxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
#f elim (pn_split … f) * /2 width=2 by ex_intro/
#g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2)
qed-.
-lemma at_inv_pxn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀j2. 0 = i1 → ↑j2 = i2 →
+lemma at_inv_pxn: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
∃∃g. @❪i1,g❫ ≘ j2 & ↑g = f.
#f elim (pn_split … f) *
#g #H #i1 #i2 #Hf #j2 #H1 #H2
]
qed-.
+alias symbol "UpArrow" (instance 5) = "successor (positive integers)".
lemma at_inv_nxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
- ∀j1. ↑j1 = i1 → 0 = i2 → ⊥.
+ ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
#f elim (pn_split f) *
#g #H #i1 #i2 #Hf #j1 #H1 #H2
[ elim (at_inv_npp … Hf … H1 H H2)
(* Note: the following inversion lemmas must be checked *)
lemma at_inv_xpx: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f →
- (0 = i1 ∧ 0 = i2) ∨
- ∃∃j1,j2. @❪j1,g❫ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
+ ∨∨ ∧∧ 𝟏 = i1 & 𝟏 = i2
+ | ∃∃j1,j2. @❪j1,g❫ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
#f * [2: #i1 ] #i2 #Hf #g #H
[ elim (at_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
| >(at_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/
]
qed-.
-lemma at_inv_xpp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f → 0 = i2 → 0 = i1.
+lemma at_inv_xpp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
#f #i1 #i2 #Hf #g #H elim (at_inv_xpx … Hf … H) -f * //
#j1 #j2 #_ #_ * -i2 #H destruct
qed-.
]
qed-.
-lemma at_inv_xxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 0 = i2 →
- ∃∃g. 0 = i1 & ⫯g = f.
+lemma at_inv_xxp: ∀f,i1,i2. @❪i1,f❫ ≘ i2 → 𝟏 = i2 →
+ ∃∃g. 𝟏 = i1 & ⫯g = f.
#f elim (pn_split f) *
#g #H #i1 #i2 #Hf #H2
[ /3 width=6 by at_inv_xpp, ex2_intro/
[ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf //
| #i2 #IH * //
#i1 #f #Hf elim (at_inv_nxn … Hf) -Hf [1,4: * |*: // ]
- /3 width=2 by le_S_S, le_S/
+ /3 width=2 by ple_succ_bi, ple_succ_dx/
]
qed-.
lemma at_increasing_strict: ∀g,i1,i2. @❪i1,g❫ ≘ i2 → ∀f. ↑f = g →
i1 < i2 ∧ @❪i1,f❫ ≘ ↓i2.
#g #i1 #i2 #Hg #f #H elim (at_inv_xnx … Hg … H) -Hg -H
-/4 width=2 by conj, at_increasing, le_S_S/
+/4 width=2 by conj, at_increasing, ple_succ_bi/
qed-.
lemma at_fwd_id_ex: ∀f,i. @❪i,f❫ ≘ i → ∃g. ⫯g = f.
#f elim (pn_split f) * /2 width=2 by ex_intro/
#g #H #i #Hf elim (at_inv_xnx … Hf … H) -Hf -H
#j2 #Hg #H destruct lapply (at_increasing … Hg) -Hg
-#H elim (lt_le_false … H) -H //
+#H elim (plt_ge_false … H) -H //
qed-.
(* Basic properties *********************************************************)
[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
#g [ #x2 ] #Hg [ #H2 ] #H0
[ * /3 width=3 by at_refl, ex2_intro/
- #i1 #Hi12 destruct lapply (le_S_S_to_le … Hi12) -Hi12
+ #i1 #Hi12 destruct lapply (ple_inv_succ_bi … Hi12) -Hi12
#Hi12 elim (IH … Hg … Hi12) -x2 -IH
- /3 width=7 by at_push, ex2_intro, le_S_S/
+ /3 width=7 by at_push, ex2_intro, ple_succ_bi/
| #i1 #Hi12 elim (IH … Hg … Hi12) -IH -i2
- /3 width=5 by at_next, ex2_intro, le_S_S/
+ /3 width=5 by at_next, ex2_intro, ple_succ_bi/
]
| elim (at_inv_xxp … Hf) -Hf //
- #g * -i2 #H2 #i1 #Hi12 <(le_n_O_to_eq … Hi12)
+ #g * -i2 #H2 #i1 #Hi12 <(ple_inv_unit_dx … Hi12)
/3 width=3 by at_refl, ex2_intro/
]
qed-.
lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @❪i2,f❫ ≘ i2 → @❪i1,f❫ ≘ i1.
-#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
+#i1 #i2 #H @(ple_ind_alt … H) -i1 -i2 [ #i2 | #i1 #i2 #_ #IH ]
#f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/
qed-.
i1 < i2 → j1 < j2.
#j2 elim j2 -j2
[ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f //
- #g #H21 #_ #j1 #i1 #_ #Hi elim (lt_le_false … Hi) -Hi //
+ #g #H21 #_ #j1 #i1 #_ #Hi elim (plt_ge_false … Hi) -Hi //
| #j2 #IH #i2 #f #H2f * //
- #j1 #i1 #H1f #Hi elim (lt_inv_gen … Hi)
- #x2 #_ #H21 elim (at_inv_nxn … H2f … H21) -H2f [1,3: * |*: // ]
+ #j1 #i1 #H1f #Hi elim (plt_inv_gen … Hi)
+ #_ #Hi2 elim (at_inv_nxn … H2f (↓i2)) -H2f [1,3: * |*: // ]
#g #H2g #H
[ elim (at_inv_xpn … H1f … H) -f
- /4 width=8 by lt_S_S_to_lt, lt_S_S/
- | /4 width=8 by at_inv_xnn, lt_S_S/
+ /4 width=8 by plt_inv_succ_bi, plt_succ_bi/
+ | /4 width=8 by at_inv_xnn, plt_succ_bi/
]
]
qed-.
j1 < j2 → i1 < i2.
#j1 elim j1 -j1
[ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f //
- #g * -i1 #H #j2 #i2 #H2f #Hj elim (lt_inv_O1 … Hj) -Hj
- #x2 #H22 elim (at_inv_xpn … H2f … H H22) -f //
+ #g * -i1 #H #j2 #i2 #H2f #Hj lapply (plt_des_gen … Hj) -Hj
+ #H22 elim (at_inv_xpn … H2f … (↓j2) H) -f //
| #j1 #IH *
[ #f #H1f elim (at_inv_pxn … H1f) -H1f [ |*: // ]
- #g #H1g #H #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj
+ #g #H1g #H #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
/3 width=7 by at_inv_xnn/
- | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj
- #y2 #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ]
+ | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (plt_inv_succ_sn … Hj) -Hj
+ #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ]
#g #Hg #H
- [ elim (at_inv_xpn … H2f … H H22) -f -H22
- /3 width=7 by lt_S_S/
+ [ elim (at_inv_xpn … H2f … (↓j2) H) -f
+ /3 width=7 by plt_succ_bi/
| /3 width=7 by at_inv_xnn/
]
]
qed-.
theorem at_mono: ∀f,i,i1. @❪i,f❫ ≘ i1 → ∀i2. @❪i,f❫ ≘ i2 → i2 = i1.
-#f #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /3 width=6 by at_inv_monotonic, eq_sym/
+#f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
+#Hi elim (plt_ge_false i i) /3 width=6 by at_inv_monotonic, eq_sym/
qed-.
theorem at_inj: ∀f,i1,i. @❪i1,f❫ ≘ i → ∀i2. @❪i2,f❫ ≘ i → i1 = i2.
-#f #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/
+#f #i1 #i #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
+#Hi elim (plt_ge_false i i) /2 width=6 by at_monotonic/
qed-.
theorem at_div_comm: ∀f2,g2,f1,g1.
(* Properties on tls ********************************************************)
-lemma at_pxx_tls: ∀n,f. @❪0,f❫ ≘ n → @❪0,⫱*[n]f❫ ≘ 0.
-#n elim n -n //
+(* Note: this requires ↑ on first n *)
+lemma at_pxx_tls: ∀n,f. @❪𝟏,f❫ ≘ ↑n → @❪𝟏,⫱*[n]f❫ ≘ 𝟏.
+#n @(nat_ind_succ … n) -n //
#n #IH #f #Hf
cases (at_inv_pxn … Hf) -Hf [ |*: // ] #g #Hg #H0 destruct
<tls_xn /2 width=1 by/
qed.
-lemma at_tls: ∀i2,f. ⫯⫱*[↑i2]f ≡ ⫱*[i2]f → ∃i1. @❪i1,f❫ ≘ i2.
-#i2 elim i2 -i2
+(* Note: this requires ↑ on third n2 *)
+lemma at_tls: ∀n2,f. ⫯⫱*[↑n2]f ≡ ⫱*[n2]f → ∃i1. @❪i1,f❫ ≘ ↑n2.
+#n2 @(nat_ind_succ … n2) -n2
[ /4 width=4 by at_eq_repl_back, at_refl, ex_intro/
-| #i2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
+| #n2 #IH #f <tls_xn <tls_xn in ⊢ (??%→?); #H
elim (IH … H) -IH -H #i1 #Hf
elim (pn_split f) * #g #Hg destruct /3 width=8 by at_push, at_next, ex_intro/
]
(* Inversion lemmas with tls ************************************************)
-lemma at_inv_nxx: ∀n,g,i1,j2. @❪↑i1,g❫ ≘ j2 → @❪0,g❫ ≘ n →
- ∃∃i2. @❪i1,⫱*[↑n]g❫ ≘ i2 & ↑(n+i2) = j2.
+(* Note: this does not require ↑ on second and third p *)
+lemma at_inv_nxx: ∀p,g,i1,j2. @❪↑i1,g❫ ≘ j2 → @❪𝟏,g❫ ≘ p →
+ ∃∃i2. @❪i1,⫱*[p]g❫ ≘ i2 & p+i2 = j2.
#n elim n -n
[ #g #i1 #j2 #Hg #H
elim (at_inv_pxp … H) -H [ |*: // ] #f #H0
]
qed-.
-lemma at_inv_tls: ∀i2,i1,f. @❪i1,f❫ ≘ i2 → ⫯⫱*[↑i2]f ≡ ⫱*[i2]f.
-#i2 elim i2 -i2
+(* Note: this requires ↑ on first n2 *)
+lemma at_inv_tls: ∀n2,i1,f. @❪i1,f❫ ≘ ↑n2 → ⫯⫱*[↑n2]f ≡ ⫱*[n2]f.
+#n2 @(nat_ind_succ … n2) -n2
[ #i1 #f #Hf elim (at_inv_xxp … Hf) -Hf // #g #H1 #H destruct
/2 width=1 by eq_refl/
-| #i2 #IH #i1 #f #Hf
+| #n2 #IH #i1 #f #Hf
elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
[ #g #j1 #Hg #H1 #H2 | #g #Hg #Ho ] destruct
<tls_xn /2 width=2 by/
(* Advanced properties on isid **********************************************)
corec lemma isid_at: ∀f. (∀i. @❪i,f❫ ≘ i) → 𝐈❪f❫.
-#f #Hf lapply (Hf 0)
+#f #Hf lapply (Hf (𝟏))
#H cases (at_fwd_id_ex … H) -H
#g #H @(isid_push … H) /3 width=7 by at_inv_npn/
qed-.
theorem at_div_id_sn: ∀f. H_at_div 𝐈𝐝 f f 𝐈𝐝.
/3 width=6 by at_div_id_dx, at_div_comm/ qed-.
-
-(* Properties with uniform relocations **************************************)
-
-lemma at_uni: ∀n,i. @❪i,𝐔❨n❩❫ ≘ n+i.
-#n elim n -n /2 width=5 by at_next/
-qed.
-
-(* Inversion lemmas with uniform relocations ********************************)
-
-lemma at_inv_uni: ∀n,i,j. @❪i,𝐔❨n❩❫ ≘ j → j = n+i.
-/2 width=4 by at_mono/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_rplus_succ.ma".
+include "ground/relocation/rtmap_uni.ma".
+include "ground/relocation/rtmap_at.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+(* Properties with uniform relocations **************************************)
+
+lemma at_uni: ∀n,i. @❪i,𝐔❨n❩❫ ≘ i+n.
+#n @(nat_ind_succ … n) -n /2 width=5 by at_next/
+qed.
+
+(* Inversion lemmas with uniform relocations ********************************)
+
+lemma at_inv_uni: ∀n,i,j. @❪i,𝐔❨n❩❫ ≘ j → j = i+n.
+/2 width=4 by at_mono/ qed-.
(**************************************************************************)
include "ground/notation/functions/basic_2.ma".
-include "ground/relocation/rtmap_at.ma".
+include "ground/relocation/rtmap_uni.ma".
(* RELOCATION MAP ***********************************************************)
interpretation "basic relocation (rtmap)"
'Basic m n = (basic m n).
-(* Prioerties with application **********************************************)
+(* Basic properties *********************************************************)
-lemma at_basic_lt: ∀m,n,i. i < m → @❪i, 𝐁❨m,n❩❫ ≘ i.
-#m elim m -m [ #n #i #H elim (lt_zero_false … H) ]
-#m #IH #n * [ /2 width=2 by refl, at_refl/ ]
-#i #H lapply (lt_S_S_to_lt … H) -H /3 width=7 by refl, at_push/
+lemma at_basic_succ_sn (m) (n): ⫯𝐁❨m,n❩ = 𝐁❨↑m,n❩.
+#m #n >pushs_S //
qed.
-lemma at_basic_ge: ∀m,n,i. m ≤ i → @❪i, 𝐁❨m,n❩❫ ≘ n+i.
-#m elim m -m //
-#m #IH #n #j #H
-elim (le_inv_S1 … H) -H #i #Hmi #H destruct
-/3 width=7 by refl, at_push/
+lemma at_basic_zero_succ (n): ↑𝐁❨𝟎,n❩ = 𝐁❨𝟎,↑n❩.
+#n >nexts_S //
qed.
-
-(* Inversion lemmas with application ****************************************)
-
-lemma at_basic_inv_lt: ∀m,n,i,j. i < m → @❪i, 𝐁❨m,n❩❫ ≘ j → i = j.
-/3 width=4 by at_basic_lt, at_mono/ qed-.
-
-lemma at_basic_inv_ge: ∀m,n,i,j. m ≤ i → @❪i, 𝐁❨m,n❩❫ ≘ j → n+i = j.
-/3 width=4 by at_basic_ge, at_mono/ qed-.
(* *)
(**************************************************************************)
-include "ground/relocation/rtmap_after.ma".
+include "ground/arith/nat_le_pred.ma".
+include "ground/relocation/rtmap_after_uni.ma".
include "ground/relocation/rtmap_basic.ma".
(* RELOCATION MAP ***********************************************************)
(* Properties with composition **********************************************)
-lemma after_basic_rc (m2,m1,n2,n1):
- m1 ≤ m2 → m2 ≤ m1+n1 → 𝐁❨m2,n2❩ ⊚ 𝐁❨m1,n1❩ ≘ 𝐁❨m1,n2+n1❩.
-#m2 elim m2 -m2
-[ #m1 #n2 #n1 #Hm21 #_
- <(le_n_O_to_eq … Hm21) -m1 //
-| #m2 #IH *
- [ #n2 #n1 #_ < plus_O_n #H
- elim (le_inv_S1 … H) -H #x #Hx #H destruct
- <plus_n_Sm
- @after_push [4:|*: // ]
- @(IH 0 … Hx) -IH -n2 -x //
- | #m1 #n2 #n1 #H1 #H2
- lapply (le_S_S_to_le … H1) -H1 #H1
- lapply (le_S_S_to_le … H2) -H2 #H2
- /3 width=7 by after_refl/
- ]
+lemma after_basic_rc (m2,m1):
+ m1 ≤ m2 → ∀n2,n1.m2 ≤ n1+m1 → 𝐁❨m2,n2❩ ⊚ 𝐁❨m1,n1❩ ≘ 𝐁❨m1,n1+n2❩.
+#m2 #m1 @(nat_ind_2_succ … m2 m1) -m2 -m1
+[ #m1 #H #n2 #n1 #_
+ <(nle_inv_zero_dx … H) -m1 //
+| #m2 #IH #_ #n2 #n1 <nplus_zero_dx #H
+ elim (nle_inv_succ_sn … H) -H #Hm2 #Hn1
+ >Hn1 -Hn1 <nplus_succ_sn
+ /3 width=7 by after_push/
+| #m2 #m1 #IH #H1 #n2 #n1 <nplus_succ_dx #H2
+ lapply (nle_inv_succ_bi … H1) -H1 #H1
+ lapply (nle_inv_succ_bi … H2) -H2 #H2
+ /3 width=7 by after_refl/
]
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/arith/nat_plus_rplus.ma".
+include "ground/relocation/rtmap_basic_nat.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+(* Prioerties with application **********************************************)
+
+lemma at_basic_lt (m) (n) (i):
+ ninj i ≤ m → @❪i, 𝐁❨m,n❩❫ ≘ i.
+#m #n #i >(npsucc_pred i) #Hmi
+/2 width=1 by rm_nat_basic_lt/
+qed.
+
+lemma at_basic_ge (m) (n) (i):
+ m < ninj i → @❪i, 𝐁❨m,n❩❫ ≘ i+n.
+#m #n #i >(npsucc_pred i) #Hmi <nrplus_npsucc_sn
+/3 width=1 by rm_nat_basic_ge, nlt_inv_succ_dx/
+qed.
+
+(* Inversion lemmas with application ****************************************)
+
+lemma at_basic_inv_lt (m) (n) (i) (j):
+ ninj i ≤ m → @❪i, 𝐁❨m,n❩❫ ≘ j → i = j.
+/3 width=4 by at_basic_lt, at_mono/ qed-.
+
+lemma at_basic_inv_ge (m) (n) (i) (j):
+ m < ninj i → @❪i, 𝐁❨m,n❩❫ ≘ j → i+n = j.
+/3 width=4 by at_basic_ge, at_mono/ 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/relocation/rtmap_nat_uni.ma".
+include "ground/relocation/rtmap_basic.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+(* Prioerties with application **********************************************)
+
+lemma rm_nat_basic_lt (m) (n) (l):
+ l < m → @↑❪l, 𝐁❨m,n❩❫ ≘ l.
+#m @(nat_ind_succ … m) -m
+[ #n #i #H elim (nlt_inv_zero_dx … H)
+| #m #IH #n #l @(nat_ind_succ … l) -l
+ [ #_ /2 width=2 by refl, at_refl/
+ | #l #_ #H
+ lapply (nlt_inv_succ_bi … H) -H #Hlm
+ /3 width=7 by refl, at_push/
+ ]
+]
+qed.
+
+lemma rm_nat_basic_ge (m) (n) (l):
+ m ≤ l → @↑❪l, 𝐁❨m,n❩❫ ≘ l+n.
+#m @(nat_ind_succ … m) -m //
+#m #IH #n #l #H
+elim (nle_inv_succ_sn … H) -H #Hml #H >H -H
+/3 width=7 by rm_nat_push/
+qed.
+
+(* Inversion lemmas with application ****************************************)
+
+lemma rm_nat_basic_inv_lt (m) (n) (l) (k):
+ l < m → @↑❪l, 𝐁❨m,n❩❫ ≘ k → l = k.
+/3 width=4 by rm_nat_basic_lt, rm_nat_mono/ qed-.
+
+lemma rm_nat_basic_inv_ge (m) (n) (l) (k):
+ m ≤ l → @↑❪l, 𝐁❨m,n❩❫ ≘ k → l+n = k.
+/3 width=4 by rm_nat_basic_ge, rm_nat_mono/ qed-.
include "ground/notation/relations/rcoafter_3.ma".
include "ground/relocation/rtmap_sor.ma".
+include "ground/relocation/rtmap_nat.ma".
include "ground/relocation/rtmap_after.ma".
(* RELOCATION MAP ***********************************************************)
(* Forward lemmas with pushs ************************************************)
-lemma coafter_fwd_pushs: ∀j,i,g2,f1,g. g2 ~⊚ ⫯*[i]f1 ≘ g → @❪i, g2❫ ≘ j →
- ∃f. ⫯*[j] f = g.
-#j elim j -j
-[ #i #g2 #f1 #g #Hg #H
- elim (at_inv_xxp … H) -H [|*: // ] #f2 #H1 #H2 destruct
- /2 width=2 by ex_intro/
-| #j #IH * [| #i ] #g2 #f1 #g #Hg #H
- [ elim (at_inv_pxn … H) -H [|*: // ] #f2 #Hij #H destruct
+lemma coafter_fwd_pushs: ∀k,l,g2,f1,g. g2 ~⊚ ⫯*[l]f1 ≘ g → @↑❪l, g2❫ ≘ k →
+ ∃∃f. ⫱*[k]g2 ~⊚ f1 ≘ f & ⫯*[k] f = g.
+#k @(nat_ind_succ … k) -k
+[ #l #g2 #f1 #g #Hg #H
+ elim (rm_nat_inv_xxp … H) -H [|*: // ] #f2 #H1 #H2 destruct
+ /2 width=3 by ex2_intro/
+| #k #IH * [| #l ] #g2 #f1 #g #Hg #H
+ [ elim (rm_nat_inv_pxn … H) -H [|*: // ] #f2 #Hlk #H destruct
elim (coafter_inv_nxx … Hg) -Hg [|*: // ] #f #Hf #H destruct
- elim (IH … Hf Hij) -f1 -f2 -IH /2 width=2 by ex_intro/
- | elim (at_inv_nxn … H) -H [1,4: * |*: // ] #f2 #Hij #H destruct
+ elim (IH … Hf Hlk) -IH -Hf -Hlk /2 width=3 by ex2_intro/
+ | elim (rm_nat_inv_nxn … H) -H [1,4: * |*: // ] #f2 #Hlk #H destruct
[ elim (coafter_inv_ppx … Hg) -Hg [|*: // ] #f #Hf #H destruct
- elim (IH … Hf Hij) -f1 -f2 -i /2 width=2 by ex_intro/
+ elim (IH … Hf Hlk) -IH -Hf -Hlk /2 width=3 by ex2_intro/
| elim (coafter_inv_nxx … Hg) -Hg [|*: // ] #f #Hf #H destruct
- elim (IH … Hf Hij) -f1 -f2 -i /2 width=2 by ex_intro/
+ elim (IH … Hf Hlk) -IH -Hf -Hlk /2 width=3 by ex2_intro/
]
]
]
(* Properties with iterated tail ********************************************)
-lemma coafter_tls: ∀j,i,f1,f2,f. @❪i, f1❫ ≘ j →
- f1 ~⊚ f2 ≘ f → ⫱*[j]f1 ~⊚ ⫱*[i]f2 ≘ ⫱*[j]f.
-#j elim j -j [ #i | #j #IH * [| #i ] ] #f1 #f2 #f #Hf1 #Hf
-[ elim (at_inv_xxp … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 destruct //
-| elim (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
+lemma coafter_tls: ∀l2,l1,f1,f2,f. @↑❪l1, f1❫ ≘ l2 →
+ f1 ~⊚ f2 ≘ f → ⫱*[l2]f1 ~⊚ ⫱*[l1]f2 ≘ ⫱*[l2]f.
+#l2 @(nat_ind_succ … l2) -l2 [ #l1 | #l2 #IH * [| #l1 ] ] #f1 #f2 #f #Hf1 #Hf
+[ elim (rm_nat_inv_xxp … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 destruct //
+| elim (rm_nat_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
elim (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
lapply (IH … Hg1 Hg) -IH -Hg1 -Hg //
-| elim (at_inv_nxn … Hf1) -Hf1 [1,4: * |*: // ] #g1 #Hg1 #H1
+| elim (rm_nat_inv_xxn … Hf1) -Hf1 [1,3: * |*: // ] #g1 [ #k1 ] #Hg1 [ #H ] #H1
[ elim (coafter_inv_pxx … Hf … H1) -Hf * #g2 #g #Hg #H2 #H0 destruct
lapply (IH … Hg1 Hg) -IH -Hg1 -Hg #H //
| elim (coafter_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
]
qed.
-lemma coafter_tls_O: ∀n,f1,f2,f. @❪0, f1❫ ≘ n →
- f1 ~⊚ f2 ≘ f → ⫱*[n]f1 ~⊚ f2 ≘ ⫱*[n]f.
+lemma coafter_tls_O: ∀k,f1,f2,f. @↑❪𝟎, f1❫ ≘ k →
+ f1 ~⊚ f2 ≘ f → ⫱*[k]f1 ~⊚ f2 ≘ ⫱*[k]f.
/2 width=1 by coafter_tls/ qed.
+(* Note: this does not require ↑ first and second j *)
lemma coafter_tls_succ: ∀g2,g1,g. g2 ~⊚ g1 ≘ g →
- ∀n. @❪0, g2❫ ≘ n → ⫱*[↑n]g2 ~⊚ ⫱g1 ≘ ⫱*[↑n]g.
-#g2 #g1 #g #Hg #n #Hg2
+ ∀j. @❪𝟏, g2❫ ≘ j → ⫱*[j]g2 ~⊚ ⫱g1 ≘ ⫱*[j]g.
+#g2 #g1 #g #Hg #j #Hg2
+lapply (rm_nat_pred_bi … Hg2) -Hg2 #Hg2
lapply (coafter_tls … Hg2 … Hg) -Hg #Hg
lapply (at_pxx_tls … Hg2) -Hg2 #H
elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
-elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct
-<tls_S <tls_S <H2 <H0 -g2 -g -n //
+elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0
+>(npsucc_pred j) <tls_S <tls_S //
qed.
-
-lemma coafter_fwd_xpx_pushs: ∀g2,f1,g,i,j. @❪i, g2❫ ≘ j → g2 ~⊚ ⫯*[↑i]f1 ≘ g →
- ∃∃f. ⫱*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[↑j]f = g.
-#g2 #g1 #g #i #j #Hg2 <pushs_xn #Hg
-elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
+(*
+lemma coafter_fwd_xpx_pushs: ∀g2,f1,g,i,j. @❪i, g2❫ ≘ j → g2 ~⊚ ⫯*[i]⫯f1 ≘ g →
+ ∃∃f. ⫱*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j]⫯f = g.
+#g2 #g1 #g #i #j #Hg2 <pushs_xn #Hg(coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs <tls_pushs #Hf
lapply (at_inv_tls … Hg2) -Hg2 #H
lapply (coafter_eq_repl_fwd2 … Hf … H) -H -Hf #Hf
elim (coafter_inv_pnx … Hf) [|*: // ] -Hf #g #Hg #H destruct
/2 width=3 by ex2_intro/
qed-.
-
+*)
(* Properties with test for identity ****************************************)
corec lemma coafter_isid_sn: ∀f1. 𝐈❪f1❫ → ∀f2. f1 ~⊚ f2 ≘ f2.
lemma coafter_isid_inv_dx: ∀f1,f2,f. f1 ~⊚ f2 ≘ f → 𝐈❪f2❫ → 𝐈❪f❫.
/4 width=4 by eq_id_isid, coafter_isid_dx, coafter_mono/ qed-.
-(* Properties with test for uniform relocations *****************************)
-
-lemma coafter_isuni_isid: ∀f2. 𝐈❪f2❫ → ∀f1. 𝐔❪f1❫ → f1 ~⊚ f2 ≘ f2.
-#f #Hf #g #H elim H -g
-/3 width=5 by coafter_isid_sn, coafter_eq_repl_back0, coafter_next, eq_push_inv_isid/
-qed.
-
-
-(*
-lemma coafter_isid_isuni: ∀f1,f2. 𝐈❪f2❫ → 𝐔❪f1❫ → f1 ~⊚ ↑f2 ≘ ↑f1.
-#f1 #f2 #Hf2 #H elim H -H
-/5 width=7 by coafter_isid_dx, coafter_eq_repl_back2, coafter_next, coafter_push, eq_push_inv_isid/
-qed.
-
-lemma coafter_uni_next2: ∀f2. 𝐔❪f2❫ → ∀f1,f. ↑f2 ~⊚ f1 ≘ f → f2 ~⊚ ↑f1 ≘ f.
-#f2 #H elim H -f2
-[ #f2 #Hf2 #f1 #f #Hf
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H0 destruct
- /4 width=7 by coafter_isid_inv_sn, coafter_isid_sn, coafter_eq_repl_back0, eq_next/
-| #f2 #_ #g2 #H2 #IH #f1 #f #Hf
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H0 destruct
- /3 width=5 by coafter_next/
-]
-qed.
-*)
-
-(* Properties with uniform relocations **************************************)
-
-lemma coafter_uni_sn: ∀i,f. 𝐔❨i❩ ~⊚ f ≘ ⫯*[i] f.
-#i elim i -i /2 width=5 by coafter_isid_sn, coafter_next/
-qed.
-
-(*
-lemma coafter_uni: ∀n1,n2. 𝐔❨n1❩ ~⊚ 𝐔❨n2❩ ≘ 𝐔❨n1+n2❩.
-@nat_elim2
-/4 width=5 by coafter_uni_next2, coafter_isid_sn, coafter_isid_dx, coafter_next/
-qed.
-
-(* Forward lemmas on at *****************************************************)
-
-lemma coafter_at_fwd: ∀i,i1,f. @❪i1, f❫ ≘ i → ∀f2,f1. f2 ~⊚ f1 ≘ f →
- ∃∃i2. @❪i1, f1❫ ≘ i2 & @❪i2, f2❫ ≘ i.
-#i elim i -i [2: #i #IH ] #i1 #f #Hf #f2 #f1 #Hf21
-[ elim (at_inv_xxn … Hf) -Hf [1,3:* |*: // ]
- [1: #g #j1 #Hg #H0 #H |2,4: #g #Hg #H ]
-| elim (at_inv_xxp … Hf) -Hf //
- #g #H1 #H
-]
-[2: elim (coafter_inv_xxn … Hf21 … H) -f *
- [ #g2 #g1 #Hg21 #H2 #H1 | #g2 #Hg21 #H2 ]
-|*: elim (coafter_inv_xxp … Hf21 … H) -f
- #g2 #g1 #Hg21 #H2 #H1
-]
-[4: -Hg21 |*: elim (IH … Hg … Hg21) -g -IH ]
-/3 width=9 by at_refl, at_push, at_next, ex2_intro/
-qed-.
-
-lemma coafter_fwd_at: ∀i,i2,i1,f1,f2. @❪i1, f1❫ ≘ i2 → @❪i2, f2❫ ≘ i →
- ∀f. f2 ~⊚ f1 ≘ f → @❪i1, f❫ ≘ i.
-#i elim i -i [2: #i #IH ] #i2 #i1 #f1 #f2 #Hf1 #Hf2 #f #Hf
-[ elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- #g2 [ #j2 ] #Hg2 [ #H22 ] #H20
- [ elim (at_inv_xxn … Hf1 … H22) -i2 *
- #g1 [ #j1 ] #Hg1 [ #H11 ] #H10
- [ elim (coafter_inv_ppx … Hf … H20 H10) -f1 -f2 /3 width=7 by at_push/
- | elim (coafter_inv_pnx … Hf … H20 H10) -f1 -f2 /3 width=6 by at_next/
- ]
- | elim (coafter_inv_nxx … Hf … H20) -f2 /3 width=7 by at_next/
- ]
-| elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H22 #H20
- elim (at_inv_xxp … Hf1 … H22) -i2 #g1 #H11 #H10
- elim (coafter_inv_ppx … Hf … H20 H10) -f1 -f2 /2 width=2 by at_refl/
-]
-qed-.
-
-lemma coafter_fwd_at2: ∀f,i1,i. @❪i1, f❫ ≘ i → ∀f1,i2. @❪i1, f1❫ ≘ i2 →
- ∀f2. f2 ~⊚ f1 ≘ f → @❪i2, f2❫ ≘ i.
-#f #i1 #i #Hf #f1 #i2 #Hf1 #f2 #H elim (coafter_at_fwd … Hf … H) -f
-#j1 #H #Hf2 <(at_mono … Hf1 … H) -i1 -i2 //
-qed-.
-
-lemma coafter_fwd_at1: ∀i,i2,i1,f,f2. @❪i1, f❫ ≘ i → @❪i2, f2❫ ≘ i →
- ∀f1. f2 ~⊚ f1 ≘ f → @❪i1, f1❫ ≘ i2.
-#i elim i -i [2: #i #IH ] #i2 #i1 #f #f2 #Hf #Hf2 #f1 #Hf1
-[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
- #g [ #j1 ] #Hg [ #H01 ] #H00
- elim (at_inv_xxn … Hf2) -Hf2 [1,3,5,7: * |*: // ]
- #g2 [1,3: #j2 ] #Hg2 [1,2: #H22 ] #H20
- [ elim (coafter_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=7 by at_push/
- | elim (coafter_inv_pxn … Hf1 … H20 H00) -f2 -f /3 width=5 by at_next/
- | elim (coafter_inv_nxp … Hf1 … H20 H00)
- | /4 width=9 by coafter_inv_nxn, at_next/
- ]
-| elim (at_inv_xxp … Hf) -Hf // #g #H01 #H00
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H21 #H20
- elim (coafter_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=2 by at_refl/
-]
-qed-.
-
-(* Properties with at *******************************************************)
-
-lemma coafter_uni_dx: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. f2 ~⊚ 𝐔❨i1❩ ≘ f → 𝐔❨i2❩ ~⊚ ⫱*[i2] f2 ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- lapply (coafter_isid_inv_dx … Hf ?) -Hf
- /3 width=3 by coafter_isid_sn, coafter_eq_repl_back0/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct
- elim (coafter_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- /3 width=5 by coafter_next/
- | #g2 #Hg2 #H2 destruct
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- /3 width=5 by coafter_next/
- ]
-]
-qed.
-
-lemma coafter_uni_sn: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. 𝐔❨i2❩ ~⊚ ⫱*[i2] f2 ≘ f → f2 ~⊚ 𝐔❨i1❩ ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- lapply (coafter_isid_inv_sn … Hf ?) -Hf
- /3 width=3 by coafter_isid_dx, coafter_eq_repl_back0/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct /3 width=7 by coafter_push/
- | #g2 #Hg2 #H2 destruct /3 width=5 by coafter_next/
- ]
-]
-qed-.
-
-lemma coafter_uni_succ_dx: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. f2 ~⊚ 𝐔❨↑i1❩ ≘ f → 𝐔❨↑i2❩ ~⊚ ⫱*[↑i2] f2 ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- elim (coafter_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H
- lapply (coafter_isid_inv_dx … Hg ?) -Hg
- /4 width=5 by coafter_isid_sn, coafter_eq_repl_back0, coafter_next/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct
- elim (coafter_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- /3 width=5 by coafter_next/
- | #g2 #Hg2 #H2 destruct
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- /3 width=5 by coafter_next/
- ]
-]
-qed.
-
-lemma coafter_uni_succ_sn: ∀i2,i1,f2. @❪i1, f2❫ ≘ i2 →
- ∀f. 𝐔❨↑i2❩ ~⊚ ⫱*[↑i2] f2 ≘ f → f2 ~⊚ 𝐔❨↑i1❩ ≘ f.
-#i2 elim i2 -i2
-[ #i1 #f2 #Hf2 #f #Hf
- elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H1 #H2 destruct
- elim (coafter_inv_nxx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
- lapply (coafter_isid_inv_sn … Hg ?) -Hg
- /4 width=7 by coafter_isid_dx, coafter_eq_repl_back0, coafter_push/
-| #i2 #IH #i1 #f2 #Hf2 #f #Hf
- elim (coafter_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
- elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
- [ #g2 #j1 #Hg2 #H1 #H2 destruct <tls_xn in Hg; /3 width=7 by coafter_push/
- | #g2 #Hg2 #H2 destruct <tls_xn in Hg; /3 width=5 by coafter_next/
- ]
-]
-qed-.
-
-lemma coafter_uni_one_dx: ∀f2,f. ⫯f2 ~⊚ 𝐔❨↑O❩ ≘ f → 𝐔❨↑O❩ ~⊚ f2 ≘ f.
-#f2 #f #H @(coafter_uni_succ_dx … (⫯f2)) /2 width=3 by at_refl/
-qed.
-
-lemma coafter_uni_one_sn: ∀f1,f. 𝐔❨↑O❩ ~⊚ f1 ≘ f → ⫯f1 ~⊚ 𝐔❨↑O❩ ≘ f.
-/3 width=3 by coafter_uni_succ_sn, at_refl/ qed-.
-*)
(* Forward lemmas with istot ************************************************)
-(*
-lemma coafter_istot_fwd: ∀f2,f1,f. f2 ~⊚ f1 ≘ f → 𝐓❪f2❫ → 𝐓❪f1❫ → 𝐓❪f❫.
-#f2 #f1 #f #Hf #Hf2 #Hf1 #i1 elim (Hf1 i1) -Hf1
-#i2 #Hf1 elim (Hf2 i2) -Hf2
-/3 width=7 by coafter_fwd_at, ex_intro/
-qed-.
-
-lemma coafter_fwd_istot_dx: ∀f2,f1,f. f2 ~⊚ f1 ≘ f → 𝐓❪f❫ → 𝐓❪f1❫.
-#f2 #f1 #f #H #Hf #i1 elim (Hf i1) -Hf
-#i2 #Hf elim (coafter_at_fwd … Hf … H) -f /2 width=2 by ex_intro/
-qed-.
-lemma coafter_fwd_istot_sn: ∀f2,f1,f. f2 ~⊚ f1 ≘ f → 𝐓❪f❫ → 𝐓❪f2❫.
-#f2 #f1 #f #H #Hf #i1 elim (Hf i1) -Hf
-#i #Hf elim (coafter_at_fwd … Hf … H) -f
-#i2 #Hf1 #Hf2 lapply (at_increasing … Hf1) -f1
-#Hi12 elim (at_le_ex … Hf2 … Hi12) -i2 /2 width=2 by ex_intro/
-qed-.
-
-lemma coafter_inv_istot: ∀f2,f1,f. f2 ~⊚ f1 ≘ f → 𝐓❪f❫ → 𝐓❪f2❫ ∧ 𝐓❪f1❫.
-/3 width=4 by coafter_fwd_istot_sn, coafter_fwd_istot_dx, conj/ qed-.
-
-lemma coafter_at1_fwd: ∀f1,i1,i2. @❪i1, f1❫ ≘ i2 → ∀f2. 𝐓❪f2❫ → ∀f. f2 ~⊚ f1 ≘ f →
- ∃∃i. @❪i2, f2❫ ≘ i & @❪i1, f❫ ≘ i.
-#f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2
-/3 width=8 by coafter_fwd_at, ex2_intro/
-qed-.
-
-lemma coafter_fwd_isid_sn: ∀f2,f1,f. 𝐓❪f❫ → f2 ~⊚ f1 ≘ f → f1 ≡ f → 𝐈❪f2❫.
-#f2 #f1 #f #H #Hf elim (coafter_inv_istot … Hf H) -H
-#Hf2 #Hf1 #H @isid_at_total // -Hf2
-#i2 #i #Hf2 elim (Hf1 i2) -Hf1
-#i0 #Hf1 lapply (at_increasing … Hf1)
-#Hi20 lapply (coafter_fwd_at2 … i0 … Hf1 … Hf) -Hf
-/3 width=7 by at_eq_repl_back, at_mono, at_id_le/
-qed-.
-
-lemma coafter_fwd_isid_dx: ∀f2,f1,f. 𝐓❪f❫ → f2 ~⊚ f1 ≘ f → f2 ≡ f → 𝐈❪f1❫.
-#f2 #f1 #f #H #Hf elim (coafter_inv_istot … Hf H) -H
-#Hf2 #Hf1 #H2 @isid_at_total // -Hf1
-#i1 #i2 #Hi12 elim (coafter_at1_fwd … Hi12 … Hf) -f1
-/3 width=8 by at_inj, at_eq_repl_back/
-qed-.
-*)
-corec fact coafter_inj_O_aux: ∀f1. @❪0, f1❫ ≘ 0 → H_coafter_inj f1.
+corec fact coafter_inj_O_aux: ∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_coafter_inj f1.
#f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
cases (at_inv_pxp … H1f1) -H1f1 [ |*: // ] #g1 #H1
lapply (istot_inv_push … H2f1 … H1) -H2f1 #H2g1
-cases (H2g1 0) #n #Hn
+cases (H2g1 (𝟏)) #n #Hn
cases (coafter_inv_pxx … H1f … H1) -H1f * #g21 #g #H1g #H21 #H
[ cases (coafter_inv_pxp … H2f … H1 H) -f1 -f #g22 #H2g #H22
@(eq_push … H21 H22) -f21 -f22
| cases (coafter_inv_pxn … H2f … H1 H) -f1 -f #g22 #H2g #H22
@(eq_next … H21 H22) -f21 -f22
]
-@(coafter_inj_O_aux (⫱*[n]g1) … (⫱*[n]g)) -coafter_inj_O_aux
+@(coafter_inj_O_aux (⫱*[↓n]g1) … (⫱*[↓n]g)) -coafter_inj_O_aux
/2 width=1 by coafter_tls, istot_tls, at_pxx_tls/
qed-.
-fact coafter_inj_aux: (∀f1. @❪0, f1❫ ≘ 0 → H_coafter_inj f1) →
- ∀i2,f1. @❪0, f1❫ ≘ i2 → H_coafter_inj f1.
+fact coafter_inj_aux: (∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_coafter_inj f1) →
+ ∀i2,f1. @❪𝟏, f1❫ ≘ i2 → H_coafter_inj f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #H1g1 #H1
qed-.
theorem coafter_inj: ∀f1. H_coafter_inj f1.
-#f1 #H cases (H 0) /3 width=7 by coafter_inj_aux, coafter_inj_O_aux/
+#f1 #H cases (H (𝟏)) /3 width=7 by coafter_inj_aux, coafter_inj_O_aux/
qed-.
-corec fact coafter_fwd_isid2_O_aux: ∀f1. @❪0, f1❫ ≘ 0 →
+corec fact coafter_fwd_isid2_O_aux: ∀f1. @❪𝟏, f1❫ ≘ 𝟏 →
H_coafter_fwd_isid2 f1.
#f1 #H1f1 #f2 #f #H #H2f1 #Hf
cases (at_inv_pxp … H1f1) -H1f1 [ |*: // ] #g1 #H1
lapply (istot_inv_push … H2f1 … H1) -H2f1 #H2g1
-cases (H2g1 0) #n #Hn
+cases (H2g1 (𝟏)) #n #Hn
cases (coafter_inv_pxx … H … H1) -H * #g2 #g #H #H2 #H0
[ lapply (isid_inv_push … Hf … H0) -Hf #Hg
@(isid_push … H2) -H2
]
qed-.
-fact coafter_fwd_isid2_aux: (∀f1. @❪0, f1❫ ≘ 0 → H_coafter_fwd_isid2 f1) →
- ∀i2,f1. @❪0, f1❫ ≘ i2 → H_coafter_fwd_isid2 f1.
+fact coafter_fwd_isid2_aux: (∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_coafter_fwd_isid2 f1) →
+ ∀i2,f1. @❪𝟏, f1❫ ≘ i2 → H_coafter_fwd_isid2 f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
qed-.
lemma coafter_fwd_isid2: ∀f1. H_coafter_fwd_isid2 f1.
-#f1 #f2 #f #Hf #H cases (H 0)
+#f1 #f2 #f #Hf #H cases (H (𝟏))
/3 width=7 by coafter_fwd_isid2_aux, coafter_fwd_isid2_O_aux/
qed-.
-fact coafter_isfin2_fwd_O_aux: ∀f1. @❪0, f1❫ ≘ 0 →
+fact coafter_isfin2_fwd_O_aux: ∀f1. @❪𝟏, f1❫ ≘ 𝟏 →
H_coafter_isfin2_fwd f1.
#f1 #Hf1 #f2 #H
generalize in match Hf1; generalize in match f1; -f1
#f2 #_ #IH #f1 #H #Hf1 #f #Hf
elim (at_inv_pxp … H) -H [ |*: // ] #g1 #H1
lapply (istot_inv_push … Hf1 … H1) -Hf1 #Hg1
-elim (Hg1 0) #n #Hn
+elim (Hg1 (𝟏)) #n #Hn
[ elim (coafter_inv_ppx … Hf) | elim (coafter_inv_pnx … Hf)
] -Hf [1,6: |*: // ] #g #Hg #H0 destruct
/5 width=6 by isfin_next, isfin_push, isfin_inv_tls, istot_tls, at_pxx_tls, coafter_tls_O/
qed-.
-fact coafter_isfin2_fwd_aux: (∀f1. @❪0, f1❫ ≘ 0 → H_coafter_isfin2_fwd f1) →
- ∀i2,f1. @❪0, f1❫ ≘ i2 → H_coafter_isfin2_fwd f1.
+fact coafter_isfin2_fwd_aux: (∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_coafter_isfin2_fwd f1) →
+ ∀i2,f1. @❪𝟏, f1❫ ≘ i2 → H_coafter_isfin2_fwd f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #f2 #Hf2 #H2f1 #f #Hf
elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
qed-.
lemma coafter_isfin2_fwd: ∀f1. H_coafter_isfin2_fwd f1.
-#f1 #f2 #Hf2 #Hf1 cases (Hf1 0)
+#f1 #f2 #Hf2 #Hf1 cases (Hf1 (𝟏))
/3 width=7 by coafter_isfin2_fwd_aux, coafter_isfin2_fwd_O_aux/
qed-.
/3 width=11 by coafter_refl, coafter_push, sor_np, sor_pn, sor_nn, ex3_2_intro/
]
qed-.
-
-(* Properties with after ****************************************************)
-(*
-corec theorem coafter_trans1: ∀f0,f3,f4. f0 ~⊚ f3 ≘ f4 →
- ∀f1,f2. f1 ~⊚ f2 ≘ f0 →
- ∀f. f2 ~⊚ f3 ≘ f → f1 ~⊚ f ≘ f4.
-#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4
-[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
- cases (coafter_inv_xxp … Hg0 … H0) -g0
- #f1 #f2 #Hf0 #H1 #H2
- cases (coafter_inv_ppx … Hg … H2 H3) -g2 -g3
- #f #Hf #H /3 width=7 by coafter_refl/
-| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
- cases (coafter_inv_xxp … Hg0 … H0) -g0
- #f1 #f2 #Hf0 #H1 #H2
- cases (coafter_inv_pnx … Hg … H2 H3) -g2 -g3
- #f #Hf #H /3 width=7 by coafter_push/
-| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg
- cases (coafter_inv_xxn … Hg0 … H0) -g0 *
- [ #f1 #f2 #Hf0 #H1 #H2
- cases (coafter_inv_nxx … Hg … H2) -g2
- #f #Hf #H /3 width=7 by coafter_push/
- | #f1 #Hf0 #H1 /3 width=6 by coafter_next/
- ]
-]
-qed-.
-
-corec theorem coafter_trans2: ∀f1,f0,f4. f1 ~⊚ f0 ≘ f4 →
- ∀f2, f3. f2 ~⊚ f3 ≘ f0 →
- ∀f. f1 ~⊚ f2 ≘ f → f ~⊚ f3 ≘ f4.
-#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4
-[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
- cases (coafter_inv_xxp … Hg0 … H0) -g0
- #f2 #f3 #Hf0 #H2 #H3
- cases (coafter_inv_ppx … Hg … H1 H2) -g1 -g2
- #f #Hf #H /3 width=7 by coafter_refl/
-| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
- cases (coafter_inv_xxn … Hg0 … H0) -g0 *
- [ #f2 #f3 #Hf0 #H2 #H3
- cases (coafter_inv_ppx … Hg … H1 H2) -g1 -g2
- #f #Hf #H /3 width=7 by coafter_push/
- | #f2 #Hf0 #H2
- cases (coafter_inv_pnx … Hg … H1 H2) -g1 -g2
- #f #Hf #H /3 width=6 by coafter_next/
- ]
-| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg
- cases (coafter_inv_nxx … Hg … H1) -g1
- #f #Hg #H /3 width=6 by coafter_next/
-]
-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/relocation/rtmap_uni.ma".
+include "ground/relocation/rtmap_coafter.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+(* Properties with test for uniform relocations *****************************)
+
+lemma coafter_isuni_isid: ∀f2. 𝐈❪f2❫ → ∀f1. 𝐔❪f1❫ → f1 ~⊚ f2 ≘ f2.
+#f #Hf #g #H elim H -g
+/3 width=5 by coafter_isid_sn, coafter_eq_repl_back0, coafter_next, eq_push_inv_isid/
+qed.
+
+(* Properties with uniform relocations **************************************)
+
+lemma coafter_uni_sn: ∀n,f. 𝐔❨n❩ ~⊚ f ≘ ⫯*[n] f.
+#n @(nat_ind_succ … n) -n
+/2 width=5 by coafter_isid_sn, coafter_next/
+qed.
(* RELOCATION MAP ***********************************************************)
inductive fcla: relation2 rtmap nat ≝
-| fcla_isid: ∀f. 𝐈❪f❫ → fcla f 0
+| fcla_isid: ∀f. 𝐈❪f❫ → fcla f (𝟎)
| fcla_push: ∀f,n. fcla f n → fcla (⫯f) n
| fcla_next: ∀f,n. fcla f n → fcla (↑f) (↑n)
.
lemma cla_inv_nn: ∀g,m. 𝐂❪g❫ ≘ m → ∀f,n. ↑f = g → ↑n = m → 𝐂❪f❫ ≘ n.
#g #m #H #f #n #H1 #H2 elim (fcla_inv_nx … H … H1) -g
-#x #Hf #H destruct //
+#x #Hf #H destruct <(eq_inv_nsucc_bi … H) -n //
qed-.
-lemma cla_inv_np: ∀g,m. 𝐂❪g❫ ≘ m → ∀f. ↑f = g → 0 = m → ⊥.
+lemma cla_inv_np: ∀g,m. 𝐂❪g❫ ≘ m → ∀f. ↑f = g → 𝟎 = m → ⊥.
#g #m #H #f #H1 elim (fcla_inv_nx … H … H1) -g
-#x #_ #H1 #H2 destruct
+#x #_ #H1 #H2 destruct /2 width=2 by eq_inv_zero_nsucc/
qed-.
-lemma fcla_inv_xp: ∀g,m. 𝐂❪g❫ ≘ m → 0 = m → 𝐈❪g❫.
+lemma fcla_inv_xp: ∀g,m. 𝐂❪g❫ ≘ m → 𝟎 = m → 𝐈❪g❫.
#g #m #H elim H -g -m /3 width=3 by isid_push/
-#g #m #_ #_ #H destruct
+#g #m #_ #_ #H destruct elim (eq_inv_zero_nsucc … H)
qed-.
-lemma fcla_inv_isid: ∀f,n. 𝐂❪f❫ ≘ n → 𝐈❪f❫ → 0 = n.
+lemma fcla_inv_isid: ∀f,n. 𝐂❪f❫ ≘ n → 𝐈❪f❫ → 𝟎 = n.
#f #n #H elim H -f -n /3 width=3 by isid_inv_push/
#f #n #_ #_ #H elim (isid_inv_next … H) -H //
qed-.
[ /2 width=3 by fcla_inv_isid/
| /3 width=3 by fcla_inv_px/
| #f #n1 #_ #IH #n2 #H elim (fcla_inv_nx … H) -H [2,3 : // ]
- #g #Hf #H destruct /3 width=1 by eq_f/
+ #g #Hf #H destruct >IH //
]
qed-.
(* *)
(**************************************************************************)
-include "ground/relocation/nstream_id.ma".
+include "ground/relocation/pstream_id.ma".
include "ground/relocation/rtmap_isid.ma".
(* RELOCATION MAP ***********************************************************)
(* Properties with iterated next ********************************************)
lemma isdiv_nexts: ∀n,f. 𝛀❪f❫ → 𝛀❪↑*[n]f❫.
-#n elim n -n /3 width=3 by isdiv_next/
+#n @(nat_ind_succ … n) -n /3 width=3 by isdiv_next/
qed.
(* Inversion lemmas with iterated next **************************************)
lemma isdiv_inv_nexts: ∀n,g. 𝛀❪↑*[n]g❫ → 𝛀❪g❫.
-#n elim n -n /3 width=3 by isdiv_inv_next/
+#n @(nat_ind_succ … n) -n /3 width=3 by isdiv_inv_next/
qed.
(* Properties with tail *****************************************************)
(* Properties with iterated tail ********************************************)
lemma isdiv_tls: ∀n,g. 𝛀❪g❫ → 𝛀❪⫱*[n]g❫.
-#n elim n -n /3 width=1 by isdiv_tl/
+#n @(nat_ind_succ … n) -n /3 width=1 by isdiv_tl/
qed.
(* Properties with iterated push ********************************************)
lemma isfin_pushs: ∀n,f. 𝐅❪f❫ → 𝐅❪⫯*[n]f❫.
-#n elim n -n /3 width=3 by isfin_push/
+#n @(nat_ind_succ … n) -n /3 width=3 by isfin_push/
qed.
(* Inversion lemmas with iterated push **************************************)
lemma isfin_inv_pushs: ∀n,g. 𝐅❪⫯*[n]g❫ → 𝐅❪g❫.
-#n elim n -n /3 width=3 by isfin_inv_push/
+#n @(nat_ind_succ … n) -n /3 width=3 by isfin_inv_push/
qed.
(* Properties with tail *****************************************************)
(* Inversion lemmas with iterated tail **************************************)
lemma isfin_inv_tls: ∀n,f. 𝐅❪⫱*[n]f❫ → 𝐅❪f❫.
-#n elim n -n /3 width=1 by isfin_inv_tl/
+#n @(nat_ind_succ … n) -n /3 width=1 by isfin_inv_tl/
qed-.
(* Properties with iterated push ********************************************)
lemma isid_pushs: ∀n,f. 𝐈❪f❫ → 𝐈❪⫯*[n]f❫.
-#n elim n -n /3 width=3 by isid_push/
+#n @(nat_ind_succ … n) -n /3 width=3 by isid_push/
qed.
(* Inversion lemmas with iterated push **************************************)
lemma isid_inv_pushs: ∀n,g. 𝐈❪⫯*[n]g❫ → 𝐈❪g❫.
-#n elim n -n /3 width=3 by isid_inv_push/
+#n @(nat_ind_succ … n) -n /3 width=3 by isid_inv_push/
qed.
(* Properties with tail *****************************************************)
(* Properties with iterated tail ********************************************)
lemma isid_tls: ∀n,g. 𝐈❪g❫ → 𝐈❪⫱*[n]g❫.
-#n elim n -n /3 width=1 by isid_tl/
+#n @(nat_ind_succ … n) -n /3 width=1 by isid_tl/
qed.
(* *)
(**************************************************************************)
-include "ground/notation/relations/istotal_1.ma".
+include "ground/notation/relations/ist_1.ma".
include "ground/relocation/rtmap_at.ma".
(* RELOCATION MAP ***********************************************************)
definition istot: predicate rtmap ≝ λf. ∀i. ∃j. @❪i,f❫ ≘ j.
interpretation "test for totality (rtmap)"
- 'IsTotal f = (istot f).
+ 'IsT f = (istot f).
(* Basic inversion lemmas ***************************************************)
(* Properties on tls ********************************************************)
lemma istot_tls: ∀n,f. 𝐓❪f❫ → 𝐓❪⫱*[n]f❫.
-#n elim n -n /3 width=1 by istot_tl/
+#n @(nat_ind_succ … n) -n //
+#n #IH #f #Hf <tls_S
+/3 width=1 by istot_tl/
qed.
(* Main forward lemmas on at ************************************************)
#Hf1 #Hf2 #Hi
[ @(eq_push … H1 H2) @at_ext -at_ext /2 width=3 by istot_inv_push/ -Hf1 -Hf2
#i #i1 #i2 #Hg1 #Hg2 lapply (Hi (↑i) (↑i1) (↑i2) ??) /2 width=7 by at_push/
-| cases (Hf2 0) -Hf1 -Hf2 -at_ext
+| cases (Hf2 (𝟏)) -Hf1 -Hf2 -at_ext
#j2 #Hf2 cases (at_increasing_strict … Hf2 … H2) -H2
- lapply (Hi 0 0 j2 … Hf2) /2 width=2 by at_refl/ -Hi -Hf2 -H1
- #H2 #H cases (lt_le_false … H) -H //
-| cases (Hf1 0) -Hf1 -Hf2 -at_ext
+ lapply (Hi (𝟏) (𝟏) j2 … Hf2) /2 width=2 by at_refl/ -Hi -Hf2 -H1
+ #H2 #H cases (plt_ge_false … H) -H //
+| cases (Hf1 (𝟏)) -Hf1 -Hf2 -at_ext
#j1 #Hf1 cases (at_increasing_strict … Hf1 … H1) -H1
- lapply (Hi 0 j1 0 Hf1 ?) /2 width=2 by at_refl/ -Hi -Hf1 -H2
- #H1 #H cases (lt_le_false … H) -H //
+ lapply (Hi (𝟏) j1 (𝟏) Hf1 ?) /2 width=2 by at_refl/ -Hi -Hf1 -H2
+ #H1 #H cases (plt_ge_false … H) -H //
| @(eq_next … H1 H2) @at_ext -at_ext /2 width=3 by istot_inv_next/ -Hf1 -Hf2
#i #i1 #i2 #Hg1 #Hg2 lapply (Hi i (↑i1) (↑i2) ??) /2 width=5 by at_next/
]
lemma at_dec: ∀f,i1,i2. 𝐓❪f❫ → Decidable (@❪i1,f❫ ≘ i2).
#f #i1 #i2 #Hf lapply (Hf i1) -Hf *
-#j2 #Hf elim (eq_nat_dec i2 j2)
+#j2 #Hf elim (eq_pnat_dec i2 j2)
[ #H destruct /2 width=1 by or_introl/
| /4 width=6 by at_mono, or_intror/
]
qed-.
-lemma is_at_dec_le: ∀f,i2,i. 𝐓❪f❫ → (∀i1. i1 + i ≤ i2 → @❪i1,f❫ ≘ i2 → ⊥) →
- Decidable (∃i1. @❪i1,f❫ ≘ i2).
-#f #i2 #i #Hf elim i -i
-[ #Ht @or_intror * /3 width=3 by at_increasing/
-| #i #IH #Ht elim (at_dec f (i2-i) i2) /3 width=2 by ex_intro, or_introl/
- #Hi2 @IH -IH #i1 #H #Hi elim (le_to_or_lt_eq … H) -H /2 width=3 by/
- #H destruct -Ht /2 width=1 by/
-]
-qed-.
-
lemma is_at_dec: ∀f,i2. 𝐓❪f❫ → Decidable (∃i1. @❪i1,f❫ ≘ i2).
-#f #i2 #Hf @(is_at_dec_le ?? (↑i2)) /2 width=4 by lt_le_false/
+#f #i2 #Hf
+lapply (dec_plt (λi1.@❪i1,f❫ ≘ i2) … (↑i2)) [| * ]
+[ /2 width=1 by at_dec/
+| * /3 width=2 by ex_intro, or_introl/
+| #H @or_intror * #i1 #Hi12
+ /5 width=3 by at_increasing, plt_succ_dx, ex2_intro/
+]
qed-.
(* Advanced properties on isid **********************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/notation/relations/ratsucc_3.ma".
+include "ground/arith/nat_lt_pred.ma".
+include "ground/relocation/rtmap_at.ma".
+
+(* NON-NEGATIVE APPLICATION FOR RELOCATION MAPS *****************************)
+
+definition rm_nat: relation3 rtmap nat nat ≝
+ λf,l1,l2. @❪↑l1,f❫ ≘ ↑l2.
+
+interpretation
+ "relational non-negative application (relocation maps)"
+ 'RAtSucc l1 f l2 = (rm_nat f l1 l2).
+
+(* Basic properties *********************************************************)
+
+lemma rm_nat_refl (f) (g) (k1) (k2):
+ (⫯f) = g → 𝟎 = k1 → 𝟎 = k2 → @↑❪k1,g❫ ≘ k2.
+#f #g #k1 #k2 #H1 #H2 #H3 destruct
+/2 width=2 by at_refl/
+qed.
+
+lemma rm_nat_push (f) (l1) (l2) (g) (k1) (k2):
+ @↑❪l1,f❫ ≘ l2 → ⫯f = g → ↑l1 = k1 → ↑l2 = k2 → @↑❪k1,g❫ ≘ k2.
+#f #l1 #l2 #g #k1 #k2 #Hf #H1 #H2 #H3 destruct
+/2 width=7 by at_push/
+qed.
+
+lemma rm_nat_next (f) (l1) (l2) (g) (k2):
+ @↑❪l1,f❫ ≘ l2 → ↑f = g → ↑l2 = k2 → @↑❪l1,g❫ ≘ k2.
+#f #l1 #l2 #g #k2 #Hf #H1 #H2 destruct
+/2 width=5 by at_next/
+qed.
+
+lemma rm_nat_pred_bi (f) (i1) (i2):
+ @❪i1,f❫ ≘ i2 → @↑❪↓i1,f❫ ≘ ↓i2.
+#f #i1 #i2
+>(npsucc_pred i1) in ⊢ (%→?); >(npsucc_pred i2) in ⊢ (%→?);
+//
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma rm_nat_inv_ppx (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g. 𝟎 = l1 → ⫯g = f → 𝟎 = l2.
+#f #l1 #l2 #H #g #H1 #H2 destruct
+lapply (at_inv_ppx … H ???) -H
+/2 width=2 by eq_inv_npsucc_bi/
+qed-.
+
+lemma rm_nat_inv_npx (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f →
+ ∃∃k2. @↑❪k1,g❫ ≘ k2 & ↑k2 = l2.
+#f #l1 #l2 #H #g #k1 #H1 #H2 destruct
+elim (at_inv_npx … H) -H [|*: // ] #k2 #Hg
+>(npsucc_pred (↑l2)) #H
+@(ex2_intro … (↓k2)) //
+<pnpred_psucc //
+qed-.
+
+lemma rm_nat_inv_xnx (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g. ↑g = f →
+ ∃∃k2. @↑❪l1,g❫ ≘ k2 & ↑k2 = l2.
+#f #l1 #l2 #H #g #H1 destruct
+elim (at_inv_xnx … H) -H [|*: // ] #k2
+>(npsucc_pred (k2)) in ⊢ (%→?→?); #Hg #H
+@(ex2_intro … (↓k2)) //
+<pnpred_psucc //
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma rm_nat_inv_ppn (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g,k2. 𝟎 = l1 → ⫯g = f → ↑k2 = l2 → ⊥.
+#f #l1 #l2 #Hf #g #k2 #H1 #H <(rm_nat_inv_ppx … Hf … H1 H) -f -g -l1 -l2
+/2 width=3 by eq_inv_nsucc_zero/
+qed-.
+
+lemma rm_nat_inv_npp (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g,k1. ↑k1 = l1 → ⫯g = f → 𝟎 = l2 → ⊥.
+#f #l1 #l2 #Hf #g #k1 #H1 #H elim (rm_nat_inv_npx … Hf … H1 H) -f -l1
+#x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/
+qed-.
+
+lemma rm_nat_inv_npn (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g,k1,k2. ↑k1 = l1 → ⫯g = f → ↑k2 = l2 → @↑❪k1,g❫ ≘ k2.
+#f #l1 #l2 #Hf #g #k1 #k2 #H1 #H elim (rm_nat_inv_npx … Hf … H1 H) -f -l1
+#x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 //
+qed-.
+
+lemma rm_nat_inv_xnp (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g. ↑g = f → 𝟎 = l2 → ⊥.
+#f #l1 #l2 #Hf #g #H elim (rm_nat_inv_xnx … Hf … H) -f
+#x2 #Hg * -l2 /2 width=3 by eq_inv_zero_nsucc/
+qed-.
+
+lemma rm_nat_inv_xnn (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g,k2. ↑g = f → ↑k2 = l2 → @↑❪l1,g❫ ≘ k2.
+#f #l1 #l2 #Hf #g #k2 #H elim (rm_nat_inv_xnx … Hf … H) -f
+#x2 #Hg * -l2 #H >(eq_inv_nsucc_bi … H) -k2 //
+qed-.
+
+lemma rm_nat_inv_pxp (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → 𝟎 = l1 → 𝟎 = l2 → ∃g. ⫯g = f.
+#f elim (pn_split … f) * /2 width=2 by ex_intro/
+#g #H #l1 #l2 #Hf #H1 #H2 cases (rm_nat_inv_xnp … Hf … H H2)
+qed-.
+
+lemma rm_nat_inv_pxn (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀k2. 𝟎 = l1 → ↑k2 = l2 →
+ ∃∃g. @↑❪l1,g❫ ≘ k2 & ↑g = f.
+#f elim (pn_split … f) *
+#g #H #l1 #l2 #Hf #k2 #H1 #H2
+[ elim (rm_nat_inv_ppn … Hf … H1 H H2)
+| /3 width=5 by rm_nat_inv_xnn, ex2_intro/
+]
+qed-.
+
+lemma rm_nat_inv_nxp (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀k1. ↑k1 = l1 → 𝟎 = l2 → ⊥.
+#f elim (pn_split f) *
+#g #H #l1 #l2 #Hf #k1 #H1 #H2
+[ elim (rm_nat_inv_npp … Hf … H1 H H2)
+| elim (rm_nat_inv_xnp … Hf … H H2)
+]
+qed-.
+
+lemma rm_nat_inv_nxn (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀k1,k2. ↑k1 = l1 → ↑k2 = l2 →
+ ∨∨ ∃∃g. @↑❪k1,g❫ ≘ k2 & ⫯g = f
+ | ∃∃g. @↑❪l1,g❫ ≘ k2 & ↑g = f.
+#f elim (pn_split f) *
+/4 width=7 by rm_nat_inv_xnn, rm_nat_inv_npn, ex2_intro, or_intror, or_introl/
+qed-.
+
+(* Note: the following inversion lemmas must be checked *)
+lemma rm_nat_inv_xpx (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g. ⫯g = f →
+ ∨∨ ∧∧ 𝟎 = l1 & 𝟎 = l2
+ | ∃∃k1,k2. @↑❪k1,g❫ ≘ k2 & ↑k1 = l1 & ↑k2 = l2.
+#f * [2: #l1 ] #l2 #Hf #g #H
+[ elim (rm_nat_inv_npx … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
+| >(rm_nat_inv_ppx … Hf … H) -f /3 width=1 by conj, or_introl/
+]
+qed-.
+
+lemma rm_nat_inv_xpp (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g. ⫯g = f → 𝟎 = l2 → 𝟎 = l1.
+#f #l1 #l2 #Hf #g #H elim (rm_nat_inv_xpx … Hf … H) -f * //
+#k1 #k2 #_ #_ * -l2 #H elim (eq_inv_zero_nsucc … H)
+qed-.
+
+lemma rm_nat_inv_xpn (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → ∀g,k2. ⫯g = f → ↑k2 = l2 →
+ ∃∃k1. @↑❪k1,g❫ ≘ k2 & ↑k1 = l1.
+#f #l1 #l2 #Hf #g #k2 #H elim (rm_nat_inv_xpx … Hf … H) -f *
+[ #_ * -l2 #H elim (eq_inv_nsucc_zero … H)
+| #x1 #x2 #Hg #H1 * -l2 #H
+ lapply (eq_inv_nsucc_bi … H) -H #H destruct
+ /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma rm_nat_inv_xxp (f) (l1) (l2):
+ @↑❪l1,f❫ ≘ l2 → 𝟎 = l2 → ∃∃g. 𝟎 = l1 & ⫯g = f.
+#f elim (pn_split f) *
+#g #H #l1 #l2 #Hf #H2
+[ /3 width=6 by rm_nat_inv_xpp, ex2_intro/
+| elim (rm_nat_inv_xnp … Hf … H H2)
+]
+qed-.
+
+lemma rm_nat_inv_xxn (f) (l1) (l2): @↑❪l1,f❫ ≘ l2 → ∀k2. ↑k2 = l2 →
+ ∨∨ ∃∃g,k1. @↑❪k1,g❫ ≘ k2 & ↑k1 = l1 & ⫯g = f
+ | ∃∃g. @↑❪l1,g❫ ≘ k2 & ↑g = f.
+#f elim (pn_split f) *
+#g #H #l1 #l2 #Hf #k2 #H2
+[ elim (rm_nat_inv_xpn … Hf … H H2) -l2 /3 width=5 by or_introl, ex3_2_intro/
+| lapply (rm_nat_inv_xnn … Hf … H H2) -l2 /3 width=3 by or_intror, ex2_intro/
+]
+qed-.
+
+(* Main destructions ********************************************************)
+
+theorem rm_nat_monotonic (k2) (l2) (f):
+ @↑❪l2,f❫ ≘ k2 → ∀k1,l1. @↑❪l1,f❫ ≘ k1 → l1 < l2 → k1 < k2.
+#k2 @(nat_ind_succ … k2) -k2
+[ #l2 #f #H2f elim (rm_nat_inv_xxp … H2f) -H2f //
+ #g #H21 #_ #k1 #l1 #_ #Hi destruct
+ elim (nlt_inv_zero_dx … Hi)
+| #k2 #IH #l2 #f #H2f #k1 @(nat_ind_succ … k1) -k1 //
+ #k1 #_ #l1 #H1f #Hl elim (nlt_inv_gen … Hl)
+ #_ #Hl2 elim (rm_nat_inv_nxn … H2f (↓l2)) -H2f [1,3: * |*: // ]
+ #g #H2g #H
+ [ elim (rm_nat_inv_xpn … H1f … H) -f
+ /4 width=8 by nlt_inv_succ_bi, nlt_succ_bi/
+ | /4 width=8 by rm_nat_inv_xnn, nlt_succ_bi/
+ ]
+]
+qed-.
+
+theorem rm_nat_inv_monotonic (k1) (l1) (f):
+ @↑❪l1,f❫ ≘ k1 → ∀k2,l2. @↑❪l2,f❫ ≘ k2 → k1 < k2 → l1 < l2.
+#k1 @(nat_ind_succ … k1) -k1
+[ #l1 #f #H1f elim (rm_nat_inv_xxp … H1f) -H1f //
+ #g * -l1 #H #k2 #l2 #H2f #Hk
+ lapply (nlt_des_gen … Hk) -Hk #H22
+ elim (rm_nat_inv_xpn … H2f … (↓k2) H) -f //
+| #k1 #IH #l1 @(nat_ind_succ … l1) -l1
+ [ #f #H1f elim (rm_nat_inv_pxn … H1f) -H1f [ |*: // ]
+ #g #H1g #H #k2 #l2 #H2f #Hj elim (nlt_inv_succ_sn … Hj) -Hj
+ /3 width=7 by rm_nat_inv_xnn/
+ | #l1 #_ #f #H1f #k2 #l2 #H2f #Hj elim (nlt_inv_succ_sn … Hj) -Hj
+ #Hj #H22 elim (rm_nat_inv_nxn … H1f) -H1f [1,4: * |*: // ]
+ #g #Hg #H
+ [ elim (rm_nat_inv_xpn … H2f … (↓k2) H) -f
+ /3 width=7 by nlt_succ_bi/
+ | /3 width=7 by rm_nat_inv_xnn/
+ ]
+ ]
+]
+qed-.
+
+theorem rm_nat_mono (f) (l) (l1) (l2):
+ @↑❪l,f❫ ≘ l1 → @↑❪l,f❫ ≘ l2 → l2 = l1.
+#f #l #l1 #l2 #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) //
+#Hi elim (nlt_ge_false l l) /3 width=6 by rm_nat_inv_monotonic, eq_sym/
+qed-.
+
+theorem rm_nat_inj (f) (l1) (l2) (l):
+ @↑❪l1,f❫ ≘ l → @↑❪l2,f❫ ≘ l → l1 = l2.
+#f #l1 #l2 #l #H1 #H2 elim (nat_split_lt_eq_gt l2 l1) //
+#Hi elim (nlt_ge_false l l) /2 width=6 by rm_nat_monotonic/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.tcs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground/arith/nat_plus.ma".
+include "ground/relocation/rtmap_uni.ma".
+include "ground/relocation/rtmap_nat.ma".
+
+(* NON-NEGATIVE APPLICATION FOR RELOCATION MAPS *****************************)
+
+(* Properties with uniform relocations **************************************)
+
+lemma rm_nat_uni (n) (l): @↑❪l,𝐔❨n❩❫ ≘ l+n.
+#n @(nat_ind_succ … n) -n /2 width=5 by rm_nat_next/
+qed.
+
+(* Inversion lemmas with uniform relocations ********************************)
+
+lemma rm_nat_inv_uni (n) (l) (k): @↑❪l,𝐔❨n❩❫ ≘ k → k = l+n.
+/2 width=4 by rm_nat_mono/ qed-.
(**************************************************************************)
include "ground/notation/functions/uparrowstar_2.ma".
+include "ground/arith/nat_succ_iter.ma".
include "ground/relocation/rtmap_eq.ma".
(* RELOCATION MAP ***********************************************************)
-rec definition nexts (f:rtmap) (n:nat) on n: rtmap ≝ match n with
-[ O ⇒ f | S m ⇒ ↑(nexts f m) ].
+definition nexts (f:rtmap) (n:nat) ≝ next^n f.
interpretation "nexts (rtmap)" 'UpArrowStar n f = (nexts f n).
+(* Basic properties *********************************************************)
+
+lemma nexts_O: ∀f. f = ↑*[𝟎] f.
+// qed.
+
+lemma nexts_S: ∀f,n. ↑↑*[n] f = ↑*[↑n] f.
+#f #n @(niter_succ … next)
+qed.
+
+lemma nexts_eq_repl: ∀n. eq_repl (λf1,f2. ↑*[n] f1 ≡ ↑*[n] f2).
+#n @(nat_ind_succ … n) -n /3 width=5 by eq_next/
+qed.
+
+(* Advanced properties ******************************************************)
+
+lemma nexts_swap: ∀f,n. ↑↑*[n] f = ↑*[n] ↑f.
+#f #n @(niter_appl … next)
+qed.
+
+lemma nexts_xn: ∀n,f. ↑*[n] ↑f = ↑*[↑n] f.
+// qed.
+
(* Basic_inversion lemmas *****************************************************)
lemma eq_inv_nexts_sn: ∀n,f1,g2. ↑*[n] f1 ≡ g2 →
∃∃f2. f1 ≡ f2 & ↑*[n] f2 = g2.
-#n elim n -n /2 width=3 by ex2_intro/
+#n @(nat_ind_succ … n) -n /2 width=3 by ex2_intro/
#n #IH #f1 #g2 #H elim (eq_inv_nx … H) -H [|*: // ]
#f0 #Hf10 #H1 elim (IH … Hf10) -IH -Hf10 #f2 #Hf12 #H2 destruct
/2 width=3 by ex2_intro/
lemma eq_inv_nexts_dx: ∀n,f2,g1. g1 ≡ ↑*[n] f2 →
∃∃f1. f1 ≡ f2 & ↑*[n] f1 = g1.
-#n elim n -n /2 width=3 by ex2_intro/
+#n @(nat_ind_succ … n) -n /2 width=3 by ex2_intro/
#n #IH #f2 #g1 #H elim (eq_inv_xn … H) -H [|*: // ]
#f0 #Hf02 #H1 elim (IH … Hf02) -IH -Hf02 #f1 #Hf12 #H2 destruct
/2 width=3 by ex2_intro/
qed-.
-
-(* Basic properties *********************************************************)
-
-lemma nexts_O: ∀f. f = ↑*[0] f.
-// qed.
-
-lemma nexts_S: ∀f,n. ↑↑*[n] f = ↑*[↑n] f.
-// qed.
-
-lemma nexts_eq_repl: ∀n. eq_repl (λf1,f2. ↑*[n] f1 ≡ ↑*[n] f2).
-#n elim n -n /3 width=5 by eq_next/
-qed.
-
-(* Advanced properties ******************************************************)
-
-lemma nexts_xn: ∀n,f. ↑*[n] ↑f = ↑*[↑n] f.
-#n elim n -n //
-qed.
(**************************************************************************)
include "ground/notation/functions/upspoonstar_2.ma".
+include "ground/arith/nat_succ_iter.ma".
include "ground/relocation/rtmap_eq.ma".
(* RELOCATION MAP ***********************************************************)
-rec definition pushs (f:rtmap) (n:nat) on n: rtmap ≝ match n with
-[ O ⇒ f | S m ⇒ ⫯(pushs f m) ].
+definition pushs (f:rtmap) (n:nat) ≝ push^n f.
interpretation "pushs (rtmap)" 'UpSpoonStar n f = (pushs f n).
+(* Basic properties *********************************************************)
+
+lemma pushs_O: ∀f. f = ⫯*[𝟎] f.
+// qed.
+
+lemma pushs_S: ∀f,n. ⫯⫯*[n] f = ⫯*[↑n] f.
+#f #n @(niter_succ … push)
+qed.
+
+lemma pushs_eq_repl: ∀n. eq_repl (λf1,f2. ⫯*[n] f1 ≡ ⫯*[n] f2).
+#n @(nat_ind_succ … n) -n /3 width=5 by eq_push/
+qed.
+
+(* Advanced properties ******************************************************)
+
+lemma push_swap (n) (f): ⫯⫯*[n] f = ⫯*[n] ⫯f.
+#n #f @(niter_appl … push)
+qed.
+
+lemma pushs_xn: ∀n,f. ⫯*[n] ⫯f = ⫯*[↑n] f.
+// qed.
+
(* Basic_inversion lemmas *****************************************************)
lemma eq_inv_pushs_sn: ∀n,f1,g2. ⫯*[n] f1 ≡ g2 →
∃∃f2. f1 ≡ f2 & ⫯*[n] f2 = g2.
-#n elim n -n /2 width=3 by ex2_intro/
+#n @(nat_ind_succ … n) -n /2 width=3 by ex2_intro/
#n #IH #f1 #g2 #H elim (eq_inv_px … H) -H [|*: // ]
#f0 #Hf10 #H1 elim (IH … Hf10) -IH -Hf10 #f2 #Hf12 #H2 destruct
/2 width=3 by ex2_intro/
lemma eq_inv_pushs_dx: ∀n,f2,g1. g1 ≡ ⫯*[n] f2 →
∃∃f1. f1 ≡ f2 & ⫯*[n] f1 = g1.
-#n elim n -n /2 width=3 by ex2_intro/
+#n @(nat_ind_succ … n) -n /2 width=3 by ex2_intro/
#n #IH #f2 #g1 #H elim (eq_inv_xp … H) -H [|*: // ]
#f0 #Hf02 #H1 elim (IH … Hf02) -IH -Hf02 #f1 #Hf12 #H2 destruct
/2 width=3 by ex2_intro/
qed-.
-
-(* Basic properties *********************************************************)
-
-lemma pushs_O: ∀f. f = ⫯*[0] f.
-// qed.
-
-lemma pushs_S: ∀f,n. ⫯⫯*[n] f = ⫯*[↑n] f.
-// qed.
-
-lemma pushs_eq_repl: ∀n. eq_repl (λf1,f2. ⫯*[n] f1 ≡ ⫯*[n] f2).
-#n elim n -n /3 width=5 by eq_push/
-qed.
-
-(* Advanced properties ******************************************************)
-
-lemma pushs_xn: ∀n,f. ⫯*[n] ⫯f = ⫯*[↑n] f.
-#n elim n -n //
-qed.
/3 width=5 by sle_push, sle_next, sle_weak/
qed-.
-(* Properties with iteraded push ********************************************)
+(* Properties with iterated push ********************************************)
-lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀i. ⫯*[i] f1 ⊆ ⫯*[i] f2.
-#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_push/
+lemma sle_pushs: ∀f1,f2. f1 ⊆ f2 → ∀n. ⫯*[n] f1 ⊆ ⫯*[n] f2.
+#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n
+/2 width=5 by sle_push/
qed.
(* Properties with tail *****************************************************)
(* Properties with iteraded tail ********************************************)
-lemma sle_tls: ∀f1,f2. f1 ⊆ f2 → ∀i. ⫱*[i] f1 ⊆ ⫱*[i] f2.
-#f1 #f2 #Hf12 #i elim i -i /2 width=5 by sle_tl/
+lemma sle_tls: ∀f1,f2. f1 ⊆ f2 → ∀n. ⫱*[n] f1 ⊆ ⫱*[n] f2.
+#f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n
+/2 width=5 by sle_tl/
qed.
(* Properties with isid *****************************************************)
(* *)
(**************************************************************************)
+include "ground/xoa/or_3.ma".
+include "ground/xoa/ex_3_1.ma".
include "ground/xoa/ex_4_2.ma".
include "ground/notation/relations/runion_3.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_le_max.ma".
include "ground/relocation/rtmap_isfin.ma".
include "ground/relocation/rtmap_sle.ma".
lemma sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≘ f →
∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≘ ⫱*[n]f.
-#f1 #f2 #f #Hf #n elim n -n /2 width=1 by sor_tl/
+#f1 #f2 #f #Hf #n @(nat_ind_succ … n) -n
+/2 width=1 by sor_tl/
qed.
(* Properies with test for identity *****************************************)
∃∃f,n. f1 ⋓ f2 ≘ f & 𝐂❪f❫ ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
#f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by sor_isid_sn, ex4_2_intro/
#f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by fcla_push, fcla_next, ex4_2_intro, sor_isid_dx/
-#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <plus_n_Sm ] (**) (* full auto fails *)
-[ /3 width=7 by fcla_next, sor_pn, max_S2_le_S, le_S_S, ex4_2_intro/
-| /4 width=7 by fcla_next, sor_nn, le_S, le_S_S, ex4_2_intro/
+#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (**) (* full auto fails *)
+[ /3 width=7 by fcla_next, sor_pn, nle_max_sn_succ_dx, nle_succ_bi, ex4_2_intro/
+| /4 width=7 by fcla_next, sor_nn, nle_succ_dx, nle_succ_bi, ex4_2_intro/
| /3 width=7 by fcla_push, sor_pp, ex4_2_intro/
-| /3 width=7 by fcla_next, sor_np, max_S1_le_S, le_S_S, ex4_2_intro/
+| /3 width=7 by fcla_next, sor_np, nle_max_sn_succ_sn, nle_succ_bi, ex4_2_intro/
]
qed-.
elim (IH … Hf) -f /3 width=3 by fcla_push, ex2_intro/
| #f #n #_ #IH #f1 #f2 #H
elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g1 #g2 #Hf #H1 #H2 destruct
- elim (IH … Hf) -f /3 width=3 by fcla_push, fcla_next, le_S_S, le_S, ex2_intro/
+ elim (IH … Hf) -f /3 width=3 by fcla_push, fcla_next, nle_succ_bi, nle_succ_dx, ex2_intro/
]
qed-.
(* RELOCATION MAP ***********************************************************)
-rec definition tls (f:rtmap) (n:nat) on n: rtmap ≝ match n with
-[ O ⇒ f | S m ⇒ ⫱(tls f m) ].
+definition tls (f:rtmap) (n:nat) ≝ tl^n f.
interpretation "tls (rtmap)" 'DropPreds n f = (tls f n).
(* Basic properties *********************************************************)
-lemma tls_O: ∀f. f = ⫱*[0] f.
+lemma tls_O: ∀f. f = ⫱*[𝟎] f.
// qed.
lemma tls_S: ∀f,n. ⫱ ⫱*[n] f = ⫱*[↑n] f.
-// qed.
+#f #n @(niter_succ … tl)
+qed.
lemma tls_eq_repl: ∀n. eq_repl (λf1,f2. ⫱*[n] f1 ≡ ⫱*[n] f2).
-#n elim n -n /3 width=1 by tl_eq_repl/
+#n @(nat_ind_succ … n) -n /3 width=1 by tl_eq_repl/
qed.
(* Advanced properties ******************************************************)
-lemma tls_xn: ∀n,f. ⫱*[n] ⫱f = ⫱*[↑n] f.
-#n elim n -n //
+lemma tls_swap (n) (f): ⫱ ⫱*[n] f = ⫱*[n] ⫱f.
+#f #n @(niter_appl … tl)
qed.
+lemma tls_xn: ∀n,f. ⫱*[n] ⫱f = ⫱*[↑n] f.
+// qed.
+
(* Properties with pushs ****************************************************)
lemma tls_pushs: ∀n,f. f = ⫱*[n] ⫯*[n] f.
-#n elim n -n //
-#n #IH #f <tls_xn //
+#n @(nat_ind_succ … n) -n //
+#n #IH #f <tls_xn <pushs_S <tl_push_rew //
qed.
(**************************************************************************)
include "ground/notation/functions/uniform_1.ma".
+include "ground/relocation/rtmap_nexts.ma".
include "ground/relocation/rtmap_id.ma".
include "ground/relocation/rtmap_isuni.ma".
(* RELOCATION MAP ***********************************************************)
-rec definition uni (n:nat) on n: rtmap ≝ match n with
-[ O ⇒ 𝐈𝐝
-| S n ⇒ ↑(uni n)
-].
+definition uni (n) ≝ ↑*[n] 𝐈𝐝.
interpretation "uniform relocation (rtmap)"
'Uniform n = (uni n).
(* Basic properties *********************************************************)
-lemma uni_zero: 𝐈𝐝 = 𝐔❨0❩.
+lemma uni_zero: 𝐈𝐝 = 𝐔❨𝟎❩.
// qed.
lemma uni_succ: ∀n. ↑𝐔❨n❩ = 𝐔❨↑n❩.
-// qed.
+/2 width=1 by nexts_S/ qed.
(* Basic inversion lemmas ***************************************************)
-lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯f → 0 = n ∧ 𝐈𝐝 ≡ f.
-#f * /3 width=5 by eq_inv_pp, conj/
-#n <uni_succ #H elim (eq_inv_np … H) -H //
+lemma uni_inv_push_dx: ∀f,n. 𝐔❨n❩ ≡ ⫯f → 𝟎 = n ∧ 𝐈𝐝 ≡ f.
+#f #n @(nat_ind_succ … n) -n
+[ /3 width=5 by eq_inv_pp, conj/
+| #n #_ <uni_succ #H elim (eq_inv_np … H) -H //
+]
qed-.
-lemma uni_inv_push_sn: ∀f,n. ⫯f ≡ 𝐔❨n❩ → 0 = n ∧ 𝐈𝐝 ≡ f.
+lemma uni_inv_push_sn: ∀f,n. ⫯f ≡ 𝐔❨n❩ → 𝟎 = n ∧ 𝐈𝐝 ≡ f.
/3 width=1 by uni_inv_push_dx, eq_sym/ qed-.
-lemma uni_inv_id_dx: ∀n. 𝐔❨n❩ ≡ 𝐈𝐝 → 0 = n.
+lemma uni_inv_id_dx: ∀n. 𝐔❨n❩ ≡ 𝐈𝐝 → 𝟎 = n.
#n <id_rew #H elim (uni_inv_push_dx … H) -H //
qed-.
-lemma uni_inv_id_sn: ∀n. 𝐈𝐝 ≡ 𝐔❨n❩ → 0 = n.
+lemma uni_inv_id_sn: ∀n. 𝐈𝐝 ≡ 𝐔❨n❩ → 𝟎 = n.
/3 width=1 by uni_inv_id_dx, eq_sym/ qed-.
lemma uni_inv_next_dx: ∀f,n. 𝐔❨n❩ ≡ ↑f → ∃∃m. 𝐔❨m❩ ≡ f & ↑m = n.
-#f *
+#f #n @(nat_ind_succ … n) -n
[ <uni_zero <id_rew #H elim (eq_inv_pn … H) -H //
-| #n <uni_succ /3 width=5 by eq_inv_nn, ex2_intro/
+| #n #_ <uni_succ /3 width=5 by eq_inv_nn, ex2_intro/
]
qed-.
(* Properties with test for identity ****************************************)
-lemma uni_isid: ∀f. 𝐈❪f❫ → 𝐔❨0❩ ≡ f.
+lemma uni_isid: ∀f. 𝐈❪f❫ → 𝐔❨𝟎❩ ≡ f.
/2 width=1 by eq_id_inv_isid/ qed-.
(* Inversion lemmas with test for identity **********************************)
-lemma uni_inv_isid: ∀f. 𝐔❨0❩ ≡ f → 𝐈❪f❫.
+lemma uni_inv_isid: ∀f. 𝐔❨𝟎❩ ≡ f → 𝐈❪f❫.
/2 width=1 by eq_id_isid/ qed-.
(* Properties with finite colength assignment ***************************)
lemma fcla_uni: ∀n. 𝐂❪𝐔❨n❩❫ ≘ n.
-#n elim n -n /2 width=1 by fcla_isid, fcla_next/
+#n @(nat_ind_succ … n) -n
+/2 width=1 by fcla_isid, fcla_next/
qed.
(* Properties with test for finite colength ***************************)
(* Properties with test for uniformity **************************************)
lemma isuni_uni: ∀n. 𝐔❪𝐔❨n❩❫.
-#n elim n -n /3 width=3 by isuni_isid, isuni_next/
+#n @(nat_ind_succ … n) -n
+/3 width=3 by isuni_isid, isuni_next/
qed.
lemma uni_isuni: ∀f. 𝐔❪f❫ → ∃n. 𝐔❨n❩ ≡ f.
(* Inversion lemmas with test for uniformity ********************************)
lemma uni_inv_isuni: ∀n,f. 𝐔❨n❩ ≡ f → 𝐔❪f❫.
-#n elim n -n /3 width=1 by uni_inv_isid, isuni_isid/
-#n #IH #x <uni_succ #H elim (eq_inv_nx … H) -H /3 width=3 by isuni_next/
+#n @(nat_ind_succ … n) -n
+[ /3 width=1 by uni_inv_isid, isuni_isid/
+| #n #IH #x <uni_succ #H elim (eq_inv_nx … H) -H /3 width=3 by isuni_next/
+]
qed-.
[ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" "nat_le_max" * ]
[ "nat_max ( ?∨? )" * ]
[ "nat_minus ( ?-? )" "nat_minus_plus" * ]
- [ "nat_plus ( ?+? )" "nat_plus_pred" * ]
+ [ "nat_plus ( ?+? )" "nat_plus_pred" "nat_plus_rplus" * ]
+ [ "nat_rplus ( ?+? )" "nat_rplus_succ" * ]
[ "nat_pred ( ↓? )" "nat_pred_succ" * ]
[ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ]
[ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" *"nat_tri" ]
}
]
[ { "positive integers" * } {
+ [ "nat_lt ( ?<? )" "pnat_lt_pred" * ]
+ [ "pnat_le ( ?≤? )" "pnat_le_pred" "pnat_le_plus" * ]
[ "pnat_plus ( ?+? )" * ]
+ [ "nat_pred ( ↓? )" * ]
[ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" "pnat_tri" * ]
}
]
projects / helm.git / commitdiff