From ffbc6cd1358d61072105766052c7498a1f37c769 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 22 Mar 2011 18:53:26 +0000 Subject: [PATCH] - lambda_notation.ma: more notation and bug fixes - 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 --- matita/matita/lib/lambda/ext.ma | 86 -------------------- matita/matita/lib/lambda/ext_lambda.ma | 90 +++++++++++++++++++++ matita/matita/lib/lambda/lambda_notation.ma | 48 ++++++++--- matita/matita/lib/lambda/subst.ma | 15 +--- matita/matita/lib/lambda/terms.ma | 34 ++++++++ matita/matita/lib/lambda/types.ma | 8 +- 6 files changed, 172 insertions(+), 109 deletions(-) create mode 100644 matita/matita/lib/lambda/ext_lambda.ma create mode 100644 matita/matita/lib/lambda/terms.ma diff --git a/matita/matita/lib/lambda/ext.ma b/matita/matita/lib/lambda/ext.ma index 2e2f30359..7e64aba31 100644 --- a/matita/matita/lib/lambda/ext.ma +++ b/matita/matita/lib/lambda/ext.ma @@ -12,9 +12,7 @@ (* *) (**************************************************************************) -include "lambda/subst.ma". include "basics/list.ma". -include "lambda/lambda_notation.ma". (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************) @@ -115,88 +113,4 @@ lemma all2_symmetric: ∀A. ∀P:A→A→Prop. symmetric … P → symmetric … #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. diff --git a/matita/matita/lib/lambda/ext_lambda.ma b/matita/matita/lib/lambda/ext_lambda.ma new file mode 100644 index 000000000..952161107 --- /dev/null +++ b/matita/matita/lib/lambda/ext_lambda.ma @@ -0,0 +1,90 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma index 26185019a..a5fb014ed 100644 --- a/matita/matita/lib/lambda/lambda_notation.ma +++ b/matita/matita/lib/lambda/lambda_notation.ma @@ -34,32 +34,62 @@ notation "hbox((! ^ term 90 b) term 50 a)" (* 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(《term 90 T》)" +notation "hvbox(〚T〛)" non associative with precedence 50 for @{'EInt $T}. -notation "hvbox(《term 90 T》 break _ [term 90 E])" +notation "hvbox(〚T〛 break _ [E])" non associative with precedence 50 for @{'EInt1 $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 @{'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}. diff --git a/matita/matita/lib/lambda/subst.ma b/matita/matita/lib/lambda/subst.ma index 565432a9d..ac0480224 100644 --- a/matita/matita/lib/lambda/subst.ma +++ b/matita/matita/lib/lambda/subst.ma @@ -9,16 +9,7 @@ \ / 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 ≝ @@ -56,10 +47,8 @@ ndefinition subst ≝ λa.λt.subst_aux t 0 a. 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 ***) diff --git a/matita/matita/lib/lambda/terms.ma b/matita/matita/lib/lambda/terms.ma new file mode 100644 index 000000000..915c13446 --- /dev/null +++ b/matita/matita/lib/lambda/terms.ma @@ -0,0 +1,34 @@ +(* + ||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. diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma index 543b3b7b9..dd730bf3b 100644 --- a/matita/matita/lib/lambda/types.ma +++ b/matita/matita/lib/lambda/types.ma @@ -53,7 +53,6 @@ inductive TJ: list T → T → T → Prop ≝ | 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. *) @@ -212,3 +211,10 @@ theorem substitution_tj: #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. -- 2.39.2