From ae626612bff9c3746dd7647bbada791c737e348c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 28 Feb 2021 20:38:50 +0100 Subject: [PATCH] update in gruound + library refactored and restyled + recomm updated --- .../lambdadelta/bin/recomm/bGroundLib.mrc | 6 ++ .../lambdadelta/bin/recomm/dGroundLib.mrc | 9 +++ .../lambdadelta/bin/recomm/mrcOutput.ml | 8 ++- .../lambdadelta/bin/recomm/pGroundLib.mrc | 2 + .../lambdadelta/bin/recomm/rGroundArith.mrc | 2 +- .../lambdadelta/bin/recomm/rGroundLib.mrc | 10 +++ .../lambdadelta/bin/recomm/recommGc.ml | 24 ++++--- .../bin/recomm/recommGcbGroundLib.ml | 17 +++++ .../bin/recomm/recommGcbGroundLib.mli | 0 .../bin/recomm/recommGcdGroundLib.ml | 19 ++++++ .../bin/recomm/recommGcdGroundLib.mli | 0 .../bin/recomm/recommGcpGroundLib.ml | 11 ++++ .../bin/recomm/recommGcpGroundLib.mli | 0 .../bin/recomm/recommGcrGroundArith.ml | 1 - .../bin/recomm/recommGcrGroundLib.ml | 19 ++++++ .../bin/recomm/recommGcrGroundLib.mli | 0 .../lambdadelta/bin/recomm/recommGcsWith.ml | 2 + .../lambdadelta/bin/recomm/recommLexer.mll | 3 +- .../lambdadelta/bin/recomm/recommOutput.ml | 13 ++-- .../lambdadelta/bin/recomm/recommPccFor.ml | 1 + .../contribs/lambdadelta/bin/recomm/sWith.mrc | 2 +- .../lambdadelta/ground/arith/nat_le_max.ma | 4 +- .../{insert_eq => generated}/insert_eq_1.ma | 0 .../ground/{pull => generated}/pull_2.ma | 0 .../ground/{pull => generated}/pull_4.ma | 0 .../contribs/lambdadelta/ground/lib/exteq.ma | 4 +- .../lambdadelta/ground/lib/list_eq.ma | 2 +- .../contribs/lambdadelta/ground/lib/logic.ma | 2 +- .../lambdadelta/ground/lib/lstar_2a.ma | 2 +- .../contribs/lambdadelta/ground/lib/ltc.ma | 4 +- .../lambdadelta/ground/lib/ltc_ctc.ma | 8 +-- .../lambdadelta/ground/lib/relations.ma | 66 +++++++++---------- .../contribs/lambdadelta/ground/lib/star.ma | 10 +-- .../contribs/lambdadelta/ground/lib/stream.ma | 8 +++ .../lambdadelta/ground/relocation/nstream.ma | 2 +- 35 files changed, 187 insertions(+), 74 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/pGroundLib.mrc create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/rGroundLib.mrc create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.mli create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.ml create mode 100644 matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.mli rename matita/matita/contribs/lambdadelta/ground/{insert_eq => generated}/insert_eq_1.ma (100%) rename matita/matita/contribs/lambdadelta/ground/{pull => generated}/pull_2.ma (100%) rename matita/matita/contribs/lambdadelta/ground/{pull => generated}/pull_4.ma (100%) diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc new file mode 100644 index 000000000..fdc932735 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc @@ -0,0 +1,6 @@ +PcsAnd b "" true false +eq +land +lsub +compose, function composition +ctc, contextual transitive closure diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc new file mode 100644 index 000000000..c829279fd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/dGroundLib.mrc @@ -0,0 +1,9 @@ +PccFor d "" true false +GROUND NOTATION, GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ +RELATIONS +FUNCTIONS +LOGIC +BOOLEANS +LISTS +STREAMS +GENERATED LIBRARY diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml index 19128fb63..f39e07e03 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml @@ -48,10 +48,16 @@ let write_component st = write_mli cmod let write_index st = + let p = float (List.length st.ET.mods) in + let p = + if p > 0. then truncate (log10 p) else -1 + in + let ps = Printf.sprintf "%%0%uu" (succ p) in + let fmt = Scanf.format_from_string ps "%u" in 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%03u = RecommGc%s\n" (succ i) name + Printf.fprintf och "module G%(%u%) = RecommGc%s\n" fmt (succ i) name in List.iteri iter st.ET.mods; close_out och; diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/pGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundLib.mrc new file mode 100644 index 000000000..5b2fc18af --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/pGroundLib.mrc @@ -0,0 +1,2 @@ +PcsPar p "" true false +(with reflexivity) diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc index bfc2730fc..ac34215e1 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundArith.mrc @@ -8,7 +8,7 @@ PREDECESSOR ADDITION SUBTRACTION LEFT SUBTRACTION -MAXIMUM, MAXIMUN +MAXIMUM ORDER STRICT ORDER ARITHMETICAL PROPERTIES diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/rGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundLib.mrc new file mode 100644 index 000000000..7c2382e22 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/rGroundLib.mrc @@ -0,0 +1,10 @@ +PccFor r "" true false +CONJUNCTION +DISJUNCTION +EXTENSIONAL EQUIVALENCE +TRANSITIVE CLOSURE +LABELLED TRANSITIVE CLOSURE +NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE +HEAD AND TAIL +ITERATED TAIL +LENGTH diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml index b3fd0b550..58f1f1001 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGc.ml @@ -1,10 +1,14 @@ -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 +module G01 = RecommGcbGroundArith +module G02 = RecommGcbGroundCounters +module G03 = RecommGcbGroundLib +module G04 = RecommGcdGroundArith +module G05 = RecommGcdGroundCounters +module G06 = RecommGcdGroundLib +module G07 = RecommGcpGroundArith +module G08 = RecommGcpGroundLib +module G09 = RecommGcrGroundArith +module G10 = RecommGcrGroundCounters +module G11 = RecommGcrGroundLib +module G12 = RecommGcsAttr +module G13 = RecommGcsMain +module G14 = RecommGcsWith diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml new file mode 100644 index 000000000..94db88ed7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml @@ -0,0 +1,17 @@ +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 + | "ctc" :: tl -> k T.OK ("ctc" :: outs) tl + | "contextual" :: "transitive" :: "closure" :: tl -> k T.OK ("ctc" :: outs) tl + | "compose" :: tl -> k T.OK ("compose" :: outs) tl + | "function" :: "composition" :: tl -> k T.OK ("compose" :: outs) tl + | "lsub" :: tl -> k T.OK ("lsub" :: outs) tl + | "land" :: tl -> k T.OK ("land" :: outs) tl + | "eq" :: tl -> k T.OK ("eq" :: outs) tl + | _ -> k T.OO outs ins + +let main = + R.register_b step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml new file mode 100644 index 000000000..7fda12b7c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.ml @@ -0,0 +1,19 @@ +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 + | "GENERATED" :: "LIBRARY" :: tl -> k T.OK ("LIBRARY" :: "GENERATED" :: outs) tl + | "STREAMS" :: tl -> k T.OK ("STREAMS" :: outs) tl + | "LISTS" :: tl -> k T.OK ("LISTS" :: outs) tl + | "BOOLEANS" :: tl -> k T.OK ("BOOLEANS" :: outs) tl + | "LOGIC" :: tl -> k T.OK ("LOGIC" :: outs) tl + | "FUNCTIONS" :: tl -> k T.OK ("FUNCTIONS" :: outs) tl + | "RELATIONS" :: tl -> k T.OK ("RELATIONS" :: outs) tl + | "GROUND" :: "NOTATION" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl + | "GENERAL" :: "NOTATION" :: "USED" :: "BY" :: "THE" :: "FORMAL" :: "SYSTEM" :: "\206\187\206\180" :: tl -> k T.OK ("NOTATION" :: "GROUND" :: outs) tl + | _ -> k T.OO outs ins + +let main = + R.register_d step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundLib.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.ml new file mode 100644 index 000000000..085f6dff6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.ml @@ -0,0 +1,11 @@ +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 + | "(with" :: "reflexivity)" :: tl -> k T.OK ("reflexivity)" :: "(with" :: outs) tl + | _ -> k T.OO outs ins + +let main = + R.register_p step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcpGroundLib.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml index 091cc7f5f..136681a29 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml @@ -8,7 +8,6 @@ let step k st outs ins = | "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 diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.ml new file mode 100644 index 000000000..644497245 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.ml @@ -0,0 +1,19 @@ +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 + | "LENGTH" :: tl -> k T.OK ("LENGTH" :: outs) tl + | "ITERATED" :: "TAIL" :: tl -> k T.OK ("TAIL" :: "ITERATED" :: outs) tl + | "HEAD" :: "AND" :: "TAIL" :: tl -> k T.OK ("TAIL" :: "AND" :: "HEAD" :: outs) tl + | "NAT-LABELED" :: "REFLEXIVE" :: "AND" :: "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: "AND" :: "REFLEXIVE" :: "NAT-LABELED" :: outs) tl + | "LABELLED" :: "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: "LABELLED" :: outs) tl + | "TRANSITIVE" :: "CLOSURE" :: tl -> k T.OK ("CLOSURE" :: "TRANSITIVE" :: outs) tl + | "EXTENSIONAL" :: "EQUIVALENCE" :: tl -> k T.OK ("EQUIVALENCE" :: "EXTENSIONAL" :: outs) tl + | "DISJUNCTION" :: tl -> k T.OK ("DISJUNCTION" :: outs) tl + | "CONJUNCTION" :: tl -> k T.OK ("CONJUNCTION" :: outs) tl + | _ -> k T.OO outs ins + +let main = + R.register_r step diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.mli b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundLib.mli new file mode 100644 index 000000000..e69de29bb diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml index 091bb2d12..8d00bb812 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcsWith.ml @@ -6,6 +6,8 @@ let step k st outs ins = if st = T.KO then k st outs ins else match ins with | "with" :: tl -> k T.OK ("with" :: outs) tl + | "of" :: tl -> k T.OK ("with" :: outs) tl + | "for" :: tl -> k T.OK ("with" :: outs) tl | _ -> k T.OO outs ins let main = diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll index 99ff840af..83a289247 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll @@ -5,6 +5,7 @@ let keys = [| "Note"; + "NOTE"; |] let heads = [| @@ -37,9 +38,9 @@ aux (String.length s - 1) let disambiguate_word s = - if is_uppercase_ascii s then EP.CW s else if Array.mem s keys then EP.KW s else if Array.mem s heads then EP.HW s else + if is_uppercase_ascii s then EP.CW s else EP.SW s let log s = diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml index e0f3f1d70..187a2984b 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml @@ -13,8 +13,8 @@ let string_length_utf8 s = in l - aux 0 0 -let complete s = - let l = !width - string_length_utf8 s - 6 in +let complete s n = + let l = !width - string_length_utf8 s - 5 - n in if l < 0 then begin Printf.eprintf "overfull: %S\n" s; "" @@ -30,13 +30,16 @@ let out_src och = function | ET.Mark s -> Printf.fprintf och "(* *%s*)" s | ET.Key (s1, s2) -> - Printf.fprintf och "(* %s%s*)" 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 -> let s = String.concat " " ss in - Printf.fprintf och "(* %s %s*)" s (complete s) + Printf.fprintf och "(* %s %s*)" s (complete s 1) | ET.Slice ss -> let s = String.capitalize_ascii (String.concat " " ss) in - Printf.fprintf och "(* %s %s*)" s (complete s) + Printf.fprintf och "(* %s %s*)" s (complete s 1) | ET.Other (s1, s2, s3) -> Printf.fprintf och "%s%s%s" s1 s2 s3 diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml index 41a787dbd..4111798fc 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommPccFor.ml @@ -14,6 +14,7 @@ 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 + | "OF" :: tl -> !d_line (k_exit k) ET.OO ("FOR" :: outs) tl | _ -> k ET.KO outs ins let k_or k st outs ins = diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc index ecd022556..f057ad614 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/sWith.mrc @@ -1,2 +1,2 @@ check s "GcsMain" false false -with +with, of, for diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma index 0ad906540..b877b8649 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma @@ -35,9 +35,7 @@ lemma nle_max_dx_refl_sn (m) (n): m ≤ (m ∨ n). qed. lemma nle_max_dx_refl_dx (m) (n): n ≤ (m ∨ n). -#m #n @(nat_ind_2_succ … n m) -m -n // -#m #n #IH (Hf i) -Hf /2 width=3 by ltc_dx/ qed. -(* Inversions with contextual transitive closure ****************************) +(* Inversions with ctc ******************************************************) lemma ltc_inv_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B): associative … f → annulment_2 … f i → diff --git a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma index 56f6e21f7..328e2ea5b 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/relations.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/relations.ma @@ -17,28 +17,7 @@ include "ground/xoa/and_3.ma". include "ground/xoa/ex_2_2.ma". include "ground/lib/logic.ma". -(* GENERIC RELATIONS ********************************************************) - -definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝ - λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2. - -(* Inclusion ****************************************************************) - -definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝ - λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2). - -interpretation - "2-relation inclusion" - 'subseteq R1 R2 = (subR2 ?? R1 R2). - -definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝ - λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3). - -interpretation - "3-relation inclusion" - 'subseteq R1 R2 = (subR3 ??? R1 R2). - -(* Properties of relations **************************************************) +(* RELATIONS ****************************************************************) definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝ λA,B,C,D,E.A→B→C→D→E→Prop. @@ -46,7 +25,10 @@ definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] definition relation6: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝ λA,B,C,D,E,F.A→B→C→D→E→F→Prop. -(**) (* we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *) +definition replace_2 (A) (B): relation3 (relation2 A B) (relation A) (relation B) ≝ + λR,Sa,Sb. ∀a1,b1. R a1 b1 → ∀a2. Sa a1 a2 → ∀b2. Sb b1 b2 → R a2 b2. + +(* * we don't use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *) definition c_reflexive (A) (B): predicate (relation3 A B B) ≝ λR. ∀a,b. R a b b. @@ -95,15 +77,7 @@ definition is_mono (B:Type[0]): predicate (predicate B) ≝ definition is_inj2 (A,B:Type[0]): predicate (relation2 A B) ≝ λR. ∀a1,b. R a1 b → ∀a2. R a2 b → a1 = a2. -(* Main properties of equality **********************************************) - -theorem canc_sn_eq (A): left_cancellable A (eq …). -// qed-. - -theorem canc_dx_eq (A): right_cancellable A (eq …). -// qed-. - -(* Normal form and strong normalization *************************************) +(* NOTE: Normal form and strong normalization *******************************) definition NF (A): relation A → relation A → predicate A ≝ λR,S,a1. ∀a2. R a1 a2 → S a1 a2. @@ -135,13 +109,13 @@ lemma NF_to_SN_sn (A) (R) (S): ∀a. NF_sn A R S a → SN_sn A R S a. elim HSa12 -HSa12 /2 width=1 by/ qed. -(* Normal form and strong normalization with unboxed triples ****************) +(* NOTE: Normal form and strong normalization with unboxed triples **********) inductive SN3 (A) (B) (C) (R,S:relation6 A B C A B C): relation3 A B C ≝ | SN3_intro: ∀a1,b1,c1. (∀a2,b2,c2. R a1 b1 c1 a2 b2 c2 → (S a1 b1 c1 a2 b2 c2 → ⊥) → SN3 … R S a2 b2 c2) → SN3 … R S a1 b1 c1 . -(* Relations with unboxed triples *******************************************) +(* NOTE: Reflexive closure with unboxed triples *****************************) definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝ λR,a1,b1,c1,a2,b2,c2. @@ -150,3 +124,27 @@ definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝ lemma tri_RC_reflexive (A) (B) (C): ∀R. tri_reflexive A B C (tri_RC … R). /3 width=1 by and3_intro, or_intror/ qed. + +(* NOTE: Inclusion for relations ********************************************) + +definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝ + λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2). + +interpretation + "2-relation inclusion" + 'subseteq R1 R2 = (subR2 ?? R1 R2). + +definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝ + λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3). + +interpretation + "3-relation inclusion" + 'subseteq R1 R2 = (subR3 ??? R1 R2). + +(* Main constructions with eq ***********************************************) + +theorem canc_sn_eq (A): left_cancellable A (eq …). +// qed-. + +theorem canc_dx_eq (A): right_cancellable A (eq …). +// qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/star.ma b/matita/matita/contribs/lambdadelta/ground/lib/star.ma index 5e748c5ea..ee7ff16f7 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/star.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/star.ma @@ -15,7 +15,7 @@ include "basics/star1.ma". include "ground/lib/relations.ma". -(* TRANSITIVE CLOSURE *******************************************************) +(* TRANSITIVE CLOSURE FOR RELATIONS *****************************************) definition CTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝ λA,B,R,a. TC … (R a). @@ -139,7 +139,7 @@ elim (TC_idem … (S L2) … T1 T2) #_ #H1 #H2 #_ @H2 @HSR /3 width=3 by/ qed-. -(* Normal form and strong normalization *************************************) +(* NOTE: Normal form and strong normalization *******************************) lemma SN_to_NF: ∀A,R,S. NF_dec A R S → ∀a1. SN A R S a1 → @@ -149,7 +149,7 @@ lemma SN_to_NF: ∀A,R,S. NF_dec A R S → * #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3 by star_compl, ex2_intro/ qed-. -(* Relations with unboxed pairs *********************************************) +(* NOTE: Relations with unboxed pairs ***************************************) lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R → ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 → @@ -186,11 +186,11 @@ lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B. ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2. #A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1 [ /2 width=1 by or_introl/ -| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4 by ex2_2_intro, or_intror/ (**) (* auto fails without #_ *) +| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4 by ex2_2_intro, or_intror/ (* * auto fails without #_ *) ] qed-. -(* Relations with unboxed triples *******************************************) +(* NOTE: Relations with unboxed triples *************************************) definition tri_star: ∀A,B,C,R. tri_relation A B C ≝ λA,B,C,R. tri_RC A B C (tri_TC … R). diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma index d0e05e17e..ff7a6c349 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/stream.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/stream.ma @@ -30,3 +30,11 @@ interpretation lemma stream_rew (A) (t:stream A): match t with [ stream_cons a u ⇒ a ⨮ u ] = t. #A * // qed. + +(* Basic inversions *********************************************************) + +lemma eq_inv_stream_cons_bi (A) (a1,a2:A) (u1) (u2): + a1 ⨮ u1 = a2 ⨮ u2 → ∧∧ a1 = a2 & u1 = u2. +#A #a1 #a2 #u1 #u2 #H destruct +/2 width=1 by conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma index 42c174ddc..8819cdc51 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/nstream.ma @@ -88,7 +88,7 @@ lemma iota_next: ∀R,a,b,f. b f = case_type0 R a b (↑f). #R #a #b * // qed. -(* Specific properties ******************************************************) +(* Poperties with stream_tl *************************************************) lemma tl_push: ∀f. f = ⫰⫯f. // qed. -- 2.39.2