--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* THE FORMAL SYSTEM λδ - MATITA SOURCE SCRIPTS
+ * Specification started: 2011 April 17
+ * - Patience on me so that I gain peace and perfection! -
+ * [ suggested invocation to start formal specifications with ]
+ *)
+
+include "Ground-2/ground.ma".
+include "Basic-2/notation.ma".
+
+(* BINARY ITEMS *************************************************************)
+
+(* binary binding items *)
+inductive bind2: Type[0] ≝
+| Abbr: bind2 (* abbreviation *)
+| Abst: bind2 (* abstraction *)
+.
+
+(* binary non-binding items *)
+inductive flat2: Type[0] ≝
+| Appl: flat2 (* application *)
+| Cast: flat2 (* explicit type annotation *)
+.
+
+(* binary items *)
+inductive item2: Type[0] ≝
+| Bind: bind2 → item2 (* binding item *)
+| Flat: flat2 → item2 (* non-binding item *)
+.
+
+coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2.
+
+coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2.
--- /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 "Basic-2/grammar/term.ma".
+
+(* LOCAL ENVIRONMENTS *******************************************************)
+
+(* local environments *)
+inductive lenv: Type[0] ≝
+| LSort: lenv (* empty *)
+| LPair: lenv → bind2 → term → lenv (* binary binding construction *)
+.
+
+interpretation "sort (local environment)" 'Star = LSort.
+
+interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T).
--- /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 "Basic-2/grammar/lenv.ma".
+
+(* LENGTH *******************************************************************)
+
+(* the length of a local environment *)
+let rec length L ≝ match L with
+[ LSort ⇒ 0
+| LPair L _ _ ⇒ length L + 1
+].
+
+interpretation "length (local environment)" 'card L = (length L).
--- /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 "Basic-2/grammar/term_weight.ma".
+include "Basic-2/grammar/lenv.ma".
+
+(* WEIGHTS ******************************************************************)
+
+(* the weight of a local environment *)
+let rec lw L ≝ match L with
+[ LSort ⇒ 0
+| LPair L _ V ⇒ lw L + #V
+].
+
+interpretation "weight (local environment)" 'Weight L = (lw L).
+
+(* the weight of a closure *)
+definition cw: lenv → term → ? ≝ λL,T. #L + #T.
+
+interpretation "weight (closure)" 'Weight L T = (cw L T).
+
+axiom cw_wf_ind: ∀P:lenv→term→Prop.
+ (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
+ ∀L,T. P L T.
--- /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 "Ground-2/ground.ma".
+
+(* SORT HIERARCHY ***********************************************************)
+
+(* sort hierarchy specifications *)
+record sh: Type[0] ≝ {
+ next: nat → nat; (* next sort in the hierarchy *)
+ next_lt: ∀k. k < next k (* strict monotonicity condition *)
+}.
--- /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 "Basic-2/grammar/item.ma".
+
+(* TERMS ********************************************************************)
+
+(* terms *)
+inductive term: Type[0] ≝
+| TSort: nat → term (* sort: starting at 0 *)
+| TLRef: nat → term (* reference by index: starting at 0 *)
+| TPair: item2 → term → term → term (* binary item construction *)
+.
+
+interpretation "sort (term)" 'Star k = (TSort k).
+
+interpretation "local reference (term)" 'Weight i = (TLRef i).
+
+interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
+
+interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2).
+
+interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2).
--- /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 "Basic-2/grammar/term.ma".
+
+(* WEIGHT *******************************************************************)
+
+(* the weight of a term *)
+let rec tw T ≝ match T with
+[ TSort _ ⇒ 1
+| TLRef _ ⇒ 1
+| TPair _ V T ⇒ tw V + tw T + 1
+].
+
+interpretation "weight (term)" 'Weight T = (tw T).
+
+axiom tw_wf_ind: ∀P:term→Prop.
+ (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) →
+ ∀T. P T.
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-(* Syntax *******************************************************************)
+(* Grammar ******************************************************************)
notation "hvbox( ⋆ )"
non associative with precedence 90
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/reduction/tpr.ma".
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/substitution/tps.ma".
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/substitution/lift_weight.ma".
include "Basic-2/substitution/tps_tps.ma".
include "Basic-2/reduction/tpr_lift.ma".
include "Basic-2/reduction/tpr_tps.ma".
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/substitution/leq.ma".
include "Basic-2/substitution/lift.ma".
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/syntax/length.ma".
+include "Basic-2/grammar/lenv_length.ma".
(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
-
-include "Basic-2/syntax/term.ma".
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/grammar/term_weight.ma".
(* RELOCATION ***************************************************************)
]
qed.
+(* Basic forward lemmas *****************************************************)
+
+lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #T1 = #T2.
+#d #e #T1 #T2 #H elim H -d e T1 T2; normalize //
+qed.
+
(* Basic inversion lemmas ***************************************************)
lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
+++ /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 "Basic-2/syntax/weight.ma".
-include "Basic-2/substitution/lift.ma".
-
-(* RELOCATION ***************************************************************)
-
-lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #T1 = #T2.
-#d #e #T1 #T2 #H elim H -d e T1 T2; normalize //
-qed.
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/substitution/drop.ma".
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/substitution/drop_drop.ma".
include "Basic-2/substitution/tps.ma".
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/substitution/tps_lift.ma".
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic-2/substitution/tps_split.ma".
-(*
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department of the University of Bologna, Italy.
- ||I||
- ||T||
- ||A|| This file is distributed under the terms of the
- \ / GNU General Public License Version 2
- \ /
- V_______________________________________________________________ *)
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Ground-2/xoa_props.ma".
projects / helm.git / commitdiff