--- /dev/null
+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) | $<
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
(* *)
(**************************************************************************)
-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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="matita">
+ <key name="rt_base_dir">$(MATITA_RT_BASE_DIR)</key>
+ </section>
+ <section name="xoa">
+ <key name="output_dir">contribs/lambda/</key>
+ <key name="objects">xoa</key>
+ <key name="notations">xoa_notation</key>
+ <key name="include">basics/pts.ma</key>
+ <key name="ex">2 1</key>
+ <key name="ex">3 2</key>
+ </section>
+</helm_registry>
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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) }.
+
projects / helm.git / commitdiff