From: Ferruccio Guidi Date: Sun, 5 Apr 2009 23:38:16 +0000 (+0000) Subject: - Procedural: now we generate the exact tactic (in place of some apply tactics) and... X-Git-Tag: make_still_working~4121 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ef05c795559108c1d33cfa048531849807867a81;p=helm.git - Procedural: now we generate the exact tactic (in place of some apply tactics) and we do not perform conversion steps before it (1104 change tactics omitted in the lambda-delta devel) - new target for the PREDICATIVE-TOPOLOGY devel: now is "limits" --- diff --git a/helm/software/components/acic_procedural/procedural1.ml b/helm/software/components/acic_procedural/procedural1.ml index 4b9127002..ad3152530 100644 --- a/helm/software/components/acic_procedural/procedural1.ml +++ b/helm/software/components/acic_procedural/procedural1.ml @@ -241,8 +241,9 @@ let get_intro = function | C.Anonymous -> None | C.Name s -> Some s -let mk_preamble st what script = - convert st what @ script +let mk_preamble st what script = match script with + | T.Exact _ :: _ -> script + | _ -> convert st what @ script let mk_arg st = function | C.ARel (_, _, i, name) as what -> convert st ~name:(name, i) what @@ -270,7 +271,7 @@ let mk_fwd_rewrite st dtext name tl direction v t ity = assert (Ut.is_sober st.context (H.cic ity)); let ity = H.acic_bc st.context ity in let br1 = [T.Id ""] in - let br2 = List.rev (T.Apply (w, "assumption") :: script None) in + let br2 = List.rev (T.Exact (w, "assumption") :: script None) in let text = "non-linear rewrite" in st, [T.Branch ([br2; br1], ""); T.Cut (name, ity, text)] end @@ -320,24 +321,24 @@ and proc_letin st what name v w t = let qt = proc_proof (next (add st entry)) t in List.rev_append rqv qt else - [T.Apply (what, dtext)] + [T.Exact (what, dtext)] in mk_preamble st what script and proc_rel st what = let _, dtext = test_depth st in let text = "assumption" in - let script = [T.Apply (what, dtext ^ text)] in + let script = [T.Exact (what, dtext ^ text)] in mk_preamble st what script and proc_mutconstruct st what = let _, dtext = test_depth st in - let script = [T.Apply (what, dtext)] in + let script = [T.Exact (what, dtext)] in mk_preamble st what script and proc_const st what = let _, dtext = test_depth st in - let script = [T.Apply (what, dtext)] in + let script = [T.Exact (what, dtext)] in mk_preamble st what script and proc_appl st what hd tl = @@ -391,7 +392,7 @@ and proc_appl st what hd tl = let hd = mk_exp_args hd tl classes synth in script @ [T.Apply (hd, dtext ^ text); T.Branch (qs, "")] else - [T.Apply (what, dtext)] + [T.Exact (what, dtext)] in mk_preamble st what script @@ -411,14 +412,14 @@ and proc_case st what uri tyno u v ts = let script = List.rev (mk_arg st v) in script @ [T.Cases (v, e, dtext ^ text); T.Branch (qs, "")] else - [T.Apply (what, dtext)] + [T.Exact (what, dtext)] in mk_preamble st what script and proc_other st what = let _, dtext = test_depth st in let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head what) in - let script = [T.Apply (what, dtext ^ text)] in + let script = [T.Exact (what, dtext ^ text)] in mk_preamble st what script and proc_proof st t = @@ -458,7 +459,7 @@ try let aux (inv, _) v = if I.overlaps synth inv then None else if I.S.is_empty inv then Some (get_note (fun st -> proc_proof st v)) else - Some (get_note (fun _ -> [T.Apply (v, dtext ^ "dependent")])) + Some (get_note (fun _ -> [T.Exact (v, dtext ^ "dependent")])) in let ps = T.list_map2_filter aux classes ts in let b = List.length ps > 1 in diff --git a/helm/software/components/acic_procedural/proceduralTeX.ml b/helm/software/components/acic_procedural/proceduralTeX.ml index 55be4ddb3..279ebecb9 100644 --- a/helm/software/components/acic_procedural/proceduralTeX.ml +++ b/helm/software/components/acic_procedural/proceduralTeX.ml @@ -194,6 +194,8 @@ let rec xl frm = function | T.Statement _ :: l | T.Qed _ :: l -> xl frm l + | T.Exact (t, _) :: l -> + F.fprintf frm "\\Exact{%a}" xat t; xl frm l | T.Intros (_, [r], _) :: l -> F.fprintf frm "\\Intro{%a}{%a}" xx r xl l | T.LetIn (r, v, _) :: l -> diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index cb4c11d2e..75ce2ee64 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -74,6 +74,7 @@ type step = Note of note | Statement of flavour * name * what * body * note | Qed of note | Id of note + | Exact of what * note | Intros of count option * name list * note | Cut of name * what * note | LetIn of name * what * note @@ -166,6 +167,10 @@ let mk_id punctation = let tactic = G.IdTac floc in mk_tactic tactic punctation +let mk_exact t punctation = + let tactic = G.Exact (floc, t) in + mk_tactic tactic punctation + let mk_intros xi xids punctation = let tactic = G.Intros (floc, (xi, xids)) in mk_tactic tactic punctation @@ -239,6 +244,7 @@ let rec render_step sep a = function | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a | Inductive (lps, ts, s) -> mk_inductive lps ts :: mk_thnote s a | Qed s -> mk_qed :: mk_tacnote s a + | Exact (t, s) -> mk_exact t sep :: mk_tacnote s a | Id s -> mk_id sep :: mk_tacnote s a | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a @@ -275,6 +281,7 @@ let rec count_step a = function | Note _ | Statement _ | Id _ + | Exact _ | Qed _ -> a | Branch (pps, _) -> List.fold_left count_steps a pps | _ -> succ a @@ -292,6 +299,7 @@ let rec count_node a = function | Intros _ | Clear _ | ClearBody _ -> a + | Exact (t, _) | Cut (_, t, _) | LetIn (_, t, _) | Apply (t, _) -> count a (H.cic t) diff --git a/helm/software/components/acic_procedural/proceduralTypes.mli b/helm/software/components/acic_procedural/proceduralTypes.mli index aa6ad3aa5..13161daad 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.mli +++ b/helm/software/components/acic_procedural/proceduralTypes.mli @@ -53,6 +53,7 @@ type step = Note of note | Statement of flavour * name * what * body * note | Qed of note | Id of note + | Exact of what * note | Intros of count option * name list * note | Cut of name * what * note | LetIn of name * what * note diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile deleted file mode 100644 index a3e891435..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/Makefile +++ /dev/null @@ -1,16 +0,0 @@ -include ../Makefile.defs - -DIR=$(shell basename $$PWD) - -$(DIR) all: - $(BIN)matitac -$(DIR).opt opt all.opt: - $(BIN)matitac.opt -clean: - $(BIN)matitaclean -clean.opt: - $(BIN)matitaclean.opt -depend: - $(BIN)matitadep -depend.opt: - $(BIN)matitadep.opt diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma deleted file mode 100644 index f337d8ce5..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma +++ /dev/null @@ -1,79 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* STATO: COMPILA *) - -(* Project started Wed Oct 12, 2005 ***************************************) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs". - -include "logic/connectives.ma". - -(* ACZEL CATEGORIES: - - We use typoids with a compatible membership relation - - The category is intended to be the domain of the membership relation - - The membership relation is necessary because we need to regard the - domain of a propositional function (ie a predicative subset) as a - quantification domain and therefore as a category, but there is no - type in CIC representing the domain of a propositional function - - We set up a single equality predicate, parametric on the category, - defined as the reflexive, symmetic, transitive and compatible closure - of the cle1 predicate given inside the category. Then we prove the - properties of the equality that usually are axiomatized inside the - category structure. This makes categories easier to use -*) - -definition true_f \def \lambda (X:Type). \lambda (_:X). True. - -definition false_f \def \lambda (X:Type). \lambda (_:X). False. - -record Class: Type \def { - class:> Type; - cin: class \to Prop; - ceq: class \to class \to Prop; - cin_repl: \forall c1,c2. cin c1 \to ceq c1 c2 \to cin c2; - ceq_repl: \forall c1,c2,d1,d2. cin c1 \to - ceq c1 c2 \to ceq c1 d1 \to ceq c2 d2 \to ceq d1 d2; - ceq_refl: \forall c. cin c \to ceq c c -}. - -(* external universal quantification *) -inductive call (C:Class) (P:C \to Prop) : Prop \def - | call_intro: (\forall c. cin ? c \to P c) \to call C P. - -inductive call2 (C1,C2:Class) (P:C1 \to C2 \to Prop) : Prop \def - | call2_intro: - (\forall c1,c2. cin ? c1 \to cin ? c2 \to P c1 c2) \to call2 C1 C2 P. - -(* notations **************************************************************) - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "external for all" 'xforall \eta.x = - (cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call.ind#xpointer(1/1) _ x). - -notation > "hvbox(\xforall ident i opt (: ty) break . p)" - with precedence 20 -for @{ 'xforall ${default - @{\lambda ${ident i} : $ty. $p} - @{\lambda ${ident i} . $p}}}. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "external for all 2" 'xforall2 \eta.x \eta.y = - (cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call2.ind#xpointer(1/1) _ _ x y). - -notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)" - with precedence 20 -for @{ 'xforall2 ${default - @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p} - @{\lambda ${ident i1}, ${ident i2}. $p}}}. diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma deleted file mode 100644 index b86e5f296..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma +++ /dev/null @@ -1,32 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* STATO: NON COMPILA: dev'essere aggiornato *) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq". - -include "class_defs.ma". - -theorem ceq_trans: \forall C. \xforall c1,c2. ceq C c1 c2 \to - \xforall c3. ceq ? c2 c3 \to ceq ? c1 c3. -intros. - -(* -apply ceq_intro; apply cle_trans; [|auto new timeout=100|auto new timeout=100||auto new timeout=100|auto new timeout=100]. -qed. - -theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1. -intros; elim H; clear H.; auto new timeout=100. -qed. -*) diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma deleted file mode 100644 index 1d6c763ab..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma +++ /dev/null @@ -1,63 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* STATO: NON COMPILA: attendo che l'oggetto "pippo" venga accettato *) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_defs". - -include "iff.ma". -include "domain_data.ma". - -(* COMPLETE OVERLAP ALGEBRAS -*) - -record COA: Type \def { - coa:> Class; (* carrier *) - le: coa \to coa \to Prop; (* inclusion *) - ov: coa \to coa \to Prop; (* overlap *) - sup: \forall (D:Domain). (D \to coa) \to coa; (* supremum *) - inf: \forall (D:Domain). (D \to coa) \to coa; (* infimum *) - le_refl: \forall p. le p p; - le_trans: \forall p,r. le p r \to \forall q. le r q \to le p q; - le_antysym: \forall q,p. le q p \to le p q \to ceq ? p q; - ov_sym: \forall q,p. ov q p \to ov p q; - sup_le: \forall D,ps,q. le (sup D ps) q \liff \iforall d. le (ps d) q; - inf_le: \forall D,p,qs. le p (inf D qs) \liff \iforall d. le p (qs d); - sup_ov: \forall D,ps,q. ov (sup D ps) q \liff \iexists d. ov (ps d) q; - density: \forall p,q. (\forall r. ov p r \to ov q r) \to le p q -}. - -definition zero: \forall (P:COA). P \def - \lambda (P:COA). inf P ? (dvoid_ixfam P). - -definition one: \forall (P:COA). P \def - \lambda (P:COA). sup P ? (dvoid_ixfam P). - -definition binf: \forall (P:COA). P \to P \to P \def - \lambda (P:COA). \lambda p0,p1. - inf P ? (dbool_ixfam P p0 p1). - -definition bsup: \forall (P:COA). P \to P \to P \def - \lambda (P:COA). \lambda p0,p1. - sup P ? (dbool_ixfam P p0 p1). - -(* - inf_ov: forall p q, ov p q -> ov p (inf QDBool (bool_family _ p q)) - properness: ov zero zero -> False; - distributivity: forall I p q, id _ (inf QDBool (bool_family _ (sup I p) q)) (sup I (fun i => (inf QDBool (bool_family _ (p i) q)))); -*) - -inductive pippo : Prop \def - | Pippo: let x \def zero in zero = x \to pippo. - diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma deleted file mode 100644 index da2c1f678..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/coa_props.ma +++ /dev/null @@ -1,31 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* STATO: NON COMPILA: perche' dipende da coa_defs *) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_props". - -include "coa_defs.ma". - -inductive True:Prop \def T:True. - -theorem zero_le: - \forall (P:COA). \forall (p:P). (le ? (zero P) p) \to True. - intros. - exact T. -qed. - - - - diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends deleted file mode 100644 index 13fa00c5a..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/depends +++ /dev/null @@ -1,12 +0,0 @@ -class_eq.ma class_defs.ma -domain_defs.ma class_defs.ma -coa_props.ma coa_defs.ma -class_defs.ma logic/connectives.ma -domain_data.ma datatypes/bool.ma datatypes/constructors.ma domain_defs.ma -subset_defs.ma domain_defs.ma -coa_defs.ma domain_data.ma iff.ma -iff.ma ../../library/logic/connectives.ma -../../library/logic/connectives.ma -datatypes/bool.ma -datatypes/constructors.ma -logic/connectives.ma diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma deleted file mode 100644 index 5bc9c2a7d..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_data.ma +++ /dev/null @@ -1,42 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* STATO: NON COMPILA: dev'essere aggiornato *) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_data". - -include "datatypes/constructors.ma". -include "datatypes/bool.ma". -include "domain_defs.ma". - -(* QUANTIFICATION DOMAINS - - Here we define some useful domains based on data types -*) - -definition DBool : Domain \def - mk_Domain (mk_Class bool (true_f ?) (eq ?)). - -definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def - \lambda C,c0,c1,b. - match b in bool with - [ false \Rightarrow c0 - | true \Rightarrow c1 - ]. - -definition DVoid : Domain \def - mk_Domain (mk_Class void (true_f ?) (eq ?)). - -definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def - \lambda C,v. - match v in void with []. diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma deleted file mode 100644 index dcdf84644..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma +++ /dev/null @@ -1,60 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* STATO: COMPILA *) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs". - -include "class_defs.ma". - -(* QUANTIFICATION DOMAINS - - These are the categories on which we allow quantification - - We set up single quantifiers, parametric on the domain, so they - already have the properties that usually are axiomatized inside the - domain structure. This makes domains easier to use -*) - -record Domain: Type \def { - qd:> Class -}. - -(* internal universal quantification *) -inductive dall (D:Domain) (P:D \to Prop) : Prop \def - | dall_intro: (\forall d:D. cin D d \to P d) \to dall D P. - -(* internal existential quantification *) -inductive dex (D:Domain) (P:D \to Prop) : Prop \def - | dex_intro: \forall d:D. cin D d \land P d \to dex D P. - -(* notations **************************************************************) - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "internal for all" 'iforall \eta.x = - (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dall.ind#xpointer(1/1) _ x). - -notation > "hvbox(\iforall ident i opt (: ty) break . p)" - right associative with precedence 20 -for @{ 'iforall ${default - @{\lambda ${ident i} : $ty. $p)} - @{\lambda ${ident i} . $p}}}. - -(*CSC: the URI must disappear: there is a bug now *) -interpretation "internal exists" 'dexists \eta.x = - (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dex.ind#xpointer(1/1) _ x). - -notation > "hvbox(\iexists ident i opt (: ty) break . p)" - right associative with precedence 20 -for @{ 'dexists ${default - @{\lambda ${ident i} : $ty. $p)} - @{\lambda ${ident i} . $p}}}. diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma deleted file mode 100644 index 0e6205148..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/iff.ma +++ /dev/null @@ -1,33 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* STATO: COMPILA *) - -set "baseuri" "cic:/matita/logic/iff". - -include "../../library/logic/connectives.ma". - -definition Iff : Prop \to Prop \to Prop \def - \lambda A,B. (A \to B) \land (B \to A). - - (*CSC: the URI must disappear: there is a bug now *) -interpretation "logical iff" 'iff x y = (cic:/matita/logic/iff/Iff.con x y). - -notation > "hvbox(a break \liff b)" - left associative with precedence 25 -for @{ 'iff $a $b }. - -notation < "hvbox(a break \leftrightarrow b)" - left associative with precedence 25 -for @{ 'iff $a $b }. diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root deleted file mode 100644 index cde289d74..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/root +++ /dev/null @@ -1 +0,0 @@ -baseuri=cic:/matita/PREDICATIVE-TOPOLOGY diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma deleted file mode 100644 index 7469f08af..000000000 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma +++ /dev/null @@ -1,68 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* STATO: NON COMPILA: dev'essere aggiornato *) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs". - -include "domain_defs.ma". - -(* SUBSETS - - We use predicative subsets coded as propositional functions - according to G.Sambin and S.Valentini "Toolbox" -*) - -definition Subset \def \lambda (D:Domain). D \to Prop. - -(* subset membership (epsilon) *) -definition sin : \forall D. Subset D \to D \to Prop \def - \lambda (D:Domain). \lambda U,d. cin D d \and U d. - -(* subset top (full subset) *) -definition stop \def \lambda (D:Domain). true_f D. - -(* subset bottom (empty subset) *) -definition sbot \def \lambda (D:Domain). false_f D. - -(* subset and (binary intersection) *) -definition sand: \forall D. Subset D \to Subset D \to Subset D \def - \lambda D,U1,U2,d. U1 d \land U2 d. - -(* subset or (binary union) *) -definition sor: \forall D. Subset D \to Subset D \to Subset D \def - \lambda D,U1,U2,d. U1 d \lor U2 d. - -(* subset less or equal (inclusion) *) -definition sle: \forall D. Subset D \to Subset D \to Prop \def - \lambda D,U1,U2. \iforall d. U1 d \to U2 d. - -(* subset overlap *) -definition sover: \forall D. Subset D \to Subset D \to Prop \def - \lambda D,U1,U2. \iexists d. U1 d \land U2 d. - -(* coercions **************************************************************) - -(* -(* the class of the subsets of a domain (not an implicit coercion) *) -definition class_of_subsets_of \def - \lambda D. mk_Class (Subset D) (true_f ?) (sle ?). -*) - -(* the domain built upon a subset (not an implicit coercion) *) -definition domain_of_subset: \forall D. Subset D \to Domain \def - \lambda (D:Domain). \lambda U. - mk_Domain (mk_Class D (sin D U) (cle1 D)). - -(* the full subset of a domain *) -coercion stop. diff --git a/helm/software/matita/contribs/limits/Makefile b/helm/software/matita/contribs/limits/Makefile new file mode 100644 index 000000000..a3e891435 --- /dev/null +++ b/helm/software/matita/contribs/limits/Makefile @@ -0,0 +1,16 @@ +include ../Makefile.defs + +DIR=$(shell basename $$PWD) + +$(DIR) all: + $(BIN)matitac +$(DIR).opt opt all.opt: + $(BIN)matitac.opt +clean: + $(BIN)matitaclean +clean.opt: + $(BIN)matitaclean.opt +depend: + $(BIN)matitadep +depend.opt: + $(BIN)matitadep.opt diff --git a/helm/software/matita/contribs/limits/class_defs.ma b/helm/software/matita/contribs/limits/class_defs.ma new file mode 100644 index 000000000..f337d8ce5 --- /dev/null +++ b/helm/software/matita/contribs/limits/class_defs.ma @@ -0,0 +1,79 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STATO: COMPILA *) + +(* Project started Wed Oct 12, 2005 ***************************************) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs". + +include "logic/connectives.ma". + +(* ACZEL CATEGORIES: + - We use typoids with a compatible membership relation + - The category is intended to be the domain of the membership relation + - The membership relation is necessary because we need to regard the + domain of a propositional function (ie a predicative subset) as a + quantification domain and therefore as a category, but there is no + type in CIC representing the domain of a propositional function + - We set up a single equality predicate, parametric on the category, + defined as the reflexive, symmetic, transitive and compatible closure + of the cle1 predicate given inside the category. Then we prove the + properties of the equality that usually are axiomatized inside the + category structure. This makes categories easier to use +*) + +definition true_f \def \lambda (X:Type). \lambda (_:X). True. + +definition false_f \def \lambda (X:Type). \lambda (_:X). False. + +record Class: Type \def { + class:> Type; + cin: class \to Prop; + ceq: class \to class \to Prop; + cin_repl: \forall c1,c2. cin c1 \to ceq c1 c2 \to cin c2; + ceq_repl: \forall c1,c2,d1,d2. cin c1 \to + ceq c1 c2 \to ceq c1 d1 \to ceq c2 d2 \to ceq d1 d2; + ceq_refl: \forall c. cin c \to ceq c c +}. + +(* external universal quantification *) +inductive call (C:Class) (P:C \to Prop) : Prop \def + | call_intro: (\forall c. cin ? c \to P c) \to call C P. + +inductive call2 (C1,C2:Class) (P:C1 \to C2 \to Prop) : Prop \def + | call2_intro: + (\forall c1,c2. cin ? c1 \to cin ? c2 \to P c1 c2) \to call2 C1 C2 P. + +(* notations **************************************************************) + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "external for all" 'xforall \eta.x = + (cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call.ind#xpointer(1/1) _ x). + +notation > "hvbox(\xforall ident i opt (: ty) break . p)" + with precedence 20 +for @{ 'xforall ${default + @{\lambda ${ident i} : $ty. $p} + @{\lambda ${ident i} . $p}}}. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "external for all 2" 'xforall2 \eta.x \eta.y = + (cic:/matita/PREDICATIVE-TOPOLOGY/class_defs/call2.ind#xpointer(1/1) _ _ x y). + +notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)" + with precedence 20 +for @{ 'xforall2 ${default + @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p} + @{\lambda ${ident i1}, ${ident i2}. $p}}}. diff --git a/helm/software/matita/contribs/limits/class_eq.ma b/helm/software/matita/contribs/limits/class_eq.ma new file mode 100644 index 000000000..b86e5f296 --- /dev/null +++ b/helm/software/matita/contribs/limits/class_eq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STATO: NON COMPILA: dev'essere aggiornato *) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq". + +include "class_defs.ma". + +theorem ceq_trans: \forall C. \xforall c1,c2. ceq C c1 c2 \to + \xforall c3. ceq ? c2 c3 \to ceq ? c1 c3. +intros. + +(* +apply ceq_intro; apply cle_trans; [|auto new timeout=100|auto new timeout=100||auto new timeout=100|auto new timeout=100]. +qed. + +theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1. +intros; elim H; clear H.; auto new timeout=100. +qed. +*) diff --git a/helm/software/matita/contribs/limits/coa_defs.ma b/helm/software/matita/contribs/limits/coa_defs.ma new file mode 100644 index 000000000..1d6c763ab --- /dev/null +++ b/helm/software/matita/contribs/limits/coa_defs.ma @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STATO: NON COMPILA: attendo che l'oggetto "pippo" venga accettato *) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_defs". + +include "iff.ma". +include "domain_data.ma". + +(* COMPLETE OVERLAP ALGEBRAS +*) + +record COA: Type \def { + coa:> Class; (* carrier *) + le: coa \to coa \to Prop; (* inclusion *) + ov: coa \to coa \to Prop; (* overlap *) + sup: \forall (D:Domain). (D \to coa) \to coa; (* supremum *) + inf: \forall (D:Domain). (D \to coa) \to coa; (* infimum *) + le_refl: \forall p. le p p; + le_trans: \forall p,r. le p r \to \forall q. le r q \to le p q; + le_antysym: \forall q,p. le q p \to le p q \to ceq ? p q; + ov_sym: \forall q,p. ov q p \to ov p q; + sup_le: \forall D,ps,q. le (sup D ps) q \liff \iforall d. le (ps d) q; + inf_le: \forall D,p,qs. le p (inf D qs) \liff \iforall d. le p (qs d); + sup_ov: \forall D,ps,q. ov (sup D ps) q \liff \iexists d. ov (ps d) q; + density: \forall p,q. (\forall r. ov p r \to ov q r) \to le p q +}. + +definition zero: \forall (P:COA). P \def + \lambda (P:COA). inf P ? (dvoid_ixfam P). + +definition one: \forall (P:COA). P \def + \lambda (P:COA). sup P ? (dvoid_ixfam P). + +definition binf: \forall (P:COA). P \to P \to P \def + \lambda (P:COA). \lambda p0,p1. + inf P ? (dbool_ixfam P p0 p1). + +definition bsup: \forall (P:COA). P \to P \to P \def + \lambda (P:COA). \lambda p0,p1. + sup P ? (dbool_ixfam P p0 p1). + +(* + inf_ov: forall p q, ov p q -> ov p (inf QDBool (bool_family _ p q)) + properness: ov zero zero -> False; + distributivity: forall I p q, id _ (inf QDBool (bool_family _ (sup I p) q)) (sup I (fun i => (inf QDBool (bool_family _ (p i) q)))); +*) + +inductive pippo : Prop \def + | Pippo: let x \def zero in zero = x \to pippo. + diff --git a/helm/software/matita/contribs/limits/coa_props.ma b/helm/software/matita/contribs/limits/coa_props.ma new file mode 100644 index 000000000..da2c1f678 --- /dev/null +++ b/helm/software/matita/contribs/limits/coa_props.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STATO: NON COMPILA: perche' dipende da coa_defs *) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/coa_props". + +include "coa_defs.ma". + +inductive True:Prop \def T:True. + +theorem zero_le: + \forall (P:COA). \forall (p:P). (le ? (zero P) p) \to True. + intros. + exact T. +qed. + + + + diff --git a/helm/software/matita/contribs/limits/depends b/helm/software/matita/contribs/limits/depends new file mode 100644 index 000000000..13fa00c5a --- /dev/null +++ b/helm/software/matita/contribs/limits/depends @@ -0,0 +1,12 @@ +class_eq.ma class_defs.ma +domain_defs.ma class_defs.ma +coa_props.ma coa_defs.ma +class_defs.ma logic/connectives.ma +domain_data.ma datatypes/bool.ma datatypes/constructors.ma domain_defs.ma +subset_defs.ma domain_defs.ma +coa_defs.ma domain_data.ma iff.ma +iff.ma ../../library/logic/connectives.ma +../../library/logic/connectives.ma +datatypes/bool.ma +datatypes/constructors.ma +logic/connectives.ma diff --git a/helm/software/matita/contribs/limits/domain_data.ma b/helm/software/matita/contribs/limits/domain_data.ma new file mode 100644 index 000000000..5bc9c2a7d --- /dev/null +++ b/helm/software/matita/contribs/limits/domain_data.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STATO: NON COMPILA: dev'essere aggiornato *) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_data". + +include "datatypes/constructors.ma". +include "datatypes/bool.ma". +include "domain_defs.ma". + +(* QUANTIFICATION DOMAINS + - Here we define some useful domains based on data types +*) + +definition DBool : Domain \def + mk_Domain (mk_Class bool (true_f ?) (eq ?)). + +definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def + \lambda C,c0,c1,b. + match b in bool with + [ false \Rightarrow c0 + | true \Rightarrow c1 + ]. + +definition DVoid : Domain \def + mk_Domain (mk_Class void (true_f ?) (eq ?)). + +definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def + \lambda C,v. + match v in void with []. diff --git a/helm/software/matita/contribs/limits/domain_defs.ma b/helm/software/matita/contribs/limits/domain_defs.ma new file mode 100644 index 000000000..dcdf84644 --- /dev/null +++ b/helm/software/matita/contribs/limits/domain_defs.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STATO: COMPILA *) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs". + +include "class_defs.ma". + +(* QUANTIFICATION DOMAINS + - These are the categories on which we allow quantification + - We set up single quantifiers, parametric on the domain, so they + already have the properties that usually are axiomatized inside the + domain structure. This makes domains easier to use +*) + +record Domain: Type \def { + qd:> Class +}. + +(* internal universal quantification *) +inductive dall (D:Domain) (P:D \to Prop) : Prop \def + | dall_intro: (\forall d:D. cin D d \to P d) \to dall D P. + +(* internal existential quantification *) +inductive dex (D:Domain) (P:D \to Prop) : Prop \def + | dex_intro: \forall d:D. cin D d \land P d \to dex D P. + +(* notations **************************************************************) + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "internal for all" 'iforall \eta.x = + (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dall.ind#xpointer(1/1) _ x). + +notation > "hvbox(\iforall ident i opt (: ty) break . p)" + right associative with precedence 20 +for @{ 'iforall ${default + @{\lambda ${ident i} : $ty. $p)} + @{\lambda ${ident i} . $p}}}. + +(*CSC: the URI must disappear: there is a bug now *) +interpretation "internal exists" 'dexists \eta.x = + (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dex.ind#xpointer(1/1) _ x). + +notation > "hvbox(\iexists ident i opt (: ty) break . p)" + right associative with precedence 20 +for @{ 'dexists ${default + @{\lambda ${ident i} : $ty. $p)} + @{\lambda ${ident i} . $p}}}. diff --git a/helm/software/matita/contribs/limits/iff.ma b/helm/software/matita/contribs/limits/iff.ma new file mode 100644 index 000000000..0e6205148 --- /dev/null +++ b/helm/software/matita/contribs/limits/iff.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STATO: COMPILA *) + +set "baseuri" "cic:/matita/logic/iff". + +include "../../library/logic/connectives.ma". + +definition Iff : Prop \to Prop \to Prop \def + \lambda A,B. (A \to B) \land (B \to A). + + (*CSC: the URI must disappear: there is a bug now *) +interpretation "logical iff" 'iff x y = (cic:/matita/logic/iff/Iff.con x y). + +notation > "hvbox(a break \liff b)" + left associative with precedence 25 +for @{ 'iff $a $b }. + +notation < "hvbox(a break \leftrightarrow b)" + left associative with precedence 25 +for @{ 'iff $a $b }. diff --git a/helm/software/matita/contribs/limits/root b/helm/software/matita/contribs/limits/root new file mode 100644 index 000000000..cde289d74 --- /dev/null +++ b/helm/software/matita/contribs/limits/root @@ -0,0 +1 @@ +baseuri=cic:/matita/PREDICATIVE-TOPOLOGY diff --git a/helm/software/matita/contribs/limits/subset_defs.ma b/helm/software/matita/contribs/limits/subset_defs.ma new file mode 100644 index 000000000..7469f08af --- /dev/null +++ b/helm/software/matita/contribs/limits/subset_defs.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STATO: NON COMPILA: dev'essere aggiornato *) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs". + +include "domain_defs.ma". + +(* SUBSETS + - We use predicative subsets coded as propositional functions + according to G.Sambin and S.Valentini "Toolbox" +*) + +definition Subset \def \lambda (D:Domain). D \to Prop. + +(* subset membership (epsilon) *) +definition sin : \forall D. Subset D \to D \to Prop \def + \lambda (D:Domain). \lambda U,d. cin D d \and U d. + +(* subset top (full subset) *) +definition stop \def \lambda (D:Domain). true_f D. + +(* subset bottom (empty subset) *) +definition sbot \def \lambda (D:Domain). false_f D. + +(* subset and (binary intersection) *) +definition sand: \forall D. Subset D \to Subset D \to Subset D \def + \lambda D,U1,U2,d. U1 d \land U2 d. + +(* subset or (binary union) *) +definition sor: \forall D. Subset D \to Subset D \to Subset D \def + \lambda D,U1,U2,d. U1 d \lor U2 d. + +(* subset less or equal (inclusion) *) +definition sle: \forall D. Subset D \to Subset D \to Prop \def + \lambda D,U1,U2. \iforall d. U1 d \to U2 d. + +(* subset overlap *) +definition sover: \forall D. Subset D \to Subset D \to Prop \def + \lambda D,U1,U2. \iexists d. U1 d \land U2 d. + +(* coercions **************************************************************) + +(* +(* the class of the subsets of a domain (not an implicit coercion) *) +definition class_of_subsets_of \def + \lambda D. mk_Class (Subset D) (true_f ?) (sle ?). +*) + +(* the domain built upon a subset (not an implicit coercion) *) +definition domain_of_subset: \forall D. Subset D \to Domain \def + \lambda (D:Domain). \lambda U. + mk_Domain (mk_Class D (sin D U) (cle1 D)). + +(* the full subset of a domain *) +coercion stop.