mrc: $(MRCS:%.mrc=recommGc%.ml)
@./mrc.native .
-recommGc%.ml recommGc%.mli: %.mrc mrc.ml
+recommGc%.ml recommGc%.mli: %.mrc mrc*.ml mrc*.mli
@./mrc.native $<
.PHONY: test mrc
--- /dev/null
+PcsAnd b "" true false
+niter
+ntri
+nsucc
+npred
+nplus
+nminus
+nmax
+nle
+nlt
+ysucc
+ypred
+yplus
+ylminus, yminus
+yle
+ylt
--- /dev/null
+PccFor d "" true false
+POSITIVE INTEGERS
+NON-NEGATIVE INTEGERS
+NON-NEGATIVE INTEGERS WITH INFINITY
+WELL-FOUNDED INDUCTION
+λδ-2A
+λδ-2B
let cap = String.capitalize_ascii
-let ok b =
- if b then "true" else "ok"
+let ko b =
+ if b then "KO" else "OO"
let write_mli name =
let file = name ^ ".mli" in
let iter hd words =
let lhs = List.map (Printf.sprintf "%S :: ") words in
let rhs = List.map (Printf.sprintf "%S :: ") hd in
- Printf.fprintf och " | %stl -> k %s (%souts) tl\n"
- (String.concat "" lhs) (ok st.ET.para) (String.concat "" rhs)
+ Printf.fprintf och " | %stl -> k T.OK (%souts) tl\n"
+ (String.concat "" lhs) (String.concat "" rhs)
in
match subst with
| [] -> ()
let write_component st =
let cmod = "recommGc" ^ st.ET.cmod in
let och = open_out (cmod ^ ".ml") in
+ Printf.fprintf och "module T = RecommTypes\n";
+ Printf.fprintf och "module R = Recomm%s\n" (cap st.ET.rmod);
if st.ET.dmod <> "" then begin
- Printf.fprintf och "module D = Recomm%s\n\n" (cap st.ET.dmod)
+ Printf.fprintf och "module D = Recomm%s\n" (cap st.ET.dmod)
+ end;
+ Printf.fprintf och "\n";
+ Printf.fprintf och "let step k st outs ins =\n";
+ if st.ET.para then begin
+ Printf.fprintf och " if st <> T.OO then k st outs ins else\n"
+ end else begin
+ Printf.fprintf och " if st = T.KO then k st outs ins else\n"
end;
- Printf.fprintf och "let step k ok outs ins =\n";
- Printf.fprintf och " if ok then k ok outs ins else\n";
Printf.fprintf och " match ins with\n";
List.iter (write_subst st och) st.ET.substs;
- Printf.fprintf och " | _ -> k %s outs ins\n\n" (ok st.ET.optn);
+ Printf.fprintf och " | _ -> k T.%s outs ins\n\n" (ko st.ET.optn);
Printf.fprintf och "let main =\n";
- Printf.fprintf och " Recomm%s.register_%s step\n" (cap st.ET.rmod) st.ET.rfun;
+ Printf.fprintf och " R.register_%s step\n" st.ET.rfun;
close_out och;
write_mli cmod
let cmod = Filename.concat st.ET.cdir "recommGc" in
let och = open_out (cmod ^ ".ml") in
let iter i name =
- Printf.fprintf och "module G%u = RecommGc%s\n" (succ i) name
+ Printf.fprintf och "module G%03u = RecommGc%s\n" (succ i) name
in
List.iteri iter st.ET.mods;
close_out och;
--- /dev/null
+PcsPar p "" true false
+(semigroup properties)
--- /dev/null
+PccFor r "" true false
+DISCRIMINATOR
+ITERATED FUNCTION
+TRICHOTOMY OPERATOR
+NAT-INJECTION
+SUCCESSOR
+PREDECESSOR
+ADDITION
+SUBTRACTION
+LEFT SUBTRACTION
+MAXIMUM, MAXIMUN
+ORDER
+STRICT ORDER
+ARITHMETICAL PROPERTIES
PccFor r "" true false
-ADDITION
-MAXIMUM, MAXIMUN
SHIFT
module P1 = RecommPccFor
module P2 = RecommPcsAnd
+module P3 = RecommPcsPar
module G = RecommGc
let s_line = ref ES.id
-let k_final b ws1 ws2 = b, ws1, ws2
+let k_final r ws1 ws2 = r, ws1, ws2
type status =
{
| _ -> true
let mute_o = [|
- "___ ";
- "||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 ";
+ " ";
+ " ___ ";
+ " ||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 ";
"";
|]
recomm tl @@ add hd @@ st
| ET.Title ss :: tl ->
if middle st then Printf.eprintf "middle: TITLE\n";
- let b, ss1, ss2 = !c_line k_final false [] ss in
+ let r, ss1, ss2 = !c_line k_final ET.OO [] ss in
let ss2 =
- if ss2 = [] then ss2 else "*" :: ss2
+ if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2
in
let ss = List.rev_append ss1 ss2 in
let s = String.concat " " ss in
recomm tl @@ add (ET.Title ss) @@ st
| ET.Slice ss :: tl ->
if middle st then Printf.eprintf "middle: Section\n";
- let b, ss1, ss2 = !s_line k_final false [] ss in
+ let r, ss1, ss2 = !s_line k_final ET.OO [] ss in
let ss2 =
- if ss2 = [] then ss2 else "*" :: ss2
+ if r <> ET.KO && ss2 = [] then ss2 else "*" :: ss2
in
let ss = List.rev_append ss1 ss2 in
let s = String.capitalize_ascii (String.concat " " ss) in
-module G1 = RecommGcbGroundCounters
-module G2 = RecommGcdGroundCounters
-module G3 = RecommGcrGroundCounters
-module G4 = RecommGcsAttr
-module G5 = RecommGcsMain
-module G6 = RecommGcsWith
+module G001 = RecommGcbGroundArith
+module G002 = RecommGcbGroundCounters
+module G003 = RecommGcdGroundArith
+module G004 = RecommGcdGroundCounters
+module G005 = RecommGcpGroundArith
+module G006 = RecommGcrGroundArith
+module G007 = RecommGcrGroundCounters
+module G008 = RecommGcsAttr
+module G009 = RecommGcsMain
+module G010 = RecommGcsWith
--- /dev/null
+module T = RecommTypes
+module R = RecommPcsAnd
+
+let step k st outs ins =
+ if st <> T.OO then k st outs ins else
+ match ins with
+ | "ylt" :: tl -> k T.OK ("ylt" :: outs) tl
+ | "yle" :: tl -> k T.OK ("yle" :: outs) tl
+ | "ylminus" :: tl -> k T.OK ("ylminus" :: outs) tl
+ | "yminus" :: tl -> k T.OK ("ylminus" :: outs) tl
+ | "yplus" :: tl -> k T.OK ("yplus" :: outs) tl
+ | "ypred" :: tl -> k T.OK ("ypred" :: outs) tl
+ | "ysucc" :: tl -> k T.OK ("ysucc" :: outs) tl
+ | "nlt" :: tl -> k T.OK ("nlt" :: outs) tl
+ | "nle" :: tl -> k T.OK ("nle" :: outs) tl
+ | "nmax" :: tl -> k T.OK ("nmax" :: outs) tl
+ | "nminus" :: tl -> k T.OK ("nminus" :: outs) tl
+ | "nplus" :: tl -> k T.OK ("nplus" :: outs) tl
+ | "npred" :: tl -> k T.OK ("npred" :: outs) tl
+ | "nsucc" :: tl -> k T.OK ("nsucc" :: outs) tl
+ | "ntri" :: tl -> k T.OK ("ntri" :: outs) tl
+ | "niter" :: tl -> k T.OK ("niter" :: outs) tl
+ | _ -> k T.OO outs ins
+
+let main =
+ R.register_b step
-let step k ok outs ins =
- if ok then k ok outs ins else
+module T = RecommTypes
+module R = RecommPcsAnd
+
+let step k st outs ins =
+ if st <> T.OO then k st outs ins else
match ins with
- | "rtc_plus" :: tl -> k true ("rtc_plus" :: outs) tl
- | "rtc_max" :: tl -> k true ("rtc_max" :: outs) tl
- | "rtc_shift" :: tl -> k true ("rtc_shift" :: outs) tl
- | _ -> k ok outs ins
+ | "rtc_plus" :: tl -> k T.OK ("rtc_plus" :: outs) tl
+ | "rtc_max" :: tl -> k T.OK ("rtc_max" :: outs) tl
+ | "rtc_shift" :: tl -> k T.OK ("rtc_shift" :: outs) tl
+ | _ -> k T.OO outs ins
let main =
- RecommPcsAnd.register_b step
+ R.register_b step
--- /dev/null
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+ if st <> T.OO then k st outs ins else
+ match ins with
+ | "\206\187\206\180-2B" :: tl -> k T.OK ("\206\187\206\180-2B" :: outs) tl
+ | "\206\187\206\180-2A" :: tl -> k T.OK ("\206\187\206\180-2A" :: outs) tl
+ | "WELL-FOUNDED" :: "INDUCTION" :: tl -> k T.OK ("INDUCTION" :: "WELL-FOUNDED" :: outs) tl
+ | "NON-NEGATIVE" :: "INTEGERS" :: "WITH" :: "INFINITY" :: tl -> k T.OK ("INFINITY" :: "WITH" :: "INTEGERS" :: "NON-NEGATIVE" :: outs) tl
+ | "NON-NEGATIVE" :: "INTEGERS" :: tl -> k T.OK ("INTEGERS" :: "NON-NEGATIVE" :: outs) tl
+ | "POSITIVE" :: "INTEGERS" :: tl -> k T.OK ("INTEGERS" :: "POSITIVE" :: outs) tl
+ | _ -> k T.OO outs ins
+
+let main =
+ R.register_d step
-let step k ok outs ins =
- if ok then k ok outs ins else
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+ if st <> T.OO then k st outs ins else
match ins with
- | "T-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "T-TRANSITION" :: outs) tl
- | "T-BOUND" :: "RT-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl
- | "RT-TRANSITION" :: "COUNTERS" :: tl -> k true ("COUNTERS" :: "RT-TRANSITION" :: outs) tl
- | _ -> k ok outs ins
+ | "T-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "T-TRANSITION" :: outs) tl
+ | "T-BOUND" :: "RT-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "RT-TRANSITION" :: "T-BOUND" :: outs) tl
+ | "RT-TRANSITION" :: "COUNTERS" :: tl -> k T.OK ("COUNTERS" :: "RT-TRANSITION" :: outs) tl
+ | _ -> k T.OO outs ins
let main =
- RecommPccFor.register_d step
+ R.register_d step
--- /dev/null
+module T = RecommTypes
+module R = RecommPcsPar
+
+let step k st outs ins =
+ if st <> T.OO then k st outs ins else
+ match ins with
+ | "(semigroup" :: "properties)" :: tl -> k T.OK ("properties)" :: "(semigroup" :: outs) tl
+ | _ -> k T.OO outs ins
+
+let main =
+ R.register_p step
--- /dev/null
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+ if st <> T.OO then k st outs ins else
+ match ins with
+ | "ARITHMETICAL" :: "PROPERTIES" :: tl -> k T.OK ("PROPERTIES" :: "ARITHMETICAL" :: outs) tl
+ | "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl
+ | "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl
+ | "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
+ | "MAXIMUN" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
+ | "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
+ | "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
+ | "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
+ | "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
+ | "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
+ | "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl
+ | "TRICHOTOMY" :: "OPERATOR" :: tl -> k T.OK ("OPERATOR" :: "TRICHOTOMY" :: outs) tl
+ | "ITERATED" :: "FUNCTION" :: tl -> k T.OK ("FUNCTION" :: "ITERATED" :: outs) tl
+ | "DISCRIMINATOR" :: tl -> k T.OK ("DISCRIMINATOR" :: outs) tl
+ | _ -> k T.OO outs ins
+
+let main =
+ R.register_r step
-let step k ok outs ins =
- if ok then k ok outs ins else
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+ if st <> T.OO then k st outs ins else
match ins with
- | "SHIFT" :: tl -> k true ("SHIFT" :: outs) tl
- | "MAXIMUM" :: tl -> k true ("MAXIMUM" :: outs) tl
- | "MAXIMUN" :: tl -> k true ("MAXIMUM" :: outs) tl
- | "ADDITION" :: tl -> k true ("ADDITION" :: outs) tl
- | _ -> k ok outs ins
+ | "SHIFT" :: tl -> k T.OK ("SHIFT" :: outs) tl
+ | _ -> k T.OO outs ins
let main =
- RecommPccFor.register_r step
+ R.register_r step
-let step k ok outs ins =
- if ok then k ok outs ins else
+module T = RecommTypes
+module R = RecommCheck
+
+let step k st outs ins =
+ if st = T.KO then k st outs ins else
match ins with
- | "main" :: tl -> k ok ("main" :: outs) tl
- | "basic" :: tl -> k ok ("basic" :: outs) tl
- | "advanced" :: tl -> k ok ("advanced" :: outs) tl
- | _ -> k ok outs ins
+ | "main" :: tl -> k T.OK ("main" :: outs) tl
+ | "helper" :: tl -> k T.OK ("helper" :: outs) tl
+ | "basic" :: tl -> k T.OK ("basic" :: outs) tl
+ | "advanced" :: tl -> k T.OK ("advanced" :: outs) tl
+ | _ -> k T.OO outs ins
let main =
- RecommCheck.register_s step
+ R.register_s step
+module T = RecommTypes
+module R = RecommCheck
module D = RecommGcsAttr
-let step k ok outs ins =
- if ok then k ok outs ins else
+let step k st outs ins =
+ if st = T.KO then k st outs ins else
match ins with
- | "eliminations" :: tl -> k ok ("eliminations" :: outs) tl
- | "eliminators" :: tl -> k ok ("eliminations" :: outs) tl
- | "destructions" :: tl -> k ok ("destructions" :: outs) tl
- | "forward" :: "properties" :: tl -> k ok ("destructions" :: outs) tl
- | "forward" :: "lemmas" :: tl -> k ok ("destructions" :: outs) tl
- | "inversions" :: tl -> k ok ("inversions" :: outs) tl
- | "inversion" :: "properties" :: tl -> k ok ("inversions" :: outs) tl
- | "inversion" :: "lemmas" :: tl -> k ok ("inversions" :: outs) tl
- | "constructions" :: tl -> k ok ("constructions" :: outs) tl
- | "properties" :: tl -> k ok ("constructions" :: outs) tl
- | _ -> k true outs ins
+ | "iterators" :: tl -> k T.OK ("iterators" :: outs) tl
+ | "eliminations" :: tl -> k T.OK ("eliminations" :: outs) tl
+ | "eliminators" :: tl -> k T.OK ("eliminations" :: outs) tl
+ | "equalities" :: tl -> k T.OK ("equalities" :: outs) tl
+ | "destructions" :: tl -> k T.OK ("destructions" :: outs) tl
+ | "forward" :: "properties" :: tl -> k T.OK ("destructions" :: outs) tl
+ | "forward" :: "lemmas" :: tl -> k T.OK ("destructions" :: outs) tl
+ | "inversions" :: tl -> k T.OK ("inversions" :: outs) tl
+ | "inversion" :: "properties" :: tl -> k T.OK ("inversions" :: outs) tl
+ | "inversion" :: "lemmas" :: tl -> k T.OK ("inversions" :: outs) tl
+ | "inversion" :: tl -> k T.OK ("inversions" :: outs) tl
+ | "constructions" :: tl -> k T.OK ("constructions" :: outs) tl
+ | "properties" :: tl -> k T.OK ("constructions" :: outs) tl
+ | _ -> k T.KO outs ins
let main =
- RecommCheck.register_s step
+ R.register_s step
+module T = RecommTypes
+module R = RecommCheck
module D = RecommGcsMain
-let step k ok outs ins =
- if ok then k ok outs ins else
+let step k st outs ins =
+ if st = T.KO then k st outs ins else
match ins with
- | "with" :: tl -> k ok ("with" :: outs) tl
- | _ -> k true outs ins
+ | "with" :: tl -> k T.OK ("with" :: outs) tl
+ | _ -> k T.OO outs ins
let main =
- RecommCheck.register_s step
+ R.register_s step
|]
let heads = [|
- "Advanved";
+ "Advanced";
"Basic";
"Constructions";
"Forward";
"Destructions";
"Eliminations";
"Eliminators";
+ "Equalities";
+ "Helper";
"Inversion";
"Inversions";
+ "Iterators";
"Main";
"Properties";
|]
let SP = " "
let NL = "\n"
let SR = "*"
-let OP = "(*" SP*
+let OP = "(*"
let CP = SR* "*)"
let PP = CP SP* OP
let WF = ['A'-'Z' 'a'-'z']
let replace = ref false
+let string_length_utf8 s =
+ let l = String.length s in
+ let rec aux r i =
+ if i >= l then r else
+ if '\x80' <= s.[i] && s.[i] <= '\xBF'
+ then aux (succ r) (succ i) else aux r (succ i)
+ in
+ l - aux 0 0
+
let complete s =
- let l = !width - String.length s - 6 in
+ let l = !width - string_length_utf8 s - 6 in
if l < 0 then begin
Printf.eprintf "overfull: %S\n" s;
""
| ET.Text s ->
Printf.fprintf och "%s" s
| ET.Mark s ->
- Printf.fprintf och "(* %s**)" s
+ Printf.fprintf och "(* *%s*)" s
| ET.Key (s1, s2) ->
Printf.fprintf och "(* %s%s*)" s1 s2
| ET.Title ss ->
%%
-inn_r:
+sp:
+ | { "" }
| SP { $1 }
+
+inn_r:
| NL { $1 }
| SW { $1 }
| OT { $1 }
inn:
| inn_r { $1 }
- | KW { $1 }
- | CW { $1 }
- | HW { $1 }
+ | SP { $1 }
+ | KW { $1 }
+ | CW { $1 }
+ | HW { $1 }
inns_r:
| inn_r { $1 }
| out { $1 }
| out outs { $1 ^ $2 }
-sw:
- | HW { lc $1 }
- | SW { lc $1 }
+cc:
+ | CW { $1 }
+ | OT { $1 }
+
+cw:
+ | cc { $1 }
+ | cc cw { $1 ^ $2 }
cws:
| { [] }
| SP { [] }
- | SP CW cws { $2 :: $3 }
+ | SP cw cws { $2 :: $3 }
+
+sc:
+ | HW { lc $1 }
+ | SW { lc $1 }
+ | OT { $1 }
+
+sw:
+ | sc { $1 }
+ | sc sw { $1 ^ $2 }
sws:
| { [] }
src_l:
| NL { ET.Line $1 }
- | OP PP inns CP { ET.Mark $3 }
- | OP KW inns CP { ET.Key ($2, $3) }
- | OP CW cws CP { ET.Title ($2 :: $3) }
- | OP HW sws CP { ET.Slice (lc $2 :: $3) }
- | OP CP { ET.Other ($1, "", $2) }
- | OP inns_r CP { ET.Other ($1, $2, $3) }
+ | 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 }
src:
| outs { ET.Text $1 }
module EC = RecommCheck
module ES = RecommStep
+module ET = RecommTypes
let d_line = ref ES.id
let r_line = ref ES.id
-let k_for k ok outs ins =
- if ok then begin
- match ins with
- | "FOR" :: tl -> !d_line k false ("FOR" :: outs) tl
- | _ -> k true outs ins
- end else begin
- k true outs ins
- end
-
-let k_or k ok outs ins =
- if ok then k ok outs ins else
- !r_line (k_for k) ok outs ins
-
-let step k ok outs ins =
- if ok then k ok outs ins else
- !d_line (k_or k) ok outs ins
+let k_exit k st out ins =
+ if st <> ET.OK then k ET.KO out ins else
+ k st out ins
+
+let k_for k st outs ins =
+ if st <> ET.OK then k ET.KO outs ins else
+ match ins with
+ | "FOR" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl
+ | _ -> k ET.KO outs ins
+
+let k_or k st outs ins =
+ if st <> ET.OO then k st outs ins else
+ !r_line (k_for k) st outs ins
+
+let step k st outs ins =
+ if st = ET.KO then k st outs ins else
+ !d_line (k_or k) ET.OO outs ins
let register_d =
ES.register d_line
module EC = RecommCheck
module ES = RecommStep
+module ET = RecommTypes
module D = RecommGcsWith
let b_line = ref ES.id
-let rec k_and k ok outs ins =
- if ok then begin
- match ins with
- | "and" :: tl -> step k false ("and" :: outs) tl
- | _ -> k true outs ins
- end else begin
- k true outs ins
- end
+let rec k_and k st outs ins =
+ if st <> ET.OK then k ET.KO outs ins else
+ match ins with
+ | "and" :: tl -> step k ET.OK ("and" :: outs) tl
+ | _ -> k ET.OK outs ins
-and step k ok outs ins =
- if ok then k ok outs ins else
- !b_line (k_and k) ok outs ins
+and step k st outs ins =
+ if st <> ET.OK then k st outs ins else
+ !b_line (k_and k) ET.OO outs ins
let register_b =
ES.register b_line
--- /dev/null
+module EC = RecommCheck
+module ES = RecommStep
+module ET = RecommTypes
+
+module D = RecommPcsAnd
+
+let p_line = ref ES.id
+
+let step k st outs ins =
+ if st = ET.KO then k st outs ins else
+ !p_line k ET.OO outs ins
+
+let register_p =
+ ES.register p_line
+
+let main =
+ EC.register_s step
--- /dev/null
+val register_p: RecommTypes.step -> unit
val id: ('s, 't) RecommTypes.astep
val register: ('s, 't) RecommTypes.astep ref -> ('s, 't) RecommTypes.astep -> unit
-
type ('s, 't) astep = ('s, 't) aproc -> ('s, 't) aproc
-type step = (bool, bool * words * words) astep
+type return = KO
+ | OK
+ | OO
+
+type step = (return, return * words * words) astep
check s "" false false
advanced
basic
+helper
main
check s "GcsAttr" false true
constructions, properties
-inversions, inversion properties, inversion lemmas
+inversions, inversion properties, inversion lemmas, inversion
destructions, forward properties, forward lemmas
+equalities
eliminations, eliminators
+iterators
-check s "GcsMain" false true
+check s "GcsMain" false false
with
include "ground/arith/nat_plus.ma".
include "ground/arith/nat_le.ma".
-(* ORDER FOR NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
-(* Constructions with nplus ***********************************************************)
+(* Constructions with nplus *************************************************)
(*** monotonic_le_plus_l *)
lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.
(*** max_SS *)
lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
#n1 #n2
-@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion gets in the way *)
+@trans_eq [3: @ntri_succ_bi | skip ] (* * rewrite fails because δ-expansion gets in the way *)
<ntri_f_tri //
qed.
/3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
qed.
-(* Advanved constructions (semigroup properties) ****************************)
+(* Advanced constructions (semigroup properties) ****************************)
(*** plus_S1 *)
lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
(*** commutative_plus *)
lemma nplus_comm: commutative … nplus.
#m @(nat_ind_succ … m) -m //
-qed-. (**) (* gets in the way with auto *)
+qed-. (* * gets in the way with auto *)
(*** associative_plus *)
lemma nplus_assoc: associative … nplus.
* //
qed.
-(* Inversion with nsucc *****************************************************)
+(* Inversions with nsucc ****************************************************)
(*** nat_split *)
lemma nat_split_zero_pos (n): ∨∨ 𝟎 = n | n = ↑↓n.
#m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
qed-.
-(* Basic inversions ***************************************************************)
+(* Basic inversions *********************************************************)
(*** injective_S *)
lemma eq_inv_nsucc_bi: injective … nsucc.
lemma pplus_comm: commutative … pplus.
#p elim p -p //
-qed-. (**) (* gets in the way with auto *)
+qed-. (* * gets in the way with auto *)
lemma pplus_assoc: associative … pplus.
#p #q #r elim r -r //
"infinity (non-negative integers with infinity)"
'Infinity = yinf.
-(* Inversion lemmas *********************************************************)
+(* Inversions ***************************************************************)
(* Note: destruct *)
(*** yinj_inj *)
#x #y #H destruct //
qed-.
-(* Basic properties *********************************************************)
+(* Basic constructions ******************************************************)
(*** eq_ynat_dec *)
lemma eq_ynat_dec (y1,y2:ynat): Decidable (y1 = y2).
(* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
-(* Constructions with yminus and yplus **************************************)
+(* Constructions with ylminus and yplus *************************************)
(*** yle_plus1_to_minus_inj2 *)
lemma yle_plus_sn_dx_lminus_dx (n) (x) (z):
x ≤ yinj_nat o + y → x - o ≤ y.
/2 width=1 by yle_plus_dx_dx_lminus_sn/ qed.
-(* Destructions with yminus and yplus ***************************************)
+(* Destructions with ylminus and yplus **************************************)
(*** yplus_minus_comm_inj *)
lemma ylminus_plus_comm_23 (n) (x) (z):
]
qed-.
-(* Inversions with yminus and yplus *****************************************)
+(* Inversions with ylminus and yplus ****************************************)
(*** yminus_plus *)
lemma yplus_lminus_sn_refl_sn (n) (x):
#n1 #m2 #x1 #y2 #Hnx1 #H12
lapply (yle_plus_bi_dx (yinj_nat m2) … Hnx1) >H12 #H
lapply (yle_inv_plus_bi_sn_inj … H) -H #Hmy2
-generalize in match H12; -H12 (**) (* rewrite in hyp *)
+generalize in match H12; -H12 (* * rewrite in hyp *)
>(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
lapply (eq_inv_yplus_bi_dx_inj … H) -H
>(yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H
(* Advanced constructions ***************************************************)
-(* yminus_O1 *)
+(*** yminus_O1 *)
lemma ylminus_zero_sn (n): 𝟎 = 𝟎 - n.
// qed.
(* Basic destructions *******************************************************)
-(* ylt_fwd_gen ylt_inv_Y2 *)
+(*** ylt_fwd_gen ylt_inv_Y2 *)
lemma ylt_des_gen_sn (x) (y):
x < y → ∃m. x = yinj_nat m.
#x #y * -x -y
(* Inversions with yle ******************************************************)
-(* ylt_yle_false *)
+(*** ylt_yle_false *)
lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥.
/3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-.
(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
-(* Cobstructions with yle and ylminus **************************************)
+(* Constructions with yle and ylminus ***************************************)
(*** monotonic_ylt_minus_dx *)
lemma ylt_lminus_bi_dx (o) (x) (y):
(* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
-(* Constructions with yle and ylminus and yplus ****************************)
+(* Constructions with yle and ylminus and yplus *****************************)
(*** ylt_plus2_to_minus_inj2 *)
lemma ylt_plus_dx_dx_lminus_sn (o) (x) (y):
x < ∞ → ↑x ≤ y → x < y.
/3 width=3 by ylt_yle_trans, ylt_succ_dx_refl/ qed.
-(* Inversions and destructions on yle ***************************************)
+(* Inversions with yle and ysucc ********************************************)
(*** ylt_inv_le *)
lemma ylt_inv_le_succ_sn (x) (y):
z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
#z #x1 #x2 #y1 #y2 #Hz
<yplus_plus_comm_23 <yplus_plus_comm_23 in ⊢ (???%→?); #H
-@(eq_inv_yplus_bi_dx … H) // (**) (* auto does not work *)
+@(eq_inv_yplus_bi_dx … H) // (* * auto does not work *)
qed-.
(*** ylt_inv_plus_Y *)
include "ground/arith/nat.ma".
include "ground/arith/ynat.ma".
-(* NON-NEGATIVE INTEGERS TO NON-NEGATIVE INTEGERS WITH INFINITY *************)
+(* NAT-INJECTION FOR NON-NEGATIVE INTEGERS WITH INFINITY ********************)
(*** yinj *)
definition yinj_nat (n) ≝ match n with
<nplus_succ_dx >ysucc_inj >ysucc_inj <yplus_succ_dx //
qed.
-(* Advaced constructions ****************************************************)
+(* Advanced constructions ***************************************************)
(*** ysucc_iter_Y yplus_Y1 *)
lemma yplus_inf_sn (x): ∞ = ∞ + x.
#x @(ynat_split_nat_inf … x) -x //
qed.
-(* Inversion with ysucc *****************************************************)
+(* Inversions with ysucc ****************************************************)
(*** ynat_cases *)
lemma ynat_split_zero_pos (x): ∨∨ 𝟎 = x | x = ↑↓x.
lemma ysucc_inf: ∞ = ↑(∞).
// qed.
-(* Inversion lemmas *********************************************************)
+(* Inversions ***************************************************************)
(*** ysucc_inv_inj_sn *)
lemma eq_inv_inj_ysucc (n1) (x2):
lemma eq_inv_ysucc_zero (x): ↑x = 𝟎 → ⊥.
/2 width=2 by eq_inv_zero_ysucc/ qed-.
-(* Eliminators **************************************************************)
+(* Eliminations *************************************************************)
(*** ynat_ind *)
lemma ynat_ind_succ (Q:predicate …):
(* GENERIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***********)
-(* Advanved properties with free variables inclusion ************************)
+(* Advanced properties with free variables inclusion ************************)
lemma reqg_fsge_comp (S):
reflexive … S →