From 2b51cf74b9a5f37d0f91780ceae4b8f4d0ee38a1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 23 Nov 2012 17:27:38 +0000 Subject: [PATCH] the theory of substitution is started ... --- matita/matita/contribs/lambda/Makefile | 29 ++++++++ matita/matita/contribs/lambda/lift.ma | 69 +++++++++++++++++++ matita/matita/contribs/lambda/preamble.ma | 33 +++++++++ matita/matita/contribs/lambda/term.ma | 39 ++++++----- matita/matita/contribs/lambda/trichotomy.ma | 42 +++++++++++ matita/matita/contribs/lambda/xoa.conf.xml | 14 ++++ matita/matita/contribs/lambda/xoa.ma | 34 +++++++++ matita/matita/contribs/lambda/xoa_notation.ma | 36 ++++++++++ 8 files changed, 279 insertions(+), 17 deletions(-) create mode 100644 matita/matita/contribs/lambda/Makefile create mode 100644 matita/matita/contribs/lambda/lift.ma create mode 100644 matita/matita/contribs/lambda/preamble.ma create mode 100644 matita/matita/contribs/lambda/trichotomy.ma create mode 100644 matita/matita/contribs/lambda/xoa.conf.xml create mode 100644 matita/matita/contribs/lambda/xoa.ma create mode 100644 matita/matita/contribs/lambda/xoa_notation.ma diff --git a/matita/matita/contribs/lambda/Makefile b/matita/matita/contribs/lambda/Makefile new file mode 100644 index 000000000..cc3a3bf91 --- /dev/null +++ b/matita/matita/contribs/lambda/Makefile @@ -0,0 +1,29 @@ +H = @ +XOA_DIR = ../../../components/binaries/xoa +XOA = xoa.native +DEP_DIR = ../../../components/binaries/matitadep +DEP = matitadep.native +MAC_DIR = ../../../components/binaries/mac +MAC = mac.native + +XOA_CONF = xoa.conf.xml +XOA_TARGETS = xoa_notation.ma xoa.ma + +all: xoa + $(H)../../matitac.opt + +# xoa ######################################################################## + +xoa: $(XOA_TARGETS) + +$(XOA_TARGETS): $(XOA_CONF) + @echo " EXEC $(XOA) $(XOA_CONF)" + $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA_CONF) + +# dep ######################################################################## + +deps: MAS = $(shell find $* -name "*.ma") + +deps: $(DEP_DIR)/$(DEP) + @echo " MATITADEP" + $(H)grep "include \"" $(MAS) | $< diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/lift.ma new file mode 100644 index 000000000..4383713e7 --- /dev/null +++ b/matita/matita/contribs/lambda/lift.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "trichotomy.ma". +include "term.ma". + +(* RELOCATION ***************************************************************) + +(* Policy: depth (level) metavariables: d, e + height metavariables : h, k +*) +(* Note: indexes start at zero *) +let rec lift d h M on M ≝ match M with +[ VRef i ⇒ #(tri … i d i (i + h) (i + h)) +| Abst A ⇒ 𝛌. (lift (d+1) h A) +| Appl B A ⇒ @(lift d h B). (lift d h A) +]. + +interpretation "relocation" 'Lift d h M = (lift d h M). + +notation "hvbox( ↑ [ d , break h ] break term 55 M )" + non associative with precedence 55 + for @{ 'Lift $d $h $M }. + +notation > "hvbox( ↑ [ h ] break term 55 M )" + non associative with precedence 55 + for @{ 'Lift 0 $h $M }. + +notation > "hvbox( ↑ term 55 M )" + non associative with precedence 55 + for @{ 'Lift 0 1 $M }. + +lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i. +normalize /3 width=1/ +qed. + +lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h). +#d #h #i #H elim (le_to_or_lt_eq … H) -H +normalize // /3 width=1/ +qed. + +lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C → + ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A. +#C #d #h * normalize +[ #i #H destruct +| #A #H destruct /2 width=3/ +| #B #A #H destruct +] +qed-. + +lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C → + ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A. +#D #C #d #h * normalize +[ #i #H destruct +| #A #H destruct +| #B #A #H destruct /2 width=5/ +] +qed-. diff --git a/matita/matita/contribs/lambda/preamble.ma b/matita/matita/contribs/lambda/preamble.ma new file mode 100644 index 000000000..53a433d40 --- /dev/null +++ b/matita/matita/contribs/lambda/preamble.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 *) +(* *) +(**************************************************************************) + +include "arithmetics/nat.ma". + +include "xoa_notation.ma". +include "xoa.ma". + +(* Note: For some reason this cannot be in the standard library *) +interpretation "logical false" 'false = False. + +notation "⊥" + non associative with precedence 90 + for @{'false}. + +lemma lt_refl_false: ∀n. n < n → ⊥. +#n #H elim (lt_to_not_eq … H) -H /2 width=1/ +qed-. + +lemma lt_zero_false: ∀n. n < 0 → ⊥. +#n #H elim (lt_to_not_le … H) -H /2 width=1/ +qed-. diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma index 80a1de667..7710c05fb 100644 --- a/matita/matita/contribs/lambda/term.ma +++ b/matita/matita/contribs/lambda/term.ma @@ -12,37 +12,42 @@ (* *) (**************************************************************************) -include "arithmetics/nat.ma". +(* Initial invocation: - Patience on us to gain peace and perfection! - *) + +include "preamble.ma". + +(* TERM STRUCTURE ***********************************************************) (* Policy: term metavariables: A, B, C, D - de Bruijn indexes : i, j, h, k + de Bruijn indexes : i, j *) inductive term: Type[0] ≝ -| VRef: nat → term (* variable reference by index, starts at zero *) -| Abst: term → term (* function formation *) -| Appl: term → term → term (* function application, argument comes first *) +| VRef: nat → term (* variable reference by index *) +| Abst: term → term (* function formation *) +| Appl: term → term → term (* function application *) . +interpretation "term construction (variable reference by index)" + 'VariableReferenceByIndex i = (VRef i). + +interpretation "term construction (abstraction)" + 'Abstraction A = (Abst A). + +interpretation "term construction (application)" + 'Application C A = (Appl C A). + notation "hvbox( # term 90 i )" non associative with precedence 55 for @{ 'VariableReferenceByIndex $i }. -interpretation "term construction (variable reference by index)" - 'VariableReferenceByIndex i = (VRef i). - -notation "hvbox( 𝛌 term 55 A )" +notation "hvbox( 𝛌 . term 55 A )" non associative with precedence 55 for @{ 'Abstraction $A }. -interpretation "term construction (abstraction)" - 'Abstraction A = (Abst A). +notation > "hvbox( 𝛌 term 55 A )" + non associative with precedence 55 + for @{ 'Abstraction $A }. notation "hvbox( @ term 55 C . break term 55 A )" non associative with precedence 55 for @{ 'Application $C $A }. - -interpretation "term construction (application)" - 'Application C A = (Appl C A). - -lemma prova_notazione: ∀A,i. @A.𝛌#i = @A.𝛌#i. -// qed-. diff --git a/matita/matita/contribs/lambda/trichotomy.ma b/matita/matita/contribs/lambda/trichotomy.ma new file mode 100644 index 000000000..52dc027d4 --- /dev/null +++ b/matita/matita/contribs/lambda/trichotomy.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 *) +(* *) +(**************************************************************************) + +include "preamble.ma". + +(* TRICHOTOMY OPERATOR ******************************************************) + +(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *) +let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝ + match n1 with + [ O ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ] + | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ] + ]. + +lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1. +#A #a1 #a2 #a3 #n2 elim n2 -n2 +[ #n1 #H elim (lt_zero_false … H) +| #n2 #IH #n1 elim n1 -n1 // /3 width=1/ +] +qed. + +lemma tri_eq: ∀A,a1,a2,a3,n. tri A n n a1 a2 a3 = a2. +#A #a1 #a2 #a3 #n elim n -n normalize // +qed. + +lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3. +#A #a1 #a2 #a3 #n1 elim n1 -n1 +[ #n2 #H elim (lt_zero_false … H) +| #n1 #IH #n2 elim n2 -n2 // /3 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml new file mode 100644 index 000000000..72b1258bd --- /dev/null +++ b/matita/matita/contribs/lambda/xoa.conf.xml @@ -0,0 +1,14 @@ + + +
+ $(MATITA_RT_BASE_DIR) +
+
+ contribs/lambda/ + xoa + xoa_notation + basics/pts.ma + 2 1 + 3 2 +
+ diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/xoa.ma new file mode 100644 index 000000000..4e6e6aed9 --- /dev/null +++ b/matita/matita/contribs/lambda/xoa.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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +(* multiple existental quantifier (2, 1) *) + +inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝ + | ex2_1_intro: ∀x0. P0 x0 → P1 x0 → ex2_1 ? ? ? +. + +interpretation "multiple existental quantifier (2, 1)" 'Ex P0 P1 = (ex2_1 ? P0 P1). + +(* multiple existental quantifier (3, 2) *) + +inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ + | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). + diff --git a/matita/matita/contribs/lambda/xoa_notation.ma b/matita/matita/contribs/lambda/xoa_notation.ma new file mode 100644 index 000000000..b6498bb76 --- /dev/null +++ b/matita/matita/contribs/lambda/xoa_notation.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (2, 1) *) + +notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) }. + +notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) }. + +(* multiple existental quantifier (3, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. + -- 2.39.2