]> matita.cs.unibo.it Git - helm.git/commitdiff
- lambda_notation.ma: more notation and bug fixes
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 22 Mar 2011 18:53:26 +0000 (18:53 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 22 Mar 2011 18:53:26 +0000 (18:53 +0000)
- 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
matita/matita/lib/lambda/ext_lambda.ma [new file with mode: 0644]
matita/matita/lib/lambda/lambda_notation.ma
matita/matita/lib/lambda/subst.ma
matita/matita/lib/lambda/terms.ma [new file with mode: 0644]
matita/matita/lib/lambda/types.ma

index 2e2f30359e991f52deef558948f631c13d8cff0f..7e64aba31ff7d40ca240c63052a2c0769fffa7f3 100644 (file)
@@ -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 (file)
index 0000000..9521611
--- /dev/null
@@ -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.
index 26185019a6653cecf97dd1a5fbf4cb2860868d18..a5fb014ed7d284cc6cc493bd969c351baa297ef6 100644 (file)
@@ -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(ã\80\8aterm 90 Tã\80\8b)"
+notation "hvbox(ã\80\9a\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\9a\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\9a\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}.
index 565432a9dfb3c29231e9272df2f7cbc67e8ed55f..ac0480224d7cc74fa39b3905ca031805efc0e07d 100644 (file)
@@ -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 (file)
index 0000000..915c134
--- /dev/null
@@ -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.
index 543b3b7b9e8dd182580f781273b7e377df69a58f..dd730bf3be9b503b270f5853ac72bdfbc93e7bf0 100644 (file)
@@ -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.