| Cic.Const (u,exp_named_subst) ->
UriManagerSet.singleton u
| Cic.MutInd (u, t, exp_named_subst) ->
+ let rec projections_of uris =
+ List.flatten
+ (List.map
+ (fun uri ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ projections_of (CicUtil.projections_of_record o uri))
+ uris)
+ in
let uri = UriManager.uri_of_uriref u t None in
- UriManagerSet.singleton uri
+ List.fold_right UriManagerSet.add
+ (projections_of [u]) (UriManagerSet.singleton uri)
| Cic.MutConstruct (u, t, c, exp_named_subst) ->
let uri = UriManager.uri_of_uriref u t (Some c) in
- UriManagerSet.singleton uri
+ UriManagerSet.singleton uri
| Cic.Cast (t, _) -> signature_concl t
| Cic.Prod (_, s, t) ->
UriManagerSet.union (signature_concl s) (signature_concl t)
try
let ty' = unfold context ty in
if is_an_equality ty' then Some(t,ty') else None
- with _ -> None) (* catturare l'eccezione giusta di unfold *)
+ with ProofEngineTypes.Fail _ -> None)
equations
in
let bag = Equality.mk_equality_bag () in
| (m, s, _, _, [],_)::orlist ->
(* complete success *)
Proved (m, s, orlist, tables, cache, maxm)
- | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist ->
+ | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
+ when not flags.AutoTypes.do_types ->
(* skip since not Prop, don't even check if closed by side-effect *)
aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
| (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
(* timeout *)
debug_print (lazy ("FAIL: TIMEOUT"));
Gaveup (tables, cache, maxm)
- | (m, s, size, don, (D (gno,depth,P as g))::todo, fl)::orlist as status ->
+ | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
(* attack g *)
match calculate_goal_ty g s m with
| None ->
let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
let size = int "size" ((AutoTypes.default_flags()).AutoTypes.maxsize) in
let gsize = int "gsize" ((AutoTypes.default_flags()).AutoTypes.maxgoalsizefactor) in
+ let do_type = bool "type" false in
let timeout = int "timeout" 0 in
{ AutoTypes.maxdepth =
if use_only_paramod then 2 else depth;
AutoTypes.close_more = close_more;
AutoTypes.dont_cache_failures = false;
AutoTypes.maxgoalsizefactor = gsize;
+ AutoTypes.do_types = do_type;
}
let applyS_tac ~dbd ~term ~params ~universe =
ProofEngineTypes.tactic
type auto_status =
- Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
+ Cic.context *
+ (* or list: goalno, goaltype, grey, depth, candidates: (goalno, c) *)
+ (int * Cic.term * bool * int * (int * Cic.term) list) list *
+ (* and list *)
(int * Cic.term * int) list *
+ (* last moves *)
Cic.term list
+
val get_auto_status : unit -> auto_status
val pause: bool -> unit
val step : unit -> unit
use_only_paramod : bool;
close_more : bool;
dont_cache_failures: bool;
+ do_types: bool;
}
let default_flags _ =
use_paramod=true;
use_only_paramod=false;
close_more=false;
- dont_cache_failures=false}
+ dont_cache_failures=false;
+ do_types=false;
+}
;;
(* (metasenv, subst, (metano,depth)list *)
use_paramod: bool;
use_only_paramod : bool;
close_more : bool;
- dont_cache_failures: bool
+ dont_cache_failures: bool;
+ do_types: bool;
}
val default_flags : unit -> flags
intros (E); unfold; intros (x); apply ap_coreflexive;
qed.
-lemma eq_symmetric:∀E.symmetric ? (eq E).
+lemma eq_sym_:∀E.symmetric ? (eq E).
intros (E); unfold; intros (x y Exy); unfold; unfold; intros (Ayx); apply Exy;
apply ap_symmetric; assumption;
qed.
-lemma eq_symmetric_:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x := eq_symmetric.
+lemma eq_sym:∀E:apartness.∀x,y:E.x ≈ y → y ≈ x := eq_sym_.
-coercion cic:/matita/excedence/eq_symmetric_.con.
+coercion cic:/matita/excedence/eq_sym.con.
-lemma eq_transitive_: ∀E.transitive ? (eq E).
+lemma eq_trans_: ∀E.transitive ? (eq E).
(* bug. intros k deve fare whd quanto basta *)
intros 6 (E x y z Exy Eyz); intro Axy; cases (ap_cotransitive ???y Axy);
[apply Exy|apply Eyz] assumption.
qed.
-lemma eq_transitive:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_transitive_.
+lemma eq_trans:∀E:apartness.∀x,y,z:E.x ≈ y → y ≈ z → x ≈ z ≝ eq_trans_.
(* BUG: vedere se ricapita *)
lemma le_antisymmetric: ∀E.antisymmetric ? (le E) (eq ?).
(* generation of coercions to make *_rew[lr] easier *)
lemma feq_plusr_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → y+x ≈ z+x.
-compose feq_plusr with eq_symmetric_ (H); apply H; assumption;
+compose feq_plusr with eq_sym (H); apply H; assumption;
qed.
coercion cic:/matita/groups/feq_plusr_sym_.con nocomposites.
lemma feq_plusl_sym_: ∀G:abelian_group.∀x,y,z:G.z ≈ y → x+y ≈ x+z.
-compose feq_plusl with eq_symmetric_ (H); apply H; assumption;
+compose feq_plusl with eq_sym (H); apply H; assumption;
qed.
coercion cic:/matita/groups/feq_plusl_sym_.con nocomposites.
lemma fap_plusr: ∀G:abelian_group.∀x,y,z:G. y # z → y+x # z+x.
intros (G x y z Ayz); apply (plus_strong_extr ? (-x));
apply (ap_rewl ??? (y + (x + -x)));
-[1: apply (eq_symmetric ??? (plus_assoc ????));
+[1: apply (eq_sym ??? (plus_assoc ????));
|2: apply (ap_rewr ??? (z + (x + -x)));
- [1: apply (eq_symmetric ??? (plus_assoc ????));
+ [1: apply (eq_sym ??? (plus_assoc ????));
|2: apply (ap_rewl ??? (y + (-x+x)) (plus_comm ? x (-x)));
apply (ap_rewl ??? (y + 0) (opp_inverse ??));
apply (ap_rewl ??? (0 + y) (plus_comm ???));
theorem eq_opp_plus_plus_opp_opp:
∀G:abelian_group.∀x,y:G. -(x+y) ≈ -x + -y.
intros (G x y); apply (plus_cancr ??? (x+y));
-apply (eq_transitive ?? 0 ? (opp_inverse ??));
-apply (eq_transitive ?? (-x + -y + x + y)); [2: apply (eq_symmetric ??? (plus_assoc ????))]
-apply (eq_transitive ?? (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm]
-apply (eq_transitive ?? (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;]
-apply (eq_transitive ?? (-y + 0 + y));
- [2: apply feq_plusr; apply feq_plusl; apply eq_symmetric; apply opp_inverse]
-apply (eq_transitive ?? (-y + y));
- [2: apply feq_plusr; apply eq_symmetric;
- apply (eq_transitive ?? (0+-y)); [apply plus_comm|apply zero_neutral]]
-apply eq_symmetric; apply opp_inverse.
+apply (eq_trans ?? 0 ? (opp_inverse ??));
+apply (eq_trans ?? (-x + -y + x + y)); [2: apply (eq_sym ??? (plus_assoc ????))]
+apply (eq_trans ?? (-y + -x + x + y)); [2: repeat apply feq_plusr; apply plus_comm]
+apply (eq_trans ?? (-y + (-x + x) + y)); [2: apply feq_plusr; apply plus_assoc;]
+apply (eq_trans ?? (-y + 0 + y));
+ [2: apply feq_plusr; apply feq_plusl; apply eq_sym; apply opp_inverse]
+apply (eq_trans ?? (-y + y));
+ [2: apply feq_plusr; apply eq_sym;
+ apply (eq_trans ?? (0+-y)); [apply plus_comm|apply zero_neutral]]
+apply eq_sym; apply opp_inverse.
qed.
theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x.
intros (G x); apply (plus_cancl ??? (-x));
-apply (eq_transitive ?? (--x + -x)); [apply plus_comm]
-apply (eq_transitive ?? 0); [apply opp_inverse]
-apply eq_symmetric; apply opp_inverse;
+apply (eq_trans ?? (--x + -x)); [apply plus_comm]
+apply (eq_trans ?? 0); [apply opp_inverse]
+apply eq_sym; apply opp_inverse;
qed.
theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption]
intro G; apply (plus_cancr ??? 0);
-apply (eq_transitive ?? 0); [apply zero_neutral;]
-apply eq_symmetric; apply opp_inverse;
+apply (eq_trans ?? 0); [apply zero_neutral;]
+apply eq_sym; apply opp_inverse;
qed.
+
+lemma feq_oppr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x ≈ -y → x ≈ -z.
+intros (G x y z H1 H2); apply (plus_cancr ??? z);
+apply (eq_trans ?? 0 ?? (opp_inverse ?z));
+apply (eq_trans ?? (-y + z) ? H2);
+apply (eq_trans ?? (-y + y) ? H1);
+apply (eq_trans ?? 0 ? (opp_inverse ??));
+apply eq_reflexive;
+qed.
+
+lemma feq_oppl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → -y ≈ x → -z ≈ x.
+intros (G x y z H1 H2); apply eq_sym; apply (feq_oppr ??y);
+[2:apply eq_sym] assumption;
+qed.
+
+lemma eq_opp: ∀G:abelian_group.∀x,y:G. x ≈ y → -x ≈ -y.
+intros (G x y H); apply (feq_oppl ??y ? H); apply eq_reflexive;
+qed.
+
+coercion cic:/matita/groups/eq_opp.con nocomposites.
+
+lemma eq_opp_sym: ∀G:abelian_group.∀x,y:G. y ≈ x → -x ≈ -y.
+compose eq_opp with eq_sym (H); apply H; assumption;
+qed.
+
+coercion cic:/matita/groups/eq_opp_sym.con nocomposites.
+
+lemma eq_opp_plusr: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(x + z) ≈ -(y + z).
+compose feq_plusr with eq_opp(H); apply H; assumption;
+qed.
+
+coercion cic:/matita/groups/eq_opp_plusr.con nocomposites.
+
+lemma eq_opp_plusl: ∀G:abelian_group.∀x,y,z:G. x ≈ y → -(z + x) ≈ -(z + y).
+compose feq_plusl with eq_opp(H); apply H; assumption;
+qed.
+
+coercion cic:/matita/groups/eq_opp_plusl.con nocomposites.
+++ /dev/null
-matita-0.4.97.tar.gz
\ No newline at end of file
+++ /dev/null
-- manpages have wrong patch for conffile
-- hide:
- - publish
- - hbugs in cicbrowser
- - light bulb
+++ /dev/null
-matita (0.4.97-1) unstable; urgency=low
-
- * New version svn tag 0.4.96.
-
- -- Enrico Tassi <gareuselesinge@debian.org> Fri, 16 Nov 2007 20:37:55 +0100
-
-matita (0.4.96-1) unstable; urgency=low
-
- * First upload of svn tag 0.4.96 (Closes: #448156).
-
- -- Enrico Tassi <gareuselesinge@debian.org> Fri, 26 Oct 2007 11:25:03 +0200
-
+++ /dev/null
-Source: matita
-Section: math
-Priority: optional
-Maintainer: Enrico Tassi <gareuselesinge@debian.org>
-Uploaders: Stefano Zacchiroli <zack@debian.org>
-Homepage: http://matita.cs.unibo.it
-Build-Depends: ocaml (>= 3.10.0), ocaml-findlib, libgdome2-ocaml-dev, liblablgtk2-ocaml-dev, liblablgtkmathview-ocaml-dev, liblablgtksourceview-ocaml-dev, libsqlite3-ocaml-dev, libocamlnet-ocaml-dev, libzip-ocaml-dev, libhttp-ocaml-dev, ocaml-ulex08, libexpat-ocaml-dev, debhelper, cdbs, libmysql-ocaml-dev, camlp5, dpatch, help2man
-Standards-Version: 3.7.2
-XS-Vcs-Svn: svn://mowgli.cs.unibo.it/trunk/helm/software/pkg-matita/trunk/
-XS-Vcs-Browser: http://helm.cs.unibo.it/websvn/listing.php?path=/trunk/helm/software/pkg-matita/trunk/
-
-Package: matita
-Architecture: any
-Depends: ${shlibs:Depends}
-Recommends: matita-standard-library, graphviz
-Description: interactive theorem prover
- Matita is a graphical interactive theorem prover based on the Calculus of
- (Co)Inductive Constructions.
- .
- Matita adopts XML-encoded proof objects are produced for storage and exchange.
- This makes it compatible, at some extent, with Coq.
- .
- The graphical interface has been inspired by CtCoq and Proof General. It
- supports high quality bidimensional rendering of proofs and formulae
- transformed on-the-fly to MathML markup
-
-Package: matita-standard-library
-Architecture: all
-Depends: matita (= ${binary:Version})
-Description: standard library for the Matita interactive theorem prover
- Matita is a graphical interactive theorem prover based on the Calculus of
- (Co)Inductive Constructions.
- .
- This package contains the standard library of theorems of the
- matita interactive theorem prover.
+++ /dev/null
-This package was debianized by Enrico Tassi <gareuselesinge@debian.org>
-Wed Oct 17 17:48:32 CEST 2007.
-
-It was downloaded from http://matita.cs.unibo.it.
-
-Copyright © 2000-2007 The Matita Team.
-The software is released under the terms of the GNU/GPL license.
-See /usr/share/common-licenses/GPL
-
-File components/extlib/trie.ml:
-Copyright (C) 2000 Jean-Christophe FILLIATRE
-Released under LGPL version 2
-See /usr/share/common-licenses/LGPL-2
-
-File components/syntax_extensions/data/dictionary-tex.xml:
-Copyright (C) 2002-2003 Luca Padovani <lpadovan@cs.unibo.it>,
- 2003 Paolo Marinelli <pmarinel@cs.unibo.it>.
-Released under LGPL version 2.1
-See /usr/share/common-licenses/LGPL-2.1
-
-All .ma files are released under LGPL version 2.1
-See /usr/share/common-licenses/LGPL-2.1
-
-Files components/tactics/setoids.ml, components/tactics/setoids.mli and
-components/tactics/fourier.ml are part of The Coq Proof Assistant
-Copyright (C) The Coq Development Team
-Released under LGPL version 2.1
-See /usr/share/common-licenses/LGPL-2.1
-
+++ /dev/null
-/usr/share/matita/ma/
-/usr/share/matita/xml/
+++ /dev/null
-/usr/share/matita/ma/
-/usr/share/matita/xml/
-/usr/share/matita/metadata.db
+++ /dev/null
-/usr/bin
-/usr/share/matita/
+++ /dev/null
-usr/share/matita/help
-usr/share/matita/icons
-usr/share/matita/AUTHORS
-usr/share/matita/LICENSE
-usr/share/matita/*.xml
-usr/share/matita/*.in
-usr/share/matita/*.lang
-usr/share/matita/*.gtkrc
-usr/share/matita/*.moo
-usr/share/matita/*.templ
-usr/share/matita/matita usr/bin/
-usr/share/matita/matitac usr/bin/
-usr/share/matita/matitamake usr/bin/
-usr/share/matita/matitadep usr/bin/
-usr/share/matita/matitaclean usr/bin/
-usr/share/man/* usr/share/man/
+++ /dev/null
-?package(matita):needs="X11" \
- section="Applications/Science/Mathematics" \
- title="Matita" \
- longtitle="Matita interactive theorem prover" \
- command="/usr/bin/matita" \
- icon="/usr/share/matita/icons/matita-32.xpm"
+++ /dev/null
-conf_debianonly=1
-conf_origtargzpath=../tarballs/
+++ /dev/null
-matita.conf.xml.in.dpatch
+++ /dev/null
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## matita.conf.xml.in.dpatch by Enrico Tassi <gareuselesinge@debian.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: No description.
-
-@DPATCH@
-diff -urNad trunk~/matita/matita.conf.xml.in trunk/matita/matita.conf.xml.in
---- trunk~/matita/matita.conf.xml.in 2007-10-29 17:13:47.000000000 +0100
-+++ trunk/matita/matita.conf.xml.in 2007-11-07 15:57:56.000000000 +0100
-@@ -49,17 +49,17 @@
- <!-- The following snippet is used by the helm team
- note that user's tables are named diffrently from library tables,
- so they can coexists on the same db -->
--
-+<!--
- <key name="metadata">@DBHOST@ matita helm none legacy</key>
- <key name="metadata">@DBHOST@ public helm none library</key>
- <key name="metadata">@DBHOST@ matita helm none user</key>
--
-+-->
- <!-- The following snippet it what you want to use a local sqlite db
- and acess remotely to the coq library trought mowgli
- <key name="metadata">@DBHOST@ matita helm none legacy</key>
-+-->
- <key name="metadata">file://$(matita.rt_base_dir) metadata.db helm helm library</key>
- <key name="metadata">file://$(matita.basedir) user.db helm helm user</key>
-- -->
-
- <!--
- If you have a large amount of metadata, you may be interested in using
-@@ -90,11 +90,13 @@
- (e.g. the Matita standard library)
- "legacy" implies "ro"
- -->
-+<!--
- <key name="prefix">
- cic:/matita/
- file:///projects/helm/library/matita_contribs/matita
- ro
- </key>
-+-->
- <key name="prefix">
- cic:/matita/
- file://$(matita.rt_base_dir)/xml/standard-library/
-@@ -104,6 +106,7 @@
- cic:/matita/
- file://$(user.home)/.matita/xml/matita/
- </key>
-+<!--
- <key name="prefix">
- cic:/
- file://@RT_BASE_DIR@/xml/legacy-library/coq/
-@@ -119,5 +122,6 @@
- http://mowgli.cs.unibo.it/xml/
- legacy
- </key>
-+-->
- </section>
- </helm_registry>
+++ /dev/null
-#!/usr/bin/make -f
-
-include /usr/share/cdbs/1/class/makefile.mk
-include /usr/share/cdbs/1/class/autotools.mk
-include /usr/share/cdbs/1/rules/debhelper.mk
-include /usr/share/cdbs/1/rules/dpatch.mk
-
-DEB_CONFIGURE_EXTRA_FLAGS := \
- --with-runtime-dir=/usr/share/matita \
- --prefix=/usr/ \
- --with-dbhost=FAKE_HOST
-DEB_DESTDIR := debian/tmp/
-DEB_DH_INSTALL_SOURCEDIR := $(DEB_DESTDIR)
-# don't perform regular installation
-DEB_MAKE_INSTALL_TARGET :=
-
-common-install-arch::
- # install matita
- make install-arch DESTDIR=$(DEB_DESTDIR) MATITA_CFLAGS=-noinnertypes
- # generate manpages
- mkdir -p $(DEB_DESTDIR)/usr/share/man/man1/
- MATITA_RT_BASE_DIR=debian/tmp/usr/share/matita/ \
- help2man --name="Matita interative theorem prover - batch compiler" -N \
- $(DEB_DESTDIR)/usr/share/matita/matitac \
- | gzip -9 > $(DEB_DESTDIR)/usr/share/man/man1/matitac.1.gz
- MATITA_RT_BASE_DIR=debian/tmp/usr/share/matita/ \
- help2man --name="Matita interative theorem prover - build tool" -N \
- $(DEB_DESTDIR)/usr/share/matita/matitamake \
- | gzip -9 > $(DEB_DESTDIR)/usr/share/man/man1/matitamake.1.gz
- MATITA_RT_BASE_DIR=debian/tmp/usr/share/matita/ \
- help2man --name="Matita interative theorem prover - cleanup tool" -N \
- $(DEB_DESTDIR)/usr/share/matita/matitaclean \
- | gzip -9 > $(DEB_DESTDIR)/usr/share/man/man1/matitaclean.1.gz
- MATITA_RT_BASE_DIR=debian/tmp/usr/share/matita/ \
- help2man --name="Matita interative theorem prover - dependency analyzer" -N \
- $(DEB_DESTDIR)/usr/share/matita/matitadep \
- | gzip -9 > $(DEB_DESTDIR)/usr/share/man/man1/matitadep.1.gz
- if [ -e $(DEB_DESTDIR)/usr/share/matita/matitac.opt ]; then\
- ln -s /usr/share/man/man1/matitac.1.gz \
- $(DEB_DESTDIR)/usr/share/man/man1/matitac.opt.1.gz;\
- fi
- # install .opt .byte (symlinks are installed with .install
- mkdir -p debian/matita/usr/bin/
- cp matita/matita.byte debian/matita/usr/bin/ || true
- cp matita/matitac.byte debian/matita/usr/bin/ || true
- cp matita/matita.opt debian/matita/usr/bin/ || true
- cp matita/matitac.opt debian/matita/usr/bin/ || true
-
-common-install-indep::
- # install matita library
- make install-indep DESTDIR=$(DEB_DESTDIR) MATITA_CFLAGS=-noinnertypes
- # innerypes removal
- # find $(DEB_DESTDIR) -name \*.xml.types.gz -exec rm {} \;
projects / helm.git / commitdiff