- terms.ma: contains the data structure of terms and related functions (not involving substitution).
- ext_lambda.ma: cut off of previous ext.ma, containing the lambda-related objects
- subst.ma, types.ma: we removed notation from here
- types.ma: we added special cases of the weakening and thinning lemmas as axioms
(* *)
(**************************************************************************)
-include "lambda/subst.ma".
include "basics/list.ma".
-include "lambda/lambda_notation.ma".
(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
#A #P #HP #l1 elim l1 -l1 [ #l2 #H >H // ]
#x1 #l1 #IH1 #l2 elim l2 -l2 [ #false elim false ]
#x2 #l2 #_ #H elim H -H /3/
-qed.
-
-(* terms **********************************************************************)
-
-(* Appl F l generalizes App applying F to a list of arguments
- * The head of l is applied first
- *)
-let rec Appl F l on l ≝ match l with
- [ nil ⇒ F
- | cons A D ⇒ Appl (App F A) D
- ].
-
-lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
-#N #l elim l -l // #hd #tl #IHl #M >IHl //
-qed.
-
-(* FG: not needed for now
-(* nautral terms *)
-inductive neutral: T → Prop ≝
- | neutral_sort: ∀n.neutral (Sort n)
- | neutral_rel: ∀i.neutral (Rel i)
- | neutral_app: ∀M,N.neutral (App M N)
-.
-*)
-
-(* substitution ***************************************************************)
-
-(* FG: do we need this?
-definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
-
-lemma lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
- Appl (lift F p k) (map … (lift0 p k) l).
-#p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
-qed.
-*)
-
-lemma lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
-#i #p #k #Hik normalize >(le_to_leb_true … Hik) //
-qed.
-
-lemma lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
-#i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
qed.
-
-lemma lift_app: ∀M,N,k,p.
- lift (App M N) k p = App (lift M k p) (lift N k p).
-// qed.
-
-lemma lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
- Lambda (lift N k p) (lift M (k + 1) p).
-// qed.
-
-lemma lift_prod: ∀N,M,k,p.
- lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
-// qed.
-
-lemma subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
-// qed.
-
-lemma subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
-// qed.
-
-lemma subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
-// qed.
-
-
-axiom lift_subst_lt: ∀A,B,i,j,k. lift (B[j≝A]) (j+k) i =
- (lift B (j+k+1) i)[j≝lift A k i].
-
-(* telescopic delifting substitution of l in M.
- * Rel 0 is replaced with the head of l
- *)
-let rec tsubst M l on l ≝ match l with
- [ nil ⇒ M
- | cons A D ⇒ (tsubst M[0≝A] D)
- ].
-
-interpretation "telescopic substitution" 'Subst1 M l = (tsubst M l).
-
-lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[l] = t.
-#l elim l -l; normalize // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
-qed.
-
-lemma tsubst_sort: ∀n,l. (Sort n)[l] = Sort n.
-// 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 "lambda/ext.ma".
+include "lambda/subst.ma".
+
+(* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
+
+(* terms **********************************************************************)
+
+(* FG: not needed for now
+(* nautral terms *)
+inductive neutral: T → Prop ≝
+ | neutral_sort: ∀n.neutral (Sort n)
+ | neutral_rel: ∀i.neutral (Rel i)
+ | neutral_app: ∀M,N.neutral (App M N)
+.
+*)
+
+(* substitution ***************************************************************)
+
+(* FG: do we need this?
+definition lift0 ≝ λp,k,M . lift M p k. (**) (* remove definition *)
+
+lemma lift_appl: ∀p,k,l,F. lift (Appl F l) p k =
+ Appl (lift F p k) (map … (lift0 p k) l).
+#p #k #l (elim l) -l /2/ #A #D #IHl #F >IHl //
+qed.
+*)
+
+lemma lift_rel_lt: ∀i,p,k. (S i) ≤ k → lift (Rel i) k p = Rel i.
+#i #p #k #Hik normalize >(le_to_leb_true … Hik) //
+qed.
+
+lemma lift_rel_ge: ∀i,p,k. (S i) ≰ k → lift (Rel i) k p = Rel (i+p).
+#i #p #k #Hik normalize >(lt_to_leb_false (S i) k) /2/
+qed.
+
+lemma lift_app: ∀M,N,k,p.
+ lift (App M N) k p = App (lift M k p) (lift N k p).
+// qed.
+
+lemma lift_lambda: ∀N,M,k,p. lift (Lambda N M) k p =
+ Lambda (lift N k p) (lift M (k + 1) p).
+// qed.
+
+lemma lift_prod: ∀N,M,k,p.
+ lift (Prod N M) k p = Prod (lift N k p) (lift M (k + 1) p).
+// qed.
+
+lemma subst_app: ∀M,N,k,L. (App M N)[k≝L] = App M[k≝L] N[k≝L].
+// qed.
+
+lemma subst_lambda: ∀N,M,k,L. (Lambda N M)[k≝L] = Lambda N[k≝L] M[k+1≝L].
+// qed.
+
+lemma subst_prod: ∀N,M,k,L. (Prod N M)[k≝L] = Prod N[k≝L] M[k+1≝L].
+// qed.
+
+
+axiom lift_subst_lt: ∀A,B,i,j,k. lift (B[j≝A]) (j+k) i =
+ (lift B (j+k+1) i)[j≝lift A k i].
+
+(* telescopic delifting substitution of l in M.
+ * Rel 0 is replaced with the head of l
+ *)
+let rec tsubst M l on l ≝ match l with
+ [ nil ⇒ M
+ | cons A D ⇒ (tsubst M[0≝A] D)
+ ].
+
+interpretation "telescopic substitution" 'Subst M l = (tsubst M l).
+
+lemma tsubst_refl: ∀l,t. (lift t 0 (|l|))[/l] = t.
+#l elim l -l; normalize // #hd #tl #IHl #t cut (S (|tl|) = |tl| + 1) // (**) (* eliminate cut *)
+qed.
+
+lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n.
+// qed.
(* lifting, substitution *)
-notation "hvbox(M break [ l ])"
+notation "hvbox(↑ [ p break , k ] break t)"
+ non associative with precedence 50
+ for @{'Lift1 $p $k $t}.
+
+notation "hvbox(M break [ / l ])"
+ non associative with precedence 90
+ for @{'Subst $M $l}.
+
+notation "hvbox(M break [ k ≝ N ])"
non associative with precedence 90
- for @{'Subst1 $M $l}.
+ for @{'Subst1 $M $k $N}.
+
+(* type judgements *)
+
+notation "hvbox(G break ⊢ A break : B)"
+ non associative with precedence 45
+ for @{'TJ $G $A $B}.
+
+notation "hvbox(G break ⊢ A break ÷ B)"
+ non associative with precedence 45
+ for @{'TJ0 $G $A $B}.
-(* interpretation *)
+(* interpretations *)
-notation "hvbox(〚term 90 T〛)"
+notation "hvbox(║T║)"
non associative with precedence 50
for @{'IInt $T}.
-notation "hvbox(〚term 90 T〛 break _ [term 90 E])"
+notation "hvbox(║T║ break _ [E])"
non associative with precedence 50
for @{'IInt1 $T $E}.
-notation "hvbox(〚term 90 T〛 break _ [term 90 E1 break , term 90 E2])"
+notation "hvbox(║T║ break _ [E1 break , E2])"
non associative with precedence 50
for @{'IInt2 $T $E1 $E2}.
-notation "hvbox(ã\80\8aterm 90 Tã\80\8b)"
+notation "hvbox(ã\80\9aTã\80\9b)"
non associative with precedence 50
for @{'EInt $T}.
-notation "hvbox(ã\80\8aterm 90 Tã\80\8b break _ [term 90 E])"
+notation "hvbox(ã\80\9aTã\80\9b break _ [E])"
non associative with precedence 50
for @{'EInt1 $T $E}.
-notation "hvbox(ã\80\8aterm 90 Tã\80\8b break _ [term 90 E1 break , term 90 E2])"
+notation "hvbox(ã\80\9aTã\80\9b break _ [E1 break , E2])"
non associative with precedence 50
for @{'EInt2 $T $E1 $E2}.
+
+notation "hvbox(《T》)"
+ non associative with precedence 50
+ for @{'XInt $T}.
+
+notation "hvbox(《T》 break _ [E])"
+ non associative with precedence 50
+ for @{'XInt1 $T $E}.
+
+notation "hvbox(《T》 break _ [E1 break , E2])"
+ non associative with precedence 50
+ for @{'XInt2 $T $E1 $E2}.
\ /
V_______________________________________________________________ *)
-include "arithmetics/nat.ma".
-
-inductive T : Type[0] ≝
- | Sort: nat → T (* starts from 0 *)
- | Rel: nat → T (* starts from ... ? *)
- | App: T → T → T (* function, argument *)
- | Lambda: T → T → T (* type, body *)
- | Prod: T → T → T (* type, body *)
- | D: T → T (* dummifier *)
-.
+include "lambda/terms.ma".
(* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
let rec lift t k p ≝
notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
*)
-notation "M [ k := N ]" non associative with precedence 90 for @{'Subst $M $k $N}.
-
(* interpretation "Subst" 'Subst N M = (subst N M). *)
-interpretation "Subst" 'Subst M k N = (subst M k N).
+interpretation "Subst" 'Subst1 M k N = (subst M k N).
(*** properties of lift and subst ***)
--- /dev/null
+(*
+ ||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 "basics/list.ma".
+include "lambda/lambda_notation.ma".
+
+inductive T : Type[0] ≝
+ | Sort: nat → T (* starts from 0 *)
+ | Rel: nat → T (* starts from 0 *)
+ | App: T → T → T (* function, argument *)
+ | Lambda: T → T → T (* type, body *)
+ | Prod: T → T → T (* type, body *)
+ | D: T → T (* dummifier *)
+.
+
+(* Appl F l generalizes App applying F to a list of arguments
+ * The head of l is applied first
+ *)
+let rec Appl F l on l ≝ match l with
+ [ nil ⇒ F
+ | cons A D ⇒ Appl (App F A) D
+ ].
+
+lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
+#N #l elim l -l // #hd #tl #IHl #M >IHl //
+qed.
| dummy: ∀G.∀A,B.∀i.
TJ G A B → TJ G B (Sort i) → TJ G (D A) B.
-notation "hvbox(G break ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
interpretation "type judgement" 'TJ G A B = (TJ G A B).
(* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
#G1 #D #N #Heq #tjN @dummy /2/
]
qed.
+
+(* weakening lemma: special case *)
+axiom tj_weak_1: ∀G,t,u. G ⊢ t : u → ∀w. w :: G ⊢ lift t 0 1 : lift u 0 1.
+
+
+(* thinning lemma: special case *)
+axiom tj_thin_1: ∀w,G,t,u. w :: G ⊢ lift t 0 1 : lift u 0 1 → G ⊢ t : u.
projects / helm.git / commitdiff