From e5287c72c8b3ac246a23b17efe6cb2576b91d3c4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 20 Sep 2015 18:49:03 +0000 Subject: [PATCH] limits: we set up a different foundation lambdadelta: Makefile updated for new version of probe --- matita/matita/contribs/lambdadelta/Makefile | 4 +- matita/matita/contribs/limits/Makefile | 30 ++++++++++++++ matita/matita/contribs/limits/u0_class.ma | 34 +++++++++++++++ .../matita/contribs/limits/u0_predicates.ma | 41 +++++++++++++++++++ 4 files changed, 107 insertions(+), 2 deletions(-) create mode 100644 matita/matita/contribs/limits/Makefile create mode 100644 matita/matita/contribs/limits/u0_class.ma create mode 100644 matita/matita/contribs/limits/u0_predicates.ma diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 064c24db9..f3d8b3232 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -25,7 +25,7 @@ MAC_OPTS := PRB_DIR := ../../../components/binaries/probe PRB := probe.native -PRB_OPTS := $(XOA_OPTS) -g +PRB_OPTS := $(XOA_OPTS) -g -i ORIG := . ./orig.sh ORIGS := basic_2/basic_1.orig @@ -52,7 +52,7 @@ define MAS_TEMPLATE $(1)/$(1)_probe.txt: $$(MAS_$(1)) @echo " PROBE $(1)" - $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -on -i > $$@ + $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -on -c > $$@ $(1)/$(1)_mac.txt: $$(MAS_$(1)) @echo " MAC $(1)" diff --git a/matita/matita/contribs/limits/Makefile b/matita/matita/contribs/limits/Makefile new file mode 100644 index 000000000..c5a88d110 --- /dev/null +++ b/matita/matita/contribs/limits/Makefile @@ -0,0 +1,30 @@ +H := @ + +ALPHA_DIR ?= $(HOME)/mps/ocamlbuild/alpha +ALPHA = alpha.native + +MATITAC = ../../matitac.opt + +PRB_DIR := ../../../components/binaries/probe +PRB := probe.native +PRB_OPTS := ../../matita.conf.xml -g -i + +AMAS = $(wildcard *.ama) + +all: $(AMAS:%.ama=%.ma) + @$(MATITAC) + +clean: + $(H)$(RM) *~ + +clean_all: clean + $(H)$(RM) $(AMAS:%.ama=%.ma) + +probe: + @echo PROBE . + $(H)$(PRB_DIR)/$(PRB) $(PRB_OPTS) . + +.PHONY: all clean clean_all probe + +%.ma: %.ama + $(H)$(ALPHA_DIR)/$(ALPHA) < $< > $@ diff --git a/matita/matita/contribs/limits/u0_class.ma b/matita/matita/contribs/limits/u0_class.ma new file mode 100644 index 000000000..49c715a01 --- /dev/null +++ b/matita/matita/contribs/limits/u0_class.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "u0_predicates.ma". + +(* CLASSES ************************************************************) + +record u0_class: Type[1] ≝ { + u0_class_t :> Type[0]; + u0_class_in: u0_predicate1 u0_class_t; + u0_class_eq: u0_predicate2 u0_class_t +}. + +interpretation "u0 class membership" 'mem a C = (u0_class_in C a). + +definition u0_class_all: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∀a. a ∈ C → P a. + +definition u0_class_ex: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∃a. a ∈ C ∧ P a. + +record is_u0_class (C:u0_class): Prop ≝ { + u0_class_repl1: can_u0_replace1 C (u0_class_all C) (u0_class_eq C) (u0_class_in C); + u0_class_refl : is_u0_reflexive C (u0_class_all C) (u0_class_eq C) +}. diff --git a/matita/matita/contribs/limits/u0_predicates.ma b/matita/matita/contribs/limits/u0_predicates.ma new file mode 100644 index 000000000..13650cfde --- /dev/null +++ b/matita/matita/contribs/limits/u0_predicates.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "preamble.ma". + +(* RELATIONS **********************************************************) + +definition u0_predicate1: Type[0] → Type[1] ≝ λT.T → Prop. + +definition u0_predicate2: Type[0] → Type[1] ≝ λT.T → u0_predicate1 T. + +definition u1_predicate1: Type[1] → Type[2] ≝ λT.T → Prop. + +definition u0_quantifier: Type[0] → Type[2] ≝ λT. u1_predicate1 (u0_predicate1 T). + +record is_u0_reflexive (T:Type[0]) (All:u0_quantifier T) (R:u0_predicate2 T): Prop ≝ +{ + u0_refl: All (λa. R a a) +}. + +record can_u0_replace1 (T:Type[0]) (All:u0_quantifier T) (Q:u0_predicate2 T) (R:u0_predicate1 T): Prop ≝ +{ + u0_repl1: All (λa. R a → All (λb. Q b a → R b)) +}. +(* +record can_u0_replac2 (T:Type[0]) (All:u0_quantifier T) (Q:u0_predicate2 T) (R:u0_predicate2 T): Prop ≝ +{ + u0_reflexivity: All (λa. R a a) +}. +*) -- 2.39.2